open Symb
open Fol


let rec string_of_terme (_, t) = match t with
  | `Constant i -> i
  | `Variable i -> i
  | `Function (f, l) -> f ^ " (" ^ String.concat ", " (List.map string_of_terme l) ^ ")"

type negsimpl_formula = [
| boool
| fol_atom
| `Negation of fol_atom
| `Conjunction of negsimpl_formula list
| `Disjunction of negsimpl_formula list
| `Exists of (ident * basesort) list * negsimpl_formula
| `Forall of (ident * basesort) list * negsimpl_formula
]

(*
let rec negsimpl_coerce : negsimpl_formula -> fol_formula = function
  | `Negation f -> `Negation (negsimpl_coerce (f :> negsimpl_formula))
  | `Conjunction l -> `Conjunction (List.map negsimpl_coerce l)
  | `Disjunction l -> `Disjunction (List.map negsimpl_coerce l)
  | `Exists (l, f) -> `Exists (l, negsimpl_coerce f)
  | `Forall (l, f) -> `Forall (l, negsimpl_coerce f)
  | `True | `False | `Predicate _ | `Equality _ as f -> f
*)

let rec neg_simpl : fol_formula -> negsimpl_formula = function
  | `Negation f -> begin match f with
      | `Negation g -> neg_simpl g
      | `True -> `False
      | `False -> `True
      | `Forall (l, h) -> neg_simpl (`Exists (l, (`Negation h)))
      | `Exists (l, h) -> neg_simpl (`Forall (l, (`Negation h)))
      | `Disjunction l -> neg_simpl (`Conjunction (List.map (fun h -> `Negation h) l))
      | `Conjunction l -> neg_simpl (`Disjunction (List.map (fun h -> `Negation h) l))
      | #fol_atom as g -> `Negation g
    end
  | `Conjunction l -> `Conjunction (List.map neg_simpl l)
  | `Disjunction l -> `Disjunction (List.map neg_simpl l)
  | `Forall (l, f) -> `Forall (l, neg_simpl f)
  | `Exists (l, f) -> `Exists (l, neg_simpl f)
  | #boool | #fol_atom as g -> g

let rec eg sigma (_, t1) (_, t2) =
  match t1 with
    | `Variable i -> begin match t2 with
        | `Variable j -> sigma i = sigma j
        | _ -> false
      end
    | `Function (f, l) -> begin match t2 with
        | `Function (g, m) -> f = g && List.for_all2 (eg sigma) l m
        | _ -> false
      end
    | _ -> t1 = t2

let termes_egaux t1 t2 = eg (fun x -> x) t1 t2

(*
let rec termes_egaux (_, t1) (_, t2) =
  match t1 with
    | `Function (f, l) -> begin match t2 with
        | `Function (g, m) -> f = g && List.for_all2 termes_egaux l m
        | _ -> false
      end
    | _ -> t1 = t2
*)


let rec terme_frais od (_, t) = match t with
  | `Variable v -> v <> od
  | `Function (_, tl) -> List.for_all (terme_frais od) tl
  | _ -> true

let rec formule_fraiche (od : ident) : fol_formula -> bool = function
  | `Equality (t1, t2) -> terme_frais od t1 && terme_frais od t2
  | `Predicate (_, l) -> List.for_all (terme_frais od) l
  | `Negation f -> formule_fraiche od f
  | `Conjunction l | `Disjunction l -> List.for_all (formule_fraiche od) l
  | `Exists (l, _) when List.mem_assoc od l -> true
  | `Forall (l, _) when List.mem_assoc od l -> true
  | `Exists (_, f) | `Forall (_, f) -> formule_fraiche od f
  | _ -> true

let terme_frais_scope t = List.for_all (fun v -> terme_frais v t)

let subst_naive_negation od nw f = match subst_naive_atome od nw f with
  | `True -> `False
  | `False -> `True
  | #fol_atom as f -> `Negation f

let subst_naive od nw : negsimpl_formula -> negsimpl_formula =
  subst_naive_aux subst_naive_negation od nw

let rec aux_uniformiser accu_v accu_f = function
  | [] -> (accu_v, accu_f)
  | ((v, t)::q) ->
      let v2 = nouveau_symbole v in
(*      prerr_endline ("alpha : " ^ v ^ " := " ^ v2); *)
      aux_uniformiser ((v2, t)::accu_v) (subst_naive v (`Unknown, `Variable v2) accu_f) q

and uniformiser = function
  | `Exists (l, f) -> `Exists (aux_uniformiser [] (uniformiser f) l)
  | `Forall (l, f) -> `Forall (aux_uniformiser [] (uniformiser f) l)
  | `Conjunction l -> `Conjunction (List.rev_map uniformiser l)
  | `Disjunction l -> `Disjunction (List.rev_map uniformiser l)
  | f -> f


let rec alleger accu f = function
  | [] -> accu
  | (v, _)::q when formule_fraiche v f -> alleger accu f q
  | v::q -> alleger (v::accu) f q

let rec bool_simpl : negsimpl_formula -> negsimpl_formula = function
  | `Conjunction l ->
      let l2 = List.rev_map bool_simpl l in
      let rec aux accu = function
        | [] -> accu
        | `True::q -> aux accu q
        | `False::_ -> [`False]
        | a::q -> aux (a::accu) q
      in begin match aux [] l2 with
        | [] -> `True
        | [f] -> f
        | l3 -> `Conjunction l3
      end
  | `Disjunction l ->
      let l2 = List.rev_map bool_simpl l in
      let rec aux accu = function
        | [] -> accu
        | `False::q -> aux accu q
        | `True::_ -> [`True]
        | a::q -> aux (a::accu) q
      in begin match aux [] l2 with
        | [] -> `False
        | [f] -> f
        | l3 -> `Disjunction l3
      end
  | `Exists (l, f) -> let f2 = bool_simpl f in
    begin match alleger [] (f2 : negsimpl_formula :> fol_formula) l with
      | [] -> f2
      | l2 -> `Exists (l2, f2)
    end
  | `Forall (l, f) -> let f2 = bool_simpl f in begin match alleger [] (f2 : negsimpl_formula :> fol_formula) l with
      | [] -> f2
      | l2 -> `Forall (l2, f2)
    end
  | `Equality (t1, t2) when termes_egaux t1 t2 -> `True
  | f -> f


let rec quant_simpl : negsimpl_formula -> negsimpl_formula = function
  | `Exists ([], f0) -> quant_simpl f0
  | `Exists (((v, _) as k)::q, f0) ->
      let f = quant_simpl (`Exists (q, f0)) in
      let rec aux_v scope conj = function
        | [] -> None
        | [`Equality ((_, `Variable v1), v2)] 
            when (v1 = v) && terme_frais v1 v2 ->
            Some (v2, (scope, conj))
        | [`Equality (v2, (_, `Variable v1))] 
            when (v1 = v) && terme_frais v1 v2 ->
            Some (v2, (scope, conj))
        | [`Conjunction l] -> aux_v scope conj l
        | [`Exists (l', f')] ->
            if List.mem_assoc v l'
            then None
            else aux_v (l' @ scope) conj [f']
        | [_] -> None
        | a::r -> begin match aux_v scope conj [a] with
            | None -> aux_v scope (a::conj) r
            | Some (v2, (scope2, conj2)) -> Some (v2, (scope2, conj2 @ r))
          end
      in begin match aux_v [] [] [f] with
        | None -> `Exists ([k], f)
        | Some (v2, (scope, conj)) -> begin
            prerr_endline ("Dropped : " ^ v ^ " := " ^ string_of_terme v2) ;
            bool_simpl (`Exists (scope, subst_naive v v2 (`Conjunction conj)))
          end
      end

  | `Forall ([], f0) -> quant_simpl f0

  | `Forall (((v, _) as k)::q, f0) ->
      let f = quant_simpl (`Forall (q, f0)) in
      let rec aux_v scope conj = function
        | [] -> None
        | [`Negation (`Equality ((_, `Variable v1), v2))] 
            when (v1 = v) && terme_frais v1 v2 ->
            Some (v2, (scope, conj))
        | [`Negation (`Equality (v2, (_, `Variable v1)))] 
            when (v1 = v) && terme_frais v1 v2 ->
            Some (v2, (scope, conj))
        | [`Disjunction l] -> aux_v scope conj l
        | [`Forall (l', f')] ->
            if List.mem_assoc v l'
            then None
            else aux_v (l' @ scope) conj [f']
        | [_] -> None
        | a::r -> begin match aux_v scope conj [a] with
            | None -> aux_v scope (a::conj) r
            | Some (v2, (scope2, conj2)) -> Some (v2, (scope2, conj2 @ r))
          end
      in begin match aux_v [] [] [f] with
        | None -> `Forall ([k], f)
        | Some (v2, (scope, conj)) -> begin
            prerr_endline ("Dropped : " ^ v ^ " := " ^ string_of_terme v2) ;
            bool_simpl (`Forall (scope, subst_naive v v2 (`Disjunction conj)))
          end
      end
  | `Conjunction l -> bool_simpl (`Conjunction (List.rev_map quant_simpl l))
  | `Disjunction l -> bool_simpl (`Disjunction (List.rev_map quant_simpl l))
  | f -> bool_simpl f

let implique_atom sigma a b = match a with
  | `Predicate (f, l) -> begin match b with
      | `Predicate (g, m) -> f = g && List.for_all2 (eg sigma) l m
      | _ -> false
    end
  | `Equality (u, v) -> begin match b with
      | `Equality (s, t) -> let e = (eg sigma) in let eu = e u and ev = e v in (eu s && ev t) || (eu t && ev s)
      | _ -> false
    end
  | _ -> false (* a = b *)

let rec maj_sigma_2 (sigma : 'a -> 'a) (l : ('a * 'a) list) (v : 'a) : 'a = match l with
  | [] -> sigma v
  | ((x, z)::_) when x = v -> z
  | _::q -> maj_sigma_2 sigma q v

let maj_sigma sigma l = match l with
  | [] -> sigma
  | _ -> maj_sigma_2 sigma l

let rec auximpli (sigma : 'a -> 'a) (u : ('a * 'b) list) (v : ('a * 'b) list) (accu : ('a * 'a) list) : (('a -> 'a) option) = match u with
  | [] -> begin match v with
      | [] -> Some (maj_sigma sigma accu)
      | _ -> None
    end
  | ((x, _)::q) -> begin match v with
      | ((y, _)::r) ->
          let z = nouveau_symbole "implique" in
          auximpli sigma q r ((y, z)::(x, z)::accu)
      | _ -> None
    end

let rec unifier l m f g = match l, m with
| [], [] -> Some (f, g)
| (x, _)::q, (y, _)::r ->
let z = `Unknown, `Variable (nouveau_symbole "unifier") in
 unifier q r (subst_naive x z f) (subst_naive y z g)
| _ -> None

let eqvars l m = List.for_all2 (fun (x, _) (y, _) -> x = y) l m

let rec non_impli sigma a b = match a, b with
  | `True, _ | _, `True -> true
  | `Conjunction l, _ -> List.for_all (fun h -> non_impli sigma h b) l
  | _, `Conjunction l -> List.for_all (non_impli sigma a) l
  | _, `Disjunction l -> List.exists (non_impli sigma a) l
  | `Disjunction l, _ -> List.exists (fun h -> non_impli sigma h b) l
  | #fol_atom as c, `Negation d -> implique_atom sigma d c
  | `Exists (l, f), `Forall (m, g) | `Forall (l, f), `Exists (m, g) ->
      (* begin match auximpli sigma l m [] with
        | None -> false
        | Some sigma2 -> non_impli sigma2 f g
      end *)
      eqvars l m && non_impli sigma f g (*
      begin match unifier l m f g with
       | Some (f', g') -> non_impli sigma f' g'
       | None -> false
      end *)
  | `Negation c, (#fol_atom as d) -> implique_atom sigma c d
  | _ -> false (* a = b *)


let rec impli_non sigma a b = match a, b with
  | `False, _ | _, `False -> true
  | `Disjunction l, _ -> List.for_all (fun h -> impli_non sigma h b) l
  | _, `Disjunction l -> List.for_all (impli_non sigma a) l
  | _, `Conjunction l -> List.exists (impli_non sigma a) l
  | `Conjunction l, _ -> List.exists (fun h -> impli_non sigma h b) l
  | `Negation c, (#fol_atom as d) -> implique_atom sigma d c
  | `Forall (l, f), `Exists (m, g) | `Exists (l, f), `Forall (m, g) ->
      (* begin match auximpli sigma l m [] with
        | None -> false
        | Some sigma2 -> impli_non sigma2 f g
      end *)
      eqvars l m && impli_non sigma f g (*
      begin match unifier l m f g with
       | Some (f', g') -> impli_non sigma f' g'
       | None -> false
      end *)
  | #fol_atom as c, `Negation d -> implique_atom sigma c d
  | _ -> false (* a = b *) 

let rec impli sigma a b = match a, b with
  | `False, _ | _, `True -> true
  | `Disjunction l, _ -> List.for_all (fun h -> impli sigma h b) l
  | _, `Conjunction l -> List.for_all (impli sigma a) l
  | _, `Disjunction l -> List.exists (impli sigma a) l
  | `Conjunction l, _ -> List.exists (fun h -> impli sigma h b) l
  | `Negation c, `Negation d -> implique_atom sigma d c
  | `Forall (l, f), `Forall (m, g) | `Exists (l, f), `Exists (m, g) ->
      (* begin match auximpli sigma l m [] with
        | None -> false
        | Some sigma2 -> impli sigma2 f g
      end *)
      eqvars l m && impli sigma f g (*
      begin match unifier l m f g with
       | Some (f', g') -> impli sigma f' g'
       | None -> false
      end *)
  | #fol_atom as c, (#fol_atom as d) -> implique_atom sigma c d
  | _ -> false (* a = b *)



(*
let rec impli a b =
  a = `False || b = `True || match a with
    | `Disjunction l -> List.for_all (fun h -> impli h b) l
    | _ -> begin match b with
        | `Conjunction l -> List.for_all (impli a) l
        | `Disjunction l -> List.exists (impli a) l
        | _ -> begin match a with
            | `Disjunction l -> List.exists (fun h -> impli h b) l
            | `Negation c -> begin match b with
                | `Negation d -> implique_atom d c
                | _ -> false
              end 
            | `Forall (l, c) -> begin match b with
                | `Forall (m, d) -> eqvars l m && (impli c d)
                | _ -> false
              end
            | `Exists (l, c) -> begin match b with
                | `Exists (m, d) -> eqvars l m && (impli c d)
                | _ -> false
              end
            | #fol_atom as c -> begin match b with
                | #fol_atom as d -> implique_atom c d
                | _ -> false
              end
            | _ -> a = b
          end
      end

let rec impli sigma a b =
  a = `False || b = `True || match a with
    | `Disjunction l -> List.for_all (fun h -> impli sigma h b) l
    | _ -> begin match b with
        | `Conjunction l -> List.for_all (impli sigma a) l
        | `Disjunction l -> List.exists (impli sigma a) l
        | _ -> begin match a with
            | `Disjunction l -> List.exists (fun h -> impli sigma h b) l
            | `Negation c -> begin match b with
                | `Negation d -> implique_atom sigma d c
                | _ -> false
              end 
            | `Forall (l, c) -> begin match b with
                | `Forall (m, d) -> begin match auximpli sigma l m [] with
                    | None -> false
                    | Some sigma2 -> impli sigma2 c d
                  end
                | _ -> false
              end
            | `Exists (l, c) -> begin match b with
                | `Exists (m, d) -> begin match auximpli sigma l m [] with
                    | None -> false
                    | Some sigma2 -> impli sigma2 c d
                  end
                | _ -> false
              end
            | #fol_atom as c -> begin match b with
                | #fol_atom as d -> implique_atom sigma c d
                | _ -> false
              end
            | _ -> a = b
          end
      end
*)

let impl_k = ref 0

let implique a b =
  (*
  incr impl_k;
  impl_k := !impl_k mod 1000000;
    if !impl_k = 0 then (
     Gc.full_major (); 
    prerr_string "."; flush stderr; 
  ); *)
  impli (fun x -> x) a b

let recip impl a b = impl b a

let ajout_hyp impl f l =
  if List.exists (impl f) l then (
    l 
  ) else if List.exists (recip impl f) l then
  let rec aux accu = function
    | [] -> f::accu
    | c::s when impl c f ->
        aux accu s
    | c::s -> aux (c::accu) s
  in aux [] l
  else (
    (f::l)
  )

let ajout_concl impl = ajout_hyp (recip impl)

let elim_hyp impl =
  let rec aux accu = function
  | [] -> accu
  | a::q -> aux (ajout_hyp impl a accu) q
  in aux []

let elim_concl impl = elim_hyp (recip impl)

let eliminer_hypotheses = elim_hyp implique
let eliminer_conclusions = elim_concl implique

let rec elaguer = function
  | `Conjunction l -> bool_simpl (`Conjunction (eliminer_conclusions (List.rev_map elaguer l)))
  | `Disjunction l -> bool_simpl (`Disjunction (eliminer_hypotheses (List.rev_map elaguer l)))
  | `Forall (l, f) -> bool_simpl (`Forall (l, elaguer f))
  | `Exists (l, f) -> bool_simpl (`Exists (l, elaguer f))
  | f -> bool_simpl f



(* NF algorithm *)

type forme_atome = [
| boool
| fol_atom
| `Negation of fol_atom
]

type forme_stricte = [
| `Forall of (ident * basesort) list * forme_ou_stricte
| `Exists of (ident * basesort) list * forme_et_stricte
| forme_atome
]
and forme_ou = [
| `Disjunction of forme_et_stricte list
]
and forme_et = [
| `Conjunction of forme_ou_stricte list
]
and forme_et_stricte = [
| `Conjunction of forme_stricte list
]
and forme_ou_stricte = [
| `Disjunction of forme_stricte list
]


let impl_stricte = (implique : negsimpl_formula -> negsimpl_formula -> bool :> forme_stricte -> forme_stricte -> bool)
let impl_et_stricte = (implique : negsimpl_formula -> negsimpl_formula -> bool :> forme_et_stricte -> forme_et_stricte -> bool)
let impl_ou_stricte = (implique : negsimpl_formula -> negsimpl_formula -> bool :> forme_ou_stricte -> forme_ou_stricte -> bool)

let ajout_hyp_stricte = ajout_hyp impl_stricte
let ajout_concl_stricte = ajout_concl impl_stricte

let elim_hyp_et = elim_hyp impl_et_stricte
let elim_concl_ou = elim_concl impl_ou_stricte

let elim_hyp_str = elim_hyp impl_stricte
let elim_concl_str = elim_concl impl_stricte

let rec nier_stricte = function
  | `Negation (#fol_atom as at) -> at
  | `Forall (l, f) -> `Exists (l, nier_ou_stricte f)
  | `Exists (l, f) -> `Forall (l, nier_et_stricte f)
  | `True -> `False
  | `False -> `True
  | #fol_atom as at -> `Negation at

and nier_et_stricte (`Conjunction l) = `Disjunction (List.rev_map nier_stricte l)

and nier_ou_stricte (`Disjunction l) = `Conjunction (List.rev_map nier_stricte l)

let rec contrad_stricte_et = function
  | [] -> false
  | a::q -> List.exists (fun b -> let c = nier_stricte b in impl_stricte a c) q || contrad_stricte_et q

let rec contrad_stricte_ou = function
  | [] -> false
  | a::q -> List.exists (fun b -> let c = nier_stricte b in impl_stricte c a) q || contrad_stricte_ou q

let ou_contrad (`Disjunction l as e) =
  if contrad_stricte_ou l then (
    prerr_endline "contradiction disjointe !";
    `Disjunction [`True]
  ) else e

let et_contrad (`Conjunction l as e) =
  if contrad_stricte_et l then (
    prerr_endline "contradiction conjointe !";
    `Conjunction [`False]
  ) else e




(*
  Distribution

  CONVENTION

  If the distribution function below is given the usual implication
  function, then it is assumed to take a list of disjoined conjunctions -
  that is : it takes [[a1; a2]; [b1; b2]] as input, that represents (a1 &
  a2) | (b1 & b2) - and to return a list of conjoined disjunctions - - that
  is : to return (in a probably different order) [[a1; b1]; [a1; b2]; [a2;
  b1]; [a2; b2]] that represents (a1 | b1) & (a1 | b2) & (a2 | b1) & (a2 |
  b2) -.

  To use it for the other purpose, just pass it the reciprocal implication.

  Okay ?!

  Tahina Ramananandro, 2006-07-06
*)

let ajout_clause impl =
  ajout_concl (fun hl cl ->
    List.for_all (fun h -> List.exists (fun c -> impl h c) cl) hl)
    


let rec auxpasse impl accu accu0 = function      
  | [] -> accu
  | b1::bf -> 
      auxpasse impl (aux accu0 impl b1 bf accu accu0) accu0 bf
and  aux accu0 impl b1 bf accu1 = function
  | [] -> accu1 (* auxpasse impl accu1 accu0 bf *)
  | l1::lf ->
      (* was : aux ((b1::l1)::accu1) lf *)
      aux accu0 impl b1 bf (ajout_clause impl (ajout_hyp impl b1 l1) accu1) lf
    

let passe impl accu0 l =
  let n = List.length l
  and n0 = List.length accu0 in
  prerr_endline ("pret a distri " ^ string_of_int n ^ " sur accu " ^ string_of_int n0 ^ " soit " ^ string_of_int (n * n0));
    prerr_endline (String.concat " - " (List.map (fun l -> string_of_int (List.length l)) accu0) );
      auxpasse impl [] accu0 l

let rec distri2 impl accu0 = function
  | [] -> accu0
  | k1::kf -> distri2 impl (passe impl accu0 k1) kf

(* Pardonnez-moi, lavez-moi de tous mes peches, et dites-vous bien que je ne suis pas totalement perdu
En effet je ne suis pas amoureux *)
let distri impl _ disjconj =
  let entree = ref disjconj
  and sortie_avant = ref [[]]
  and sortie_apres = ref []
  and source = ref [[]]
  and conj = ref []
  and formule = ref `True
  and n = ref 0
  and n0 = ref 0
  and nt = ref (List.length disjconj)
  and clause_apres = ref []
  in
  while !entree <> []
  do
    conj := List.hd !entree;
    entree := List.tl !entree;
    n := List.length !conj;
    n0 := List.length !sortie_avant;
    prerr_endline ("reste " ^ string_of_int !nt ^ " pret a distri " ^ string_of_int !n ^ " sur accu " ^ string_of_int !n0 ^ " soit " ^ string_of_int (!n * !n0));
   (*    prerr_endline (String.concat " - " (List.map (fun l -> string_of_int (List.length l)) !sortie_avant)); *)
    decr nt;
    sortie_apres := [];
    while !conj <> []
    do
      formule := List.hd !conj;
      conj := List.tl !conj;
      source := !sortie_avant;
      while !source <> []
      do
      (* if !n = 1
      then clause_apres := !formule::(List.hd !source)
      else *) clause_apres := ajout_hyp impl !formule (List.hd !source) ;
      source := List.tl !source;        
      (* if !n = 1
      then sortie_apres := !clause_apres :: !sortie_apres
      else *) begin
	sortie_apres := ajout_clause impl !clause_apres !sortie_apres;
       end ;
       Gc.major ();
      done;
    done;
    sortie_avant := !sortie_apres;
  done;
  prerr_endline "fin de distri";
  !sortie_avant


let rec partir od frais nonfrais : forme_stricte list -> (forme_stricte list * forme_stricte list) = function
  | [] -> frais, nonfrais
  | a::q when formule_fraiche od (a : forme_stricte :> fol_formula) -> partir od (a::frais) nonfrais q
  | a::q -> partir od frais (a::nonfrais) q



let rec rentrer_forall ((v, _) as k) (`Disjunction m) =
  let aux = function
    | `Forall (l, f) -> `Forall (l, rentrer_forall k f)
    | f -> `Forall ([k], `Disjunction [f])
  in match partir v [] [] m with
    | indep, [] -> `Disjunction indep
    | indep, [f] -> `Disjunction ((aux f)::indep)
    | indep, dep -> `Disjunction ((`Forall ([k], `Disjunction dep))::indep)


let rec rentrer_exists ((v, _) as k) (`Conjunction m) =
  let aux = function
    | `Exists (l, f) -> `Exists (l, rentrer_exists k f)
    | f -> `Exists ([k], `Conjunction [f])
  in match partir v [] [] m with
    | indep, [] -> `Conjunction indep
    | indep, [f] -> `Conjunction ((aux f)::indep)
    | indep, dep -> `Conjunction ((`Exists ([k], `Conjunction dep))::indep)

let k_et = ref 0
let k_ou = ref 0

let rec forme_et (f0: negsimpl_formula) : forme_et =
  incr k_et;
  let i = !k_et in  
  prerr_endline ("forme_et : " ^ string_of_int i);
  match f0 with
  | `Conjunction l ->
      let rec aux accu : forme_et list -> forme_et = function
        | [] -> `Conjunction accu
        | (`Conjunction l3)::q -> aux (l3 @ accu) q
      in aux [] (List.rev_map forme_et l)

  | `Exists ([], f) | `Forall ([], f) -> forme_et f

  | `Forall (((v, _) as k)::q, f) ->
      let (`Conjunction l) = forme_et (`Forall (q, f)) in
      `Conjunction (List.rev_map (rentrer_forall k) l)

  | `Disjunction _ | `Exists _ as f ->
      let (`Disjunction l) = forme_ou f in
      prerr_endline ("retour forme_et : " ^ string_of_int i);
      let l2 = List.rev_map (fun (`Conjunction c) -> c) l in
      let l3 = distri impl_stricte [[]] l2 in
      prerr_endline ("fin de distri, forme_et : " ^ string_of_int i);
      let l4 = List.rev_map (fun c -> ou_contrad (`Disjunction (elim_hyp_str c))) l3
      in
      `Conjunction (elim_concl_ou l4)

  | #forme_atome as f -> `Conjunction [`Disjunction [f]]

and forme_ou (f0: negsimpl_formula) : forme_ou = 
  incr k_ou;
  let i = !k_ou in
  prerr_endline ("forme_ou : " ^ string_of_int i);
  match f0 with
  | `Disjunction l ->
      let rec aux accu = function
        | [] -> `Disjunction accu
        | (`Disjunction l3)::q -> aux (l3 @ accu) q
      in aux [] (List.rev_map forme_ou l)

  | `Exists ([], f) | `Forall ([], f) ->  forme_ou f

  | `Exists (((v, _) as k)::q, f) ->
      let (`Disjunction l) = forme_ou (`Exists (q, f)) in
      `Disjunction (List.rev_map (rentrer_exists k) l)

  | `Conjunction _ | `Forall _ as f ->
      let (`Conjunction l) = forme_et f in
      prerr_endline ("retour forme_ou : " ^ string_of_int i);
      let l2 = List.rev_map (fun (`Disjunction c) -> c) l in
      let l3 = distri (recip impl_stricte) [[]] l2 in
      prerr_endline ("fin de distri, forme_ou : " ^ string_of_int i);
      let l4 = List.rev_map (fun c -> et_contrad (`Conjunction (elim_concl_str c))) l3
      in
      `Disjunction (elim_hyp_et l4)


  | #forme_atome as f -> `Disjunction [`Conjunction [f]]


      

(* Final algorithm *)

let rec terme_ferme scope (_, t) = match t with
  | `Variable v -> let b = List.mem v scope in
    if not b then prerr_endline ("variable libre: " ^ v);
    b
  | `Function (_, l) -> List.for_all (terme_ferme scope) l
  | _ -> true

let rec formule_fermee scope = function
  | `Equality (t1, t2) -> terme_ferme scope t1 && terme_ferme scope t2
  | `Predicate (_, l) -> List.for_all (terme_ferme scope) l
  | `Negation f -> formule_fermee scope f
  | `Conjunction l | `Disjunction l -> List.for_all (formule_fermee scope) l
  | `Exists (l, f) | `Forall (l, f) -> formule_fermee (List.rev_map fst l @ scope) f
  | _ -> true

let simplifier_formule f =
  if not (formule_fermee [] f) then failwith "la formule ORIGINALE n'est pas fermee";
  let f2 = uniformiser (neg_simpl f) in
  if not (formule_fermee [] (f2 : negsimpl_formula :> fol_formula)) then failwith "la formule UNIFORMISEE n'est pas fermee";
  let f3 = quant_simpl f2 in
  if not (formule_fermee [] (f3 : negsimpl_formula :> fol_formula)) then failwith "la formule SIMPLIFIEE n'est pas fermee";
  f3


let simplifier_hyp f =
  let f2 = simplifier_formule f in 
  let f3 = forme_ou f2 in
  if not (formule_fermee [] (f3 : forme_ou :> fol_formula)) then failwith "l'HYPOTHESE SIMPLIFIEE n'est pas fermee";
  f3

let simplifier_concl f =
  let f2 = simplifier_formule f in 
  let f3 = forme_et f2 in
  prerr_endline "fin de forme";
  if not (formule_fermee [] (f3 : forme_et :> fol_formula)) then failwith "la CONCLUSION SIMPLIFIEE n'est pas fermee";
  f3 



let simplifier_resultat res = let res2 = {
(*  res_axiomes = [(forme_ou (`Conjunction (List.map simplifier_formule res.res_axiomes)) : forme_ou :> fol_formula)]; *)
  res_axiomes = (List.rev_map (fun (x, f) -> (x,  (* simplifier_formule *) neg_simpl f)) res.res_axiomes);
  res_theoremes = 
    let r1 = List.rev_map (fun (n, t) -> (n, (simplifier_concl t : forme_et :> negsimpl_formula))) res.res_theoremes in
    (*    let r2 = List.map (fun (n, t) -> (n, separer_et t)) r1 in *)
    (*    let r2 = List.map (fun (n, t) -> (n, un_niveau t)) r1 in *)
    (* let r2 = List.map (fun (n, t) -> (n, un_niveau_rec (n,t))) r1 in
    let r3 = List.fold_left (
      fun accu (n, l) -> List.fold_left (
        fun accu2 t -> (nouveau_symbole n, t)::accu2
      ) accu l
    ) [] r2
    in
    r3 *) r1
    ;
} in
match res2.res_theoremes with
  | [] -> res2
  | (n, _)::_ ->
      let fichier = n ^ ".marshal" in
      let ch = open_out_bin fichier in
      Marshal.to_channel ch res2 [];
      close_out ch;
      res2