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 (a : negsimpl_formula) (b : negsimpl_formula) = match (a, b) with
  | _, `Conjunction [] | `Disjunction [], _ | _, `True | `False, _ -> true
  | `Predicate (f, []), `Predicate (g, []) -> f = g
  | `Predicate (f, t::l), `Predicate (g, u::m) -> termes_egaux t u && implique (`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)
  | _, `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 (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))
  | _ -> false


let rec eliminer_hypotheses = function
  | [] -> []
  | a::q -> let r = eliminer_hypotheses q in
    let rec aux f accu = function
      | [] -> f::accu
      | c::s when implique f c -> aux c accu s
      | c::s when implique c f -> aux f accu s
      | c::s -> aux f (c::accu) s
    in aux a [] r

let rec eliminer_conclusions = function
  | [] -> []
  | a::q -> let r = eliminer_conclusions q in
    let rec aux f accu = function
      | [] -> f::accu
      | c::s when implique c f -> aux c accu s
      | c::s when implique f c -> aux f accu s
      | c::s -> aux f (c::accu) s
    in aux a [] r


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 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 rentrer_forall ((v, _) as k) (accu : forme_stricte list) : forme_stricte -> forme_stricte list = function
  | `Forall (l, _) as f when List.mem v (List.map fst l) -> f::accu
  | `Forall (l, `Disjunction m) -> begin match partir v [] [] m with
      | [], [] -> accu
      | indep, [] -> (`Forall (l, `Disjunction indep))::accu
      | [], dep -> (`Forall (k::l, `Disjunction dep))::accu
      | indep, dep ->
          (`Forall (l, `Disjunction indep))::(`Forall (k::l, `Disjunction dep))::accu
    end
  | `Exists _ as f when formule_fraiche v (f : forme_stricte :> fol_formula) -> f::accu
  | `Exists _ as f -> (`Forall ([k], `Disjunction [f]))::accu
  | #forme_atome as f when formule_fraiche v (f : forme_stricte :> fol_formula) -> f::accu
  | #forme_atome as f -> (`Forall ([k], `Disjunction [f]))::accu

let rentrer_exists ((v, _) as k) (accu : forme_stricte list) : forme_stricte -> forme_stricte list = function
  | `Exists (l, _) as f when List.mem v (List.map fst l) -> f::accu
  | `Exists (l, `Conjunction m) -> begin match partir v [] [] m  with
      | [], [] -> accu
      | indep, [] ->  (`Exists (l, `Conjunction indep))::accu
      | [], dep -> (`Exists (k::l, `Conjunction dep))::accu
      | indep, dep ->
          (`Exists (l, `Conjunction indep))::(`Exists (k::l, `Conjunction dep))::accu
    end
  | `Forall _ as f when formule_fraiche v (f : forme_stricte :> fol_formula) -> f::accu
  | `Forall _ as f -> (`Exists ([k], `Conjunction [f]))::accu
  | #forme_atome as f when formule_fraiche v (f : forme_stricte :> fol_formula) -> f::accu
  | #forme_atome as f -> (`Exists ([k], `Conjunction [f]))::accu

let rec forme_et : negsimpl_formula -> forme_et = function
  | `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 (fun (`Disjunction m) -> `Disjunction (List.fold_left (rentrer_forall k) [] m)) l
      )

  | `Disjunction _ | `Exists _ as f ->
      let (`Disjunction l) = forme_ou f in
      let rec distribuer accu = function
        | [] -> `Conjunction (List.map (fun h -> `Disjunction h) accu)
        | (`Conjunction m)::q -> distribuer (
            List.concat (
              List.map (fun c ->
                List.map (fun l ->
                  c::l
                ) accu
              ) m
            )
          ) q              
      in 
      distribuer [[]] l

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

and forme_ou : negsimpl_formula -> forme_ou = function
  | `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 (fun (`Conjunction m) -> `Conjunction (List.fold_left (rentrer_exists k) [] m)) l
      )

  | `Conjunction _ | `Forall _ as f ->
      let (`Conjunction l) = forme_et f in
      let rec distribuer accu = function
        | [] -> `Disjunction (List.map (fun h -> `Conjunction h) accu)
        | (`Disjunction m)::q -> distribuer (
            List.concat (
              List.map (fun c ->
                List.map (fun l ->
                  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_resultat res = let res2 = {
  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_formule t : negsimpl_formula :> 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