* Many improvements (expecially in exceptions handling)

* The cases in which existential variables are now handled "correctly"
  have been increased. Neverthless, existential variables are still implemented
  in a completely wrong way.
* First commit after the commit of cic_unification.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 268d2846ee853b1613a7fa2e08d6d0ab584f5279..f6556ed8c58614589af187b497486ffc8e6c4cb4 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -165,50 +165,60 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 
 (* CALLBACKS *)
 
+exception RefreshSequentException of exn;;
+exception RefreshProofException of exn;;
+
 let refresh_proof (output : GMathView.math_view) =
- let uri,currentproof =
-  match !ProofEngine.proof with
-     None -> assert false
-   | Some (uri,metasenv,bo,ty) ->
-      uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
- in
- let
-  (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
- =
-  Cic2acic.acic_object_of_cic_object currentproof
- in
-  let mml = mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types in
-   output#load_tree mml ;
-   current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ try
+  let uri,currentproof =
+   match !ProofEngine.proof with
+      None -> assert false
+    | Some (uri,metasenv,bo,ty) ->
+       uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
+  in
+   let
+    (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
+   =
+    Cic2acic.acic_object_of_cic_object currentproof
+   in
+    let mml =
+     mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
+    in
+     output#load_tree mml ;
+     current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+ with
+  e -> raise (RefreshProofException e)
 ;;
 
 let refresh_sequent (proofw : GMathView.math_view) =
- match !ProofEngine.goal with
-    None -> proofw#unload
-  | Some (_,currentsequent) ->
-     let metasenv =
-      match !ProofEngine.proof with
-         None -> assert false
-       | Some (_,metasenv,_,_) -> metasenv
-     in
-      let sequent_gdome,ids_to_terms,ids_to_father_ids =
-       SequentPp.XmlPp.print_sequent metasenv currentsequent
+ try
+  match !ProofEngine.goal with
+     None -> proofw#unload
+   | Some (_,currentsequent) ->
+      let metasenv =
+       match !ProofEngine.proof with
+          None -> assert false
+        | Some (_,metasenv,_,_) -> metasenv
       in
-       let sequent_doc =
-        Xml2Gdome.document_of_xml domImpl sequent_gdome
+       let sequent_gdome,ids_to_terms,ids_to_father_ids =
+        SequentPp.XmlPp.print_sequent metasenv currentsequent
        in
-        let sequent_mml =
-         applyStylesheets sequent_doc sequent_styles sequent_args
+        let sequent_doc =
+         Xml2Gdome.document_of_xml domImpl sequent_gdome
         in
-         proofw#load_tree ~dom:sequent_mml ;
-         current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+         let sequent_mml =
+          applyStylesheets sequent_doc sequent_styles sequent_args
+         in
+          proofw#load_tree ~dom:sequent_mml ;
+          current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
+ with
+  e -> raise (RefreshSequentException e)
+;;
+
 (*
 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
  ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
-ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
- ~name:"/public/sacerdot/guruguru2" ~indent:true ())
 *)
-;;
 
 let mml_of_cic_term term =
  let context =
@@ -256,11 +266,26 @@ let call_tactic tactic rendering_window () =
     refresh_sequent proofw ;
     refresh_proof output
    with
-    e ->
-     output_html outputhtml
-      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
-     ProofEngine.proof := savedproof ;
-     ProofEngine.goal := savedgoal ;
+      RefreshSequentException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
+       refresh_sequent proofw
+    | RefreshProofException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
+       refresh_sequent proofw ;
+       refresh_proof output
+    | e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+       ProofEngine.proof := savedproof ;
+       ProofEngine.goal := savedgoal ;
   end
 ;;
 
@@ -304,11 +329,33 @@ let call_tactic_with_input tactic rendering_window () =
     with
        CicTextualParser0.Eof ->
         inputt#delete_text 0 inputlen
+     | RefreshSequentException e ->
+        output_html outputhtml
+         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+        ProofEngine.proof := savedproof ;
+        ProofEngine.goal := savedgoal ;
+        refresh_sequent proofw
+     | RefreshProofException e ->
+        output_html outputhtml
+         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+prerr_endline "PROVA CHE FA SOLLEVARE UN'ECCEZIONE:" ; flush stderr ;
+begin
+match !ProofEngine.proof with Some (_,metasenv,bo,_) ->
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^
+CicPp.ppterm ty) ; flush stderr) metasenv ;
+prerr_endline ("PROOF: " ^ CicPp.ppterm bo) ; flush stderr ;
+end ;
+        ProofEngine.proof := savedproof ;
+        ProofEngine.goal := savedgoal ;
+        refresh_sequent proofw ;
+        refresh_proof output
      | e ->
         output_html outputhtml
-         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>");
+         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
         ProofEngine.proof := savedproof ;
-        ProofEngine.goal := savedgoal
+        ProofEngine.goal := savedgoal ;
 ;;
 
 let call_tactic_with_goal_input tactic rendering_window () =
@@ -338,9 +385,26 @@ let call_tactic_with_goal_input tactic rendering_window () =
                refresh_proof rendering_window#output
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
-          e ->
-           output_html outputhtml
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+            RefreshSequentException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw
+          | RefreshProofException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw ;
+             refresh_proof output
+          | e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
         end
    | None ->
       output_html outputhtml
@@ -409,9 +473,26 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
                  end
            | None -> assert false (* "ERROR: No current term!!!" *)
          with
-          e ->
-           output_html outputhtml
-            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+            RefreshSequentException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw
+          | RefreshProofException e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+               "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
+             refresh_sequent proofw ;
+             refresh_proof output
+          | e ->
+             output_html outputhtml
+              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+             ProofEngine.proof := savedproof ;
+             ProofEngine.goal := savedgoal ;
         end
    | None ->
       output_html outputhtml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 5f64134b50dc6db1995f091f5ac3f6c335dcfce2..ac828a9598c794ca832edbfbc7a0c76e41b86d72 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -28,7 +28,21 @@ let cic_context_of_named_context =
   )
 ;;
 
-let refine_meta_with_brand_new_metasenv meta term newmetasenv =
+(* refine_meta_with_brand_new_metasenv meta term apply_subst_replacing    *)
+(*   newmetasenv                                                          *)
+(* This (heavy) function must be called when a tactic can instantiate old *)
+(* metavariables (i.e. existential variables). It substitues the metasenv *)
+(* of the proof with the result of removing [meta] from the domain of     *)
+(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
+(* in the current proof. Finally it applies [apply_subst_replacing] to    *)
+(*  current proof.                                                        *)
+(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
+(*CSC: ci ripasso sopra apply_subst!!!                                     *)
+(*CSC: Inoltre, potrebbe essere questa funzione ad applicare apply_subst a *)
+(*CSC: newmetasenv!!!                                                      *)
+let refine_meta_with_brand_new_metasenv meta term apply_subst_replacing
+ newmetasenv
+=
  let (uri,bo,ty) =
   match !proof with
      None -> assert false
@@ -37,7 +51,7 @@ let refine_meta_with_brand_new_metasenv meta term newmetasenv =
   let subst_in t =
    ProofEngineReduction.replace ~what:(Cic.Meta meta) ~with_what:term ~where:t
   in
-   let bo' = subst_in bo in
+   let bo' = apply_subst_replacing (subst_in bo) in
    let metasenv' = List.remove_assoc meta newmetasenv in
     proof := Some (uri,metasenv',bo',ty)
 ;;
@@ -236,9 +250,9 @@ let new_metasenv_for_apply ty =
 ;;
 
 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
-let classify_metas newmeta in_subst_domain apply_subst =
- List.fold_left
-  (fun (old_uninst,new_uninst) (i,ty) ->
+let classify_metas newmeta in_subst_domain apply_subst metasenv =
+ List.fold_right
+  (fun (i,ty) (old_uninst,new_uninst) ->
     if in_subst_domain i then
      old_uninst,new_uninst
     else
@@ -247,7 +261,7 @@ let classify_metas newmeta in_subst_domain apply_subst =
        ((i,ty')::old_uninst),new_uninst
       else
        old_uninst,((i,ty')::new_uninst)
-  ) ([],[])
+  ) metasenv ([],[])
 ;;
 
 (* The term bo must be closed in the current context *)
@@ -276,6 +290,14 @@ let apply term =
        let subst = CicUnification.fo_unif newmetasenv ciccontext consthead ty in
         let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
         let apply_subst = CicUnification.apply_subst subst in
+(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
+        let apply_subst_replacing t =
+         List.fold_left
+          (fun t (i,bo) ->
+            ProofEngineReduction.replace
+             ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+          t subst
+        in
          let old_uninstantiatedmetas,new_uninstantiatedmetas =
           classify_metas newmeta in_subst_domain apply_subst newmetasenv
          in
@@ -289,11 +311,18 @@ let apply term =
             in
             Cic.Appl (term::arguments)
          in
-          refine_meta_with_brand_new_metasenv metano bo'
+          refine_meta_with_brand_new_metasenv metano bo' apply_subst_replacing
             (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
+prerr_endline "QUI4" ; flush stderr ; (
           match new_uninstantiatedmetas with
              [] -> goal := None
            | (i,ty)::_ -> goal := Some (i,(context,ty))
+) ;
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (new_uninstantiatedmetas@old_uninstantiatedmetas)
+; prerr_endline "FATTO" ; flush stderr ;
+List.iter (function (i,ty) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm ty) ; flush stderr) (match !proof with Some (_,m,_,_) -> m) ;
+prerr_endline ("PROVA: " ^ CicPp.ppterm (match !proof with Some (_,_,b,_) -> b))
+; prerr_endline "FATTO2" ; flush stderr
 ;;
 
 let eta_expand metasenv ciccontext t arg =
@@ -449,11 +478,25 @@ prerr_endline "unwind"; flush stderr;
                (* When unwinding the META that corresponds to the elimination *)
                (* predicate (which is emeta), we must also perform one-step   *)
                (* beta-reduction.                                             *)
-               let apply_subst =
-                function t ->
-                 let t' = CicUnification.apply_subst subst1 t in
-                  CicUnification.apply_subst_reducing
-                   subst2 (Some (emeta,List.length fargs)) t'
+               let apply_subst t =
+                let t' = CicUnification.apply_subst subst1 t in
+                 CicUnification.apply_subst_reducing
+                  subst2 (Some (emeta,List.length fargs)) t'
+               in
+(*CSC: estremamente inefficiente: fare una passata sola per rimpiazzarle tutte*)
+               let apply_subst_replacing t =
+                let t' =
+                 List.fold_left
+                  (fun t (i,bo) ->
+                    ProofEngineReduction.replace
+                     ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+                  t subst1
+                in
+                 List.fold_left
+                  (fun t (i,bo) ->
+                    ProofEngineReduction.replace
+                     ~what:(Cic.Meta i) ~with_what:bo ~where:t)
+                  t' subst2
                in
                 let newmetasenv' =
                  List.map (function (i,ty) -> i, apply_subst ty) newmetasenv
@@ -469,6 +512,7 @@ prerr_endline "unwind"; flush stderr;
 prerr_endline ("BODY': " ^ CicPp.ppterm bo') ; flush stdout ;
 List.iter (function (i,t) -> prerr_endline ("?" ^ string_of_int i ^ ": " ^ CicPp.ppterm t)) (new_uninstantiatedmetas@old_uninstantiatedmetas) ; flush stderr ;
                    refine_meta_with_brand_new_metasenv metano bo'
+                     apply_subst_replacing
                      (new_uninstantiatedmetas@old_uninstantiatedmetas) ;
                    match new_uninstantiatedmetas with
                       [] -> goal := None