]> matita.cs.unibo.it Git - helm.git/commitdiff
cleanup of saturate
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 26 Apr 2006 09:59:07 +0000 (09:59 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 26 Apr 2006 09:59:07 +0000 (09:59 +0000)
components/tactics/paramodulation/saturation.ml

index 59b06ef2986e711d900a81d1588773b1df868d96..5cc6e811e293fe5e80afd926a1ab32e5e1e7254c 100644 (file)
@@ -1522,21 +1522,29 @@ let saturate
   in
   match res with
   | ParamodulationSuccess 
-    (Some ((goalproof,newproof,subsumption_subst, newproof_menv),(proof, proof_menv))) ->
+      (Some 
+        ((goalproof,newproof,subsumption_subst, newproof_menv), (* NEW *)
+         (proof, proof_menv))) (* OLD *)
+      ->
       prerr_endline "OK, found a proof!";
-      prerr_endline (Equality.string_of_proof_old proof);
       
+      (* generation of the old proof *)
       let cic_proof = Equality.build_proof_term_old proof in
-      
+     
+      (* generation of the new proof *)
       let cic_proof_new,cic_proof_new_menv = 
-        Equality.build_goal_proof goalproof (Equality.build_proof_term_new newproof) 
+        Equality.build_goal_proof 
+          goalproof (Equality.build_proof_term_new newproof) 
       in
       let newproof_menv = 
         Equality.apply_subst_metasenv subsumption_subst 
           (newproof_menv @ cic_proof_new_menv)
       in
-      let cic_proof_new = Equality.apply_subst subsumption_subst cic_proof_new in
+      let cic_proof_new = 
+        Equality.apply_subst subsumption_subst cic_proof_new 
+      in
       
+      (* replacing fake mets with real ones *)
       let equality_for_replace i t1 =
         match t1 with
         | C.Meta (n, _) -> n = i
@@ -1573,6 +1581,8 @@ let saturate
               ~what ~with_what
               ~where:cic_proof_new
       in
+
+      (* pp new/old proof *)
       let names = names_of_context context in
       prerr_endline "OLDPROOF";
       prerr_endline (Equality.string_of_proof_old proof);
@@ -1582,6 +1592,8 @@ let saturate
       prerr_endline (Equality.string_of_proof_new ~names newproof goalproof); 
       prerr_endline "NEWPROOFCIC";
       prerr_endline (CicPp.pp cic_proof_new names); 
+
+      (* generation of proof metasenv *)
       let newmetasenv =
         let i1 =
           match new_meta_goal with
@@ -1591,119 +1603,108 @@ let saturate
       in
       let newmetasenv = newmetasenv@proof_menv in
       let newmetasenv_new = newmetasenv@newproof_menv in
+
+      (* check/refine/... build the new proof *)
       let newstatus =
-        try
-          let cic_proof,newmetasenv,proof_menv,ty, ug =
-            prerr_endline "type checking ... (old) ";
-(*            let old_ty, oldug = *)
-(*              CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *)
-(*            in*)
-            let cic_proof_new,new_ty,newmetasenv_new,newug = 
-              try
-                (*
-                 prerr_endline "refining ... (new) ";
-                 CicRefine.type_of_aux' 
-                  newmetasenv_new context cic_proof_new ugraph*)
-                let ty,ug = 
-                  prerr_endline "typechecking ... (new) ";
-                  CicTypeChecker.type_of_aux' 
-                    newmetasenv_new context cic_proof_new ugraph
-                in
-                cic_proof_new, ty, newmetasenv_new, ug
-              with
-              | CicTypeChecker.TypeCheckerFailure s ->
-                  prerr_endline "FAILURE IN TYPECHECKING";
-                  prerr_endline (Lazy.force s);
-                  assert false
-              | CicRefine.RefineFailure s 
-              | CicRefine.Uncertain s 
-              | CicRefine.AssertFailure s -> 
-                  prerr_endline "FAILURE IN REFINE";
-                  prerr_endline (Lazy.force s);
-                  interactive_comparison context cic_proof_new cic_proof;
-                  assert false
-            in
-(*
-            prerr_endline "check unif ... (old vs new) ";
-            (try 
-              ignore(CicUnification.fo_unif 
-                newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph)
-            with CicUnification.UnificationFailure _ -> 
-              prerr_endline "WARNING, new and old proofs are not unifiable");
-            prerr_endline "unif ... (new) ";
-            let subst, newmetasenv_new, newug = 
-              CicUnification.fo_unif 
-                newmetasenv_new context new_ty type_of_goal newug
-            in
-            if subst <> [] then
-              prerr_endline "UNIF SERVE ################################";
-*)
-            let subst = [] in 
-            if List.length newmetasenv_new <> 0 then
-              prerr_endline 
-                ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv
-                 [] newmetasenv_new);
-            (CicMetaSubst.apply_subst subst cic_proof_new),
-            newmetasenv_new,
-            (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new),
-            (CicMetaSubst.apply_subst subst new_ty),
-            newug
-(*            cic_proof,newmetasenv,proof_menv,oldty,oldug*)
+        let cic_proof,newmetasenv,proof_menv,ty, ug =
+          prerr_endline "type checking ... (old) ";
+          let _old_ty, _oldug = 
+            try 
+              CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph
+            with 
+              CicTypeChecker.TypeCheckerFailure s ->
+                prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!";
+                prerr_endline (Lazy.force s);
+                Cic.Implicit None, CicUniv.empty_ugraph
           in
-          prerr_endline "FINAL PROOF";
-          prerr_endline (CicPp.pp cic_proof names);
-          prerr_endline "ENDOFPROOFS";
-            
-          debug_print
-            (lazy
-               (Printf.sprintf
-                  "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
-                  (CicPp.pp type_of_goal names) (CicPp.pp ty names)
-                  (string_of_bool
-                     (fst (CicReduction.are_convertible
-                             context type_of_goal ty ug)))));
-          let real_proof =
-            ProofEngineReduction.replace
-              ~equality:equality_for_replace
-              ~what:[goal'] ~with_what:[cic_proof]
-              ~where:meta_proof
+          let cic_proof_new,new_ty,newmetasenv_new,newug = 
+            try
+              (*
+               prerr_endline "refining ... (new) ";
+               CicRefine.type_of_aux' 
+                newmetasenv_new context cic_proof_new ugraph
+              *)
+              let ty,ug = 
+                prerr_endline "typechecking ... (new) ";
+                CicTypeChecker.type_of_aux' 
+                  newmetasenv_new context cic_proof_new ugraph
+              in
+              cic_proof_new, ty, newmetasenv_new, ug
+            with
+            | CicTypeChecker.TypeCheckerFailure s ->
+                prerr_endline "THE PROOF DOESN'T TYPECHECK!!!";
+                prerr_endline (Lazy.force s);
+                assert false
+            | CicRefine.RefineFailure s 
+            | CicRefine.Uncertain s 
+            | CicRefine.AssertFailure s -> 
+                prerr_endline "FAILURE IN REFINE";
+                prerr_endline (Lazy.force s);
+                interactive_comparison context cic_proof_new cic_proof;
+                assert false
           in
-          debug_print
-            (lazy
-               (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
-                  (match uri with Some uri -> UriManager.string_of_uri uri
-                   | None -> "")
-                  (print_metasenv newmetasenv)
-                  (CicPp.pp real_proof [](* names *))
-                  (CicPp.pp term_to_prove names)));
-          ((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 cic_proof names));
-          raise (ProofEngineTypes.Fail
-                  (lazy "Found a proof, but it doesn't typecheck"))
+          if List.length newmetasenv_new <> 0 then
+            prerr_endline 
+              ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv
+               [] newmetasenv_new);
+          cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug
+          (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *)
+        in
+        prerr_endline "FINAL PROOF";
+        prerr_endline (CicPp.pp cic_proof names);
+        prerr_endline "ENDOFPROOFS";
+        (*  
+        debug_print
+          (lazy
+             (Printf.sprintf
+                "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
+                (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+                (string_of_bool
+                   (fst (CicReduction.are_convertible
+                           context type_of_goal ty ug)))));
+        *)
+        let real_proof =
+          ProofEngineReduction.replace
+            ~equality:equality_for_replace
+            ~what:[goal'] ~with_what:[cic_proof]
+            ~where:meta_proof
+        in
+        (*
+        debug_print
+          (lazy
+             (Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
+                (match uri with Some uri -> UriManager.string_of_uri uri
+                 | None -> "")
+                (print_metasenv newmetasenv)
+                (CicPp.pp real_proof [](* names *))
+                (CicPp.pp term_to_prove names)));
+        *)
+        let open_goals = List.map (fun (i,_,_) -> i) proof_menv in
+        (uri, newmetasenv, real_proof, term_to_prove), open_goals
       in
-      let tall = fs_time_info.build_all in
-      let tdemodulate = fs_time_info.demodulate in
-      let tsubsumption = fs_time_info.subsumption in
       if Utils.time then
         begin
+          let tall = fs_time_info.build_all in
+          let tdemodulate = fs_time_info.demodulate in
+          let tsubsumption = fs_time_info.subsumption in
           prerr_endline (
             (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
               (Printf.sprintf "\ntall: %.9f" tall) ^
               (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
               (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
               (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
-              (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
+              (Printf.sprintf "\nforward_simpl_times: %.9f" 
+                !forward_simpl_time) ^
               (Printf.sprintf "\nforward_simpl_new_times: %.9f" 
-                 !forward_simpl_new_time) ^
-              (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
+                !forward_simpl_new_time) ^
+              (Printf.sprintf "\nbackward_simpl_times: %.9f" 
+                !backward_simpl_time) ^
               (Printf.sprintf "\npassive_maintainance_time: %.9f" 
                  !passive_maintainance_time))
         end;
-      newstatus          
-  | _ ->
+      newstatus 
+  | ParamodulationSuccess None -> assert false
+  | ParamodulationFailure ->
       raise (ProofEngineTypes.Fail (lazy "NO proof found"))
 ;;