--- /dev/null
+(* Copyright (C) 2000-2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(* GLOBAL CONSTANTS *)
+
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
+
+let htmlheader =
+ "<html>" ^
+ " <body bgColor=\"white\">"
+;;
+
+let htmlfooter =
+ " </body>" ^
+ "</html>"
+;;
+
+let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
+(*CSC: the getter should handle the innertypes, not the FS *)
+let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
+
+(* GLOBAL REFERENCES (USED BY CALLBACKS) *)
+
+let htmlheader_and_content = ref htmlheader;;
+
+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 *)
+
+let domImpl = Gdome.domImplementation ();;
+
+let parseStyle name =
+ let style =
+ domImpl#createDocumentFromURI
+(*
+ ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
+*)
+ ~uri:("styles/" ^ name) ()
+ in
+ Gdome_xslt.processStylesheet style
+;;
+
+let d_c = parseStyle "drop_coercions.xsl";;
+let tc1 = parseStyle "objtheorycontent.xsl";;
+let hc2 = parseStyle "content_to_html.xsl";;
+let l = parseStyle "link.xsl";;
+
+let c1 = parseStyle "rootcontent.xsl";;
+let g = parseStyle "genmmlid.xsl";;
+let c2 = parseStyle "annotatedpres.xsl";;
+
+
+let getterURL = Configuration.getter_url;;
+let processorURL = Configuration.processor_url;;
+
+let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
+let mml_args =
+ ["processorURL", "'" ^ processorURL ^ "'" ;
+ "getterURL", "'" ^ getterURL ^ "'" ;
+ "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
+ "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
+ "UNICODEvsSYMBOL", "'symbol'" ;
+ "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
+ "encoding", "'iso-8859-1'" ;
+ "media-type", "'text/html'" ;
+ "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
+ "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
+ "naturalLanguage", "'yes'" ;
+ "annotations", "'no'" ;
+ "explodeall", "'true()'" ;
+ "topurl", "'http://phd.cs.unibo.it/helm'" ;
+ "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
+;;
+
+let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
+let sequent_args =
+ ["processorURL", "'" ^ processorURL ^ "'" ;
+ "getterURL", "'" ^ getterURL ^ "'" ;
+ "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
+ "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
+ "UNICODEvsSYMBOL", "'symbol'" ;
+ "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
+ "encoding", "'iso-8859-1'" ;
+ "media-type", "'text/html'" ;
+ "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
+ "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
+ "naturalLanguage", "'no'" ;
+ "annotations", "'no'" ;
+ "explodeall", "'true()'" ;
+ "topurl", "'http://phd.cs.unibo.it/helm'" ;
+ "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
+;;
+
+let parse_file filename =
+ let inch = open_in filename in
+ let rec read_lines () =
+ try
+ let line = input_line inch in
+ line ^ read_lines ()
+ with
+ End_of_file -> ""
+ in
+ read_lines ()
+;;
+
+let applyStylesheets input styles args =
+ List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
+ input styles
+;;
+
+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
+ in
+ let xmlinnertypes =
+ 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 innertypesfile) ;
+ let output = applyStylesheets input mml_styles mml_args in
+ output
+;;
+
+
+(* CALLBACKS *)
+
+exception RefreshSequentException of exn;;
+exception RefreshProofException of exn;;
+
+let refresh_proof (output : GMathView.math_view) =
+ try
+ let uri,currentproof =
+ match !ProofEngine.proof with
+ None -> assert false
+ | 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,ids_to_conjectures,ids_to_hypotheses)
+ =
+ Cic2acic.acic_object_of_cic_object currentproof
+ 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,ids_to_conjectures,ids_to_hypotheses)
+ with
+ 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 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,ids_to_hypotheses =
+ SequentPp.XmlPp.print_sequent metasenv currentsequent
+ in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
+ in
+ let sequent_mml =
+ 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,ids_to_hypotheses)
+ with
+ 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)
+;;
+
+(*
+ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
+ ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
+*)
+
+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 metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context
+ in
+ 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 =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
+ in
+ let res =
+ applyStylesheets sequent_doc sequent_styles sequent_args ;
+ in
+ current_scratch_infos :=
+ Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
+ res
+;;
+
+let output_html outputhtml msg =
+ htmlheader_and_content := !htmlheader_and_content ^ msg ;
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
+ outputhtml#set_topline (-1)
+;;
+
+(***********************)
+(* TACTICS *)
+(***********************)
+
+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 outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ begin
+ try
+ tactic () ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ 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
+;;
+
+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 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
+(*CSC: Gran cut&paste da sotto... *)
+ 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 uri,metasenv,bo,ty =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+ in
+ let context =
+ List.map
+ (function
+ Some (n,_) -> Some n
+ | None -> None)
+ (match !ProofEngine.goal with
+ None -> assert false
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context
+ )
+ in
+ try
+ while true do
+ match
+ CicTextualParserContext.main
+ curi context metasenv CicTextualLexer.token lexbuf
+ with
+ None -> ()
+ | Some (metasenv',expr) ->
+ ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ tactic expr ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen
+ | 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 ;
+;;
+
+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
+ 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 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 uri,metasenv,bo,ty =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
+ in
+ let context =
+ List.map
+ (function
+ Some (n,_) -> Some n
+ | None -> None)
+ (match !ProofEngine.goal with
+ None -> assert false
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context
+ )
+ in
+ begin
+ try
+ while true do
+ match
+ CicTextualParserContext.main curi context metasenv
+ CicTextualLexer.token lexbuf
+ with
+ None -> ()
+ | Some (metasenv',expr) ->
+ ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
+ 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
+ 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 call_tactic_with_goal_input_in_scratch tactic scratch_window () =
+ let module L = LogicalOperations in
+ let module G = Gdome in
+ let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
+ let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ match mmlwidget#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_scratch_infos with
+ (* term is the whole goal in the scratch_area *)
+ 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
+ scratch_window#show () ;
+ scratch_window#mmlwidget#load_tree ~dom:mml
+ | None -> assert false (* "ERROR: No current term!!!" *)
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None ->
+ output_html outputhtml
+ ("<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
+;;
+let apply rendering_window =
+ call_tactic_with_input ProofEngine.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
+;;
+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
+;;
+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 fourier rendering_window =
+ call_tactic ProofEngine.fourier rendering_window
+;;
+let rewritesimpl rendering_window =
+ call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
+;;
+
+
+
+let whd_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
+ scratch_window
+;;
+let reduce_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
+ scratch_window
+;;
+let simpl_in_scratch scratch_window =
+ call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
+ scratch_window
+;;
+
+
+
+(**********************)
+(* END OF TACTICS *)
+(**********************)
+
+exception OpenConjecturesStillThere;;
+exception WrongProof;;
+
+let qed rendering_window () =
+ match !ProofEngine.proof with
+ None -> assert false
+ | 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 (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_conjectures,ids_to_hypotheses)
+ =
+ Cic2acic.acic_object_of_cic_object proof
+ in
+ let mml =
+ 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,ids_to_conjectures,
+ ids_to_hypotheses)
+ end
+ else
+ raise WrongProof
+ | _ -> raise OpenConjecturesStillThere
+;;
+
+(*????
+let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
+*)
+let dtdname = "/home/tassi/miohelm/helm/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 prooffile) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof saved to " ^
+ 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 () =
+ 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 prooffile uri with
+ Cic.CurrentProof (_,metasenv,bo,ty) ->
+ typecheck_loaded_proof 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 " ^
+ prooffile ^ "</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
+ 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.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
+ 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!!!" *)
+;;
+
+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 () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ 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
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ try
+ let uri = UriManager.uri_of_string ("cic:" ^ input) in
+ CicTypeChecker.typecheck uri ;
+ let metasenv,bo,ty =
+ match CicEnvironment.get_cooked_obj uri 0 with
+ Cic.Definition (_,bo,ty,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
+ | Cic.Axiom _
+ | Cic.Variable _
+ | Cic.InductiveDefinition _ -> raise NotADefinition
+ in
+ ProofEngine.proof :=
+ Some (uri, metasenv, bo, ty) ;
+ ProofEngine.goal := None ;
+ refresh_sequent proofw ;
+ refresh_proof output ;
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
+ 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 state rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let oldinputt = (rendering_window#oldinputt : GEdit.text) in
+ 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
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ (* Do something interesting *)
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match CicTextualParser.main CicTextualLexer.token lexbuf with
+ None -> ()
+ | Some expr ->
+ 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 ;
+ refresh_sequent proofw ;
+ refresh_proof output ;
+ done
+ with
+ CicTextualParser0.Eof ->
+ inputt#delete_text 0 inputlen ;
+ ignore(oldinputt#insert_text input oldinputt#length)
+ | 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 check rendering_window scratch_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ 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
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen ^ "\n" in
+ let curi,metasenv =
+ match !ProofEngine.proof with
+ None -> UriManager.uri_of_string "cic:/dummy.con", []
+ | Some (curi,metasenv,_,_) -> curi,metasenv
+ in
+ let context,names_context =
+ let context =
+ match !ProofEngine.goal with
+ None -> []
+ | Some metano ->
+ let (_,canonical_context,_) =
+ List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ canonical_context
+ in
+ context,
+ List.map
+ (function
+ Some (n,_) -> Some n
+ | None -> None
+ ) context
+ in
+ (* Do something interesting *)
+ let lexbuf = Lexing.from_string input in
+ try
+ while true do
+ (* Execute the actions *)
+ match
+ CicTextualParserContext.main curi names_context metasenv
+ CicTextualLexer.token lexbuf
+ with
+ None -> ()
+ | Some (metasenv',expr) ->
+ try
+ 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
+ e ->
+ print_endline ("? " ^ CicPp.ppterm expr) ;
+ raise e
+ done
+ with
+ CicTextualParser0.Eof -> ()
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+exception NoObjectsLocated;;
+
+let user_uri_choice uris =
+ let uri =
+ match uris with
+ [] -> raise NoObjectsLocated
+ | [uri] -> uri
+ | uris ->
+ let choice =
+ GToolbox.question_box ~title:"Ambiguous result."
+ ~buttons:uris ~default:1
+ "Ambiguous result. Please, choose one."
+ in
+ List.nth uris (choice-1)
+ in
+ String.sub uri 4 (String.length uri - 4)
+;;
+
+let locate rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen in
+ try
+ match Str.split (Str.regexp "[ \t]+") input with
+ [] -> ()
+ | head :: tail ->
+ inputt#delete_text 0 inputlen ;
+ let MathQL.MQRefs uris, html = MQueryGenerator.locate head in
+ output_html outputhtml html ;
+ let uri' = user_uri_choice uris in
+ ignore ((inputt#insert_text uri') ~pos:0)
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+let backward rendering_window () =
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen in
+ let level = int_of_string input in
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ try
+ match !ProofEngine.goal with
+ None -> ()
+ | Some metano ->
+ let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
+ let MathQL.MQRefs uris, html =
+ MQueryGenerator.backward metasenv ey ty level
+ in
+ output_html outputhtml html ;
+ let uri' = user_uri_choice uris in
+ inputt#delete_text 0 inputlen ;
+ ignore ((inputt#insert_text uri') ~pos:0)
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+let choose_selection
+ (mmlwidget : GMathView.math_view) (element : Gdome.element option)
+=
+ let module G = Gdome in
+ let rec aux element =
+ if element#hasAttributeNS
+ ~namespaceURI:helmns
+ ~localName:(G.domString "xref")
+ then
+ mmlwidget#set_selection (Some element)
+ else
+ match element#get_parentNode with
+ None -> assert false
+ (*CSC: OCAML DIVERGES!
+ | Some p -> aux (new G.element_of_node p)
+ *)
+ | Some p -> aux (new Gdome.element_of_node p)
+ in
+ match element with
+ Some x -> aux x
+ | None -> mmlwidget#set_selection None
+;;
+
+(* STUFF TO BUILD THE GTK INTERFACE *)
+
+(* Stuff for the widget settings *)
+
+let export_to_postscript (output : GMathView.math_view) () =
+ output#export_to_postscript ~filename:"output.ps" ();
+;;
+
+let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
+ button_set_kerning button_set_transparency button_export_to_postscript
+ button_t1 ()
+=
+ let is_set = button_t1#active in
+ output#set_font_manager_type
+ (if is_set then `font_manager_t1 else `font_manager_gtk) ;
+ if is_set then
+ begin
+ button_set_anti_aliasing#misc#set_sensitive true ;
+ button_set_kerning#misc#set_sensitive true ;
+ button_set_transparency#misc#set_sensitive true ;
+ button_export_to_postscript#misc#set_sensitive true ;
+ end
+ else
+ begin
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
+ button_set_transparency#misc#set_sensitive false ;
+ button_export_to_postscript#misc#set_sensitive false ;
+ end
+;;
+
+let set_anti_aliasing output button_set_anti_aliasing () =
+ output#set_anti_aliasing button_set_anti_aliasing#active
+;;
+
+let set_kerning output button_set_kerning () =
+ output#set_kerning button_set_kerning#active
+;;
+
+let set_transparency output button_set_transparency () =
+ output#set_transparency button_set_transparency#active
+;;
+
+let changefont output font_size_spinb () =
+ output#set_font_size font_size_spinb#value_as_int
+;;
+
+let set_log_verbosity output log_verbosity_spinb () =
+ output#set_log_verbosity log_verbosity_spinb#value_as_int
+;;
+
+class settings_window (output : GMathView.math_view) sw
+ button_export_to_postscript selection_changed_callback
+=
+ let settings_window = GWindow.window ~title:"GtkMathView settings" () in
+ let vbox =
+ GPack.vbox ~packing:settings_window#add () in
+ let table =
+ GPack.table
+ ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let button_t1 =
+ GButton.toggle_button ~label:"activate t1 fonts"
+ ~packing:(table#attach ~left:0 ~top:0) () in
+ let button_set_anti_aliasing =
+ GButton.toggle_button ~label:"set_anti_aliasing"
+ ~packing:(table#attach ~left:0 ~top:1) () in
+ let button_set_kerning =
+ GButton.toggle_button ~label:"set_kerning"
+ ~packing:(table#attach ~left:1 ~top:1) () in
+ let button_set_transparency =
+ GButton.toggle_button ~label:"set_transparency"
+ ~packing:(table#attach ~left:2 ~top:1) () in
+ let table =
+ GPack.table
+ ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
+ ~border_width:5 ~packing:vbox#add () in
+ let font_size_label =
+ GMisc.label ~text:"font size:"
+ ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
+ let font_size_spinb =
+ let sadj =
+ GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+ in
+ GEdit.spin_button
+ ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
+ let log_verbosity_label =
+ GMisc.label ~text:"log verbosity:"
+ ~packing:(table#attach ~left:0 ~top:1) () in
+ let log_verbosity_spinb =
+ let sadj =
+ GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
+ in
+ GEdit.spin_button
+ ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let closeb =
+ GButton.button ~label:"Close"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+object(self)
+ method show = settings_window#show
+ initializer
+ button_set_anti_aliasing#misc#set_sensitive false ;
+ button_set_kerning#misc#set_sensitive false ;
+ button_set_transparency#misc#set_sensitive false ;
+ (* Signals connection *)
+ ignore(button_t1#connect#clicked
+ (activate_t1 output button_set_anti_aliasing button_set_kerning
+ button_set_transparency button_export_to_postscript button_t1)) ;
+ ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
+ ignore(button_set_anti_aliasing#connect#toggled
+ (set_anti_aliasing output button_set_anti_aliasing));
+ ignore(button_set_kerning#connect#toggled
+ (set_kerning output button_set_kerning)) ;
+ ignore(button_set_transparency#connect#toggled
+ (set_transparency output button_set_transparency)) ;
+ ignore(log_verbosity_spinb#connect#changed
+ (set_log_verbosity output log_verbosity_spinb)) ;
+ ignore(closeb#connect#clicked settings_window#misc#hide)
+end;;
+
+(* Scratch window *)
+
+class scratch_window outputhtml =
+ let window =
+ GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ let vbox =
+ GPack.vbox ~packing:window#add () in
+ let hbox =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let whdb =
+ GButton.button ~label:"Whd"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let reduceb =
+ GButton.button ~label:"Reduce"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let simplb =
+ GButton.button ~label:"Simpl"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ let mmlwidget =
+ GMathView.math_view
+ ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
+object(self)
+ method outputhtml = outputhtml
+ method mmlwidget = mmlwidget
+ method show () = window#misc#hide () ; window#show ()
+ initializer
+ ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
+ ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
+ ignore(whdb#connect#clicked (whd_in_scratch self)) ;
+ ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
+ ignore(simplb#connect#clicked (simpl_in_scratch self))
+end;;
+
+(* Main window *)
+
+class rendering_window output proofw (label : GMisc.label) =
+ let window =
+ GWindow.window ~title:"MathML viewer" ~border_width:2 () in
+ let hbox0 =
+ GPack.hbox ~packing:window#add () in
+ let vbox =
+ GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
+ let scrolled_window0 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox#pack ~expand:true ~padding:5) () in
+ let _ = scrolled_window0#add output#coerce in
+ let hbox1 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let settingsb =
+ GButton.button ~label:"Settings"
+ ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ 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
+ let hbox2 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ 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 =
+ GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let stateb =
+ GButton.button ~label:"State"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let openb =
+ GButton.button ~label:"Open"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let checkb =
+ GButton.button ~label:"Check"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let locateb =
+ GButton.button ~label:"Locate"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let backwardb =
+ GButton.button ~label:"Backward"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
+ ~packing:(vbox#pack ~padding:5) () in
+ let vbox1 =
+ GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
+ let scrolled_window1 =
+ GBin.scrolled_window ~border_width:10
+ ~packing:(vbox1#pack ~expand:true ~padding:5) () in
+ let _ = scrolled_window1#add proofw#coerce in
+ let hbox3 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let exactb =
+ GButton.button ~label:"Exact"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let introsb =
+ GButton.button ~label:"Intros"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let applyb =
+ GButton.button ~label:"Apply"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ 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
+ 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 hbox4 =
+ GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
+ let letinb =
+ GButton.button ~label:"Let ... 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 fourierb =
+ GButton.button ~label:"Fourier"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let rewritesimplb =
+ GButton.button ~label:"RewriteSimpl ->"
+ ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
+ let outputhtml =
+ GHtml.xmhtml
+ ~source:"<html><body bgColor=\"white\"></body></html>"
+ ~width:400 ~height: 200
+ ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
+ ~show:true () in
+ let scratch_window = new scratch_window outputhtml in
+object(self)
+ method outputhtml = outputhtml
+ method oldinputt = oldinputt
+ method inputt = inputt
+ method output = (output : GMathView.math_view)
+ method proofw = (proofw : GMathView.math_view)
+ method show = window#show
+ initializer
+ button_export_to_postscript#misc#set_sensitive false ;
+
+ (* signal handlers here *)
+ ignore(output#connect#selection_changed
+ (function elem -> proofw#unload ; choose_selection output elem)) ;
+ ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
+ ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
+ let settings_window = new settings_window output scrolled_window0
+ 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)) ;
+ ignore(checkb#connect#clicked (check self scratch_window)) ;
+ ignore(locateb#connect#clicked (locate self)) ;
+ ignore(backwardb#connect#clicked (backward 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)) ;
+ ignore(foldb#connect#clicked (fold 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(fourierb#connect#clicked (fourier self)) ;
+ ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
+ ignore(introsb#connect#clicked (intros self)) ;
+ Logger.log_callback :=
+ (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
+end;;
+
+(* MAIN *)
+
+let rendering_window = ref None;;
+
+let initialize_everything () =
+ let module U = Unix in
+ let output = GMathView.math_view ~width:350 ~height:280 ()
+ and proofw = GMathView.math_view ~width:400 ~height:275 ()
+ and label = GMisc.label ~text:"gTopLevel" () in
+ let rendering_window' =
+ new rendering_window output proofw label
+ in
+ rendering_window := Some rendering_window' ;
+ rendering_window'#show () ;
+ GMain.Main.main ()
+;;
+
+let _ =
+ CicCooking.init () ;
+ if !usedb then
+ begin
+ MQueryGenerator.init () ;
+ CicTextualParser0.set_locate_object
+ (function id ->
+ let MathQL.MQRefs uris, html = MQueryGenerator.locate id in
+ begin
+ match !rendering_window with
+ None -> assert false
+ | Some rw -> output_html rw#outputhtml html ;
+ end ;
+ let uri =
+ match uris with
+ [] ->
+ (match
+ (GToolbox.input_string ~title:"Unknown input"
+ ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+ with
+ None -> None
+ | Some uri -> Some ("cic:" ^ uri)
+ )
+ | [uri] -> Some uri
+ | _ ->
+ let choice =
+ GToolbox.question_box ~title:"Ambiguous input."
+ ~buttons:uris ~default:1 "Ambiguous input. Please, choose one."
+ in
+ if choice > 0 then
+ Some (List.nth uris (choice - 1))
+ else
+ (* No choice from the user *)
+ None
+ in
+ match uri with
+ Some uri' ->
+ (* Constant *)
+ if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+ Some (Cic.Const (UriManager.uri_of_string uri',0))
+ else
+ (try
+ (* Inductive Type *)
+ let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+ Some (Cic.MutInd (uri'',0,typeno))
+ with
+ _ ->
+ (* Constructor of an Inductive Type *)
+ let uri'',typeno,consno =
+ CicTextualLexer.indconuri_of_uri uri'
+ in
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+ Some (Cic.MutConstruct (uri'',0,typeno,consno))
+ )
+ | None -> None
+ )
+ end ;
+ ignore (GtkMain.Main.init ()) ;
+ initialize_everything () ;
+ if !usedb then MQueryGenerator.close ();
+;;
projects / helm.git / commitdiff