(* Merci à Charles Bouillaguet, Cachan INFO 2004, en stage au MIT 2006 *)


(* BEGIN Charles Bouillaguet *)

type basesort = [
  `I | `O | `F | `B | `Unknown (* Unused. Use `Unknown by default. *)
]

type sort = [
  basesort |  `Set of basesort (* Unused. Use basesort `Unknown by
                                  default. *)
]

type ident = string

let string_of_ident
    (ident : ident)
    : string =

  ident



type boool = [
  `True | `False | `BoolVar of ident | `NegatedBoolVar of ident (* Boolvars
                                                                   are
                                                                   unused
                                                                   here. *)
]  (** Boolean variables *)

type term = basesort * [
  `Int of int | `Constant of ident (* Both unused. *)
| `Variable of ident | `Function of ident*(term list)
]

type fol_atom = [
  `Predicate of ident*(term list) | `Equality of (term*term)
]

type fol_formula = [
  boool
| fol_atom
| `Negation of fol_formula
| `Conjunction of fol_formula list
| `Disjunction of fol_formula list
| `Exists of (ident*basesort) list * fol_formula
| `Forall of (ident*basesort) list * fol_formula
]

(* END Charles Bouillaguet *)



(* nouveau_symbole: Creates a fresh variable. *)

let nouveau_symbole
    : 'a -> ident  = 

  let i = ref 0 in fun () -> begin
    incr i;
    "x" ^ string_of_int !i
  end


(* implication: Forges an implication formula. *)

let implication
    (h : fol_formula) (* hypothesis *)
    (c : fol_formula) (* goal *)
    : fol_formula =

  `Disjunction [`Negation h; c]
    


(* Relations *)

type relation = [
  `Unaire of (ident -> fol_formula) (* Unary relation *)
| `Naire of (ident -> relation) (* Relation with arity greater than 1 *)
]



(* Built-in relations *)

let univ
    : relation =

  `Unaire (fun _ -> `True)



let none
    : relation =
  `Unaire (fun _ -> `False)



let iden
    : relation =

  `Naire (fun x -> `Unaire (fun y -> `Equality ((`Unknown, `Variable x),
  (`Unknown, `Variable y))))



(* atome: Creates a relation from an atomic object (which is always a
   variable name introduced by a quantifier). *)

let atome 
    (i : ident) (* Name of the atom *)
    : relation =

  `Unaire (fun x -> `Equality ((`Unknown, `Variable x), (`Unknown, `Variable i)))



(* definition: Defines a named relation. *)

let definition
   (ident : ident) (* Name of the relation *)
    : int -> relation =

  let rec aux accu = function
    | 1 -> `Unaire (fun x -> `Predicate (ident, List.rev ((`Unknown, `Variable x)::accu)))
    | n when n > 1 -> `Naire (fun x -> aux ((`Unknown, `Variable x)::accu) (n - 1))
    | _ -> invalid_arg "Fol.definition: negative arity"
  in aux []



(* defsig: Define a signature as a relation. *)

let defsig 
    (nom : ident) (* Name of the signature. *)
    (x : ident) (* Name of an atom which shall be member of the signature *)
    : fol_formula =

  `Predicate (nom, [`Unknown, `Variable x])



let rec op o f1 f2 = match f1, f2 with
  | `Unaire g1, `Unaire g2 -> `Unaire (fun x -> o (g1 x) (g2 x))
  | `Naire g1, `Naire g2 -> `Naire (fun x -> op o (g1 x) (g2 x))
  | u -> invalid_arg "Fol.op: operation between different arities"


(* si_formule: Alloy implies/else operator
   si_relation: Alloy if/then/else operator *)

let si_formule
    (hyp : fol_formula)
    (vrai : fol_formula)
    (faux : fol_formula)
    : fol_formula =

  `Conjunction [
    implication hyp vrai;
    implication (`Negation hyp) faux;
  ]



let si_relation
    (cond : fol_formula)
    : relation -> relation -> relation =

  op (si_formule cond)
    


(* plus: Alloy + operator *)

let plus 
    : relation -> relation -> relation =

  op (fun a b -> `Disjunction [a; b])



(* moins: Alloy - operator *)

let moins 
    : relation -> relation -> relation =

  op (fun a b -> `Conjunction [a; `Negation b])



(* inter: Alloy & operator *)

let inter
    : relation -> relation -> relation =

  op (fun a b -> `Conjunction [a; b])




(* tilde: Alloy ~ operator *)

let tilde
    : relation -> relation = function

  | `Naire g -> `Naire (fun x -> `Unaire (fun y -> match g y with 
      | `Unaire f -> f x | _ -> invalid_arg "Fol.tilde: non-binary"))
  | _ -> invalid_arg "Fol.tilde: non-binary"



(* jointure: Alloy . operator *)

let jointure
    : relation -> relation -> relation =
  
  let t = nouveau_symbole () in
  


  let rec aux_g f1 = function
    | `Unaire g2 -> `Unaire (fun y ->
        `Exists ([t, `Unknown], `Conjunction [f1 t; g2 x]))
    | `Naire g2 -> `Naire (fun x -> aux_g f1 (g2 x))


  in

  let rec aux_f = function
    | 


  function
    | `Unaire f1 -> begin function
        | `Unaire _ -> failwith "Fol.jointure: both relations are unary"
        | `Naire g1 ->
            let y = nouveau_symbole () in

      end
    | `Naire f1 ->
        let rec aux_g y g =

                    




(* fleche: Alloy -> operator *)

let fleche 
    (f : relation)
    (g : relation)
    : relation =
  
  let rec aux_f = function
    | `Unaire f1 -> `Naire (fun x -> let rec aux_g = function
        | `Unaire g1 -> `Unaire (fun y -> `Conjunction [f1 x; g1 y])
        | `Naire g1 -> `Naire (fun y -> aux_g (g1 y))
      in aux_g g)
    | `Naire f1 -> `Naire (fun x -> aux_f (f1 x))
  in aux_f f



(* restriction_gauche: Alloy <: operator *)

let restriction_gauche
    : relation -> relation -> relation = function

  | `Naire _ -> invalid_arg "Fol.restriction_gauche: non-unary restriction domain"
  | `Unaire cond_f -> begin function
      | `Unaire r_g -> `Unaire (fun x -> `Conjunction [cond_f x; r_g x])
      | `Naire r_g -> `Naire (fun x -> let rec aux = function
          | `Unaire r_g2 -> `Unaire (fun y -> `Conjunction [cond_f x; r_g2 y])
          | `Naire r_g2 -> `Naire (fun y -> aux (r_g2 y))
        in aux (r_g x))
    end



(* restriction_droite: Alloy :> operator *)

let restriction_droite
    (r : relation)
    : relation -> relation = function

      | `Naire 
          _ -> invalid_arg "Fol.restriction_droite: non-unary restriction domain"
      | `Unaire cond_f -> let rec aux = function
          | `Unaire r_f -> `Unaire (fun x -> `Conjunction [r_f x; cond_f x])
          | `Naire r_f -> `Naire (fun y -> aux (r_f y))
        in aux r



(* Multiplicative formulae (mult r) where r is a relation, and mult is one
   of the following : some, no, lone, one. *)

let mult_some
    : relation -> fol_formula =
  
  let rec aux vars = function
  | `Unaire f -> let x = nouveau_symbole () in `Exists ((x, `Unknown)::vars, f x)
  | `Naire f -> let x = nouveau_symbole () in aux ((x, `Unknown)::vars) (f x)
  in aux []



let mult_no 
    (f : relation)
    : fol_formula =

  `Negation (mult_some f)



let mult_lone
    (h : relation) 
    : fol_formula =
  
  let rec aux vars eqs = function
    | `Unaire f, `Unaire g ->
        let x = nouveau_symbole () in let y = nouveau_symbole () in
        `Forall ((x, `Unknown)::(y, `Unknown)::vars, implication
          (`Conjunction [f x; g y]) (`Conjunction ((`Equality ((`Unknown, `Variable
            x), (`Unknown, `Variable y)))::eqs)))
    | `Naire f, `Naire g ->
        let x = nouveau_symbole () in let y = nouveau_symbole () in
        aux ((x, `Unknown)::(y, `Unknown)::vars) ((`Equality ((`Unknown,
        `Variable x), (`Unknown, `Variable y)))::eqs) (f x, g y)
    | _ -> failwith "mult_lone: BUG (this error raised is theoretically a dead code)"
  in aux [] [] (h, h)



let mult_one
    (h : relation)
    : fol_formula = 

  `Conjunction [mult_some h; mult_lone h]



(* Inclusion and equality *)

(* inclusion: Relation inclusion *)

let inclusion
    (r1 : relation) (* sub *)
    (r2 : relation) (* super *)
    : fol_formula =

  let rec aux accu = function
    | `Unaire f1, `Unaire f2 -> 
        let x = nouveau_symbole () in
        `Forall ((x, `Unknown)::accu, implication (f1 x) (f2 x))
    | `Naire f1, `Naire f2 ->
        let x = nouveau_symbole () in
        aux ((x, `Unknown)::accu) (f1 x, f2 x)
    | _ -> invalid_arg "Fol.inclusion: inclusion between different arities"
  in aux [] (r1, r2)



(* egalite : Relation equality *)

let egalite
    (r1 : relation)
    (r2 : relation)
    : fol_formula =
  
  `Conjunction [inclusion r1 r2; inclusion r2 r1]



let contrainte_2earg contr precond = function
  | `Unaire _ -> invalid_arg "Fol.contrainte_2earg: non-binary relation"
  | `Naire f -> let x = nouveau_symbole () in 
    `Forall ([x, `Unknown], implication (precond x) (contr (f x)))



(* fonctionnelle: Relation is functional *)

let relation_fonctionnelle
    : (ident -> fol_formula) -> relation -> fol_formula =

  contrainte_2earg mult_lone



(* totale: Relation is total *)

let relation_totale
    : (ident -> fol_formula) -> relation -> fol_formula = 

  contrainte_2earg mult_some
    


(* fonction: Relation is a function *)

let relation_fonction
    (precond : ident -> fol_formula)
    (r : relation) 
    : fol_formula =

  `Conjunction [relation_fonctionnelle precond r; relation_totale precond r]



(* disjoints : The relations in the given list are disjoint one to the
   other. Actually, this function computes a list of formulae it appends to
   a stack given in input (avoids list concatenation)

   A sequence (A_i) of relations is disjoint one to the other if and only
   if for any i, A_1+...+A_i-1 and A_i are disjoint.

 *)

let rec disjoints
    (accu : fol_formula list)
    : relation list -> fol_formula list = function
        
      | a::b::q -> disjoints ((mult_no (inter a b))::accu) ((plus a b)::q)
      | _ -> accu



(* plusplus: Alloy ++ operator (overriding relations) *)

let plusplus
    (a : relation) 
    (b : relation)
    : relation =

  match a, b with
    | `Unaire _, `Unaire _ -> plus a b
    | `Naire f, `Naire g ->
        `Naire (fun x ->
          let r = g x in
          si_relation (mult_some r) r (f x)
        )
    | _ -> invalid_arg "Fol.plusplus"



(* Processing an Alloy module. *)

(* The environment where signatures, predicates and facts will be stored. *)

exception Introuvable of string

type 'token env = {
  env_noms_rels : ident list; (* The list of all the relation names
                                 (excluding sig names) *)
  env_rels : ident -> relation option; (* The relation object
                                          corresponding to every defined
                                          relation, including 
                                          signatures. For global relations,
                                          only a definition will be stored,
                                          but this store will be also used
                                          for predicate arguments.
                                       *)
  env_types : ident -> ident list list; (* The types of the global relations *)
  env_peres : ident list; (* The names of the most basic signatures *)
  env_fils : ident -> ident list; (* List of the signatures extending a
                                     given one (the "extended", not the
                                     "in") *)
  env_abstract : ident list; (* Abstract signatures *)
  env_contraintes : fol_formula list; (* The facts. Also the typing
                                         constraints, added at the
                                         finalization step. *)
  env_predicats : (ident * (relation list -> fol_formula)) list; (* The "pred"
                                                                    predicates. *)
  env_fonctions : (ident * (relation list -> relation)) list; (* The "fun"
                                                                 functions
                                                              *)
  env_theoremes : (ident * fol_formula) list;

  (* The following extra fields are needed to manage module importation.
     They are using the 'token type variable, which represents a type defined in the
     parsing module, which depends on this module. So can be defined some kind of
     cross-module recursion.
  *)
  env_searchpath: string list;
  env_modulenames: ident list;
  env_token: Lexing.lexbuf -> 'token; (* The lexer *)
  env_modul: (Lexing.lexbuf -> 'token) -> Lexing.lexbuf -> 'token env -> 'token env; (* The parser *)

  

}


(* Generic empty environment.
   Must be a function because of env_token and env_modul functions. *)

let empty_env
    (_ : 'a)
    : 'token env =

  {
    env_noms_rels = [];
    env_rels = (fun _ -> None);
    env_types = (fun _ -> []);
    env_peres = [];
    env_fils = (fun _ -> []);
    env_abstract = [];
    env_contraintes = [];
    env_predicats = [];
    env_fonctions = [];
    env_theoremes = [];
    env_searchpath = [];
    env_modulenames = [];
    env_token = (fun _ -> failwith "Fol.env_token: lexer is undefined");
    env_modul = (fun _ _ x -> prerr_endline "Fol.env_modul: warning: parser is undefined"; x);
  }


(* Function to copy an environment, forgetting about parser and lexer.
   This (unused in practice) could be useful for multi-parsing...
*)

let copy_env
    (env : 'token1 env)
    : 'token2 env =

  { (empty_env ()) with
    env_noms_rels = env.env_noms_rels;
    env_rels = env.env_rels;
    env_types = env.env_types;
    env_peres = env.env_peres;
    env_fils = env.env_fils;
    env_abstract = env.env_abstract;
    env_contraintes = env.env_contraintes;
    env_predicats = env.env_predicats;
    env_fonctions = env.env_fonctions;
    env_theoremes = env.env_theoremes;
    env_searchpath = env.env_searchpath;
    env_modulenames = env.env_modulenames;
  }

(* Generic skeleton to process a signature. It returns a modified environment. *)

let sig_generic 
    (nom : ident) (* The name of the signature. *)
    (rels0 : (ident * ident list) list) (* The relations
                                           defined inside the signature,
                                           with the types of their
                                           arguments (the first excluded =
                                           signature being defined) *)
    (foncts : ident list) (* The functional relations defined inside the
                             signature *)
    (env : 'token env) (* The input environment, to which the signature will be
                   appended to construct the output environment *)
    : 'token env =

  prerr_endline ("General signature processing for: " ^ nom);
  let rels = List.map (fun (i, tl) -> (i, nom::tl)) rels0 in
  let def = defsig nom in

  { env with

    env_noms_rels = begin
      prerr_endline ("sig " ^ nom ^ ": BEGIN processing relation names");
      let rec aux accu = function
        | [] -> 
            prerr_endline ("sig " ^ nom ^ ": END processing relation names");
            accu
        | (i, _) :: q when List.mem i accu ->
            prerr_endline ("relation " ^ i ^ ": already existing");
            aux accu q
        | (i, _) :: q ->
            prerr_endline ("adding relation: " ^ i);
            aux (i::accu) q
      in     
      aux env.env_noms_rels rels
    end;

    env_rels = begin
      prerr_endline ("sig " ^ nom ^ " : processing relations");
      let rels1 = (fun n -> if n = nom then Some (`Unaire def) else env.env_rels n) in
      let rels2 = (fun n -> match rels1 n with
        | Some _ as res -> res
        | None -> begin try
            let k = List.length (List.assoc n rels) in
            Some (
              prerr_endline ("relation " ^ n ^ " is " ^ string_of_int k ^ "ary");
              definition n k
            )
          with Not_found -> None
          end)
      in
      rels2;
    end;

    env_types = begin
      prerr_endline ("sig " ^ nom ^ " : processing relation types");
      let types1 = (fun n -> if n = nom then [[nom]] else env.env_types n) in
      let types2 = (fun n -> let l = types1 n in try
        (List.assoc n rels)::l
      with Not_found -> l)
      in
      types2
    end;
    
    env_contraintes = begin
      prerr_endline ("sig " ^ nom ^ ": BEGIN processing functionality constraints");
      let rec aux accu = function
        | [] -> 
            prerr_endline ("sig " ^ nom ^ ": END processing functionality constraints");
            accu
        | n::q ->
            prerr_endline ("functionality constraint for: " ^ n);
            aux ((relation_fonction def (definition n 2))::accu) q
      in aux env.env_contraintes foncts
    end;

  }



(* [abstract] sig Nom *)

let sig_master 
    (nom : ident) (* Signature name *)
    (abstract : bool) (* Is the signature abstract *)
    (rels0, foncts : (ident * ident list) list * (* Relations *)
      ident list) (* Functional relations *)
    (env : 'token env) (* input environment *)
    : 'token env =

  prerr_endline ("Processing master signature: " ^ nom);
  let env2 = (sig_generic nom rels0 foncts env) in {env2 with
    env_peres =
      nom::env2.env_peres;
    env_abstract = (
      if abstract
      then (nom::env2.env_abstract)
      else env2.env_abstract
    );
  }



(* sig Nom in Parent1 + Parent2 & Parent3 ... *)

let sig_in
    (nom : ident) (* Signature name *)
    (parent : relation) (* The in clause, result of processing
                                       the signature expression *)
    (rels0, foncts : (ident * ident list) list * (* Relations *)
      ident list) (* Functional relations *)
    (env : 'token env) (* input environment *)
    : 'token env =

  prerr_endline ("Processing subset signature: " ^ nom);
  let env2 = (sig_generic nom rels0 foncts env) in {
    env2 with
    env_contraintes = (inclusion (definition nom 1) 
      parent)::env2.env_contraintes;
  }


(* [abstract] sig Nom extends Parent *)

let sig_extends
    (nom : ident) (* Signature name *)
    (parent : ident) (* Extended signature *)
    (abstract : bool) (* Is the signature abstract ? *)
    (rels0, foncts : (ident * ident list) list * (* Relations *)
      ident list) (* Functional relations *)
    (env : 'token env) (* Input environment *)
    : 'token env =

  prerr_endline ("Processing extension signature: " ^ nom);
  let env2 = (sig_in nom (definition parent 1) (rels0, foncts) env) in {
    env2 with
    env_fils = (fun n -> if n = parent then (nom::(env2.env_fils n)) else
      env2.env_fils n);
    env_abstract = (if abstract then (nom::env2.env_abstract) else env2.env_abstract);
  }



(* Adding a predicate (Alloy "pred") into the env_predicats field of the
   environment. *)

let predicat
    (nom : ident) (* name *)
    (vars : ident list) (* names of the arguments *)
    (corps : 'token env -> fol_formula) (* body of the formula, using the names in
                                    vars *)
    (env : 'token env) (* source environment, into which the predicate will be
                   added, and also into which the values of the arguments
                   will be stored whenever the predicate is applied *)
    : 'token env =

  prerr_endline ("Processing predicate: " ^ nom);
  { env with
    env_predicats = (
      (nom, fun l ->
        let rec build_formula accu = function
          | ([], []) -> corps accu
          | v::w, r::s ->
              let accu2 = { accu with
                env_rels = (fun x -> if x = v then Some r else accu.env_rels x)
              } in build_formula accu2 (w, s)
          | _ -> invalid_arg ("pred " ^ nom ^ ": wrong number of arguments")
              in build_formula env (vars, l)
      )::env.env_predicats
    )
  }



(* Samely, adding a function (Alloy "fun") into the env_fonctions field of
   the environment *)

let fonction
    (nom : ident) (* name *)
    (vars : ident list) (* names of the arguments *)
    (corps : 'token env -> relation) (* body of the formula, using the names in
                                    vars *)
    (env : 'token env) (* source environment, into which the predicate will be
                   added, and also into which the values of the arguments
                   will be stored whenever the predicate is applied *)
    : 'token env =

  prerr_endline ("Processing function: " ^ nom);
  { env with
    env_fonctions = (
      (nom, fun l ->
        let rec build_relation accu = function
          | ([], []) -> corps accu
          | v::w, r::s ->
              let accu2 = { accu with
                env_rels = (fun x -> if x = v then Some r else accu.env_rels x)
              } in build_relation accu2 (w, s)
          | _ -> invalid_arg ("fun " ^ nom ^ ": wrong number of arguments")
              in build_relation env (vars, l)
      )::env.env_fonctions
    )
  }


(* Adding an axiom (Alloy "fact") into the env_contraintes field of the
   environment. *)

let axiome
    (nom : ident)
    (corps : 'token env -> fol_formula)
    (env : 'token env)
    : 'token env =

  prerr_endline ("Processing axiom: " ^ nom);
  { env with
    env_contraintes = (corps env)::env.env_contraintes }


(* Samely, adding a theorem (Alloy "assert") into the env_theorem field *)

let theoreme 
    (nom : ident)
    (corps : 'token env -> fol_formula)
    (env : 'token env)
    : 'token env =

  prerr_endline ("Processing theorem: " ^ nom);
  { env with
    env_theoremes = (nom, corps env)::env.env_theoremes }



(* Finalization : build typing constraints related to signatures. *)

type resultat = {
  res_axiomes : fol_formula list; (* axioms. *)
  res_theoremes : (ident * fol_formula) list; (* theorems *)
}

let finaliser 
    (env : 'token env)
    : resultat = 

  prerr_endline "BEGIN Finalizing";
  let envf = {
    res_axiomes = (

      prerr_endline "Processing abstract signatures";
      let rec aux_abstract accu = function
        | [] -> accu
        | (a::l) ->
            prerr_endline ("Processing abstract sig: " ^ a);
            let f = inclusion (definition a 1) (`Unaire (fun x ->
              `Disjunction (`False::(List.map (fun s -> defsig s x)
                (env.env_fils a))))) in
            aux_abstract (f::accu) l
      in let ax1 = aux_abstract env.env_contraintes env.env_abstract
      in

      prerr_endline "Processing disjoint signatures";
      let rec aux_fils_disjoints accu = function
        | [] -> accu
        | a::q ->
            prerr_endline ("Processing disjoint subsigs for: " ^ a);
            let f = env.env_fils a in
            let accu2 = 
              aux_fils_disjoints (disjoints accu (List.map (fun n ->
                definition n 1) f)) f
            in aux_fils_disjoints accu2 q
      in let ax19 = aux_fils_disjoints ax1 env.env_peres
      in
      let ax2 = disjoints ax19 (List.map (fun n -> definition n 1) env.env_peres) in

      prerr_endline "Processing relation typesystem";
      let rec aux_typage accu = function
        | [] -> accu
        | a::q -> begin
            prerr_endline ("Processing type of relation: " ^ a);
            match env.env_types a with
            | [] -> aux_typage accu q
            | t1::_ as t ->
                let rec aux_v ak = function
                  | [] -> ak
                  | _::r -> let v = nouveau_symbole () in aux_v (v::ak) r
                in let v = aux_v [] t1
                in
                let rec aux_t ak = function
                  | [] -> ak
                  | b::r ->
                      let rec aux_t_v ak2 = function
                        | [], [] -> ak2
                        | s::u, x::w -> aux_t_v ((defsig s x)::ak2) (u, w)
                        | _ -> invalid_arg "Fol.res_axiome: i"
                      in let d = `Conjunction (aux_t_v [] (b, v))
                      in aux_t (d::ak) r
                in let f1 =`Negation (`Predicate (a, List.map
                  (fun x -> (`Unknown, `Variable x)) v))
                in let f = `Forall (List.map (fun x -> (x, `Unknown)) v,
                `Disjunction (f1::(aux_t [] t)))
                in aux_typage (f::accu) q
          end                  
      in let ax3 = aux_typage ax2 env.env_noms_rels
      in
      
      prerr_endline "Processing disjunction of master sigs";

      (
        inclusion univ
          (`Unaire (fun x -> `Disjunction (`False::(List.map (fun s ->
            defsig s x) env.env_peres))))
      ) :: ax3
      

    );

    res_theoremes = begin
      env.env_theoremes;
    end;
  } in begin
    prerr_endline "END Finalizing. Enjoy the formulae !";
    envf
  end
  




(* Callings *)

(* Calling a predicate *)

let appel_predicat
    (nom : ident)
    (rels : relation list)
    (env : 'token env)
    : fol_formula =

  prerr_endline ("Calling predicate: " ^ nom);
  List.assoc nom env.env_predicats rels



(* Samely, calling a function *)

let appel_fonction
    (nom : ident)
    (rels : relation list)
    (env : 'token env)
    : relation =

  prerr_endline ("Calling function: " ^ nom);
  List.assoc nom env.env_fonctions rels



(* Calling a relation *)

let appel_relation
    (nom : ident)
    (env : 'token env)
    : relation =

  prerr_endline ("Calling relation: " ^ nom);
  match env.env_rels nom with
    | None -> invalid_arg ("relation " ^ nom ^ ": not found")
    | Some r -> r


(* Forall and exists *)

let quantifier
    quant vars corps env =
  
  let noms = List.map fst vars in

  let vars_quant = List.map (fun (v, _) -> (v, `Unknown)) vars in
  
  let precond = `Conjunction (List.map (fun (v, r) -> match r with
    | `Unaire f -> f v
    | _ -> invalid_arg "Fol.quantifier: cannot quantify over relations") vars) in
  
  let env2 = { env with
    env_rels = begin fun n ->
      if List.mem n noms
      then Some (atome n)
      else env.env_rels n
    end;
  } in

  quant vars_quant precond (corps env2)


let quant_forall
    (vars : (ident * relation) list)
    :  ('token env -> fol_formula)
    -> 'token env
    -> fol_formula =

  quantifier (fun vars_quant precond corps ->
    `Forall (vars_quant, implication precond corps)) vars


let quant_exists
    (vars : (ident * relation) list)
    : ('token env -> fol_formula)
    -> 'token env
    -> fol_formula =

  quantifier (fun vars_quant precond corps ->
    `Exists (vars_quant, `Conjunction [precond; corps])) vars



(* Processing a file. It's weird, because it could depend on the parser.
   Actually even because of the type system. But finally not.
   I have to make env dependent on the type of the tokens. 
 *)

let process_channel
    (ch : in_channel)
    (env : 'token env)
    : 'token env =

  let lexbuf = Lexing.from_channel ch in
  env.env_modul env.env_token lexbuf env


(* Process a file. Please note : if the file does not exist, then returns None.
   This, in order to allow the calling function to retry with another file name
   when importing a module. *)

let process_file
    (name : string)
    (env : 'token env)
    : 'token env option =

  if Sys.file_exists name
  then
    let ch =
      prerr_endline ("File found: " ^ name);
      open_in name in
    let env2 = process_channel ch env
    in Some (
      prerr_endline ("End of file: " ^ name);
      close_in ch;
      env2
    )
  else begin
    prerr_endline ("File not found: " ^ name);
    None
  end


(* Then, process a module. Given the search pathnames, and the module path,
   it successively tries one of them with the path of the given module. If
   it does not work, then try with the module path from which the first path item
   has been removed.

   Note that if a module of the given name has already been processed, then
   reloading another module with the same name will have no effect. *)

let process_module
    (modulepath, modulename : ident list * ident)
    (env: 'token env)
    : 'token env = 

  let searchpath = env.env_searchpath in
  prerr_endline ("Processing module: " ^ modulename);
  if List.mem modulename env.env_modulenames
  then begin
    prerr_endline ("Module with name: " ^ modulename ^ " already loaded. Skipping.");
    env
  end else begin
    prerr_endline ("No module loaded yet with name: " ^ modulename ^ ". Searching for corresponding file.");
    let rec build_fullnames = function
      | [], l -> l
      | a::q, [] -> build_fullnames (q, [a])
      | a::q, (b::_ as l) -> build_fullnames (q, (Filename.concat a b)::l)
    in let fullnames = build_fullnames (List.rev modulepath, [modulename ^ ".als"])
    in let sp = ((Sys.getcwd ())::searchpath)

    in let rec aux_fullnames = function
      | [] -> invalid_arg ("Fol.process_module: module " ^ modulename ^ " not found")
      | a::q -> let rec aux_searchpaths = function
          | [] -> 
              prerr_endline "No matching files found. Downgrading module path.";
              aux_fullnames q
          | p::r -> let f = Filename.concat p a in begin match
              prerr_endline ("Trying file: " ^ f);
              process_file (Filename.concat p a) env
            with
              | None -> aux_searchpaths r
              | Some e -> e
            end
        in aux_searchpaths sp
    in aux_fullnames fullnames
  end