1) variables occurring only in proofs anre not relocated

2) during unification the resulting metasenv is cleaned of duplicates
   (duplicates can only be variables in proofs, not in left/right)

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 5f847bcb5ec6a0affae13d1883ec667e6e03087f..ec311615ede1b41cfae7ddf18deaa31235ffc770 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -78,18 +78,20 @@ let open_equality (_,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" 
+      let w, _, (ty, left, right, o), m , id = open_equality eq in
+      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" 
               id w (CicPp.ppterm ty)
               (CicPp.ppterm left) 
               (Utils.string_of_comparison o) (CicPp.ppterm right)
+       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   | 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" 
+      let w, _, (ty, left, right, o), m , id = open_equality eq in
+      Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]" 
               id w (CicPp.pp ty names)
               (CicPp.pp left names) (Utils.string_of_comparison o)
               (CicPp.pp right names)
+       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
 ;;
 
 let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
@@ -479,15 +481,17 @@ let wfo goalproof proof =
 
 let string_of_id names id = 
   try
-    let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+    let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
     match p with
     | Exact t -> 
-        Printf.sprintf "%d = %s: %s = %s" id
+        Printf.sprintf "%d = %s: %s = %s [%s]" id
           (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
+       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
     | Step (_,(step,id1, (_,id2), _) ) ->
-        Printf.sprintf "%6d: %s %6d %6d   %s = %s" id
+        Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
           (if step = SuperpositionRight then "SupR" else "Demo") 
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
+       (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   with
       Not_found -> assert false
 
@@ -545,9 +549,17 @@ let build_proof_term h lift proof =
   let rec aux = function
      | Exact term -> CicSubstitution.lift lift term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
+         if Subst.is_in_subst 302 subst then
+           prerr_endline ("TROVATA in " ^ string_of_int id1 ^ " " ^ string_of_int id2);
+
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
-           build_proof_step lift subst p1 p2 pos l r pred
+         let p =   build_proof_step lift subst p1 p2 pos l r pred in
+(*      let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
+          if not cond then
+            prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
+          assert cond;*)
+          p
   in
    aux proof
 ;;
@@ -575,7 +587,10 @@ let build_goal_proof l initial ty se =
     let rec aux se current_proof = function
       | [] -> current_proof,se
       | (pos,id,subst,pred)::tl ->
-           let p,l,r = proof_of_id id in
+         if Subst.is_in_subst 302 subst then
+           prerr_endline ("TROVATA in " ^ string_of_int id );
+
+          let p,l,r = proof_of_id id in
            let p = build_proof_term h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
            let proof = 
@@ -597,7 +612,7 @@ let build_goal_proof l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-  canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)), se
+  (*canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty))*)proof, se
 ;;
 
 let refl_proof ty term = 
@@ -612,26 +627,29 @@ let metas_of_proof p =
   Utils.metas_of_term p
 ;;
 
-let relocate newmeta menv =
-  let subst, metasenv, newmeta = 
+let relocate newmeta menv to_be_relocated =
+  let subst, newmetasenv, newmeta = 
     List.fold_right 
-      (fun (i, context, ty) (subst, menv, maxmeta) ->         
-        let irl = [] (*
-         CicMkImplicit.identity_relocation_list_for_metavariable context *)
-        in
-        let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
-        let newmeta = maxmeta, context, ty in
-        newsubst, newmeta::menv, maxmeta+1) 
-      menv (Subst.empty_subst, [], newmeta+1)
+      (fun i (subst, metasenv, maxmeta) ->         
+        let _,context,ty = CicUtil.lookup_meta i menv in
+        let irl = [] in
+        let newmeta = Cic.Meta(maxmeta,irl) in
+        let newsubst = Subst.buildsubst i context newmeta ty subst in
+        newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) 
+      to_be_relocated (Subst.empty_subst, [], newmeta+1)
   in
-  let metasenv = Subst.apply_subst_metasenv subst metasenv in
-  let subst = Subst.flatten_subst subst in
-  subst, metasenv, newmeta
+  let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
+  subst, menv, newmeta
 
 
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
-  let subst, metasenv, newmeta = relocate newmeta menv in
+  let to_be_relocated = 
+    HExtlib.list_uniq 
+      (List.sort Pervasives.compare 
+        (Utils.metas_of_term left @ Utils.metas_of_term right)) 
+  in
+  let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in
   let left = Subst.apply_subst subst left in
   let right = Subst.apply_subst subst right in
@@ -641,8 +659,8 @@ let fix_metas newmeta eq =
         Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
   in
   let p = fix_proof p in
-  let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
-  newmeta+1, eq  
+  let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in
+  newmeta+1, eq'  
 
 exception NotMetaConvertible;;
 

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index a2e6eda07443be5d7e644136861f7520e14d3121..dd2d0a422e1fee06df487e362a3966e9b4f57c19 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -1057,7 +1057,7 @@ let superposition_left (metasenv, context, ugraph) table goal =
 (** demodulation, when the target is a goal *)
 let rec demodulation_goal env table goal =
   let goalproof,menv,_,_,left,right = open_goal goal in
-  let metasenv, context, ugraph = env in
+  let _, context, ugraph = env in
 (*  let term = Utils.guarded_simpl (~debug:true) context term in*)
   let do_right () = 
       let resright = demodulation_aux menv context ugraph table 0 right in

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index ab27f8a314b13e4b75cce13afbd272a7f9440475..36e9f99a64a710785976c200979d0764620bc849 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -139,7 +139,10 @@ let profiler3 = HExtlib.profile "P/Inference.unif_simple[resolve_meta]"
 let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
 
 let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
-  let metasenv = metasenv1 @ metasenv2 in
+  let metasenv = 
+    HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
+    (*metasenv1 @ metasenv2*)
+  in
   let subst, menv, ug =
     if not (is_simple_term t1) || not (is_simple_term t2) then (
       debug_print

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 445eccdbc2f217565c67b5f319cb2652c105066e..e12b1f8a7a1b23591749e6de244da6804152e15b 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1692,7 +1692,7 @@ let saturate
   let eq_indexes, equalities, maxm = find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
-  let goal = [], metasenv, type_of_goal in
+  let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, type_of_goal in
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
@@ -1760,6 +1760,7 @@ let saturate
     (goalproof,newproof,subsumption_subst, proof_menv) ->
       prerr_endline "OK, found a proof!";
       prerr_endline (Equality.pp_proof names goalproof newproof);
+      prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
       prerr_endline "ENDOFPROOFS";
       (* generation of the CIC proof *)
       let side_effects = 
@@ -1771,7 +1772,7 @@ let saturate
         let initial = newproof in
         Equality.build_goal_proof goalproof initial type_of_goal side_effects
       in
-prerr_endline (CicPp.pp goal_proof names);
+(*prerr_endline (CicPp.pp goal_proof names);*)
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let side_effects_t = 
         List.map (Subst.apply_subst subsumption_subst) side_effects_t
@@ -1790,6 +1791,8 @@ prerr_endline (CicPp.pp goal_proof names);
                    (Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl))) 
           ([],[],[],None) proof_menv 
       in
+prerr_endline ("RIMPIAZZATO CON " ^ match free_meta with None -> "?" | Some m -> CicPp.ppterm m);
+
       let replace where = 
         ProofEngineReduction.replace_lifting 
           ~equality:(=) ~what ~with_what ~where
@@ -1803,6 +1806,7 @@ prerr_endline (CicPp.pp goal_proof names);
           (ProofEngineHelpers.compare_metasenvs 
             ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv)
       in
+prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) );
       (* check/refine/... build the new proof *)
       let replaced_goal = 
         ProofEngineReduction.replace
@@ -1827,6 +1831,7 @@ prerr_endline (CicPp.pp goal_proof names);
       let final_subst = 
         (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
       in
+prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv);
       let _ = 
         try
           CicTypeChecker.type_of_aux' real_menv context goal_proof
@@ -1837,7 +1842,7 @@ prerr_endline (CicPp.pp goal_proof names);
         | CicTypeChecker.AssertFailure _ 
         | Invalid_argument "list_fold_left2" as exn ->
             prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-            prerr_endline (CicPp.pp goal_proof names);
+(*            prerr_endline (CicPp.pp goal_proof names); *)
             raise exn
       in
       let proof, real_metasenv =