- added Ring tactic on reals

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 85e9b5ebca09a87820decebc68f8b4fd3484ba29..15cfdcd103813cbb0f5f71ba77c2794f19204785 100644 (file)
--- 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,8 @@ let htmlfooter =
  "</html>"
 ;;
 
+let prooffile = "/home/zack/dati/HELM/currentproof.gTopLevel"
+
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
 let htmlheader_and_content = ref htmlheader;;
@@ -55,6 +57,16 @@ 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 *)
 
@@ -151,11 +163,29 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 (*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 "/home/fguidi/innertypes") ;
+   Xml.pp xmlinnertypes (Some "/tmp/innertypes") ;
    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 *)
 
@@ -632,6 +662,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
 ;;
@@ -653,6 +686,7 @@ 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
 ;;
@@ -717,7 +751,8 @@ let qed rendering_window () =
 (*????
 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
 *)
-let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
+(* let dtdname = "/home/zack/dati/HELM/V7/dtd/cic.dtd";; *)
+let dtdname = "/public/helm-cvs/helm/dtd/cic.dtd";;
 
 let save rendering_window () =
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
@@ -738,10 +773,10 @@ 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 *)
@@ -758,7 +793,7 @@ 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 :=
@@ -772,7 +807,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 ->
@@ -1370,6 +1405,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
@@ -1391,6 +1429,9 @@ class rendering_window output proofw (label : GMisc.label) =
  let letinb =
   GButton.button ~label:"Let ... In"
    ~packing:(hbox3#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
  let clearbodyb =
@@ -1399,6 +1440,9 @@ class rendering_window output proofw (label : GMisc.label) =
  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>"
@@ -1441,6 +1485,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)) ;
@@ -1448,8 +1493,10 @@ 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(dumpb#connect#clicked dumpsequent);
   ignore(introsb#connect#clicked (intros self)) ;
   Logger.log_callback :=
    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
@@ -1471,8 +1518,10 @@ let initialize_everything () =
 
 let _ =
  CicCooking.init () ;
- MQueryGenerator.init () ;
+ if !usedb then MQueryGenerator.init () ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
+ if !usedb then MQueryGenerator.close ();
  MQueryGenerator.close ()
 ;;
+