added some code to print the praamodulation proofs with a graph

[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 d9472601c958c96b62526c9af50c11e1ac5a6f9b..ff58512ea9d1f47c429d6f0f6b412fc5c96b4165 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -1280,15 +1280,24 @@ let fix_proof metasenv context all_implicits p =
          let metasenv,s = aux metasenv n s in
          let metasenv,t = aux metasenv (n+1) t in
            metasenv,Cic.LetIn(name,s,t)              
+      | Cic.Const(uri,ens) -> 
+         let metasenv,ens =
+           List.fold_right 
+             (fun (v,a) (metasenv,ens) -> 
+                let metasenv,a' = aux metasenv n a in
+                  metasenv,(v,a')::ens)
+             ens (metasenv,[])
+         in
+         metasenv,Cic.Const(uri,ens)
       | t -> metasenv,t
   in
   aux metasenv 0 p 
 ;;
 
-let fix_metasenv metasenv context =
+let fix_metasenv metasenv =
   List.fold_left 
     (fun m (i,c,t) ->
-       let m,t = fix_proof m context false t in
+       let m,t = fix_proof m c false t in
        let m = List.filter (fun (j,_,_) -> j<>i) m in
         (i,c,t)::m)
     metasenv metasenv
@@ -1310,7 +1319,7 @@ let build_proof
   if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
   else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let names = Utils.names_of_context context in
@@ -1334,28 +1343,37 @@ let build_proof
         eq_uri goalproof initial type_of_goal side_effects
         context proof_menv  
   in
+(*   Equality.draw_proof bag names goalproof newproof subsumption_id; *)
   let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
-  let real_menv =  fix_metasenv (proof_menv@metasenv) context in
+  let real_menv =  fix_metasenv (proof_menv@metasenv) in
   let real_menv,goal_proof = 
     fix_proof real_menv context false goal_proof in
 (*
   let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
     (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
 *)
+  let pp_error goal_proof names error exn =
+    prerr_endline "THE PROOF DOES NOT TYPECHECK! <begin>";
+    prerr_endline (CicPp.pp goal_proof names); 
+    prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+    prerr_endline error;
+    prerr_endline "THE PROOF DOES NOT TYPECHECK! <end>";
+    raise exn
+  in
   let goal_proof,goal_ty,real_menv,_ = 
     (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
     try
+            prerr_endline (CicPp.ppterm goal_proof);
       CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
     with 
-      | CicUtil.Meta_not_found _ 
-      | CicRefine.RefineFailure _ 
-      | CicRefine.Uncertain _ 
-      | CicRefine.AssertFailure _
+      | CicRefine.RefineFailure s 
+      | CicRefine.Uncertain s 
+      | CicRefine.AssertFailure s as exn -> 
+          pp_error goal_proof names (Lazy.force s) exn
+      | CicUtil.Meta_not_found i as exn ->
+          pp_error goal_proof names ("META NOT FOUND: "^string_of_int i) exn
       | Invalid_argument "list_fold_left2" as exn ->
-          prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-          prerr_endline (CicPp.pp goal_proof names); 
-          prerr_endline "THE PROOF DOES NOT TYPECHECK!";
-          raise exn
+          pp_error goal_proof names "Invalid_argument: list_fold_left2" exn 
   in     
   let subst_side_effects,real_menv,_ = 
     try
@@ -1522,16 +1540,17 @@ let build_proof
 let pump_actives context bag maxm active passive saturation_steps max_time =
   reset_refs();
   maxmeta := maxm;
+(*
   let max_l l = 
     List.fold_left 
      (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
       List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
      0 l in
-  let active_l = fst active in
-  let passive_l = fst passive in
-  let ma = max_l active_l in
-  let mp = max_l passive_l in
-  assert (maxm > max ma mp);
+*)
+(*   let active_l = fst active in *)
+(*   let passive_l = fst passive in *)
+(*   let ma = max_l active_l in *)
+(*   let mp = max_l passive_l in *)
   match LibraryObjects.eq_URI () with
     | None -> active, passive, !maxmeta
     | Some eq_uri -> 
@@ -1549,7 +1568,7 @@ let pump_actives context bag maxm active passive saturation_steps max_time =
 let all_subsumed bag maxm status active passive =
   maxmeta := maxm;
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let env = metasenv,context,CicUniv.empty_ugraph in
   let cleaned_goal = Utils.remove_local_context type_of_goal in
@@ -1583,19 +1602,20 @@ let given_clause
 =
   reset_refs();
   maxmeta := maxm;
+  let active_l = fst active in
+(*
   let max_l l = 
     List.fold_left 
      (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
       List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
      0 l
   in
-  let active_l = fst active in
   let passive_l = fst passive in
   let ma = max_l active_l in
   let mp = max_l passive_l in
-  assert (maxm > max ma mp);
+*)
   let proof, goalno = status in
-  let uri, metasenv, meta_proof, term_to_prove = proof in
+  let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
   let cleaned_goal = Utils.remove_local_context type_of_goal in