X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=a3894fd84cdbfa374ecc3e570ac8bbbb2fad57df;hb=430fb6e217b6ca61bfc38bb970c1bc57d5643b4c;hp=07d95ef866aa0ba5c88e6d94e3b8bbebcaafa52c;hpb=a7a7011cb7cf84e46d63651fa3a016f97533463b;p=helm.git

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 07d95ef86..a3894fd84 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -26,9 +26,135 @@
 (* $Id$ *)
 
 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 *)
@@ -37,14 +163,13 @@ type equality =
      Cic.term *          (* left side *)
      Cic.term *          (* right side *)
      Utils.comparison) * (* ordering *)  
-    Cic.metasenv *       (* environment for metas *)
-    Cic.term list        (* arguments *)
+    Cic.metasenv        (* environment for metas *)
 
 and proof =
   | NoProof (* term is the goal missing a proof *)
-  | BasicProof of Cic.term
+  | BasicProof of substitution * Cic.term
   | ProofBlock of
-      Cic.substitution * UriManager.uri *
+      substitution * UriManager.uri *
         (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
   | ProofGoalBlock of proof * proof 
   | ProofSymBlock of Cic.term list * proof
@@ -55,14 +180,14 @@ let string_of_equality ?env =
   match env with
   | None -> (
       function
-        | w, _, (ty, left, right, o), _, _ ->
+        | 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), _, _ ->
+        | 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)
@@ -72,13 +197,14 @@ let string_of_equality ?env =
 
 let rec string_of_proof = function
   | NoProof -> "NoProof " 
-  | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+  | 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" ^ (CicMetaSubst.ppsubst subst)
+      "ProofBlock" ^ (ppsubst subst)
   | ProofGoalBlock (p1, p2) ->
       Printf.sprintf "ProofGoalBlock(%s, %s)"
         (string_of_proof p1) (string_of_proof p2)
@@ -128,7 +254,7 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
     | NoProof ->
         Printf.fprintf stderr "WARNING: no proof!\n";
         noproof
-    | BasicProof term -> term
+    | BasicProof (s,term) -> apply_subst s term
     | ProofGoalBlock (proofbit, proof) ->
         print_endline "found ProofGoalBlock, going up...";
         do_build_goal_proof proofbit proof
@@ -139,15 +265,15 @@ let build_proof_term ?(noproof=Cic.Implicit None) 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
+          let _, proof', _, _ = eq in
           do_build_proof proof'
         in
         let eqproof = do_build_proof eqproof in
-        let _, _, (ty, what, other, _), menv', args' = eq in
+        let _, _, (ty, what, other, _), menv' = eq in
         let what, other =
           if pos = Utils.Left then what, other else other, what
         in
-        CicMetaSubst.apply_subst subst
+        apply_subst subst
           (Cic.Appl [Cic.Const (eq_URI, []); ty;
                      what; t'; eqproof; other; proof'])
     | SubProof (term, meta_index, proof) ->
@@ -177,10 +303,9 @@ let build_proof_term ?(noproof=Cic.Implicit None) proof =
         SubProof (term, meta_index, replace_proof newproof p)
     | p -> p
   in
-  do_build_proof proof
+  do_build_proof proof 
 ;;
 
-
 let rec metas_of_term = function
   | Cic.Meta (i, c) -> [i]
   | Cic.Var (_, ens) 
@@ -218,6 +343,7 @@ let rec metas_of_proof p =
     metas_of_term (build_proof_term p)
 ;;
 
+
 exception NotMetaConvertible;;
 
 let meta_convertibility_aux table t1 t2 =
@@ -311,8 +437,8 @@ let meta_convertibility_aux table t1 t2 =
 
 
 let meta_convertibility_eq eq1 eq2 =
-  let _, _, (ty, left, right, _), _, _ = eq1
-  and _, _, (ty', left', right', _), _, _ = eq2 in
+  let _, _, (ty, left, right, _), _ = eq1
+  and _, _, (ty', left', right', _), _ = eq2 in
   if ty <> ty' then
     false
   else if (left = left') && (right = right') then
@@ -366,18 +492,12 @@ let rec is_simple_term = function
   | _ -> false
 ;;
 
-
-let lookup_subst meta subst =
-  match meta with
-  | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
-      with Not_found -> meta
-    )
-  | _ -> assert false
+let locked menv i =
+  List.exists (fun (j,_,_) -> i = j) menv
 ;;
 
-
-let unification_simple metasenv context t1 t2 ugraph =
+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
@@ -394,28 +514,38 @@ let unification_simple metasenv context t1 t2 ugraph =
   let rec unif subst menv s t =
     let s = match s with C.Meta _ -> lookup s subst | _ -> s
     and t = match t with C.Meta _ -> lookup t subst | _ -> t
+    
     in
     match s, t with
     | s, t when s = t -> subst, menv
-    | C.Meta (i, _), C.Meta (j, _) when i > j ->
+    | C.Meta (i, _), C.Meta (j, _) 
+	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 (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
+          (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 = (i, (context, t, ty))::subst in
+	  let subst = (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 ->
           let names = names_of_context context in
-          debug_print
-            (lazy
+          (*debug_print
+            (lazy*) prerr_endline 
                (Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
                   (CicPp.pp t1 names) (CicPp.pp t2 names)
-                  (print_metasenv menv) (print_metasenv metasenv)));
+                  (print_metasenv menv) (print_metasenv metasenv));
           assert false
       )
     | _, C.Meta _ -> unif subst menv t s
@@ -437,224 +567,64 @@ let unification_simple metasenv context t1 t2 ugraph =
   List.rev subst, menv, ugraph
 ;;
 
+let profiler = HExtlib.profile "P/Inference.unif_simple[flatten]"
+let profiler2 = HExtlib.profile "P/Inference.unif_simple[flatten_fast]"
+let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
+let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
-let unification metasenv1 metasenv2 context t1 t2 ugraph =
-  let metasenv = metasenv1 metasenv2 in
+let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
+  let metasenv = metasenv1 @ metasenv2 in
   let subst, menv, ug =
     if not (is_simple_term t1) || not (is_simple_term t2) then (
       debug_print
         (lazy
            (Printf.sprintf "NOT SIMPLE TERMS: %s %s"
               (CicPp.ppterm t1) (CicPp.ppterm t2)));
-      CicUnification.fo_unif metasenv context t1 t2 ugraph
+      raise (CicUnification .UnificationFailure (lazy "Inference.unification.unif"))
     ) else
-      unification_simple metasenv context t1 t2 ugraph
+      if b then
+	(* full unification *)
+	unification_simple [] metasenv context t1 t2 ugraph
+      else
+	(* 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");
-  let subst =
+  (* let flatten subst = 
     List.map
       (fun (i, (context, term, ty)) ->
-	 let context = CicMetaSubst.apply_subst_context subst context in
-	 let term = CicMetaSubst.apply_subst subst term in
-	 let ty = CicMetaSubst.apply_subst subst ty in  
-	   (i, (context, term, ty))) subst in
-(*
-  let rec fix_term = function
-    | (Cic.Meta (i, l) as t) ->
-        let t' = lookup_subst t subst in
-        if t <> t' then fix_term t' else t
-    | Cic.Appl l -> Cic.Appl (List.map fix_term l)
-    | t -> t
+	 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 rec fix_subst = function
-    | [] -> []
-    | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
-  in 
-  fix_subst subst, menv, ug *)
-  subst, menv, ug
-;;
-
-
-let unification metasenv1 metasenv2 context t1 t2 ugraph = 
-  let (subst, metasenv, ugraph) = 
-    CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
-  if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "fo_unif");
-  (subst, metasenv, ugraph)
-    
+  let flatten subst = profiler.HExtlib.profile flatten subst in
+  let subst = flatten subst in *)
+    subst, menv, ug
 ;;
 
 exception MatchingFailure;;
 
-
-(*
-let matching_simple metasenv context t1 t2 ugraph =
-  let module C = Cic in
-  let module M = CicMetaSubst in
-  let module U = CicUnification in
-  let lookup meta subst =
-    match meta with
-    | C.Meta (i, _) -> (
-        try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
-        with Not_found -> meta
-      )
-    | _ -> assert false
-  in
-  let rec do_match subst menv s t =
-    match s, t with
-    | s, t when s = t -> subst, menv
-    | s, C.Meta (i, l) ->
-        let filter_menv i menv =
-          List.filter (fun (m, _, _) -> i <> m) menv
-        in
-        let subst, menv =
-          let value = lookup t subst in
-          match value with
-          | value when value = t ->
-              let _, _, ty = CicUtil.lookup_meta i menv in
-              (i, (context, s, ty))::subst, filter_menv i menv
-          | value when value <> s ->
-              raise MatchingFailure
-          | value -> do_match subst menv s value
-        in
-        subst, menv
-    | C.Appl ls, C.Appl lt -> (
-        try
-          List.fold_left2
-            (fun (subst, menv) s t -> do_match subst menv s t)
-            (subst, menv) ls lt
-        with Invalid_argument _ ->
-          raise MatchingFailure
-      )
-    | _, _ ->
-        raise MatchingFailure
-  in
-  let subst, menv = do_match [] metasenv t1 t2 in
-  subst, menv, ugraph
+let matching1 metasenv1 metasenv2 context t1 t2 ugraph = 
+  try 
+    unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
+  with
+    CicUnification .UnificationFailure _ ->
+      raise MatchingFailure
 ;;
-*)
 
-(*
-let matching metasenv context t1 t2 ugraph =
-    try
-      let subst, metasenv, ugraph =
-	try
-          unification metasenv context t1 t2 ugraph
-	with CicUtil.Meta_not_found _ as exn ->
-	  Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
-	    (CicPp.ppterm t1) (CicPp.ppterm t2) 
-	    (CicMetaSubst.ppmetasenv [] metasenv);
-	  raise exn
-      in
-      if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-2");
-      let t' = CicMetaSubst.apply_subst subst t1 in
-      if not (meta_convertibility t1 t') then
-        raise MatchingFailure
-      else
-        if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-1");
-        let metas = metas_of_term t1 in
-        let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-          if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua0");
-	  
-	  let subst, metasenv =
-	  List.fold_left
-	    (fun 
-	       (subst,metasenv) s ->
-		 match s with
-		   | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-		       let metasenv' =
-			 List.filter (fun (x, _, _) -> x<>j) metasenv 
-		       in
-			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
-			  (i,c,ty)::metasenv')
-		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in
-	if Utils.debug_res then
-	  ignore(check_disjoint_invariant subst metasenv "qua1");
-(*
-        let fix_subst = function
-          | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
-              (j, (c, Cic.Meta (i, lc), ty))
-          | s -> s
-        in
-        let subst = List.map fix_subst subst in *)
-	if CicMetaSubst.apply_subst subst t1 = t1 then
-          subst, metasenv, ugraph
-	else
-	  (prerr_endline "mah"; raise MatchingFailure)
-    with
-    | CicUnification.UnificationFailure _
-    | CicUnification.Uncertain _ ->
-      raise MatchingFailure
+let unification = unification_aux true 
 ;;
-*)
 
 (** matching takes in input the _disjoint_ metasenv of t1 and  t2;
 it perform unification in the union metasenv, then check that
 the first metasenv has not changed *)
 
-let matching metasenv1 metasenv2 context t1 t2 ugraph =
-      let subst, metasenv, ugraph =
-	try
-          unification metasenv1 metasenv2 context t1 t2 ugraph
-	with 
-	    CicUtil.Meta_not_found _ as exn ->
-	      Printf.eprintf "t1 == %s\nt2 = %s\nmetasenv == %s\n%!"
-		(CicPp.ppterm t1) (CicPp.ppterm t2) 
-		(CicMetaSubst.ppmetasenv [] (metasenv1@metasenv2));
-	      raise exn
-	  | CicUnification.UnificationFailure _
-	  | CicUnification.Uncertain _ ->
-	      raise MatchingFailure    
-      in
-      if Utils.debug_res then
-	    ignore(check_disjoint_invariant subst metasenv "qua-2");
-      (* let us unfold subst *)
-      if metasenv = metasenv1 then 
-	subst, metasenv, ugraph (* everything is fine *)
-      else
-	(* let us unfold subst *)
-	let subst =
-	  List.map
-	    (fun (i, (context, term, ty)) ->
-	       let context = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
-		 (i, (context, term, ty))) subst in
-	  (* let us revert Meta-Meta in subst privileging metasenv1 *)
-	let subst, metasenv =
-	  List.fold_left
-	    (fun 
-	       (subst,metasenv) s ->
-		 match s with
-		   | (i, (c, Cic.Meta (j, lc), ty)) 
-		       when (List.exists (fun (x, _, _)  -> x=i) metasenv1) &&
-			 not (List.exists (fun (x, _)  -> x=j) subst) ->
-		       let metasenv' =
-			 List.filter (fun (x, _, _) -> x<>j) metasenv 
-		       in
-			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
-			  (i,c,ty)::metasenv')
-		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in
-	(* finally, let us chek again that metasenv = metasenv1 *)
-	if metasenv = metasenv1 then 
-	  subst, metasenv, ugraph
-	else raise MatchingFailure  
-;;
+let matching = matching1;;
 
 let check_eq context msg eq =
-  let w, proof, (eq_ty, left, right, order), metas, args = eq in
+  let w, proof, (eq_ty, left, right, order), metas = eq in
   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
    (fst (CicTypeChecker.type_of_aux' metas context  left CicUniv.empty_ugraph))
    CicUniv.empty_ugraph))
@@ -700,8 +670,8 @@ 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, args) in
+                    let proof = BasicProof ([],p) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -713,7 +683,7 @@ 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 e = (w, BasicProof ([],(C.Rel index)), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -821,7 +791,7 @@ let find_library_equalities dbd context status maxmeta =
     | C.LetIn (_, s, t) | C.Cast (s, t) ->
         (has_vars s) || (has_vars t)
     | _ -> false
-  in
+ in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (uri, term, termty)::tl ->
@@ -850,8 +820,8 @@ 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 proof = BasicProof p in
-                    let e = (w, proof, stat, newmetas, args) in
+                    let proof = BasicProof ([],p) in
+                    let e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -860,7 +830,7 @@ 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 e = (w, BasicProof ([],term), stat, []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -947,7 +917,7 @@ 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
 
@@ -1013,7 +983,7 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
         (Hashtbl.copy table)
   in
   let rec fix_proof = function
-    | NoProof -> NoProof 
+   | NoProof -> NoProof 
     | BasicProof term -> BasicProof (repl term)
     | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) ->
         let subst' =
@@ -1040,30 +1010,26 @@ let fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) =
   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 = (i, (context, (Cic.Meta (maxmeta, irl)), ty)) in
+      (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 = CicMetaSubst.apply_subst_metasenv subst metasenv in
-  let subst =
-    List.map
-      (fun (i, (context, term, ty)) ->
-	 let context = CicMetaSubst.apply_subst_context subst context in
-	 let term = CicMetaSubst.apply_subst subst term in
-	 let ty = CicMetaSubst.apply_subst subst ty in  
-	 (i, (context, term, ty))) subst 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, args) =
+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
@@ -1074,21 +1040,29 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
     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 = CicMetaSubst.apply_subst subst ty in
-  let left = CicMetaSubst.apply_subst subst left in
-  let right = CicMetaSubst.apply_subst subst right in
-  let args = List.map (CicMetaSubst.apply_subst subst) args in
-  let rec fix_proof = function
+(*
+  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 term -> BasicProof (CicMetaSubst.apply_subst subst term)
+    | 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 = CicMetaSubst.apply_subst_context subst context in
-	       let term = CicMetaSubst.apply_subst subst term in
-	       let ty = CicMetaSubst.apply_subst subst ty in  
+	       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
@@ -1099,7 +1073,7 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
     @(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, args) in
+  let eq = (w, p, (ty, left, right, o), metasenv) in
   (* debug prerr_endline (string_of_equality eq); *)
   newmeta+1, eq  
 
@@ -1121,7 +1095,7 @@ let equality_of_term proof term =
       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
+      let e = (w, BasicProof ([],proof), stat, []) in
       e
   | _ ->
       raise TermIsNotAnEquality
@@ -1131,7 +1105,7 @@ let equality_of_term proof term =
 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 
 let is_weak_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) -> 
+  | (_, _, (ty, left, right, _), menv) -> 
        (left = right ||
           (meta_convertibility left right)) 
 	   (* the test below is not a good idea since it stops
@@ -1141,7 +1115,7 @@ let is_weak_identity (metasenv, context, ugraph) = function
 ;;
 
 let is_identity (metasenv, context, ugraph) = function
-  | (_, _, (ty, left, right, _), menv, _) ->
+  | (_, _, (ty, left, right, _), menv) ->
        (left = right ||
           (* (meta_convertibility left right)) *)
            (fst (CicReduction.are_convertible 
@@ -1150,7 +1124,7 @@ let is_identity (metasenv, context, ugraph) = function
 
 
 let term_of_equality equality =
-  let _, _, (ty, left, right, _), menv, _ = equality in
+  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 =