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


(* BEGIN Charles Bouillaguet *)

open Symb

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 boool = [
  `True | `False 
]  (** Boolean variables *)

type term = basesort * [
  `Constant of ident
| `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. *)



(* implication: Forges an implication formula. *)

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

  `Disjunction [`Negation h; c]
 

let equivalence
    (f : fol_formula)
    (g : fol_formula) 
    : fol_formula =

  `Conjunction [implication f g; implication g f]


let rec clore_terme scope (_, t) = `Unknown, match t with
  | `Variable i when not (List.mem i scope) -> `Constant i
  | `Function (f, l) -> `Function (f, List.map (clore_terme scope) l)
  | _ -> t

let rec clore_formule scope = function
  | `Predicate (f, l) -> `Predicate (f, List.map (clore_terme scope) l)
  | `Equality (u, v) -> `Equality (clore_terme scope u, clore_terme scope v)
  | `Negation n -> `Negation (clore_formule scope n)
  | `Conjunction l -> `Conjunction (List.rev_map (clore_formule scope) l)
  | `Disjunction l -> `Disjunction (List.rev_map (clore_formule scope) l)
  | `Exists (l, f) -> `Exists (l, clore_formule (List.rev_append (List.rev_map fst l) scope) f)
  | `Forall (l, f) -> `Forall (l, clore_formule (List.rev_append (List.rev_map fst l) scope) f)
  | f -> f
   


(* Substitution *)

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 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 rec subst_naive_aux neg od nw = function
  | `Exists (l, f) -> `Exists (l, subst_naive_aux neg od nw f)
  | `Forall (l, f) -> `Forall (l, subst_naive_aux neg od nw f)
  | `Negation f -> neg od nw f
  | `Conjunction l -> `Conjunction (List.rev_map (subst_naive_aux neg od nw) l)
  | `Disjunction l -> `Disjunction (List.rev_map (subst_naive_aux neg od nw) l)
  | #boool as f -> f
  | #fol_atom as f -> subst_naive_atome od nw f