(* 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 *) (* *) (* *) (******************************************************************************) (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *) let wrong_xpointer_format_from_wrong_xpointer_format' uri = try let index_sharp = String.index uri '#' in let index_rest = index_sharp + 10 in let baseuri = String.sub uri 0 index_sharp in let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in baseuri ^ "#" ^ rest with Not_found -> uri ;; (* GLOBAL CONSTANTS *) let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; let htmlheader = "" ^ " " ;; let htmlfooter = " " ^ "" ;; (* let prooffile = "/home/tassi/miohelm/tmp/currentproof";; *) let prooffile = "/public/sacerdot/currentproof";; (*CSC: the getter should handle the innertypes, not the FS *) (* let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; *) let innertypesfile = "/public/sacerdot/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) ;; (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *) let get_last_query = let query = ref "" in MQueryGenerator.set_confirm_query (function q -> query := MQueryUtil.text_of_query q ; true) ; function result -> !query ^ "

Result:

" ^ MQueryUtil.text_of_result result "
" ;; 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 result = MQueryGenerator.locate head in let uris = List.map (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) result in let html = ("

Locate Query:

" ^ get_last_query result ^ "

") 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 result = MQueryGenerator.backward metasenv ey ty level in let uris = List.map (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) result in let html = "

Backward Query:

" ^ "

Levels:

" ^ MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "
" ^ "

" ^ get_last_query result ^ "

" 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 Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ; CicTextualParser0.set_locate_object (function id -> let result = MQueryGenerator.locate id in let uris = List.map (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri) result in let html = ("

Locate Query:

" ^ get_last_query result ^ "

") 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 Mqint.close (); ;;