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";;
80 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
82 let htmlheader_and_content = ref htmlheader;;
84 let current_cic_infos = ref None;;
85 let current_goal_infos = ref None;;
86 let current_scratch_infos = ref None;;
88 let id_to_uris = ref ([],function _ -> None);;
90 let check_term = ref (fun _ _ _ -> assert false);;
92 exception RenderingWindowsNotInitialized;;
94 let set_rendering_window,rendering_window =
95 let rendering_window_ref = ref None in
96 (function rw -> rendering_window_ref := Some rw),
98 match !rendering_window_ref with
99 None -> raise RenderingWindowsNotInitialized
105 (* COMMAND LINE OPTIONS *)
111 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
114 Arg.parse argspec ignore ""
119 let cic_textual_parser_uri_of_uri uri' =
121 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
122 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
124 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
125 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
129 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
130 CicTextualParser0.IndTyUri (uri'',typeno)
133 (* Constructor of an Inductive Type *)
134 let uri'',typeno,consno =
135 CicTextualLexer.indconuri_of_uri uri'
137 CicTextualParser0.IndConUri (uri'',typeno,consno)
142 let term_of_uri uri =
143 let module C = Cic in
144 let module CTP = CicTextualParser0 in
145 match (cic_textual_parser_uri_of_uri uri) with
146 CTP.ConUri uri -> C.Const (uri,[])
147 | CTP.VarUri uri -> C.Var (uri,[])
148 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
149 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
152 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
156 let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris =
157 let choice = ref None in
158 let window = GWindow.dialog ~modal:true ~title () in
160 GMisc.label ~text:msg ~packing:window#vbox#add () in
161 let vbox = GPack.vbox ~border_width:10
162 ~packing:(window#action_area#pack ~expand:true ~padding:4) () in
163 let hbox1 = GPack.hbox ~border_width:10 ~packing:vbox#add () in
165 GEdit.combo ~popdown_strings:uris ~packing:hbox1#add () in
167 GButton.button ~label:"Check"
168 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
169 let hbox = GPack.hbox ~border_width:10 ~packing:vbox#add () in
171 GButton.button ~label:"Ok"
172 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
174 GButton.button ~label:cancel
175 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
178 choice := Some combo#entry#text ;
181 let check_callback () = !check_term [] [] (term_of_uri combo#entry#text) in
182 ignore (window#connect#destroy GMain.Main.quit) ;
183 ignore (cancelb#connect#clicked window#destroy) ;
184 ignore (okb#connect#clicked ok_callback) ;
185 ignore (checkb#connect#clicked check_callback) ;
186 window#set_position `CENTER ;
190 None -> raise NoChoice
196 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
198 let query = ref "" in
199 MQueryGenerator.set_confirm_query
200 (function q -> query := MQueryUtil.text_of_query q ; true) ;
201 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
204 let register_alias (id,uri) =
205 let dom,resolve_id = !id_to_uris in
207 (if List.mem id dom then dom else id::dom),
208 function id' -> if id' = id then Some uri else resolve_id id'
211 let output_html outputhtml msg =
212 htmlheader_and_content := !htmlheader_and_content ^ msg ;
213 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
214 outputhtml#set_topline (-1)
217 let locate_one_id id =
218 let result = MQueryGenerator.locate id in
222 wrong_xpointer_format_from_wrong_xpointer_format' uri
224 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
225 output_html (rendering_window ())#outputhtml html ;
230 (GToolbox.input_string ~title:"Unknown input"
231 ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
233 None -> raise NoChoice
234 | Some uri -> ["cic:" ^ uri]
239 [interactive_user_uri_choice
240 ~cancel:"Try every possibility."
241 ~title:"Ambiguous input."
243 ("Ambiguous input \"" ^ id ^
244 "\". Please, choose one interpretation:")
250 List.map cic_textual_parser_uri_of_uri uris'
253 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
254 exception AmbiguousInput;;
256 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
257 let known_ids,resolve_id = !id_to_uris in
263 if List.mem he known_ids then filter tl else he::(filter tl)
267 (* for each id in dom' we get the list of uris associated to it *)
268 let list_of_uris = List.map locate_one_id dom' in
269 (* and now we compute the list of all possible assignments from id to uris *)
271 let rec aux ids list_of_uris =
272 match ids,list_of_uris with
273 [],[] -> [resolve_id]
274 | id::idtl,uris::uristl ->
275 let resolves = aux idtl uristl in
281 function id' -> if id = id' then Some uri else f id'
285 | _,_ -> assert false
287 aux dom' list_of_uris
289 prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ;
290 (* now we select only the ones that generates well-typed terms *)
296 let metasenv',expr = mk_metasenv_and_expr resolve in
298 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
300 (CicTypeChecker.type_of_aux' metasenv context expr) ;
308 match resolve_ids' with
309 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
310 | [resolve_id] -> resolve_id
319 match resolve id with
323 CicTextualParser0.ConUri uri
324 | CicTextualParser0.VarUri uri ->
325 UriManager.string_of_uri uri
326 | CicTextualParser0.IndTyUri (uri,tyno) ->
327 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
328 string_of_int (tyno+1) ^ ")"
329 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
330 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
331 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
337 GToolbox.question_box ~title:"Ambiguous input."
339 ~default:1 "Ambiguous input. Please, choose one interpretation."
342 List.nth resolve_ids' (choice - 1)
344 (* No choice from the user *)
347 id_to_uris := known_ids @ dom', resolve_id' ;
348 mk_metasenv_and_expr resolve_id'
351 let domImpl = Gdome.domImplementation ();;
353 let parseStyle name =
355 domImpl#createDocumentFromURI
357 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
359 ~uri:("styles/" ^ name) ()
361 Gdome_xslt.processStylesheet style
364 let d_c = parseStyle "drop_coercions.xsl";;
365 let tc1 = parseStyle "objtheorycontent.xsl";;
366 let hc2 = parseStyle "content_to_html.xsl";;
367 let l = parseStyle "link.xsl";;
369 let c1 = parseStyle "rootcontent.xsl";;
370 let g = parseStyle "genmmlid.xsl";;
371 let c2 = parseStyle "annotatedpres.xsl";;
374 let getterURL = Configuration.getter_url;;
375 let processorURL = Configuration.processor_url;;
377 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
379 ["processorURL", "'" ^ processorURL ^ "'" ;
380 "getterURL", "'" ^ getterURL ^ "'" ;
381 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
382 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
383 "UNICODEvsSYMBOL", "'symbol'" ;
384 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
385 "encoding", "'iso-8859-1'" ;
386 "media-type", "'text/html'" ;
387 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
388 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
389 "naturalLanguage", "'yes'" ;
390 "annotations", "'no'" ;
391 "explodeall", "'true()'" ;
392 "topurl", "'http://phd.cs.unibo.it/helm'" ;
393 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
396 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
398 ["processorURL", "'" ^ processorURL ^ "'" ;
399 "getterURL", "'" ^ getterURL ^ "'" ;
400 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
401 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
402 "UNICODEvsSYMBOL", "'symbol'" ;
403 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
404 "encoding", "'iso-8859-1'" ;
405 "media-type", "'text/html'" ;
406 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
407 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
408 "naturalLanguage", "'no'" ;
409 "annotations", "'no'" ;
410 "explodeall", "'true()'" ;
411 "topurl", "'http://phd.cs.unibo.it/helm'" ;
412 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
415 let parse_file filename =
416 let inch = open_in filename in
417 let rec read_lines () =
419 let line = input_line inch in
427 let applyStylesheets input styles args =
428 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
432 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
433 (*CSC: ????????????????? *)
435 Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
438 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
443 None -> Xml2Gdome.document_of_xml domImpl xml
445 Xml.pp xml (Some constanttypefile) ;
446 Xml2Gdome.document_of_xml domImpl bodyxml'
448 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
449 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
451 Xml.pp xmlinnertypes (Some innertypesfile) ;
452 let output = applyStylesheets input mml_styles mml_args in
459 exception RefreshSequentException of exn;;
460 exception RefreshProofException of exn;;
462 let refresh_proof (output : GMathView.math_view) =
464 let uri,currentproof =
465 match !ProofEngine.proof with
467 | Some (uri,metasenv,bo,ty) ->
468 (*CSC: Wrong: [] is just plainly wrong *)
469 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
472 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
473 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
475 Cic2acic.acic_object_of_cic_object currentproof
478 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
480 output#load_tree mml ;
482 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
485 match !ProofEngine.proof with
487 | Some (uri,metasenv,bo,ty) ->
488 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
489 raise (RefreshProofException e)
492 let refresh_sequent ?(empty_notebook=true) notebook =
494 match !ProofEngine.goal with
496 if empty_notebook then
498 notebook#remove_all_pages ;
499 notebook#set_empty_page
502 notebook#proofw#unload
505 match !ProofEngine.proof with
507 | Some (_,metasenv,_,_) -> metasenv
509 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
510 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
511 SequentPp.XmlPp.print_sequent metasenv currentsequent
514 Xml2Gdome.document_of_xml domImpl sequent_gdome
517 applyStylesheets sequent_doc sequent_styles sequent_args
519 if empty_notebook then
521 notebook#remove_all_pages ;
522 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
524 notebook#set_current_page metano ;
525 notebook#proofw#load_tree ~dom:sequent_mml ;
526 current_goal_infos :=
527 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
531 match !ProofEngine.goal with
536 match !ProofEngine.proof with
538 | Some (_,metasenv,_,_) -> metasenv
540 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
541 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
542 raise (RefreshSequentException e)
546 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
547 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
550 let mml_of_cic_term metano term =
552 match !ProofEngine.proof with
554 | Some (_,metasenv,_,_) -> metasenv
557 match !ProofEngine.goal with
560 let (_,canonical_context,_) =
561 List.find (function (m,_,_) -> m=metano) metasenv
565 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
566 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
569 Xml2Gdome.document_of_xml domImpl sequent_gdome
572 applyStylesheets sequent_doc sequent_styles sequent_args ;
574 current_scratch_infos :=
575 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
579 (***********************)
581 (***********************)
583 let call_tactic tactic () =
584 let notebook = (rendering_window ())#notebook in
585 let output = ((rendering_window ())#output : GMathView.math_view) in
586 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
587 let savedproof = !ProofEngine.proof in
588 let savedgoal = !ProofEngine.goal in
592 refresh_sequent notebook ;
595 RefreshSequentException e ->
596 output_html outputhtml
597 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
598 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
599 ProofEngine.proof := savedproof ;
600 ProofEngine.goal := savedgoal ;
601 refresh_sequent notebook
602 | RefreshProofException e ->
603 output_html outputhtml
604 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
605 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
606 ProofEngine.proof := savedproof ;
607 ProofEngine.goal := savedgoal ;
608 refresh_sequent notebook ;
611 output_html outputhtml
612 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
613 ProofEngine.proof := savedproof ;
614 ProofEngine.goal := savedgoal ;
618 let call_tactic_with_input tactic () =
619 let notebook = (rendering_window ())#notebook in
620 let output = ((rendering_window ())#output : GMathView.math_view) in
621 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
622 let inputt = ((rendering_window ())#inputt : GEdit.text) in
623 let savedproof = !ProofEngine.proof in
624 let savedgoal = !ProofEngine.goal in
625 (*CSC: Gran cut&paste da sotto... *)
626 let inputlen = inputt#length in
627 let input = inputt#get_chars 0 inputlen ^ "\n" in
628 let lexbuf = Lexing.from_string input in
630 match !ProofEngine.proof with
632 | Some (curi,_,_,_) -> curi
634 let uri,metasenv,bo,ty =
635 match !ProofEngine.proof with
637 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
639 let canonical_context =
640 match !ProofEngine.goal with
643 let (_,canonical_context,_) =
644 List.find (function (m,_,_) -> m=metano) metasenv
658 CicTextualParserContext.main context metasenv CicTextualLexer.token
659 lexbuf register_alias
662 | Some (dom,mk_metasenv_and_expr) ->
663 let (metasenv',expr) =
664 disambiguate_input canonical_context metasenv dom
667 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
669 refresh_sequent notebook ;
673 CicTextualParser0.Eof ->
674 inputt#delete_text 0 inputlen
675 | RefreshSequentException e ->
676 output_html outputhtml
677 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
678 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
679 ProofEngine.proof := savedproof ;
680 ProofEngine.goal := savedgoal ;
681 refresh_sequent notebook
682 | RefreshProofException e ->
683 output_html outputhtml
684 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
685 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
686 ProofEngine.proof := savedproof ;
687 ProofEngine.goal := savedgoal ;
688 refresh_sequent notebook ;
691 output_html outputhtml
692 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
693 ProofEngine.proof := savedproof ;
694 ProofEngine.goal := savedgoal ;
697 let call_tactic_with_goal_input tactic () =
698 let module L = LogicalOperations in
699 let module G = Gdome in
700 let notebook = (rendering_window ())#notebook in
701 let output = ((rendering_window ())#output : GMathView.math_view) in
702 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
703 let savedproof = !ProofEngine.proof in
704 let savedgoal = !ProofEngine.goal in
705 match notebook#proofw#get_selection with
708 ((node : Gdome.element)#getAttributeNS
710 ~localName:(G.domString "xref"))#to_string
712 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
716 match !current_goal_infos with
717 Some (ids_to_terms, ids_to_father_ids,_) ->
719 tactic (Hashtbl.find ids_to_terms id) ;
720 refresh_sequent notebook ;
722 | None -> assert false (* "ERROR: No current term!!!" *)
724 RefreshSequentException e ->
725 output_html outputhtml
726 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
727 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
728 ProofEngine.proof := savedproof ;
729 ProofEngine.goal := savedgoal ;
730 refresh_sequent notebook
731 | RefreshProofException e ->
732 output_html outputhtml
733 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
734 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
735 ProofEngine.proof := savedproof ;
736 ProofEngine.goal := savedgoal ;
737 refresh_sequent notebook ;
740 output_html outputhtml
741 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
742 ProofEngine.proof := savedproof ;
743 ProofEngine.goal := savedgoal ;
746 output_html outputhtml
747 ("<h1 color=\"red\">No term selected</h1>")
750 let call_tactic_with_input_and_goal_input tactic () =
751 let module L = LogicalOperations in
752 let module G = Gdome in
753 let notebook = (rendering_window ())#notebook in
754 let output = ((rendering_window ())#output : GMathView.math_view) in
755 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
756 let inputt = ((rendering_window ())#inputt : GEdit.text) in
757 let savedproof = !ProofEngine.proof in
758 let savedgoal = !ProofEngine.goal in
759 match notebook#proofw#get_selection with
762 ((node : Gdome.element)#getAttributeNS
764 ~localName:(G.domString "xref"))#to_string
766 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
770 match !current_goal_infos with
771 Some (ids_to_terms, ids_to_father_ids,_) ->
773 (* Let's parse the input *)
774 let inputlen = inputt#length in
775 let input = inputt#get_chars 0 inputlen ^ "\n" in
776 let lexbuf = Lexing.from_string input in
778 match !ProofEngine.proof with
780 | Some (curi,_,_,_) -> curi
782 let uri,metasenv,bo,ty =
783 match !ProofEngine.proof with
785 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
787 let canonical_context =
788 match !ProofEngine.goal with
791 let (_,canonical_context,_) =
792 List.find (function (m,_,_) -> m=metano) metasenv
806 CicTextualParserContext.main context metasenv
807 CicTextualLexer.token lexbuf register_alias
810 | Some (dom,mk_metasenv_and_expr) ->
811 let (metasenv',expr) =
812 disambiguate_input canonical_context metasenv dom
815 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
816 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
818 refresh_sequent notebook ;
822 CicTextualParser0.Eof ->
823 inputt#delete_text 0 inputlen
825 | None -> assert false (* "ERROR: No current term!!!" *)
827 RefreshSequentException e ->
828 output_html outputhtml
829 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
830 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
831 ProofEngine.proof := savedproof ;
832 ProofEngine.goal := savedgoal ;
833 refresh_sequent notebook
834 | RefreshProofException e ->
835 output_html outputhtml
836 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
837 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
838 ProofEngine.proof := savedproof ;
839 ProofEngine.goal := savedgoal ;
840 refresh_sequent notebook ;
843 output_html outputhtml
844 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
845 ProofEngine.proof := savedproof ;
846 ProofEngine.goal := savedgoal ;
849 output_html outputhtml
850 ("<h1 color=\"red\">No term selected</h1>")
853 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
854 let module L = LogicalOperations in
855 let module G = Gdome in
856 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
857 let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
858 let savedproof = !ProofEngine.proof in
859 let savedgoal = !ProofEngine.goal in
860 match mmlwidget#get_selection with
863 ((node : Gdome.element)#getAttributeNS
865 ~localName:(G.domString "xref"))#to_string
867 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
871 match !current_scratch_infos with
872 (* term is the whole goal in the scratch_area *)
873 Some (term,ids_to_terms, ids_to_father_ids,_) ->
875 let expr = tactic term (Hashtbl.find ids_to_terms id) in
876 let mml = mml_of_cic_term 111 expr in
877 scratch_window#show () ;
878 scratch_window#mmlwidget#load_tree ~dom:mml
879 | None -> assert false (* "ERROR: No current term!!!" *)
882 output_html outputhtml
883 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
886 output_html outputhtml
887 ("<h1 color=\"red\">No term selected</h1>")
890 let call_tactic_with_hypothesis_input tactic () =
891 let module L = LogicalOperations in
892 let module G = Gdome in
893 let notebook = (rendering_window ())#notebook in
894 let output = ((rendering_window ())#output : GMathView.math_view) in
895 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
896 let savedproof = !ProofEngine.proof in
897 let savedgoal = !ProofEngine.goal in
898 match notebook#proofw#get_selection with
901 ((node : Gdome.element)#getAttributeNS
903 ~localName:(G.domString "xref"))#to_string
905 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
909 match !current_goal_infos with
910 Some (_,_,ids_to_hypotheses) ->
912 tactic (Hashtbl.find ids_to_hypotheses id) ;
913 refresh_sequent notebook ;
915 | None -> assert false (* "ERROR: No current term!!!" *)
917 RefreshSequentException e ->
918 output_html outputhtml
919 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
920 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
921 ProofEngine.proof := savedproof ;
922 ProofEngine.goal := savedgoal ;
923 refresh_sequent notebook
924 | RefreshProofException e ->
925 output_html outputhtml
926 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
927 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
928 ProofEngine.proof := savedproof ;
929 ProofEngine.goal := savedgoal ;
930 refresh_sequent notebook ;
933 output_html outputhtml
934 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
935 ProofEngine.proof := savedproof ;
936 ProofEngine.goal := savedgoal ;
939 output_html outputhtml
940 ("<h1 color=\"red\">No term selected</h1>")
944 let intros = call_tactic ProofEngine.intros;;
945 let exact = call_tactic_with_input ProofEngine.exact;;
946 let apply = call_tactic_with_input ProofEngine.apply;;
947 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
948 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
949 let whd = call_tactic_with_goal_input ProofEngine.whd;;
950 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
951 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
952 let fold = call_tactic_with_input ProofEngine.fold;;
953 let cut = call_tactic_with_input ProofEngine.cut;;
954 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
955 let letin = call_tactic_with_input ProofEngine.letin;;
956 let ring = call_tactic ProofEngine.ring;;
957 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
958 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
959 let fourier = call_tactic ProofEngine.fourier;;
960 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
961 let reflexivity = call_tactic ProofEngine.reflexivity;;
962 let symmetry = call_tactic ProofEngine.symmetry;;
963 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
964 let left = call_tactic ProofEngine.left;;
965 let right = call_tactic ProofEngine.right;;
966 let assumption = call_tactic ProofEngine.assumption;;
968 let whd_in_scratch scratch_window =
969 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
972 let reduce_in_scratch scratch_window =
973 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
976 let simpl_in_scratch scratch_window =
977 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
983 (**********************)
985 (**********************)
987 exception OpenConjecturesStillThere;;
988 exception WrongProof;;
991 match !ProofEngine.proof with
993 | Some (uri,[],bo,ty) ->
995 CicReduction.are_convertible []
996 (CicTypeChecker.type_of_aux' [] [] bo) ty
999 (*CSC: Wrong: [] is just plainly wrong *)
1000 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
1002 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1003 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1005 Cic2acic.acic_object_of_cic_object proof
1008 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
1010 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
1011 current_cic_infos :=
1013 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
1018 | _ -> raise OpenConjecturesStillThere
1022 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
1023 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
1025 let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
1028 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1029 match !ProofEngine.proof with
1030 None -> assert false
1031 | Some (uri, metasenv, bo, ty) ->
1033 (*CSC: Wrong: [] is just plainly wrong *)
1034 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
1036 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
1037 Cic2acic.acic_object_of_cic_object currentproof
1040 match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
1041 xml,Some bodyxml -> xml,bodyxml
1042 | _,None -> assert false
1044 Xml.pp ~quiet:true xml (Some prooffiletype) ;
1045 output_html outputhtml
1046 ("<h1 color=\"Green\">Current proof type saved to " ^
1047 prooffiletype ^ "</h1>") ;
1048 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
1049 output_html outputhtml
1050 ("<h1 color=\"Green\">Current proof body saved to " ^
1051 prooffile ^ "</h1>")
1054 (* Used to typecheck the loaded proofs *)
1055 let typecheck_loaded_proof metasenv bo ty =
1056 let module T = CicTypeChecker in
1059 (fun metasenv ((_,context,ty) as conj) ->
1060 ignore (T.type_of_aux' metasenv context ty) ;
1063 ignore (T.type_of_aux' metasenv [] ty) ;
1064 ignore (T.type_of_aux' metasenv [] bo)
1068 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1069 let output = ((rendering_window ())#output : GMathView.math_view) in
1070 let notebook = (rendering_window ())#notebook in
1072 let uri = UriManager.uri_of_string "cic:/dummy.con" in
1073 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
1074 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
1075 typecheck_loaded_proof metasenv bo ty ;
1076 ProofEngine.proof :=
1077 Some (uri, metasenv, bo, ty) ;
1079 (match metasenv with
1081 | (metano,_,_)::_ -> Some metano
1083 refresh_proof output ;
1084 refresh_sequent notebook ;
1085 output_html outputhtml
1086 ("<h1 color=\"Green\">Current proof type loaded from " ^
1087 prooffiletype ^ "</h1>") ;
1088 output_html outputhtml
1089 ("<h1 color=\"Green\">Current proof body loaded from " ^
1090 prooffile ^ "</h1>")
1093 RefreshSequentException e ->
1094 output_html outputhtml
1095 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1096 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1097 | RefreshProofException e ->
1098 output_html outputhtml
1099 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1100 "proof: " ^ Printexc.to_string e ^ "</h1>")
1102 output_html outputhtml
1103 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1107 let module L = LogicalOperations in
1108 let module G = Gdome in
1109 let notebook = (rendering_window ())#notebook in
1110 let output = (rendering_window ())#output in
1111 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1112 match (rendering_window ())#output#get_selection with
1115 ((node : Gdome.element)#getAttributeNS
1116 (*CSC: OCAML DIVERGE
1117 ((element : G.element)#getAttributeNS
1119 ~namespaceURI:helmns
1120 ~localName:(G.domString "xref"))#to_string
1122 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1126 match !current_cic_infos with
1127 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1129 L.to_sequent id ids_to_terms ids_to_father_ids ;
1130 refresh_proof output ;
1131 refresh_sequent notebook
1132 | None -> assert false (* "ERROR: No current term!!!" *)
1134 RefreshSequentException e ->
1135 output_html outputhtml
1136 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1137 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1138 | RefreshProofException e ->
1139 output_html outputhtml
1140 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1141 "proof: " ^ Printexc.to_string e ^ "</h1>")
1143 output_html outputhtml
1144 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1146 | None -> assert false (* "ERROR: No selection!!!" *)
1150 let module L = LogicalOperations in
1151 let module G = Gdome in
1152 let notebook = (rendering_window ())#notebook in
1153 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1154 match (rendering_window ())#output#get_selection with
1157 ((node : Gdome.element)#getAttributeNS
1158 (*CSC: OCAML DIVERGE
1159 ((element : G.element)#getAttributeNS
1161 ~namespaceURI:helmns
1162 ~localName:(G.domString "xref"))#to_string
1164 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1168 match !current_cic_infos with
1169 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1171 L.focus id ids_to_terms ids_to_father_ids ;
1172 refresh_sequent notebook
1173 | None -> assert false (* "ERROR: No current term!!!" *)
1175 RefreshSequentException e ->
1176 output_html outputhtml
1177 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1178 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1179 | RefreshProofException e ->
1180 output_html outputhtml
1181 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1182 "proof: " ^ Printexc.to_string e ^ "</h1>")
1184 output_html outputhtml
1185 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1187 | None -> assert false (* "ERROR: No selection!!!" *)
1190 exception NoPrevGoal;;
1191 exception NoNextGoal;;
1193 let setgoal metano =
1194 let module L = LogicalOperations in
1195 let module G = Gdome in
1196 let notebook = (rendering_window ())#notebook in
1197 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1199 match !ProofEngine.proof with
1200 None -> assert false
1201 | Some (_,metasenv,_,_) -> metasenv
1204 ProofEngine.goal := Some metano ;
1205 refresh_sequent ~empty_notebook:false notebook ;
1207 RefreshSequentException e ->
1208 output_html outputhtml
1209 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1210 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1212 output_html outputhtml
1213 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1216 exception NotADefinition;;
1219 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1220 let oldinputt = ((rendering_window ())#oldinputt : GEdit.text) in
1221 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1222 let output = ((rendering_window ())#output : GMathView.math_view) in
1223 let notebook = (rendering_window ())#notebook in
1224 let inputlen = inputt#length in
1225 let input = inputt#get_chars 0 inputlen in
1227 let uri = UriManager.uri_of_string ("cic:" ^ input) in
1228 CicTypeChecker.typecheck uri ;
1229 let metasenv,bo,ty =
1230 match CicEnvironment.get_cooked_obj uri with
1231 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1232 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1235 | Cic.InductiveDefinition _ -> raise NotADefinition
1237 ProofEngine.proof :=
1238 Some (uri, metasenv, bo, ty) ;
1239 ProofEngine.goal := None ;
1240 refresh_sequent notebook ;
1241 refresh_proof output ;
1242 inputt#delete_text 0 inputlen ;
1243 ignore(oldinputt#insert_text input oldinputt#length)
1245 RefreshSequentException e ->
1246 output_html outputhtml
1247 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1248 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1249 | RefreshProofException e ->
1250 output_html outputhtml
1251 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1252 "proof: " ^ Printexc.to_string e ^ "</h1>")
1254 output_html outputhtml
1255 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1259 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1260 let oldinputt = ((rendering_window ())#oldinputt : GEdit.text) in
1261 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1262 let output = ((rendering_window ())#output : GMathView.math_view) in
1263 let notebook = (rendering_window ())#notebook in
1264 let inputlen = inputt#length in
1265 let input = inputt#get_chars 0 inputlen ^ "\n" in
1266 (* Do something interesting *)
1267 let lexbuf = Lexing.from_string input in
1270 (* Execute the actions *)
1272 CicTextualParserContext.main [] [] CicTextualLexer.token
1273 lexbuf register_alias
1276 | Some (dom,mk_metasenv_and_expr) ->
1278 disambiguate_input [] [] dom mk_metasenv_and_expr
1280 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1281 ProofEngine.proof :=
1282 Some (UriManager.uri_of_string "cic:/dummy.con",
1283 (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1284 ProofEngine.goal := Some 1 ;
1285 refresh_sequent notebook ;
1286 refresh_proof output ;
1289 CicTextualParser0.Eof ->
1290 inputt#delete_text 0 inputlen ;
1291 ignore(oldinputt#insert_text input oldinputt#length)
1292 | RefreshSequentException e ->
1293 output_html outputhtml
1294 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1295 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1296 | RefreshProofException e ->
1297 output_html outputhtml
1298 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1299 "proof: " ^ Printexc.to_string e ^ "</h1>")
1301 output_html outputhtml
1302 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1305 let check_term_in_scratch scratch_window metasenv context expr =
1307 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1308 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1309 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1310 scratch_window#show () ;
1311 scratch_window#mmlwidget#load_tree ~dom:mml
1314 print_endline ("? " ^ CicPp.ppterm expr) ;
1318 let check scratch_window () =
1319 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1320 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1321 let inputlen = inputt#length in
1322 let input = inputt#get_chars 0 inputlen ^ "\n" in
1324 match !ProofEngine.proof with
1325 None -> UriManager.uri_of_string "cic:/dummy.con", []
1326 | Some (curi,metasenv,_,_) -> curi,metasenv
1328 let context,names_context =
1330 match !ProofEngine.goal with
1333 let (_,canonical_context,_) =
1334 List.find (function (m,_,_) -> m=metano) metasenv
1341 Some (n,_) -> Some n
1345 let lexbuf = Lexing.from_string input in
1348 (* Execute the actions *)
1350 CicTextualParserContext.main names_context metasenv CicTextualLexer.token
1351 lexbuf register_alias
1354 | Some (dom,mk_metasenv_and_expr) ->
1355 let (metasenv',expr) =
1356 disambiguate_input context metasenv dom mk_metasenv_and_expr
1358 check_term_in_scratch scratch_window metasenv' context expr
1361 CicTextualParser0.Eof -> ()
1363 output_html outputhtml
1364 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1367 exception NoObjectsLocated;;
1369 let user_uri_choice ~title ~msg uris =
1372 [] -> raise NoObjectsLocated
1375 interactive_user_uri_choice ~title ~msg uris
1377 String.sub uri 4 (String.length uri - 4)
1381 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1382 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1383 let inputlen = inputt#length in
1384 let input = inputt#get_chars 0 inputlen in
1386 match Str.split (Str.regexp "[ \t]+") input with
1389 inputt#delete_text 0 inputlen ;
1390 let result = MQueryGenerator.locate head in
1393 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1395 let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1396 output_html outputhtml html ;
1398 user_uri_choice ~title:"Ambiguous input."
1400 ("Ambiguous input \"" ^ head ^
1401 "\". Please, choose one interpetation:")
1404 ignore ((inputt#insert_text uri') ~pos:0)
1407 output_html outputhtml
1408 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1411 let searchPattern () =
1412 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1413 let inputt = ((rendering_window ())#inputt : GEdit.text) in
1414 let inputlen = inputt#length in
1415 let input = inputt#get_chars 0 inputlen in
1416 let level = int_of_string input in
1418 match !ProofEngine.proof with
1419 None -> assert false
1420 | Some (_,metasenv,_,_) -> metasenv
1423 match !ProofEngine.goal with
1426 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1427 let result = MQueryGenerator.searchPattern metasenv ey ty level in
1430 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1433 " <h1>Backward Query: </h1>" ^
1434 " <h2>Levels: </h2> " ^
1435 MQueryGenerator.string_of_levels
1436 (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1437 " <pre>" ^ get_last_query result ^ "</pre>"
1439 output_html outputhtml html ;
1441 let rec filter_out =
1445 let tl',exc = filter_out tl in
1447 if ProofEngine.can_apply (term_of_uri uri) then
1454 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1455 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1462 " <h1>Objects that can actually be applied: </h1> " ^
1463 String.concat "<br>" uris' ^ exc ^
1464 " <h1>Number of false matches: " ^
1465 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1466 " <h1>Number of good matches: " ^
1467 string_of_int (List.length uris') ^ "</h1>"
1469 output_html outputhtml html' ;
1471 user_uri_choice ~title:"Ambiguous input."
1472 ~msg:"Many lemmas can be successfully applied. Please, choose one:"
1475 inputt#delete_text 0 inputlen ;
1476 ignore ((inputt#insert_text uri') ~pos:0)
1479 output_html outputhtml
1480 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1483 let choose_selection
1484 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1486 let module G = Gdome in
1487 let rec aux element =
1488 if element#hasAttributeNS
1489 ~namespaceURI:helmns
1490 ~localName:(G.domString "xref")
1492 mmlwidget#set_selection (Some element)
1494 match element#get_parentNode with
1495 None -> assert false
1496 (*CSC: OCAML DIVERGES!
1497 | Some p -> aux (new G.element_of_node p)
1499 | Some p -> aux (new Gdome.element_of_node p)
1503 | None -> mmlwidget#set_selection None
1506 (* STUFF TO BUILD THE GTK INTERFACE *)
1508 (* Stuff for the widget settings *)
1510 let export_to_postscript (output : GMathView.math_view) () =
1511 output#export_to_postscript ~filename:"output.ps" ();
1514 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1515 button_set_kerning button_set_transparency button_export_to_postscript
1518 let is_set = button_t1#active in
1519 output#set_font_manager_type
1520 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1523 button_set_anti_aliasing#misc#set_sensitive true ;
1524 button_set_kerning#misc#set_sensitive true ;
1525 button_set_transparency#misc#set_sensitive true ;
1526 button_export_to_postscript#misc#set_sensitive true ;
1530 button_set_anti_aliasing#misc#set_sensitive false ;
1531 button_set_kerning#misc#set_sensitive false ;
1532 button_set_transparency#misc#set_sensitive false ;
1533 button_export_to_postscript#misc#set_sensitive false ;
1537 let set_anti_aliasing output button_set_anti_aliasing () =
1538 output#set_anti_aliasing button_set_anti_aliasing#active
1541 let set_kerning output button_set_kerning () =
1542 output#set_kerning button_set_kerning#active
1545 let set_transparency output button_set_transparency () =
1546 output#set_transparency button_set_transparency#active
1549 let changefont output font_size_spinb () =
1550 output#set_font_size font_size_spinb#value_as_int
1553 let set_log_verbosity output log_verbosity_spinb () =
1554 output#set_log_verbosity log_verbosity_spinb#value_as_int
1557 class settings_window (output : GMathView.math_view) sw
1558 button_export_to_postscript selection_changed_callback
1560 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1562 GPack.vbox ~packing:settings_window#add () in
1565 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1566 ~border_width:5 ~packing:vbox#add () in
1568 GButton.toggle_button ~label:"activate t1 fonts"
1569 ~packing:(table#attach ~left:0 ~top:0) () in
1570 let button_set_anti_aliasing =
1571 GButton.toggle_button ~label:"set_anti_aliasing"
1572 ~packing:(table#attach ~left:0 ~top:1) () in
1573 let button_set_kerning =
1574 GButton.toggle_button ~label:"set_kerning"
1575 ~packing:(table#attach ~left:1 ~top:1) () in
1576 let button_set_transparency =
1577 GButton.toggle_button ~label:"set_transparency"
1578 ~packing:(table#attach ~left:2 ~top:1) () in
1581 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1582 ~border_width:5 ~packing:vbox#add () in
1583 let font_size_label =
1584 GMisc.label ~text:"font size:"
1585 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1586 let font_size_spinb =
1588 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1591 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1592 let log_verbosity_label =
1593 GMisc.label ~text:"log verbosity:"
1594 ~packing:(table#attach ~left:0 ~top:1) () in
1595 let log_verbosity_spinb =
1597 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1600 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1602 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1604 GButton.button ~label:"Close"
1605 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1607 method show = settings_window#show
1609 button_set_anti_aliasing#misc#set_sensitive false ;
1610 button_set_kerning#misc#set_sensitive false ;
1611 button_set_transparency#misc#set_sensitive false ;
1612 (* Signals connection *)
1613 ignore(button_t1#connect#clicked
1614 (activate_t1 output button_set_anti_aliasing button_set_kerning
1615 button_set_transparency button_export_to_postscript button_t1)) ;
1616 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1617 ignore(button_set_anti_aliasing#connect#toggled
1618 (set_anti_aliasing output button_set_anti_aliasing));
1619 ignore(button_set_kerning#connect#toggled
1620 (set_kerning output button_set_kerning)) ;
1621 ignore(button_set_transparency#connect#toggled
1622 (set_transparency output button_set_transparency)) ;
1623 ignore(log_verbosity_spinb#connect#changed
1624 (set_log_verbosity output log_verbosity_spinb)) ;
1625 ignore(closeb#connect#clicked settings_window#misc#hide)
1628 (* Scratch window *)
1630 class scratch_window outputhtml =
1632 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1634 GPack.vbox ~packing:window#add () in
1636 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1638 GButton.button ~label:"Whd"
1639 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1641 GButton.button ~label:"Reduce"
1642 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1644 GButton.button ~label:"Simpl"
1645 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1646 let scrolled_window =
1647 GBin.scrolled_window ~border_width:10
1648 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1651 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1653 method outputhtml = outputhtml
1654 method mmlwidget = mmlwidget
1655 method show () = window#misc#hide () ; window#show ()
1657 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1658 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1659 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1660 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1661 ignore(simplb#connect#clicked (simpl_in_scratch self))
1665 let vbox1 = GPack.vbox () in
1666 let scrolled_window1 =
1667 GBin.scrolled_window ~border_width:10
1668 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1670 GMathView.math_view ~width:400 ~height:275
1671 ~packing:(scrolled_window1#add) () in
1673 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1675 GButton.button ~label:"Exact"
1676 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1678 GButton.button ~label:"Intros"
1679 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1681 GButton.button ~label:"Apply"
1682 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1683 let elimsimplintrosb =
1684 GButton.button ~label:"ElimSimplIntros"
1685 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1687 GButton.button ~label:"ElimType"
1688 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1690 GButton.button ~label:"Whd"
1691 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1693 GButton.button ~label:"Reduce"
1694 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1696 GButton.button ~label:"Simpl"
1697 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1699 GButton.button ~label:"Fold"
1700 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1702 GButton.button ~label:"Cut"
1703 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1705 GButton.button ~label:"Change"
1706 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1708 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1710 GButton.button ~label:"Let ... In"
1711 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1713 GButton.button ~label:"Ring"
1714 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1716 GButton.button ~label:"ClearBody"
1717 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1719 GButton.button ~label:"Clear"
1720 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1722 GButton.button ~label:"Fourier"
1723 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1725 GButton.button ~label:"RewriteSimpl ->"
1726 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1728 GButton.button ~label:"Reflexivity"
1729 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1731 GButton.button ~label:"Symmetry"
1732 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1734 GButton.button ~label:"Transitivity"
1735 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1737 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1739 GButton.button ~label:"Left"
1740 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1742 GButton.button ~label:"Right"
1743 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1745 GButton.button ~label:"Assumption"
1746 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1748 method proofw = proofw
1749 method content = vbox1
1751 ignore(exactb#connect#clicked exact) ;
1752 ignore(applyb#connect#clicked apply) ;
1753 ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
1754 ignore(elimtypeb#connect#clicked elimtype) ;
1755 ignore(whdb#connect#clicked whd) ;
1756 ignore(reduceb#connect#clicked reduce) ;
1757 ignore(simplb#connect#clicked simpl) ;
1758 ignore(foldb#connect#clicked fold) ;
1759 ignore(cutb#connect#clicked cut) ;
1760 ignore(changeb#connect#clicked change) ;
1761 ignore(letinb#connect#clicked letin) ;
1762 ignore(ringb#connect#clicked ring) ;
1763 ignore(clearbodyb#connect#clicked clearbody) ;
1764 ignore(clearb#connect#clicked clear) ;
1765 ignore(fourierb#connect#clicked fourier) ;
1766 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
1767 ignore(reflexivityb#connect#clicked reflexivity) ;
1768 ignore(symmetryb#connect#clicked symmetry) ;
1769 ignore(transitivityb#connect#clicked transitivity) ;
1770 ignore(leftb#connect#clicked left) ;
1771 ignore(rightb#connect#clicked right) ;
1772 ignore(assumptionb#connect#clicked assumption) ;
1773 ignore(introsb#connect#clicked intros) ;
1775 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1781 val notebook = GPack.notebook ()
1783 val mutable skip_switch_page_event = false
1784 method notebook = notebook
1786 let new_page = new page () in
1787 pages := !pages @ [n,new_page] ;
1788 notebook#append_page
1789 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
1790 new_page#content#coerce
1791 method remove_all_pages =
1792 List.iter (function _ -> notebook#remove_page 0) !pages ;
1794 method set_current_page n =
1795 let (_,page) = List.find (function (m,_) -> m=n) !pages in
1796 let new_page = notebook#page_num page#content#coerce in
1797 if new_page <> notebook#current_page then
1798 skip_switch_page_event <- true ;
1799 notebook#goto_page new_page
1800 method set_empty_page = self#add_page (-1)
1802 (snd (List.nth !pages notebook#current_page))#proofw
1805 (notebook#connect#switch_page
1807 let skip = skip_switch_page_event in
1808 skip_switch_page_event <- false ;
1811 let metano = fst (List.nth !pages i) in
1820 class rendering_window output (notebook : notebook) (label : GMisc.label) =
1822 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1824 GPack.hbox ~packing:window#add () in
1826 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1827 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1828 let scrolled_window0 =
1829 GBin.scrolled_window ~border_width:10
1830 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1831 let _ = scrolled_window0#add output#coerce in
1833 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1835 GButton.button ~label:"Settings"
1836 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1837 let button_export_to_postscript =
1838 GButton.button ~label:"export_to_postscript"
1839 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1841 GButton.button ~label:"Qed"
1842 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1844 GButton.button ~label:"Save"
1845 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1847 GButton.button ~label:"Load"
1848 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1850 GButton.button ~label:"Close"
1851 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1853 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1855 GButton.button ~label:"Prove It"
1856 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1858 GButton.button ~label:"Focus"
1859 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1860 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1861 ~packing:(vbox#pack ~padding:5) () in
1863 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1865 GButton.button ~label:"State"
1866 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1868 GButton.button ~label:"Open"
1869 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1871 GButton.button ~label:"Check"
1872 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1874 GButton.button ~label:"Locate"
1875 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1876 let searchpatternb =
1877 GButton.button ~label:"SearchPattern"
1878 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1879 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1880 ~packing:(vbox#pack ~padding:5) () in
1882 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1884 vboxl#pack ~expand:false ~fill:false ~padding:5 notebook#notebook#coerce in
1887 ~source:"<html><body bgColor=\"white\"></body></html>"
1888 ~width:400 ~height: 200
1889 ~packing:(vboxl#pack ~expand:false ~fill:false ~padding:5)
1891 let scratch_window = new scratch_window outputhtml in
1893 method outputhtml = outputhtml
1894 method oldinputt = oldinputt
1895 method inputt = inputt
1896 method output = (output : GMathView.math_view)
1897 method notebook = notebook
1898 method show = window#show
1900 notebook#set_empty_page ;
1901 button_export_to_postscript#misc#set_sensitive false ;
1902 check_term := (check_term_in_scratch scratch_window) ;
1904 (* signal handlers here *)
1905 ignore(output#connect#selection_changed
1906 (function elem -> notebook#proofw#unload ; choose_selection output elem)) ;
1907 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1908 let settings_window = new settings_window output scrolled_window0
1909 button_export_to_postscript (choose_selection output) in
1910 ignore(settingsb#connect#clicked settings_window#show) ;
1911 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1912 ignore(qedb#connect#clicked qed) ;
1913 ignore(saveb#connect#clicked save) ;
1914 ignore(loadb#connect#clicked load) ;
1915 ignore(proveitb#connect#clicked proveit) ;
1916 ignore(focusb#connect#clicked focus) ;
1917 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1918 ignore(stateb#connect#clicked state) ;
1919 ignore(openb#connect#clicked open_) ;
1920 ignore(checkb#connect#clicked (check scratch_window)) ;
1921 ignore(locateb#connect#clicked locate) ;
1922 ignore(searchpatternb#connect#clicked searchPattern) ;
1923 Logger.log_callback :=
1924 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1929 let initialize_everything () =
1930 let module U = Unix in
1931 let output = GMathView.math_view ~width:350 ~height:280 () in
1932 let notebook = new notebook in
1933 let label = GMisc.label ~text:"gTopLevel" () in
1934 let rendering_window' = new rendering_window output notebook label in
1935 set_rendering_window rendering_window' ;
1936 rendering_window'#show () ;
1942 (* Mqint.init "dbname=helm_mowgli" ; *)
1943 Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ;
1944 ignore (GtkMain.Main.init ()) ;
1945 initialize_everything () ;
1946 if !usedb then Mqint.close ();