(* Constraints due to the signature system. *)

open Symb
open Alloyast

let constr_sigext (accu : (ident * alloy_formule) list) env = 
  prerr_endline "Processing signature extensions (including abstract ones).";
  List.fold_left
    (fun accu2 s ->
      begin
        prerr_endline ("Processing sig: " ^ s.sig_name);
        let l = List.filter (fun t -> t.sig_type = Some (`Extends s.sig_name)) env.env_sig in
        let r = match l with
          | [] -> `None
          | a::q -> List.fold_left (fun l k -> `Plus (None, (l, `Variable k.sig_name))) (`Variable a.sig_name) q
        in
        if s.sig_mult = Some `Abstract
        then (nouveau_symbole ("ax_abstract_extended_" ^ s.sig_name), `Equality (`Variable s.sig_name, r))::accu
        else if r = `None
        then accu
        else (nouveau_symbole ("ax_extended_" ^ s.sig_name), `In (r, `Variable s.sig_name))::accu
      end
    )
    accu
    env.env_sig

let constr_sigmaster (accu : (ident * alloy_formule) list) env =
  prerr_endline "Processing master signature disjunction.";
  match List.filter (fun t -> t.sig_type = None) env.env_sig with
    | [] -> accu
    | a::q -> (nouveau_symbole ("ax_master_sigs"), `Equality (`Univ, List.fold_left (fun l k -> `Plus (None, (l,
      (`Variable k.sig_name)))) (`Variable a.sig_name) q))::accu

let constr_sigin accu env =
  prerr_endline "Processing subsets ('in' signatures).";
  List.fold_left
    (fun accu2 s ->
      match s.sig_type with
        | Some (`In r) ->
            let f =
              `In (`Variable s.sig_name, r)
            in (nouveau_symbole ("def_" ^ s.sig_name), f)::accu
        | _ -> accu
    )
    accu
    env.env_sig

(*
  Warning : the following function returns accu AND the list of all the
  non-unary rels along with their types.
*)

let constr_rel (accu : (ident * alloy_formule) list) env = 
  let accu2, accu_rel =
    List.fold_left
      (fun (accu, accu_rel) s ->
        List.fold_left
          begin fun (accu, accu_rel) r ->
            let rec aux accu2 = function
              | [] -> (r.sigrel_name, [s.sig_name::r.sigrel_type])::accu2
              | (n, t)::q when n = r.sigrel_name -> (n,
                    (s.sig_name::r.sigrel_type)::t)::(List.rev_append accu2 q)
              | t::q -> aux (t::accu2) q
            in
            let accu3 =
              (if r.sigrel_function
              then let n = ("fonct_" ^ r.sigrel_name ^ "_" ^ s.sig_name)
              in let v = nouveau_symbole n
              in let f = `Forall ([v, `Variable s.sig_name], `One (`Jointure
                (None, (`Variable v, `Variable r.sigrel_name))))
              in (nouveau_symbole ("ax_" ^ n), f)::accu
              else accu)
            in (accu3, aux [] accu_rel)
          end
          (accu, accu_rel)
          s.sig_rels)
      (accu, [])
      env.env_sig
  in
  List.fold_left
    (fun accu (rn, rt) ->
      let ens = List.fold_left
        (fun accu_t t ->
          `Plus (None, (accu_t, List.fold_left (fun accu_x s -> `Fleche (None, (accu_x,
          `Variable s))) (`Variable (List.hd t)) (List.tl t))))
        (let t = List.hd rt
        in List.fold_left (fun accu_x s -> `Fleche ((None, (accu_x, `Variable s))))
             (`Variable (List.hd t))
             (List.tl t))
        (List.tl rt)
      in
      let f = `In (`Variable rn, ens)
      in
      (nouveau_symbole ("def_" ^ rn), f)::accu
    )
    accu
    accu_rel


let constr_pred accu env =

  List.fold_left (fun accu2 p ->
    let vars_param = List.map (fun (x, _) -> `Variable x) p.corps_param
    in
    ("def__" ^ p.corps_nom,
    `Forall (
      p.corps_param,
      equivalence (`Predicate (p.corps_nom, vars_param)) p.corps_corps
    ))::accu2)
    accu
    env.env_pred


let constr_fun accu env =

  List.fold_left (fun accu2 p ->
    let vars_param = List.map (fun (x, _) -> `Variable x) p.corps_param
    in
    ("def__" ^ p.corps_nom,
    `Forall (
      p.corps_param,
      (`Equality (`Fonction (p.corps_nom, vars_param), p.corps_corps))
    ))::accu2)
    accu
    env.env_fun


let finaliser
    (env : 'token env)
    : int * alloy_formule resultat =

  let accu0 = env.env_fact in
  let accu1 = constr_sigext accu0 env in
  let accu2 = constr_sigmaster accu1 env in
  let accu3 = constr_sigin accu2 env in
  let accu4 = constr_rel accu3 env in
  let accu5 = constr_pred accu4 env in
  let accu6 = constr_fun accu5 env in
  let rho =
    List.fold_left max_arite_sig (fun b -> failwith ("arite non trouvee: " ^ b)) env.env_sig
  in
  let m1, accu7 = List.fold_left
    (fun (m, accu) (x, f) -> let n, g = max_arite_form env.env_pred env.env_fun rho f in (max m n, (x, g)::accu))
    (0, [])
    accu6
  in 
  let m2, assert1 = List.fold_left
    (fun (m, accu) (x, f) -> let n, g = max_arite_form env.env_pred env.env_fun rho f in (max m n, (x, g)::accu))
    (m1, [])
    env.env_assert
  in
  m1, {
    res_axiomes = accu7;
    res_theoremes = assert1;
  }