Logique des propositions en Haskell part I

---- Last modified: <MD1_logique.hs modifié par  Guillaume CONNAN le vendredi 6 septembre 2013 à 11h 43min 49s>
 
 
import qualified Data.Map as Dic
import qualified Data.Set as Set
 
type Atome = Char
type Environnement = Dic.Map Atome Bool
 
data Formule =
  Antitruc
  |Atomic Atome
  |Non Formule
  |Et Formule Formule
  |Ou Formule Formule
  |Imp Formule Formule
  |Equiv Formule Formule deriving (Eq)
 
-- Opérateurs infixes plus pratiques à utiliser
µ x = Atomic x
 
infixr 2 & 
x & y = Et x y
 
infixr 2 §
x § y = Ou x y
        
infixr 1 ==>
x ==> y = Imp x y
 
infixr 1 <==>
x <==> y = Equiv x y
 
-- exemple de formule
-- de_morg = Equiv (Non (Et (Atomic 'p') (Atomic 'q')))  (Ou (Non (Atomic 'p')) (Non (Atomic 'q')))
de_morg = Non ((µ 'p') & (µ 'q')) <==> (Non (µ 'p') § Non (µ 'q'))
 
 
-- fonction sur les formules
f :: Formule -> Formule -> Formule -> Formule -> Formule
f p q r s =
  s ==> (p & (Non (q))) § (p <==> (Non r))
 
-- exemple d'environnement
env1 = Dic.fromList[('p',True),('q',False)]
 
-- évaluation récursive d'une formule sous un environnement
eval :: Formule -> Environnement -> Bool
eval Antitruc env        = False
eval (Atomic a) env  = env Dic.! a
eval (Non f) env     = if (eval f env) then False else True
eval (Et f g) env    = if (eval f env) then (eval g env) else False
eval (Ou f g) env    = if (eval f env) then True else (eval g env)
eval (Imp f g) env   = eval (Non (f & (Non g))) env
eval (Equiv f g) env = eval ((f & g) §  ((Non f) & (Non g))) env 
 
-- renvoie l'ensemble des atomes présents dans une formule
ens_atomes :: Formule -> Set.Set Atome
ens_atomes Antitruc        = Set.empty
ens_atomes (Atomic a)  = Set.singleton a
ens_atomes (Non f)     = ens_atomes f
ens_atomes (Et f g)    = Set.union (ens_atomes f ) (ens_atomes g ) 
ens_atomes (Ou f g)    = Set.union (ens_atomes f ) (ens_atomes g )
ens_atomes (Imp f g)   = Set.union (ens_atomes f ) (ens_atomes g )
ens_atomes (Equiv f g) = Set.union (ens_atomes f ) (ens_atomes g )  
 
-- "dit" la formule comme on l'énonce habituellement
dit :: Formule -> String
dit Antitruc        = "Antitruc"
dit (Non Antitruc)  = "Vrai"
dit (Atomic a)  = [a]
dit (Non p)     = "Non " ++ (dit p)
dit (Et p q)    = "( " ++ (dit p) ++ " et " ++ (dit q) ++ " )"
dit (Ou p q)    = "( " ++ (dit p) ++ " ou " ++ (dit q) ++ " )"
dit (Imp p q)   = "( " ++ (dit p) ++ " implique " ++ (dit q) ++ " )"
dit (Equiv p q) = "( " ++ (dit p) ++ " equivaut a " ++ (dit q) ++ " )"
 
instance Show Formule where 
  show  = dit 
 
-- renvoie la liste de tous les environnements de taille n 
-- on nomme les atomes dans l'ordre alpha à partir de ini
tous_les_env :: Int -> Atome -> [Environnement]
tous_les_env 0 ini = [Dic.empty]
tous_les_env n ini =
  let insere v dic = Dic.insert  ini v dic in
  (map (\d -> insere True  d) (tous_les_env (n-1) (succ ini))) ++ 
  (map (\d -> insere False d) (tous_les_env (n-1) (succ ini)))
  
-- teste si une formule est une tautologie
est_tautologie :: Formule -> Bool
est_tautologie f =
  let ens = ens_atomes f in 
  let ini = Set.findMin ens in
  let n = Set.size ens in
  and $ map (\env -> eval f env) (tous_les_env n ini)
 
-- renvoie la table de vérité sous forme d'une liste de couples (envir, valeur)
liste_verite :: Formule -> [([(Atome,Bool)],Bool)]
liste_verite f =
  let ens = ens_atomes f in 
  let ini = Set.findMin ens in
  let n = Set.size ens in
  map (\env -> (Dic.toList env,eval f env)) (tous_les_env n ini)
 
-- joli (?) affichage de la table de vérité
table_verite :: Formule -> IO ()
table_verite f =
  let lv = liste_verite f in
  let s = foldl (++) "" [(show (fst c)) ++ " --> " ++ (show (snd c)) ++ "\n" | c <- lv] in
  putStrLn s