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 subst_term od nw = function
  | k, `Variable v when v = od -> nw
  | k, `Function (f, t) -> (k, `Function (f, List.map (subst_term od nw) t))
  | t -> t


let rec termes_egaux (_, t1) (_, t2) = match t1, t2 with
  | `Constant i, `Constant j -> i = j
  | `Variable i, `Variable j -> i = j
  | `Function (f, l), `Function (g, m) -> f = g && let rec aux = function
      | [], [] -> true
      | a::q, b::r -> termes_egaux a b && aux (q, r)
      | _ -> false
    in aux (l, m)
  | _ -> false

let rec terme_frais od (_, t) = match t with
  | `Variable v -> v <> od
  | `Function (_, tl) ->
      let rec aux = function
        | [] -> true
        | a::q -> terme_frais od a && aux q
      in aux 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) -> let rec aux = function
      | [] -> true
      | a::q -> terme_frais od a && aux q
    in aux l
  | `Negation f -> formule_fraiche od f
  | `Conjunction l | `Disjunction l -> let rec aux = function
      | [] -> true
      | a::q -> formule_fraiche od a && aux q
    in aux l
  | `Exists (l, _) when List.mem od (List.map fst l) -> true
  | `Forall (l, _) when List.mem od (List.map fst l) -> true
  | `Exists (_, f) | `Forall (_, f) -> formule_fraiche od f
  | _ -> true

let rec terme_frais_scope t = function
  | [] -> true
  | v::q -> terme_frais v t && terme_frais_scope t q

let subst_naive_atome od nw = function
  | `Predicate (id, t) -> `Predicate (id, List.map (subst_term od nw) t)
  | `Equality (t1, t2) -> begin match (subst_term od nw t1, subst_term od nw t2) with
      | v1, v2 when termes_egaux v1 v2 -> `True
      | eq -> `Equality eq
    end

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

let rec subst_naive od nw : negsimpl_formula -> negsimpl_formula = function
  | `Exists (l, f) -> `Exists (l, subst_naive od nw f)
  | `Forall (l, f) -> `Forall (l, subst_naive od nw f)
  | `Negation f -> subst_naive_negation od nw f
  | `Conjunction l -> `Conjunction (List.map (subst_naive od nw) l)
  | `Disjunction l -> `Disjunction (List.map (subst_naive od nw) l)
  | #boool as f -> f
  | #fol_atom as f -> subst_naive_atome od nw f

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.map uniformiser l)
  | `Disjunction l -> `Disjunction (List.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.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.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')] ->
            let sc2 = List.map fst l' in
            if List.mem v sc2
            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')] ->
            let sc2 = List.map fst l' in
            if List.mem v sc2
            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.map quant_simpl l))
  | `Disjunction l -> bool_simpl (`Disjunction (List.map quant_simpl l))
  | f -> bool_simpl f

let rec implique_atom = function
  | `Predicate (f, []), `Predicate (g, []) -> f = g
  | `Predicate (f, t::l), `Predicate (g, u::m) -> termes_egaux t u && implique_atom (`Predicate (f, l), `Predicate (g, m))
  | `Equality (u, v), `Equality (s, t) -> (termes_egaux u s && termes_egaux v t) || (termes_egaux u t && termes_egaux v s)
  | _ -> false


let rec implique a b (*a : negsimpl_formula) (b : negsimpl_formula*) = match (a, b) with
  | _, `Conjunction [] | `Disjunction [], _ | _, `True | `False, _ -> true
  | _, `Conjunction l -> List.for_all (implique a) l
  | `Disjunction l, _ -> List.for_all (fun h -> implique h b) l
  | `Conjunction l, _ -> List.exists (fun h -> implique h b) l
  | _, `Disjunction l -> List.exists (implique a) l
  | `Negation c, `Negation d -> implique_atom (d, c) (* (d :> negsimpl_formula) (c :> negsimpl_formula) *)
  | `Forall ([], c), `Forall ([], d) | `Exists ([], c), `Exists ([], d) -> implique c d
  | `Forall ((x, _)::l, c), `Forall ((y, _)::m, d) | `Exists ((x, _)::l, c), `Exists ((y, _)::m, d) ->
      let z = nouveau_symbole "implique" in
      implique (`Forall (l, subst_naive x (`Unknown, `Variable z) c)) (`Forall (l, subst_naive y (`Unknown, `Variable z) d))
  | (#fol_atom as c), (#fol_atom as d) -> implique_atom (c, d)
  | _ -> false


let recip impl a b = impl b a

let ajout_hyp impl =
  let rec aux accu f = function
    | [] -> f::accu
    | c::s when impl f c ->
        prerr_endline "un drop";
        aux accu c s
    | c::s when impl c f ->
        prerr_endline "un drop";
        aux accu f s
    | c::s -> aux (c::accu) f s
  in aux []

let ajout_concl impl = ajout_hyp (recip impl)

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

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.map elaguer l)))
  | `Disjunction l -> bool_simpl (`Disjunction (eliminer_hypotheses (List.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 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.map nier_stricte l)

and nier_ou_stricte (`Disjunction l) = `Conjunction (List.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 e = match e with 
    (`Disjunction l) ->
      if contrad_stricte_ou l then (
        prerr_endline "contradiction disjointe !";
        `Disjunction [`True]
      ) else e

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


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.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.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 rec distribuer accu = function
        | [] ->
            prerr_endline "fin de distri";
            `Conjunction (elim_concl_ou (List.map (fun h -> ou_contrad (`Disjunction h)) accu))
        | (`Conjunction m)::q ->
            prerr_endline "une distri";
            distribuer (
            List.concat (
              List.map (fun c ->
                List.map (fun l ->
                  ajout_hyp_stricte c l
                ) accu
              ) m
            )
          ) q              
      in 
      distribuer [[]] l

  | #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.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.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 rec distribuer accu = function
        | [] ->
            prerr_endline "fin de distri";
            `Disjunction (elim_hyp_et (List.map (fun h -> et_contrad (`Conjunction h)) accu))
        | (`Disjunction m)::q ->
            prerr_endline "une distri";
            distribuer (
            List.concat (
              List.map (fun c ->
                List.map (fun l ->
                  ajout_concl_stricte c l
                ) accu
              ) m
            )
          ) q              
      in 
      distribuer [[]] l

  | #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.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.map simplifier_formule res.res_axiomes : negsimpl_formula list :> fol_formula list);
  res_theoremes = 
    let r1 = List.map (fun (n, t) -> (n, (simplifier_concl t : forme_et :> fol_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