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);;