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

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 07d95ef86..e2f21b25c 100644
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -37,8 +37,7 @@ 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 *)
@@ -55,14 +54,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)
@@ -139,11 +138,11 @@ 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
@@ -311,8 +310,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
@@ -367,17 +366,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 +397,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 +450,76 @@ 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
+	   (i, (context, term, ty))) subst 
+  in
+  let flatten_fast subst = 
+    let resolve_meta (i, (context, term, ty)) subst = 
+	    let term = CicMetaSubst.apply_subst subst term in
+	    let ty = CicMetaSubst.apply_subst subst ty in  
+	     (i, (context, term, ty))
+    in
+    let resolve_meta t s = profiler3.HExtlib.profile (resolve_meta t) s in
+    let filter j (i,_) = i <> j in
+    let filter a b = profiler4.HExtlib.profile (filter a) b in
+    List.fold_left 
+      (fun subst (j,(c,t,ty)) as s ->  
+        let s = resolve_meta s subst in 
+        s::(List.filter (filter j) subst)) 
+      subst 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 flatten_fast subst = profiler2.HExtlib.profile flatten_fast subst in
+  (*let subst = flatten subst in*)
+(*  let subst = flatten_fast 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 +528,7 @@ let unification metasenv1 metasenv2 context t1 t2 ugraph =
   (subst, metasenv, ugraph)
     
 ;;
-
-exception MatchingFailure;;
+*)
 
 
 (*
@@ -603,7 +646,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 +665,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 +683,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,15 +699,53 @@ 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
+  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))
@@ -701,7 +792,7 @@ let find_equalities context proof =
                     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 e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -713,7 +804,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 (
@@ -851,7 +942,7 @@ let find_library_equalities dbd context status maxmeta =
                     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 e = (w, proof, stat, newmetas) in
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
@@ -860,7 +951,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
@@ -1063,7 +1154,7 @@ let relocate newmeta menv =
   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
@@ -1077,7 +1168,6 @@ let fix_metas newmeta (w, p, (ty, left, right, o), menv, args) =
   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
     | NoProof -> NoProof 
     | BasicProof term -> BasicProof (CicMetaSubst.apply_subst subst term)
@@ -1099,7 +1189,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 +1211,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 +1221,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 +1231,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 +1240,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 =