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";;
51 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
55 " <body bgColor=\"white\">"
64 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
65 let prooffile = "/public/sacerdot/currentproof";;
68 let prooffile = "/public/sacerdot/currentproof";;
69 let prooffiletype = "/public/sacerdot/currentprooftype";;
71 (*CSC: the getter should handle the innertypes, not the FS *)
73 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
74 let innertypesfile = "/public/sacerdot/innertypes";;
77 let innertypesfile = "/public/sacerdot/innertypes";;
78 let constanttypefile = "/public/sacerdot/constanttype";;
80 let empty_id_to_uris = ([],function _ -> None);;
83 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
85 let htmlheader_and_content = ref htmlheader;;
87 let current_cic_infos = ref None;;
88 let current_goal_infos = ref None;;
89 let current_scratch_infos = ref None;;
91 let id_to_uris = ref empty_id_to_uris;;
93 let check_term = ref (fun _ _ _ -> assert false);;
94 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
96 exception RenderingWindowsNotInitialized;;
98 let set_rendering_window,rendering_window =
99 let rendering_window_ref = ref None in
100 (function rw -> rendering_window_ref := Some rw),
102 match !rendering_window_ref with
103 None -> raise RenderingWindowsNotInitialized
108 exception SettingsWindowsNotInitialized;;
110 let set_settings_window,settings_window =
111 let settings_window_ref = ref None in
112 (function rw -> settings_window_ref := Some rw),
114 match !settings_window_ref with
115 None -> raise SettingsWindowsNotInitialized
120 exception OutputHtmlNotInitialized;;
122 let set_outputhtml,outputhtml =
123 let outputhtml_ref = ref None in
124 (function rw -> outputhtml_ref := Some rw),
126 match !outputhtml_ref with
127 None -> raise OutputHtmlNotInitialized
128 | Some outputhtml -> outputhtml
132 exception QedSetSensitiveNotInitialized;;
133 let qed_set_sensitive =
134 ref (function _ -> raise QedSetSensitiveNotInitialized)
137 exception SaveSetSensitiveNotInitialized;;
138 let save_set_sensitive =
139 ref (function _ -> raise SaveSetSensitiveNotInitialized)
142 (* COMMAND LINE OPTIONS *)
148 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
151 Arg.parse argspec ignore ""
153 (* A WIDGET TO ENTER CIC TERMS *)
155 class term_editor ?packing ?width ?height () =
156 let input = GEdit.text ~editable:true ?width ?height ?packing () in
158 method coerce = input#coerce
160 input#delete_text 0 input#length
161 method set_term txt =
163 ignore ((input#insert_text txt) ~pos:0)
164 method get_term ~context ~metasenv =
165 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
166 CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
172 exception IllFormedUri of string;;
174 let cic_textual_parser_uri_of_string uri' =
177 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
178 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
180 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
181 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
185 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
186 CicTextualParser0.IndTyUri (uri'',typeno)
189 (* Constructor of an Inductive Type *)
190 let uri'',typeno,consno =
191 CicTextualLexer.indconuri_of_uri uri'
193 CicTextualParser0.IndConUri (uri'',typeno,consno)
196 _ -> raise (IllFormedUri uri')
199 let term_of_cic_textual_parser_uri uri =
200 let module C = Cic in
201 let module CTP = CicTextualParser0 in
203 CTP.ConUri uri -> C.Const (uri,[])
204 | CTP.VarUri uri -> C.Var (uri,[])
205 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
206 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
209 let string_of_cic_textual_parser_uri uri =
210 let module C = Cic in
211 let module CTP = CicTextualParser0 in
214 CTP.ConUri uri -> UriManager.string_of_uri uri
215 | CTP.VarUri uri -> UriManager.string_of_uri uri
216 | CTP.IndTyUri (uri,tyno) ->
217 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
218 | CTP.IndConUri (uri,tyno,consno) ->
219 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
222 (* 4 = String.length "cic:" *)
223 String.sub uri' 4 (String.length uri' - 4)
226 let output_html outputhtml msg =
227 htmlheader_and_content := !htmlheader_and_content ^ msg ;
228 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
229 outputhtml#set_topline (-1)
232 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
236 let check_window outputhtml uris =
239 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
241 GPack.notebook ~scrollable:true ~packing:window#add () in
246 let scrolled_window =
247 GBin.scrolled_window ~border_width:10
249 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
255 ~packing:scrolled_window#add ~width:400 ~height:280 () in
258 term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
260 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
263 let mml = !mml_of_cic_term_ref 111 expr in
264 prerr_endline ("### " ^ CicPp.ppterm expr) ;
265 mmlwidget#load_tree ~dom:mml
268 output_html outputhtml
269 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
274 (notebook#connect#switch_page
275 (function i -> Lazy.force (List.nth render_terms i)))
281 interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
283 let choices = ref [] in
284 let chosen = ref false in
286 GWindow.dialog ~modal:true ~title ~width:600 () in
288 GMisc.label ~text:msg
289 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
290 let scrolled_window =
291 GBin.scrolled_window ~border_width:10
292 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
294 let expected_height = 18 * List.length uris in
295 let height = if expected_height > 400 then 400 else expected_height in
296 GList.clist ~columns:1 ~packing:scrolled_window#add
297 ~height ~selection_mode () in
298 let _ = List.map (function x -> clist#append [x]) uris in
300 GPack.hbox ~border_width:0
301 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
303 GMisc.label ~text:"None of the above. Try this one:"
304 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
306 GEdit.entry ~editable:true
307 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
309 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
311 GButton.button ~label:ok
312 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
313 let _ = okb#misc#set_sensitive false in
315 GButton.button ~label:"Check"
316 ~packing:(hbox#pack ~padding:5) () in
317 let _ = checkb#misc#set_sensitive false in
319 GButton.button ~label:"Abort"
320 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
322 let check_callback () =
323 assert (List.length !choices > 0) ;
324 check_window (outputhtml ()) !choices
326 ignore (window#connect#destroy GMain.Main.quit) ;
327 ignore (cancelb#connect#clicked window#destroy) ;
329 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
330 ignore (checkb#connect#clicked check_callback) ;
332 (clist#connect#select_row
333 (fun ~row ~column ~event ->
334 checkb#misc#set_sensitive true ;
335 okb#misc#set_sensitive true ;
336 choices := (List.nth uris row)::!choices)) ;
338 (clist#connect#unselect_row
339 (fun ~row ~column ~event ->
341 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
343 (manual_input#connect#changed
345 if manual_input#text = "" then
348 checkb#misc#set_sensitive false ;
349 okb#misc#set_sensitive false ;
350 clist#misc#set_sensitive true
354 choices := [manual_input#text] ;
355 clist#unselect_all () ;
356 checkb#misc#set_sensitive true ;
357 okb#misc#set_sensitive true ;
358 clist#misc#set_sensitive false
360 window#set_position `CENTER ;
363 if !chosen && List.length !choices > 0 then
369 let interactive_interpretation_choice interpretations =
370 let chosen = ref None in
373 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
374 let vbox = GPack.vbox ~packing:window#add () in
378 ("Ambiguous input since there are many well-typed interpretations." ^
379 " Please, choose one of them.")
380 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
382 GPack.notebook ~scrollable:true
383 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
386 (function interpretation ->
388 let expected_height = 18 * List.length interpretation in
389 let height = if expected_height > 400 then 400 else expected_height in
390 GList.clist ~columns:2 ~packing:notebook#append_page ~height
391 ~titles:["id" ; "URI"] ()
395 (function (id,uri) ->
396 let n = clist#append [id;uri] in
397 clist#set_row ~selectable:false n
400 clist#columns_autosize ()
403 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
405 GButton.button ~label:"Ok"
406 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
408 GButton.button ~label:"Abort"
409 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
411 ignore (window#connect#destroy GMain.Main.quit) ;
412 ignore (cancelb#connect#clicked window#destroy) ;
415 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
416 window#set_position `CENTER ;
420 None -> raise NoChoice
427 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
429 let query = ref "" in
430 MQueryGenerator.set_confirm_query
431 (function q -> query := MQueryUtil.text_of_query q ; true) ;
432 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
435 let domImpl = Gdome.domImplementation ();;
437 let parseStyle name =
439 domImpl#createDocumentFromURI
441 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
443 ~uri:("styles/" ^ name) ()
445 Gdome_xslt.processStylesheet style
448 let d_c = parseStyle "drop_coercions.xsl";;
449 let tc1 = parseStyle "objtheorycontent.xsl";;
450 let hc2 = parseStyle "content_to_html.xsl";;
451 let l = parseStyle "link.xsl";;
453 let c1 = parseStyle "rootcontent.xsl";;
454 let g = parseStyle "genmmlid.xsl";;
455 let c2 = parseStyle "annotatedpres.xsl";;
458 let getterURL = Configuration.getter_url;;
459 let processorURL = Configuration.processor_url;;
461 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
462 let mml_args ~explode_all =
463 ("explodeall",(if explode_all then "true()" else "false()"))::
464 ["processorURL", "'" ^ processorURL ^ "'" ;
465 "getterURL", "'" ^ getterURL ^ "'" ;
466 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
467 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
468 "UNICODEvsSYMBOL", "'symbol'" ;
469 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
470 "encoding", "'iso-8859-1'" ;
471 "media-type", "'text/html'" ;
472 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
473 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
474 "naturalLanguage", "'yes'" ;
475 "annotations", "'no'" ;
476 "URLs_or_URIs", "'URIs'" ;
477 "topurl", "'http://phd.cs.unibo.it/helm'" ;
478 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
481 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
483 ["processorURL", "'" ^ processorURL ^ "'" ;
484 "getterURL", "'" ^ getterURL ^ "'" ;
485 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
486 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
487 "UNICODEvsSYMBOL", "'symbol'" ;
488 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
489 "encoding", "'iso-8859-1'" ;
490 "media-type", "'text/html'" ;
491 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
492 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
493 "naturalLanguage", "'no'" ;
494 "annotations", "'no'" ;
495 "explodeall", "true()" ;
496 "URLs_or_URIs", "'URIs'" ;
497 "topurl", "'http://phd.cs.unibo.it/helm'" ;
498 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
501 let parse_file filename =
502 let inch = open_in filename in
503 let rec read_lines () =
505 let line = input_line inch in
513 let applyStylesheets input styles args =
514 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
519 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
521 (*CSC: ????????????????? *)
523 Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
526 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
531 None -> Xml2Gdome.document_of_xml domImpl xml
533 Xml.pp xml (Some constanttypefile) ;
534 Xml2Gdome.document_of_xml domImpl bodyxml'
536 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
537 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
539 Xml.pp xmlinnertypes (Some innertypesfile) ;
540 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
547 exception RefreshSequentException of exn;;
548 exception RefreshProofException of exn;;
550 let refresh_proof (output : GMathView.math_view) =
552 let uri,currentproof =
553 match !ProofEngine.proof with
555 | Some (uri,metasenv,bo,ty) ->
556 !qed_set_sensitive (List.length metasenv = 0) ;
557 (*CSC: Wrong: [] is just plainly wrong *)
558 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
561 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
562 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
564 Cic2acic.acic_object_of_cic_object currentproof
567 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
570 output#load_tree mml ;
572 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
575 match !ProofEngine.proof with
577 | Some (uri,metasenv,bo,ty) ->
578 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
579 raise (RefreshProofException e)
582 let refresh_sequent ?(empty_notebook=true) notebook =
584 match !ProofEngine.goal with
586 if empty_notebook then
588 notebook#remove_all_pages ~skip_switch_page_event:false ;
589 notebook#set_empty_page
592 notebook#proofw#unload
595 match !ProofEngine.proof with
597 | Some (_,metasenv,_,_) -> metasenv
599 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
600 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
601 SequentPp.XmlPp.print_sequent metasenv currentsequent
603 let regenerate_notebook () =
604 let skip_switch_page_event =
606 (m,_,_)::_ when m = metano -> false
609 notebook#remove_all_pages ~skip_switch_page_event ;
610 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
612 if empty_notebook then
614 regenerate_notebook () ;
615 notebook#set_current_page ~may_skip_switch_page_event:false metano
619 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
621 applyStylesheets sequent_doc sequent_styles sequent_args
623 notebook#set_current_page ~may_skip_switch_page_event:true metano;
624 notebook#proofw#load_tree ~dom:sequent_mml
626 current_goal_infos :=
627 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
631 match !ProofEngine.goal with
636 match !ProofEngine.proof with
638 | Some (_,metasenv,_,_) -> metasenv
641 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
642 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
643 raise (RefreshSequentException e)
644 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
648 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
649 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
652 let mml_of_cic_term metano term =
654 match !ProofEngine.proof with
656 | Some (_,metasenv,_,_) -> metasenv
659 match !ProofEngine.goal with
662 let (_,canonical_context,_) =
663 List.find (function (m,_,_) -> m=metano) metasenv
667 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
668 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
671 Xml2Gdome.document_of_xml domImpl sequent_gdome
674 applyStylesheets sequent_doc sequent_styles sequent_args ;
676 current_scratch_infos :=
677 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
681 exception OpenConjecturesStillThere;;
682 exception WrongProof;;
685 match !ProofEngine.proof with
687 | Some (uri,[],bo,ty) ->
689 CicReduction.are_convertible []
690 (CicTypeChecker.type_of_aux' [] [] bo) ty
693 (*CSC: Wrong: [] is just plainly wrong *)
694 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
696 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
697 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
699 Cic2acic.acic_object_of_cic_object proof
702 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
705 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
708 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
713 | _ -> raise OpenConjecturesStillThere
717 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
718 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
720 let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
723 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
724 match !ProofEngine.proof with
726 | Some (uri, metasenv, bo, ty) ->
728 (*CSC: Wrong: [] is just plainly wrong *)
729 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
731 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
732 Cic2acic.acic_object_of_cic_object currentproof
735 match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
736 xml,Some bodyxml -> xml,bodyxml
737 | _,None -> assert false
739 Xml.pp ~quiet:true xml (Some prooffiletype) ;
740 output_html outputhtml
741 ("<h1 color=\"Green\">Current proof type saved to " ^
742 prooffiletype ^ "</h1>") ;
743 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
744 output_html outputhtml
745 ("<h1 color=\"Green\">Current proof body saved to " ^
749 (* Used to typecheck the loaded proofs *)
750 let typecheck_loaded_proof metasenv bo ty =
751 let module T = CicTypeChecker in
754 (fun metasenv ((_,context,ty) as conj) ->
755 ignore (T.type_of_aux' metasenv context ty) ;
758 ignore (T.type_of_aux' metasenv [] ty) ;
759 ignore (T.type_of_aux' metasenv [] bo)
763 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
764 let output = ((rendering_window ())#output : GMathView.math_view) in
765 let notebook = (rendering_window ())#notebook in
767 let uri = UriManager.uri_of_string "cic:/dummy.con" in
768 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
769 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
770 typecheck_loaded_proof metasenv bo ty ;
772 Some (uri, metasenv, bo, ty) ;
776 | (metano,_,_)::_ -> Some metano
778 refresh_proof output ;
779 refresh_sequent notebook ;
780 output_html outputhtml
781 ("<h1 color=\"Green\">Current proof type loaded from " ^
782 prooffiletype ^ "</h1>") ;
783 output_html outputhtml
784 ("<h1 color=\"Green\">Current proof body loaded from " ^
785 prooffile ^ "</h1>") ;
786 !save_set_sensitive true
789 RefreshSequentException e ->
790 output_html outputhtml
791 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
792 "sequent: " ^ Printexc.to_string e ^ "</h1>")
793 | RefreshProofException e ->
794 output_html outputhtml
795 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
796 "proof: " ^ Printexc.to_string e ^ "</h1>")
798 output_html outputhtml
799 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
802 let edit_aliases () =
803 let chosen = ref false in
806 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
808 GPack.vbox ~border_width:0 ~packing:window#add () in
809 let scrolled_window =
810 GBin.scrolled_window ~border_width:10
811 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
812 let input = GEdit.text ~editable:true ~width:400 ~height:100
813 ~packing:scrolled_window#add () in
815 GPack.hbox ~border_width:0
816 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
818 GButton.button ~label:"Ok"
819 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
821 GButton.button ~label:"Cancel"
822 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
823 ignore (window#connect#destroy GMain.Main.quit) ;
824 ignore (cancelb#connect#clicked window#destroy) ;
826 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
827 let dom,resolve_id = !id_to_uris in
829 (input#insert_text ~pos:0
834 match resolve_id v with
839 (string_of_cic_textual_parser_uri uri)
845 let inputtext = input#get_chars 0 input#length in
847 let alfa = "[a-zA-Z_-]" in
848 let digit = "[0-9]" in
849 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
850 let blanks = "\( \|\t\|\n\)+" in
851 let nonblanks = "[^ \t\n]+" in
852 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
854 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
858 let n' = Str.search_forward regexpr inputtext n in
859 let id = Str.matched_group 2 inputtext in
861 cic_textual_parser_uri_of_string
862 ("cic:" ^ (Str.matched_group 5 inputtext))
864 let dom,resolve_id = aux (n' + 1) in
865 if List.mem id dom then
869 (function id' -> if id = id' then Some uri else resolve_id id')
871 Not_found -> empty_id_to_uris
875 id_to_uris := dom,resolve_id
879 let module L = LogicalOperations in
880 let module G = Gdome in
881 let notebook = (rendering_window ())#notebook in
882 let output = (rendering_window ())#output in
883 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
884 match (rendering_window ())#output#get_selection with
887 ((node : Gdome.element)#getAttributeNS
889 ((element : G.element)#getAttributeNS
892 ~localName:(G.domString "xref"))#to_string
894 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
898 match !current_cic_infos with
899 Some (ids_to_terms, ids_to_father_ids, _, _) ->
901 L.to_sequent id ids_to_terms ids_to_father_ids ;
902 refresh_proof output ;
903 refresh_sequent notebook
904 | None -> assert false (* "ERROR: No current term!!!" *)
906 RefreshSequentException e ->
907 output_html outputhtml
908 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
909 "sequent: " ^ Printexc.to_string e ^ "</h1>")
910 | RefreshProofException e ->
911 output_html outputhtml
912 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
913 "proof: " ^ Printexc.to_string e ^ "</h1>")
915 output_html outputhtml
916 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
918 | None -> assert false (* "ERROR: No selection!!!" *)
922 let module L = LogicalOperations in
923 let module G = Gdome in
924 let notebook = (rendering_window ())#notebook in
925 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
926 match (rendering_window ())#output#get_selection with
929 ((node : Gdome.element)#getAttributeNS
931 ((element : G.element)#getAttributeNS
934 ~localName:(G.domString "xref"))#to_string
936 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
940 match !current_cic_infos with
941 Some (ids_to_terms, ids_to_father_ids, _, _) ->
943 L.focus id ids_to_terms ids_to_father_ids ;
944 refresh_sequent notebook
945 | None -> assert false (* "ERROR: No current term!!!" *)
947 RefreshSequentException e ->
948 output_html outputhtml
949 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
950 "sequent: " ^ Printexc.to_string e ^ "</h1>")
951 | RefreshProofException e ->
952 output_html outputhtml
953 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
954 "proof: " ^ Printexc.to_string e ^ "</h1>")
956 output_html outputhtml
957 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
959 | None -> assert false (* "ERROR: No selection!!!" *)
962 exception NoPrevGoal;;
963 exception NoNextGoal;;
966 let module L = LogicalOperations in
967 let module G = Gdome in
968 let notebook = (rendering_window ())#notebook in
969 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
971 match !ProofEngine.proof with
973 | Some (_,metasenv,_,_) -> metasenv
976 refresh_sequent ~empty_notebook:false notebook
978 RefreshSequentException e ->
979 output_html outputhtml
980 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
981 "sequent: " ^ Printexc.to_string e ^ "</h1>")
983 output_html outputhtml
984 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
987 let show_in_show_window, show_in_show_window_callback =
989 GWindow.window ~width:800 ~border_width:2 () in
990 let scrolled_window =
991 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
993 GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
994 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
995 let href = Gdome.domString "href" in
996 let show_in_show_window uri =
997 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
999 CicTypeChecker.typecheck uri ;
1000 let obj = CicEnvironment.get_cooked_obj uri 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 obj
1008 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1011 window#set_title (UriManager.string_of_uri uri) ;
1012 window#misc#hide () ; window#show () ;
1013 mmlwidget#load_tree mml ;
1016 output_html outputhtml
1017 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1019 let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1020 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1022 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1024 show_in_show_window (UriManager.uri_of_string uri)
1026 if mmlwidget#get_action <> None then
1027 mmlwidget#action_toggle
1030 mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1032 show_in_show_window, show_in_show_window_callback
1035 exception NoObjectsLocated;;
1037 let user_uri_choice ~title ~msg uris =
1040 [] -> raise NoObjectsLocated
1044 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1049 String.sub uri 4 (String.length uri - 4)
1052 let locate_callback id =
1053 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1054 let result = MQueryGenerator.locate id in
1057 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1060 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1062 output_html outputhtml html ;
1063 user_uri_choice ~title:"Ambiguous input."
1065 ("Ambiguous input \"" ^ id ^
1066 "\". Please, choose one interpetation:")
1071 let inputt = ((rendering_window ())#inputt : term_editor) in
1072 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1075 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1077 None -> raise NoChoice
1079 let uri = locate_callback input in
1083 output_html outputhtml
1084 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1087 let input_or_locate_uri ~title =
1088 let uri = ref None in
1091 ~width:400 ~modal:true ~title ~border_width:2 () in
1092 let vbox = GPack.vbox ~packing:window#add () in
1094 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1096 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1098 GEdit.entry ~editable:true
1099 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1101 GButton.button ~label:"Check"
1102 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1103 let _ = checkb#misc#set_sensitive false in
1105 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1107 GMisc.label ~text:"You can also enter an indentifier to locate:"
1108 ~packing:(hbox2#pack ~padding:5) () in
1110 GEdit.entry ~editable:true
1111 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1113 GButton.button ~label:"Locate"
1114 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1115 let _ = locateb#misc#set_sensitive false in
1117 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1119 GButton.button ~label:"Ok"
1120 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1121 let _ = okb#misc#set_sensitive false in
1123 GButton.button ~label:"Cancel"
1124 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1126 ignore (window#connect#destroy GMain.Main.quit) ;
1128 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1129 let check_callback () =
1130 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1131 let uri = "cic:" ^ manual_input#text in
1133 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1134 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1137 Getter.Unresolved ->
1138 output_html outputhtml
1139 ("<h1 color=\"Red\">URI " ^ uri ^
1140 " does not correspond to any object.</h1>") ;
1142 | UriManager.IllFormedUri _ ->
1143 output_html outputhtml
1144 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1147 output_html outputhtml
1148 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1152 (okb#connect#clicked
1154 if check_callback () then
1156 uri := Some manual_input#text ;
1160 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1162 (manual_input#connect#changed
1164 if manual_input#text = "" then
1166 checkb#misc#set_sensitive false ;
1167 okb#misc#set_sensitive false
1171 checkb#misc#set_sensitive true ;
1172 okb#misc#set_sensitive true
1175 (locate_input#connect#changed
1176 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1178 (locateb#connect#clicked
1180 let id = locate_input#text in
1181 manual_input#set_text (locate_callback id) ;
1182 locate_input#delete_text 0 (String.length id)
1185 GMain.Main.main () ;
1187 None -> raise NoChoice
1188 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1191 let locate_one_id id =
1192 let result = MQueryGenerator.locate id in
1196 wrong_xpointer_format_from_wrong_xpointer_format' uri
1198 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1199 output_html (rendering_window ())#outputhtml html ;
1203 [UriManager.string_of_uri
1204 (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1207 interactive_user_uri_choice
1208 ~selection_mode:`EXTENDED
1209 ~ok:"Try every selection."
1210 ~title:"Ambiguous input."
1212 ("Ambiguous input \"" ^ id ^
1213 "\". Please, choose one or more interpretations:")
1216 List.map cic_textual_parser_uri_of_string uris'
1219 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1220 exception AmbiguousInput;;
1222 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1223 let known_ids,resolve_id = !id_to_uris in
1229 if List.mem he known_ids then filter tl else he::(filter tl)
1233 (* for each id in dom' we get the list of uris associated to it *)
1234 let list_of_uris = List.map locate_one_id dom' in
1235 (* and now we compute the list of all possible assignments from id to uris *)
1237 let rec aux ids list_of_uris =
1238 match ids,list_of_uris with
1239 [],[] -> [resolve_id]
1240 | id::idtl,uris::uristl ->
1241 let resolves = aux idtl uristl in
1247 function id' -> if id = id' then Some uri else f id'
1251 | _,_ -> assert false
1253 aux dom' list_of_uris
1255 let tests_no = List.length resolve_ids in
1256 if tests_no > 1 then
1257 output_html (outputhtml ())
1258 ("<h1>Disambiguation phase started: " ^
1259 string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1260 (* now we select only the ones that generates well-typed terms *)
1266 let metasenv',expr = mk_metasenv_and_expr resolve in
1268 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1270 (CicTypeChecker.type_of_aux' metasenv context expr) ;
1271 resolve::(filter tl)
1278 match resolve_ids' with
1279 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1280 | [resolve_id] -> resolve_id
1284 (function resolve ->
1288 match resolve id with
1289 None -> assert false
1292 CicTextualParser0.ConUri uri
1293 | CicTextualParser0.VarUri uri ->
1294 UriManager.string_of_uri uri
1295 | CicTextualParser0.IndTyUri (uri,tyno) ->
1296 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1297 string_of_int (tyno+1) ^ ")"
1298 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1299 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1300 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
1304 let index = interactive_interpretation_choice choices in
1305 List.nth resolve_ids' index
1307 id_to_uris := known_ids @ dom', resolve_id' ;
1308 mk_metasenv_and_expr resolve_id'
1312 let inputt = ((rendering_window ())#inputt : term_editor) 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
1317 let dom,mk_metasenv_and_expr = inputt#get_term [] [] in
1319 disambiguate_input [] [] dom mk_metasenv_and_expr
1321 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1322 ProofEngine.proof :=
1324 (UriManager.uri_of_string "cic:/dummy.con",
1325 (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1326 ProofEngine.goal := Some 1 ;
1327 refresh_sequent notebook ;
1328 refresh_proof output ;
1329 !save_set_sensitive true ;
1332 RefreshSequentException e ->
1333 output_html outputhtml
1334 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1335 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1336 | RefreshProofException e ->
1337 output_html outputhtml
1338 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1339 "proof: " ^ Printexc.to_string e ^ "</h1>")
1341 output_html outputhtml
1342 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1345 let check_term_in_scratch scratch_window metasenv context expr =
1347 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1348 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1349 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1350 scratch_window#show () ;
1351 scratch_window#mmlwidget#load_tree ~dom:mml
1354 print_endline ("? " ^ CicPp.ppterm expr) ;
1358 let check scratch_window () =
1359 let inputt = ((rendering_window ())#inputt : term_editor) in
1360 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1362 match !ProofEngine.proof with
1364 | Some (_,metasenv,_,_) -> metasenv
1366 let context,names_context =
1368 match !ProofEngine.goal with
1371 let (_,canonical_context,_) =
1372 List.find (function (m,_,_) -> m=metano) metasenv
1379 Some (n,_) -> Some n
1384 let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1385 let (metasenv',expr) =
1386 disambiguate_input context metasenv dom mk_metasenv_and_expr
1388 check_term_in_scratch scratch_window metasenv' context expr
1391 output_html outputhtml
1392 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1396 (***********************)
1398 (***********************)
1400 let call_tactic tactic () =
1401 let notebook = (rendering_window ())#notebook in
1402 let output = ((rendering_window ())#output : GMathView.math_view) in
1403 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1404 let savedproof = !ProofEngine.proof in
1405 let savedgoal = !ProofEngine.goal in
1409 refresh_sequent notebook ;
1410 refresh_proof output
1412 RefreshSequentException e ->
1413 output_html outputhtml
1414 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1415 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1416 ProofEngine.proof := savedproof ;
1417 ProofEngine.goal := savedgoal ;
1418 refresh_sequent notebook
1419 | RefreshProofException e ->
1420 output_html outputhtml
1421 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1422 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1423 ProofEngine.proof := savedproof ;
1424 ProofEngine.goal := savedgoal ;
1425 refresh_sequent notebook ;
1426 refresh_proof output
1428 output_html outputhtml
1429 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1430 ProofEngine.proof := savedproof ;
1431 ProofEngine.goal := savedgoal ;
1435 let call_tactic_with_input tactic () =
1436 let notebook = (rendering_window ())#notebook in
1437 let output = ((rendering_window ())#output : GMathView.math_view) in
1438 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1439 let inputt = ((rendering_window ())#inputt : term_editor) in
1440 let savedproof = !ProofEngine.proof in
1441 let savedgoal = !ProofEngine.goal in
1442 let uri,metasenv,bo,ty =
1443 match !ProofEngine.proof with
1444 None -> assert false
1445 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1447 let canonical_context =
1448 match !ProofEngine.goal with
1449 None -> assert false
1451 let (_,canonical_context,_) =
1452 List.find (function (m,_,_) -> m=metano) metasenv
1459 Some (n,_) -> Some n
1464 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
1465 let (metasenv',expr) =
1466 disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
1468 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1470 refresh_sequent notebook ;
1471 refresh_proof output ;
1474 RefreshSequentException e ->
1475 output_html outputhtml
1476 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1477 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1478 ProofEngine.proof := savedproof ;
1479 ProofEngine.goal := savedgoal ;
1480 refresh_sequent notebook
1481 | RefreshProofException e ->
1482 output_html outputhtml
1483 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1484 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1485 ProofEngine.proof := savedproof ;
1486 ProofEngine.goal := savedgoal ;
1487 refresh_sequent notebook ;
1488 refresh_proof output
1490 output_html outputhtml
1491 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1492 ProofEngine.proof := savedproof ;
1493 ProofEngine.goal := savedgoal ;
1496 let call_tactic_with_goal_input tactic () =
1497 let module L = LogicalOperations in
1498 let module G = Gdome in
1499 let notebook = (rendering_window ())#notebook in
1500 let output = ((rendering_window ())#output : GMathView.math_view) in
1501 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1502 let savedproof = !ProofEngine.proof in
1503 let savedgoal = !ProofEngine.goal in
1504 match notebook#proofw#get_selection with
1507 ((node : Gdome.element)#getAttributeNS
1508 ~namespaceURI:helmns
1509 ~localName:(G.domString "xref"))#to_string
1511 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1515 match !current_goal_infos with
1516 Some (ids_to_terms, ids_to_father_ids,_) ->
1518 tactic (Hashtbl.find ids_to_terms id) ;
1519 refresh_sequent notebook ;
1520 refresh_proof output
1521 | None -> assert false (* "ERROR: No current term!!!" *)
1523 RefreshSequentException e ->
1524 output_html outputhtml
1525 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1526 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1527 ProofEngine.proof := savedproof ;
1528 ProofEngine.goal := savedgoal ;
1529 refresh_sequent notebook
1530 | RefreshProofException e ->
1531 output_html outputhtml
1532 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1533 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1534 ProofEngine.proof := savedproof ;
1535 ProofEngine.goal := savedgoal ;
1536 refresh_sequent notebook ;
1537 refresh_proof output
1539 output_html outputhtml
1540 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1541 ProofEngine.proof := savedproof ;
1542 ProofEngine.goal := savedgoal ;
1545 output_html outputhtml
1546 ("<h1 color=\"red\">No term selected</h1>")
1549 let call_tactic_with_input_and_goal_input tactic () =
1550 let module L = LogicalOperations in
1551 let module G = Gdome in
1552 let notebook = (rendering_window ())#notebook in
1553 let output = ((rendering_window ())#output : GMathView.math_view) in
1554 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1555 let inputt = ((rendering_window ())#inputt : term_editor) in
1556 let savedproof = !ProofEngine.proof in
1557 let savedgoal = !ProofEngine.goal in
1558 match notebook#proofw#get_selection with
1561 ((node : Gdome.element)#getAttributeNS
1562 ~namespaceURI:helmns
1563 ~localName:(G.domString "xref"))#to_string
1565 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1569 match !current_goal_infos with
1570 Some (ids_to_terms, ids_to_father_ids,_) ->
1572 let uri,metasenv,bo,ty =
1573 match !ProofEngine.proof with
1574 None -> assert false
1575 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1577 let canonical_context =
1578 match !ProofEngine.goal with
1579 None -> assert false
1581 let (_,canonical_context,_) =
1582 List.find (function (m,_,_) -> m=metano) metasenv
1584 canonical_context in
1588 Some (n,_) -> Some n
1592 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
1594 let (metasenv',expr) =
1595 disambiguate_input canonical_context metasenv dom
1596 mk_metasenv_and_expr
1598 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1599 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
1601 refresh_sequent notebook ;
1602 refresh_proof output ;
1604 | None -> assert false (* "ERROR: No current term!!!" *)
1606 RefreshSequentException e ->
1607 output_html outputhtml
1608 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1609 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1610 ProofEngine.proof := savedproof ;
1611 ProofEngine.goal := savedgoal ;
1612 refresh_sequent notebook
1613 | RefreshProofException e ->
1614 output_html outputhtml
1615 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1616 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1617 ProofEngine.proof := savedproof ;
1618 ProofEngine.goal := savedgoal ;
1619 refresh_sequent notebook ;
1620 refresh_proof output
1622 output_html outputhtml
1623 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1624 ProofEngine.proof := savedproof ;
1625 ProofEngine.goal := savedgoal ;
1628 output_html outputhtml
1629 ("<h1 color=\"red\">No term selected</h1>")
1632 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
1633 let module L = LogicalOperations in
1634 let module G = Gdome in
1635 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
1636 let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
1637 let savedproof = !ProofEngine.proof in
1638 let savedgoal = !ProofEngine.goal in
1639 match mmlwidget#get_selection with
1642 ((node : Gdome.element)#getAttributeNS
1643 ~namespaceURI:helmns
1644 ~localName:(G.domString "xref"))#to_string
1646 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1650 match !current_scratch_infos with
1651 (* term is the whole goal in the scratch_area *)
1652 Some (term,ids_to_terms, ids_to_father_ids,_) ->
1654 let expr = tactic term (Hashtbl.find ids_to_terms id) in
1655 let mml = mml_of_cic_term 111 expr in
1656 scratch_window#show () ;
1657 scratch_window#mmlwidget#load_tree ~dom:mml
1658 | None -> assert false (* "ERROR: No current term!!!" *)
1661 output_html outputhtml
1662 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1665 output_html outputhtml
1666 ("<h1 color=\"red\">No term selected</h1>")
1669 let call_tactic_with_hypothesis_input tactic () =
1670 let module L = LogicalOperations in
1671 let module G = Gdome in
1672 let notebook = (rendering_window ())#notebook in
1673 let output = ((rendering_window ())#output : GMathView.math_view) in
1674 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1675 let savedproof = !ProofEngine.proof in
1676 let savedgoal = !ProofEngine.goal in
1677 match notebook#proofw#get_selection with
1680 ((node : Gdome.element)#getAttributeNS
1681 ~namespaceURI:helmns
1682 ~localName:(G.domString "xref"))#to_string
1684 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1688 match !current_goal_infos with
1689 Some (_,_,ids_to_hypotheses) ->
1691 tactic (Hashtbl.find ids_to_hypotheses id) ;
1692 refresh_sequent notebook ;
1693 refresh_proof output
1694 | None -> assert false (* "ERROR: No current term!!!" *)
1696 RefreshSequentException e ->
1697 output_html outputhtml
1698 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1699 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1700 ProofEngine.proof := savedproof ;
1701 ProofEngine.goal := savedgoal ;
1702 refresh_sequent notebook
1703 | RefreshProofException e ->
1704 output_html outputhtml
1705 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1706 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1707 ProofEngine.proof := savedproof ;
1708 ProofEngine.goal := savedgoal ;
1709 refresh_sequent notebook ;
1710 refresh_proof output
1712 output_html outputhtml
1713 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1714 ProofEngine.proof := savedproof ;
1715 ProofEngine.goal := savedgoal ;
1718 output_html outputhtml
1719 ("<h1 color=\"red\">No term selected</h1>")
1723 let intros = call_tactic ProofEngine.intros;;
1724 let exact = call_tactic_with_input ProofEngine.exact;;
1725 let apply = call_tactic_with_input ProofEngine.apply;;
1726 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
1727 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
1728 let whd = call_tactic_with_goal_input ProofEngine.whd;;
1729 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
1730 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
1731 let fold = call_tactic_with_input ProofEngine.fold;;
1732 let cut = call_tactic_with_input ProofEngine.cut;;
1733 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
1734 let letin = call_tactic_with_input ProofEngine.letin;;
1735 let ring = call_tactic ProofEngine.ring;;
1736 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
1737 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
1738 let fourier = call_tactic ProofEngine.fourier;;
1739 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
1740 let reflexivity = call_tactic ProofEngine.reflexivity;;
1741 let symmetry = call_tactic ProofEngine.symmetry;;
1742 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
1743 let left = call_tactic ProofEngine.left;;
1744 let right = call_tactic ProofEngine.right;;
1745 let assumption = call_tactic ProofEngine.assumption;;
1747 let whd_in_scratch scratch_window =
1748 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1751 let reduce_in_scratch scratch_window =
1752 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1755 let simpl_in_scratch scratch_window =
1756 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1762 (**********************)
1763 (* END OF TACTICS *)
1764 (**********************)
1768 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1770 show_in_show_window (input_or_locate_uri ~title:"Show")
1773 output_html outputhtml
1774 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1777 exception NotADefinition;;
1780 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1781 let output = ((rendering_window ())#output : GMathView.math_view) in
1782 let notebook = (rendering_window ())#notebook in
1784 let uri = input_or_locate_uri ~title:"Open" in
1785 CicTypeChecker.typecheck uri ;
1786 let metasenv,bo,ty =
1787 match CicEnvironment.get_cooked_obj uri with
1788 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1789 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1792 | Cic.InductiveDefinition _ -> raise NotADefinition
1794 ProofEngine.proof :=
1795 Some (uri, metasenv, bo, ty) ;
1796 ProofEngine.goal := None ;
1797 refresh_sequent notebook ;
1798 refresh_proof output
1800 RefreshSequentException e ->
1801 output_html outputhtml
1802 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1803 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1804 | RefreshProofException e ->
1805 output_html outputhtml
1806 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1807 "proof: " ^ Printexc.to_string e ^ "</h1>")
1809 output_html outputhtml
1810 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1814 let searchPattern () =
1815 let inputt = ((rendering_window ())#inputt : term_editor) in
1816 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1818 let rec get_level ?(last_invalid=false) () =
1820 GToolbox.input_string
1821 ~title:"Insert the strictness parameter for the query:"
1822 ((if last_invalid then
1823 "Invalid input (must be a non-negative natural number). Insert again "
1826 ) ^ "the strictness parameter for the query:")
1828 None -> raise NoChoice
1833 _ -> get_level ~last_invalid:true ()
1835 let level = get_level () in
1837 match !ProofEngine.proof with
1838 None -> assert false
1839 | Some (_,metasenv,_,_) -> metasenv
1841 match !ProofEngine.goal with
1844 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1845 let result = MQueryGenerator.searchPattern metasenv ey ty level in
1849 wrong_xpointer_format_from_wrong_xpointer_format' uri
1852 " <h1>Backward Query: </h1>" ^
1853 " <h2>Levels: </h2> " ^
1854 MQueryGenerator.string_of_levels
1855 (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1856 " <pre>" ^ get_last_query result ^ "</pre>"
1858 output_html outputhtml html ;
1860 let rec filter_out =
1864 let tl',exc = filter_out tl in
1867 ProofEngine.can_apply
1868 (term_of_cic_textual_parser_uri
1869 (cic_textual_parser_uri_of_string uri))
1877 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1878 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1885 " <h1>Objects that can actually be applied: </h1> " ^
1886 String.concat "<br>" uris' ^ exc ^
1887 " <h1>Number of false matches: " ^
1888 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1889 " <h1>Number of good matches: " ^
1890 string_of_int (List.length uris') ^ "</h1>"
1892 output_html outputhtml html' ;
1894 user_uri_choice ~title:"Ambiguous input."
1896 "Many lemmas can be successfully applied. Please, choose one:"
1899 inputt#set_term uri' ;
1903 output_html outputhtml
1904 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1907 let choose_selection
1908 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1910 let module G = Gdome in
1911 let rec aux element =
1912 if element#hasAttributeNS
1913 ~namespaceURI:helmns
1914 ~localName:(G.domString "xref")
1916 mmlwidget#set_selection (Some element)
1918 match element#get_parentNode with
1919 None -> assert false
1920 (*CSC: OCAML DIVERGES!
1921 | Some p -> aux (new G.element_of_node p)
1923 | Some p -> aux (new Gdome.element_of_node p)
1927 | None -> mmlwidget#set_selection None
1930 (* STUFF TO BUILD THE GTK INTERFACE *)
1932 (* Stuff for the widget settings *)
1934 let export_to_postscript (output : GMathView.math_view) =
1935 let lastdir = ref (Unix.getcwd ()) in
1938 GToolbox.select_file ~title:"Export to PostScript"
1939 ~dir:lastdir ~filename:"screenshot.ps" ()
1943 output#export_to_postscript ~filename:filename ();
1946 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1947 button_set_kerning button_set_transparency export_to_postscript_menu_item
1950 let is_set = button_t1#active in
1951 output#set_font_manager_type
1952 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1955 button_set_anti_aliasing#misc#set_sensitive true ;
1956 button_set_kerning#misc#set_sensitive true ;
1957 button_set_transparency#misc#set_sensitive true ;
1958 export_to_postscript_menu_item#misc#set_sensitive true ;
1962 button_set_anti_aliasing#misc#set_sensitive false ;
1963 button_set_kerning#misc#set_sensitive false ;
1964 button_set_transparency#misc#set_sensitive false ;
1965 export_to_postscript_menu_item#misc#set_sensitive false ;
1969 let set_anti_aliasing output button_set_anti_aliasing () =
1970 output#set_anti_aliasing button_set_anti_aliasing#active
1973 let set_kerning output button_set_kerning () =
1974 output#set_kerning button_set_kerning#active
1977 let set_transparency output button_set_transparency () =
1978 output#set_transparency button_set_transparency#active
1981 let changefont output font_size_spinb () =
1982 output#set_font_size font_size_spinb#value_as_int
1985 let set_log_verbosity output log_verbosity_spinb () =
1986 output#set_log_verbosity log_verbosity_spinb#value_as_int
1989 class settings_window (output : GMathView.math_view) sw
1990 export_to_postscript_menu_item selection_changed_callback
1992 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1994 GPack.vbox ~packing:settings_window#add () in
1997 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1998 ~border_width:5 ~packing:vbox#add () in
2000 GButton.toggle_button ~label:"activate t1 fonts"
2001 ~packing:(table#attach ~left:0 ~top:0) () in
2002 let button_set_anti_aliasing =
2003 GButton.toggle_button ~label:"set_anti_aliasing"
2004 ~packing:(table#attach ~left:0 ~top:1) () in
2005 let button_set_kerning =
2006 GButton.toggle_button ~label:"set_kerning"
2007 ~packing:(table#attach ~left:1 ~top:1) () in
2008 let button_set_transparency =
2009 GButton.toggle_button ~label:"set_transparency"
2010 ~packing:(table#attach ~left:2 ~top:1) () in
2013 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2014 ~border_width:5 ~packing:vbox#add () in
2015 let font_size_label =
2016 GMisc.label ~text:"font size:"
2017 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2018 let font_size_spinb =
2020 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2023 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2024 let log_verbosity_label =
2025 GMisc.label ~text:"log verbosity:"
2026 ~packing:(table#attach ~left:0 ~top:1) () in
2027 let log_verbosity_spinb =
2029 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2032 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2034 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2036 GButton.button ~label:"Close"
2037 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2039 method show = settings_window#show
2041 button_set_anti_aliasing#misc#set_sensitive false ;
2042 button_set_kerning#misc#set_sensitive false ;
2043 button_set_transparency#misc#set_sensitive false ;
2044 (* Signals connection *)
2045 ignore(button_t1#connect#clicked
2046 (activate_t1 output button_set_anti_aliasing button_set_kerning
2047 button_set_transparency export_to_postscript_menu_item button_t1)) ;
2048 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2049 ignore(button_set_anti_aliasing#connect#toggled
2050 (set_anti_aliasing output button_set_anti_aliasing));
2051 ignore(button_set_kerning#connect#toggled
2052 (set_kerning output button_set_kerning)) ;
2053 ignore(button_set_transparency#connect#toggled
2054 (set_transparency output button_set_transparency)) ;
2055 ignore(log_verbosity_spinb#connect#changed
2056 (set_log_verbosity output log_verbosity_spinb)) ;
2057 ignore(closeb#connect#clicked settings_window#misc#hide)
2060 (* Scratch window *)
2062 class scratch_window outputhtml =
2064 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2066 GPack.vbox ~packing:window#add () in
2068 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2070 GButton.button ~label:"Whd"
2071 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2073 GButton.button ~label:"Reduce"
2074 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2076 GButton.button ~label:"Simpl"
2077 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2078 let scrolled_window =
2079 GBin.scrolled_window ~border_width:10
2080 ~packing:(vbox#pack ~expand:true ~padding:5) () in
2083 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2085 method outputhtml = outputhtml
2086 method mmlwidget = mmlwidget
2087 method show () = window#misc#hide () ; window#show ()
2089 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2090 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2091 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2092 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2093 ignore(simplb#connect#clicked (simpl_in_scratch self))
2097 let vbox1 = GPack.vbox () in
2099 val mutable proofw_ref = None
2100 val mutable compute_ref = None
2102 Lazy.force self#compute ;
2103 match proofw_ref with
2104 None -> assert false
2105 | Some proofw -> proofw
2106 method content = vbox1
2108 match compute_ref with
2109 None -> assert false
2110 | Some compute -> compute
2114 let scrolled_window1 =
2115 GBin.scrolled_window ~border_width:10
2116 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2118 GMathView.math_view ~width:400 ~height:275
2119 ~packing:(scrolled_window1#add) () in
2120 let _ = proofw_ref <- Some proofw in
2122 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2124 GButton.button ~label:"Exact"
2125 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2127 GButton.button ~label:"Intros"
2128 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2130 GButton.button ~label:"Apply"
2131 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2132 let elimsimplintrosb =
2133 GButton.button ~label:"ElimSimplIntros"
2134 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2136 GButton.button ~label:"ElimType"
2137 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2139 GButton.button ~label:"Whd"
2140 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2142 GButton.button ~label:"Reduce"
2143 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2145 GButton.button ~label:"Simpl"
2146 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2148 GButton.button ~label:"Fold"
2149 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2151 GButton.button ~label:"Cut"
2152 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2154 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2156 GButton.button ~label:"Change"
2157 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2159 GButton.button ~label:"Let ... In"
2160 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2162 GButton.button ~label:"Ring"
2163 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2165 GButton.button ~label:"ClearBody"
2166 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2168 GButton.button ~label:"Clear"
2169 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2171 GButton.button ~label:"Fourier"
2172 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2174 GButton.button ~label:"RewriteSimpl ->"
2175 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2177 GButton.button ~label:"Reflexivity"
2178 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2180 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2182 GButton.button ~label:"Symmetry"
2183 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2185 GButton.button ~label:"Transitivity"
2186 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2188 GButton.button ~label:"Left"
2189 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2191 GButton.button ~label:"Right"
2192 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2194 GButton.button ~label:"Assumption"
2195 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2196 let searchpatternb =
2197 GButton.button ~label:"SearchPattern_Apply"
2198 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2199 ignore(exactb#connect#clicked exact) ;
2200 ignore(applyb#connect#clicked apply) ;
2201 ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2202 ignore(elimtypeb#connect#clicked elimtype) ;
2203 ignore(whdb#connect#clicked whd) ;
2204 ignore(reduceb#connect#clicked reduce) ;
2205 ignore(simplb#connect#clicked simpl) ;
2206 ignore(foldb#connect#clicked fold) ;
2207 ignore(cutb#connect#clicked cut) ;
2208 ignore(changeb#connect#clicked change) ;
2209 ignore(letinb#connect#clicked letin) ;
2210 ignore(ringb#connect#clicked ring) ;
2211 ignore(clearbodyb#connect#clicked clearbody) ;
2212 ignore(clearb#connect#clicked clear) ;
2213 ignore(fourierb#connect#clicked fourier) ;
2214 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2215 ignore(reflexivityb#connect#clicked reflexivity) ;
2216 ignore(symmetryb#connect#clicked symmetry) ;
2217 ignore(transitivityb#connect#clicked transitivity) ;
2218 ignore(leftb#connect#clicked left) ;
2219 ignore(rightb#connect#clicked right) ;
2220 ignore(assumptionb#connect#clicked assumption) ;
2221 ignore(introsb#connect#clicked intros) ;
2222 ignore(searchpatternb#connect#clicked searchPattern) ;
2223 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2229 let vbox1 = GPack.vbox () in
2230 let scrolled_window1 =
2231 GBin.scrolled_window ~border_width:10
2232 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2234 GMathView.math_view ~width:400 ~height:275
2235 ~packing:(scrolled_window1#add) () in
2237 method proofw = (assert false : GMathView.math_view)
2238 method content = vbox1
2239 method compute = (assert false : unit)
2243 let empty_page = new empty_page;;
2247 val notebook = GPack.notebook ()
2249 val mutable skip_switch_page_event = false
2250 val mutable empty = true
2251 method notebook = notebook
2253 let new_page = new page () in
2255 pages := !pages @ [n,lazy (setgoal n),new_page] ;
2256 notebook#append_page
2257 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2258 new_page#content#coerce
2259 method remove_all_pages ~skip_switch_page_event:skip =
2261 notebook#remove_page 0 (* let's remove the empty page *)
2263 List.iter (function _ -> notebook#remove_page 0) !pages ;
2265 skip_switch_page_event <- skip
2266 method set_current_page ~may_skip_switch_page_event n =
2267 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2268 let new_page = notebook#page_num page#content#coerce in
2269 if may_skip_switch_page_event && new_page <> notebook#current_page then
2270 skip_switch_page_event <- true ;
2271 notebook#goto_page new_page
2272 method set_empty_page =
2275 notebook#append_page
2276 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2277 empty_page#content#coerce
2279 let (_,_,page) = List.nth !pages notebook#current_page in
2283 (notebook#connect#switch_page
2285 let skip = skip_switch_page_event in
2286 skip_switch_page_event <- false ;
2289 let (metano,setgoal,page) = List.nth !pages i in
2290 ProofEngine.goal := Some metano ;
2291 Lazy.force (page#compute) ;
2300 class rendering_window output (notebook : notebook) =
2302 GWindow.window ~title:"MathML viewer" ~border_width:2
2303 ~allow_shrink:false () in
2304 let vbox_for_menu = GPack.vbox ~packing:window#add () in
2306 let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
2307 let factory0 = new GMenu.factory menubar in
2308 let accel_group = factory0#accel_group in
2310 let file_menu = factory0#add_submenu "File" in
2311 let factory1 = new GMenu.factory file_menu ~accel_group in
2312 let export_to_postscript_menu_item =
2315 (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
2317 let save_menu_item =
2318 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
2320 let reopen_menu_item =
2321 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
2325 factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
2327 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
2328 ignore (!save_set_sensitive false);
2329 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
2330 ignore (!qed_set_sensitive false);
2331 ignore (factory1#add_separator ()) ;
2332 let export_to_postscript_menu_item =
2333 factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
2334 ~callback:(export_to_postscript output) in
2335 ignore (factory1#add_separator ()) ;
2337 (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
2338 export_to_postscript_menu_item
2341 let edit_menu = factory0#add_submenu "Edit current proof" in
2342 let factory2 = new GMenu.factory edit_menu ~accel_group in
2343 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
2344 let proveit_menu_item =
2345 factory2#add_item "Prove It" ~key:GdkKeysyms._I
2346 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
2348 let focus_menu_item =
2349 factory2#add_item "Focus" ~key:GdkKeysyms._F
2350 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
2353 focus_and_proveit_set_sensitive :=
2355 proveit_menu_item#misc#set_sensitive b ;
2356 focus_menu_item#misc#set_sensitive b
2358 let _ = !focus_and_proveit_set_sensitive false in
2360 let settings_menu = factory0#add_submenu "Search" in
2361 let factory4 = new GMenu.factory settings_menu ~accel_group in
2363 factory4#add_item "Locate..." ~key:GdkKeysyms._T
2365 let show_menu_item =
2366 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
2369 let settings_menu = factory0#add_submenu "Settings" in
2370 let factory3 = new GMenu.factory settings_menu ~accel_group in
2372 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
2373 ~callback:edit_aliases in
2374 let _ = factory3#add_separator () in
2376 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
2377 ~callback:(function _ -> (settings_window ())#show ()) in
2379 let _ = window#add_accel_group accel_group in
2383 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
2385 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2386 let scrolled_window0 =
2387 GBin.scrolled_window ~border_width:10
2388 ~packing:(vbox#pack ~expand:true ~padding:5) () in
2389 let _ = scrolled_window0#add output#coerce in
2391 GBin.frame ~label:"Term input"
2392 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2394 GPack.vbox ~packing:frame#add () in
2396 GPack.hbox ~border_width:5 ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2398 GButton.button ~label:"State"
2399 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2401 GButton.button ~label:"Check"
2402 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2403 let scrolled_window1 =
2404 GBin.scrolled_window ~border_width:5
2405 ~packing:(vbox'#pack ~expand:true ~padding:0) () in
2407 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add () in
2409 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2411 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
2413 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
2417 ~source:"<html><body bgColor=\"white\"></body></html>"
2418 ~width:400 ~height: 100
2422 let scratch_window = new scratch_window outputhtml in
2424 method outputhtml = outputhtml
2425 method inputt = inputt
2426 method output = (output : GMathView.math_view)
2427 method notebook = notebook
2428 method show = window#show
2430 notebook#set_empty_page ;
2431 export_to_postscript_menu_item#misc#set_sensitive false ;
2432 check_term := (check_term_in_scratch scratch_window) ;
2434 (* signal handlers here *)
2435 ignore(output#connect#selection_changed
2437 choose_selection output elem ;
2438 !focus_and_proveit_set_sensitive true
2440 ignore (output#connect#clicked (show_in_show_window_callback output)) ;
2441 let settings_window = new settings_window output scrolled_window0
2442 export_to_postscript_menu_item (choose_selection output) in
2443 set_settings_window settings_window ;
2444 set_outputhtml outputhtml ;
2445 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2446 ignore(stateb#connect#clicked state) ;
2447 ignore(checkb#connect#clicked (check scratch_window)) ;
2448 Logger.log_callback :=
2449 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2454 let initialize_everything () =
2455 let module U = Unix in
2456 let output = GMathView.math_view ~width:350 ~height:280 () in
2457 let notebook = new notebook in
2458 let rendering_window' = new rendering_window output notebook in
2459 set_rendering_window rendering_window' ;
2460 mml_of_cic_term_ref := mml_of_cic_term ;
2461 rendering_window'#show () ;
2467 Mqint.init "dbname=helm_mowgli" ;
2468 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2469 ignore (GtkMain.Main.init ()) ;
2470 initialize_everything () ;
2471 if !usedb then Mqint.close ();