X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=1d5650b1ca20670fdad520c77412c6a1bd924842;hb=ee35bf33520d92753899985329cc4bfee141b808;hp=47c416d8b60b9ad472098d883f4cacf2f2026345;hpb=06e9498bf967323fe12d6383ec7b279a4546a06c;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 47c416d8b..1d5650b1c 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -151,7 +151,7 @@ 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 "/public/fguidi/innertypes") ;
+   Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
    let output = applyStylesheets input mml_styles mml_args in
     output
 ;;
@@ -181,19 +181,25 @@ let refresh_proof (output : GMathView.math_view) =
      output#load_tree mml ;
      current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
  with
-  e -> raise (RefreshProofException e)
+  e ->
+ match !ProofEngine.proof with
+    None -> assert false
+  | Some (uri,metasenv,bo,ty) ->
+prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ;
+   raise (RefreshProofException e)
 ;;
 
 let refresh_sequent (proofw : GMathView.math_view) =
  try
   match !ProofEngine.goal with
      None -> proofw#unload
-   | Some (_,currentsequent) ->
+   | Some metano ->
       let metasenv =
        match !ProofEngine.proof with
           None -> assert false
         | Some (_,metasenv,_,_) -> metasenv
       in
+      let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
        let sequent_gdome,ids_to_terms,ids_to_father_ids =
         SequentPp.XmlPp.print_sequent metasenv currentsequent
        in
@@ -206,7 +212,20 @@ let refresh_sequent (proofw : GMathView.math_view) =
           proofw#load_tree ~dom:sequent_mml ;
           current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
  with
-  e -> raise (RefreshSequentException e)
+  e ->
+let metano =
+  match !ProofEngine.goal with
+     None -> assert false
+   | Some m -> m
+in
+let metasenv =
+ match !ProofEngine.proof with
+    None -> assert false
+  | Some (_,metasenv,_,_) -> metasenv
+in
+let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
+prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
+   raise (RefreshSequentException e)
 ;;
 
 (*
@@ -214,19 +233,23 @@ ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
  ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
 *)
 
-let mml_of_cic_term term =
+let mml_of_cic_term metano term =
+ let metasenv =
+  match !ProofEngine.proof with
+     None -> []
+   | Some (_,metasenv,_,_) -> metasenv
+ in
  let context =
   match !ProofEngine.goal with
      None -> []
-   | Some (_,(context,_)) -> context
+   | Some metano ->
+      let (_,canonical_context,_) =
+       List.find (function (m,_,_) -> m=metano) metasenv
+      in
+       canonical_context
  in
-  let metasenv =
-   match !ProofEngine.proof with
-      None -> []
-    | Some (_,metasenv,_,_) -> metasenv
-  in
    let sequent_gdome,ids_to_terms,ids_to_father_ids =
-    SequentPp.XmlPp.print_sequent metasenv (context,term)
+    SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
    in
     let sequent_doc =
      Xml2Gdome.document_of_xml domImpl sequent_gdome
@@ -299,14 +322,23 @@ let call_tactic_with_input tactic rendering_window () =
        None -> assert false
      | Some (curi,_,_,_) -> curi
    in
+   let metasenv =
+    match !ProofEngine.proof with
+       None -> assert false
+     | Some (_,metasenv,_,_) -> metasenv
+   in
    let context =
     List.map
      (function
-         ProofEngine.Definition (n,_)
-       | ProofEngine.Declaration (n,_) -> n)
+         Some (n,_) -> Some n
+       | None -> None)
      (match !ProofEngine.goal with
          None -> assert false
-       | Some (_,(ctx,_)) -> ctx
+       | Some metano ->
+          let (_,canonical_context,_) =
+           List.find (function (m,_,_) -> m=metano) metasenv
+          in
+           canonical_context
      )
    in
     try
@@ -430,14 +462,23 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
                     None -> assert false
                   | Some (curi,_,_,_) -> curi
                 in
+                let metasenv =
+                 match !ProofEngine.proof with
+                    None -> assert false
+                  | Some (_,metasenv,_,_) -> metasenv
+                in
                 let context =
                  List.map
                   (function
-                      ProofEngine.Definition (n,_)
-                    | ProofEngine.Declaration (n,_) -> n)
+                      Some (n,_) -> Some n
+                    | None -> None)
                   (match !ProofEngine.goal with
                       None -> assert false
-                    | Some (_,(ctx,_)) -> ctx
+                    | Some metano ->
+                       let (_,canonical_context,_) =
+                        List.find (function (m,_,_) -> m=metano) metasenv
+                       in
+                        canonical_context
                   )
                 in
                  begin
@@ -509,7 +550,7 @@ let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
              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 expr in
+                let mml = mml_of_cic_term 111 expr in
                  scratch_window#show () ;
                  scratch_window#mmlwidget#load_tree ~dom:mml
            | None -> assert false (* "ERROR: No current term!!!" *)
@@ -530,8 +571,8 @@ let exact rendering_window =
 let apply rendering_window =
  call_tactic_with_input ProofEngine.apply rendering_window
 ;;
-let elimintros rendering_window =
- call_tactic_with_input ProofEngine.elim_intros rendering_window
+let elimintrossimpl rendering_window =
+ call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
 ;;
 let whd rendering_window =
  call_tactic_with_goal_input ProofEngine.whd rendering_window
@@ -578,7 +619,7 @@ let simpl_in_scratch scratch_window =
 exception OpenConjecturesStillThere;;
 exception WrongProof;;
 
-let save rendering_window () =
+let qed rendering_window () =
  match !ProofEngine.proof with
     None -> assert false
   | Some (uri,[],bo,ty) ->
@@ -606,6 +647,71 @@ let save rendering_window () =
   | _ -> raise OpenConjecturesStillThere
 ;;
 
+(*????
+let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
+*)
+let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
+
+let save rendering_window () =
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+  match !ProofEngine.proof with
+     None -> assert false
+   | Some (uri, metasenv, bo, ty) ->
+      let currentproof =
+       Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
+      in
+       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' =
+          [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+             Xml.xml_cdata
+              ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+             xml
+          >]
+         in
+          Xml.pp ~quiet:true xml' (Some "/public/sacerdot/currentproof") ;
+          output_html outputhtml
+           ("<h1 color=\"Green\">Current proof saved to " ^
+             "/public/sacerdot/currentproof</h1>")
+;;
+
+let load rendering_window () =
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ 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
+       Cic.CurrentProof (_,metasenv,bo,ty) ->
+        ProofEngine.proof :=
+         Some (uri, metasenv, bo, ty) ;
+        ProofEngine.goal :=
+         (match metasenv with
+             [] -> None
+           | (metano,_,_)::_ -> Some metano
+         ) ;
+        refresh_proof output ;
+        refresh_sequent proofw ;
+         output_html outputhtml
+          ("<h1 color=\"Green\">Current proof loaded from " ^
+            "/public/sacerdot/currentproof</h1>")
+     | _ -> assert false
+  with
+     RefreshSequentException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "sequent: " ^ Printexc.to_string e ^ "</h1>")
+   | RefreshProofException e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+        "proof: " ^ Printexc.to_string e ^ "</h1>")
+   | e ->
+      output_html outputhtml
+       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
 let proveit rendering_window () =
  let module L = LogicalOperations in
  let module G = Gdome in
@@ -627,8 +733,8 @@ let proveit rendering_window () =
          match !current_cic_infos with
             Some (ids_to_terms, ids_to_father_ids) ->
              let id = xpath in
-              if L.to_sequent id ids_to_terms ids_to_father_ids then
-               refresh_proof rendering_window#output ;
+              L.to_sequent id ids_to_terms ids_to_father_ids ;
+              refresh_proof rendering_window#output ;
               refresh_sequent rendering_window#proofw
           | None -> assert false (* "ERROR: No current term!!!" *)
         with
@@ -647,6 +753,98 @@ let proveit rendering_window () =
   | None -> assert false (* "ERROR: No selection!!!" *)
 ;;
 
+let focus rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+  match rendering_window#output#get_selection with
+    Some node ->
+     let xpath =
+      ((node : Gdome.element)#getAttributeNS
+      (*CSC: OCAML DIVERGE
+      ((element : G.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_cic_infos with
+            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
+          | 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>")
+         | RefreshProofException e ->
+            output_html outputhtml
+             ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+              "proof: " ^ Printexc.to_string e ^ "</h1>")
+         | e ->
+            output_html outputhtml
+             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+       end
+  | None -> assert false (* "ERROR: No selection!!!" *)
+;;
+
+exception NoPrevGoal;;
+exception NoNextGoal;;
+
+let prevgoal metasenv metano =
+ let rec aux =
+  function
+     [] -> assert false
+   | [(m,_,_)] -> raise NoPrevGoal
+   | (n,_,_)::(m,_,_)::_ when m=metano -> n
+   | _::tl -> aux tl
+ in
+  aux metasenv
+;;
+
+let nextgoal metasenv metano =
+ let rec aux =
+  function
+     [] -> assert false
+   | [(m,_,_)] when m = metano -> raise NoNextGoal
+   | (m,_,_)::(n,_,_)::_ when m=metano -> n
+   | _::tl -> aux tl
+ in
+  aux metasenv
+;;
+
+let prev_or_next_goal select_goal rendering_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+  let metasenv =
+   match !ProofEngine.proof with
+      None -> assert false
+    | Some (_,metasenv,_,_) -> metasenv
+  in
+  let metano =
+   match !ProofEngine.goal with
+      None -> assert false
+    | Some m -> m
+  in
+   try
+    ProofEngine.goal := Some (select_goal metasenv metano) ;
+    refresh_sequent rendering_window#proofw
+   with
+      RefreshSequentException e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+         "sequent: " ^ Printexc.to_string e ^ "</h1>")
+    | e ->
+       output_html outputhtml
+        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
 exception NotADefinition;;
 
 let open_ rendering_window () =
@@ -708,8 +906,8 @@ let state rendering_window () =
           let _  = CicTypeChecker.type_of_aux' [] [] expr in
            ProofEngine.proof :=
             Some (UriManager.uri_of_string "cic:/dummy.con",
-                   [1,expr], Cic.Meta 1, expr) ;
-           ProofEngine.goal := Some (1,([],expr)) ;
+                   [1,[],expr], Cic.Meta (1,[]), expr) ;
+           ProofEngine.goal := Some 1 ;
            refresh_sequent proofw ;
            refresh_proof output ;
      done
@@ -742,18 +940,22 @@ let check rendering_window scratch_window () =
       None -> UriManager.uri_of_string "cic:/dummy.con", []
     | Some (curi,metasenv,_,_) -> curi,metasenv
   in
-  let ciccontext,names_context =
+  let context,names_context =
    let context =
     match !ProofEngine.goal with
        None -> []
-     | Some (_,(ctx,_)) -> ctx
+     | Some metano ->
+        let (_,canonical_context,_) =
+         List.find (function (m,_,_) -> m=metano) metasenv
+        in
+         canonical_context
    in
-    ProofEngine.cic_context_of_named_context context,
-     List.map
-      (function
-          ProofEngine.Declaration (n,_)
-        | ProofEngine.Definition (n,_) -> n
-      ) context
+    context,
+    List.map
+     (function
+         Some (n,_) -> Some n
+       | None -> None
+     ) context
   in
    (* Do something interesting *)
    let lexbuf = Lexing.from_string input in
@@ -767,8 +969,8 @@ let check rendering_window scratch_window () =
          None -> ()
        | Some expr ->
           try
-           let ty  = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
-            let mml = mml_of_cic_term (Cic.Cast (expr,ty)) 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
           with
@@ -799,10 +1001,19 @@ let locate rendering_window () =
 
 let backward rendering_window () =
    let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+   let metasenv =
+    match !ProofEngine.proof with
+       None -> assert false
+     | Some (_,metasenv,_,_) -> metasenv
+   in
    let result =
       match !ProofEngine.goal with
          | None -> ""
-         | Some (_, (_, t)) -> (Mquery.backward t)
+         | Some metano ->
+            let (_,_,ty) =
+             List.find (function (m,_,_) -> m=metano) metasenv
+            in
+             Mquery.backward ty
       in 
    output_html outputhtml result
       
@@ -1009,9 +1220,15 @@ class rendering_window output proofw (label : GMisc.label) =
  let button_export_to_postscript =
   GButton.button ~label:"export_to_postscript"
   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let qedb =
+  GButton.button ~label:"Qed"
+   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
  let saveb =
   GButton.button ~label:"Save"
    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let loadb =
+  GButton.button ~label:"Load"
+   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
  let closeb =
   GButton.button ~label:"Close"
    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1020,6 +1237,15 @@ class rendering_window output proofw (label : GMisc.label) =
  let proveitb =
   GButton.button ~label:"Prove It"
    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let focusb =
+  GButton.button ~label:"Focus"
+   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let prevgoalb =
+  GButton.button ~label:"<"
+   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let nextgoalb =
+  GButton.button ~label:">"
+   ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
    ~packing:(vbox#pack ~padding:5) () in
  let hbox4 =
@@ -1058,8 +1284,8 @@ class rendering_window output proofw (label : GMisc.label) =
  let applyb =
   GButton.button ~label:"Apply"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
- let elimintrosb =
-  GButton.button ~label:"ElimIntros"
+ let elimintrossimplb =
+  GButton.button ~label:"ElimIntrosSimpl"
    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
  let whdb =
   GButton.button ~label:"Whd"
@@ -1108,8 +1334,13 @@ object(self)
    button_export_to_postscript (choose_selection output) in
   ignore(settingsb#connect#clicked settings_window#show) ;
   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
+  ignore(qedb#connect#clicked (qed self)) ;
   ignore(saveb#connect#clicked (save self)) ;
+  ignore(loadb#connect#clicked (load self)) ;
   ignore(proveitb#connect#clicked (proveit self)) ;
+  ignore(focusb#connect#clicked (focus self)) ;
+  ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
+  ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
   ignore(stateb#connect#clicked (state self)) ;
   ignore(openb#connect#clicked (open_ self)) ;
@@ -1118,7 +1349,7 @@ object(self)
   ignore(backwardb#connect#clicked (backward self)) ;
   ignore(exactb#connect#clicked (exact self)) ;
   ignore(applyb#connect#clicked (apply self)) ;
-  ignore(elimintrosb#connect#clicked (elimintros self)) ;
+  ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
   ignore(whdb#connect#clicked (whd self)) ;
   ignore(reduceb#connect#clicked (reduce self)) ;
   ignore(simplb#connect#clicked (simpl self)) ;