open Fol


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

let rec neg_simpl = function

      | `Negation f -> begin match f with
          | `Negation g -> 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))
          | f0 -> `Negation f0
        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)
      | f -> f

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
  | `Int i, `Int j -> i = j
  | `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 = 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 rec subst_naive 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
  | `Exists (l, f) -> `Exists (l, subst_naive od nw f)
  | `Forall (l, f) -> `Forall (l, subst_naive od nw f)
  | `Negation f -> `Negation (subst_naive od nw f)
  | `Conjunction l -> `Conjunction (List.map (subst_naive od nw) l)
  | `Disjunction l -> `Disjunction (List.map (subst_naive od nw) l)
  | f -> 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)
  | `Negation f -> `Negation (uniformiser f)
  | 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 = 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
  | `Negation f -> begin match bool_simpl f with
      | `Negation g -> g
      | `True -> `False
      | `False -> `True
      | g -> `Negation g
    end
  | `Exists (l, f) -> let f2 = bool_simpl f in begin match alleger [] f2 l with
      | [] -> f2
      | l2 -> `Exists (l2, f2)
    end
  | `Forall (l, f) -> let f2 = bool_simpl f in begin match alleger [] f2 l with
      | [] -> f2
      | l2 -> `Forall (l2, f2)
    end
  | `Equality (t1, t2) when termes_egaux t1 t2 -> `True
  | f -> f


let rec quant_simpl = function
  | `Exists ([], f0) -> quant_simpl f0
  | `Exists (((v, _) as k)::q, f0) ->
      let f = quant_simpl (`Exists (q, f0)) in
      let rec aux_v nonscope bloque = function
        | [] -> None
        | [`Equality ((_, `Variable v1), v2)]
            when (v1 = v && terme_frais_scope v2 nonscope) ->
            Some v2
        | [`Equality (v2, (_, `Variable v1))]
            when (v1 = v && terme_frais_scope v2 nonscope) ->
            Some v2
        | [`Conjunction l] -> aux_v nonscope bloque l
        | [`Disjunction [f']] -> aux_v nonscope bloque [f']
        | [`Exists (l', _)] when List.mem v (List.map fst l') -> None
        | [`Exists (l', f')] when bloque -> aux_v (List.map fst l' @ nonscope) true [f']
        | [`Exists (_, f')] -> aux_v nonscope false [f']
        | [`Forall (l', _)] when List.mem v (List.map fst l') -> None
        | [`Forall (l', f')] -> aux_v (List.map fst l' @ nonscope) true [f']
        | [_] -> None
        | a::r -> begin match aux_v nonscope bloque [a] with
            | None -> aux_v nonscope bloque r
            | Some _ as res -> res
          end
      in begin match aux_v [] false [f] with
        | None -> `Exists ([k], f)
        | Some v2 -> begin
            prerr_endline ("Dropped : " ^ v ^ " := " ^ string_of_terme v2) ;
            bool_simpl (subst_naive v v2 f)
          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 nonscope bloque = function
        | [] -> None
        | [`Negation (`Equality ((_, `Variable v1), v2))]
            when (v1 = v && terme_frais_scope v2 nonscope) ->
            Some v2
        | [`Negation (`Equality (v2, (_, `Variable v1)))]
            when (v1 = v && terme_frais_scope v2 nonscope) ->
            Some v2
        | [`Disjunction l] -> aux_v nonscope bloque l
        | [`Conjunction [f']] -> aux_v nonscope bloque [f']
        | [`Exists (l', _)] when List.mem v (List.map fst l') -> None
        | [`Exists (l', f')] -> aux_v (List.map fst l' @ nonscope) true [f']
        | [`Forall (l', _)] when List.mem v (List.map fst l') -> None
        | [`Forall (l', f')] when bloque -> aux_v (List.map fst l' @ nonscope) true [f']
        | [`Forall (_, f')] -> aux_v nonscope false [f']
        | [_] -> None
        | a::r -> begin match aux_v nonscope bloque [a] with
            | None -> aux_v nonscope bloque r
            | Some _ as res -> res
          end
      in begin match aux_v [] false [f] with
        | None -> `Forall ([k], f)
        | Some v2 -> begin
            prerr_endline ("Dropped : " ^ v ^ " := " ^ string_of_terme v2) ;
            bool_simpl (subst_naive v v2 f)
          end
      end
  | `Negation f -> bool_simpl (`Negation (quant_simpl f))
  | `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 similaires a b = match (a, b) with
  | `Conjunction [], `Conjunction [] | `Disjunction [], `Disjunction [] | `True, `True | `False, `False -> true
  | `Predicate (f, []), `Predicate (g, []) -> f = g
  | `Predicate (f, t::l), `Predicate (g, u::m) -> termes_egaux t u && similaires (`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 (c::q), `Conjunction (d::r) | `Disjunction (c::q), `Disjunction (d::r) ->
      similaires c d && similaires (`Conjunction q) (`Conjunction r)
  | `Negation c, `Negation d -> similaires c d
  | `Forall ([], c), `Forall ([], d) | `Exists ([], c), `Exists ([], d) -> similaires c d
  | `Forall ((x, _)::l, c), `Forall ((y, _)::m, d) | `Exists ((x, _)::l, c), `Exists ((y, _)::m, d) ->
      let z = nouveau_symbole "similitude" in
      similaires (`Forall (l, subst_naive x (`Unknown, `Variable z) c)) (`Forall (l, subst_naive y (`Unknown, `Variable z) d))
  | _ -> false

let rec implique a b = 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)
  | f, `Conjunction l -> List.for_all (implique f) l
  | `Disjunction l, f -> List.for_all (fun h -> implique h f) l
  | `Conjunction l, f -> List.exists (fun h -> implique h f) l
  | f, `Disjunction l -> List.exists (implique f) l
  | `Negation c, `Negation d -> implique d c
  | `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 (m, subst_naive y (`Unknown, `Variable z) d))
  | _ -> false

let rec eliminer_doublons = function
  | [] -> []
  | a::q ->
      let rec aux accu = function
        | [] -> accu
        | b::m when similaires a b -> aux accu m
        | b::m -> aux (b::accu) m
      in aux [a] (eliminer_doublons q)

let rec eliminer_conclusions = function
  | [] -> []
  | a::q ->
      let rec aux f accu = function
        | [] -> (f::accu)
        | b::r when implique f b ->
            prerr_endline "1 concl elim";
            aux f accu r
        | b::r when implique b f ->
            prerr_endline "1 concl elim";
            aux b accu r
        | b::r -> aux f (b::accu) r
      in aux a [] (eliminer_conclusions q)

let rec eliminer_hypotheses = function
  | [] -> []
  | a::q ->
      let rec aux f accu = function
        | [] -> (f::accu)
        | b::r when implique b f ->
            prerr_endline "1 hyp elim";            
            aux f accu r
        | b::r when implique f b ->
            prerr_endline "1 hyp elim";
            aux b accu r
        | b::r -> aux f (b::accu) r
      in aux a [] (eliminer_hypotheses q)


let rec elaguer = function
  | `Conjunction l -> (`Conjunction (eliminer_doublons (List.map elaguer l)))
  | `Disjunction l -> (`Disjunction (eliminer_doublons (List.map elaguer l)))
  | `Negation f -> (`Negation (elaguer f))
  | `Forall (l, f) -> (`Forall (l, elaguer f))
  | `Exists (l, f) -> (`Exists (l, elaguer f))
  | f -> f

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


let simplifier_formule f =
   (quant_simpl (elaguer_impl (uniformiser (neg_simpl f))))


let rec separer_et = function
  | `Conjunction l -> List.concat (List.map separer_et l)
  | `Forall (v, f) -> List.map (fun g -> `Forall (v, g)) (separer_et f)
  | f -> [f]

let rec separer_ou = function
  | `Disjunction l -> List.concat (List.map separer_ou l)
  | `Exists (v, f) -> List.map (fun g -> `Exists (v, g)) (separer_ou f)
  | f -> [f]

let rec distribuer accu = function
  | [] -> [`Disjunction accu]
  | a::q -> begin match eliminer_hypotheses (separer_ou a) with
      | [] -> distribuer accu q
      | [b] -> begin match eliminer_conclusions (separer_et b) with
          | [] -> [`True] (* empty conjunction *)
          | [c] -> distribuer (c::accu) q
          | l ->
              let m = accu @ q in
              List.map (fun f -> `Disjunction (f::m)) l
        end
      | l -> distribuer accu (l @ q)
    end

let rec un_niveau_f = function
  | `Forall (v, f) -> List.map (fun g -> `Forall (v, g)) (un_niveau_f f)
  | f ->  distribuer [] [f]

let un_niveau f =
  let l1 = List.concat (List.map un_niveau_f (eliminer_conclusions (separer_et f))) in
  let l2 = eliminer_conclusions l1 in
  let n = (List.length l1 - List.length l2) in
  (if n > 0 then prerr_endline (string_of_int n  ^ " conclusions rejetees") else ());
  l2

let un_niveau_rec (n, f) =
  prerr_endline ("Conjecture: " ^ n);
  Sys.catch_break true;
  let l = ref [f] in
  let n = ref 1 and n2 = ref 0 in
  try
    while !n = !n2
    do
      n := !n2;
      l := List.concat (List.map un_niveau !l);
      n2 := List.length !l;
      prerr_endline (string_of_int !n2 ^ " formulae so far");
    done;
    !l
  with Sys.Break -> !l


let simplifier_resultat res = let res2 = {
  res_axiomes = List.map simplifier_formule res.res_axiomes;
  res_theoremes = 
    let r1 = List.map (fun (n, t) -> (n, simplifier_formule t)) 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
    ;
} 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