From 6d80f8eb7df3548c7a6fa333a0acfddd4cd0d329 Mon Sep 17 00:00:00 2001 From: no author Date: Thu, 17 Oct 2002 15:16:44 +0000 Subject: [PATCH] This commit was manufactured by cvs2svn to create branch 'new_mathql'. --- helm/gTopLevel/gTopLevel.ml | 1610 +++++++++++++++++++++++++++++++++++ 1 file changed, 1610 insertions(+) create mode 100644 helm/gTopLevel/gTopLevel.ml diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml new file mode 100644 index 000000000..c980f723b --- /dev/null +++ b/helm/gTopLevel/gTopLevel.ml @@ -0,0 +1,1610 @@ +(* 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 *) +(* 06/01/2002 *) +(* *) +(* *) +(******************************************************************************) + +(* GLOBAL CONSTANTS *) + +let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; + +let htmlheader = + "" ^ + " " +;; + +let htmlfooter = + " " ^ + "" +;; + +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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + 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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + 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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + 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 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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + +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 + ("

" ^ Printexc.to_string e ^ "

") + end + | None -> + output_html outputhtml + ("

No term selected

") +;; + +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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + refresh_sequent proofw ; + refresh_proof output + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; + ProofEngine.proof := savedproof ; + ProofEngine.goal := savedgoal ; + 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 +;; +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 "\n" ; + Xml.xml_cdata + ("\n\n") ; + xml + >] + in + Xml.pp ~quiet:true xml' (Some prooffile) ; + output_html outputhtml + ("

Current proof saved to " ^ + prooffile ^ "

") +;; + +(* 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 + ("

Current proof loaded from " ^ + prooffile ^ "

") + | _ -> assert false + with + RefreshSequentException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + 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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") + 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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") +;; + +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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +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 + ("

Exception raised during the refresh of the " ^ + "sequent: " ^ Printexc.to_string e ^ "

") + | RefreshProofException e -> + output_html outputhtml + ("

Exception raised during the refresh of the " ^ + "proof: " ^ Printexc.to_string e ^ "

") + | e -> + output_html outputhtml + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +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 + ("

" ^ Printexc.to_string e ^ "

") ; +;; + +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 + ("

" ^ Printexc.to_string e ^ "

") +;; + +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 + ("

" ^ Printexc.to_string e ^ "

") +;; + +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:"" + ~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 (); +;; -- 2.39.2