X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=563c8818670507e8844a183e9a3b184065319127;hb=8f89cdd08d9ee0a243cf84201bf42e5503759ee3;hp=789a65ba5c87330d11d00c027ea602f733fb9cac;hpb=bea50d8a7fdf4063d8bf42d2983734190457e030;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 789a65ba5..563c88186 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2002, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -47,6 +47,10 @@ let htmlfooter =
  "</html>"
 ;;
 
+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) *)
 
 let htmlheader_and_content = ref htmlheader;;
@@ -55,6 +59,17 @@ let current_cic_infos = ref None;;
 let current_goal_infos = ref None;;
 let current_scratch_infos = ref None;;
 
+(* COMMAND LINE OPTIONS *)
+
+let usedb = ref true
+
+let argspec =
+  [
+    "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
+  ]
+in
+Arg.parse argspec ignore ""
+
 
 (* MISC FUNCTIONS *)
 
@@ -141,17 +156,17 @@ 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 "/public/sacerdot/innertypes") ;
+   Xml.pp xmlinnertypes (Some innertypesfile) ;
    let output = applyStylesheets input mml_styles mml_args in
     output
 ;;
@@ -171,7 +186,8 @@ let refresh_proof (output : GMathView.math_view) =
        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)
+    (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
+     ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
    =
     Cic2acic.acic_object_of_cic_object currentproof
    in
@@ -179,7 +195,8 @@ let refresh_proof (output : GMathView.math_view) =
      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)
+     current_cic_infos :=
+      Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
  with
   e ->
  match !ProofEngine.proof with
@@ -200,7 +217,7 @@ let refresh_sequent (proofw : GMathView.math_view) =
         | Some (_,metasenv,_,_) -> metasenv
       in
       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
-       let sequent_gdome,ids_to_terms,ids_to_father_ids =
+       let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
         SequentPp.XmlPp.print_sequent metasenv currentsequent
        in
         let sequent_doc =
@@ -210,7 +227,8 @@ let refresh_sequent (proofw : GMathView.math_view) =
           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)
+          current_goal_infos :=
+           Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  with
   e ->
 let metano =
@@ -248,7 +266,7 @@ let mml_of_cic_term metano term =
       in
        canonical_context
  in
-   let sequent_gdome,ids_to_terms,ids_to_father_ids =
+   let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
    in
     let sequent_doc =
@@ -257,7 +275,8 @@ let mml_of_cic_term metano term =
      let res =
       applyStylesheets sequent_doc sequent_styles sequent_args ;
      in
-      current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
+      current_scratch_infos :=
+       Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
       res
 ;;
 
@@ -322,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
@@ -344,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
@@ -397,7 +418,7 @@ let call_tactic_with_goal_input tactic rendering_window () =
         begin
          try
           match !current_goal_infos with
-             Some (ids_to_terms, ids_to_father_ids) ->
+             Some (ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
                tactic (Hashtbl.find ids_to_terms id) ;
                refresh_sequent rendering_window#proofw ;
@@ -451,7 +472,7 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
         begin
          try
           match !current_goal_infos with
-             Some (ids_to_terms, ids_to_father_ids) ->
+             Some (ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
                (* Let's parse the input *)
                let inputlen = inputt#length in
@@ -462,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
@@ -485,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 ;
@@ -547,7 +569,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
          try
           match !current_scratch_infos with
              (* term is the whole goal in the scratch_area *)
-             Some (term,ids_to_terms, ids_to_father_ids) ->
+             Some (term,ids_to_terms, ids_to_father_ids,_) ->
               let id = xpath in
                let expr = tactic term (Hashtbl.find ids_to_terms id) in
                 let mml = mml_of_cic_term 111 expr in
@@ -564,6 +586,60 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
        ("<h1 color=\"red\">No term selected</h1>")
 ;;
 
+let call_tactic_with_hypothesis_input tactic rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+  let proofw = (rendering_window#proofw : GMathView.math_view) in
+  let output = (rendering_window#output : GMathView.math_view) in
+  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+  let savedproof = !ProofEngine.proof in
+  let savedgoal  = !ProofEngine.goal in
+   match proofw#get_selection with
+     Some node ->
+      let xpath =
+       ((node : Gdome.element)#getAttributeNS
+         ~namespaceURI:helmns
+         ~localName:(G.domString "xref"))#to_string
+      in
+       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
+       else
+        begin
+         try
+          match !current_goal_infos with
+             Some (_,_,ids_to_hypotheses) ->
+              let id = xpath in
+               tactic (Hashtbl.find ids_to_hypotheses id) ;
+               refresh_sequent rendering_window#proofw ;
+               refresh_proof rendering_window#output
+           | None -> assert false (* "ERROR: No current term!!!" *)
+         with
+            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
+       ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+
 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
 let exact rendering_window =
  call_tactic_with_input ProofEngine.exact rendering_window
@@ -574,6 +650,9 @@ let apply rendering_window =
 let elimintrossimpl rendering_window =
  call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
 ;;
+let elimtype rendering_window =
+ call_tactic_with_input ProofEngine.elim_type rendering_window
+;;
 let whd rendering_window =
  call_tactic_with_goal_input ProofEngine.whd rendering_window
 ;;
@@ -595,6 +674,13 @@ let change rendering_window =
 let letin rendering_window =
  call_tactic_with_input ProofEngine.letin rendering_window
 ;;
+let ring rendering_window = call_tactic ProofEngine.ring rendering_window;;
+let clearbody rendering_window =
+ call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
+;;
+let clear rendering_window =
+ call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
+;;
 
 
 let whd_in_scratch scratch_window =
@@ -632,7 +718,7 @@ let qed rendering_window () =
        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
         let
          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
-          ids_to_inner_types)
+          ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
         =
          Cic2acic.acic_object_of_cic_object proof
         in
@@ -640,7 +726,10 @@ let qed rendering_window () =
           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
          in
           (rendering_window#output : GMathView.math_view)#load_tree mml ;
-          current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
+          current_cic_infos :=
+           Some
+            (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+             ids_to_hypotheses)
       end
      else
       raise WrongProof
@@ -660,10 +749,10 @@ let save rendering_window () =
       let currentproof =
        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
       in
-       let (acurrentproof,_,_,ids_to_inner_sorts,_) =
+       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
@@ -671,10 +760,18 @@ let save rendering_window () =
              xml
           >]
          in
-          Xml.pp ~quiet:true xml' (Some "/public/sacerdot/currentproof") ;
+          Xml.pp ~quiet:true xml' (Some prooffile) ;
           output_html outputhtml
            ("<h1 color=\"Green\">Current proof saved to " ^
-             "/public/sacerdot/currentproof</h1>")
+            prooffile ^ "</h1>")
+;;
+
+(* Used to typecheck the loaded proofs *)
+let typecheck_loaded_proof metasenv bo ty =
+ let module T = CicTypeChecker in
+  (*CSC: bisogna controllare anche il metasenv!!! *)
+  ignore (T.type_of_aux' metasenv [] ty) ;
+  ignore (T.type_of_aux' metasenv [] bo)
 ;;
 
 let load rendering_window () =
@@ -683,8 +780,9 @@ let load rendering_window () =
  let proofw = (rendering_window#proofw : GMathView.math_view) in
   try
    let uri = UriManager.uri_of_string "cic:/dummy.con" in
-    match CicParser.obj_of_xml "/public/sacerdot/currentproof" uri with
+    match CicParser.obj_of_xml prooffile uri with
        Cic.CurrentProof (_,metasenv,bo,ty) ->
+        typecheck_loaded_proof metasenv bo ty ;
         ProofEngine.proof :=
          Some (uri, metasenv, bo, ty) ;
         ProofEngine.goal :=
@@ -696,7 +794,7 @@ let load rendering_window () =
         refresh_sequent proofw ;
          output_html outputhtml
           ("<h1 color=\"Green\">Current proof loaded from " ^
-            "/public/sacerdot/currentproof</h1>")
+            prooffile ^ "</h1>")
      | _ -> assert false
   with
      RefreshSequentException e ->
@@ -731,7 +829,7 @@ let proveit rendering_window () =
        begin
         try
          match !current_cic_infos with
-            Some (ids_to_terms, ids_to_father_ids) ->
+            Some (ids_to_terms, ids_to_father_ids, _, _) ->
              let id = xpath in
               L.to_sequent id ids_to_terms ids_to_father_ids ;
               refresh_proof rendering_window#output ;
@@ -772,7 +870,7 @@ let focus rendering_window () =
        begin
         try
          match !current_cic_infos with
-            Some (ids_to_terms, ids_to_father_ids) ->
+            Some (ids_to_terms, ids_to_father_ids, _, _) ->
              let id = xpath in
               L.focus id ids_to_terms ids_to_father_ids ;
               refresh_sequent rendering_window#proofw
@@ -963,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
@@ -996,7 +1094,7 @@ let locate rendering_window () =
            | [] -> ""
            | head :: tail ->
 	       inputt#delete_text 0 inputlen;
-	       Mquery.locate head 
+	       MQueryGenerator.locate head 
      with
         e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
   )
@@ -1017,12 +1115,13 @@ let backward rendering_window () =
        match !ProofEngine.goal with
           | None -> ""
           | Some metano ->
-             let (_,_,ty) =
+             let (_, ey ,ty) =
               List.find (function (m,_,_) -> m=metano) metasenv
              in
-              Mquery.backward ty level
+              MQueryGenerator.backward metasenv ey ty level
        in 
    output_html outputhtml result
+;;
       
 let choose_selection
      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
@@ -1294,6 +1393,9 @@ class rendering_window output proofw (label : GMisc.label) =
  let elimintrossimplb =
   GButton.button ~label:"ElimIntrosSimpl"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let elimtypeb =
+  GButton.button ~label:"ElimType"
+   ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
  let whdb =
   GButton.button ~label:"Whd"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1312,9 +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:(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 outputhtml =
   GHtml.xmhtml
    ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -1357,6 +1470,7 @@ object(self)
   ignore(exactb#connect#clicked (exact self)) ;
   ignore(applyb#connect#clicked (apply self)) ;
   ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
+  ignore(elimtypeb#connect#clicked (elimtype self)) ;
   ignore(whdb#connect#clicked (whd self)) ;
   ignore(reduceb#connect#clicked (reduce self)) ;
   ignore(simplb#connect#clicked (simpl self)) ;
@@ -1364,6 +1478,9 @@ object(self)
   ignore(cutb#connect#clicked (cut self)) ;
   ignore(changeb#connect#clicked (change self)) ;
   ignore(letinb#connect#clicked (letin self)) ;
+  ignore(ringb#connect#clicked (ring self)) ;
+  ignore(clearbodyb#connect#clicked (clearbody self)) ;
+  ignore(clearb#connect#clicked (clear self)) ;
   ignore(introsb#connect#clicked (intros self)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
@@ -1385,8 +1502,8 @@ let initialize_everything () =
 
 let _ =
  CicCooking.init () ;
- Mquery.init () ;
+ if !usedb then MQueryGenerator.init () ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- Mquery.close ()
+ if !usedb then MQueryGenerator.close ();
 ;;