the tactic now returns as open goals the open metas in the proof

subsumption is now used correctly in given_clause_fullred

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index e6a2463c099a8a084e4ac83e42497eac382e3653..873cc5698cadab2be35ce92860a7cab7ad7c14ec 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -407,7 +407,13 @@ let find_all_matches
 (*
   returns true if target is subsumed by some equality in table
 *)
-let subsumption env table target =
+let subsumption env table target = 
+  (* 
+  let print_res l =
+    prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+    ((pos,equation),_)) -> Inference.string_of_equality equation)l))
+  in
+  *)
   let _, _, (ty, left, right, _), tmetas = target in
   let metasenv, context, ugraph = env in
   let metasenv = tmetas in
@@ -434,16 +440,18 @@ let subsumption env table target =
         find_all_matches ~unif_fun:Inference.matching
           metasenv context ugraph 0 left ty leftc
   in
+(*  print_res leftr;*)
   let rec ok what = function
-    | [] -> false, []
-    | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
+    | [] -> None
+    | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+        let _, _, (_, l, r, o), m = equation in
         try
           let other = if pos = Utils.Left then r else l in
           let subst', menv', ug' =
             let t1 = Unix.gettimeofday () in
             try
               let r = 
-                Inference.matching metasenv menv context what other ugraph
+                Inference.matching metasenv m context what other ugraph
               in
               let t2 = Unix.gettimeofday () in
               match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
@@ -455,15 +463,13 @@ let subsumption env table target =
           in
           (match merge_if_possible subst subst' with
           | None -> ok what tl
-          | Some s -> true, s)
+          | Some s -> Some (s, equation))
         with Inference.MatchingFailure ->
           ok what tl
   in
-  let r, subst = ok right leftr in
-  let r, s =
-    if r then
-      true, subst
-    else
+  match ok right leftr with
+  | Some _ as res -> res
+  | None -> 
       let rightr =
         match right with
           | Cic.Meta _ -> [] 
@@ -472,14 +478,13 @@ let subsumption env table target =
                 find_all_matches ~unif_fun:Inference.matching
                   metasenv context ugraph 0 right ty rightc
       in
+(*        print_res rightr;*)
         ok left rightr
-  in
 (*     (if r then  *)
 (*        debug_print  *)
 (*          (lazy *)
 (*             (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
 (*                (Inference.string_of_equality target) (Utils.print_subst s)))); *)
-    r, s
 ;;
 
 let rec demodulation_aux ?from ?(typecheck=false) 
@@ -709,6 +714,8 @@ let rec demodulation_equality ?from newmeta env table sign target =
           prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
           prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
           prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+          prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
+            newmenv));
           raise exc;
       else () 
     in

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index d10d7e6d86a9ef102c6f544da1df4c6c47b4bbaa..5af20df5c66bc17b93e707f501cd314aae4dd6e2 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -49,7 +49,7 @@ val subsumption :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   Inference.equality ->
-  bool * Inference.substitution
+  (Inference.substitution * Inference.equality) option
 val superposition_left :
   int ->
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->

diff --git a/helm/software/components/tactics/paramodulation/inference.ml b/helm/software/components/tactics/paramodulation/inference.ml
index 547a235590a7991ddc8144f94f0ade20984b7aa7..a3894fd84cdbfa374ecc3e570ac8bbbb2fad57df 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.ml
+++ b/helm/software/components/tactics/paramodulation/inference.ml
@@ -541,11 +541,11 @@ let unification_simple locked_menv metasenv context t1 t2 ugraph =
           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

diff --git a/helm/software/components/tactics/paramodulation/inference.mli b/helm/software/components/tactics/paramodulation/inference.mli
index 107e3b81911ca470d0422b190811e692947afa52..b08054ca4f2c90c72dc97ade2d53e493b8ed0260 100644 (file)
--- a/helm/software/components/tactics/paramodulation/inference.mli
+++ b/helm/software/components/tactics/paramodulation/inference.mli
@@ -142,4 +142,5 @@ val metas_of_proof: proof -> int list
 val fix_metas: int -> equality -> int * equality
 
 val apply_subst: substitution -> Cic.term -> Cic.term
+val apply_subst_metasenv: substitution -> Cic.metasenv -> Cic.metasenv
 val ppsubst: substitution -> string

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 07c6c601291ce9660e7d86ee5a9f9ec63b52399b..e88a061a3e9ae85b27aea9118329f3acfe3c8dde 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -87,7 +87,7 @@ let test eq = false
 
 type result =
   | ParamodulationFailure
-  | ParamodulationSuccess of Inference.proof option * environment
+  | ParamodulationSuccess of (Inference.proof * Cic.metasenv) option
 ;;
 
 type goal = proof * Cic.metasenv * Cic.term;;
@@ -650,17 +650,20 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) =
       else
         match passive_table with
         | None -> 
-            if fst (Indexing.subsumption env active_table c) then
-              None
-            else
+            if Indexing.subsumption env active_table c = None then
               res
+            else
+              None
         | Some passive_table ->
             if Indexing.in_index passive_table c then None
             else 
-              let r1, _ = Indexing.subsumption env active_table c in
-              if r1 then None else
-                let r2, _ = Indexing.subsumption env passive_table c in 
-                if r2 then None else res
+              if Indexing.subsumption env active_table c = None then
+                if Indexing.subsumption env passive_table c = None then
+                  res 
+                else
+                  None
+              else
+                None
 ;;
 
 type fs_time_info_t = {
@@ -736,10 +739,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active =
   let subs =
     match passive_table with
     | None ->
-        (fun e -> not (fst (Indexing.subsumption env active_table e)))
+        (fun e -> (Indexing.subsumption env active_table e = None))
     | Some passive_table ->
-        (fun e -> not ((fst (Indexing.subsumption env active_table e)) ||
-                         (fst (Indexing.subsumption env passive_table e))))
+        (fun e -> ((Indexing.subsumption env active_table e = None) &&
+                         (Indexing.subsumption env passive_table e = None)))
   in
 (*   let t1 = Unix.gettimeofday () in *)
 (*   let t2 = Unix.gettimeofday () in *)
@@ -782,8 +785,11 @@ let rec simplify_goal env goal ?passive (active_list, active_table) =
         let changed', goal = demodulate passive_table goal in
         (changed || changed'), goal
   in
-  changed, if not changed then goal 
-  else snd (simplify_goal env goal ?passive (active_list, active_table))
+  changed,
+  if not changed then 
+    goal 
+  else 
+    snd (simplify_goal env goal ?passive (active_list, active_table)) 
 ;;
 
 
@@ -976,9 +982,12 @@ let make_theorems theorems =
 
 
 let activate_goal (active, passive) =
-  match passive with
-  | goal_conj::tl -> true, (goal_conj::active, tl)
-  | [] -> false, (active, passive)
+  if active = [] then
+    match passive with
+    | goal_conj::tl -> true, (goal_conj::active, tl)
+    | [] -> false, (active, passive)
+  else  
+    true, (active,passive)
 ;;
 
 
@@ -1741,6 +1750,31 @@ and given_clause_aux dbd env goals theorems passive active =
 ;;
 *)
 
+let check_if_goal_is_subsumed env (proof,menv,ty) table =
+  match ty with
+  | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
+    when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+      (let goal_equation = 0,proof,(eq_ty,left,right,Eq),menv in
+      match Indexing.subsumption env table goal_equation with
+      | Some (subst, (_,p,_,m)) ->
+          let p = Inference.apply_subst subst (Inference.build_proof_term p) in
+          let newp =
+            let rec repl = function
+              | Inference.ProofGoalBlock (_, gp) ->
+                  Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
+              | Inference.NoProof -> Inference.BasicProof ([],p)
+              | Inference.BasicProof _ -> Inference.BasicProof ([],p)
+              | Inference.SubProof (t, i, p2) ->
+                  Inference.SubProof (t, i, repl p2)
+              | _ -> assert false
+            in
+            repl proof
+          in
+          Some (newp,Inference.apply_subst_metasenv subst m @ menv)
+      | None -> None)
+  | _ -> None
+;;
+
 let counter = ref 0
 
 (** given-clause algorithm with full reduction strategy *)
@@ -1790,22 +1824,13 @@ let rec given_clause_fullred dbd env goals theorems passive active =
                 | _ -> assert false
               in
               repl proof
-            in true, Some newp
-        | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_-> 
-            (* here we check if the goal is subsumed by an active *)
-            let ok, subst = 
-              (* the first m is unused *)
-               Indexing.subsumption (m,context,CicUniv.empty_ugraph) 
-                 (snd active)
-                 (0,proof,(eq_ty,left,right,Eq),m)
-            in
-            if ok then
-              begin
-                prerr_endline "The goal is subsumed by an active";
-                false, None
-              end
-            else
-              ok, None
+            in true, Some (newp,m)
+        | (_, [proof,m,ty])::_ ->
+            (match check_if_goal_is_subsumed env (proof,m,ty) (snd active) with
+            | None -> false,None
+            | Some (newproof,m) ->
+                prerr_endline "Proof found by subsumption!";
+                true, Some (newproof,m))
         | _ -> false, None
     in 
     if ok then
@@ -1844,7 +1869,7 @@ let rec given_clause_fullred dbd env goals theorems passive active =
                 (let x,y,_ = passive in (fst x)@(fst y)))) in
           prerr_endline s;
           prerr_endline sp; *)
-      ParamodulationSuccess (proof, env))
+      ParamodulationSuccess (proof))
     else
       given_clause_fullred_aux dbd env goals theorems passive active
   else
@@ -1974,7 +1999,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active =
               (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign)
                        (string_of_equality ~env current)));
             let _, proof, _, m = current in 
-            ParamodulationSuccess (Some proof, env)
+            ParamodulationSuccess (Some (proof, m))
           ) else (
             debug_print
               (lazy "\n================================================");
@@ -2094,10 +2119,10 @@ end prova *)
             | true, goal ->
                 let proof =
                   match goal with
-                  | Some goal -> let _, proof, _, _ = goal in Some proof
+                  | Some goal -> let _, proof, _, env = goal in Some (proof,env)
                   | None -> None
                 in
-                ParamodulationSuccess (proof, env)
+                ParamodulationSuccess proof
           )
   
 ;;
@@ -2269,7 +2294,7 @@ let main dbd full term metasenv ugraph =
         match res with
         | ParamodulationFailure ->
             Printf.printf "NO proof found! :-(\n\n"
-        | ParamodulationSuccess (Some proof, env) ->
+        | ParamodulationSuccess (Some (proof, env)) ->
             let proof = Inference.build_proof_term proof in
             Printf.printf "OK, found a proof!\n";
             (* REMEMBER: we have to instantiate meta_proof, we should use
@@ -2300,7 +2325,7 @@ let main dbd full term metasenv ugraph =
             in
             ()
               
-        | ParamodulationSuccess (None, env) ->
+        | ParamodulationSuccess None ->
             Printf.printf "Success, but no proof?!?\n\n"
       in
         if Utils.time then
@@ -2362,6 +2387,7 @@ let saturate
   let module C = Cic in
   reset_refs ();
   Indexing.init_index ();
+  counter := 0;
   maxdepth := depth;
   maxwidth := width;
 (*  CicUnification.unif_ty := false;*)
@@ -2439,9 +2465,30 @@ let saturate
     (res, finish -. start)
   in
   match res with
-  | ParamodulationSuccess (Some proof, _) ->
+  | ParamodulationSuccess (Some (proof, proof_menv)) ->
       debug_print (lazy "OK, found a proof!");
       let proof = Inference.build_proof_term proof in
+      let equality_for_replace i t1 =
+        match t1 with
+        | C.Meta (n, _) -> n = i
+        | _ -> false
+      in
+      let proof_menv, what, with_what = 
+        let irl = 
+          CicMkImplicit.identity_relocation_list_for_metavariable context
+        in
+        List.fold_left 
+          (fun (acc1,acc2,acc3) (i,_,ty) -> 
+            (i,context,ty)::acc1, 
+            (Cic.Meta(i,[]))::acc2, 
+            (Cic.Meta(i,irl)) ::acc3) 
+          ([],[],[]) proof_menv 
+      in
+      let proof = ProofEngineReduction.replace_lifting
+              ~equality:(=)
+              ~what ~with_what
+              ~where:proof
+      in
       (* prerr_endline (CicPp.ppterm proof); *)
       let names = names_of_context context in
       let newmetasenv =
@@ -2451,6 +2498,7 @@ let saturate
         in
         List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
       in
+      let newmetasenv = newmetasenv@proof_menv in
       let newstatus =
         try
           let ty, ug =
@@ -2465,11 +2513,6 @@ let saturate
                   (string_of_bool
                      (fst (CicReduction.are_convertible
                              context type_of_goal ty ug)))));
-          let equality_for_replace i t1 =
-            match t1 with
-            | C.Meta (n, _) -> n = i
-            | _ -> false
-          in
           let real_proof =
             ProofEngineReduction.replace
               ~equality:equality_for_replace
@@ -2484,7 +2527,8 @@ let saturate
                   (print_metasenv newmetasenv)
                   (CicPp.pp real_proof [](* names *))
                   (CicPp.pp term_to_prove names)));
-          ((uri, newmetasenv, real_proof, term_to_prove), [])
+          ((uri, newmetasenv, real_proof, term_to_prove), 
+            List.map (fun (i,_,_) -> i) proof_menv)
         with CicTypeChecker.TypeCheckerFailure _ ->
           debug_print (lazy "THE PROOF DOESN'T TYPECHECK!!!");
           debug_print (lazy (CicPp.pp proof names));

diff --git a/helm/software/components/tactics/paramodulation/saturation.mli b/helm/software/components/tactics/paramodulation/saturation.mli
index 17fbb8cfdb326a18a5848f1b1ef36972ab0da1fe..95f258124f10942c7905c042e225eb303707ec61 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.mli
+++ b/helm/software/components/tactics/paramodulation/saturation.mli
@@ -33,7 +33,7 @@ val saturate :
   ?width:int ->
   ProofEngineTypes.proof * ProofEngineTypes.goal ->
   (UriManager.uri option * Cic.conjecture list * Cic.term * Cic.term) *
-  'a list
+  ProofEngineTypes.goal list
 
 val weight_age_ratio : int ref
 val weight_age_counter: int ref