open Symb
open Alloyast
open Fol

let rec subst_naive od nw (t : fol_formula) : fol_formula =
  subst_naive_aux subst_naive od nw t

let rec term_of_relation = function
  | `Plus (Some n, (a, b)) -> `Unknown, `Function ("alloyop__plus_" ^ string_of_int n, [term_of_relation a; term_of_relation b])
  | `Moins (Some n, (a, b)) -> `Unknown, `Function ("alloyop__moins_" ^ string_of_int n, [term_of_relation a; term_of_relation b])
  | `Inter (Some n, (a, b)) -> `Unknown, `Function ("alloyop__inter_" ^ string_of_int n, [term_of_relation a; term_of_relation b])
  | `Fleche (Some (p,q), (a, b)) -> `Unknown, `Function ("alloyop__fleche_" ^ string_of_int p ^ "_" ^ string_of_int q, [term_of_relation a; term_of_relation b])
  | `Jointure (Some (p, q), (a, b)) -> `Unknown, `Function ("alloyop__jointure_" ^ string_of_int p ^ "_" ^ string_of_int q, [term_of_relation a; term_of_relation b])
  | `Restriction_droite (Some n, (a, b)) -> `Unknown, `Function ("alloyop__restd_" ^ string_of_int n, [term_of_relation a; term_of_relation b])
  | `Restriction_gauche (Some n, (a, b)) -> `Unknown, `Function ("alloyop__restg_" ^ string_of_int n, [term_of_relation a; term_of_relation b])
  | `Tilde a -> `Unknown, `Function ("alloyop__tilde", [term_of_relation a])
  | `Fonction (a, l) -> `Unknown, `Function (a, List.map term_of_relation l)
  | `Variable i -> `Unknown, `Variable i
  | `Univ -> `Unknown, `Constant "univ"
  | `Iden -> `Unknown, `Constant "iden"
  | `None -> `Unknown, `Constant "none"
  | _ -> failwith "arites non toutes renseignees"

let fol_of_none t =
  `Equality (t, (`Unknown, `Constant "none"))

let fol_of_one t =
  `Predicate ("alloyth__singl", [t;])

let fol_of_quant l f =
  let l2 = List.rev_map (fun (x, r) -> ((x, nouveau_symbole ("quant_" ^ x)), r)) l in
  let f2 = List.fold_left (fun accu ((x, w), _) -> subst_naive x (`Unknown, `Variable w) accu) f l2 in
  (List.rev_map (fun ((x, w), r) -> (w, r)) l2, f2)
 

let rec fol_of_alloy : alloy_formule -> fol_formula = function
  | `Predicate (f, l) ->
      `Predicate (f, List.map term_of_relation l)
  | `Some r -> `Negation (fol_of_none (term_of_relation r))
  | `No r -> fol_of_none (term_of_relation r)
  | `Lone r ->
      let t = term_of_relation r in
      `Disjunction [fol_of_none t; fol_of_one t]
  | `One r -> fol_of_one (term_of_relation r)
  | `In (a, b) -> `Predicate ("in", [term_of_relation a; term_of_relation b])
  | `Equality (a, b) -> `Equality (term_of_relation a, term_of_relation b)
  | `Negation f -> `Negation (fol_of_alloy f)
  | `Conjunction l -> `Conjunction (List.map fol_of_alloy l)
  | `Disjunction l -> `Disjunction (List.map fol_of_alloy l)
  | `Exists (l, f) -> let (l2, f2) = fol_of_quant l (fol_of_alloy f) in
    `Exists
      (List.rev_map (fun (x, _) -> (x, `Unknown)) l2,
      `Conjunction (f2::(
        List.rev_map (fun (x, r) -> `Predicate ("alloyth__elem", [
          `Unknown, `Variable x;
          term_of_relation r;
        ])) l2
      )))
  | `Forall (l, f) -> let (l2, f2) = fol_of_quant l (fol_of_alloy f) in
    `Forall
      (List.rev_map (fun (x, _) -> (x, `Unknown)) l2,
      implication (`Conjunction (
        List.rev_map (fun (x, r) -> `Predicate ("alloyth__elem", [
          `Unknown, `Variable x;
          term_of_relation r;
        ])) l2)) f2)


let close_fol_of_alloy f = clore_formule [] (fol_of_alloy f)


(* Theorie des relations. A partir de l'arite *)

let singl : ident * fol_formula =
  "def_singl", `Forall (
    ["x", `Unknown],
    equivalence 
      (fol_of_one (`Unknown, `Variable "x"))
      (`Forall
        (["y", `Unknown],
        implication
          (`Predicate ("alloyth__elem",
          [`Unknown, `Variable "y"; `Unknown, `Variable "x";]))
          (`Equality ((`Unknown, `Variable "y"), (`Unknown, `Variable "x")))
        )))

let elem_singl : ident * fol_formula =
  "ax_elem_singl", `Forall (
    ["x", `Unknown; "a", `Unknown],
    implication
      (`Predicate ("alloyth__elem",
      [`Unknown, `Variable "x"; `Unknown, `Variable "a";]))
      (fol_of_one (`Unknown, `Variable "x"))
  )

let none : ident * fol_formula =
  "def_none", `Forall (
    ["x", `Unknown],
    `Negation
      (`Predicate ("alloyth__elem", [`Unknown, `Variable "x"; `Unknown, `Constant "none"])))

let incl : ident * fol_formula =
  "def_in", `Forall (
    ["a", `Unknown; "b", `Unknown],
    equivalence
      (`Predicate ("in",
      [`Unknown, `Variable "a"; `Unknown, `Variable "b";]))
      (`Forall
        (["x", `Unknown],
        implication
          (`Predicate ("alloyth__elem",
          [`Unknown, `Variable "x"; `Unknown, `Variable "a";]))
          (`Predicate ("alloyth__elem",
          [`Unknown, `Variable "x"; `Unknown, `Variable "b";]))
        )
      )
  )

let in_antisym : ident * fol_formula =
  "ax_in_antisym", `Forall (
    ["a", `Unknown; "b", `Unknown],
    equivalence
      (`Conjunction [
        `Predicate ("in", [`Unknown, `Variable "a"; `Unknown, `Variable "b"]);
        `Predicate ("in", [`Unknown, `Variable "b"; `Unknown, `Variable "a"]);
      ])
      (`Equality ((`Unknown, `Variable "a"), (`Unknown, `Variable "b")))
  )


(* Arite *)


let ar i x = `Predicate ("alloyth__arite" ^ string_of_int i, [`Unknown, `Variable x])


let arite accu n =
  let l : fol_formula list = iterer (fun i -> ar i "x") n in
  let accu2 =
    ("ax_arite", `Forall (["x", `Unknown], `Disjunction l))
    ::("ax_vide_arite", `Forall (["x", `Unknown], implication
      (fol_of_none (`Unknown, `Variable "x"))
      (`Conjunction l)))
    ::accu
  in
  let (_, accu3) = List.fold_left 
    (fun ((anc : fol_formula list), (ak : (ident * fol_formula) list)) (nouv : fol_formula) ->
      (nouv::anc, (nouveau_symbole "ax_arite_vide", `Forall (["x", `Unknown], implication
        (`Conjunction [`Disjunction anc; nouv])
        (fol_of_none (`Unknown, `Variable "x"))
      ))::ak))
    ([List.hd l], accu2)
    (List.tl l)
  in
  let accu4 = plier_gauche
    (fun ak i ->
      ("ax_arite_in_" ^ string_of_int i,
      `Forall (["a", `Unknown], equivalence
        (ar i "a")
        (`Forall (["y", `Unknown], implication
          (`Predicate ("alloyth__elem", [`Unknown, `Variable "y"; `Unknown, `Variable "a"]))
          (ar i "y")
        ))
      ))::ak
    )
    accu3
    n
  in
  accu4

(* Tuple *)

let tuple accu n =
  let p = n - 1 in
  plier_gauche
    (fun ak j ->
      let i = j + 1 in
      let l = iterer (fun q -> "x" ^ string_of_int q) i and l' = iterer (fun q -> "y" ^ string_of_int q) i in
      let lq = List.rev_map (fun v -> (v, `Unknown)) l and lq' = List.rev_map (fun v -> (v, `Unknown)) l'
      and lt = List.map (fun v -> (`Unknown, `Variable v)) l and lt' = List.map (fun v -> (`Unknown, `Variable v)) l' in
      
      ("ax_tuple_decomp_" ^ string_of_int i,
      `Forall (["a", `Unknown], implication (
        `Conjunction [
          fol_of_one (`Unknown, `Variable "a");
          ar i "a";
        ]
      ) (
        `Exists (lq, `Predicate ("alloyth__tuple" ^ string_of_int i, (`Unknown, `Variable "a")::lt))
      )))
      ::("ax_tuple_valide_" ^ string_of_int i,
      `Forall (("a", `Unknown)::lq, implication
        (`Predicate ("alloyth__tuple" ^  string_of_int i, (`Unknown, `Variable "a")::lt))
        (`Conjunction
          (
            List.fold_left
              (fun ak x ->
                (ar 1 x)::(fol_of_one (`Unknown, `Variable x))::ak
              ) [
                ar i "a";
                fol_of_one (`Unknown, `Variable "a");
              ]
              l
          )
        )
      ))
      ::("ax_tuple_ex_" ^ string_of_int i,
      `Forall (lq, implication
        (`Conjunction 
          (
            List.fold_left
              (fun ak x ->
                (ar 1 x)::(fol_of_one (`Unknown, `Variable x))::ak
              ) [] l
          )
        ) (
          `Exists (["a", `Unknown],
          `Predicate ("alloyth__tuple" ^ string_of_int i, (`Unknown, `Variable "a")::lt))
        )
      ))
      ::("ax_tuple_eq_compo_" ^ string_of_int i,
      `Forall (("a", `Unknown)::(List.rev_append lq lq'), implication
        (`Conjunction [
          `Predicate ("alloyth__tuple" ^ string_of_int i, (`Unknown, `Variable "a")::lt);
          `Predicate ("alloyth__tuple" ^ string_of_int i, (`Unknown, `Variable "a")::lt');
        ]) (
          `Conjunction (iterer (fun q -> `Equality ((`Unknown, `Variable ("x" ^ string_of_int q)), (`Unknown, `Variable ("y" ^ string_of_int q)))) i)
        )
      ))
      ::("ax_tuple_eq_" ^ string_of_int i,
      `Forall (("a", `Unknown)::("b",`Unknown)::lq, implication
        (`Conjunction [
          `Predicate ("alloyth__tuple" ^ string_of_int i, (`Unknown, `Variable "a")::lt);
          `Predicate ("alloyth__tuple" ^ string_of_int i, (`Unknown, `Variable "b")::lt);
        ])
        (`Equality ((`Unknown, `Variable "a"), (`Unknown, `Variable "b")))
      ))
      ::ak
    )
    accu
    p


(* Artefact pour les singletons unaires *)

let tuple1 : ident * fol_formula =
  "ax_tuple1", let x = `Unknown, `Variable "x"
  and y = `Unknown, `Variable "y"
  in
  `Forall (["x", `Unknown; "y", `Unknown], equivalence
    (`Predicate ("alloyth__tuple1", [x; y]))
    (`Conjunction [`Equality (x, y); ar 1 "x"; ar 1 "y"; fol_of_one x; fol_of_one y])
  )


(* Plus *)

let plus accu i =
  let a = `Unknown, `Variable "a"
  and b = `Unknown, `Variable "b"
  and x = `Unknown, `Variable "x" in
  ("def_plus_" ^ string_of_int i,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Conjunction [ar i "a"; ar i "b"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__plus_" ^ string_of_int i, [a; b])]))
      (`Disjunction [
        `Predicate ("alloyth__elem", [x; a]);
        `Predicate ("alloyth__elem", [x; b]);
      ])
    ))
  ))
  ::("ax_plus_exces_" ^ string_of_int i,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar i "b"]))
    (fol_of_none (`Unknown, `Function ("alloyop__plus_" ^ string_of_int i, [a; b])))
  ))
  ::accu


let moins accu i =
  let a = `Unknown, `Variable "a"
  and b = `Unknown, `Variable "b"
  and x = `Unknown, `Variable "x" in
  ("def_moins_" ^ string_of_int i,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Conjunction [ar i "a"; ar i "b"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__moins_" ^ string_of_int i, [a; b])]))
      (`Conjunction [
        `Predicate ("alloyth__elem", [x; a]);
        `Negation (`Predicate ("alloyth__elem", [x; b]));
      ])
    ))
  ))
  ::("ax_moins_exces_" ^ string_of_int i,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar i "b"]))
    (fol_of_none (`Unknown, `Function ("alloyop__moins_" ^ string_of_int i, [a; b])))
  ))
  ::accu


let inter accu i =
  let a = `Unknown, `Variable "a"
  and b = `Unknown, `Variable "b"
  and x = `Unknown, `Variable "x" in
  ("def_inter_" ^ string_of_int i,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Conjunction [ar i "a"; ar i "b"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__inter_" ^ string_of_int i, [a; b])]))
      (`Conjunction [
        `Predicate ("alloyth__elem", [x; a]);
        `Predicate ("alloyth__elem", [x; b]);
      ])
    ))
  ))
  ::("ax_inter_exces_" ^ string_of_int i,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar i "b"]))
    (fol_of_none (`Unknown, `Function ("alloyop__inter_" ^ string_of_int i, [a; b])))
  ))
  ::accu

let tilde accu =
  let a = `Unknown, `Variable "a"
  and x = `Unknown, `Variable "x"
  and y = `Unknown, `Variable "y"
  and z = `Unknown, `Variable "z"
  and t = `Unknown, `Variable "t" in
  ("def_tilde",
  `Forall (["a", `Unknown; "x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__tilde", [a])]))
      (`Exists (["y", `Unknown; "z", `Unknown; "t", `Unknown], 
      `Conjunction [
        `Predicate ("alloyth__tuple2", [x; y; z]);
        `Predicate ("alloyth__tuple2", [t; z; y]);
        `Predicate ("alloyth__elem", [t; a]);
      ]
      ))
  ))
  ::accu

let jointure accu i j =
  let a = `Unknown, `Variable "a"
  and b = `Unknown, `Variable "b"
  and x = `Unknown, `Variable "x"
  and ly = iterer (fun q -> "y" ^ string_of_int q) (i - 1)
  and lz = iterer (fun q -> "z" ^ string_of_int q) (j - 1)
  and t = `Unknown, `Variable "t"
  and u = `Unknown, `Variable "u"
  and v = `Unknown, `Variable "v"
  in
  ("def_jointure_" ^ string_of_int i ^ "_" ^ string_of_int j,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Conjunction [ar i "a"; ar j "b"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__jointure_" ^ string_of_int i ^ "_" ^ string_of_int j, [a; b])]))
      (`Exists (("v", `Unknown)::("u", `Unknown)::("t", `Unknown)::(List.rev_map (fun v -> (v, `Unknown)) (List.rev_append ly lz)) , `Conjunction [
        `Predicate ("alloyth__tuple" ^ string_of_int (i + j - 2), x::(List.map (fun v -> (`Unknown, `Variable v)) (ly @ lz)));
        `Predicate ("alloyth__tuple" ^ string_of_int i, u::((List.map (fun v -> (`Unknown, `Variable v)) ly) @ [t]));
        `Predicate ("alloyth__tuple" ^ string_of_int j, v::t::(List.map (fun v -> (`Unknown, `Variable v)) lz));
        `Predicate ("alloyth__elem", [u; a]);
        `Predicate ("alloyth__elem", [v; b]);
      ]))
    ))
  ))
  ::("ax_jointure_exces_" ^ string_of_int i ^ "_" ^ string_of_int j,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar j "b"]))
    (fol_of_none (`Unknown, `Function ("alloyop__jointure_" ^ string_of_int i ^ "_" ^ string_of_int j, [a; b])))
  ))
  ::accu

let fleche accu i j =
  let a = `Unknown, `Variable "a"
  and b = `Unknown, `Variable "b"
  and x = `Unknown, `Variable "x"
  and ly = iterer (fun q -> "y" ^ string_of_int q) i
  and lz = iterer (fun q -> "z" ^ string_of_int q) j
  and u = `Unknown, `Variable "u"
  and v = `Unknown, `Variable "v"
  in
  ("def_fleche_" ^ string_of_int i ^ "_" ^ string_of_int j,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Conjunction [ar i "a"; ar j "b"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__fleche_" ^ string_of_int i ^ "_" ^ string_of_int j, [a; b])]))
      (`Exists (("v", `Unknown)::("u", `Unknown)::(List.rev_map (fun v -> (v, `Unknown)) (List.rev_append ly lz)) , `Conjunction [
        `Predicate ("alloyth__tuple" ^ string_of_int (i + j), x::(List.map (fun v -> (`Unknown, `Variable v)) (ly @ lz)));
        `Predicate ("alloyth__tuple" ^ string_of_int i, u::(List.map (fun v -> (`Unknown, `Variable v)) ly));
        `Predicate ("alloyth__tuple" ^ string_of_int j, v::(List.map (fun v -> (`Unknown, `Variable v)) lz));
        `Predicate ("alloyth__elem", [u; a]);
        `Predicate ("alloyth__elem", [v; b]);
      ]))
    ))
  ))
  ::("ax_fleche_exces_" ^ string_of_int i ^ "_" ^ string_of_int j,
  `Forall (["a", `Unknown; "b", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar j "b"]))
    (fol_of_none (`Unknown, `Function ("alloyop__fleche_" ^ string_of_int i ^ "_" ^ string_of_int j, [a; b])))
  ))
  ::accu


let restriction_gauche accu i =
  let a = `Unknown, `Variable "a"
  and k = `Unknown, `Variable "k"
  and x = `Unknown, `Variable "x"
  and ly = iterer (fun q -> "y" ^ string_of_int q) i
  in
  ("def_restg_" ^ string_of_int i,
  `Forall (["a", `Unknown; "k", `Unknown], implication
    (`Conjunction [ar i "a"; ar 1 "k"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__restg_" ^ string_of_int i, [k; a])]))
      (`Exists (List.rev_map (fun v -> (v, `Unknown)) ly, `Conjunction [
        `Predicate ("alloyth__tuple" ^ string_of_int i, x::(List.map (fun v -> (`Unknown, `Variable v)) ly));
        `Predicate ("alloyth__elem", [x; a]);
        `Predicate ("alloyth__elem", [`Unknown, `Variable "y1"; k]);
      ]))
    ))
  ))
  ::("ax_restg_exces_" ^ string_of_int i,
  `Forall (["a", `Unknown; "k", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar 1 "k"]))
    (fol_of_none (`Unknown, `Function ("alloyop__fleche_" ^ string_of_int i, [k; a])))
  ))
  ::accu

let restriction_droite accu i =
  let a = `Unknown, `Variable "a"
  and k = `Unknown, `Variable "k"
  and x = `Unknown, `Variable "x"
  and ly = iterer (fun q -> "y" ^ string_of_int q) i
  in
  ("def_restd_" ^ string_of_int i,
  `Forall (["a", `Unknown; "k", `Unknown], implication
    (`Conjunction [ar i "a"; ar 1 "k"])
    (`Forall (["x", `Unknown], equivalence
      (`Predicate ("alloyth__elem", [x; `Unknown, `Function ("alloyop__restd_" ^ string_of_int i, [a; k])]))
      (`Exists (List.rev_map (fun v -> (v, `Unknown)) ly, `Conjunction [
        `Predicate ("alloyth__tuple" ^ string_of_int i, x::(List.map (fun v -> (`Unknown, `Variable v)) ly));
        `Predicate ("alloyth__elem", [x; a]);
        `Predicate ("alloyth__elem", [`Unknown, `Variable ("y" ^ string_of_int i); k]);
      ]))
    ))
  ))
  ::("ax_restd_exces_" ^ string_of_int i,
  `Forall (["a", `Unknown; "k", `Unknown], implication
    (`Negation (`Conjunction [ar i "a"; ar 1 "k"]))
    (fol_of_none (`Unknown, `Function ("alloyop__restd_" ^ string_of_int i, [a; k])))
  ))
  ::accu


let univ =
  "def_univ", `Forall (["x", `Unknown], equivalence
    (`Predicate ("alloyth__elem", [`Unknown, `Variable "x"; `Unknown, `Constant "univ"]))
    (`Conjunction [fol_of_one (`Unknown, `Variable "x"); ar 1 "x"]))

let iden =
  let x = `Unknown, `Variable "x" and y = `Unknown, `Variable "y" in
  "def_iden", 
  `Forall (["x", `Unknown], equivalence
    (`Predicate ("alloyth__elem", [x; `Unknown, `Constant "iden"]))
    (`Exists (["y", `Unknown], `Predicate ("alloyth__tuple2", [x; y; y]))))



let theorie accu n = 
  let accu1 = univ::iden::tuple1::singl::elem_singl::none::incl::in_antisym::accu in
  let accu2 = arite accu1 n in
  let accu3 = tuple accu2 n in
  let accu4 = plier_gauche plus accu3 n in
  let accu5 = plier_gauche moins accu4 n in
  let accu6 = plier_gauche inter accu5 n in
  let accu7 = tilde accu6 in
  let accu8 =
    plier_gauche (fun ak i -> plier_gauche (fun ak2 j -> jointure ak2 i j) ak (min n (n + 2 - i))) accu7 n
  in
  let accu9 =
    plier_gauche (fun ak i -> plier_gauche (fun ak2 j -> fleche ak2 i j) ak (min n (n - i))) accu8 n
  in
  let accu10 = plier_gauche restriction_gauche accu9 n in
  let accu11 = plier_gauche restriction_droite accu10 n in
  accu11
    
let convert_res
    (res : alloy_formule resultat)
    : fol_formula resultat =

  {
    res_axiomes = List.rev_map (fun (x, f) -> (x, close_fol_of_alloy f)) res.res_axiomes;
    res_theoremes = List.rev_map (fun (x, f) -> (x, close_fol_of_alloy f)) res.res_theoremes;
  }