X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Ftactics%2Fparamodulation%2Finference.ml;h=f5508c8c146cc72bc2c418b5ae80770febf6fd4c;hb=86d27070abaa7844fa53ab83b8a57489cc2d7e1a;hp=fdaf68018ee5971516f1be9700ae497cf6bafe4c;hpb=1d7de941e98a1d80ef3103636148537ada3e2b9e;p=helm.git

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index fdaf68018..f5508c8c1 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -367,17 +367,21 @@ let rec is_simple_term = function
 ;;
 
 
-let lookup_subst meta subst =
+let rec lookup_subst meta subst =
   match meta with
   | Cic.Meta (i, _) -> (
-      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
+      try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst 
+      in lookup_subst t subst 
       with Not_found -> meta
     )
-  | _ -> assert false
+  | _ -> meta
 ;;
 
+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 module C = Cic in
   let module M = CicMetaSubst in
   let module U = CicUnification in
@@ -394,14 +398,24 @@ 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
@@ -437,45 +451,56 @@ let unification_simple metasenv context t1 t2 ugraph =
   List.rev subst, menv, ugraph
 ;;
 
+let profiler = HExtlib.profile "flatten"
 
-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
+	   (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 flatten subst = profiler.HExtlib.profile flatten subst in
+  let subst = flatten subst in
+    subst, menv, ug
+;;
+
+exception MatchingFailure;;
+
+let matching1 metasenv1 metasenv2 context t1 t2 ugraph = 
+  try 
+    unification_aux false metasenv1 metasenv2 context t1 t2 ugraph
+  with
+    CicUnification .UnificationFailure _ ->
+      raise MatchingFailure
 ;;
 
+let unification = unification_aux true 
+;;
 
+
+
+(*
 let unification metasenv1 metasenv2 context t1 t2 ugraph = 
   let (subst, metasenv, ugraph) = 
     CicUnification.fo_unif (metasenv1@metasenv2) context t1 t2 ugraph in
@@ -484,8 +509,7 @@ let unification metasenv1 metasenv2 context t1 t2 ugraph =
   (subst, metasenv, ugraph)
     
 ;;
-
-exception MatchingFailure;;
+*)
 
 
 (*
@@ -603,7 +627,8 @@ let matching metasenv context t1 t2 ugraph =
 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 matching2 metasenv1 metasenv2 context t1 t2 ugraph =
       let subst, metasenv, ugraph =
 	try
           unification metasenv1 metasenv2 context t1 t2 ugraph
@@ -621,9 +646,17 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 	    ignore(check_disjoint_invariant subst metasenv "qua-2");
       (* let us unfold subst *)
       if metasenv = metasenv1 then 
-	subst, metasenv, ugraph (* everything is fine *)
+	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
+	  subst, metasenv, ugraph (* everything is fine *)
       else
 	(* let us unfold subst *)
+	(* 
 	let subst =
 	  List.map
 	    (fun (i, (context, term, ty)) ->
@@ -631,6 +664,7 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 	       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
@@ -646,13 +680,51 @@ let matching metasenv1 metasenv2 context t1 t2 ugraph =
 			 ((j, (c, Cic.Meta (i, lc), ty))::subst,
 			  (i,c,ty)::metasenv')
 		   |_ -> s::subst,metasenv) ([],metasenv) subst
-	in
+	in	
 	(* finally, let us chek again that metasenv = metasenv1 *)
 	if metasenv = metasenv1 then 
 	  subst, metasenv, ugraph
 	else raise MatchingFailure  
 ;;
 
+(* debug 
+let matching metasenv1 metasenv2 context t1 t2 ugraph =
+  let rc1 = 
+    try Some (matching1 metasenv1 metasenv2 context t1 t2 ugraph)
+    with MatchingFailure -> None
+  in
+  let rc2 = 
+    try 
+      Some (matching2 metasenv1 metasenv2 context t1 t2 ugraph)
+    with MatchingFailure -> None
+  in
+  match rc1,rc2 with
+  | Some (s,m,g) , None -> 
+      prerr_endline (CicPp.ppterm t1);
+      prerr_endline (CicPp.ppterm t2);
+      prerr_endline "SOLO NOI";
+      prerr_endline (CicMetaSubst.ppsubst s);
+      s,m,g
+  | None , Some _ -> 
+      prerr_endline (CicPp.ppterm t1);
+      prerr_endline (CicPp.ppterm t2);
+      prerr_endline "SOLO LUI";
+      assert false
+  | None, None -> raise MatchingFailure 
+  | Some (s,m,g), Some (s',m',g') ->
+      let s = List.sort (fun (i,_) (j,_) -> i - j) s in
+      let s' = List.sort (fun (i,_) (j,_) -> i - j) s' in
+      if s <> s' then 
+	begin
+	  prerr_endline (CicMetaSubst.ppsubst s);
+	  prerr_endline (CicMetaSubst.ppsubst s');
+	  prerr_endline (CicPp.ppterm t1);
+	  prerr_endline (CicPp.ppterm t2);
+	  	end;
+      s,m,g
+*)  
+let matching = matching1;;
+
 let check_eq context msg eq =
   let w, proof, (eq_ty, left, right, order), metas, args = eq in
   if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
@@ -698,9 +770,10 @@ let find_equalities context proof =
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
-                    let w = compute_equality_weight ty 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, (ty, t1, t2, o), newmetas, args) in
+                    let e = (w, proof, stat, newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -710,8 +783,9 @@ let find_equalities context proof =
               let t1 = S.lift index t1 in
               let t2 = S.lift index t2 in
               let o = !Utils.compare_terms t1 t2 in
-              let w = compute_equality_weight ty t1 t2 in
-              let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
+              let stat = (ty,t1,t2,o) in
+              let w = compute_equality_weight stat in
+              let e = (w, BasicProof (C.Rel index), stat, [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in (
@@ -846,17 +920,19 @@ let find_library_equalities dbd context status maxmeta =
                       (lazy
                          (Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
-                    let w = compute_equality_weight ty 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, (ty, t1, t2, o), newmetas, args) in
+                    let e = (w, proof, stat, newmetas, args) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
               when iseq uri && not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
-              let w = compute_equality_weight ty t1 t2 in
-              let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in
+              let stat = (ty,t1,t2,o) in
+              let w = compute_equality_weight stat in
+              let e = (w, BasicProof term, stat, [], []) in
               Some e, (newmeta+1)
           | _ -> None, newmeta
         in
@@ -1115,8 +1191,9 @@ let equality_of_term proof term =
   match term with
   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
       let o = !Utils.compare_terms t1 t2 in
-      let w = compute_equality_weight ty t1 t2 in
-      let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) 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