New unification and new matching.

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 07d95ef866aa0ba5c88e6d94e3b8bbebcaafa52c..f5508c8c146cc72bc2c418b5ae80770febf6fd4c 100644 (file)
--- 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

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index b3fa5f3fcd955d283fede4fef9ef6eea912a1edf..b6678683d5d73688473e9d91b9849d429030df57 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -468,8 +468,12 @@ let infer env sign current (active_list, active_table) =
               let neg, pos = infer_positive table tl in
               neg, res @ pos
         in
+        let maxm, copy_of_current = Inference.fix_metas !maxmeta current in
+        maxmeta := maxm;
         let curr_table = Indexing.index Indexing.empty current in
-        let neg, pos = infer_positive curr_table active_list in
+        let neg, pos = 
+         infer_positive curr_table ((sign,copy_of_current)::active_list) 
+       in
          if Utils.debug_metas then 
            ignore(List.map 
                     (function current -> 
@@ -1774,7 +1778,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
                  " LOCALMAX: " ^ string_of_int !Indexing.local_max ^
                 " #ACTIVES: " ^ string_of_int (size_of_active active) ^
                  " #PASSIVES: " ^ string_of_int (size_of_passive passive));
-  if (size_of_active active) mod 54 = 0 then
+  if (size_of_active active) mod 50 = 0 then
     (let s = Printf.sprintf "actives:\n%s\n"
       (String.concat "\n"
          ((List.map
@@ -1828,6 +1832,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
       forward_simpl_time := !forward_simpl_time +. (time2 -. time1);
       match res with
       | None ->
+          (* weight_age_counter := !weight_age_counter + 1; *)
           given_clause_fullred dbd env goals theorems passive active
       | Some (sign, current) ->
           if (sign = Negative) && (is_identity env current) then (

diff --git a/components/tactics/paramodulation/utils.ml b/components/tactics/paramodulation/utils.ml
index 8fb1d42bcf60bf6adae07c5ae7826995632f245e..db19e87d1d89f77f67ed818df82b625e323da12e 100644 (file)
--- a/components/tactics/paramodulation/utils.ml
+++ b/components/tactics/paramodulation/utils.ml
@@ -41,8 +41,6 @@ let print_metasenv metasenv =
 ;;
 
 
-
-
 let print_subst ?(prefix="\n") subst =
     String.concat prefix
      (List.map