1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
40 let index_sharp = String.index uri '#' in
41 let index_rest = index_sharp + 10 in
42 let baseuri = String.sub uri 0 index_sharp in
43 let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
48 (* GLOBAL CONSTANTS *)
50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
54 " <body bgColor=\"white\">"
63 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
64 let prooffile = "/public/sacerdot/currentproof";;
67 let prooffile = "/public/sacerdot/currentproof";;
68 let prooffiletype = "/public/sacerdot/currentprooftype";;
70 (*CSC: the getter should handle the innertypes, not the FS *)
72 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
73 let innertypesfile = "/public/sacerdot/innertypes";;
76 let innertypesfile = "/public/sacerdot/innertypes";;
77 let constanttypefile = "/public/sacerdot/constanttype";;
79 let empty_id_to_uris = ([],function _ -> None);;
82 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
84 let htmlheader_and_content = ref htmlheader;;
86 let current_cic_infos = ref None;;
87 let current_goal_infos = ref None;;
88 let current_scratch_infos = ref None;;
90 let id_to_uris = ref empty_id_to_uris;;
92 let check_term = ref (fun _ _ _ -> assert false);;
94 exception RenderingWindowsNotInitialized;;
96 let set_rendering_window,rendering_window =
97 let rendering_window_ref = ref None in
98 (function rw -> rendering_window_ref := Some rw),
100 match !rendering_window_ref with
101 None -> raise RenderingWindowsNotInitialized
106 exception SettingsWindowsNotInitialized;;
108 let set_settings_window,settings_window =
109 let settings_window_ref = ref None in
110 (function rw -> settings_window_ref := Some rw),
112 match !settings_window_ref with
113 None -> raise SettingsWindowsNotInitialized
118 (* COMMAND LINE OPTIONS *)
124 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
127 Arg.parse argspec ignore ""
132 let cic_textual_parser_uri_of_string uri' =
134 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
135 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
137 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
138 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
142 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
143 CicTextualParser0.IndTyUri (uri'',typeno)
146 (* Constructor of an Inductive Type *)
147 let uri'',typeno,consno =
148 CicTextualLexer.indconuri_of_uri uri'
150 CicTextualParser0.IndConUri (uri'',typeno,consno)
154 let term_of_cic_textual_parser_uri uri =
155 let module C = Cic in
156 let module CTP = CicTextualParser0 in
158 CTP.ConUri uri -> C.Const (uri,[])
159 | CTP.VarUri uri -> C.Var (uri,[])
160 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
161 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
164 let string_of_cic_textual_parser_uri uri =
165 let module C = Cic in
166 let module CTP = CicTextualParser0 in
169 CTP.ConUri uri -> UriManager.string_of_uri uri
170 | CTP.VarUri uri -> UriManager.string_of_uri uri
171 | CTP.IndTyUri (uri,tyno) ->
172 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
173 | CTP.IndConUri (uri,tyno,consno) ->
174 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
177 (* 4 = String.length "cic:" *)
178 String.sub uri' 4 (String.length uri' - 4)
181 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
185 let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris =
186 let choice = ref None in
187 let window = GWindow.dialog ~modal:true ~title () in
189 GMisc.label ~text:msg ~packing:window#vbox#add () in
190 let vbox = GPack.vbox ~border_width:10
191 ~packing:(window#action_area#pack ~expand:true ~padding:4) () in
192 let hbox1 = GPack.hbox ~border_width:10 ~packing:vbox#add () in
194 GEdit.combo ~popdown_strings:uris ~packing:hbox1#add () in
196 GButton.button ~label:"Check"
197 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
198 let hbox = GPack.hbox ~border_width:10 ~packing:vbox#add () in
200 GButton.button ~label:"Ok"
201 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
203 GButton.button ~label:cancel
204 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
207 choice := Some combo#entry#text ;
210 let check_callback () =
212 (term_of_cic_textual_parser_uri
213 (cic_textual_parser_uri_of_string combo#entry#text))
215 ignore (window#connect#destroy GMain.Main.quit) ;
216 ignore (cancelb#connect#clicked window#destroy) ;
217 ignore (okb#connect#clicked ok_callback) ;
218 ignore (checkb#connect#clicked check_callback) ;
219 window#set_position `CENTER ;
223 None -> raise NoChoice
229 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
231 let query = ref "" in
232 MQueryGenerator.set_confirm_query
233 (function q -> query := MQueryUtil.text_of_query q ; true) ;
234 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
237 let register_alias (id,uri) =
238 let dom,resolve_id = !id_to_uris in
240 (if List.mem id dom then dom else id::dom),
241 function id' -> if id' = id then Some uri else resolve_id id'
244 let output_html outputhtml msg =
245 htmlheader_and_content := !htmlheader_and_content ^ msg ;
246 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
247 outputhtml#set_topline (-1)
250 let locate_one_id id =
251 let result = MQueryGenerator.locate id in
255 wrong_xpointer_format_from_wrong_xpointer_format' uri
257 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
258 output_html (rendering_window ())#outputhtml html ;
263 (GToolbox.input_string ~title:"Unknown input"
264 ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
266 None -> raise NoChoice
267 | Some uri -> ["cic:" ^ uri]
272 [interactive_user_uri_choice
273 ~cancel:"Try every possibility."
274 ~title:"Ambiguous input."
276 ("Ambiguous input \"" ^ id ^
277 "\". Please, choose one interpretation:")
283 List.map cic_textual_parser_uri_of_string uris'
286 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
287 exception AmbiguousInput;;
289 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
290 let known_ids,resolve_id = !id_to_uris in
296 if List.mem he known_ids then filter tl else he::(filter tl)
300 (* for each id in dom' we get the list of uris associated to it *)
301 let list_of_uris = List.map locate_one_id dom' in
302 (* and now we compute the list of all possible assignments from id to uris *)
304 let rec aux ids list_of_uris =
305 match ids,list_of_uris with
306 [],[] -> [resolve_id]
307 | id::idtl,uris::uristl ->
308 let resolves = aux idtl uristl in
314 function id' -> if id = id' then Some uri else f id'
318 | _,_ -> assert false
320 aux dom' list_of_uris
322 prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ;
323 (* now we select only the ones that generates well-typed terms *)
329 let metasenv',expr = mk_metasenv_and_expr resolve in
331 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
333 (CicTypeChecker.type_of_aux' metasenv context expr) ;
341 match resolve_ids' with
342 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
343 | [resolve_id] -> resolve_id
352 match resolve id with
356 CicTextualParser0.ConUri uri
357 | CicTextualParser0.VarUri uri ->
358 UriManager.string_of_uri uri
359 | CicTextualParser0.IndTyUri (uri,tyno) ->
360 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
361 string_of_int (tyno+1) ^ ")"
362 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
363 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
364 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
370 GToolbox.question_box ~title:"Ambiguous input."
372 ~default:1 "Ambiguous input. Please, choose one interpretation."
375 List.nth resolve_ids' (choice - 1)
377 (* No choice from the user *)
380 id_to_uris := known_ids @ dom', resolve_id' ;
381 mk_metasenv_and_expr resolve_id'
384 let domImpl = Gdome.domImplementation ();;
386 let parseStyle name =
388 domImpl#createDocumentFromURI
390 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
392 ~uri:("styles/" ^ name) ()
394 Gdome_xslt.processStylesheet style
397 let d_c = parseStyle "drop_coercions.xsl";;
398 let tc1 = parseStyle "objtheorycontent.xsl";;
399 let hc2 = parseStyle "content_to_html.xsl";;
400 let l = parseStyle "link.xsl";;
402 let c1 = parseStyle "rootcontent.xsl";;
403 let g = parseStyle "genmmlid.xsl";;
404 let c2 = parseStyle "annotatedpres.xsl";;
407 let getterURL = Configuration.getter_url;;
408 let processorURL = Configuration.processor_url;;
410 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
412 ["processorURL", "'" ^ processorURL ^ "'" ;
413 "getterURL", "'" ^ getterURL ^ "'" ;
414 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
415 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
416 "UNICODEvsSYMBOL", "'symbol'" ;
417 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
418 "encoding", "'iso-8859-1'" ;
419 "media-type", "'text/html'" ;
420 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
421 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
422 "naturalLanguage", "'yes'" ;
423 "annotations", "'no'" ;
424 "explodeall", "'true()'" ;
425 "topurl", "'http://phd.cs.unibo.it/helm'" ;
426 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
429 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
431 ["processorURL", "'" ^ processorURL ^ "'" ;
432 "getterURL", "'" ^ getterURL ^ "'" ;
433 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
434 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
435 "UNICODEvsSYMBOL", "'symbol'" ;
436 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
437 "encoding", "'iso-8859-1'" ;
438 "media-type", "'text/html'" ;
439 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
440 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
441 "naturalLanguage", "'no'" ;
442 "annotations", "'no'" ;
443 "explodeall", "'true()'" ;
444 "topurl", "'http://phd.cs.unibo.it/helm'" ;
445 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
448 let parse_file filename =
449 let inch = open_in filename in
450 let rec read_lines () =
452 let line = input_line inch in
460 let applyStylesheets input styles args =
461 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
465 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
466 (*CSC: ????????????????? *)
468 Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
471 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
476 None -> Xml2Gdome.document_of_xml domImpl xml
478 Xml.pp xml (Some constanttypefile) ;
479 Xml2Gdome.document_of_xml domImpl bodyxml'
481 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
482 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
484 Xml.pp xmlinnertypes (Some innertypesfile) ;
485 let output = applyStylesheets input mml_styles mml_args in
492 exception RefreshSequentException of exn;;
493 exception RefreshProofException of exn;;
495 let refresh_proof (output : GMathView.math_view) =
497 let uri,currentproof =
498 match !ProofEngine.proof with
500 | Some (uri,metasenv,bo,ty) ->
501 (*CSC: Wrong: [] is just plainly wrong *)
502 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
505 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
506 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
508 Cic2acic.acic_object_of_cic_object currentproof
511 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
513 output#load_tree mml ;
515 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
518 match !ProofEngine.proof with
520 | Some (uri,metasenv,bo,ty) ->
521 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
522 raise (RefreshProofException e)
525 let refresh_sequent ?(empty_notebook=true) notebook =
527 match !ProofEngine.goal with
529 if empty_notebook then
531 notebook#remove_all_pages ;
532 notebook#set_empty_page
535 notebook#proofw#unload
538 match !ProofEngine.proof with
540 | Some (_,metasenv,_,_) -> metasenv
542 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
543 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
544 SequentPp.XmlPp.print_sequent metasenv currentsequent
547 Xml2Gdome.document_of_xml domImpl sequent_gdome
550 applyStylesheets sequent_doc sequent_styles sequent_args
552 if empty_notebook then
554 notebook#remove_all_pages ;
555 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
557 notebook#set_current_page metano ;
558 notebook#proofw#load_tree ~dom:sequent_mml ;
559 current_goal_infos :=
560 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
564 match !ProofEngine.goal with
569 match !ProofEngine.proof with
571 | Some (_,metasenv,_,_) -> metasenv
573 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
574 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
575 raise (RefreshSequentException e)
579 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
580 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
583 let mml_of_cic_term metano term =
585 match !ProofEngine.proof with
587 | Some (_,metasenv,_,_) -> metasenv
590 match !ProofEngine.goal with
593 let (_,canonical_context,_) =
594 List.find (function (m,_,_) -> m=metano) metasenv
598 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
599 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
602 Xml2Gdome.document_of_xml domImpl sequent_gdome
605 applyStylesheets sequent_doc sequent_styles sequent_args ;
607 current_scratch_infos :=
608 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
612 (***********************)
614 (***********************)
616 let call_tactic tactic () =
617 let notebook = (rendering_window ())#notebook in
618 let output = ((rendering_window ())#output : GMathView.math_view) in
619 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
620 let savedproof = !ProofEngine.proof in
621 let savedgoal = !ProofEngine.goal in
625 refresh_sequent notebook ;
628 RefreshSequentException e ->
629 output_html outputhtml
630 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
631 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
632 ProofEngine.proof := savedproof ;
633 ProofEngine.goal := savedgoal ;
634 refresh_sequent notebook
635 | RefreshProofException e ->
636 output_html outputhtml
637 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
638 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
639 ProofEngine.proof := savedproof ;
640 ProofEngine.goal := savedgoal ;
641 refresh_sequent notebook ;
644 output_html outputhtml
645 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
646 ProofEngine.proof := savedproof ;
647 ProofEngine.goal := savedgoal ;
651 let call_tactic_with_input tactic () =
652 let notebook = (rendering_window ())#notebook in
653 let output = ((rendering_window ())#output : GMathView.math_view) in
654 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
655 let inputt = ((rendering_window ())#inputt : GEdit.text) in
656 let savedproof = !ProofEngine.proof in
657 let savedgoal = !ProofEngine.goal in
658 (*CSC: Gran cut&paste da sotto... *)
659 let inputlen = inputt#length in
660 let input = inputt#get_chars 0 inputlen ^ "\n" in
661 let lexbuf = Lexing.from_string input in
663 match !ProofEngine.proof with
665 | Some (curi,_,_,_) -> curi
667 let uri,metasenv,bo,ty =
668 match !ProofEngine.proof with
670 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
672 let canonical_context =
673 match !ProofEngine.goal with
676 let (_,canonical_context,_) =
677 List.find (function (m,_,_) -> m=metano) metasenv
691 CicTextualParserContext.main context metasenv CicTextualLexer.token
692 lexbuf register_alias
695 | Some (dom,mk_metasenv_and_expr) ->
696 let (metasenv',expr) =
697 disambiguate_input canonical_context metasenv dom
700 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
702 refresh_sequent notebook ;
706 CicTextualParser0.Eof ->
707 inputt#delete_text 0 inputlen
708 | RefreshSequentException e ->
709 output_html outputhtml
710 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
711 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
712 ProofEngine.proof := savedproof ;
713 ProofEngine.goal := savedgoal ;
714 refresh_sequent notebook
715 | RefreshProofException e ->
716 output_html outputhtml
717 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
718 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
719 ProofEngine.proof := savedproof ;
720 ProofEngine.goal := savedgoal ;
721 refresh_sequent notebook ;
724 output_html outputhtml
725 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
726 ProofEngine.proof := savedproof ;
727 ProofEngine.goal := savedgoal ;
730 let call_tactic_with_goal_input tactic () =
731 let module L = LogicalOperations in
732 let module G = Gdome in
733 let notebook = (rendering_window ())#notebook in
734 let output = ((rendering_window ())#output : GMathView.math_view) in
735 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
736 let savedproof = !ProofEngine.proof in
737 let savedgoal = !ProofEngine.goal in
738 match notebook#proofw#get_selection with
741 ((node : Gdome.element)#getAttributeNS
743 ~localName:(G.domString "xref"))#to_string
745 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
749 match !current_goal_infos with
750 Some (ids_to_terms, ids_to_father_ids,_) ->
752 tactic (Hashtbl.find ids_to_terms id) ;
753 refresh_sequent notebook ;
755 | None -> assert false (* "ERROR: No current term!!!" *)
757 RefreshSequentException e ->
758 output_html outputhtml
759 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
760 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
761 ProofEngine.proof := savedproof ;
762 ProofEngine.goal := savedgoal ;
763 refresh_sequent notebook
764 | RefreshProofException e ->
765 output_html outputhtml
766 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
767 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
768 ProofEngine.proof := savedproof ;
769 ProofEngine.goal := savedgoal ;
770 refresh_sequent notebook ;
773 output_html outputhtml
774 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
775 ProofEngine.proof := savedproof ;
776 ProofEngine.goal := savedgoal ;
779 output_html outputhtml
780 ("<h1 color=\"red\">No term selected</h1>")
783 let call_tactic_with_input_and_goal_input tactic () =
784 let module L = LogicalOperations in
785 let module G = Gdome in
786 let notebook = (rendering_window ())#notebook in
787 let output = ((rendering_window ())#output : GMathView.math_view) in
788 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
789 let inputt = ((rendering_window ())#inputt : GEdit.text) in
790 let savedproof = !ProofEngine.proof in
791 let savedgoal = !ProofEngine.goal in
792 match notebook#proofw#get_selection with
795 ((node : Gdome.element)#getAttributeNS
797 ~localName:(G.domString "xref"))#to_string
799 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
803 match !current_goal_infos with
804 Some (ids_to_terms, ids_to_father_ids,_) ->
806 (* Let's parse the input *)
807 let inputlen = inputt#length in
808 let input = inputt#get_chars 0 inputlen ^ "\n" in
809 let lexbuf = Lexing.from_string input in
811 match !ProofEngine.proof with
813 | Some (curi,_,_,_) -> curi
815 let uri,metasenv,bo,ty =
816 match !ProofEngine.proof with
818 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
820 let canonical_context =
821 match !ProofEngine.goal with
824 let (_,canonical_context,_) =
825 List.find (function (m,_,_) -> m=metano) metasenv
839 CicTextualParserContext.main context metasenv
840 CicTextualLexer.token lexbuf register_alias
843 | Some (dom,mk_metasenv_and_expr) ->
844 let (metasenv',expr) =
845 disambiguate_input canonical_context metasenv dom
848 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
849 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
851 refresh_sequent notebook ;
855 CicTextualParser0.Eof ->
856 inputt#delete_text 0 inputlen
858 | None -> assert false (* "ERROR: No current term!!!" *)
860 RefreshSequentException e ->
861 output_html outputhtml
862 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
863 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
864 ProofEngine.proof := savedproof ;
865 ProofEngine.goal := savedgoal ;
866 refresh_sequent notebook
867 | RefreshProofException e ->
868 output_html outputhtml
869 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
870 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
871 ProofEngine.proof := savedproof ;
872 ProofEngine.goal := savedgoal ;
873 refresh_sequent notebook ;
876 output_html outputhtml
877 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
878 ProofEngine.proof := savedproof ;
879 ProofEngine.goal := savedgoal ;
882 output_html outputhtml
883 ("<h1 color=\"red\">No term selected</h1>")
886 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
887 let module L = LogicalOperations in
888 let module G = Gdome in
889 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
890 let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
891 let savedproof = !ProofEngine.proof in
892 let savedgoal = !ProofEngine.goal in
893 match mmlwidget#get_selection with
896 ((node : Gdome.element)#getAttributeNS
898 ~localName:(G.domString "xref"))#to_string
900 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
904 match !current_scratch_infos with
905 (* term is the whole goal in the scratch_area *)
906 Some (term,ids_to_terms, ids_to_father_ids,_) ->
908 let expr = tactic term (Hashtbl.find ids_to_terms id) in
909 let mml = mml_of_cic_term 111 expr in
910 scratch_window#show () ;
911 scratch_window#mmlwidget#load_tree ~dom:mml
912 | None -> assert false (* "ERROR: No current term!!!" *)
915 output_html outputhtml
916 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
919 output_html outputhtml
920 ("<h1 color=\"red\">No term selected</h1>")
923 let call_tactic_with_hypothesis_input tactic () =
924 let module L = LogicalOperations in
925 let module G = Gdome in
926 let notebook = (rendering_window ())#notebook in
927 let output = ((rendering_window ())#output : GMathView.math_view) in
928 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
929 let savedproof = !ProofEngine.proof in
930 let savedgoal = !ProofEngine.goal in
931 match notebook#proofw#get_selection with
934 ((node : Gdome.element)#getAttributeNS
936 ~localName:(G.domString "xref"))#to_string
938 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
942 match !current_goal_infos with
943 Some (_,_,ids_to_hypotheses) ->
945 tactic (Hashtbl.find ids_to_hypotheses id) ;
946 refresh_sequent notebook ;
948 | None -> assert false (* "ERROR: No current term!!!" *)
950 RefreshSequentException e ->
951 output_html outputhtml
952 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
953 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
954 ProofEngine.proof := savedproof ;
955 ProofEngine.goal := savedgoal ;
956 refresh_sequent notebook
957 | RefreshProofException e ->
958 output_html outputhtml
959 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
960 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
961 ProofEngine.proof := savedproof ;
962 ProofEngine.goal := savedgoal ;
963 refresh_sequent notebook ;
966 output_html outputhtml
967 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
968 ProofEngine.proof := savedproof ;
969 ProofEngine.goal := savedgoal ;
972 output_html outputhtml
973 ("<h1 color=\"red\">No term selected</h1>")
977 let intros = call_tactic ProofEngine.intros;;
978 let exact = call_tactic_with_input ProofEngine.exact;;
979 let apply = call_tactic_with_input ProofEngine.apply;;
980 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
981 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
982 let whd = call_tactic_with_goal_input ProofEngine.whd;;
983 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
984 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
985 let fold = call_tactic_with_input ProofEngine.fold;;
986 let cut = call_tactic_with_input ProofEngine.cut;;
987 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
988 let letin = call_tactic_with_input ProofEngine.letin;;
989 let ring = call_tactic ProofEngine.ring;;
990 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
991 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
992 let fourier = call_tactic ProofEngine.fourier;;
993 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
994 let reflexivity = call_tactic ProofEngine.reflexivity;;
995 let symmetry = call_tactic ProofEngine.symmetry;;
996 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
997 let left = call_tactic ProofEngine.left;;
998 let right = call_tactic ProofEngine.right;;
999 let assumption = call_tactic ProofEngine.assumption;;
1001 let whd_in_scratch scratch_window =
1002 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1005 let reduce_in_scratch scratch_window =
1006 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1009 let simpl_in_scratch scratch_window =
1010 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1016 (**********************)
1017 (* END OF TACTICS *)
1018 (**********************)
1020 exception OpenConjecturesStillThere;;
1021 exception WrongProof;;
1024 match !ProofEngine.proof with
1025 None -> assert false
1026 | Some (uri,[],bo,ty) ->
1028 CicReduction.are_convertible []
1029 (CicTypeChecker.type_of_aux' [] [] bo) ty
1032 (*CSC: Wrong: [] is just plainly wrong *)
1033 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
1035 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1036 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1038 Cic2acic.acic_object_of_cic_object proof
1041 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
1043 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
1044 current_cic_infos :=
1046 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
1051 | _ -> raise OpenConjecturesStillThere
1055 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
1056 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
1058 let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
1061 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1062 match !ProofEngine.proof with
1063 None -> assert false
1064 | Some (uri, metasenv, bo, ty) ->
1066 (*CSC: Wrong: [] is just plainly wrong *)
1067 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
1069 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
1070 Cic2acic.acic_object_of_cic_object currentproof
1073 match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
1074 xml,Some bodyxml -> xml,bodyxml
1075 | _,None -> assert false
1077 Xml.pp ~quiet:true xml (Some prooffiletype) ;
1078 output_html outputhtml
1079 ("<h1 color=\"Green\">Current proof type saved to " ^
1080 prooffiletype ^ "</h1>") ;
1081 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
1082 output_html outputhtml
1083 ("<h1 color=\"Green\">Current proof body saved to " ^
1084 prooffile ^ "</h1>")
1087 (* Used to typecheck the loaded proofs *)
1088 let typecheck_loaded_proof metasenv bo ty =
1089 let module T = CicTypeChecker in
1092 (fun metasenv ((_,context,ty) as conj) ->
1093 ignore (T.type_of_aux' metasenv context ty) ;
1096 ignore (T.type_of_aux' metasenv [] ty) ;
1097 ignore (T.type_of_aux' metasenv [] bo)
1101 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1102 let output = ((rendering_window ())#output : GMathView.math_view) in
1103 let notebook = (rendering_window ())#notebook in
1105 let uri = UriManager.uri_of_string "cic:/dummy.con" in
1106 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
1107 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
1108 typecheck_loaded_proof metasenv bo ty ;
1109 ProofEngine.proof :=
1110 Some (uri, metasenv, bo, ty) ;
1112 (match metasenv with
1114 | (metano,_,_)::_ -> Some metano
1116 refresh_proof output ;
1117 refresh_sequent notebook ;
1118 output_html outputhtml
1119 ("<h1 color=\"Green\">Current proof type loaded from " ^
1120 prooffiletype ^ "</h1>") ;
1121 output_html outputhtml
1122 ("<h1 color=\"Green\">Current proof body loaded from " ^
1123 prooffile ^ "</h1>")
1126 RefreshSequentException e ->
1127 output_html outputhtml
1128 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1129 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1130 | RefreshProofException e ->
1131 output_html outputhtml
1132 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1133 "proof: " ^ Printexc.to_string e ^ "</h1>")
1135 output_html outputhtml
1136 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1139 let edit_aliases () =
1140 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1141 let dom,resolve_id = !id_to_uris in
1142 let inputlen = inputt#length in
1143 inputt#delete_text 0 inputlen ;
1145 inputt#insert_text ~pos:0
1150 match resolve_id v with
1151 None -> assert false
1154 "alias " ^ v ^ " " ^
1155 (string_of_cic_textual_parser_uri uri)
1158 id_to_uris := empty_id_to_uris
1162 let module L = LogicalOperations in
1163 let module G = Gdome in
1164 let notebook = (rendering_window ())#notebook in
1165 let output = (rendering_window ())#output in
1166 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1167 match (rendering_window ())#output#get_selection with
1170 ((node : Gdome.element)#getAttributeNS
1171 (*CSC: OCAML DIVERGE
1172 ((element : G.element)#getAttributeNS
1174 ~namespaceURI:helmns
1175 ~localName:(G.domString "xref"))#to_string
1177 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1181 match !current_cic_infos with
1182 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1184 L.to_sequent id ids_to_terms ids_to_father_ids ;
1185 refresh_proof output ;
1186 refresh_sequent notebook
1187 | None -> assert false (* "ERROR: No current term!!!" *)
1189 RefreshSequentException e ->
1190 output_html outputhtml
1191 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1192 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1193 | RefreshProofException e ->
1194 output_html outputhtml
1195 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1196 "proof: " ^ Printexc.to_string e ^ "</h1>")
1198 output_html outputhtml
1199 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1201 | None -> assert false (* "ERROR: No selection!!!" *)
1205 let module L = LogicalOperations in
1206 let module G = Gdome in
1207 let notebook = (rendering_window ())#notebook in
1208 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1209 match (rendering_window ())#output#get_selection with
1212 ((node : Gdome.element)#getAttributeNS
1213 (*CSC: OCAML DIVERGE
1214 ((element : G.element)#getAttributeNS
1216 ~namespaceURI:helmns
1217 ~localName:(G.domString "xref"))#to_string
1219 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1223 match !current_cic_infos with
1224 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1226 L.focus id ids_to_terms ids_to_father_ids ;
1227 refresh_sequent notebook
1228 | None -> assert false (* "ERROR: No current term!!!" *)
1230 RefreshSequentException e ->
1231 output_html outputhtml
1232 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1233 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1234 | RefreshProofException e ->
1235 output_html outputhtml
1236 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1237 "proof: " ^ Printexc.to_string e ^ "</h1>")
1239 output_html outputhtml
1240 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1242 | None -> assert false (* "ERROR: No selection!!!" *)
1245 exception NoPrevGoal;;
1246 exception NoNextGoal;;
1248 let setgoal metano =
1249 let module L = LogicalOperations in
1250 let module G = Gdome in
1251 let notebook = (rendering_window ())#notebook in
1252 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1254 match !ProofEngine.proof with
1255 None -> assert false
1256 | Some (_,metasenv,_,_) -> metasenv
1259 ProofEngine.goal := Some metano ;
1260 refresh_sequent ~empty_notebook:false notebook ;
1262 RefreshSequentException e ->
1263 output_html outputhtml
1264 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1265 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1267 output_html outputhtml
1268 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1271 exception NotADefinition;;
1274 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1275 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1276 let output = ((rendering_window ())#output : GMathView.math_view) in
1277 let notebook = (rendering_window ())#notebook in
1278 let inputlen = inputt#length in
1279 let input = inputt#get_chars 0 inputlen in
1281 let uri = UriManager.uri_of_string ("cic:" ^ input) in
1282 CicTypeChecker.typecheck uri ;
1283 let metasenv,bo,ty =
1284 match CicEnvironment.get_cooked_obj uri with
1285 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1286 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1289 | Cic.InductiveDefinition _ -> raise NotADefinition
1291 ProofEngine.proof :=
1292 Some (uri, metasenv, bo, ty) ;
1293 ProofEngine.goal := None ;
1294 refresh_sequent notebook ;
1295 refresh_proof output ;
1296 inputt#delete_text 0 inputlen
1298 RefreshSequentException e ->
1299 output_html outputhtml
1300 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1301 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1302 | RefreshProofException e ->
1303 output_html outputhtml
1304 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1305 "proof: " ^ Printexc.to_string e ^ "</h1>")
1307 output_html outputhtml
1308 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1312 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1313 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1314 let output = ((rendering_window ())#output : GMathView.math_view) in
1315 let notebook = (rendering_window ())#notebook in
1316 let inputlen = inputt#length in
1317 let input = inputt#get_chars 0 inputlen ^ "\n" in
1318 (* Do something interesting *)
1319 let lexbuf = Lexing.from_string input in
1322 (* Execute the actions *)
1324 CicTextualParserContext.main [] [] CicTextualLexer.token
1325 lexbuf register_alias
1328 | Some (dom,mk_metasenv_and_expr) ->
1330 disambiguate_input [] [] dom mk_metasenv_and_expr
1332 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1333 ProofEngine.proof :=
1334 Some (UriManager.uri_of_string "cic:/dummy.con",
1335 (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1336 ProofEngine.goal := Some 1 ;
1337 refresh_sequent notebook ;
1338 refresh_proof output ;
1341 CicTextualParser0.Eof ->
1342 inputt#delete_text 0 inputlen
1343 | RefreshSequentException e ->
1344 output_html outputhtml
1345 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1346 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1347 | RefreshProofException e ->
1348 output_html outputhtml
1349 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1350 "proof: " ^ Printexc.to_string e ^ "</h1>")
1352 output_html outputhtml
1353 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1356 let check_term_in_scratch scratch_window metasenv context expr =
1358 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1359 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1360 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1361 scratch_window#show () ;
1362 scratch_window#mmlwidget#load_tree ~dom:mml
1365 print_endline ("? " ^ CicPp.ppterm expr) ;
1369 let check scratch_window () =
1370 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1371 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1372 let inputlen = inputt#length in
1373 let input = inputt#get_chars 0 inputlen ^ "\n" in
1375 match !ProofEngine.proof with
1376 None -> UriManager.uri_of_string "cic:/dummy.con", []
1377 | Some (curi,metasenv,_,_) -> curi,metasenv
1379 let context,names_context =
1381 match !ProofEngine.goal with
1384 let (_,canonical_context,_) =
1385 List.find (function (m,_,_) -> m=metano) metasenv
1392 Some (n,_) -> Some n
1396 let lexbuf = Lexing.from_string input in
1399 (* Execute the actions *)
1401 CicTextualParserContext.main names_context metasenv CicTextualLexer.token
1402 lexbuf register_alias
1405 | Some (dom,mk_metasenv_and_expr) ->
1406 let (metasenv',expr) =
1407 disambiguate_input context metasenv dom mk_metasenv_and_expr
1409 check_term_in_scratch scratch_window metasenv' context expr
1412 CicTextualParser0.Eof -> ()
1414 output_html outputhtml
1415 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1418 exception NoObjectsLocated;;
1420 let user_uri_choice ~title ~msg uris =
1423 [] -> raise NoObjectsLocated
1426 interactive_user_uri_choice ~title ~msg uris
1428 String.sub uri 4 (String.length uri - 4)
1432 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1433 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1434 let inputlen = inputt#length in
1435 let input = inputt#get_chars 0 inputlen in
1437 match Str.split (Str.regexp "[ \t]+") input with
1440 inputt#delete_text 0 inputlen ;
1441 let result = MQueryGenerator.locate head in
1444 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1446 let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1447 output_html outputhtml html ;
1449 user_uri_choice ~title:"Ambiguous input."
1451 ("Ambiguous input \"" ^ head ^
1452 "\". Please, choose one interpetation:")
1455 ignore ((inputt#insert_text uri') ~pos:0)
1458 output_html outputhtml
1459 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1462 let searchPattern () =
1463 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1464 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1465 let inputlen = inputt#length in
1466 let input = inputt#get_chars 0 inputlen in
1467 let level = int_of_string input in
1469 match !ProofEngine.proof with
1470 None -> assert false
1471 | Some (_,metasenv,_,_) -> metasenv
1474 match !ProofEngine.goal with
1477 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1478 let result = MQueryGenerator.searchPattern metasenv ey ty level in
1481 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1484 " <h1>Backward Query: </h1>" ^
1485 " <h2>Levels: </h2> " ^
1486 MQueryGenerator.string_of_levels
1487 (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1488 " <pre>" ^ get_last_query result ^ "</pre>"
1490 output_html outputhtml html ;
1492 let rec filter_out =
1496 let tl',exc = filter_out tl in
1499 ProofEngine.can_apply
1500 (term_of_cic_textual_parser_uri
1501 (cic_textual_parser_uri_of_string uri))
1509 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1510 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1517 " <h1>Objects that can actually be applied: </h1> " ^
1518 String.concat "<br>" uris' ^ exc ^
1519 " <h1>Number of false matches: " ^
1520 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1521 " <h1>Number of good matches: " ^
1522 string_of_int (List.length uris') ^ "</h1>"
1524 output_html outputhtml html' ;
1526 user_uri_choice ~title:"Ambiguous input."
1527 ~msg:"Many lemmas can be successfully applied. Please, choose one:"
1530 inputt#delete_text 0 inputlen ;
1531 ignore ((inputt#insert_text uri') ~pos:0)
1534 output_html outputhtml
1535 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1538 let choose_selection
1539 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1541 let module G = Gdome in
1542 let rec aux element =
1543 if element#hasAttributeNS
1544 ~namespaceURI:helmns
1545 ~localName:(G.domString "xref")
1547 mmlwidget#set_selection (Some element)
1549 match element#get_parentNode with
1550 None -> assert false
1551 (*CSC: OCAML DIVERGES!
1552 | Some p -> aux (new G.element_of_node p)
1554 | Some p -> aux (new Gdome.element_of_node p)
1558 | None -> mmlwidget#set_selection None
1561 (* STUFF TO BUILD THE GTK INTERFACE *)
1563 (* Stuff for the widget settings *)
1565 let export_to_postscript (output : GMathView.math_view) =
1566 let lastdir = ref (Unix.getcwd ()) in
1569 GToolbox.select_file ~title:"Export to PostScript"
1570 ~dir:lastdir ~filename:"screenshot.ps" ()
1574 output#export_to_postscript ~filename:filename ();
1577 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1578 button_set_kerning button_set_transparency export_to_postscript_menu_item
1581 let is_set = button_t1#active in
1582 output#set_font_manager_type
1583 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1586 button_set_anti_aliasing#misc#set_sensitive true ;
1587 button_set_kerning#misc#set_sensitive true ;
1588 button_set_transparency#misc#set_sensitive true ;
1589 export_to_postscript_menu_item#misc#set_sensitive true ;
1593 button_set_anti_aliasing#misc#set_sensitive false ;
1594 button_set_kerning#misc#set_sensitive false ;
1595 button_set_transparency#misc#set_sensitive false ;
1596 export_to_postscript_menu_item#misc#set_sensitive false ;
1600 let set_anti_aliasing output button_set_anti_aliasing () =
1601 output#set_anti_aliasing button_set_anti_aliasing#active
1604 let set_kerning output button_set_kerning () =
1605 output#set_kerning button_set_kerning#active
1608 let set_transparency output button_set_transparency () =
1609 output#set_transparency button_set_transparency#active
1612 let changefont output font_size_spinb () =
1613 output#set_font_size font_size_spinb#value_as_int
1616 let set_log_verbosity output log_verbosity_spinb () =
1617 output#set_log_verbosity log_verbosity_spinb#value_as_int
1620 class settings_window (output : GMathView.math_view) sw
1621 export_to_postscript_menu_item selection_changed_callback
1623 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1625 GPack.vbox ~packing:settings_window#add () in
1628 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1629 ~border_width:5 ~packing:vbox#add () in
1631 GButton.toggle_button ~label:"activate t1 fonts"
1632 ~packing:(table#attach ~left:0 ~top:0) () in
1633 let button_set_anti_aliasing =
1634 GButton.toggle_button ~label:"set_anti_aliasing"
1635 ~packing:(table#attach ~left:0 ~top:1) () in
1636 let button_set_kerning =
1637 GButton.toggle_button ~label:"set_kerning"
1638 ~packing:(table#attach ~left:1 ~top:1) () in
1639 let button_set_transparency =
1640 GButton.toggle_button ~label:"set_transparency"
1641 ~packing:(table#attach ~left:2 ~top:1) () in
1644 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1645 ~border_width:5 ~packing:vbox#add () in
1646 let font_size_label =
1647 GMisc.label ~text:"font size:"
1648 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1649 let font_size_spinb =
1651 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1654 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1655 let log_verbosity_label =
1656 GMisc.label ~text:"log verbosity:"
1657 ~packing:(table#attach ~left:0 ~top:1) () in
1658 let log_verbosity_spinb =
1660 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1663 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1665 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1667 GButton.button ~label:"Close"
1668 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1670 method show = settings_window#show
1672 button_set_anti_aliasing#misc#set_sensitive false ;
1673 button_set_kerning#misc#set_sensitive false ;
1674 button_set_transparency#misc#set_sensitive false ;
1675 (* Signals connection *)
1676 ignore(button_t1#connect#clicked
1677 (activate_t1 output button_set_anti_aliasing button_set_kerning
1678 button_set_transparency export_to_postscript_menu_item button_t1)) ;
1679 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1680 ignore(button_set_anti_aliasing#connect#toggled
1681 (set_anti_aliasing output button_set_anti_aliasing));
1682 ignore(button_set_kerning#connect#toggled
1683 (set_kerning output button_set_kerning)) ;
1684 ignore(button_set_transparency#connect#toggled
1685 (set_transparency output button_set_transparency)) ;
1686 ignore(log_verbosity_spinb#connect#changed
1687 (set_log_verbosity output log_verbosity_spinb)) ;
1688 ignore(closeb#connect#clicked settings_window#misc#hide)
1691 (* Scratch window *)
1693 class scratch_window outputhtml =
1695 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1697 GPack.vbox ~packing:window#add () in
1699 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1701 GButton.button ~label:"Whd"
1702 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1704 GButton.button ~label:"Reduce"
1705 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1707 GButton.button ~label:"Simpl"
1708 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1709 let scrolled_window =
1710 GBin.scrolled_window ~border_width:10
1711 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1714 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1716 method outputhtml = outputhtml
1717 method mmlwidget = mmlwidget
1718 method show () = window#misc#hide () ; window#show ()
1720 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1721 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1722 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1723 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1724 ignore(simplb#connect#clicked (simpl_in_scratch self))
1728 let vbox1 = GPack.vbox () in
1729 let scrolled_window1 =
1730 GBin.scrolled_window ~border_width:10
1731 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1733 GMathView.math_view ~width:400 ~height:275
1734 ~packing:(scrolled_window1#add) () in
1736 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1738 GButton.button ~label:"Exact"
1739 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1741 GButton.button ~label:"Intros"
1742 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1744 GButton.button ~label:"Apply"
1745 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1746 let elimsimplintrosb =
1747 GButton.button ~label:"ElimSimplIntros"
1748 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1750 GButton.button ~label:"ElimType"
1751 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1753 GButton.button ~label:"Whd"
1754 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1756 GButton.button ~label:"Reduce"
1757 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1759 GButton.button ~label:"Simpl"
1760 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1762 GButton.button ~label:"Fold"
1763 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1765 GButton.button ~label:"Cut"
1766 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1768 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1770 GButton.button ~label:"Change"
1771 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1773 GButton.button ~label:"Let ... In"
1774 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1776 GButton.button ~label:"Ring"
1777 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1779 GButton.button ~label:"ClearBody"
1780 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1782 GButton.button ~label:"Clear"
1783 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1785 GButton.button ~label:"Fourier"
1786 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1788 GButton.button ~label:"RewriteSimpl ->"
1789 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1791 GButton.button ~label:"Reflexivity"
1792 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1794 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1796 GButton.button ~label:"Symmetry"
1797 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1799 GButton.button ~label:"Transitivity"
1800 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1802 GButton.button ~label:"Left"
1803 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1805 GButton.button ~label:"Right"
1806 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1808 GButton.button ~label:"Assumption"
1809 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1811 method proofw = proofw
1812 method content = vbox1
1814 ignore(exactb#connect#clicked exact) ;
1815 ignore(applyb#connect#clicked apply) ;
1816 ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
1817 ignore(elimtypeb#connect#clicked elimtype) ;
1818 ignore(whdb#connect#clicked whd) ;
1819 ignore(reduceb#connect#clicked reduce) ;
1820 ignore(simplb#connect#clicked simpl) ;
1821 ignore(foldb#connect#clicked fold) ;
1822 ignore(cutb#connect#clicked cut) ;
1823 ignore(changeb#connect#clicked change) ;
1824 ignore(letinb#connect#clicked letin) ;
1825 ignore(ringb#connect#clicked ring) ;
1826 ignore(clearbodyb#connect#clicked clearbody) ;
1827 ignore(clearb#connect#clicked clear) ;
1828 ignore(fourierb#connect#clicked fourier) ;
1829 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
1830 ignore(reflexivityb#connect#clicked reflexivity) ;
1831 ignore(symmetryb#connect#clicked symmetry) ;
1832 ignore(transitivityb#connect#clicked transitivity) ;
1833 ignore(leftb#connect#clicked left) ;
1834 ignore(rightb#connect#clicked right) ;
1835 ignore(assumptionb#connect#clicked assumption) ;
1836 ignore(introsb#connect#clicked intros) ;
1838 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1844 val notebook = GPack.notebook ()
1846 val mutable skip_switch_page_event = false
1847 method notebook = notebook
1849 let new_page = new page () in
1850 pages := !pages @ [n,new_page] ;
1851 notebook#append_page
1852 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
1853 new_page#content#coerce
1854 method remove_all_pages =
1855 List.iter (function _ -> notebook#remove_page 0) !pages ;
1857 method set_current_page n =
1858 let (_,page) = List.find (function (m,_) -> m=n) !pages in
1859 let new_page = notebook#page_num page#content#coerce in
1860 if new_page <> notebook#current_page then
1861 skip_switch_page_event <- true ;
1862 notebook#goto_page new_page
1863 method set_empty_page = self#add_page (-1)
1865 (snd (List.nth !pages notebook#current_page))#proofw
1868 (notebook#connect#switch_page
1870 let skip = skip_switch_page_event in
1871 skip_switch_page_event <- false ;
1874 let metano = fst (List.nth !pages i) in
1883 class rendering_window output (notebook : notebook) =
1885 GWindow.window ~title:"MathML viewer" ~border_width:2
1886 ~allow_shrink:false () in
1887 let vbox_for_menu = GPack.vbox ~packing:window#add () in
1889 let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
1890 let factory0 = new GMenu.factory menubar in
1891 let accel_group = factory0#accel_group in
1893 let file_menu = factory0#add_submenu "File" in
1894 let factory1 = new GMenu.factory file_menu ~accel_group in
1895 let export_to_postscript_menu_item =
1898 (factory1#add_item "Load" ~key:GdkKeysyms._L ~callback:load) ;
1899 ignore (factory1#add_item "Save" ~key:GdkKeysyms._S ~callback:save) ;
1900 ignore (factory1#add_separator ()) ;
1901 let export_to_postscript_menu_item =
1902 factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
1903 ~callback:(export_to_postscript output) in
1904 ignore (factory1#add_separator ()) ;
1906 (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
1907 export_to_postscript_menu_item
1910 let edit_menu = factory0#add_submenu "Edit" in
1911 let factory2 = new GMenu.factory edit_menu ~accel_group in
1912 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
1913 let proveit_menu_item =
1914 factory2#add_item "Prove It" ~key:GdkKeysyms._I
1915 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
1917 let focus_menu_item =
1918 factory2#add_item "Focus" ~key:GdkKeysyms._F
1919 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
1922 focus_and_proveit_set_sensitive :=
1924 proveit_menu_item#misc#set_sensitive b ;
1925 focus_menu_item#misc#set_sensitive b
1927 let _ = factory2#add_separator () in
1928 let _ = factory2#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
1929 let _ = !focus_and_proveit_set_sensitive false in
1931 let settings_menu = factory0#add_submenu "Settings" in
1932 let factory3 = new GMenu.factory settings_menu ~accel_group in
1934 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
1935 ~callback:edit_aliases in
1936 let _ = factory3#add_separator () in
1938 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
1939 ~callback:(function _ -> (settings_window ())#show ()) in
1941 let _ = window#add_accel_group accel_group in
1945 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
1947 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1948 let scrolled_window0 =
1949 GBin.scrolled_window ~border_width:10
1950 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1951 let _ = scrolled_window0#add output#coerce in
1953 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1955 GButton.button ~label:"State"
1956 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1958 GButton.button ~label:"Open"
1959 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1961 GButton.button ~label:"Check"
1962 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1964 GButton.button ~label:"Locate"
1965 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1966 let searchpatternb =
1967 GButton.button ~label:"SearchPattern"
1968 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1969 let scrolled_window1 =
1970 GBin.scrolled_window ~border_width:10
1971 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1972 let inputt = GEdit.text ~editable:true ~width:400 ~height:100
1973 ~packing:scrolled_window1#add () in
1975 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1977 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
1978 let frame = GBin.frame ~packing:(vboxl#pack ~expand:true ~padding:5) () in
1981 ~source:"<html><body bgColor=\"white\"></body></html>"
1982 ~width:400 ~height: 100
1986 let scratch_window = new scratch_window outputhtml in
1988 method outputhtml = outputhtml
1989 method inputt = inputt
1990 method output = (output : GMathView.math_view)
1991 method notebook = notebook
1992 method show = window#show
1994 notebook#set_empty_page ;
1995 export_to_postscript_menu_item#misc#set_sensitive false ;
1996 check_term := (check_term_in_scratch scratch_window) ;
1998 (* signal handlers here *)
1999 ignore(output#connect#selection_changed
2001 notebook#proofw#unload ;
2002 choose_selection output elem ;
2003 !focus_and_proveit_set_sensitive true
2005 let settings_window = new settings_window output scrolled_window0
2006 export_to_postscript_menu_item (choose_selection output) in
2007 set_settings_window settings_window ;
2008 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2009 ignore(stateb#connect#clicked state) ;
2010 ignore(openb#connect#clicked open_) ;
2011 ignore(checkb#connect#clicked (check scratch_window)) ;
2012 ignore(locateb#connect#clicked locate) ;
2013 ignore(searchpatternb#connect#clicked searchPattern) ;
2014 Logger.log_callback :=
2015 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2020 let initialize_everything () =
2021 let module U = Unix in
2022 let output = GMathView.math_view ~width:350 ~height:280 () in
2023 let notebook = new notebook in
2024 let rendering_window' = new rendering_window output notebook in
2025 set_rendering_window rendering_window' ;
2026 rendering_window'#show () ;
2032 Mqint.init "dbname=helm_mowgli" ;
2033 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2034 ignore (GtkMain.Main.init ()) ;
2035 initialize_everything () ;
2036 if !usedb then Mqint.close ();