Updated to use the new parser that creates (stacks of) existential variables

when an implicit arguments is found.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 15cfdcd103813cbb0f5f71ba77c2794f19204785..563c8818670507e8844a183e9a3b184065319127 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,7 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/home/zack/dati/HELM/currentproof.gTopLevel"
+let prooffile = "/public/sacerdot/currentproof";;
+(*CSC: the getter should handle the innertypes, not the FS *)
+let innertypesfile = "/public/sacerdot/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -68,6 +70,7 @@ let argspec =
 in
 Arg.parse argspec ignore ""
 
+
 (* MISC FUNCTIONS *)
 
 let domImpl = Gdome.domImplementation ();;
@@ -153,39 +156,21 @@ let applyStylesheets input styles args =
 
 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
  let xml =
-  Cic2Xml.print_object uri ids_to_inner_sorts annobj 
+  Cic2Xml.print_object uri ~ids_to_inner_sorts annobj 
  in
  let xmlinnertypes =
-  Cic2Xml.print_inner_types uri ids_to_inner_sorts
-   ids_to_inner_types
+  Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
+   ~ids_to_inner_types
  in
   let input = Xml2Gdome.document_of_xml domImpl xml in
 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 (*CSC: local.                                                              *)
-   Xml.pp xmlinnertypes (Some "/tmp/innertypes") ;
+   Xml.pp xmlinnertypes (Some innertypesfile) ;
    let output = applyStylesheets input mml_styles mml_args in
     output
 ;;
 
-  (* pretty print on standard output the current sequent *)
-let dumpsequent () =
-  let metasenv =
-    match !ProofEngine.proof with
-    | None -> assert false
-    | Some (_, metasenv, _, _) -> metasenv
-  in
-  let seq =
-    match !ProofEngine.goal with
-    | None -> assert false
-    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
-  in
-  print_string (
-    "<current_seq>\n" ^
-    (SequentPp.TextualPp.print_sequent seq) ^
-    "\n</current_seq>");
-  print_newline ()
-;;
 
 (* CALLBACKS *)
 
@@ -356,10 +341,10 @@ let call_tactic_with_input tactic rendering_window () =
        None -> assert false
      | Some (curi,_,_,_) -> curi
    in
-   let metasenv =
+   let uri,metasenv,bo,ty =
     match !ProofEngine.proof with
        None -> assert false
-     | Some (_,metasenv,_,_) -> metasenv
+     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
    in
    let context =
     List.map
@@ -378,10 +363,12 @@ let call_tactic_with_input tactic rendering_window () =
     try
      while true do
       match
-       CicTextualParserContext.main curi context CicTextualLexer.token lexbuf
+       CicTextualParserContext.main
+        curi context metasenv CicTextualLexer.token lexbuf
       with
          None -> ()
-       | Some expr ->
+       | Some (metasenv',expr) ->
+          ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
           tactic expr ;
           refresh_sequent proofw ;
           refresh_proof output
@@ -496,10 +483,10 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
                     None -> assert false
                   | Some (curi,_,_,_) -> curi
                 in
-                let metasenv =
+                let uri,metasenv,bo,ty =
                  match !ProofEngine.proof with
                     None -> assert false
-                  | Some (_,metasenv,_,_) -> metasenv
+                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
                 in
                 let context =
                  List.map
@@ -519,11 +506,12 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
                   try
                    while true do
                     match
-                     CicTextualParserContext.main curi context
+                     CicTextualParserContext.main curi context metasenv
                       CicTextualLexer.token lexbuf
                     with
                        None -> ()
-                     | Some expr ->
+                     | Some (metasenv',expr) ->
+                        ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
                         tactic ~goal_input:(Hashtbl.find ids_to_terms id)
                          ~input:expr ;
                         refresh_sequent proofw ;
@@ -751,8 +739,7 @@ let qed rendering_window () =
 (*????
 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
 *)
-(* let dtdname = "/home/zack/dati/HELM/V7/dtd/cic.dtd";; *)
-let dtdname = "/public/helm-cvs/helm/dtd/cic.dtd";;
+let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
 
 let save rendering_window () =
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
@@ -765,7 +752,7 @@ let save rendering_window () =
        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
         Cic2acic.acic_object_of_cic_object currentproof
        in
-        let xml = Cic2Xml.print_object uri ids_to_inner_sorts acurrentproof in
+        let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
          let xml' =
           [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
              Xml.xml_cdata
@@ -1074,13 +1061,13 @@ let check rendering_window scratch_window () =
      while true do
       (* Execute the actions *)
       match
-       CicTextualParserContext.main curi names_context CicTextualLexer.token
-        lexbuf
+       CicTextualParserContext.main curi names_context metasenv
+        CicTextualLexer.token lexbuf
       with
          None -> ()
-       | Some expr ->
+       | Some (metasenv',expr) ->
           try
-           let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
+           let ty  = CicTypeChecker.type_of_aux' metasenv' context expr in
             let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
              scratch_window#show () ;
              scratch_window#mmlwidget#load_tree ~dom:mml
@@ -1134,6 +1121,7 @@ let backward rendering_window () =
               MQueryGenerator.backward metasenv ey ty level
        in 
    output_html outputhtml result
+;;
       
 let choose_selection
      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
@@ -1426,23 +1414,20 @@ class rendering_window output proofw (label : GMisc.label) =
  let changeb =
   GButton.button ~label:"Change"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let hbox4 =
+  GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
  let letinb =
   GButton.button ~label:"Let ... In"
-   ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let ringb =
   GButton.button ~label:"Ring"
-   ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let hbox4 =
-  GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let clearbodyb =
   GButton.button ~label:"ClearBody"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let clearb =
   GButton.button ~label:"Clear"
    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
- let dumpb =
-  GButton.button ~label:"Dump"
-   ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
  let outputhtml =
   GHtml.xmhtml
    ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -1496,7 +1481,6 @@ object(self)
   ignore(ringb#connect#clicked (ring self)) ;
   ignore(clearbodyb#connect#clicked (clearbody self)) ;
   ignore(clearb#connect#clicked (clear self)) ;
-  ignore(dumpb#connect#clicked dumpsequent);
   ignore(introsb#connect#clicked (intros self)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
@@ -1522,6 +1506,4 @@ let _ =
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  if !usedb then MQueryGenerator.close ();
- MQueryGenerator.close ()
 ;;
-