]> matita.cs.unibo.it Git - helm.git/commitdiff
added a new type for proofs.
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 26 Apr 2006 09:21:07 +0000 (09:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 26 Apr 2006 09:21:07 +0000 (09:21 +0000)
14 files changed:
components/tactics/.depend
components/tactics/Makefile
components/tactics/autoTactic.ml
components/tactics/paramodulation/equality.ml [new file with mode: 0644]
components/tactics/paramodulation/equality.mli [new file with mode: 0644]
components/tactics/paramodulation/equality_indexing.ml
components/tactics/paramodulation/equality_indexing.mli
components/tactics/paramodulation/indexing.ml
components/tactics/paramodulation/indexing.mli
components/tactics/paramodulation/inference.ml
components/tactics/paramodulation/inference.mli
components/tactics/paramodulation/saturation.ml
components/tactics/paramodulation/utils.ml
components/tactics/paramodulation/utils.mli

index 10862a5b016c7bb78694e7e44ecb769072472c39..41cc4bb6779322542701fec58bf8f6396a29d986 100644 (file)
@@ -5,11 +5,13 @@ reductionTactics.cmi: proofEngineTypes.cmi
 proofEngineStructuralRules.cmi: proofEngineTypes.cmi 
 primitiveTactics.cmi: proofEngineTypes.cmi 
 metadataQuery.cmi: proofEngineTypes.cmi 
-paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi 
+paramodulation/equality.cmi: paramodulation/utils.cmi 
+paramodulation/inference.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
+    paramodulation/equality.cmi 
 paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \
-    paramodulation/inference.cmi 
+    paramodulation/equality.cmi 
 paramodulation/indexing.cmi: paramodulation/utils.cmi \
-    paramodulation/inference.cmi paramodulation/equality_indexing.cmi 
+    paramodulation/equality_indexing.cmi paramodulation/equality.cmi 
 paramodulation/saturation.cmi: proofEngineTypes.cmi 
 variousTactics.cmi: proofEngineTypes.cmi 
 autoTactic.cmi: proofEngineTypes.cmi 
@@ -56,30 +58,34 @@ metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
     hashtbl_equiv.cmx metadataQuery.cmi 
 paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi 
 paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi 
-paramodulation/inference.cmo: paramodulation/utils.cmi \
-    proofEngineReduction.cmi proofEngineHelpers.cmi metadataQuery.cmi \
+paramodulation/equality.cmo: paramodulation/utils.cmi \
+    proofEngineReduction.cmi paramodulation/equality.cmi 
+paramodulation/equality.cmx: paramodulation/utils.cmx \
+    proofEngineReduction.cmx paramodulation/equality.cmi 
+paramodulation/inference.cmo: paramodulation/utils.cmi proofEngineHelpers.cmi \
+    metadataQuery.cmi paramodulation/equality.cmi \
     paramodulation/inference.cmi 
-paramodulation/inference.cmx: paramodulation/utils.cmx \
-    proofEngineReduction.cmx proofEngineHelpers.cmx metadataQuery.cmx \
+paramodulation/inference.cmx: paramodulation/utils.cmx proofEngineHelpers.cmx \
+    metadataQuery.cmx paramodulation/equality.cmx \
     paramodulation/inference.cmi 
 paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
-    paramodulation/inference.cmi paramodulation/equality_indexing.cmi 
+    paramodulation/equality.cmi paramodulation/equality_indexing.cmi 
 paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
-    paramodulation/inference.cmx paramodulation/equality_indexing.cmi 
+    paramodulation/equality.cmx paramodulation/equality_indexing.cmi 
 paramodulation/indexing.cmo: paramodulation/utils.cmi \
     paramodulation/inference.cmi paramodulation/equality_indexing.cmi \
-    paramodulation/indexing.cmi 
+    paramodulation/equality.cmi paramodulation/indexing.cmi 
 paramodulation/indexing.cmx: paramodulation/utils.cmx \
     paramodulation/inference.cmx paramodulation/equality_indexing.cmx \
-    paramodulation/indexing.cmi 
+    paramodulation/equality.cmx paramodulation/indexing.cmi 
 paramodulation/saturation.cmo: paramodulation/utils.cmi reductionTactics.cmi \
     proofEngineTypes.cmi proofEngineReduction.cmi primitiveTactics.cmi \
     paramodulation/inference.cmi paramodulation/indexing.cmi \
-    paramodulation/saturation.cmi 
+    paramodulation/equality.cmi paramodulation/saturation.cmi 
 paramodulation/saturation.cmx: paramodulation/utils.cmx reductionTactics.cmx \
     proofEngineTypes.cmx proofEngineReduction.cmx primitiveTactics.cmx \
     paramodulation/inference.cmx paramodulation/indexing.cmx \
-    paramodulation/saturation.cmi 
+    paramodulation/equality.cmx paramodulation/saturation.cmi 
 variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
     proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
     variousTactics.cmi 
@@ -88,10 +94,10 @@ variousTactics.cmx: tacticals.cmx proofEngineTypes.cmx \
     variousTactics.cmi 
 autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \
     proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \
-    paramodulation/inference.cmi autoTactic.cmi 
+    paramodulation/equality.cmi autoTactic.cmi 
 autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
     proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \
-    paramodulation/inference.cmx autoTactic.cmi 
+    paramodulation/equality.cmx autoTactic.cmi 
 introductionTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
     introductionTactics.cmi 
 introductionTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
index cb38579e1b6308e339cdc1ab3d8a1a6428283e91..2cecc04019710d2e02ea38b98dc2dd535dc25c89 100644 (file)
@@ -7,6 +7,7 @@ INTERFACE_FILES = \
        tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
        primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
   paramodulation/utils.mli \
+  paramodulation/equality.mli\
   paramodulation/inference.mli\
   paramodulation/equality_indexing.mli\
   paramodulation/indexing.mli \
index 42df90768263b2749c30f9ff81c1c0dcf4f9b12c..9db6ed1c9094d3816c374592d401d5ba35fcdd7f 100644 (file)
@@ -334,7 +334,7 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
       | Some _ ->
           let _, metasenv, _, _ = proof in
           let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          full || (Inference.term_is_equality meta_goal)
+          full || (Equality.term_is_equality meta_goal)
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
new file mode 100644 (file)
index 0000000..70f8f85
--- /dev/null
@@ -0,0 +1,738 @@
+(* cOpyright (C) 2005, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
+
+
+(******* CIC substitution ***************************************************)
+
+type cic_substitution = Cic.substitution
+let cic_apply_subst = CicMetaSubst.apply_subst
+let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
+let cic_ppsubst = CicMetaSubst.ppsubst
+let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
+let cic_flatten_subst subst =
+    List.map
+      (fun (i, (context, term, ty)) ->
+         let context = (* cic_apply_subst_context subst*) context in
+         let term = cic_apply_subst subst term in
+         let ty = cic_apply_subst subst ty in  
+         (i, (context, term, ty))) subst
+let rec cic_lookup_subst meta subst =
+  match meta with
+  | Cic.Meta (i, _) -> (
+      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
+      in cic_lookup_subst t subst 
+      with Not_found -> meta
+    )
+  | _ -> meta
+;;
+
+let cic_merge_subst_if_possible s1 s2 =
+  let already_in = Hashtbl.create 13 in
+  let rec aux acc = function
+    | ((i,_,x) as s)::tl ->
+        (try 
+          let x' = Hashtbl.find already_in i in
+          if x = x' then aux acc tl else None
+        with
+        | Not_found -> 
+            Hashtbl.add already_in i x;
+            aux (s::acc) tl)
+    | [] -> Some acc 
+  in  
+    aux [] (s1@s2)
+;;
+
+(******** NAIF substitution **************************************************)
+(* 
+ * naif version of apply subst; the local context of metas is ignored;
+ * we assume the substituted term must be lifted according to the nesting
+ * depth of the meta. 
+ * Alternatively, we could used implicit instead of metas 
+ *)
+
+type naif_substitution = (int * Cic.term) list 
+
+let naif_apply_subst subst term =
+ let rec aux k t =
+   match t with
+       Cic.Rel _ -> t
+     | Cic.Var (uri,exp_named_subst) -> 
+         let exp_named_subst' =
+           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+         in
+           Cic.Var (uri, exp_named_subst')
+    | Cic.Meta (i, l) -> 
+        (try
+          aux k (CicSubstitution.lift k (List.assoc i subst)) 
+         with Not_found -> t)
+    | Cic.Sort _
+    | Cic.Implicit _ -> t
+    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
+    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
+    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
+    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
+    | Cic.Appl [] -> assert false
+    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
+    | Cic.Const (uri,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+        in
+          if exp_named_subst' != exp_named_subst then
+            Cic.Const (uri, exp_named_subst')
+          else
+            t (* TODO: provare a mantenere il piu' possibile sharing *)
+    | Cic.MutInd (uri,typeno,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+        in
+          Cic.MutInd (uri,typeno,exp_named_subst')
+    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
+        in
+          Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
+    | Cic.MutCase (sp,i,outty,t,pl) ->
+        let pl' = List.map (aux k) pl in
+          Cic.MutCase (sp, i, aux k outty, aux k t, pl')
+    | Cic.Fix (i, fl) ->
+        let len = List.length fl in
+        let fl' =
+         List.map 
+           (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
+        in
+          Cic.Fix (i, fl')
+    | Cic.CoFix (i, fl) ->
+        let len = List.length fl in
+        let fl' =
+          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
+        in
+          Cic.CoFix (i, fl')
+in
+  aux 0 term
+;;
+
+(* naif version of apply_subst_metasenv: we do not apply the 
+substitution to the context *)
+
+let naif_apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, context, naif_apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.mem_assoc i subst))
+      metasenv)
+
+let naif_ppsubst names subst =
+  "{" ^ String.concat "; "
+    (List.map
+      (fun (idx, t) ->
+         Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
+    subst) ^ "}"
+;;
+
+let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
+
+let naif_flatten_subst subst = 
+  List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
+;;
+
+let rec naif_lookup_subst meta subst =
+  match meta with
+    | Cic.Meta (i, _) ->
+        (try
+          naif_lookup_subst (List.assoc i subst) subst
+        with
+            Not_found -> meta)
+    | _ -> meta
+;;
+
+let naif_merge_subst_if_possible s1 s2 =
+  let already_in = Hashtbl.create 13 in
+  let rec aux acc = function
+    | ((i,x) as s)::tl ->
+        (try 
+          let x' = Hashtbl.find already_in i in
+          if x = x' then aux acc tl else None
+        with
+        | Not_found -> 
+            Hashtbl.add already_in i x;
+            aux (s::acc) tl)
+    | [] -> Some acc 
+  in  
+    aux [] (s1@s2)
+;;
+
+(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
+
+type substitution = naif_substitution
+let apply_subst = naif_apply_subst
+let apply_subst_metasenv = naif_apply_subst_metasenv
+let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
+let buildsubst = naif_buildsubst
+let flatten_subst = naif_flatten_subst
+let lookup_subst = naif_lookup_subst
+
+(* filter out from metasenv the variables in substs *)
+let filter subst metasenv =
+  List.filter
+    (fun (m, _, _) ->
+         try let _ = List.find (fun (i, _) -> m = i) subst in false
+         with Not_found -> true)
+    metasenv
+;;
+
+let is_in_subst i subst = List.mem_assoc i subst;;
+  
+let merge_subst_if_possible = naif_merge_subst_if_possible;;
+
+let empty_subst = [];;
+
+(********* EQUALITY **********************************************************)
+
+type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type uncomparable = int -> int 
+type equality =
+    uncomparable *       (* trick to break structural equality *)
+    int  *               (* weight *)
+    proof * 
+    (Cic.term *          (* type *)
+     Cic.term *          (* left side *)
+     Cic.term *          (* right side *)
+     Utils.comparison) * (* ordering *)  
+    Cic.metasenv  *      (* environment for metas *)
+    int                  (* id *)
+and proof = new_proof * old_proof 
+
+and new_proof = 
+  | Exact of Cic.term
+  | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)  
+and old_proof =
+  | NoProof (* term is the goal missing a proof *)
+  | BasicProof of substitution * Cic.term
+  | ProofBlock of
+      substitution * UriManager.uri *
+        (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
+  | ProofGoalBlock of old_proof * old_proof 
+  | ProofSymBlock of Cic.term list * old_proof
+  | SubProof of Cic.term * int * old_proof
+and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+;;
+
+(* globals *)
+let maxid = ref 0;;
+let id_to_eq = Hashtbl.create 1024;;
+
+let freshid () =
+  incr maxid; !maxid
+;;
+
+let reset () = 
+  maxid := 0;
+  Hashtbl.clear  id_to_eq
+;;
+
+let uncomparable = fun _ -> 0
+
+let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
+  let id = freshid () in
+  let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
+  Hashtbl.add id_to_eq id eq;
+  eq
+;;
+
+let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
+  (weight,proof,(ty,l,r,o),m,id)
+
+let string_of_equality ?env eq =
+  match env with
+  | None ->
+      let w, _, (ty, left, right, o), _ , id = open_equality eq in
+      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" 
+              id w (CicPp.ppterm ty)
+              (CicPp.ppterm left) 
+              (Utils.string_of_comparison o) (CicPp.ppterm right)
+  | Some (_, context, _) -> 
+      let names = Utils.names_of_context context in
+      let w, _, (ty, left, right, o), _ , id = open_equality eq in
+      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s" 
+              id w (CicPp.pp ty names)
+              (CicPp.pp left names) (Utils.string_of_comparison o)
+              (CicPp.pp right names)
+;;
+
+let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
+  Pervasives.compare s1 s2
+;;
+
+let rec string_of_proof_old ?(names=[]) = function
+  | NoProof -> "NoProof " 
+  | BasicProof (s, t) -> "BasicProof(" ^ 
+      ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
+  | SubProof (t, i, p) ->
+      Printf.sprintf "SubProof(%s, %s, %s)"
+        (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
+  | ProofSymBlock (_,p) -> 
+      Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
+  | ProofBlock (subst, _, _, _ ,(_,eq),old) -> 
+      let _,(_,p),_,_,_ = open_equality eq in 
+      "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
+      string_of_proof_old p ^ ")"
+  | ProofGoalBlock (p1, p2) ->
+      Printf.sprintf "ProofGoalBlock(%s, %s)"
+        (string_of_proof_old p1) (string_of_proof_old p2)
+;;
+
+
+let proof_of_id id =
+  try
+    let (_,(p,_),(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+      p,m,l,r
+  with
+      Not_found -> assert false
+
+
+let string_of_proof_new ?(names=[]) p gp = 
+  let str_of_rule = function
+    | SuperpositionRight -> "SupR"
+    | SuperpositionLeft -> "SupL"
+    | Demodulation -> "Demod"
+  in
+  let str_of_pos = function
+    | Utils.Left -> "left"
+    | Utils.Right -> "right"
+  in
+  let fst4 (x,_,_,_) = x in
+  let rec aux margin name = 
+    let prefix = String.make margin ' ' ^ name ^ ": " in function 
+    | Exact t -> 
+        Printf.sprintf "%sExact (%s)\n" 
+          prefix (CicPp.pp t names)
+    | Step (subst,(rule,eq1,(pos,eq2),pred)) -> 
+        Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
+          prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
+          (CicPp.pp pred names)^ 
+        aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^ 
+        aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2)) 
+  in
+  aux 0 "" p ^ 
+  String.concat "\n" 
+    (List.map 
+      (fun (pos,i,s,t) -> 
+        (Printf.sprintf 
+          "GOAL: %s %d %s %s\n" 
+            (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^ 
+        aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i)))
+      gp)
+;;
+
+let ppsubst = ppsubst ~names:[]
+
+(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
+let build_ens_for_sym_eq sym_eq_URI termlist =
+  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+  match obj with
+  | Cic.Constant (_, _, _, uris, _) ->
+      assert (List.length uris <= List.length termlist);
+      let rec aux = function
+        | [], tl -> [], tl
+        | (uri::uris), (term::tl) ->
+            let ens, args = aux (uris, tl) in
+            (uri, term)::ens, args
+        | _, _ -> assert false
+      in
+      aux (uris, termlist)
+  | _ -> assert false
+;;
+
+let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
+  let rec do_build_proof proof = 
+    match proof with
+    | NoProof ->
+        Printf.fprintf stderr "WARNING: no proof!\n";
+        noproof
+    | BasicProof (s,term) -> apply_subst s term
+    | ProofGoalBlock (proofbit, proof) ->
+        print_endline "found ProofGoalBlock, going up...";
+        do_build_goal_proof proofbit proof
+    | ProofSymBlock (termlist, proof) ->
+        let proof = do_build_proof proof in
+        let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
+        Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
+    | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
+        let t' = Cic.Lambda (name, ty, bo) in
+        let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
+        let proof' = do_build_proof proof in
+        let eqproof = do_build_proof eqproof in
+        let what, other =
+          if pos = Utils.Left then what, other else other, what
+        in
+        apply_subst subst
+          (Cic.Appl [Cic.Const (eq_URI, []); ty;
+                     what; t'; eqproof; other; proof'])
+    | SubProof (term, meta_index, proof) ->
+        let proof = do_build_proof proof in
+        let eq i = function
+          | Cic.Meta (j, _) -> i = j
+          | _ -> false
+        in
+        ProofEngineReduction.replace
+          ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
+
+  and do_build_goal_proof proofbit proof =
+    match proof with
+    | ProofGoalBlock (pb, p) ->
+        do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
+    | _ -> do_build_proof (replace_proof proofbit proof)
+
+  and replace_proof newproof = function
+    | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
+        let eqproof' = replace_proof newproof eqproof in
+        ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
+    | ProofGoalBlock (pb, p) ->
+        let pb' = replace_proof newproof pb in
+        ProofGoalBlock (pb', p)
+    | BasicProof _ -> newproof
+    | SubProof (term, meta_index, p) ->
+        SubProof (term, meta_index, replace_proof newproof p)
+    | p -> p
+  in
+  do_build_proof proof 
+;;
+
+let build_proof_term_new proof =
+  let rec aux extra = function
+     | Exact term -> term, []
+     | Step (subst,(_, id1, (pos,id2), pred)) ->
+         let p,m1,_,_ = proof_of_id id1 in
+         let p1,m2 = aux [] p in
+         let p,m3,l,r = proof_of_id id2 in 
+         let p2,m4 = aux [] p in
+         let p1 = apply_subst subst p1 in
+         let p2 = apply_subst subst p2 in
+         let l = apply_subst subst l in
+         let r = apply_subst subst r in
+         let pred = apply_subst subst pred in
+         let ty = (* Cic.Implicit None *) 
+           match pred with
+           | Cic.Lambda (_,ty,_) -> ty 
+           | _ -> assert false
+         in
+         let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+           if pos = Utils.Left then l,r else r,l
+         in
+         let eq_URI =
+           match pos with 
+           | Utils.Left -> Utils.eq_ind_URI () 
+           | Utils.Right ->  Utils.eq_ind_r_URI ()
+         in 
+         (Cic.Appl [
+           Cic.Const (eq_URI, []); 
+           ty; what; pred; p1; other; p2]), 
+         (apply_subst_metasenv subst (m1@m2@m3@m4))
+  in
+   aux [] proof
+         
+
+let build_goal_proof l (refl,reflmenv) =
+  let proof, menv, subst = 
+   List.fold_left 
+   (fun  (current_proof,current_menv,current_subst) (pos,id,subst,pred) -> 
+      let p,m,l,r = proof_of_id id in
+      let p,m1 = build_proof_term_new p in
+      let p = apply_subst subst p in
+      let l = apply_subst subst l in
+      let r = apply_subst subst r in
+      let pred = apply_subst subst pred in
+      let newm = apply_subst_metasenv subst (m@m1) in
+      let ty = (* Cic.Implicit None *) 
+        match pred with
+        | Cic.Lambda (_,ty,_) -> ty 
+        | _ -> assert false
+      in
+      let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+        if pos = Utils.Right then l,r else r,l
+      in
+      let eq_URI =
+        match pos with
+          | Utils.Left -> Utils.eq_ind_r_URI ()
+          | Utils.Right ->  Utils.eq_ind_URI () 
+      in
+        ((Cic.Appl [Cic.Const (eq_URI, []);
+          ty; what; pred; current_proof; other; p]), 
+         current_menv @ newm, subst @ current_subst))
+   (refl,reflmenv,[]) l
+  in
+  proof, menv
+;;
+
+let refl_proof ty term = 
+  Cic.Appl 
+    [Cic.MutConstruct 
+       (LibraryObjects.eq_URI (), 0, 1, []);
+       ty; term]
+;;
+
+let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
+
+let relocate newmeta menv =
+  let subst, metasenv, newmeta = 
+    List.fold_right 
+      (fun (i, context, ty) (subst, menv, maxmeta) ->         
+        let irl = [] (*
+         CicMkImplicit.identity_relocation_list_for_metavariable context *)
+        in
+        let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
+        let newmeta = maxmeta, context, ty in
+        newsubst, newmeta::menv, maxmeta+1) 
+      menv ([], [], newmeta+1)
+  in
+  let metasenv = apply_subst_metasenv subst metasenv in
+  let subst = flatten_subst subst in
+  subst, metasenv, newmeta
+
+
+let fix_metas newmeta eq = 
+  let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
+  (* debug 
+  let _ , eq = 
+    fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
+  prerr_endline (string_of_equality eq); *)
+  let subst, metasenv, newmeta = relocate newmeta menv in
+  let ty = apply_subst subst ty in
+  let left = apply_subst subst left in
+  let right = apply_subst subst right in
+  let fix_proof = function
+    | NoProof -> NoProof 
+    | BasicProof (subst',term) -> BasicProof (subst@subst',term)
+    | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
+        (*
+        let newsubst = 
+          List.map
+            (fun (i, (context, term, ty)) ->
+               let context = apply_subst_context subst context in
+               let term = apply_subst subst term in
+               let ty = apply_subst subst ty in  
+                 (i, (context, term, ty))) subst' in *)
+          ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
+    | p -> assert false
+  in
+  let fix_new_proof = function
+    | Exact p -> Exact (apply_subst subst p)
+    | Step (s,(r,id1,(pos,id2),pred)) -> 
+        Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
+  in
+  let new_p = fix_new_proof p1 in
+  let old_p = fix_proof p2 in
+  let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
+  (* debug prerr_endline (string_of_equality eq); *)
+  newmeta+1, eq  
+
+exception NotMetaConvertible;;
+
+let meta_convertibility_aux table t1 t2 =
+  let module C = Cic in
+  let rec aux ((table_l, table_r) as table) t1 t2 =
+    match t1, t2 with
+    | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
+        let m1_binding, table_l =
+          try List.assoc m1 table_l, table_l
+          with Not_found -> m2, (m1, m2)::table_l
+        and m2_binding, table_r =
+          try List.assoc m2 table_r, table_r
+          with Not_found -> m1, (m2, m1)::table_r
+        in
+        if (m1_binding <> m2) || (m2_binding <> m1) then
+          raise NotMetaConvertible
+        else (
+          try
+            List.fold_left2
+              (fun res t1 t2 ->
+                 match t1, t2 with
+                 | None, Some _ | Some _, None -> raise NotMetaConvertible
+                 | None, None -> res
+                 | Some t1, Some t2 -> (aux res t1 t2))
+              (table_l, table_r) tl1 tl2
+          with Invalid_argument _ ->
+            raise NotMetaConvertible
+        )
+    | C.Var (u1, ens1), C.Var (u2, ens2)
+    | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
+        aux_ens table ens1 ens2
+    | C.Cast (s1, t1), C.Cast (s2, t2)
+    | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
+    | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
+    | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
+        let table = aux table s1 s2 in
+        aux table t1 t2
+    | C.Appl l1, C.Appl l2 -> (
+        try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
+        with Invalid_argument _ -> raise NotMetaConvertible
+      )
+    | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
+        when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
+    | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
+        when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
+        aux_ens table ens1 ens2
+    | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
+        when (UriManager.eq u1 u2) && i1 = i2 ->
+        let table = aux table s1 s2 in
+        let table = aux table t1 t2 in (
+          try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
+          with Invalid_argument _ -> raise NotMetaConvertible
+        )
+    | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
+        try
+          List.fold_left2
+            (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
+               if i1 <> i2 then raise NotMetaConvertible
+               else
+                 let res = (aux res s1 s2) in aux res t1 t2)
+            table il1 il2
+        with Invalid_argument _ -> raise NotMetaConvertible
+      )
+    | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
+        try
+          List.fold_left2
+            (fun res (n1, s1, t1) (n2, s2, t2) ->
+               let res = aux res s1 s2 in aux res t1 t2)
+            table il1 il2
+        with Invalid_argument _ -> raise NotMetaConvertible
+      )
+    | t1, t2 when t1 = t2 -> table
+    | _, _ -> raise NotMetaConvertible
+        
+  and aux_ens table ens1 ens2 =
+    let cmp (u1, t1) (u2, t2) =
+      Pervasives.compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
+    in
+    let ens1 = List.sort cmp ens1
+    and ens2 = List.sort cmp ens2 in
+    try
+      List.fold_left2
+        (fun res (u1, t1) (u2, t2) ->
+           if not (UriManager.eq u1 u2) then raise NotMetaConvertible
+           else aux res t1 t2)
+        table ens1 ens2
+    with Invalid_argument _ -> raise NotMetaConvertible
+  in
+  aux table t1 t2
+;;
+
+
+let meta_convertibility_eq eq1 eq2 =
+  let _, _, (ty, left, right, _), _,_ = open_equality eq1 in
+  let _, _, (ty', left', right', _), _,_ = open_equality eq2 in
+  if ty <> ty' then
+    false
+  else if (left = left') && (right = right') then
+    true
+  else if (left = right') && (right = left') then
+    true
+  else
+    try
+      let table = meta_convertibility_aux ([], []) left left' in
+      let _ = meta_convertibility_aux table right right' in
+      true
+    with NotMetaConvertible ->
+      try
+        let table = meta_convertibility_aux ([], []) left right' in
+        let _ = meta_convertibility_aux table right left' in
+        true
+      with NotMetaConvertible ->
+        false
+;;
+
+
+let meta_convertibility t1 t2 =
+  if t1 = t2 then
+    true
+  else
+    try
+      ignore(meta_convertibility_aux ([], []) t1 t2);
+      true
+    with NotMetaConvertible ->
+      false
+;;
+
+exception TermIsNotAnEquality;;
+
+let term_is_equality term =
+  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+  match term with
+  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+  | _ -> false
+;;
+
+let equality_of_term proof term =
+  let eq_uri = LibraryObjects.eq_URI () in
+  let iseq uri = UriManager.eq uri eq_uri in
+  match term with
+  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+      let o = !Utils.compare_terms t1 t2 in
+      let stat = (ty,t1,t2,o) in
+      let w = Utils.compute_equality_weight stat in
+      let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
+      e
+  | _ ->
+      raise TermIsNotAnEquality
+;;
+
+let is_weak_identity eq = 
+  let _,_,(_,left, right,_),_,_ = open_equality eq in
+  left = right || meta_convertibility left right 
+;;
+
+let is_identity (_, context, ugraph) eq = 
+  let _,_,(ty,left,right,_),menv,_ = open_equality eq in
+  left = right ||
+  (* (meta_convertibility left right)) *)
+  fst (CicReduction.are_convertible ~metasenv:menv context left right ugraph)
+;;
+
+
+let term_of_equality equality =
+  let _, _, (ty, left, right, _), menv, _= open_equality equality in
+  let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
+  let argsno = List.length menv in
+  let t =
+    CicSubstitution.lift argsno
+      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+  in
+  snd (
+    List.fold_right
+      (fun (i,_,ty) (n, t) ->
+         let name = Cic.Name ("X" ^ (string_of_int n)) in
+         let ty = CicSubstitution.lift (n-1) ty in
+         let t = 
+           ProofEngineReduction.replace
+             ~equality:eq ~what:[i]
+             ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
+         in
+           (n-1, Cic.Prod (name, ty, t)))
+      menv (argsno, t))
+;;
+
diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
new file mode 100644 (file)
index 0000000..9ef8d21
--- /dev/null
@@ -0,0 +1,115 @@
+(* Copyright (C) 2006, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
+
+type substitution 
+
+type rule = SuperpositionRight | SuperpositionLeft |Demodulation
+
+type equality 
+
+and proof = new_proof * old_proof
+
+and new_proof =
+    Exact of Cic.term
+  | Step of substitution * (rule * int * (Utils.pos * int) * Cic.term)
+
+and old_proof =
+    NoProof
+  | BasicProof of substitution * Cic.term
+  | ProofBlock of substitution * UriManager.uri * (Cic.name * Cic.term) *
+      Cic.term * (Utils.pos * equality) * old_proof
+  | ProofGoalBlock of old_proof * old_proof
+  | ProofSymBlock of Cic.term list * old_proof
+  | SubProof of Cic.term * int * old_proof
+
+and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+       
+
+val empty_subst : substitution
+val apply_subst : substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv : substitution -> Cic.metasenv -> Cic.metasenv
+val ppsubst : substitution -> string
+val buildsubst : 
+  int -> Cic.context -> Cic.term -> Cic.term -> substitution -> 
+    substitution
+val flatten_subst : substitution -> substitution 
+val lookup_subst : Cic.term -> substitution -> Cic.term
+val filter : substitution -> Cic.metasenv -> Cic.metasenv
+val is_in_subst : int -> substitution -> bool
+val merge_subst_if_possible: 
+  substitution -> substitution -> 
+    substitution option
+
+val reset : unit -> unit
+
+val mk_equality :
+  int * proof * 
+  (Cic.term * Cic.term * Cic.term * Utils.comparison) *
+  Cic.metasenv -> 
+    equality
+    
+val open_equality :
+  equality ->
+    int * proof * 
+    (Cic.term * Cic.term * Cic.term * Utils.comparison) *
+    Cic.metasenv * int
+val compare : equality -> equality -> int
+val string_of_equality : ?env:Utils.environment -> equality -> string
+val string_of_proof_old : ?names:(Cic.name option)list -> old_proof -> string
+val string_of_proof_new : 
+  ?names:(Cic.name option)list -> new_proof -> goal_proof -> string
+val build_proof_term_new: new_proof -> Cic.term * Cic.metasenv
+val build_proof_term_old: ?noproof:Cic.term -> old_proof -> Cic.term
+val build_goal_proof: 
+  goal_proof -> (Cic.term * Cic.metasenv) -> Cic.term * Cic.metasenv
+val refl_proof: Cic.term -> Cic.term -> Cic.term 
+(** ensures that metavariables in equality are unique *)
+val fix_metas: int -> equality -> int * equality
+val metas_of_proof: proof -> int list
+
+exception TermIsNotAnEquality;;
+
+(**
+   raises TermIsNotAnEquality if term is not an equation.
+   The first Cic.term is a proof of the equation
+*)
+val equality_of_term: Cic.term -> Cic.term -> equality
+
+(**
+   Re-builds the term corresponding to this equality
+*)
+val term_of_equality: equality -> Cic.term
+val term_is_equality: Cic.term -> bool
+
+(** tests a sort of alpha-convertibility between the two terms, but on the
+    metavariables *)
+val meta_convertibility: Cic.term -> Cic.term -> bool
+
+(** meta convertibility between two equations *)
+val meta_convertibility_eq: equality -> equality -> bool
+
+val is_weak_identity: equality -> bool
+val is_identity: Utils.environment -> equality -> bool
+
index 4c07731d51f3bb4e46b2c58aa1dce78e181800d4..d5e5353e9bd585f58427237e6083a952d7e62bf4 100644 (file)
@@ -27,7 +27,7 @@
 
 module type EqualityIndex =
   sig
-    module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+    module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
     val arities : (Cic.term, int) Hashtbl.t
     type key = Cic.term
     type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
@@ -35,16 +35,18 @@ module type EqualityIndex =
     val retrieve_generalizations : t -> key -> PosEqSet.t
     val retrieve_unifiables : t -> key -> PosEqSet.t
     val init_index : unit -> unit
-    val remove_index : t -> Inference.equality -> t
-    val index : t -> Inference.equality -> t
-    val in_index : t -> Inference.equality -> bool
+    val remove_index : t -> Equality.equality -> t
+    val index : t -> Equality.equality -> t
+    val in_index : t -> Equality.equality -> bool
   end
 
 module DT = 
 struct
     module OrderedPosEquality = struct
-       type t = Utils.pos * Inference.equality
-       let compare = Pervasives.compare
+       type t = Utils.pos * Equality.equality
+       let compare (p1,e1) (p2,e2) = 
+         let rc = Pervasives.compare p1 p2 in
+           if rc = 0 then Equality.compare e1 e2 else rc
       end
 
     module PosEqSet = Set.Make(OrderedPosEquality);;
@@ -58,7 +60,7 @@ struct
     ;;
 
     let remove_index tree equality = 
-      let _, _, (_, l, r, ordering), _ = equality in
+      let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
        match ordering with
          | Utils.Gt -> remove_index tree l (Utils.Left, equality)
          | Utils.Lt -> remove_index tree r (Utils.Right, equality)
@@ -67,7 +69,7 @@ struct
                remove_index tree l (Utils.Left, equality)
 
     let index tree equality = 
-      let _, _, (_, l, r, ordering), _ = equality in
+      let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
        match ordering with
          | Utils.Gt -> index tree l (Utils.Left, equality)
          | Utils.Lt -> index tree r (Utils.Right, equality)
@@ -77,9 +79,9 @@ struct
   
 
     let in_index tree equality = 
-      let _, _, (_, l, r, ordering), _ = equality in
+      let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
       let meta_convertibility (pos,equality') = 
-       Inference.meta_convertibility_eq equality equality' 
+       Equality.meta_convertibility_eq equality equality' 
       in
        in_index tree l meta_convertibility || in_index tree r meta_convertibility
 
@@ -88,8 +90,10 @@ struct
 module PT = 
   struct
     module OrderedPosEquality = struct
-       type t = Utils.pos * Inference.equality
-       let compare = Pervasives.compare
+       type t = Utils.pos * Equality.equality
+       let compare (p1,e1) (p2,e2) = 
+         let rc = Pervasives.compare p1 p2 in
+           if rc = 0 then Equality.compare e1 e2 else rc
       end
 
     module PosEqSet = Set.Make(OrderedPosEquality);;
@@ -103,7 +107,7 @@ module PT =
     ;;
 
     let remove_index tree equality = 
-      let _, _, (_, l, r, ordering), _ = equality in
+      let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
          match ordering with
          | Utils.Gt -> remove_index tree l (Utils.Left, equality)
          | Utils.Lt -> remove_index tree r (Utils.Right, equality)
@@ -112,7 +116,7 @@ module PT =
                remove_index tree l (Utils.Left, equality)
 
     let index tree equality = 
-      let _, _, (_, l, r, ordering), _ = equality in
+      let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
        match ordering with
          | Utils.Gt -> index tree l (Utils.Left, equality)
          | Utils.Lt -> index tree r (Utils.Right, equality)
@@ -122,9 +126,9 @@ module PT =
   
 
     let in_index tree equality = 
-      let _, _, (_, l, r, ordering), _ = equality in
+      let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
       let meta_convertibility (pos,equality') = 
-       Inference.meta_convertibility_eq equality equality' 
+       Equality.meta_convertibility_eq equality equality' 
       in
        in_index tree l meta_convertibility || in_index tree r meta_convertibility
 end
index d7c3bec5ec179db7cb33028b566f84ea694f8578..58b28458d6308f5fb620b7279af45ec894fc2d8b 100644 (file)
@@ -25,7 +25,7 @@
 
 module type EqualityIndex =
   sig
-    module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+    module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
     val arities : (Cic.term, int) Hashtbl.t
     type key = Cic.term
     type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
@@ -33,9 +33,9 @@ module type EqualityIndex =
     val retrieve_generalizations : t -> key -> PosEqSet.t
     val retrieve_unifiables : t -> key -> PosEqSet.t
     val init_index : unit -> unit
-    val remove_index : t -> Inference.equality -> t
-    val index : t -> Inference.equality -> t
-    val in_index : t -> Inference.equality -> bool
+    val remove_index : t -> Equality.equality -> t
+    val index : t -> Equality.equality -> t
+    val in_index : t -> Equality.equality -> bool
   end
 
 module DT : EqualityIndex
index 873cc5698cadab2be35ce92860a7cab7ad7c14ec..d71e7c5a793702bbdd2210f40b9f44ebe5146699 100644 (file)
@@ -62,7 +62,7 @@ let string_of_res ?env =
     | Some (t, s, m, u, ((p,e), eq_URI)) ->
         Printf.sprintf "Some: (%s, %s, %s)" 
           (Utils.string_of_pos p)
-          (Inference.string_of_equality ?env e)
+          (Equality.string_of_equality ?env e)
           (CicPp.ppterm t)
 ;;
 
@@ -85,7 +85,7 @@ let print_candidates ?env mode term res =
        (List.map
           (fun (p, e) ->
              Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
-               (Inference.string_of_equality ?env e))
+               (Equality.string_of_equality ?env e))
           res));
 ;;
 
@@ -93,7 +93,7 @@ let print_candidates ?env mode term res =
 let indexing_retrieval_time = ref 0.;;
 
 
-let apply_subst = Inference.apply_subst
+let apply_subst = Equality.apply_subst
 
 let index = Index.index
 let remove_index = Index.remove_index
@@ -103,7 +103,7 @@ let init_index = Index.init_index
 
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-        (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -124,19 +124,20 @@ let check_for_duplicates metas msg =
 let check_res res msg =
   match res with
       Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
-        let eqs = Inference.string_of_equality (snd eq_found) in
+        let eqs = Equality.string_of_equality (snd eq_found) in
         check_disjoint_invariant subst menv msg;
         check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
     | None -> ()
 ;;
 
 let check_target context target msg =
-  let w, proof, (eq_ty, left, right, order), metas = target in
+  let w, proof, (eq_ty, left, right, order), metas,_ = 
+    Equality.open_equality target in
   (* check that metas does not contains duplicates *)
-  let eqs = Inference.string_of_equality target in
+  let eqs = Equality.string_of_equality target in
   let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
-  let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
-    @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof)  in
+  let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
+    @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof)  in
   let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
   let _ = if menv <> metas then 
     begin 
@@ -177,13 +178,6 @@ let check_target context target msg =
    the position will always be Left, and if the ordering is left < right,
    position will be Right.
 *)
-let local_max = ref 100;;
-
-let make_variant (p,eq) =
-  let maxmeta, eq = Inference.fix_metas !local_max eq in
-  local_max := maxmeta;
-  p, eq
-;;
 
 let get_candidates ?env mode tree term =
   let t1 = Unix.gettimeofday () in
@@ -245,17 +239,21 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
   function
     | [] -> None
     | candidate::tl ->
-        let pos, (_, proof, (ty, left, right, o), metas) = candidate in
+        let pos, equality = candidate in
+       let (_, proof, (ty, left, right, o), metas,_) = 
+         Equality.open_equality equality in
         if Utils.debug_metas then 
           ignore(check_target context (snd candidate) "find_matches");
         if Utils.debug_res then 
           begin
-            let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
-            let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
-            let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
-            let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof))  ^ "\n" in
+            let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
+            let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
+            let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+            let p="proof = "^
+              (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n" 
+            in
               check_for_duplicates metas "gia nella metas";
-              check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
+              check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
           end;
         if check && not (fst (CicReduction.are_convertible
                                 ~metasenv context termty ty ugraph)) then (
@@ -332,7 +330,8 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
   function
     | [] -> []
     | candidate::tl ->
-        let pos, (_, _, (ty, left, right, o), metas) = candidate in
+        let pos, equality = candidate in 
+       let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
         let do_match c eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
@@ -414,24 +413,9 @@ let subsumption env table target =
     ((pos,equation),_)) -> Inference.string_of_equality equation)l))
   in
   *)
-  let _, _, (ty, left, right, _), tmetas = target in
+  let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let metasenv, context, ugraph = env in
   let metasenv = tmetas in
-  let merge_if_possible s1 s2 =
-    let already_in = Hashtbl.create 13 in
-    let rec aux acc = function
-      | ((i,x) as s)::tl ->
-          (try 
-            let x' = Hashtbl.find already_in i in
-            if x = x' then aux acc tl else None
-          with
-          | Not_found -> 
-              Hashtbl.add already_in i x;
-              aux (s::acc) tl)
-      | [] -> Some acc 
-    in  
-      aux [] (s1@s2)
-  in
   let leftr =
     match left with
     | Cic.Meta _ -> []   
@@ -444,7 +428,7 @@ let subsumption env table target =
   let rec ok what = function
     | [] -> None
     | (_, subst, menv, ug, ((pos,equation),_))::tl ->
-        let _, _, (_, l, r, o), m = equation in
+        let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
@@ -461,7 +445,7 @@ let subsumption env table target =
               match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
               raise e
           in
-          (match merge_if_possible subst subst' with
+          (match Equality.merge_subst_if_possible subst subst' with
           | None -> ok what tl
           | Some s -> Some (s, equation))
         with Inference.MatchingFailure ->
@@ -499,11 +483,10 @@ let rec demodulation_aux ?from ?(typecheck=false)
   if List.exists (fun (i,_,_) -> i = 2840) metasenv
   then
     (prerr_endline ("term: " ^(CicPp.ppterm term));
-     List.iter (fun (_,x) -> prerr_endline (Inference.string_of_equality  x))
+     List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality  x))
        candidates;
      prerr_endline ("-------");
      prerr_endline ("+++++++"));
-(*   let candidates = List.map make_variant candidates in *)
   let res =
     match term with
       | C.Meta _ -> None
@@ -610,14 +593,16 @@ let rec demodulation_equality ?from newmeta env table sign target =
   let module HL = HelmLibraryObjects in
   let module U = Utils in
   let metasenv, context, ugraph = env in
-  let w, proof, (eq_ty, left, right, order), metas = target in
+  let w, ((proof_new, proof_old) as proof), 
+     (eq_ty, left, right, order), metas, id = 
+    Equality.open_equality target in
   (* first, we simplify *)
   let right = U.guarded_simpl context right in
   let left = U.guarded_simpl context left in
   let order = !Utils.compare_terms left right in
   let stat = (eq_ty, left, right, order) in 
   let w = Utils.compute_equality_weight stat in
-  let target = w, proof, stat, metas in
+  let target = Equality.mk_equality (w, proof, stat, metas) in
   if Utils.debug_metas then 
     ignore(check_target context target "demod equalities input");
   let metasenv' = (* metasenv @ *) metas in
@@ -630,18 +615,22 @@ let rec demodulation_equality ?from newmeta env table sign target =
       begin
         ignore(check_for_duplicates menv "input1");
         ignore(check_disjoint_invariant subst menv "input2");
-        let substs = Inference.ppsubst subst in 
+        let substs = Equality.ppsubst subst in 
         ignore(check_target context (snd eq_found) ("input3" ^ substs))
       end;
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let (_, (proof'_new,proof'_old), 
+        (ty, what, other, _), menv',id') = Equality.open_equality equality in
     let ty =
-    try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
-      let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
-      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
+      let bo = 
+        Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+(*      let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
+      let name = C.Name "x" in
       incr demod_counter;
       let bo' =
         let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
@@ -650,46 +639,55 @@ let rec demodulation_equality ?from newmeta env table sign target =
       in
       if sign = Utils.Positive then
           (bo,
-           Inference.ProofBlock (
-             subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
+           (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
+                        (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
+           Equality.ProofBlock (
+             subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
       else
+        assert false
+(*
        begin
         prerr_endline "***************************************negative";
         let metaproof = 
           incr maxmeta;
           let irl =
             CicMkImplicit.identity_relocation_list_for_metavariable context in
-(*           debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(*           print_newline (); *)
+(*        debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(*        print_newline (); *)
           C.Meta (!maxmeta, irl)
         in
           let eq_found =
-            let proof' =
+            let proof'_old' =
               let termlist =
                 if pos = Utils.Left then [ty; what; other]
                 else [ty; other; what]
               in
-              Inference.ProofSymBlock (termlist, proof')
+              Equality.ProofSymBlock (termlist, proof'_old)
             in
+            let proof'_new' = assert false (* not implemented *) in
             let what, other =
               if pos = Utils.Left then what, other else other, what
             in
-            pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
+            pos, 
+              Equality.mk_equality 
+                (0, (proof'_new',proof'_old'), 
+                (ty, other, what, Utils.Incomparable),menv')
           in
           let target_proof =
             let pb =
-              Inference.ProofBlock 
+              Equality.ProofBlock 
                (subst, eq_URI, (name, ty), bo',
-                 eq_found, Inference.BasicProof ([],metaproof))
+                 eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
             in
-            match proof with
-            | Inference.BasicProof _ ->
+            assert false, (* not implemented *)
+            (match snd proof with
+            | Equality.BasicProof _ ->
                 (* print_endline "replacing a BasicProof"; *)
                 pb
-            | Inference.ProofGoalBlock (_, parent_proof) ->
+            | Equality.ProofGoalBlock (_, parent_proof) ->
   (* print_endline "replacing another ProofGoalBlock"; *)
-                Inference.ProofGoalBlock (pb, parent_proof)
-            | _ -> assert false
+                Equality.ProofGoalBlock (pb, parent_proof)
+            | _ -> assert false)
           in
         let refl =
           C.Appl [C.MutConstruct (* reflexivity *)
@@ -697,23 +695,28 @@ let rec demodulation_equality ?from newmeta env table sign target =
                   eq_ty; if is_left then right else left]          
         in
         (bo,
-         Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
-       end
+         (assert false, (* not implemented *)
+         Equality.ProofGoalBlock 
+           (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
+      end
+*)
     in
     let newmenv = (* Inference.filter subst *) menv in
     let _ = 
       if Utils.debug_metas then 
         try ignore(CicTypeChecker.type_of_aux'
-          newmenv context (Inference.build_proof_term newproof) ugraph);
+          newmenv context 
+            (Equality.build_proof_term_old (snd newproof)) ugraph);
           () 
         with exc ->                   
           prerr_endline "sempre lui";
-          prerr_endline (Inference.ppsubst subst);
-          prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+          prerr_endline (Equality.ppsubst subst);
+          prerr_endline (CicPp.ppterm 
+            (Equality.build_proof_term_old (snd newproof)));
           prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
-          prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+          prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
           prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
             newmenv));
           raise exc;
@@ -726,7 +729,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
     let res =
       let w = Utils.compute_equality_weight stat in
-      (w, newproof, stat,newmenv) in
+      Equality.mk_equality (w, newproof, stat,newmenv) 
+    in
     if Utils.debug_metas then 
       ignore(check_target context res "buildnew_target output");
     !maxmeta, res 
@@ -741,8 +745,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
-          if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
-            (Inference.meta_convertibility_eq target newtarget) then
+          if (Equality.is_weak_identity newtarget) ||
+            (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
           else 
             demodulation_equality newmeta env table sign newtarget
@@ -752,8 +756,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
           match res with
           | Some t ->
               let newmeta, newtarget = build_newtarget false t in
-                if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
-                  (Inference.meta_convertibility_eq target newtarget) then
+                if (Equality.is_weak_identity newtarget) ||
+                  (Equality.meta_convertibility_eq target newtarget) then
                     newmeta, newtarget
                 else
                    demodulation_equality newmeta env table sign newtarget
@@ -903,6 +907,9 @@ let sup_l_counter = ref 1;;
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
+let superposition_left newmeta (metasenv, context, ugraph) table target = 
+  assert false
+(*
 let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module C = Cic in
   let module S = CicSubstitution in
@@ -910,25 +917,23 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in
-  let weight, proof, (eq_ty, left, right, ordering), menv = target in
+  let weight, proof, (eq_ty, left, right, ordering), menv, id = 
+    Equality.open_equality target 
+  in
   if Utils.debug_metas then
     ignore(check_target context target "superpositionleft");
   let expansions, _ =
     let term = if ordering = U.Gt then left else right in
-      begin 
-        let t1 = Unix.gettimeofday () in
-        let res = betaexpand_term metasenv context ugraph table 0 term in
-        let t2 = Unix.gettimeofday () in
-          beta_expand_time := !beta_expand_time  +. (t2 -. t1);
-        res
-      end
+    betaexpand_term metasenv context ugraph table 0 term
   in
   let maxmeta = ref newmeta in
   let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
 (*     debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
+    let proof'_new, proof'_old = proof' in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       let bo' =  U.guarded_simpl context (apply_subst s (S.subst other bo)) in
@@ -952,26 +957,30 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
             if pos = Utils.Left then [ty; what; other]
             else [ty; other; what]
           in
-          Inference.ProofSymBlock (termlist, proof')
+          proof'_new, (* MAH????? *)
+          Equality.ProofSymBlock (termlist, proof'_old)
         in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+        pos, 
+          Equality.mk_equality 
+            (0, proof', (ty, other, what, Utils.Incomparable), menv')
       in
-      let target_proof =
+      let target_proof = assert false (*
         let pb =
-          Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
-                                Inference.BasicProof ([],metaproof))
+          Equality.ProofBlock 
+            (s, eq_URI, (name, ty), bo'', eq_found,
+            Equality.BasicProof (Equality.empty_subst,metaproof))
         in
         match proof with
-        | Inference.BasicProof _ ->
+        | Equality.BasicProof _ ->
 (*             debug_print (lazy "replacing a BasicProof"); *)
             pb
-        | Inference.ProofGoalBlock (_, parent_proof) ->
+        | Equality.ProofGoalBlock (_, parent_proof) ->
 (*             debug_print (lazy "replacing another ProofGoalBlock"); *)
-            Inference.ProofGoalBlock (pb, parent_proof)
-        | _ -> assert false
+            Equality.ProofGoalBlock (pb, parent_proof)
+        | _ -> assert false*)
       in
       let refl =
         C.Appl [C.MutConstruct (* reflexivity *)
@@ -979,7 +988,10 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
                 eq_ty; if ordering = U.Gt then right else left]
       in
       (bo',
-       Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
+       (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
+         assert false), (* il predicato della beta expand non viene tenuto? *) 
+       Equality.ProofGoalBlock 
+        (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
     in
     let left, right =
       if ordering = U.Gt then newgoal, right else left, newgoal in
@@ -990,12 +1002,12 @@ let superposition_left newmeta (metasenv, context, ugraph) table target =
     build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
 
     let w = Utils.compute_equality_weight stat in
-    (w, newproof, stat, newmenv) 
+    Equality.mk_equality (w, newproof, stat, newmenv) 
 
   in
   !maxmeta, List.map build_new expansions
 ;;
-
+*)
 
 let sup_r_counter = ref 1;;
 
@@ -1013,7 +1025,9 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   let module HL = HelmLibraryObjects in
   let module CR = CicReduction in
   let module U = Utils in 
-  let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in 
+  let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id = 
+    Equality.open_equality target 
+  in 
   if Utils.debug_metas then 
     ignore (check_target context target "superpositionright");
   let metasenv' = newmetas in
@@ -1045,12 +1059,15 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       ignore (check_target context (snd eq_found) "buildnew1" );
     let time1 = Unix.gettimeofday () in
     
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality =  eq_found in
+    let (_, proof', (ty, what, other, _), menv',id') = 
+      Equality.open_equality  equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newgoal, newproof =
       (* qua *)
       let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
-      let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
+(*      let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+      let name = C.Name "x" in
       incr sup_r_counter;
       let bo'' =
         let l, r =
@@ -1059,7 +1076,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
                 S.lift 1 eq_ty; l; r]
       in
       bo',
-      Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
+      ( Equality.Step (s,(Equality.SuperpositionRight,
+                     id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
+       Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
+       
     in
     let newmeta, newequality = 
       let left, right =
@@ -1070,10 +1090,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
       let stat = (eq_ty, left, right, neworder) in
       let eq' =
         let w = Utils.compute_equality_weight stat in
-        (w, newproof, stat, newmenv) in
+        Equality.mk_equality (w, newproof, stat, newmenv) in
       if Utils.debug_metas then 
         ignore (check_target context eq' "buildnew3");
-      let newm, eq' = Inference.fix_metas !maxmeta eq' in
+      let newm, eq' = Equality.fix_metas !maxmeta eq' in
       if Utils.debug_metas then 
         ignore (check_target context eq' "buildnew4");
       newm, eq'
@@ -1087,7 +1107,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
   in
   let new1 = List.map (build_new U.Gt) res1
   and new2 = List.map (build_new U.Lt) res2 in
-  let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
+  let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
   (!maxmeta,
    (List.filter ok (new1 @ new2)))
 ;;
@@ -1101,68 +1121,78 @@ let rec demodulation_goal newmeta env table goal =
   let module HL = HelmLibraryObjects in
   let metasenv, context, ugraph = env in
   let maxmeta = ref newmeta in
-  let proof, metas, term = goal in
+  let (cicproof,proof), metas, term = goal in
   let term = Utils.guarded_simpl (~debug:true) context term in
-  let goal = proof, metas, term in
+  let goal = (cicproof,proof), metas, term in
   let metasenv' = metas in
   
   let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let (_, (proofnew',proof'), (ty, what, other, _), menv',id) = 
+      Equality.open_equality equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let ty =
       try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
       with CicUtil.Meta_not_found _ -> ty
     in
-    let newterm, newproof =
-      let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+    let newterm, newproof, newcicproof =
+      let bo = 
+       Utils.guarded_simpl context (apply_subst subst(S.subst other t)) 
+      in
       let bo' = apply_subst subst t in 
-      let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
+(*      let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
+      let name = C.Name "x" in
       incr demod_counter;
       let metaproof = 
         incr maxmeta;
-        let irl =
-          CicMkImplicit.identity_relocation_list_for_metavariable context in
+        let irl = [] (*
+          CicMkImplicit.identity_relocation_list_for_metavariable context *) in 
 (*         debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
         C.Meta (!maxmeta, irl)
       in
       let eq_found =
-        let proof' =
+        let eq_found_proof =
           let termlist =
             if pos = Utils.Left then [ty; what; other]
             else [ty; other; what]
           in
-          Inference.ProofSymBlock (termlist, proof')
+          Equality.ProofSymBlock (termlist, proof')
         in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+        pos, 
+       Equality.mk_equality 
+         (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
       in
       let goal_proof =
         let pb =
-          Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
-                                eq_found, Inference.BasicProof ([],metaproof))
+          Equality.ProofBlock 
+           (subst, eq_URI, (name, ty), bo',
+             eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
         in
         let rec repl = function
-          | Inference.NoProof ->
+          | Equality.NoProof ->
 (*               debug_print (lazy "replacing a NoProof"); *)
               pb
-          | Inference.BasicProof _ ->
+          | Equality.BasicProof _ ->
 (*               debug_print (lazy "replacing a BasicProof"); *)
               pb
-          | Inference.ProofGoalBlock (_, parent_proof) ->
+          | Equality.ProofGoalBlock (_, parent_proof) ->
 (*               debug_print (lazy "replacing another ProofGoalBlock"); *)
-              Inference.ProofGoalBlock (pb, parent_proof)
-          | Inference.SubProof (term, meta_index, p)  ->
+              Equality.ProofGoalBlock (pb, parent_proof)
+          | Equality.SubProof (term, meta_index, p)  ->
               prerr_endline "subproof!";
-              Inference.SubProof (term, meta_index, repl p)
+              Equality.SubProof (term, meta_index, repl p)
           | _ -> assert false
         in repl proof
       in
-      bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
+      let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+      bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
+        (newcicproofstep::cicproof)
     in
     let newmetasenv = (* Inference.filter subst *) menv in
-    !maxmeta, (newproof, newmetasenv, newterm)
+    !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
   in  
   let res =
     demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
@@ -1171,12 +1201,12 @@ let rec demodulation_goal newmeta env table goal =
   | Some t ->
       let newmeta, newgoal = build_newgoal t in
       let _, _, newg = newgoal in
-      if Inference.meta_convertibility term newg then
-        newmeta, newgoal
+      if Equality.meta_convertibility term newg then
+        true, newmeta, newgoal
       else
         demodulation_goal newmeta env table newgoal
   | None ->
-      newmeta, goal
+      false, newmeta, goal
 ;;
 
 (** demodulation, when the target is a theorem *)
@@ -1191,18 +1221,20 @@ let rec demodulation_theorem newmeta env table theorem =
   let metasenv' = metas in
   
   let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
-    let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+    let pos, equality = eq_found in
+    let (_, proof', (ty, what, other, _), menv',id) = 
+      Equality.open_equality equality in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newty =
       let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
       let bo' = apply_subst subst t in 
       let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
       incr demod_counter;
-      let newproof =
-        Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
-                              Inference.BasicProof ([],term))
+      let newproofold =
+        Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+                              Equality.BasicProof (Equality.empty_subst,term))
       in
-      (Inference.build_proof_term newproof, bo)
+      (Equality.build_proof_term_old newproofold, bo)
     in    
     !maxmeta, (newterm, newty, menv)
   in  
@@ -1213,7 +1245,7 @@ let rec demodulation_theorem newmeta env table theorem =
   | Some t ->
       let newmeta, newthm = build_newtheorem t in
       let newt, newty, _ = newthm in
-      if Inference.meta_convertibility termty newty then
+      if Equality.meta_convertibility termty newty then
         newmeta, newthm
       else
         demodulation_theorem newmeta env table newthm
index 5af20df5c66bc17b93e707f501cd314aae4dd6e2..1c6102a07aa304563d70aac7825a12357aec3e02 100644 (file)
 
 (* $Id$ *)
 
-val beta_expand_time : float ref
-
 module Index :
   sig
     module PosEqSet : Set.S 
-      with type elt = Utils.pos * Inference.equality
+      with type elt = Utils.pos * Equality.equality
       and type t = Equality_indexing.DT.PosEqSet.t
     type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
     type key = Cic.term
   end
 
-val index : Index.t -> Inference.equality -> Index.t
-val remove_index : Index.t -> Inference.equality -> Index.t
-val in_index : Index.t -> Inference.equality -> bool
+val index : Index.t -> Equality.equality -> Index.t
+val remove_index : Index.t -> Equality.equality -> Index.t
+val in_index : Index.t -> Equality.equality -> bool
 val empty : Index.t
 val match_unif_time_ok : float ref
 val match_unif_time_no : float ref
@@ -48,34 +46,35 @@ val build_newtarget_time : float ref
 val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Inference.equality ->
-  (Inference.substitution * Inference.equality) option
+  Equality.equality ->
+  (Equality.substitution * Equality.equality) option
 val superposition_left :
   int ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Inference.equality ->
-   int * Inference.equality list
+  Equality.equality ->
+   int * Equality.equality list
 
 val superposition_right :
   int ->
   'a * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Inference.equality ->
-  int * Inference.equality list
+  Equality.equality ->
+  int * Equality.equality list
 
 val demodulation_equality :
   ?from:string -> 
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Utils.equality_sign -> Inference.equality -> int * Inference.equality
+  Utils.equality_sign -> Equality.equality -> int * Equality.equality
 val demodulation_goal :
   int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  Inference.proof * Cic.metasenv * Index.key ->
-  int * (Inference.proof * Cic.metasenv * Index.key)
+  (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key ->
+  bool * int * 
+   ((Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Index.key)
 val demodulation_theorem :
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
@@ -84,7 +83,5 @@ val demodulation_theorem :
   'a * (Cic.term * Index.key * Cic.metasenv)
 val check_target:
   Cic.context ->
-    Inference.equality -> string -> unit
+    Equality.equality -> string -> unit
 
-(* maxmeta for relocate *)
-val local_max : int ref
index a3894fd84cdbfa374ecc3e570ac8bbbb2fad57df..f088d54543aa265f6550e53bf0552f886c409e8f 100644 (file)
 open Utils;;
 open Printf;;
 
-let metas_of_proof_time = ref 0.;;
-let metas_of_term_time = ref 0.;;
-(*
-type substitution = Cic.substitution 
-let apply_subst = CicMetaSubst.apply_subst
-let apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
-let ppsubst = CicMetaSubst.ppsubst
-let buildsubst n context t ty = (n,(context,t,ty))
-let flatten_subst subst =
-    List.map
-      (fun (i, (context, term, ty)) ->
-        let context = (*` apply_subst_context subst*) context in
-        let term = apply_subst subst term in
-        let ty = apply_subst subst ty in  
-        (i, (context, term, ty))) subst
-let rec lookup_subst meta subst =
-  match meta with
-  | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
-      in lookup_subst t subst 
-      with Not_found -> meta
-    )
-  | _ -> meta
-;;
-*)
-
-(* naif version of apply subst; the local context of metas is ignored;
-we assume the substituted term must be lifted according to the nesting
-depth of the meta. Alternatively, ee could used implicit instead of
-metas *)
-
-
-type substitution = (int * Cic.term) list 
-
-let apply_subst subst term =
- let rec aux k t =
-   match t with
-       Cic.Rel _ -> t
-     | Cic.Var (uri,exp_named_subst) -> 
-        let exp_named_subst' =
-           List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-        in
-          Cic.Var (uri, exp_named_subst')
-    | Cic.Meta (i, l) -> 
-        (try
-          aux k (CicSubstitution.lift k (List.assoc i subst)) 
-         with Not_found -> t)
-    | Cic.Sort _
-    | Cic.Implicit _ -> t
-    | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
-    | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
-    | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
-    | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
-    | Cic.Appl [] -> assert false
-    | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
-    | Cic.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-       in
-         if exp_named_subst' != exp_named_subst then
-           Cic.Const (uri, exp_named_subst')
-         else
-           t (* TODO: provare a mantenere il piu' possibile sharing *)
-    | Cic.MutInd (uri,typeno,exp_named_subst) ->
-       let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-       in
-         Cic.MutInd (uri,typeno,exp_named_subst')
-    | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
-       let exp_named_subst' =
-          List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
-       in
-         Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
-    | Cic.MutCase (sp,i,outty,t,pl) ->
-       let pl' = List.map (aux k) pl in
-         Cic.MutCase (sp, i, aux k outty, aux k t, pl')
-    | Cic.Fix (i, fl) ->
-       let len = List.length fl in
-       let fl' =
-         List.map 
-          (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
-       in
-         Cic.Fix (i, fl')
-    | Cic.CoFix (i, fl) ->
-       let len = List.length fl in
-       let fl' =
-          List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
-       in
-         Cic.CoFix (i, fl')
-in
-  aux 0 term
-;;
-
-(* naif version of apply_subst_metasenv: we do not apply the 
-substitution to the context *)
-
-let apply_subst_metasenv subst metasenv =
-  List.map
-    (fun (n, context, ty) ->
-      (n, context, apply_subst subst ty))
-    (List.filter
-      (fun (i, _, _) -> not (List.mem_assoc i subst))
-      metasenv)
-
-let ppsubst subst =
-  String.concat "\n"
-    (List.map
-      (fun (idx, t) ->
-         sprintf "%d:= %s" idx (CicPp.ppterm t))
-       subst)
-;;
-
-let buildsubst n context t ty = (n,t) ;;
-
-let flatten_subst subst = 
-  List.map (fun (i,t) -> i, apply_subst subst t ) subst
-;;
-
-let rec lookup_subst meta subst =
-  match meta with
-    | Cic.Meta (i, _) ->
-       (try
-         lookup_subst (List.assoc i subst) subst
-       with
-           Not_found -> meta)
-    | _ -> meta
-;;
-
-type equality =
-    int  *               (* weight *)
-    proof * 
-    (Cic.term *          (* type *)
-     Cic.term *          (* left side *)
-     Cic.term *          (* right side *)
-     Utils.comparison) * (* ordering *)  
-    Cic.metasenv        (* environment for metas *)
-
-and proof =
-  | NoProof (* term is the goal missing a proof *)
-  | BasicProof of substitution * Cic.term
-  | ProofBlock of
-      substitution * UriManager.uri *
-        (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
-  | ProofGoalBlock of proof * proof 
-  | ProofSymBlock of Cic.term list * proof
-  | SubProof of Cic.term * int * proof
-;;
-
-let string_of_equality ?env =
-  match env with
-  | None -> (
-      function
-        | w, _, (ty, left, right, o), _ ->
-            Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
-              (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
-    )
-  | Some (_, context, _) -> (
-      let names = names_of_context context in
-      function
-        | w, _, (ty, left, right, o), _ ->
-            Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
-              (CicPp.pp left names) (string_of_comparison o)
-              (CicPp.pp right names)
-    )
-;;
-
-
-let rec string_of_proof = function
-  | NoProof -> "NoProof " 
-  | BasicProof (s, t) -> "BasicProof " ^ 
-      (CicPp.ppterm (apply_subst s t))
-  | SubProof (t, i, p) ->
-      Printf.sprintf "SubProof(%s, %s, %s)"
-        (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
-  | ProofSymBlock _ -> "ProofSymBlock"
-  | ProofBlock (subst, _, _, _ ,_,_) -> 
-      "ProofBlock" ^ (ppsubst subst)
-  | ProofGoalBlock (p1, p2) ->
-      Printf.sprintf "ProofGoalBlock(%s, %s)"
-        (string_of_proof p1) (string_of_proof p2)
-;;
-
-
 let check_disjoint_invariant subst metasenv msg =
   if (List.exists 
-       (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+        (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
   then 
     begin 
       prerr_endline ("not disjoint: " ^ msg);
@@ -221,257 +38,6 @@ let check_disjoint_invariant subst metasenv msg =
     end
 ;;
 
-(* filter out from metasenv the variables in substs *)
-let filter subst metasenv =
-  List.filter
-    (fun (m, _, _) ->
-         try let _ = List.find (fun (i, _) -> m = i) subst in false
-         with Not_found -> true)
-    metasenv
-;;
-
-(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
-let build_ens_for_sym_eq sym_eq_URI termlist =
-  let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
-  match obj with
-  | Cic.Constant (_, _, _, uris, _) ->
-      assert (List.length uris <= List.length termlist);
-      let rec aux = function
-        | [], tl -> [], tl
-        | (uri::uris), (term::tl) ->
-            let ens, args = aux (uris, tl) in
-            (uri, term)::ens, args
-        | _, _ -> assert false
-      in
-      aux (uris, termlist)
-  | _ -> assert false
-;;
-
-
-let build_proof_term ?(noproof=Cic.Implicit None) proof =
-  let rec do_build_proof proof = 
-    match proof with
-    | NoProof ->
-        Printf.fprintf stderr "WARNING: no proof!\n";
-        noproof
-    | BasicProof (s,term) -> apply_subst s term
-    | ProofGoalBlock (proofbit, proof) ->
-        print_endline "found ProofGoalBlock, going up...";
-        do_build_goal_proof proofbit proof
-    | ProofSymBlock (termlist, proof) ->
-        let proof = do_build_proof proof in
-        let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in
-        Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
-    | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
-        let t' = Cic.Lambda (name, ty, bo) in
-        let proof' =
-          let _, proof', _, _ = eq in
-          do_build_proof proof'
-        in
-        let eqproof = do_build_proof eqproof in
-        let _, _, (ty, what, other, _), menv' = eq in
-        let what, other =
-          if pos = Utils.Left then what, other else other, what
-        in
-        apply_subst subst
-          (Cic.Appl [Cic.Const (eq_URI, []); ty;
-                     what; t'; eqproof; other; proof'])
-    | SubProof (term, meta_index, proof) ->
-        let proof = do_build_proof proof in
-        let eq i = function
-          | Cic.Meta (j, _) -> i = j
-          | _ -> false
-        in
-        ProofEngineReduction.replace
-          ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
-
-  and do_build_goal_proof proofbit proof =
-    match proof with
-    | ProofGoalBlock (pb, p) ->
-        do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
-    | _ -> do_build_proof (replace_proof proofbit proof)
-
-  and replace_proof newproof = function
-    | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
-        let eqproof' = replace_proof newproof eqproof in
-        ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
-    | ProofGoalBlock (pb, p) ->
-        let pb' = replace_proof newproof pb in
-        ProofGoalBlock (pb', p)
-    | BasicProof _ -> newproof
-    | SubProof (term, meta_index, p) ->
-        SubProof (term, meta_index, replace_proof newproof p)
-    | p -> p
-  in
-  do_build_proof proof 
-;;
-
-let rec metas_of_term = function
-  | Cic.Meta (i, c) -> [i]
-  | Cic.Var (_, ens) 
-  | Cic.Const (_, ens) 
-  | Cic.MutInd (_, _, ens) 
-  | Cic.MutConstruct (_, _, _, ens) ->
-      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
-  | Cic.Cast (s, t)
-  | Cic.Prod (_, s, t)
-  | Cic.Lambda (_, s, t)
-  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
-  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
-  | Cic.MutCase (uri, i, s, t, l) ->
-      (metas_of_term s) @ (metas_of_term t) @
-        (List.flatten (List.map metas_of_term l))
-  | Cic.Fix (i, il) ->
-      List.flatten
-        (List.map (fun (s, i, t1, t2) ->
-                     (metas_of_term t1) @ (metas_of_term t2)) il)
-  | Cic.CoFix (i, il) ->
-      List.flatten
-        (List.map (fun (s, t1, t2) ->
-                     (metas_of_term t1) @ (metas_of_term t2)) il)
-  | _ -> []
-;;      
-
-let rec metas_of_proof p = 
-  if Utils.debug then
-    let t1 = Unix.gettimeofday () in
-    let res = metas_of_term (build_proof_term p) in
-    let t2 = Unix.gettimeofday () in
-    metas_of_proof_time := !metas_of_proof_time  +. (t2 -. t1);
-    res
-  else 
-    metas_of_term (build_proof_term p)
-;;
-
-
-exception NotMetaConvertible;;
-
-let meta_convertibility_aux table t1 t2 =
-  let module C = Cic in
-  let rec aux ((table_l, table_r) as table) t1 t2 =
-    match t1, t2 with
-    | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
-        let m1_binding, table_l =
-          try List.assoc m1 table_l, table_l
-          with Not_found -> m2, (m1, m2)::table_l
-        and m2_binding, table_r =
-          try List.assoc m2 table_r, table_r
-          with Not_found -> m1, (m2, m1)::table_r
-        in
-        if (m1_binding <> m2) || (m2_binding <> m1) then
-          raise NotMetaConvertible
-        else (
-          try
-            List.fold_left2
-              (fun res t1 t2 ->
-                 match t1, t2 with
-                 | None, Some _ | Some _, None -> raise NotMetaConvertible
-                 | None, None -> res
-                 | Some t1, Some t2 -> (aux res t1 t2))
-              (table_l, table_r) tl1 tl2
-          with Invalid_argument _ ->
-            raise NotMetaConvertible
-        )
-    | C.Var (u1, ens1), C.Var (u2, ens2)
-    | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
-        aux_ens table ens1 ens2
-    | C.Cast (s1, t1), C.Cast (s2, t2)
-    | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
-    | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
-    | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
-        let table = aux table s1 s2 in
-        aux table t1 t2
-    | C.Appl l1, C.Appl l2 -> (
-        try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
-        with Invalid_argument _ -> raise NotMetaConvertible
-      )
-    | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
-        when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
-    | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
-        when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
-        aux_ens table ens1 ens2
-    | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
-        when (UriManager.eq u1 u2) && i1 = i2 ->
-        let table = aux table s1 s2 in
-        let table = aux table t1 t2 in (
-          try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
-          with Invalid_argument _ -> raise NotMetaConvertible
-        )
-    | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
-        try
-          List.fold_left2
-            (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
-               if i1 <> i2 then raise NotMetaConvertible
-               else
-                 let res = (aux res s1 s2) in aux res t1 t2)
-            table il1 il2
-        with Invalid_argument _ -> raise NotMetaConvertible
-      )
-    | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
-        try
-          List.fold_left2
-            (fun res (n1, s1, t1) (n2, s2, t2) ->
-               let res = aux res s1 s2 in aux res t1 t2)
-            table il1 il2
-        with Invalid_argument _ -> raise NotMetaConvertible
-      )
-    | t1, t2 when t1 = t2 -> table
-    | _, _ -> raise NotMetaConvertible
-        
-  and aux_ens table ens1 ens2 =
-    let cmp (u1, t1) (u2, t2) =
-      compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
-    in
-    let ens1 = List.sort cmp ens1
-    and ens2 = List.sort cmp ens2 in
-    try
-      List.fold_left2
-        (fun res (u1, t1) (u2, t2) ->
-           if not (UriManager.eq u1 u2) then raise NotMetaConvertible
-           else aux res t1 t2)
-        table ens1 ens2
-    with Invalid_argument _ -> raise NotMetaConvertible
-  in
-  aux table t1 t2
-;;
-
-
-let meta_convertibility_eq eq1 eq2 =
-  let _, _, (ty, left, right, _), _ = eq1
-  and _, _, (ty', left', right', _), _ = eq2 in
-  if ty <> ty' then
-    false
-  else if (left = left') && (right = right') then
-    true
-  else if (left = right') && (right = left') then
-    true
-  else
-    try
-      let table = meta_convertibility_aux ([], []) left left' in
-      let _ = meta_convertibility_aux table right right' in
-      true
-    with NotMetaConvertible ->
-      try
-        let table = meta_convertibility_aux ([], []) left right' in
-        let _ = meta_convertibility_aux table right left' in
-        true
-      with NotMetaConvertible ->
-        false
-;;
-
-
-let meta_convertibility t1 t2 =
-  if t1 = t2 then
-    true
-  else
-    try
-      ignore(meta_convertibility_aux ([], []) t1 t2);
-      true
-    with NotMetaConvertible ->
-      false
-;;
-
-
 let rec check_irl start = function
   | [] -> true
   | None::tl -> check_irl (start+1) tl
@@ -480,7 +46,6 @@ let rec check_irl start = function
   | _ -> false
 ;;
 
-
 let rec is_simple_term = function
   | Cic.Appl ((Cic.Meta _)::_) -> false
   | Cic.Appl l -> List.for_all is_simple_term l
@@ -497,11 +62,10 @@ let locked menv i =
 ;;
 
 let unification_simple locked_menv metasenv context t1 t2 ugraph =
-  let debug_print x = prerr_endline (Lazy.force x) in
   let module C = Cic in
   let module M = CicMetaSubst in
   let module U = CicUnification in
-  let lookup = lookup_subst in
+  let lookup = Equality.lookup_subst in
   let rec occurs_check subst what where =
     match where with
     | t when what = t -> true
@@ -519,24 +83,24 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     match s, t with
     | s, t when s = t -> subst, menv
     | C.Meta (i, _), C.Meta (j, _) 
-       when (locked locked_menv i) &&(locked locked_menv j) ->
-       raise
+        when (locked locked_menv i) &&(locked locked_menv j) ->
+        raise
           (U.UnificationFailure (lazy "Inference.unification.unif"))
-    | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->        
-       unif subst menv t s
+    | C.Meta (i, _), C.Meta (j, _) when (locked locked_menv i) ->          
+        unif subst menv t s
     | C.Meta (i, _), C.Meta (j, _) when (i > j) && not (locked locked_menv j) ->
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
         raise
           (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t when (locked locked_menv i) -> 
-       raise
+        raise
           (U.UnificationFailure (lazy "Inference.unification.unif"))
     | C.Meta (i, l), t -> (
         try
           let _, _, ty = CicUtil.lookup_meta i menv in
-          assert (not (List.mem_assoc i subst));
-         let subst = (buildsubst i context t ty)::subst in
+          assert (not (Equality.is_in_subst i subst));
+          let subst = Equality.buildsubst i context t ty subst in
           let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
           subst, menv
         with CicUtil.Meta_not_found m ->
@@ -562,9 +126,9 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
     | _, _ ->
         raise (U.UnificationFailure (lazy "Inference.unification.unif"))
   in
-  let subst, menv = unif [] metasenv t1 t2 in
-  let menv = filter subst menv in
-  List.rev subst, menv, ugraph
+  let subst, menv = unif Equality.empty_subst metasenv t1 t2 in
+  let menv = Equality.filter subst menv in
+  subst, menv, ugraph
 ;;
 
 let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
@@ -583,21 +147,21 @@ let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
       raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
     ) else
       if b then
-       (* full unification *)
-       unification_simple [] metasenv context t1 t2 ugraph
+        (* full unification *)
+        unification_simple [] metasenv context t1 t2 ugraph
       else
-       (* matching: metasenv1 is locked *)
-       unification_simple metasenv1 metasenv context t1 t2 ugraph
+        (* matching: metasenv1 is locked *)
+        unification_simple metasenv1 metasenv context t1 t2 ugraph
   in
   if Utils.debug_res then
-           ignore(check_disjoint_invariant subst menv "unif");
+            ignore(check_disjoint_invariant subst menv "unif");
   (* let flatten subst = 
     List.map
       (fun (i, (context, term, ty)) ->
-        let context = apply_subst_context subst context in
-        let term = apply_subst subst term in
-        let ty = apply_subst subst ty in  
-          (i, (context, term, ty))) subst 
+         let context = apply_subst_context subst context in
+         let term = apply_subst subst term in
+         let ty = apply_subst subst ty in  
+           (i, (context, term, ty))) subst 
   in
   let flatten subst = profiler.HExtlib.profile flatten subst in
   let subst = flatten subst in *)
@@ -670,8 +234,11 @@ let find_equalities context proof =
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof = BasicProof ([],p) in
-                    let e = (w, proof, stat, newmetas) in
+                    let proof_old = 
+                      Equality.BasicProof (Equality.empty_subst,p) in
+                    let proof_new = Equality.Exact p in
+                    let proof = proof_new , proof_old in
+                    let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -683,15 +250,19 @@ let find_equalities context proof =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof ([],(C.Rel index)), stat, []) in
+              let p = C.Rel index in
+              let proof_old = Equality.BasicProof (Equality.empty_subst,p) in
+              let proof_new = Equality.Exact p in
+              let proof = proof_new, proof_old in
+              let e = Equality.mk_equality (w, proof,stat,[]) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
           match do_find context term with
           | Some p, newmeta ->
               let tl, newmeta' = (aux (index+1) newmeta tl) in
-             if newmeta' < newmeta then 
-               prerr_endline "big trouble";
+              if newmeta' < newmeta then 
+                prerr_endline "big trouble";
               (index, p)::tl, newmeta' (* max???? *)
           | None, _ ->
               aux (index+1) newmeta tl
@@ -701,7 +272,7 @@ let find_equalities context proof =
   in
   let il, maxm = aux 1 newmeta context in
   let indexes, equalities = List.split il in
-  ignore (List.iter (check_eq context "find") equalities);
+  (* ignore (List.iter (check_eq context "find") equalities); *)
   indexes, equalities, maxm
 ;;
 
@@ -811,17 +382,20 @@ let find_library_equalities dbd context status maxmeta =
                 else
                   C.Appl (term::args)
               in (
-                match head with
-                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                    when (iseq uri) && (ok_types ty newmetas) ->
+                  match head with
+                    | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+                        when (iseq uri) && (ok_types ty newmetas) ->
                     debug_print
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let stat = (ty,t1,t2,o) in
                     let w = compute_equality_weight stat in
-                    let proof = BasicProof ([],p) in
-                    let e = (w, proof, stat, newmetas) in
+                    let proof_old = 
+                      Equality.BasicProof (Equality.empty_subst,p) in
+                    let proof_new = Equality.Exact p in
+                    let proof = proof_new, proof_old in
+                    let e = Equality.mk_equality (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -830,28 +404,32 @@ let find_library_equalities dbd context status maxmeta =
               let o = !Utils.compare_terms t1 t2 in
               let stat = (ty,t1,t2,o) in
               let w = compute_equality_weight stat in
-              let e = (w, BasicProof ([],term), stat, []) in
+              let old_proof = Equality.BasicProof (Equality.empty_subst,term) in
+              let new_proof = Equality.Exact term in 
+              let proof = new_proof, old_proof in
+              let e = Equality.mk_equality (w, proof, stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
         match res with
         | Some e ->
             let tl, newmeta' = aux newmeta tl in
-             if newmeta' < newmeta then 
-               prerr_endline "big trouble";
+              if newmeta' < newmeta then 
+                prerr_endline "big trouble";
               (uri, e)::tl, newmeta' (* max???? *)
         | None ->
             aux newmeta tl
   in
   let found, maxm = aux maxmeta candidates in
   let uriset, eqlist = 
+    let mceq = Equality.meta_convertibility_eq in
     (List.fold_left
        (fun (s, l) (u, e) ->
-          if List.exists (meta_convertibility_eq e) (List.map snd l) then (
+          if List.exists (mceq e) (List.map snd l) then (
             debug_print
               (lazy
                  (Printf.sprintf "NO!! %s already there!"
-                    (string_of_equality e)));
+                    (Equality.string_of_equality e)));
             (UriManager.UriSet.add u s, l)
           ) else (UriManager.UriSet.add u s, (u, e)::l))
        (UriManager.UriSet.empty, []) found)
@@ -917,230 +495,3 @@ let find_context_hypotheses env equalities_indexes =
   res
 ;;
 
-(*
-let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
-  let table = Hashtbl.create (List.length args) in
-
-  let newargs, newmeta =
-    List.fold_right
-      (fun t (newargs, index) ->
-         match t with
-         | Cic.Meta (i, l) ->
-             if Hashtbl.mem table i then
-               let idx = Hashtbl.find table i in
-               ((Cic.Meta (idx, l))::newargs, index+1)
-             else
-               let _ = Hashtbl.add table i index in
-               ((Cic.Meta (index, l))::newargs, index+1)
-         | _ -> assert false)
-      args ([], newmeta+1)
-  in
-
-  let repl where =
-    ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
-      ~where
-  in
-  let menv' =
-    List.fold_right
-      (fun (i, context, term) menv ->
-         try
-           let index = Hashtbl.find table i in
-           (index, context, term)::menv
-         with Not_found ->
-           (i, context, term)::menv)
-      menv []
-  in
-  let ty = repl ty
-  and left = repl left
-  and right = repl right in
-  let metas = 
-    (metas_of_term left) @ 
-      (metas_of_term right) @ 
-      (metas_of_term ty) @ (metas_of_proof p) in
-  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
-  let newargs =
-    List.filter
-      (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
-  in
-  let _ =
-    if List.length metas > 0 then 
-      let first = List.hd metas in
-      (* this new equality might have less variables than its parents: here
-         we fill the gap with a dummy arg. Example:
-         with (f X Y) = X we can simplify
-         (g X) = (f X Y) in
-         (g X) = X. 
-         So the new equation has only one variable, but it still has type like
-         \lambda X,Y:..., so we need to pass a dummy arg for Y
-         (I hope this makes some sense...)
-      *)
-      Hashtbl.iter
-        (fun k v ->
-           if not (List.exists
-                     (function Cic.Meta (i, _) -> i = v | _ -> assert false)
-                     newargs) then
-             Hashtbl.replace table k first)
-        (Hashtbl.copy table)
-  in
-  let rec fix_proof = function
-   | NoProof -> NoProof 
-    | BasicProof term -> BasicProof (repl term)
-    | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
-        let subst' =
-          List.fold_left
-            (fun s arg ->
-               match arg with
-               | Cic.Meta (i, l) -> (
-                   try
-                     let j = Hashtbl.find table i in
-                     if List.mem_assoc i subst then
-                       s
-                     else
-                       let _, context, ty = CicUtil.lookup_meta i menv in
-                       (i, (context, Cic.Meta (j, l), ty))::s
-                   with Not_found | CicUtil.Meta_not_found _ ->
-                     s
-                 )
-               | _ -> assert false)
-            [] args
-        in
-        ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
-    | p -> assert false
-  in
-  let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
-  (newmeta +1, neweq)
-;;
-*)
-
-let relocate newmeta menv =
-  let subst, metasenv, newmeta = 
-    List.fold_right 
-      (fun (i, context, ty) (subst, menv, maxmeta) ->         
-       let irl = [] (*
-        CicMkImplicit.identity_relocation_list_for_metavariable context *)
-       in
-        let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty in
-        let newmeta = maxmeta, context, ty in
-        newsubst::subst, newmeta::menv, maxmeta+1) 
-      menv ([], [], newmeta+1)
-  in
-  let metasenv = apply_subst_metasenv subst metasenv in
-  let subst = flatten_subst subst in
-  subst, metasenv, newmeta
-
-
-let fix_metas newmeta (w, p, (ty, left, right, o), menv) =
-  (*
-  let metas = (metas_of_term left)@(metas_of_term right)
-    @(metas_of_term ty)@(metas_of_proof p) in
-  let menv = List.filter (fun (i, _, _) -> List.mem i metas) menv in
-  *)
-  (* debug 
-  let _ , eq = 
-    fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
-  prerr_endline (string_of_equality eq); *)
-  let subst, metasenv, newmeta = relocate newmeta menv in
-(*
-  if newmeta > 2839 then
-    begin
-      prerr_endline (CicPp.ppterm left ^ " = " ^ CicPp.ppterm right);
-      prerr_endline (CicMetaSubst.ppsubst subst);
-      prerr_endline (CicMetaSubst.ppmetasenv [] metasenv);
-      assert false;
-    end;
-*)
-  let ty = apply_subst subst ty in
-  let left = apply_subst subst left in
-  let right = apply_subst subst right in
-  let fix_proof = function
-    | NoProof -> NoProof 
-    | BasicProof (subst',term) -> BasicProof (subst@subst',term)
-    | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
-       (*
-       let newsubst = 
-          List.map
-           (fun (i, (context, term, ty)) ->
-              let context = apply_subst_context subst context in
-              let term = apply_subst subst term in
-              let ty = apply_subst subst ty in  
-                (i, (context, term, ty))) subst' in *)
-          ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
-    | p -> assert false
-  in
-  let p = fix_proof p in
-  (*
-  let metas = (metas_of_term left)@(metas_of_term right)
-    @(metas_of_term ty)@(metas_of_proof p) in
-  let metasenv = List.filter (fun (i, _, _) -> List.mem i metas) metasenv in
-  *)
-  let eq = (w, p, (ty, left, right, o), metasenv) in
-  (* debug prerr_endline (string_of_equality eq); *)
-  newmeta+1, eq  
-
-let term_is_equality term =
-  let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
-  match term with
-  | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
-  | _ -> false
-;;
-
-
-exception TermIsNotAnEquality;;
-
-let equality_of_term proof term =
-  let eq_uri = LibraryObjects.eq_URI () in
-  let iseq uri = UriManager.eq uri eq_uri in
-  match term with
-  | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
-      let o = !Utils.compare_terms t1 t2 in
-      let stat = (ty,t1,t2,o) in
-      let w = compute_equality_weight stat in
-      let e = (w, BasicProof ([],proof), stat, []) in
-      e
-  | _ ->
-      raise TermIsNotAnEquality
-;;
-
-
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
-
-let is_weak_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv) -> 
-       (left = right ||
-          (meta_convertibility left right)) 
-          (* the test below is not a good idea since it stops
-             demodulation too early *)
-           (* (fst (CicReduction.are_convertible 
-                 ~metasenv:(metasenv @ menv) context left right ugraph)))*)
-;;
-
-let is_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv) ->
-       (left = right ||
-          (* (meta_convertibility left right)) *)
-           (fst (CicReduction.are_convertible 
-                 ~metasenv:(metasenv @ menv) context left right ugraph)))
-;;
-
-
-let term_of_equality equality =
-  let _, _, (ty, left, right, _), menv = equality in
-  let eq i = function Cic.Meta (j, _) -> i = j | _ -> false in
-  let argsno = List.length menv in
-  let t =
-    CicSubstitution.lift argsno
-      (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
-  in
-  snd (
-    List.fold_right
-      (fun (i,_,ty) (n, t) ->
-         let name = Cic.Name ("X" ^ (string_of_int n)) in
-         let ty = CicSubstitution.lift (n-1) ty in
-         let t = 
-           ProofEngineReduction.replace
-             ~equality:eq ~what:[i]
-             ~with_what:[Cic.Rel (argsno - (n - 1))] ~where:t
-         in
-           (n-1, Cic.Prod (name, ty, t)))
-      menv (argsno, t))
-;;
index b08054ca4f2c90c72dc97ade2d53e493b8ed0260..08d1c8f266010354deb9c48dbcf86d9c16fc7c1d 100644 (file)
  * http://cs.unibo.it/helm/.
  *)
 
-val metas_of_proof_time : float ref
-
-(* type substitution = Cic.substitution *)
-type substitution = (int * Cic.term) list 
-
-type equality =
-    int *                (* weight *)
-    proof *              (* proof *)
-    (Cic.term *          (* type *)
-     Cic.term *          (* left side *)
-     Cic.term *          (* right side *)
-     Utils.comparison) * (* ordering *)  
-    Cic.metasenv        (* environment for metas *)
-
-and proof =
-  | NoProof   (* no proof *)
-  | BasicProof of substitution * Cic.term (* already a proof of a goal *)
-  | ProofBlock of (* proof of a rewrite step *)
-      substitution * UriManager.uri * (* eq_ind or eq_ind_r *)
-        (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
-  | ProofGoalBlock of proof * proof
-      (* proof of the new meta, proof of the goal from which this comes *)
-  | ProofSymBlock of Cic.term list * proof (* expl.named subst, proof *)
-  | SubProof of Cic.term * int * proof
-      (* parent proof, subgoal, proof of the subgoal *)
-
-type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
-
-(** builds the Cic.term encoded by proof *)
-val build_proof_term: ?noproof:Cic.term -> proof -> Cic.term
-
-val string_of_proof: proof -> string
-
-val filter : substitution -> Cic.metasenv -> Cic.metasenv
-
 exception MatchingFailure
 
 (** matching between two terms. Can raise MatchingFailure *)
 val matching:
-  Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> Cic.metasenv -> Cic.context -> 
+  Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  substitution * Cic.metasenv * CicUniv.universe_graph
+    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
 
 (**
    special unification that checks if the two terms are "simple", and in
    such case should be significantly faster than CicUnification.fo_unif
 *)
 val unification:
-  Cic.metasenv -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term ->
+  Cic.metasenv -> Cic.metasenv -> Cic.context -> 
+  Cic.term -> Cic.term ->
   CicUniv.universe_graph ->
-  substitution * Cic.metasenv * CicUniv.universe_graph
+    Equality.substitution * Cic.metasenv * CicUniv.universe_graph
 
     
 (**
@@ -83,64 +50,28 @@ val unification:
    fresh metas...
 *)
 val find_equalities:
-  Cic.context -> ProofEngineTypes.proof -> int list * equality list * int
+  Cic.context -> ProofEngineTypes.proof -> 
+    int list * Equality.equality list * int
 
 (**
    searches the library for equalities that can be applied to the current goal
 *)
 val find_library_equalities:
   HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
-  UriManager.UriSet.t * (UriManager.uri * equality) list * int
+    UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int
 
 (**
    searches the library for theorems that are not equalities (returned by the
    function above)
 *)
 val find_library_theorems:
-  HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t ->
-  (Cic.term * Cic.term * Cic.metasenv) list
+  HMysql.dbd -> Utils.environment -> ProofEngineTypes.status -> 
+  UriManager.UriSet.t ->
+    (Cic.term * Cic.term * Cic.metasenv) list
 
 (**
    searches the context for hypotheses that are not equalities
 *)
 val find_context_hypotheses:
-  environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
-
-
-exception TermIsNotAnEquality;;
-
-(**
-   raises TermIsNotAnEquality if term is not an equation.
-   The first Cic.term is a proof of the equation
-*)
-val equality_of_term: Cic.term -> Cic.term -> equality
-
-(**
-   Re-builds the term corresponding to this equality
-*)
-val term_of_equality: equality -> Cic.term
-
-val term_is_equality: Cic.term -> bool
-
-(** tests a sort of alpha-convertibility between the two terms, but on the
-    metavariables *)
-val meta_convertibility: Cic.term -> Cic.term -> bool
-
-(** meta convertibility between two equations *)
-val meta_convertibility_eq: equality -> equality -> bool
-
-val is_weak_identity: environment -> equality -> bool
-val is_identity: environment -> equality -> bool
-
-val string_of_equality: ?env:environment -> equality -> string
-
-
-val metas_of_term: Cic.term -> int list
-val metas_of_proof: proof -> int list
-
-(** ensures that metavariables in equality are unique *)
-val fix_metas: int -> equality -> int * equality
+  Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list
 
-val apply_subst: substitution -> Cic.term -> Cic.term
-val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
-val ppsubst: substitution -> string
index 5b5121e8677ea61a45642b6fd236302e9e4d6540..59b06ef2986e711d900a81d1588773b1df868d96 100644 (file)
@@ -70,16 +70,20 @@ let maxmeta = ref 0;;
 let maxdepth = ref 3;;
 let maxwidth = ref 3;;
 
+type new_proof = 
+  Equality.goal_proof * Equality.new_proof * Equality.substitution * Cic.metasenv
+type old_proof = Equality.old_proof * Cic.metasenv
 type result =
   | ParamodulationFailure
-  | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option
+  | ParamodulationSuccess of (new_proof * old_proof) option
 ;;
 
-type goal = proof * Cic.metasenv * Cic.term;;
+type goal = (Equality.goal_proof * Equality.old_proof) * Cic.metasenv * Cic.term;;
 
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
-let symbols_of_equality (_, _, (_, left, right, _), _) =
+let symbols_of_equality equality = 
+  let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in
   let m1 = symbols_of_term left in
   let m = 
     TermMap.fold
@@ -96,14 +100,14 @@ let symbols_of_equality (_, _, (_, left, right, _), _) =
 
 (* griggio *)
 module OrderedEquality = struct 
-  type t = Inference.equality
+  type t = Equality.equality
 
   let compare eq1 eq2 =
-    match meta_convertibility_eq eq1 eq2 with
+    match Equality.meta_convertibility_eq eq1 eq2 with
     | true -> 0
     | false ->
-        let w1, _, (ty, left, right, _), m1 = eq1
-        and w2, _, (ty', left', right', _), m2 = eq2 in
+        let w1, _, (ty,left, right, _), m1,_ = Equality.open_equality eq1 in
+        let w2, _, (ty',left', right', _), m2,_ = Equality.open_equality eq2 in
         match Pervasives.compare w1 w2 with
         | 0 -> 
             let res = (List.length m1) - (List.length m2) in 
@@ -142,7 +146,7 @@ let rec select env goals passive =
     match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false
   in
   let (pos_list, pos_set), passive_table = passive in
-  let remove eq l = List.filter (fun e -> e <> eq) l in
+  let remove eq l = List.filter (fun e -> Equality.compare e eq <> 0) l in
   if !weight_age_ratio > 0 then
     weight_age_counter := !weight_age_counter - 1;
   match !weight_age_counter with
@@ -192,7 +196,7 @@ let rec select env goals passive =
       let passive_table =
         Indexing.remove_index passive_table current
       in
-       current,
+        current,
       ((remove current pos_list, EqualitySet.remove current pos_set),
        passive_table))
   | _ ->
@@ -255,8 +259,6 @@ let prune_passive howmany (active, _) passive =
   and in_age = round (howmany /. (ratio +. 1.)) in 
   debug_print
     (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
-  let symbols, card = None, 0
-  in
   let counter = ref !symbols_ratio in
   let rec pickw w ps =
     if w > 0 then
@@ -264,7 +266,7 @@ let prune_passive howmany (active, _) passive =
         let _ =
           counter := !counter - 1;
           if !counter = 0 then counter := !symbols_ratio in
-       let e = EqualitySet.min_elt ps in
+        let e = EqualitySet.min_elt ps in
         let ps' = pickw (w-1) (EqualitySet.remove e ps) in
           EqualitySet.add e ps'
       else
@@ -300,7 +302,7 @@ let prune_passive howmany (active, _) passive =
 
 
 (** inference of new equalities between current and some in active *)
-let infer env current ((active_list:Inference.equality list), active_table) =
+let infer env current (active_list, active_table) =
   let (_,c,_) = env in 
   if Utils.debug_metas then
     (ignore(Indexing.check_target c current "infer1");
@@ -325,9 +327,9 @@ let infer env current ((active_list:Inference.equality list), active_table) =
                      (function current -> 
                         Indexing.check_target c current "sup2") res);
               let pos = infer_positive table tl in
-             res @ pos
+              res @ pos
       in
-      let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+      let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
         maxmeta := maxm;
       let curr_table = Indexing.index Indexing.empty current in
       let pos = infer_positive curr_table (copy_of_current::active_list) 
@@ -336,7 +338,7 @@ let infer env current ((active_list:Inference.equality list), active_table) =
         ignore(List.map 
                  (function current -> 
                     Indexing.check_target c current "sup3") pos);
-       res @ pos
+        res @ pos
   in
   derived_clauses := !derived_clauses + (List.length new_pos);
   match !maximal_retained_equality with
@@ -365,7 +367,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
     let newmeta, newcurrent =
       Indexing.demodulation_equality !maxmeta env table sign current in
     maxmeta := newmeta;
-    if is_identity env newcurrent then
+    if Equality.is_identity env newcurrent then
 (*         debug_print  *)
 (*           (lazy *)
 (*              (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
@@ -396,7 +398,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
             match demodulate passive_table newcurrent with
               | None -> None
               | Some newnewcurrent -> 
-                  if newcurrent <> newnewcurrent then 
+                  if Equality.compare newcurrent newnewcurrent <> 0 then 
                     demod newnewcurrent
                   else Some newnewcurrent
   in 
@@ -404,6 +406,7 @@ let forward_simplify env (sign,current) ?passive (active_list, active_table) =
   match res with
   | None -> None
   | Some c ->
+      (* immagino non funzioni piu'... *)
       if Indexing.in_index active_table c then
         None
       else
@@ -471,7 +474,7 @@ let forward_simplify_new env new_pos ?passive active =
   let new_pos_set =
     List.fold_left
       (fun s e ->
-         if not (Inference.is_identity env e) then
+         if not (Equality.is_identity env e) then
            if EqualitySet.mem e s then s
            else EqualitySet.add e s
          else s)
@@ -510,12 +513,11 @@ let rec simplify_goal env goal ?passive (active_list, active_table) =
     | None -> None
     | Some ((_, _), pt) -> Some pt
   in
-
   let demodulate table goal = 
-    let newmeta, newgoal =
+    let changed, newmeta, newgoal =
       Indexing.demodulation_goal !maxmeta env table goal in
     maxmeta := newmeta;
-    goal <> newgoal, newgoal
+    changed, newgoal
   in
   let changed, goal =
     match passive_table with
@@ -565,28 +567,28 @@ let backward_simplify_active env new_pos new_table min_weight active =
   let active_list, newa = 
     List.fold_right
       (fun equality (res, newn) ->
-         let ew, _, _, _ = equality in
+         let ew, _, _, _,_ = Equality.open_equality equality in
          if ew < min_weight then
            equality::res, newn
          else
            match forward_simplify env (Utils.Positive, equality) (new_pos, new_table) with
            | None -> res, newn
            | Some e ->
-               if equality = e then
+               if Equality.compare equality e = 0 then
                  e::res, newn
                else 
                  res, e::newn)
       active_list ([], [])
   in
   let find eq1 where =
-    List.exists (meta_convertibility_eq eq1) where
+    List.exists (Equality.meta_convertibility_eq eq1) where
   in
   let active, newa =
     List.fold_right
       (fun eq (res, tbl) ->
          if List.mem eq res then
            res, tbl
-         else if (is_identity env eq) || (find eq res) then (
+         else if (Equality.is_identity env eq) || (find eq res) then (
            res, tbl
          ) 
          else
@@ -594,8 +596,8 @@ let backward_simplify_active env new_pos new_table min_weight active =
       active_list ([], Indexing.empty),
     List.fold_right
       (fun eq p ->
-         if (is_identity env eq) then p
-        else eq::p)
+         if (Equality.is_identity env eq) then p
+         else eq::p)
       newa []
   in
   match newa with
@@ -608,7 +610,7 @@ let backward_simplify_active env new_pos new_table min_weight active =
 let backward_simplify_passive env new_pos new_table min_weight passive =
   let (pl, ps), passive_table = passive in
   let f sign equality (resl, ress, newn) =
-    let ew, _, _, _ = equality in
+    let ew, _, _, _ , _ = Equality.open_equality equality in
     if ew < min_weight then
       equality::resl, ress, newn
     else
@@ -636,7 +638,7 @@ let backward_simplify env new' ?passive active =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
-         let ew, _, _, _ = e in
+         let ew, _, _, _ , _ = Equality.open_equality e in
          e::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) new'
   in
@@ -658,7 +660,7 @@ let close env new' given =
   let new_pos, new_table, min_weight =
     List.fold_left
       (fun (l, t, w) e ->
-         let ew, _, _, _ = e in
+         let ew, _, _, _ , _ = Equality.open_equality e in
          e::l, Indexing.index t e, min ew w)
       ([], Indexing.empty, 1000000) (snd new')
   in
@@ -670,7 +672,9 @@ let close env new' given =
 ;;
 
 let is_commutative_law eq =
-  let w, proof, (eq_ty, left, right, order), metas = eq in
+  let w, proof, (eq_ty, left, right, order), metas , _ = 
+    Equality.open_equality eq 
+  in
     match left,right with
         Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1], 
         Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
@@ -686,7 +690,7 @@ let prova env new' active =
          (Printf.sprintf "symmetric:\n%s\n"
             (String.concat "\n"
                (List.map
-                  (fun e -> string_of_equality ~env e)
+                  (fun e -> Equality.string_of_equality ~env e)
                    given)))) in
     close env new' given
 ;;
@@ -794,7 +798,7 @@ let simplify_equalities env equalities =
     (lazy 
        (Printf.sprintf "equalities:\n%s\n"
           (String.concat "\n"
-             (List.map string_of_equality equalities))));
+             (List.map Equality.string_of_equality equalities))));
   debug_print (lazy "SIMPLYFYING EQUALITIES...");
   match equalities with
     | [] -> []
@@ -806,7 +810,7 @@ let simplify_equalities env equalities =
             (lazy
                (Printf.sprintf "equalities AFTER:\n%s\n"
                   (String.concat "\n"
-                     (List.map string_of_equality res))));
+                     (List.map Equality.string_of_equality res))));
           res
 ;;
 
@@ -822,28 +826,42 @@ let print_goals goals =
            Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals))
 ;;
 
-let check_if_goal_is_subsumed env (proof,menv,ty) table =
+let check_if_goal_is_subsumed env ((cicproof,proof),menv,ty) table =
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
-      (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in
-      match Indexing.subsumption env table goal_equation with
-      | Some (subst, (_,p,_,m)) ->
-          let p = Inference.apply_subst subst (Inference.build_proof_term p) in
-          let newp =
-            let rec repl = function
-              | Inference.ProofGoalBlock (_, gp) ->
-                  Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
-              | Inference.NoProof -> Inference.BasicProof ([],p)
-              | Inference.BasicProof _ -> Inference.BasicProof ([],p)
-              | Inference.SubProof (t, i, p2) ->
-                  Inference.SubProof (t, i, repl p2)
-              | _ -> assert false
-            in
-            repl proof
-          in
-          Some (newp,Inference.apply_subst_metasenv subst m @ menv)
-      | None -> None)
+      (let goal_equation = 
+         Equality.mk_equality
+           (0,(Equality.Exact (Cic.Rel (-1)),proof),(eq_ty,left,right,Eq),menv) 
+       in
+         match Indexing.subsumption env table goal_equation with
+           | Some (subst, equality ) ->
+               let (_,(np,p),(ty,l,r,_),m,id) = 
+                 Equality.open_equality equality in
+               let p = Equality.apply_subst subst 
+                 (Equality.build_proof_term_old p) in
+               let newp =
+                 let rec repl = function
+                   | Equality.ProofGoalBlock (_, gp) ->
+                       Equality.ProofGoalBlock 
+                         (Equality.BasicProof (Equality.empty_subst,p), gp)
+                   | Equality.NoProof -> 
+                       Equality.BasicProof (Equality.empty_subst,p)
+                   | Equality.BasicProof _ -> 
+                       Equality.BasicProof (Equality.empty_subst,p)
+                   | Equality.SubProof (t, i, p2) ->
+                       Equality.SubProof (t, i, repl p2)
+                   | _ -> assert false
+                 in
+                   repl proof
+               in
+               let newcicp,np,subst,cicmenv = 
+                 cicproof,np, subst, (m @ menv) 
+               in
+                 Some 
+                  ((newcicp,np,subst,cicmenv),
+                   (newp, Equality.apply_subst_metasenv subst m @ menv ))
+           | None -> None)
   | _ -> None
 ;;
 
@@ -883,22 +901,31 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
             in
             let newp =
               let rec repl = function
-                | Inference.ProofGoalBlock (_, gp) ->
-                    Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
-                | Inference.NoProof -> Inference.BasicProof ([],p)
-                | Inference.BasicProof _ -> Inference.BasicProof ([],p)
-                | Inference.SubProof (t, i, p2) ->
-                    Inference.SubProof (t, i, repl p2)
+                | Equality.ProofGoalBlock (_, gp) ->
+                    Equality.ProofGoalBlock 
+                      (Equality.BasicProof (Equality.empty_subst,p), gp)
+                | Equality.NoProof -> 
+
+                    Equality.BasicProof (Equality.empty_subst,p)
+                | Equality.BasicProof _ -> 
+                    Equality.BasicProof (Equality.empty_subst,p)
+                | Equality.SubProof (t, i, p2) ->
+                    Equality.SubProof (t, i, repl p2)
                 | _ -> assert false
               in
-              repl proof
-            in true, Some (newp,m)
+              repl (snd proof)
+            in 
+                 let reflproof = Equality.refl_proof eq_ty left in
+            true, 
+              Some ((fst proof,Equality.Exact reflproof,
+                     Equality.empty_subst,m),
+                    (newp,m))
         | (_, [proof,m,ty])::_ ->
             (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with
             | None -> false,None
-            | Some (newproof,m) ->
+            | Some p ->
                 prerr_endline "Proof found by subsumption!";
-                true, Some (newproof,m))
+                true, Some p)
         | _ -> false, None
     in 
     if ok then
@@ -940,7 +967,6 @@ let rec given_clause_fullred dbd env goals theorems ~passive active =
 and given_clause_fullred_aux dbd env goals theorems passive active =
   prerr_endline (string_of_int !counter ^ 
                  " MAXMETA: " ^ string_of_int !maxmeta ^ 
-                 " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
                  " #ACTIVES: " ^ string_of_int (size_of_active active) ^
                  " #PASSIVES: " ^ string_of_int (size_of_passive passive));
   incr counter;
@@ -1008,7 +1034,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
   | false ->
       let current, passive = select env (fst goals) passive in
       prerr_endline 
-        ("Selected = " ^ string_of_equality ~env current);
+        ("Selected = " ^ Equality.string_of_equality ~env current);
 (* ^ 
            (let w,p,(t,l,r,o),m = current in
            " size w: " ^ string_of_int (HExtlib.estimate_size w)^
@@ -1029,8 +1055,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
           (* weight_age_counter := !weight_age_counter + 1; *)
           given_clause_fullred dbd env goals theorems passive active
       | Some current ->
-          debug_print (lazy (Printf.sprintf "selected: %s"
-                               (string_of_equality ~env current)));
+          prerr_endline (Printf.sprintf "selected sipl: %s"
+                               (Equality.string_of_equality ~env current));
           let t1 = Unix.gettimeofday () in
           let new' = infer env current active in
           let _ =
@@ -1040,12 +1066,12 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                     (String.concat "\n"
                        (List.map
                           (fun e -> "Positive " ^
-                             (string_of_equality ~env e)) new'))))
+                             (Equality.string_of_equality ~env e)) new'))))
           in
           let t2 = Unix.gettimeofday () in
             infer_time := !infer_time +. (t2 -. t1);
             let active =
-              if is_identity env current then active
+              if Equality.is_identity env current then active
               else
                 let al, tbl = active in
                   al @ [current], Indexing.index tbl current
@@ -1065,14 +1091,13 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               | None, None -> active, passive, new'
               | Some p, None
               | None, Some p ->
-                  let np = new' in
-                    if Utils.debug_metas then
-                      begin
-                        List.iter 
-                          (fun x->Indexing.check_target context x "simplify1")
-                          p;
-                      end;
-                    simplify (new' @ p) active passive
+                  if Utils.debug_metas then
+                    begin
+                      List.iter 
+                        (fun x->Indexing.check_target context x "simplify1")
+                        p;
+                    end;
+                  simplify (new' @ p) active passive
               | Some p, Some rp ->
                   simplify (new' @ p @ rp) active passive
             in
@@ -1105,7 +1130,7 @@ end prova *)
                    (Printf.sprintf "active:\n%s\n"
                       (String.concat "\n"
                          ((List.map
-                             (fun e -> (string_of_equality ~env e))
+                             (fun e -> (Equality.string_of_equality ~env e))
                              (fst active))))))
             in
             let _ =
@@ -1115,7 +1140,7 @@ end prova *)
                       (String.concat "\n"
                          ((List.map
                              (fun e -> "Negative " ^
-                                (string_of_equality ~env e)) new')))))
+                                (Equality.string_of_equality ~env e)) new')))))
             in
             let passive = add_to_passive passive new' in
               given_clause_fullred dbd env goals theorems passive active
@@ -1142,10 +1167,10 @@ let rec saturate_equations env goal accept_fun passive active =
         saturate_equations env goal accept_fun passive active
     | Some current ->
         debug_print (lazy (Printf.sprintf "selected: %s"
-                             (string_of_equality ~env current)));
+                             (Equality.string_of_equality ~env current)));
         let new' = infer env current active in
         let active =
-          if is_identity env current then active
+          if Equality.is_identity env current then active
           else
             let al, tbl = active in
             al @ [current], Indexing.index tbl current
@@ -1167,24 +1192,25 @@ let rec saturate_equations env goal accept_fun passive active =
                (Printf.sprintf "active:\n%s\n"
                   (String.concat "\n"
                      (List.map
-                         (fun e -> string_of_equality ~env e)
+                         (fun e -> Equality.string_of_equality ~env e)
                          (fst active)))))
         in
-       let _ =
+        let _ =
           debug_print
             (lazy
                (Printf.sprintf "new':\n%s\n"
                   (String.concat "\n"
                      (List.map
                          (fun e -> "Negative " ^
-                            (string_of_equality ~env e)) new'))))
+                            (Equality.string_of_equality ~env e)) new'))))
         in
         let new' = List.filter accept_fun new' in
         let passive = add_to_passive passive new' in
         saturate_equations env goal accept_fun passive active
 ;;
   
-
+let main dbd full term metasenv ugraph = ()
+(*
 let main dbd full term metasenv ugraph =
   let module C = Cic in
   let module T = CicTypeChecker in
@@ -1246,7 +1272,9 @@ let main dbd full term metasenv ugraph =
                   (fst theorems)))))
   in
   (*try*)
-    let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
+    let goal = 
+      ([],Equality.BasicProof (Equality.empty_subst ,new_meta_goal)), [], goal 
+    in
     let equalities = simplify_equalities env 
       (equalities@library_equalities) in 
     let active = make_active () in
@@ -1258,7 +1286,7 @@ let main dbd full term metasenv ugraph =
     Printf.printf "\nequalities:\n%s\n"
       (String.concat "\n"
          (List.map
-            (string_of_equality ~env) equalities));
+            (Equality.string_of_equality ~env) equalities));
 (*             (equalities @ library_equalities))); *)
       print_endline "--------------------------------------------------";
       let start = Unix.gettimeofday () in
@@ -1274,17 +1302,27 @@ let main dbd full term metasenv ugraph =
         match res with
         | ParamodulationFailure ->
             Printf.printf "NO proof found! :-(\n\n"
-        | ParamodulationSuccess (Some (proof, env)) ->
-            let proof = Inference.build_proof_term proof in
+        | ParamodulationSuccess (Some ((cicproof,cicmenv),(proof, env))) ->
             Printf.printf "OK, found a proof!\n";
+            let oldproof = Equation.build_proof_term proof in
+            let newproof,_,newenv,_ = 
+                CicRefine.type_of_aux' 
+                  cicmenv context cicproof CicUniv.empty_ugraph
+            in
             (* REMEMBER: we have to instantiate meta_proof, we should use
                apply  the "apply" tactic to proof and status 
             *)
             let names = names_of_context context in
+            prerr_endline "OLD PROOF";
             print_endline (PP.pp proof names);
+            prerr_endline "NEW PROOF";
+            print_endline (PP.pp newproof names);
             let newmetasenv =
               List.fold_left
-                (fun m (_, _, _, menv) -> m @ menv) metasenv equalities
+                (fun m eq -> 
+                  let (_, _, _, menv,_) = Equality.open_equality eq in 
+                  m @ menv) 
+              metasenv equalities
             in
             let _ =
               (*try*)
@@ -1316,8 +1354,6 @@ let main dbd full term metasenv ugraph =
                        "backward_simpl_time: %.9f\n")
               !infer_time !forward_simpl_time !forward_simpl_new_time
               !backward_simpl_time) ^
-              (Printf.sprintf "beta_expand_time: %.9f\n"
-                 !Indexing.beta_expand_time) ^
               (Printf.sprintf "passive_maintainance_time: %.9f\n"
                  !passive_maintainance_time) ^
               (Printf.sprintf "    successful unification/matching time: %.9f\n"
@@ -1337,14 +1373,13 @@ let main dbd full term metasenv ugraph =
     raise exc
 *)
 ;;
-
+*)
 
 let default_depth = !maxdepth
 and default_width = !maxwidth;;
 
 let reset_refs () =
   maxmeta := 0;
-  Indexing.local_max := 100;
   symbols_counter := 0;
   weight_age_counter := !weight_age_ratio;
   processed_clauses := 0;
@@ -1358,10 +1393,50 @@ let reset_refs () =
   passive_maintainance_time := 0.;
   derived_clauses := 0;
   kept_clauses := 0;
-  Indexing.beta_expand_time := 0.;
-  Inference.metas_of_proof_time := 0.;
+  Equality.reset ();
+;;
+
+let interactive_comparison context t1 t2 =
+  let rc = ref [] in
+  let module P = Printf in
+  let rec aux n context t1 t2 =
+(*    let names = names_of_context context in*)
+    let pp t1 t2 = () (*
+      P.eprintf "%s%s === %s\n" (String.make n ' ') 
+      (CicPp.pp t1 names) (CicPp.pp t2 names) *)
+    in
+    match t1,t2 with
+    | _, Cic.Appl [Cic.Const(uri,_);t2] when 
+      UriManager.eq uri (UriManager.uri_of_string
+      "cic:/Coq/Init/Logic/sym_eq.con")-> aux n context t1 t2
+    | Cic.Implicit _, _ -> pp t1 t2
+    | Cic.Meta (n,_), _ -> 
+        rc := (n,t2,context) :: !rc;
+        pp (Cic.Meta(n,[])) t2
+    | Cic.Rel n1, Cic.Rel n2 when n1 = n2 -> pp t1 t2
+    | Cic.Appl l1,Cic.Appl l2 -> 
+        if List.length l1 <> List.length l2 then
+          begin
+            prerr_endline "ERROR: application with diff num of args";
+            pp t1 t2
+          end
+        else
+          List.iter2 (aux (n+1) context) l1 l2
+    | Cic.Lambda (name,s,t1),Cic.Lambda(_,_,t2) ->
+        let context = (Some (name,(Cic.Decl s)))::context in
+        aux (n+1) context t1 t2
+    | Cic.Const (u1,_), Cic.Const (u2,_) when UriManager.eq u1 u2 -> 
+        pp t1 t2
+    | _,_ -> pp t1 t2
+  in
+  aux 0 context t1 t2;
+  List.iter (fun (n,t,ctx) -> 
+    let names = names_of_context ctx in 
+    Printf.eprintf "%d := %s\n" n (CicPp.pp t  names)) 
+    (HExtlib.list_uniq (List.sort (fun (x,_,_) (y,_,_) -> x-y) !rc))
 ;;
 
+
 let saturate 
     dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) status = 
   let module C = Cic in
@@ -1375,7 +1450,6 @@ let saturate
   let goal' = goal in
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
-  prerr_endline ("CTX: " ^ string_of_int (HExtlib.estimate_size context));
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let new_meta_goal, metasenv, type_of_goal =
     let irl =
@@ -1389,7 +1463,9 @@ let saturate
   in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
+  let goal = 
+    ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal 
+  in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
@@ -1445,20 +1521,31 @@ let saturate
     (res, finish -. start)
   in
   match res with
-  | ParamodulationSuccess (Some (proof, proof_menv)) ->
+  | ParamodulationSuccess 
+    (Some ((goalproof,newproof,subsumption_subst, newproof_menv),(proof, proof_menv))) ->
       prerr_endline "OK, found a proof!";
-      debug_print (lazy "OK, found a proof!");
-      let proof = Inference.build_proof_term proof in
+      prerr_endline (Equality.string_of_proof_old proof);
+      
+      let cic_proof = Equality.build_proof_term_old proof in
+      
+      let cic_proof_new,cic_proof_new_menv = 
+        Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof) 
+      in
+      let newproof_menv = 
+        Equality.apply_subst_metasenv subsumption_subst 
+          (newproof_menv @ cic_proof_new_menv)
+      in
+      let cic_proof_new = Equality.apply_subst subsumption_subst cic_proof_new in
+      
       let equality_for_replace i t1 =
         match t1 with
         | C.Meta (n, _) -> n = i
         | _ -> false
       in
-      prerr_endline "replacing metas";
+      let mkirl = CicMkImplicit.identity_relocation_list_for_metavariable in
+      prerr_endline "replacing metas (old)";
       let proof_menv, what, with_what = 
-        let irl = 
-          CicMkImplicit.identity_relocation_list_for_metavariable context
-        in
+        let irl = mkirl context in
         List.fold_left 
           (fun (acc1,acc2,acc3) (i,_,ty) -> 
             (i,context,ty)::acc1, 
@@ -1466,13 +1553,35 @@ let saturate
             (Cic.Meta(i,irl)) ::acc3) 
           ([],[],[]) proof_menv 
       in
-      let proof = ProofEngineReduction.replace_lifting
+      let cic_proof = ProofEngineReduction.replace_lifting
+              ~equality:(=)
+              ~what ~with_what
+              ~where:cic_proof
+      in
+      prerr_endline "replacing metas (new)";
+      let newproof_menv, what, with_what = 
+        let irl = mkirl context in
+        List.fold_left 
+          (fun (acc1,acc2,acc3) (i,_,ty) -> 
+            (i,context,ty)::acc1, 
+            (Cic.Meta(i,[]))::acc2, 
+            (Cic.Meta(i,irl)) ::acc3) 
+          ([],[],[]) newproof_menv 
+      in
+      let cic_proof_new = ProofEngineReduction.replace_lifting
               ~equality:(=)
               ~what ~with_what
-              ~where:proof
+              ~where:cic_proof_new
       in
-      (* prerr_endline (CicPp.ppterm proof); *)
       let names = names_of_context context in
+      prerr_endline "OLDPROOF";
+      prerr_endline (Equality.string_of_proof_old proof);
+      prerr_endline "OLDPROOFCIC";
+      prerr_endline (CicPp.pp cic_proof names); 
+      prerr_endline "NEWPROOF";
+      prerr_endline (Equality.string_of_proof_new ~names newproof goalproof); 
+      prerr_endline "NEWPROOFCIC";
+      prerr_endline (CicPp.pp cic_proof_new names); 
       let newmetasenv =
         let i1 =
           match new_meta_goal with
@@ -1481,13 +1590,70 @@ let saturate
         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
       in
       let newmetasenv = newmetasenv@proof_menv in
+      let newmetasenv_new = newmetasenv@newproof_menv in
       let newstatus =
         try
-          let ty, ug =
-            prerr_endline "type checking ... ";
-            CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+          let cic_proof,newmetasenv,proof_menv,ty, ug =
+            prerr_endline "type checking ... (old) ";
+(*            let old_ty, oldug = *)
+(*              CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *)
+(*            in*)
+            let cic_proof_new,new_ty,newmetasenv_new,newug = 
+              try
+                (*
+                 prerr_endline "refining ... (new) ";
+                 CicRefine.type_of_aux' 
+                  newmetasenv_new context cic_proof_new ugraph*)
+                let ty,ug = 
+                  prerr_endline "typechecking ... (new) ";
+                  CicTypeChecker.type_of_aux' 
+                    newmetasenv_new context cic_proof_new ugraph
+                in
+                cic_proof_new, ty, newmetasenv_new, ug
+              with
+              | CicTypeChecker.TypeCheckerFailure s ->
+                  prerr_endline "FAILURE IN TYPECHECKING";
+                  prerr_endline (Lazy.force s);
+                  assert false
+              | CicRefine.RefineFailure s 
+              | CicRefine.Uncertain s 
+              | CicRefine.AssertFailure s -> 
+                  prerr_endline "FAILURE IN REFINE";
+                  prerr_endline (Lazy.force s);
+                  interactive_comparison context cic_proof_new cic_proof;
+                  assert false
+            in
+(*
+            prerr_endline "check unif ... (old vs new) ";
+            (try 
+              ignore(CicUnification.fo_unif 
+                newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph)
+            with CicUnification.UnificationFailure _ -> 
+              prerr_endline "WARNING, new and old proofs are not unifiable");
+            prerr_endline "unif ... (new) ";
+            let subst, newmetasenv_new, newug = 
+              CicUnification.fo_unif 
+                newmetasenv_new context new_ty type_of_goal newug
+            in
+            if subst <> [] then
+              prerr_endline "UNIF SERVE ################################";
+*)
+            let subst = [] in 
+            if List.length newmetasenv_new <> 0 then
+              prerr_endline 
+                ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv
+                 [] newmetasenv_new);
+            (CicMetaSubst.apply_subst subst cic_proof_new),
+            newmetasenv_new,
+            (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new),
+            (CicMetaSubst.apply_subst subst new_ty),
+            newug
+(*            cic_proof,newmetasenv,proof_menv,oldty,oldug*)
           in
-          prerr_endline (CicPp.pp proof [](* names *));
+          prerr_endline "FINAL PROOF";
+          prerr_endline (CicPp.pp cic_proof names);
+          prerr_endline "ENDOFPROOFS";
+            
           debug_print
             (lazy
                (Printf.sprintf
@@ -1499,7 +1665,7 @@ let saturate
           let real_proof =
             ProofEngineReduction.replace
               ~equality:equality_for_replace
-              ~what:[goal'] ~with_what:[proof]
+              ~what:[goal'] ~with_what:[cic_proof]
               ~where:meta_proof
           in
           debug_print
@@ -1514,7 +1680,7 @@ let saturate
             List.map (fun (i,_,_) -> i) proof_menv)
         with CicTypeChecker.TypeCheckerFailure _ ->
           debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
-          debug_print (lazy (CicPp.pp proof names));
+          debug_print (lazy (CicPp.pp cic_proof names));
           raise (ProofEngineTypes.Fail
                   (lazy "Found a proof, but it doesn't typecheck"))
       in
@@ -1529,10 +1695,6 @@ let saturate
               (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
               (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
               (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
-              (Printf.sprintf "\nbeta_expand_time: %.9f\n"
-                 !Indexing.beta_expand_time) ^
-              (Printf.sprintf "\nmetas_of_proof: %.9f\n"
-                 !Inference.metas_of_proof_time) ^
               (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
               (Printf.sprintf "\nforward_simpl_new_times: %.9f" 
                  !forward_simpl_new_time) ^
@@ -1629,7 +1791,7 @@ let retrieve_and_print dbd term metasenv ugraph =
                           (fun (u, e) ->
                              Printf.sprintf "%s: %s"
                                (UriManager.string_of_uri u)
-                               (string_of_equality e)
+                               (Equality.string_of_equality e)
                           )
                           res))));
             res in
@@ -1669,7 +1831,9 @@ let main_demod_equalities dbd term metasenv ugraph =
   in
   let env = (metasenv, context, ugraph) in
   (*try*)
-    let goal = Inference.BasicProof ([],new_meta_goal), [], goal in
+    let goal = 
+      ([],Equality.BasicProof (Equality.empty_subst,new_meta_goal)), [], goal 
+    in
     let equalities = simplify_equalities env (equalities@library_equalities) in
     let active = make_active () in
     let passive = make_passive equalities in
@@ -1678,7 +1842,7 @@ let main_demod_equalities dbd term metasenv ugraph =
     Printf.printf "\nequalities:\n%s\n"
       (String.concat "\n"
          (List.map
-            (string_of_equality ~env) equalities));
+            (Equality.string_of_equality ~env) equalities));
     print_endline "--------------------------------------------------";
     print_endline "GO!";
     start_time := Unix.gettimeofday ();
@@ -1705,12 +1869,12 @@ let main_demod_equalities dbd term metasenv ugraph =
       EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
     in
     Printf.printf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
-       (String.concat "\n" (List.map (string_of_equality ~env) active)) 
+       (String.concat "\n" (List.map (Equality.string_of_equality ~env) active)) 
      (*  (String.concat "\n"
          (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
 (*       (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
       (String.concat "\n"
-         (List.map (fun e -> CicPp.ppterm (term_of_equality e)) passive));
+         (List.map (fun e -> CicPp.ppterm (Equality.term_of_equality e)) passive));
     print_newline ();
 (*
   with e ->
@@ -1729,7 +1893,9 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let library_equalities = List.map snd library_equalities in
   let goalterm = Cic.Meta (metano,irl) in
-  let initgoal = Inference.BasicProof ([],goalterm), [], ty in
+  let initgoal = 
+    ([],Equality.BasicProof (Equality.empty_subst,goalterm)), [], ty 
+  in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
   let equalities = simplify_equalities env (equalities@library_equalities) in   
   let table = 
@@ -1737,14 +1903,15 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
       (fun tbl eq -> Indexing.index tbl eq) 
       Indexing.empty equalities 
   in
-  let newmeta,(newproof,newmetasenv, newty) = Indexing.demodulation_goal 
-    maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal 
+  let _, newmeta,(newproof,newmetasenv, newty) = 
+    Indexing.demodulation_goal 
+      maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal 
   in
   if newmeta != maxm then
     begin
       let opengoal = Cic.Meta(maxm,irl) in
       let proofterm = 
-        Inference.build_proof_term ~noproof:opengoal newproof in
+        Equality.build_proof_term_old ~noproof:opengoal (snd newproof) in
         let extended_metasenv = (maxm,context,newty)::metasenv in
         let extended_status = 
           (curi,extended_metasenv,pbo,pty),goal in
index db19e87d1d89f77f67ed818df82b625e323da12e..18ccd5f79b52c0fe471de74101b57698323868f5 100644 (file)
@@ -60,6 +60,8 @@ let string_of_comparison = function
   | Eq -> "="
   | Incomparable -> "I"
 
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
 module OrderedTerm =
 struct
   type t = Cic.term
@@ -291,7 +293,7 @@ end
 module IntSet = Set.Make(OrderedInt)
 
 let compute_equality_weight (ty,left,right,o) =
-  let factor = 1 in
+  let factor = 2 in
   match o with
     | Lt -> 
        let w, m = (weight_of_term 
@@ -731,3 +733,30 @@ let eq_XURI () =
   let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
   UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
 let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
+
+let rec metas_of_term = function
+  | Cic.Meta (i, c) -> [i]
+  | Cic.Var (_, ens) 
+  | Cic.Const (_, ens) 
+  | Cic.MutInd (_, _, ens) 
+  | Cic.MutConstruct (_, _, _, ens) ->
+      List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+  | Cic.Cast (s, t)
+  | Cic.Prod (_, s, t)
+  | Cic.Lambda (_, s, t)
+  | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+  | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+  | Cic.MutCase (uri, i, s, t, l) ->
+      (metas_of_term s) @ (metas_of_term t) @
+        (List.flatten (List.map metas_of_term l))
+  | Cic.Fix (i, il) ->
+      List.flatten
+        (List.map (fun (s, i, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | Cic.CoFix (i, il) ->
+      List.flatten
+        (List.map (fun (s, t1, t2) ->
+                     (metas_of_term t1) @ (metas_of_term t2)) il)
+  | _ -> []
+;;      
+
index bef03b1415538e577a197d1843c509a8d1f23be9..f44cab460ee5837043e07cfc29eb23a5f7d5fbe7 100644 (file)
@@ -34,6 +34,8 @@ type weight = int * (int * int) list;;
 
 type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
 
+type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph
+
 val print_metasenv: Cic.metasenv -> string
 
 val print_subst: ?prefix:string -> Cic.substitution -> string
@@ -90,3 +92,6 @@ val eq_ind_r_URI: unit -> UriManager.uri
 val sym_eq_URI: unit -> UriManager.uri
 val eq_XURI: unit -> UriManager.uri
 val trans_eq_URI: unit -> UriManager.uri
+
+val metas_of_term: Cic.term -> int list
+