X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=0cfccab99f388ec5bd73e4265e150e647ba32b38;hb=e627ae3edfbe950b87069b625ec9317acaf03ec5;hp=4f8a29d76cbd70cbe99a545a4bd9e7bec5a17233;hpb=c6a3408b6e603bed4f3d3c15f897b9007d98bb6f;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 4f8a29d76..0cfccab99 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -52,6 +52,7 @@ let htmlfooter =
let htmlheader_and_content = ref htmlheader;;
let current_cic_infos = ref None;;
+let current_goal_infos = ref None;;
(* MISC FUNCTIONS *)
@@ -143,14 +144,12 @@ let applyStylesheets input styles args =
input styles
;;
-let mml_of_cic_object annobj ids_to_inner_sorts ids_to_inner_types =
+let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
let xml =
- Cic2Xml.print_object
- (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts annobj
+ Cic2Xml.print_object uri ids_to_inner_sorts annobj
in
let xmlinnertypes =
- Cic2Xml.print_inner_types
- (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts
+ Cic2Xml.print_inner_types uri ids_to_inner_sorts
ids_to_inner_types
in
let input = Xml2Gdome.document_of_xml domImpl xml in
@@ -166,17 +165,18 @@ let mml_of_cic_object annobj ids_to_inner_sorts ids_to_inner_types =
(* CALLBACKS *)
let refresh_proof (output : GMathView.math_view) =
- let currentproof =
+ let uri,currentproof =
match !ProofEngine.proof with
None -> assert false
- | Some (metasenv,bo,ty) -> Cic.CurrentProof ("unnamed", metasenv, bo, ty)
+ | 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 acic ids_to_inner_sorts ids_to_inner_types 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)
;;
@@ -188,9 +188,9 @@ let refresh_sequent (proofw : GMathView.math_view) =
let metasenv =
match !ProofEngine.proof with
None -> assert false
- | Some (metasenv,_,_) -> metasenv
+ | Some (_,metasenv,_,_) -> metasenv
in
- let sequent_gdome =
+ let sequent_gdome,ids_to_terms,ids_to_father_ids =
SequentPp.XmlPp.print_sequent metasenv currentsequent
in
let sequent_doc =
@@ -199,7 +199,8 @@ let refresh_sequent (proofw : GMathView.math_view) =
let sequent_mml =
applyStylesheets sequent_doc sequent_styles sequent_args
in
- proofw#load_tree ~dom:sequent_mml
+ proofw#load_tree ~dom:sequent_mml ;
+ current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
(*
ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
@@ -210,7 +211,8 @@ ignore(domImpl#saveDocumentToFile ~doc:sequent_mml
let output_html outputhtml msg =
htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter)
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
+ outputhtml#set_topline (-1)
;;
(***********************)
@@ -220,7 +222,6 @@ let output_html outputhtml msg =
let call_tactic tactic rendering_window () =
let proofw = (rendering_window#proofw : GMathView.math_view) in
let output = (rendering_window#output : 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
@@ -241,7 +242,6 @@ let call_tactic tactic rendering_window () =
let call_tactic_with_input tactic rendering_window () =
let proofw = (rendering_window#proofw : GMathView.math_view) in
let output = (rendering_window#output : GMathView.math_view) in
- let output = (rendering_window#output : GMathView.math_view) in
let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let inputt = (rendering_window#inputt : GEdit.text) in
let savedproof = !ProofEngine.proof in
@@ -250,6 +250,11 @@ let call_tactic_with_input tactic rendering_window () =
let inputlen = inputt#length in
let input = inputt#get_chars 0 inputlen ^ "\n" in
let lexbuf = Lexing.from_string input in
+ let curi =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (curi,_,_,_) -> curi
+ in
let context =
List.map
(function (_,n,_) -> n)
@@ -261,7 +266,7 @@ let call_tactic_with_input tactic rendering_window () =
try
while true do
match
- CicTextualParserContext.main context CicTextualLexer.token lexbuf
+ CicTextualParserContext.main curi context CicTextualLexer.token lexbuf
with
None -> ()
| Some expr ->
@@ -280,6 +285,113 @@ prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
ProofEngine.goal := savedgoal
;;
+let call_tactic_with_goal_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_terms, ids_to_father_ids) ->
+ let id = xpath in
+ tactic (Hashtbl.find ids_to_terms id) ;
+ refresh_sequent rendering_window#proofw ;
+ refresh_proof rendering_window#output
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ e ->
+ prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
+ end
+ | None ->
+ output_html outputhtml
+ ("No term selected
")
+;;
+
+let call_tactic_with_input_and_goal_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 inputt = (rendering_window#inputt : GEdit.text) 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_terms, ids_to_father_ids) ->
+ let id = xpath in
+ (* Let's parse the input *)
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ let lexbuf = Lexing.from_string input in
+ let curi =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (curi,_,_,_) -> curi
+ in
+ let context =
+ List.map
+ (function (_,n,_) -> n)
+ (match !ProofEngine.goal with
+ None -> assert false
+ | Some (_,(ctx,_)) -> ctx
+ )
+ in
+ begin
+ try
+ while true do
+ match
+ CicTextualParserContext.main curi context
+ CicTextualLexer.token lexbuf
+ with
+ None -> ()
+ | Some expr ->
+ tactic ~goal_input:(Hashtbl.find ids_to_terms id)
+ ~input:expr ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen
+ end
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ e ->
+prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
+ end
+ | None ->
+ output_html outputhtml
+ ("No term selected
")
+;;
+
let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
let exact rendering_window =
call_tactic_with_input ProofEngine.exact rendering_window
@@ -287,6 +399,30 @@ let exact rendering_window =
let apply rendering_window =
call_tactic_with_input ProofEngine.apply rendering_window
;;
+let elim rendering_window =
+ call_tactic_with_input ProofEngine.elim rendering_window
+;;
+let whd rendering_window =
+ call_tactic_with_goal_input ProofEngine.whd rendering_window
+;;
+let reduce rendering_window =
+ call_tactic_with_goal_input ProofEngine.reduce rendering_window
+;;
+let simpl rendering_window =
+ call_tactic_with_goal_input ProofEngine.simpl rendering_window
+;;
+let fold rendering_window =
+ call_tactic_with_input ProofEngine.fold rendering_window
+;;
+let cut rendering_window =
+ call_tactic_with_input ProofEngine.cut rendering_window
+;;
+let change rendering_window =
+ call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
+;;
+
+
+
(**********************)
(* END OF TACTICS *)
@@ -298,11 +434,11 @@ exception WrongProof;;
let save rendering_window () =
match !ProofEngine.proof with
None -> assert false
- | Some ([],bo,ty) ->
+ | Some (uri,[],bo,ty) ->
if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then
begin
(*CSC: Wrong: [] is just plainly wrong *)
- let proof = Cic.Definition ("unnamed",bo,ty,[]) in
+ 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)
@@ -310,7 +446,7 @@ let save rendering_window () =
Cic2acic.acic_object_of_cic_object proof
in
let mml =
- mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types
+ 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)
@@ -368,7 +504,9 @@ let state rendering_window () =
| Some expr ->
try
let _ = CicTypeChecker.type_of_aux' [] [] expr in
- ProofEngine.proof := Some ([1,expr], Cic.Meta 1, expr) ;
+ ProofEngine.proof :=
+ Some (UriManager.uri_of_string "cic:/dummy.con",
+ [1,expr], Cic.Meta 1, expr) ;
ProofEngine.goal := Some (1,([],expr)) ;
refresh_sequent proofw ;
refresh_proof output ;
@@ -587,6 +725,27 @@ 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 elimb =
+ GButton.button ~label:"Elim"
+ ~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
+ let reduceb =
+ GButton.button ~label:"Reduce"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let simplb =
+ GButton.button ~label:"Simpl"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let foldb =
+ GButton.button ~label:"Fold"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let cutb =
+ GButton.button ~label:"Cut"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let changeb =
+ GButton.button ~label:"Change"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:""
@@ -618,6 +777,13 @@ object(self)
ignore(stateb#connect#clicked (state self)) ;
ignore(exactb#connect#clicked (exact self)) ;
ignore(applyb#connect#clicked (apply self)) ;
+ ignore(elimb#connect#clicked (elim self)) ;
+ ignore(whdb#connect#clicked (whd self)) ;
+ ignore(reduceb#connect#clicked (reduce self)) ;
+ ignore(simplb#connect#clicked (simpl self)) ;
+ ignore(foldb#connect#clicked (fold self)) ;
+ ignore(cutb#connect#clicked (cut self)) ;
+ ignore(changeb#connect#clicked (change self)) ;
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
@@ -639,5 +805,6 @@ let initialize_everything () =
let _ =
CicCooking.init () ;
+ ignore (GtkMain.Main.init ()) ;
initialize_everything ()
;;