Demodulate used to be a reduction_kind and it used to take a ~pattern.

[helm.git] / helm / software / components / tactics / paramodulation / saturation.ml

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 81c2a15f1920d2cd7e496643cf912d6042432bc3..6cd2bcf4a8240813ef0bdf520902576d69369fb8 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -126,7 +126,11 @@ let passive_is_empty = function
   | _ -> false
 ;;
 
-
+let no_more_passive_goals = function
+  | _,[] -> true
+  | _ -> false
+;;
+  
 let size_of_passive ((passive_list, ps), _) = List.length passive_list
 (* EqualitySet.cardinal ps *)
 ;;
@@ -913,8 +917,8 @@ let pp_goal_set msg goals names =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*
   let names = names_of_context ctx in
+(*
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
 *)
   match ty with
@@ -928,8 +932,10 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
        match Indexing.unification env table goal_equation with 
         | Some (subst, equality, swapped ) ->
             prerr_endline 
-              ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
-            prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
+              ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+            prerr_endline 
+              ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
+            prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
@@ -1028,8 +1034,11 @@ let infer_goal_set env active goals =
             let new_passive_goals =
               if Utils.metas_of_term t1 = [] then passive_goals
               else 
-                let new' = 
-                   Indexing.superposition_left env (snd active) selected in
+                let newmaxmeta,new' = 
+                   Indexing.superposition_left env (snd active) selected
+                   !maxmeta 
+                in
+                maxmeta := newmaxmeta;
                 passive_goals @ new'
             in
             selected::active_goals, new_passive_goals
@@ -1064,16 +1073,17 @@ let infer_goal_set env active goals =
 ;;
 *)
 
-let infer_goal_set_with_current env current goals = 
+let infer_goal_set_with_current env current goals active = 
   let active_goals, passive_goals = goals in
-  let l,table,_  = build_table [current] in
   let active_goals, _ = 
-    simplify_goal_set env goals (l,table)
+    simplify_goal_set env goals active
   in
+  let l,table,_  = build_table [current] in
   active_goals, 
   List.fold_left 
     (fun acc g ->
-      let new' = Indexing.superposition_left env table g in
+      let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+      maxmeta := newmaxmeta;
       acc @ new')
     passive_goals active_goals
 ;;
@@ -1150,7 +1160,11 @@ let given_clause
       | None -> 
           (* SELECTION *)
           if passive_is_empty passive then
-            ParamodulationFailure "No more passive"(*maybe this is a success! *)
+            if no_more_passive_goals goals then 
+              ParamodulationFailure "No more passive equations/goals"
+              (*maybe this is a success! *)
+            else
+              step goals theorems passive active (iterno+1)
           else
             begin
               (* COLLECTION OF GARBAGED EQUALITIES *)
@@ -1187,11 +1201,22 @@ let given_clause
                   prerr_endline "infer";
                   let new' = infer eq_uri env current active in
                   prerr_endline "infer goal";
-                  let goals = infer_goal_set_with_current env current goals in
+(*
+      match check_if_goals_set_is_solved env active goals with
+      | Some p -> 
+          prerr_endline 
+            (Printf.sprintf "Found a proof in: %f\n" 
+              (Unix.gettimeofday() -. initial_time));
+          ParamodulationSuccess p
+      | None -> 
+*)
                   let active = 
                       let al, tbl = active in
                       al @ [current], Indexing.index tbl current
                   in
+                  let goals = 
+                    infer_goal_set_with_current env current goals active 
+                  in
                   (* FORWARD AND BACKWARD SIMPLIFICATION *)
                   prerr_endline "fwd/back simpl";
                   let rec simplify new' active passive =
@@ -1555,7 +1580,7 @@ let saturate
 *)
       let goals = make_goal_set goal in
       let max_iterations = 10000 in
-      let max_time = Unix.gettimeofday () +.  600. (* minutes *) in
+      let max_time = Unix.gettimeofday () +.  300. (* minutes *) in
       given_clause 
         eq_uri env goals theorems passive active max_iterations max_time 
     in
@@ -1571,7 +1596,6 @@ let saturate
       prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
-      prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
       prerr_endline "ENDOFPROOFS";
       (* generation of the CIC proof *)
       let side_effects = 
@@ -1584,6 +1608,7 @@ let saturate
         Equality.build_goal_proof 
           eq_uri goalproof initial type_of_goal side_effects
       in
+      prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
 (*prerr_endline (CicPp.pp goal_proof names);*)
@@ -1848,7 +1873,7 @@ let main_demod_equalities dbd term metasenv ugraph =
 *)
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
+let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = 
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let eq_uri = eq_of_goal ty in 
@@ -1892,13 +1917,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) =
   else (* if newty = ty then *)
     raise (ProofEngineTypes.Fail (lazy "no progress"))
   (*else ProofEngineTypes.apply_tactic 
-    (ReductionTactics.simpl_tac ~pattern) 
-    initialstatus*)
+    (ReductionTactics.simpl_tac
+      ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
 ;;
 
-let demodulate_tac ~dbd ~pattern = 
-  ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)
-;;
+let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
 
 let rec find_in_ctx i name = function
   | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
@@ -1966,6 +1989,12 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
       let t = Equality.term_of_equality eq_uri e in
       prerr_endline (CicPp.pp t names)) 
   eql;
+  prerr_endline ("\n result proofs: ");
+  List.iter (fun e -> 
+    prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+    let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
+    Subst.ppsubst s ^ "\n" ^ 
+    CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
   if demod_table <> "" then
     begin
       let demod =