demoml/demo.ml

64 lines
1.9 KiB
OCaml

type formule =
| Atome of string
| Et of formule * formule
| Ou of formule * formule
| Non of formule
| Fleche of formule * formule;;
let rec appartient x l =
match l with
| [] -> false
| t::q -> (x = t) || appartient x q;;
let rec commun l1 l2 = (*definition d'axiome*)
match l1 with
| [] -> false
| t::q -> (appartient t l2) || (commun q l2);;
let rec addgauche f l =
match l with
| [] -> []
| t::q -> match t with (x,y) -> (f::x,y)::(addgauche f q);;
let rec adddroite f l =
match l with
| [] -> []
| t::q -> match t with (x,y) -> (x,f::y)::(adddroite f q);;
(* Les deux fonctions precedentes ne sont utilisees qu'une fois, et il faut juste
* savoir qu'elles permettent de considerer le cas "atomique" d'une formule*)
let rec atomique f = (*teste si une liste de formule est inexpendable*)
match f with
| [] -> true
| t::q -> match t with
| Atome(a) -> atomique q
| _ -> false;;
let rec developgauche f g = (*Application des regles gauches*)
match f with
| [] -> [(f,g)]
| t::q -> match t with
| Atome(a) -> addgauche t (developgauche q g)
| Et(a,b) -> [((a::b::q),g)]
| Ou(a,b) -> [((a::q),g);((b::q),g)]
| Non(a) -> [(q,(a::g))]
| Fleche(a,b) -> [(q,(a::g));((b::q),g)];;
let rec developdroite f g = (*Application des regles droites*)
match g with
| [] -> [(f,g)]
| t::q -> match t with
| Atome(a) -> adddroite t (developdroite f q)
| Et(a,b) -> [(f,(a::q));(f,(b::q))]
| Ou(a,b) -> [(f,(a::b::q))]
| Non(a) -> [((a::f),q)]
| Fleche(a,b) -> [((a::f),(b::q))];;
let rec calcul l =
match l with
| [] -> true
| (f,g)::q -> if atomique f then if atomique g then (commun f g) && (calcul q)
else (calcul (developdroite f g)) && (calcul q)
else (calcul (developgauche f g)) && (calcul q);;