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 (* GLOBAL CONSTANTS *)
39 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
43 " <body bgColor=\"white\">"
53 Sys.getenv "GTOPLEVEL_PROOFFILE"
55 Not_found -> "/public/currentproof"
60 Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
62 Not_found -> "/public/currentprooftype"
65 (*CSC: the getter should handle the innertypes, not the FS *)
69 Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
71 Not_found -> "/public/innertypes"
74 let constanttypefile =
76 Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
78 Not_found -> "/public/constanttype"
81 let postgresqlconnectionstring =
83 Sys.getenv "POSTGRESQL_CONNECTION_STRING"
85 Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
88 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
90 let htmlheader_and_content = ref htmlheader;;
92 let current_cic_infos = ref None;;
93 let current_goal_infos = ref None;;
94 let current_scratch_infos = ref None;;
96 let check_term = ref (fun _ _ _ -> assert false);;
97 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
99 exception RenderingWindowsNotInitialized;;
101 let set_rendering_window,rendering_window =
102 let rendering_window_ref = ref None in
103 (function rw -> rendering_window_ref := Some rw),
105 match !rendering_window_ref with
106 None -> raise RenderingWindowsNotInitialized
111 exception SettingsWindowsNotInitialized;;
113 let set_settings_window,settings_window =
114 let settings_window_ref = ref None in
115 (function rw -> settings_window_ref := Some rw),
117 match !settings_window_ref with
118 None -> raise SettingsWindowsNotInitialized
123 exception OutputHtmlNotInitialized;;
125 let set_outputhtml,outputhtml =
126 let outputhtml_ref = ref None in
127 (function rw -> outputhtml_ref := Some rw),
129 match !outputhtml_ref with
130 None -> raise OutputHtmlNotInitialized
131 | Some outputhtml -> outputhtml
135 exception QedSetSensitiveNotInitialized;;
136 let qed_set_sensitive =
137 ref (function _ -> raise QedSetSensitiveNotInitialized)
140 exception SaveSetSensitiveNotInitialized;;
141 let save_set_sensitive =
142 ref (function _ -> raise SaveSetSensitiveNotInitialized)
145 (* COMMAND LINE OPTIONS *)
151 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
154 Arg.parse argspec ignore ""
158 let term_of_cic_textual_parser_uri uri =
159 let module C = Cic in
160 let module CTP = CicTextualParser0 in
162 CTP.ConUri uri -> C.Const (uri,[])
163 | CTP.VarUri uri -> C.Var (uri,[])
164 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
165 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
168 let string_of_cic_textual_parser_uri uri =
169 let module C = Cic in
170 let module CTP = CicTextualParser0 in
173 CTP.ConUri uri -> UriManager.string_of_uri uri
174 | CTP.VarUri uri -> UriManager.string_of_uri uri
175 | CTP.IndTyUri (uri,tyno) ->
176 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
177 | CTP.IndConUri (uri,tyno,consno) ->
178 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
181 (* 4 = String.length "cic:" *)
182 String.sub uri' 4 (String.length uri' - 4)
185 let output_html outputhtml msg =
186 htmlheader_and_content := !htmlheader_and_content ^ msg ;
187 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
188 outputhtml#set_topline (-1)
191 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
195 let check_window outputhtml uris =
198 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
200 GPack.notebook ~scrollable:true ~packing:window#add () in
205 let scrolled_window =
206 GBin.scrolled_window ~border_width:10
208 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
213 GMathViewAux.single_selection_math_view
214 ~packing:scrolled_window#add ~width:400 ~height:280 () in
217 term_of_cic_textual_parser_uri
218 (Misc.cic_textual_parser_uri_of_string uri)
220 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
223 let mml = !mml_of_cic_term_ref 111 expr in
224 mmlwidget#load_doc ~dom:mml
227 output_html outputhtml
228 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
233 (notebook#connect#switch_page
234 (function i -> Lazy.force (List.nth render_terms i)))
240 interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
241 ?(enable_button_for_non_vars=false) ~title ~msg uris
243 let choices = ref [] in
244 let chosen = ref false in
245 let use_only_constants = ref false in
247 GWindow.dialog ~modal:true ~title ~width:600 () in
249 GMisc.label ~text:msg
250 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
251 let scrolled_window =
252 GBin.scrolled_window ~border_width:10
253 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
255 let expected_height = 18 * List.length uris in
256 let height = if expected_height > 400 then 400 else expected_height in
257 GList.clist ~columns:1 ~packing:scrolled_window#add
258 ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
259 let _ = List.map (function x -> clist#append [x]) uris in
261 GPack.hbox ~border_width:0
262 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
264 GMisc.label ~text:"None of the above. Try this one:"
265 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
267 GEdit.entry ~editable:true
268 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
270 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
272 GButton.button ~label:ok
273 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
274 let _ = okb#misc#set_sensitive false in
279 if enable_button_for_non_vars then
280 hbox#pack ~expand:false ~fill:false ~padding:5 w)
281 ~label:"Try constants only" () in
283 GButton.button ~label:"Check"
284 ~packing:(hbox#pack ~padding:5) () in
285 let _ = checkb#misc#set_sensitive false in
287 GButton.button ~label:"Abort"
288 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
290 let check_callback () =
291 assert (List.length !choices > 0) ;
292 check_window (outputhtml ()) !choices
294 ignore (window#connect#destroy GMain.Main.quit) ;
295 ignore (cancelb#connect#clicked window#destroy) ;
297 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
299 (nonvarsb#connect#clicked
301 use_only_constants := true ;
305 ignore (checkb#connect#clicked check_callback) ;
307 (clist#connect#select_row
308 (fun ~row ~column ~event ->
309 checkb#misc#set_sensitive true ;
310 okb#misc#set_sensitive true ;
311 choices := (List.nth uris row)::!choices)) ;
313 (clist#connect#unselect_row
314 (fun ~row ~column ~event ->
316 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
318 (manual_input#connect#changed
320 if manual_input#text = "" then
323 checkb#misc#set_sensitive false ;
324 okb#misc#set_sensitive false ;
325 clist#misc#set_sensitive true
329 choices := [manual_input#text] ;
330 clist#unselect_all () ;
331 checkb#misc#set_sensitive true ;
332 okb#misc#set_sensitive true ;
333 clist#misc#set_sensitive false
335 window#set_position `CENTER ;
339 if !use_only_constants then
341 (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
344 if List.length !choices > 0 then !choices else raise NoChoice
349 let interactive_interpretation_choice interpretations =
350 let chosen = ref None in
353 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
354 let vbox = GPack.vbox ~packing:window#add () in
358 ("Ambiguous input since there are many well-typed interpretations." ^
359 " Please, choose one of them.")
360 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
362 GPack.notebook ~scrollable:true
363 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
366 (function interpretation ->
368 let expected_height = 18 * List.length interpretation in
369 let height = if expected_height > 400 then 400 else expected_height in
370 GList.clist ~columns:2 ~packing:notebook#append_page ~height
371 ~titles:["id" ; "URI"] ()
375 (function (id,uri) ->
376 let n = clist#append [id;uri] in
377 clist#set_row ~selectable:false n
380 clist#columns_autosize ()
383 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
385 GButton.button ~label:"Ok"
386 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
388 GButton.button ~label:"Abort"
389 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
391 ignore (window#connect#destroy GMain.Main.quit) ;
392 ignore (cancelb#connect#clicked window#destroy) ;
395 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
396 window#set_position `CENTER ;
400 None -> raise NoChoice
407 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
409 let query = ref "" in
410 MQueryGenerator.set_confirm_query
411 (function q -> query := MQueryUtil.text_of_query q ; true) ;
412 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
416 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
418 (*CSC: ????????????????? *)
420 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
424 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
425 ~ask_dtd_to_the_getter:true
429 None -> Xml2Gdome.document_of_xml Misc.domImpl xml
431 Xml.pp xml (Some constanttypefile) ;
432 Xml2Gdome.document_of_xml Misc.domImpl bodyxml'
434 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
435 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
437 Xml.pp xmlinnertypes (Some innertypesfile) ;
438 let output = ApplyStylesheets.apply_proof_stylesheets input ~explode_all in
443 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
446 let struri = UriManager.string_of_uri uri in
447 let idx = (String.rindex struri '/') + 1 in
448 String.sub struri idx (String.length struri - idx)
450 let path = pathname ^ "/" ^ name in
452 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
456 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
457 ~ask_dtd_to_the_getter:false
460 let innertypesuri = UriManager.innertypesuri_of_uri uri in
461 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
462 Getter.register innertypesuri
463 (Configuration.annotations_url ^
464 Str.replace_first (Str.regexp "^cic:") ""
465 (UriManager.string_of_uri innertypesuri) ^ ".xml"
467 (* constant type / variable / mutual inductive types definition *)
468 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
470 (Configuration.annotations_url ^
471 Str.replace_first (Str.regexp "^cic:") ""
472 (UriManager.string_of_uri uri) ^ ".xml"
479 match UriManager.bodyuri_of_uri uri with
481 | Some bodyuri -> bodyuri
483 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
484 Getter.register bodyuri
485 (Configuration.annotations_url ^
486 Str.replace_first (Str.regexp "^cic:") ""
487 (UriManager.string_of_uri bodyuri) ^ ".xml"
494 exception RefreshSequentException of exn;;
495 exception RefreshProofException of exn;;
497 let refresh_proof (output : GMathViewAux.single_selection_math_view) =
499 let uri,currentproof =
500 match !ProofEngine.proof with
502 | Some (uri,metasenv,bo,ty) ->
503 !qed_set_sensitive (List.length metasenv = 0) ;
504 (*CSC: Wrong: [] is just plainly wrong *)
505 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
508 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
509 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
511 Cic2acic.acic_object_of_cic_object currentproof
514 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
517 output#load_doc ~dom:mml ;
519 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
522 match !ProofEngine.proof with
524 | Some (uri,metasenv,bo,ty) ->
525 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
526 raise (RefreshProofException e)
529 let refresh_sequent ?(empty_notebook=true) notebook =
531 match !ProofEngine.goal with
533 if empty_notebook then
535 notebook#remove_all_pages ~skip_switch_page_event:false ;
536 notebook#set_empty_page
539 notebook#proofw#unload
542 match !ProofEngine.proof with
544 | Some (_,metasenv,_,_) -> metasenv
546 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
547 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
548 SequentPp.XmlPp.print_sequent metasenv currentsequent
550 let regenerate_notebook () =
551 let skip_switch_page_event =
553 (m,_,_)::_ when m = metano -> false
556 notebook#remove_all_pages ~skip_switch_page_event ;
557 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
559 if empty_notebook then
561 regenerate_notebook () ;
562 notebook#set_current_page ~may_skip_switch_page_event:false metano
567 Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in
569 ApplyStylesheets.apply_sequent_stylesheets sequent_doc
571 notebook#set_current_page ~may_skip_switch_page_event:true metano;
572 notebook#proofw#load_doc ~dom:sequent_mml
574 current_goal_infos :=
575 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
579 match !ProofEngine.goal with
584 match !ProofEngine.proof with
586 | Some (_,metasenv,_,_) -> metasenv
589 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
590 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
591 raise (RefreshSequentException e)
592 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
596 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
597 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
600 let mml_of_cic_term metano term =
602 match !ProofEngine.proof with
604 | Some (_,metasenv,_,_) -> metasenv
607 match !ProofEngine.goal with
610 let (_,canonical_context,_) =
611 List.find (function (m,_,_) -> m=metano) metasenv
615 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
616 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
619 Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome
621 let res = ApplyStylesheets.apply_sequent_stylesheets sequent_doc in
622 current_scratch_infos :=
623 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
627 exception OpenConjecturesStillThere;;
628 exception WrongProof;;
630 let pathname_of_annuri uristring =
631 Configuration.annotations_dir ^
632 Str.replace_first (Str.regexp "^cic:") "" uristring
635 let make_dirs dirpath =
636 ignore (Unix.system ("mkdir -p " ^ dirpath))
639 let save_obj uri obj =
641 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
642 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
644 Cic2acic.acic_object_of_cic_object obj
646 (* let's save the theorem and register it to the getter *)
647 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
649 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
654 match !ProofEngine.proof with
656 | Some (uri,[],bo,ty) ->
658 CicReduction.are_convertible []
659 (CicTypeChecker.type_of_aux' [] [] bo) ty
662 (*CSC: Wrong: [] is just plainly wrong *)
663 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
665 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
666 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
668 Cic2acic.acic_object_of_cic_object proof
671 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
674 ((rendering_window ())#output : GMathViewAux.single_selection_math_view)#load_doc mml ;
675 !qed_set_sensitive false ;
676 (* let's save the theorem and register it to the getter *)
677 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
679 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
683 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
688 | _ -> raise OpenConjecturesStillThere
692 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
693 match !ProofEngine.proof with
695 | Some (uri, metasenv, bo, ty) ->
697 (*CSC: Wrong: [] is just plainly wrong *)
698 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
700 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
701 Cic2acic.acic_object_of_cic_object currentproof
705 Cic2Xml.print_object uri ~ids_to_inner_sorts
706 ~ask_dtd_to_the_getter:true acurrentproof
708 xml,Some bodyxml -> xml,bodyxml
709 | _,None -> assert false
711 Xml.pp ~quiet:true xml (Some prooffiletype) ;
712 output_html outputhtml
713 ("<h1 color=\"Green\">Current proof type saved to " ^
714 prooffiletype ^ "</h1>") ;
715 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
716 output_html outputhtml
717 ("<h1 color=\"Green\">Current proof body saved to " ^
721 (* Used to typecheck the loaded proofs *)
722 let typecheck_loaded_proof metasenv bo ty =
723 let module T = CicTypeChecker in
726 (fun metasenv ((_,context,ty) as conj) ->
727 ignore (T.type_of_aux' metasenv context ty) ;
730 ignore (T.type_of_aux' metasenv [] ty) ;
731 ignore (T.type_of_aux' metasenv [] bo)
735 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
736 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
737 let notebook = (rendering_window ())#notebook in
740 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
743 None -> raise NoChoice
745 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
746 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
747 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
748 typecheck_loaded_proof metasenv bo ty ;
750 Some (uri, metasenv, bo, ty) ;
754 | (metano,_,_)::_ -> Some metano
756 refresh_proof output ;
757 refresh_sequent notebook ;
758 output_html outputhtml
759 ("<h1 color=\"Green\">Current proof type loaded from " ^
760 prooffiletype ^ "</h1>") ;
761 output_html outputhtml
762 ("<h1 color=\"Green\">Current proof body loaded from " ^
763 prooffile ^ "</h1>") ;
764 !save_set_sensitive true
767 RefreshSequentException e ->
768 output_html outputhtml
769 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
770 "sequent: " ^ Printexc.to_string e ^ "</h1>")
771 | RefreshProofException e ->
772 output_html outputhtml
773 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
774 "proof: " ^ Printexc.to_string e ^ "</h1>")
776 output_html outputhtml
777 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
780 let edit_aliases () =
781 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
782 let id_to_uris = inputt#id_to_uris in
783 let chosen = ref false in
786 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
788 GPack.vbox ~border_width:0 ~packing:window#add () in
789 let scrolled_window =
790 GBin.scrolled_window ~border_width:10
791 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
792 let input = GEdit.text ~editable:true ~width:400 ~height:100
793 ~packing:scrolled_window#add () in
795 GPack.hbox ~border_width:0
796 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
798 GButton.button ~label:"Ok"
799 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
801 GButton.button ~label:"Cancel"
802 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
803 ignore (window#connect#destroy GMain.Main.quit) ;
804 ignore (cancelb#connect#clicked window#destroy) ;
806 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
807 let dom,resolve_id = !id_to_uris in
809 (input#insert_text ~pos:0
814 match resolve_id v with
819 (string_of_cic_textual_parser_uri uri)
825 let inputtext = input#get_chars 0 input#length in
827 let alfa = "[a-zA-Z_-]" in
828 let digit = "[0-9]" in
829 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
830 let blanks = "\( \|\t\|\n\)+" in
831 let nonblanks = "[^ \t\n]+" in
832 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
834 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
838 let n' = Str.search_forward regexpr inputtext n in
839 let id = Str.matched_group 2 inputtext in
841 Misc.cic_textual_parser_uri_of_string
842 ("cic:" ^ (Str.matched_group 5 inputtext))
844 let dom,resolve_id = aux (n' + 1) in
845 if List.mem id dom then
849 (function id' -> if id = id' then Some uri else resolve_id id')
851 Not_found -> TermEditor.empty_id_to_uris
855 id_to_uris := (dom,resolve_id)
859 let module L = LogicalOperations in
860 let module G = Gdome in
861 let notebook = (rendering_window ())#notebook in
862 let output = (rendering_window ())#output in
863 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
864 match (rendering_window ())#output#get_selection with
867 ((node : Gdome.element)#getAttributeNS
869 ((element : G.element)#getAttributeNS
871 ~namespaceURI:Misc.helmns
872 ~localName:(G.domString "xref"))#to_string
874 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
878 match !current_cic_infos with
879 Some (ids_to_terms, ids_to_father_ids, _, _) ->
881 L.to_sequent id ids_to_terms ids_to_father_ids ;
882 refresh_proof output ;
883 refresh_sequent notebook
884 | None -> assert false (* "ERROR: No current term!!!" *)
886 RefreshSequentException e ->
887 output_html outputhtml
888 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
889 "sequent: " ^ Printexc.to_string e ^ "</h1>")
890 | RefreshProofException e ->
891 output_html outputhtml
892 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
893 "proof: " ^ Printexc.to_string e ^ "</h1>")
895 output_html outputhtml
896 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
898 | None -> assert false (* "ERROR: No selection!!!" *)
902 let module L = LogicalOperations in
903 let module G = Gdome in
904 let notebook = (rendering_window ())#notebook in
905 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
906 match (rendering_window ())#output#get_selection with
909 ((node : Gdome.element)#getAttributeNS
911 ((element : G.element)#getAttributeNS
913 ~namespaceURI:Misc.helmns
914 ~localName:(G.domString "xref"))#to_string
916 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
920 match !current_cic_infos with
921 Some (ids_to_terms, ids_to_father_ids, _, _) ->
923 L.focus id ids_to_terms ids_to_father_ids ;
924 refresh_sequent notebook
925 | None -> assert false (* "ERROR: No current term!!!" *)
927 RefreshSequentException e ->
928 output_html outputhtml
929 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
930 "sequent: " ^ Printexc.to_string e ^ "</h1>")
931 | RefreshProofException e ->
932 output_html outputhtml
933 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
934 "proof: " ^ Printexc.to_string e ^ "</h1>")
936 output_html outputhtml
937 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
939 | None -> assert false (* "ERROR: No selection!!!" *)
942 exception NoPrevGoal;;
943 exception NoNextGoal;;
946 let module L = LogicalOperations in
947 let module G = Gdome in
948 let notebook = (rendering_window ())#notebook in
949 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
951 match !ProofEngine.proof with
953 | Some (_,metasenv,_,_) -> metasenv
956 refresh_sequent ~empty_notebook:false notebook
958 RefreshSequentException e ->
959 output_html outputhtml
960 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
961 "sequent: " ^ Printexc.to_string e ^ "</h1>")
963 output_html outputhtml
964 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
968 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
971 GWindow.window ~width:800 ~border_width:2 () in
972 let scrolled_window =
973 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
975 GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
976 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
977 let href = Gdome.domString "href" in
978 let show_in_show_window_obj uri obj =
979 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
982 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
983 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
985 Cic2acic.acic_object_of_cic_object obj
988 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
991 window#set_title (UriManager.string_of_uri uri) ;
992 window#misc#hide () ; window#show () ;
993 mmlwidget#load_doc mml ;
996 output_html outputhtml
997 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
999 let show_in_show_window_uri uri =
1000 let obj = CicEnvironment.get_obj uri in
1001 show_in_show_window_obj uri obj
1003 let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
1004 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1006 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1008 show_in_show_window_uri (UriManager.uri_of_string uri)
1010 ignore (mmlwidget#action_toggle n)
1013 mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
1015 show_in_show_window_obj, show_in_show_window_uri,
1016 show_in_show_window_callback
1019 exception NoObjectsLocated;;
1021 let user_uri_choice ~title ~msg uris =
1024 [] -> raise NoObjectsLocated
1028 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1033 String.sub uri 4 (String.length uri - 4)
1036 let locate_callback id =
1037 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1038 let result = MQueryGenerator.locate id in
1042 Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
1045 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1047 output_html outputhtml html ;
1048 user_uri_choice ~title:"Ambiguous input."
1050 ("Ambiguous input \"" ^ id ^
1051 "\". Please, choose one interpetation:")
1056 let input_or_locate_uri ~title =
1057 let uri = ref None in
1060 ~width:400 ~modal:true ~title ~border_width:2 () in
1061 let vbox = GPack.vbox ~packing:window#add () in
1063 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1065 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1067 GEdit.entry ~editable:true
1068 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1070 GButton.button ~label:"Check"
1071 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1072 let _ = checkb#misc#set_sensitive false in
1074 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1076 GMisc.label ~text:"You can also enter an indentifier to locate:"
1077 ~packing:(hbox2#pack ~padding:5) () in
1079 GEdit.entry ~editable:true
1080 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1082 GButton.button ~label:"Locate"
1083 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1084 let _ = locateb#misc#set_sensitive false in
1086 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1088 GButton.button ~label:"Ok"
1089 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1090 let _ = okb#misc#set_sensitive false in
1092 GButton.button ~label:"Cancel"
1093 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1095 ignore (window#connect#destroy GMain.Main.quit) ;
1097 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1098 let check_callback () =
1099 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1100 let uri = "cic:" ^ manual_input#text in
1102 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1103 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1106 Getter.Unresolved ->
1107 output_html outputhtml
1108 ("<h1 color=\"Red\">URI " ^ uri ^
1109 " does not correspond to any object.</h1>") ;
1111 | UriManager.IllFormedUri _ ->
1112 output_html outputhtml
1113 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1116 output_html outputhtml
1117 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1121 (okb#connect#clicked
1123 if check_callback () then
1125 uri := Some manual_input#text ;
1129 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1131 (manual_input#connect#changed
1133 if manual_input#text = "" then
1135 checkb#misc#set_sensitive false ;
1136 okb#misc#set_sensitive false
1140 checkb#misc#set_sensitive true ;
1141 okb#misc#set_sensitive true
1144 (locate_input#connect#changed
1145 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1147 (locateb#connect#clicked
1149 let id = locate_input#text in
1150 manual_input#set_text (locate_callback id) ;
1151 locate_input#delete_text 0 (String.length id)
1154 GMain.Main.main () ;
1156 None -> raise NoChoice
1157 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1160 exception AmbiguousInput;;
1162 (* A WIDGET TO ENTER CIC TERMS *)
1166 let output_html msg = output_html (outputhtml ()) msg;;
1167 let interactive_user_uri_choice =
1168 fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
1169 interactive_user_uri_choice ~selection_mode ?ok
1170 ?enable_button_for_non_vars ~title ~msg;;
1171 let interactive_interpretation_choice = interactive_interpretation_choice;;
1172 let input_or_locate_uri = input_or_locate_uri;;
1176 module TermEditor' = TermEditor.Make(Callbacks);;
1178 (* OTHER FUNCTIONS *)
1181 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1182 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1185 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1187 None -> raise NoChoice
1189 let uri = locate_callback input in
1193 output_html outputhtml
1194 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1198 exception UriAlreadyInUse;;
1199 exception NotAUriToAConstant;;
1201 let new_inductive () =
1202 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1203 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1204 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1205 let notebook = (rendering_window ())#notebook in
1207 let chosen = ref false in
1208 let inductive = ref true in
1209 let paramsno = ref 0 in
1210 let get_uri = ref (function _ -> assert false) in
1211 let get_base_uri = ref (function _ -> assert false) in
1212 let get_names = ref (function _ -> assert false) in
1213 let get_types_and_cons = ref (function _ -> assert false) in
1214 let get_context_and_subst = ref (function _ -> assert false) in
1217 ~width:600 ~modal:true ~position:`CENTER
1218 ~title:"New Block of Mutual (Co)Inductive Definitions"
1219 ~border_width:2 () in
1220 let vbox = GPack.vbox ~packing:window#add () in
1222 GPack.hbox ~border_width:0
1223 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1225 GMisc.label ~text:"Enter the URI for the new block:"
1226 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1228 GEdit.entry ~editable:true
1229 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1231 GPack.hbox ~border_width:0
1232 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1236 "Enter the number of left parameters in every arity and constructor type:"
1237 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1238 let paramsno_entry =
1239 GEdit.entry ~editable:true ~text:"0"
1240 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1242 GPack.hbox ~border_width:0
1243 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1245 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1246 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1248 GButton.radio_button ~label:"Inductive"
1249 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1251 GButton.radio_button ~label:"Coinductive"
1252 ~group:inductiveb#group
1253 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1255 GPack.hbox ~border_width:0
1256 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1258 GMisc.label ~text:"Enter the list of the names of the types:"
1259 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1261 GEdit.entry ~editable:true
1262 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1264 GPack.hbox ~border_width:0
1265 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1267 GButton.button ~label:"> Next"
1268 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1269 let _ = okb#misc#set_sensitive true in
1271 GButton.button ~label:"Abort"
1272 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1273 ignore (window#connect#destroy GMain.Main.quit) ;
1274 ignore (cancelb#connect#clicked window#destroy) ;
1278 (okb#connect#clicked
1281 let uristr = "cic:" ^ uri_entry#text in
1282 let namesstr = names_entry#text in
1283 let paramsno' = int_of_string (paramsno_entry#text) in
1284 match Str.split (Str.regexp " +") namesstr with
1286 | (he::tl) as names ->
1287 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1290 ignore (Getter.resolve uri) ;
1291 raise UriAlreadyInUse
1293 Getter.Unresolved ->
1294 get_uri := (function () -> uri) ;
1295 get_names := (function () -> names) ;
1296 inductive := inductiveb#active ;
1297 paramsno := paramsno' ;
1302 output_html outputhtml
1303 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1311 GBin.frame ~label:name
1312 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1313 let vbox = GPack.vbox ~packing:frame#add () in
1314 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1316 GMisc.label ~text:("Enter its type:")
1317 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1318 let scrolled_window =
1319 GBin.scrolled_window ~border_width:5
1320 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1322 TermEditor'.term_editor
1323 ~width:400 ~height:20 ~packing:scrolled_window#add
1324 ~share_id_to_uris_with:inputt ()
1325 ~isnotempty_callback:
1327 (*non_empty_type := b ;*)
1328 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1331 GPack.hbox ~border_width:0
1332 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1334 GMisc.label ~text:("Enter the list of its constructors:")
1335 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1336 let cons_names_entry =
1337 GEdit.entry ~editable:true
1338 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1339 (newinputt,cons_names_entry)
1342 vbox#remove hboxn#coerce ;
1344 GPack.hbox ~border_width:0
1345 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1347 GButton.button ~label:"> Next"
1348 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1350 GButton.button ~label:"Abort"
1351 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1352 ignore (cancelb#connect#clicked window#destroy) ;
1354 (okb#connect#clicked
1357 let names = !get_names () in
1358 let types_and_cons =
1360 (fun name (newinputt,cons_names_entry) ->
1361 let consnamesstr = cons_names_entry#text in
1362 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1364 newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1367 [] -> expr,cons_names
1368 | _ -> raise AmbiguousInput
1369 ) names type_widgets
1371 let uri = !get_uri () in
1373 (* Let's see if so far the definition is well-typed *)
1376 (* To test if the arities of the inductive types are well *)
1377 (* typed, we check the inductive block definition where *)
1378 (* no constructor is given to each type. *)
1381 (fun name (ty,cons) -> (name, !inductive, ty, []))
1382 names types_and_cons
1384 CicTypeChecker.typecheck_mutual_inductive_defs uri
1385 (tys,params,paramsno)
1387 get_context_and_subst :=
1391 (fun (context,subst) name (ty,_) ->
1393 (Some (Cic.Name name, Cic.Decl ty))::context,
1394 (Cic.MutInd (uri,!i,[]))::subst
1397 ) ([],[]) names types_and_cons) ;
1398 let types_and_cons' =
1400 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1401 names types_and_cons
1403 get_types_and_cons := (function () -> types_and_cons') ;
1408 output_html outputhtml
1409 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1412 and phase3 name cons =
1413 let get_cons_types = ref (function () -> assert false) in
1416 ~width:600 ~modal:true ~position:`CENTER
1417 ~title:(name ^ " Constructors")
1418 ~border_width:2 () in
1419 let vbox = GPack.vbox ~packing:window2#add () in
1420 let cons_type_widgets =
1422 (function consname ->
1424 GPack.hbox ~border_width:0
1425 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1427 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1428 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1429 let scrolled_window =
1430 GBin.scrolled_window ~border_width:5
1431 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1433 TermEditor'.term_editor
1434 ~width:400 ~height:20 ~packing:scrolled_window#add
1435 ~share_id_to_uris_with:inputt ()
1436 ~isnotempty_callback:
1438 (* (*non_empty_type := b ;*)
1439 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1444 GPack.hbox ~border_width:0
1445 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1447 GButton.button ~label:"> Next"
1448 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1449 let _ = okb#misc#set_sensitive true in
1451 GButton.button ~label:"Abort"
1452 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1453 ignore (window2#connect#destroy GMain.Main.quit) ;
1454 ignore (cancelb#connect#clicked window2#destroy) ;
1456 (okb#connect#clicked
1460 let context,subst= !get_context_and_subst () in
1465 inputt#get_metasenv_and_term ~context ~metasenv:[]
1469 let undebrujined_expr =
1471 (fun expr t -> CicSubstitution.subst t expr) expr subst
1473 name, undebrujined_expr
1474 | _ -> raise AmbiguousInput
1475 ) cons cons_type_widgets
1477 get_cons_types := (function () -> cons_types) ;
1481 output_html outputhtml
1482 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1485 GMain.Main.main () ;
1486 let okb_pressed = !chosen in
1488 if (not okb_pressed) then
1491 assert false (* The control never reaches this point *)
1494 (!get_cons_types ())
1497 (* No more phases left or Abort pressed *)
1499 GMain.Main.main () ;
1503 let uri = !get_uri () in
1506 let tys = !get_types_and_cons () in
1507 let obj = Cic.InductiveDefinition tys params !paramsno in
1510 prerr_endline (CicPp.ppobj obj) ;
1511 CicTypeChecker.typecheck_mutual_inductive_defs uri
1512 (tys,params,!paramsno) ;
1515 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1516 prerr_endline (CicPp.ppobj obj) ;
1518 (* We already know that obj is well-typed. We need to add it to the *)
1519 (* environment in order to compute the inner-types without having to *)
1520 (* debrujin it or having to modify lots of other functions to avoid *)
1521 (* asking the environment for the MUTINDs we are defining now. *)
1522 CicEnvironment.put_inductive_definition uri obj ;
1524 show_in_show_window_obj uri obj
1527 output_html outputhtml
1528 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1531 let mk_fresh_name_callback context name ~typ =
1533 match ProofEngineHelpers.mk_fresh_name context name ~typ with
1534 Cic.Name fresh_name -> fresh_name
1535 | Cic.Anonymous -> assert false
1538 GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
1539 ("Enter a fresh name for the hypothesis " ^
1541 (List.map (function None -> None | Some (n,_) -> Some n) context))
1543 Some fresh_name' -> Cic.Name fresh_name'
1544 | None -> raise NoChoice
1548 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1549 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1550 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1551 let notebook = (rendering_window ())#notebook in
1553 let chosen = ref false in
1554 let get_metasenv_and_term = ref (function _ -> assert false) in
1555 let get_uri = ref (function _ -> assert false) in
1556 let non_empty_type = ref false in
1559 ~width:600 ~modal:true ~title:"New Proof or Definition"
1560 ~border_width:2 () in
1561 let vbox = GPack.vbox ~packing:window#add () in
1563 GPack.hbox ~border_width:0
1564 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1566 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1567 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1569 GEdit.entry ~editable:true
1570 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1572 GPack.hbox ~border_width:0
1573 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1575 GMisc.label ~text:"Enter the theorem or definition type:"
1576 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1577 let scrolled_window =
1578 GBin.scrolled_window ~border_width:5
1579 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1580 (* the content of the scrolled_window is moved below (see comment) *)
1582 GPack.hbox ~border_width:0
1583 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1585 GButton.button ~label:"Ok"
1586 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1587 let _ = okb#misc#set_sensitive false in
1589 GButton.button ~label:"Cancel"
1590 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1591 (* moved here to have visibility of the ok button *)
1593 TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
1594 ~share_id_to_uris_with:inputt ()
1595 ~isnotempty_callback:
1597 non_empty_type := b ;
1598 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1601 newinputt#set_term inputt#get_as_string ;
1604 uri_entry#connect#changed
1606 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1608 ignore (window#connect#destroy GMain.Main.quit) ;
1609 ignore (cancelb#connect#clicked window#destroy) ;
1611 (okb#connect#clicked
1615 let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1616 let uristr = "cic:" ^ uri_entry#text in
1617 let uri = UriManager.uri_of_string uristr in
1618 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1619 raise NotAUriToAConstant
1623 ignore (Getter.resolve uri) ;
1624 raise UriAlreadyInUse
1626 Getter.Unresolved ->
1627 get_metasenv_and_term := (function () -> metasenv,parsed) ;
1628 get_uri := (function () -> uri) ;
1633 output_html outputhtml
1634 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1637 GMain.Main.main () ;
1640 let metasenv,expr = !get_metasenv_and_term () in
1641 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1642 ProofEngine.proof :=
1643 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1644 ProofEngine.goal := Some 1 ;
1645 refresh_sequent notebook ;
1646 refresh_proof output ;
1647 !save_set_sensitive true ;
1649 ProofEngine.intros ~mk_fresh_name_callback () ;
1650 refresh_sequent notebook ;
1651 refresh_proof output
1653 RefreshSequentException e ->
1654 output_html outputhtml
1655 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1656 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1657 | RefreshProofException e ->
1658 output_html outputhtml
1659 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1660 "proof: " ^ Printexc.to_string e ^ "</h1>")
1662 output_html outputhtml
1663 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1666 let check_term_in_scratch scratch_window metasenv context expr =
1668 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1669 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1670 scratch_window#show () ;
1671 scratch_window#mmlwidget#load_doc ~dom:mml
1674 print_endline ("? " ^ CicPp.ppterm expr) ;
1678 let check scratch_window () =
1679 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1680 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1682 match !ProofEngine.proof with
1684 | Some (_,metasenv,_,_) -> metasenv
1687 match !ProofEngine.goal with
1690 let (_,canonical_context,_) =
1691 List.find (function (m,_,_) -> m=metano) metasenv
1696 let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
1697 check_term_in_scratch scratch_window metasenv' context expr
1700 output_html outputhtml
1701 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1704 let decompose_uris_choice_callback uris =
1705 (* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
1706 let module U = UriManager in
1709 match Misc.cic_textual_parser_uri_of_string uri with
1710 CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
1711 | _ -> assert false)
1712 (interactive_user_uri_choice
1713 ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false
1714 ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose"
1716 (function (uri,typeno,_) ->
1717 U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
1722 (***********************)
1724 (***********************)
1726 let call_tactic tactic () =
1727 let notebook = (rendering_window ())#notebook in
1728 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1729 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1730 let savedproof = !ProofEngine.proof in
1731 let savedgoal = !ProofEngine.goal in
1735 refresh_sequent notebook ;
1736 refresh_proof output
1738 RefreshSequentException e ->
1739 output_html outputhtml
1740 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1741 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1742 ProofEngine.proof := savedproof ;
1743 ProofEngine.goal := savedgoal ;
1744 refresh_sequent notebook
1745 | RefreshProofException e ->
1746 output_html outputhtml
1747 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1748 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1749 ProofEngine.proof := savedproof ;
1750 ProofEngine.goal := savedgoal ;
1751 refresh_sequent notebook ;
1752 refresh_proof output
1754 output_html outputhtml
1755 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1756 ProofEngine.proof := savedproof ;
1757 ProofEngine.goal := savedgoal ;
1761 let call_tactic_with_input tactic () =
1762 let notebook = (rendering_window ())#notebook in
1763 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1764 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1765 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1766 let savedproof = !ProofEngine.proof in
1767 let savedgoal = !ProofEngine.goal in
1768 let uri,metasenv,bo,ty =
1769 match !ProofEngine.proof with
1770 None -> assert false
1771 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1773 let canonical_context =
1774 match !ProofEngine.goal with
1775 None -> assert false
1777 let (_,canonical_context,_) =
1778 List.find (function (m,_,_) -> m=metano) metasenv
1783 let metasenv',expr =
1784 inputt#get_metasenv_and_term canonical_context metasenv
1786 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1788 refresh_sequent notebook ;
1789 refresh_proof output ;
1792 RefreshSequentException e ->
1793 output_html outputhtml
1794 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1795 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1796 ProofEngine.proof := savedproof ;
1797 ProofEngine.goal := savedgoal ;
1798 refresh_sequent notebook
1799 | RefreshProofException e ->
1800 output_html outputhtml
1801 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1802 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1803 ProofEngine.proof := savedproof ;
1804 ProofEngine.goal := savedgoal ;
1805 refresh_sequent notebook ;
1806 refresh_proof output
1808 output_html outputhtml
1809 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1810 ProofEngine.proof := savedproof ;
1811 ProofEngine.goal := savedgoal ;
1814 let call_tactic_with_goal_input tactic () =
1815 let module L = LogicalOperations in
1816 let module G = Gdome in
1817 let notebook = (rendering_window ())#notebook in
1818 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1819 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1820 let savedproof = !ProofEngine.proof in
1821 let savedgoal = !ProofEngine.goal in
1822 match notebook#proofw#get_selections with
1825 ((node : Gdome.element)#getAttributeNS
1826 ~namespaceURI:Misc.helmns
1827 ~localName:(G.domString "xref"))#to_string
1829 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1833 match !current_goal_infos with
1834 Some (ids_to_terms, ids_to_father_ids,_) ->
1836 tactic (Hashtbl.find ids_to_terms id) ;
1837 refresh_sequent notebook ;
1838 refresh_proof output
1839 | None -> assert false (* "ERROR: No current term!!!" *)
1841 RefreshSequentException e ->
1842 output_html outputhtml
1843 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1844 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1845 ProofEngine.proof := savedproof ;
1846 ProofEngine.goal := savedgoal ;
1847 refresh_sequent notebook
1848 | RefreshProofException e ->
1849 output_html outputhtml
1850 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1851 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1852 ProofEngine.proof := savedproof ;
1853 ProofEngine.goal := savedgoal ;
1854 refresh_sequent notebook ;
1855 refresh_proof output
1857 output_html outputhtml
1858 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1859 ProofEngine.proof := savedproof ;
1860 ProofEngine.goal := savedgoal ;
1863 output_html outputhtml
1864 ("<h1 color=\"red\">No term selected</h1>")
1866 output_html outputhtml
1867 ("<h1 color=\"red\">Many terms selected</h1>")
1870 let call_tactic_with_goal_inputs tactic () =
1871 let module L = LogicalOperations in
1872 let module G = Gdome in
1873 let notebook = (rendering_window ())#notebook in
1875 ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1876 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1877 let savedproof = !ProofEngine.proof in
1878 let savedgoal = !ProofEngine.goal in
1880 let term_of_node node =
1882 ((node : Gdome.element)#getAttributeNS
1883 ~namespaceURI:Misc.helmns
1884 ~localName:(G.domString "xref"))#to_string
1886 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1888 match !current_goal_infos with
1889 Some (ids_to_terms, ids_to_father_ids,_) ->
1891 (Hashtbl.find ids_to_terms id)
1892 | None -> assert false (* "ERROR: No current term!!!" *)
1894 match notebook#proofw#get_selections with
1896 output_html outputhtml
1897 ("<h1 color=\"red\">No term selected</h1>")
1899 let terms = List.map term_of_node l in
1900 match !current_goal_infos with
1901 Some (ids_to_terms, ids_to_father_ids,_) ->
1903 refresh_sequent notebook ;
1904 refresh_proof output
1905 | None -> assert false (* "ERROR: No current term!!!" *)
1907 RefreshSequentException e ->
1908 output_html outputhtml
1909 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1910 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1911 ProofEngine.proof := savedproof ;
1912 ProofEngine.goal := savedgoal ;
1913 refresh_sequent notebook
1914 | RefreshProofException e ->
1915 output_html outputhtml
1916 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1917 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1918 ProofEngine.proof := savedproof ;
1919 ProofEngine.goal := savedgoal ;
1920 refresh_sequent notebook ;
1921 refresh_proof output
1923 output_html outputhtml
1924 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1925 ProofEngine.proof := savedproof ;
1926 ProofEngine.goal := savedgoal
1929 let call_tactic_with_input_and_goal_input tactic () =
1930 let module L = LogicalOperations in
1931 let module G = Gdome in
1932 let notebook = (rendering_window ())#notebook in
1933 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1934 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1935 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1936 let savedproof = !ProofEngine.proof in
1937 let savedgoal = !ProofEngine.goal in
1938 match notebook#proofw#get_selections with
1941 ((node : Gdome.element)#getAttributeNS
1942 ~namespaceURI:Misc.helmns
1943 ~localName:(G.domString "xref"))#to_string
1945 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1949 match !current_goal_infos with
1950 Some (ids_to_terms, ids_to_father_ids,_) ->
1952 let uri,metasenv,bo,ty =
1953 match !ProofEngine.proof with
1954 None -> assert false
1955 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1957 let canonical_context =
1958 match !ProofEngine.goal with
1959 None -> assert false
1961 let (_,canonical_context,_) =
1962 List.find (function (m,_,_) -> m=metano) metasenv
1964 canonical_context in
1965 let (metasenv',expr) =
1966 inputt#get_metasenv_and_term canonical_context metasenv
1968 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1969 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
1971 refresh_sequent notebook ;
1972 refresh_proof output ;
1974 | None -> assert false (* "ERROR: No current term!!!" *)
1976 RefreshSequentException e ->
1977 output_html outputhtml
1978 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1979 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1980 ProofEngine.proof := savedproof ;
1981 ProofEngine.goal := savedgoal ;
1982 refresh_sequent notebook
1983 | RefreshProofException e ->
1984 output_html outputhtml
1985 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1986 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1987 ProofEngine.proof := savedproof ;
1988 ProofEngine.goal := savedgoal ;
1989 refresh_sequent notebook ;
1990 refresh_proof output
1992 output_html outputhtml
1993 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1994 ProofEngine.proof := savedproof ;
1995 ProofEngine.goal := savedgoal ;
1998 output_html outputhtml
1999 ("<h1 color=\"red\">No term selected</h1>")
2001 output_html outputhtml
2002 ("<h1 color=\"red\">Many terms selected</h1>")
2005 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2006 let module L = LogicalOperations in
2007 let module G = Gdome in
2009 (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
2010 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2011 let savedproof = !ProofEngine.proof in
2012 let savedgoal = !ProofEngine.goal in
2013 match mmlwidget#get_selections with
2016 ((node : Gdome.element)#getAttributeNS
2017 ~namespaceURI:Misc.helmns
2018 ~localName:(G.domString "xref"))#to_string
2020 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2024 match !current_scratch_infos with
2025 (* term is the whole goal in the scratch_area *)
2026 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2028 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2029 let mml = mml_of_cic_term 111 expr in
2030 scratch_window#show () ;
2031 scratch_window#mmlwidget#load_doc ~dom:mml
2032 | None -> assert false (* "ERROR: No current term!!!" *)
2035 output_html outputhtml
2036 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2039 output_html outputhtml
2040 ("<h1 color=\"red\">No term selected</h1>")
2042 output_html outputhtml
2043 ("<h1 color=\"red\">Many terms selected</h1>")
2046 let call_tactic_with_goal_inputs_in_scratch tactic scratch_window () =
2047 let module L = LogicalOperations in
2048 let module G = Gdome in
2050 (scratch_window#mmlwidget : GMathViewAux.multi_selection_math_view) in
2051 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2052 let savedproof = !ProofEngine.proof in
2053 let savedgoal = !ProofEngine.goal in
2054 match mmlwidget#get_selections with
2056 output_html outputhtml
2057 ("<h1 color=\"red\">No term selected</h1>")
2060 match !current_scratch_infos with
2061 (* term is the whole goal in the scratch_area *)
2062 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2063 let term_of_node node =
2065 ((node : Gdome.element)#getAttributeNS
2066 ~namespaceURI:Misc.helmns
2067 ~localName:(G.domString "xref"))#to_string
2069 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2072 Hashtbl.find ids_to_terms id
2074 let terms = List.map term_of_node l in
2075 let expr = tactic terms term in
2076 let mml = mml_of_cic_term 111 expr in
2077 scratch_window#show () ;
2078 scratch_window#mmlwidget#load_doc ~dom:mml
2079 | None -> assert false (* "ERROR: No current term!!!" *)
2082 output_html outputhtml
2083 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2086 let call_tactic_with_hypothesis_input tactic () =
2087 let module L = LogicalOperations in
2088 let module G = Gdome in
2089 let notebook = (rendering_window ())#notebook in
2090 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2091 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2092 let savedproof = !ProofEngine.proof in
2093 let savedgoal = !ProofEngine.goal in
2094 match notebook#proofw#get_selections with
2097 ((node : Gdome.element)#getAttributeNS
2098 ~namespaceURI:Misc.helmns
2099 ~localName:(G.domString "xref"))#to_string
2101 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2105 match !current_goal_infos with
2106 Some (_,_,ids_to_hypotheses) ->
2108 tactic (Hashtbl.find ids_to_hypotheses id) ;
2109 refresh_sequent notebook ;
2110 refresh_proof output
2111 | None -> assert false (* "ERROR: No current term!!!" *)
2113 RefreshSequentException e ->
2114 output_html outputhtml
2115 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2116 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2117 ProofEngine.proof := savedproof ;
2118 ProofEngine.goal := savedgoal ;
2119 refresh_sequent notebook
2120 | RefreshProofException e ->
2121 output_html outputhtml
2122 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2123 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2124 ProofEngine.proof := savedproof ;
2125 ProofEngine.goal := savedgoal ;
2126 refresh_sequent notebook ;
2127 refresh_proof output
2129 output_html outputhtml
2130 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2131 ProofEngine.proof := savedproof ;
2132 ProofEngine.goal := savedgoal ;
2135 output_html outputhtml
2136 ("<h1 color=\"red\">No term selected</h1>")
2138 output_html outputhtml
2139 ("<h1 color=\"red\">Many terms selected</h1>")
2143 let intros = call_tactic (ProofEngine.intros ~mk_fresh_name_callback);;
2144 let exact = call_tactic_with_input ProofEngine.exact;;
2145 let apply = call_tactic_with_input ProofEngine.apply;;
2146 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2147 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2148 let whd = call_tactic_with_goal_inputs ProofEngine.whd;;
2149 let reduce = call_tactic_with_goal_inputs ProofEngine.reduce;;
2150 let simpl = call_tactic_with_goal_inputs ProofEngine.simpl;;
2151 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2152 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2153 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2154 let cut = call_tactic_with_input (ProofEngine.cut ~mk_fresh_name_callback);;
2155 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2156 let letin = call_tactic_with_input (ProofEngine.letin ~mk_fresh_name_callback);;
2157 let ring = call_tactic ProofEngine.ring;;
2158 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2159 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2160 let fourier = call_tactic ProofEngine.fourier;;
2161 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2162 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2163 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2164 let reflexivity = call_tactic ProofEngine.reflexivity;;
2165 let symmetry = call_tactic ProofEngine.symmetry;;
2166 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2167 let exists = call_tactic ProofEngine.exists;;
2168 let split = call_tactic ProofEngine.split;;
2169 let left = call_tactic ProofEngine.left;;
2170 let right = call_tactic ProofEngine.right;;
2171 let assumption = call_tactic ProofEngine.assumption;;
2173 call_tactic_with_goal_inputs (ProofEngine.generalize ~mk_fresh_name_callback);;
2174 let absurd = call_tactic_with_input ProofEngine.absurd;;
2175 let contradiction = call_tactic ProofEngine.contradiction;;
2177 call_tactic_with_input
2178 (ProofEngine.decompose ~uris_choice_callback:decompose_uris_choice_callback);;
2180 let whd_in_scratch scratch_window =
2181 call_tactic_with_goal_inputs_in_scratch ProofEngine.whd_in_scratch
2184 let reduce_in_scratch scratch_window =
2185 call_tactic_with_goal_inputs_in_scratch ProofEngine.reduce_in_scratch
2188 let simpl_in_scratch scratch_window =
2189 call_tactic_with_goal_inputs_in_scratch ProofEngine.simpl_in_scratch
2195 (**********************)
2196 (* END OF TACTICS *)
2197 (**********************)
2201 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2203 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2206 output_html outputhtml
2207 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2210 exception NotADefinition;;
2213 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2214 let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2215 let notebook = (rendering_window ())#notebook in
2217 let uri = input_or_locate_uri ~title:"Open" in
2218 CicTypeChecker.typecheck uri ;
2219 let metasenv,bo,ty =
2220 match CicEnvironment.get_cooked_obj uri with
2221 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2222 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2225 | Cic.InductiveDefinition _ -> raise NotADefinition
2227 ProofEngine.proof :=
2228 Some (uri, metasenv, bo, ty) ;
2229 ProofEngine.goal := None ;
2230 refresh_sequent notebook ;
2231 refresh_proof output
2233 RefreshSequentException e ->
2234 output_html outputhtml
2235 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2236 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2237 | RefreshProofException e ->
2238 output_html outputhtml
2239 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2240 "proof: " ^ Printexc.to_string e ^ "</h1>")
2242 output_html outputhtml
2243 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2246 let show_query_results results =
2249 ~modal:false ~title:"Query results." ~border_width:2 () in
2250 let vbox = GPack.vbox ~packing:window#add () in
2252 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2255 ~text:"Click on a URI to show that object"
2256 ~packing:hbox#add () in
2257 let scrolled_window =
2258 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2259 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2260 let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2263 (function (uri,_) ->
2267 clist#set_row ~selectable:false n
2270 clist#columns_autosize () ;
2272 (clist#connect#select_row
2273 (fun ~row ~column ~event ->
2274 let (uristr,_) = List.nth results row in
2276 Misc.cic_textual_parser_uri_of_string
2277 (Misc.wrong_xpointer_format_from_wrong_xpointer_format'
2280 CicTextualParser0.ConUri uri
2281 | CicTextualParser0.VarUri uri
2282 | CicTextualParser0.IndTyUri (uri,_)
2283 | CicTextualParser0.IndConUri (uri,_,_) ->
2284 show_in_show_window_uri uri
2290 let refine_constraints (must_obj,must_rel,must_sort) =
2291 let chosen = ref false in
2292 let use_only = ref false in
2295 ~modal:true ~title:"Constraints refinement."
2296 ~width:800 ~border_width:2 () in
2297 let vbox = GPack.vbox ~packing:window#add () in
2299 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2302 ~text: "\"Only\" constraints can be enforced or not."
2303 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2305 GButton.toggle_button ~label:"Enforce \"only\" constraints"
2306 ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2309 (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2310 (* Notebook for the constraints choice *)
2312 GPack.notebook ~scrollable:true
2313 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2314 (* Rel constraints *)
2317 ~text: "Constraints on Rels" () in
2319 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2322 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2325 ~text: "You can now specify the constraints on Rels."
2326 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2327 let expected_height = 25 * (List.length must_rel + 2) in
2328 let height = if expected_height > 400 then 400 else expected_height in
2329 let scrolled_window =
2330 GBin.scrolled_window ~border_width:10 ~height ~width:600
2331 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2332 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2333 let rel_constraints =
2335 (function (position,depth) ->
2338 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2342 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2344 None -> position, ref None
2346 let mutable_ref = ref (Some depth') in
2348 GButton.toggle_button
2349 ~label:("depth = " ^ string_of_int depth') ~active:true
2350 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2353 (depthb#connect#toggled
2355 let sel_depth = if depthb#active then Some depth' else None in
2356 mutable_ref := sel_depth
2358 position, mutable_ref
2360 (* Sort constraints *)
2363 ~text: "Constraints on Sorts" () in
2365 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2368 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2371 ~text: "You can now specify the constraints on Sorts."
2372 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2373 let expected_height = 25 * (List.length must_sort + 2) in
2374 let height = if expected_height > 400 then 400 else expected_height in
2375 let scrolled_window =
2376 GBin.scrolled_window ~border_width:10 ~height ~width:600
2377 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2378 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2379 let sort_constraints =
2381 (function (position,depth,sort) ->
2384 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2387 ~text:(sort ^ " " ^ position)
2388 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2390 None -> position, ref None, sort
2392 let mutable_ref = ref (Some depth') in
2394 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2396 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2399 (depthb#connect#toggled
2401 let sel_depth = if depthb#active then Some depth' else None in
2402 mutable_ref := sel_depth
2404 position, mutable_ref, sort
2406 (* Obj constraints *)
2409 ~text: "Constraints on constants" () in
2411 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2414 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2417 ~text: "You can now specify the constraints on constants."
2418 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2419 let expected_height = 25 * (List.length must_obj + 2) in
2420 let height = if expected_height > 400 then 400 else expected_height in
2421 let scrolled_window =
2422 GBin.scrolled_window ~border_width:10 ~height ~width:600
2423 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2424 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2425 let obj_constraints =
2427 (function (uri,position,depth) ->
2430 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2433 ~text:(uri ^ " " ^ position)
2434 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2436 None -> uri, position, ref None
2438 let mutable_ref = ref (Some depth') in
2440 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2442 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2445 (depthb#connect#toggled
2447 let sel_depth = if depthb#active then Some depth' else None in
2448 mutable_ref := sel_depth
2450 uri, position, mutable_ref
2452 (* Confirm/abort buttons *)
2454 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2456 GButton.button ~label:"Ok"
2457 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2459 GButton.button ~label:"Abort"
2460 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2462 ignore (window#connect#destroy GMain.Main.quit) ;
2463 ignore (cancelb#connect#clicked window#destroy) ;
2465 (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2466 window#set_position `CENTER ;
2468 GMain.Main.main () ;
2470 let chosen_must_rel =
2472 (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2473 let chosen_must_sort =
2475 (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2478 let chosen_must_obj =
2480 (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2483 (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2485 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2486 Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2494 let completeSearchPattern () =
2495 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
2496 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2498 let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2499 let must = MQueryLevels2.get_constraints expr in
2500 let must',only = refine_constraints must in
2501 let results = MQueryGenerator.searchPattern must' only in
2502 show_query_results results
2505 output_html outputhtml
2506 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2509 let insertQuery () =
2510 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2512 let chosen = ref None in
2515 ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2516 let vbox = GPack.vbox ~packing:window#add () in
2518 GMisc.label ~text:"Insert Query. For Experts Only."
2519 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2520 let scrolled_window =
2521 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2522 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2523 let input = GEdit.text ~editable:true
2524 ~packing:scrolled_window#add () in
2526 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2528 GButton.button ~label:"Ok"
2529 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2531 GButton.button ~label:"Load from file..."
2532 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2534 GButton.button ~label:"Abort"
2535 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2536 ignore (window#connect#destroy GMain.Main.quit) ;
2537 ignore (cancelb#connect#clicked window#destroy) ;
2539 (okb#connect#clicked
2541 chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2543 (loadb#connect#clicked
2546 GToolbox.select_file ~title:"Select Query File" ()
2550 let inch = open_in filename in
2551 let rec read_file () =
2553 let line = input_line inch in
2554 line ^ "\n" ^ read_file ()
2558 let text = read_file () in
2559 input#delete_text 0 input#length ;
2560 ignore (input#insert_text text ~pos:0))) ;
2561 window#set_position `CENTER ;
2563 GMain.Main.main () ;
2568 Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2570 show_query_results results
2573 output_html outputhtml
2574 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2577 let choose_must list_of_must only =
2578 let chosen = ref None in
2579 let user_constraints = ref [] in
2582 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2583 let vbox = GPack.vbox ~packing:window#add () in
2585 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2589 ("You can now specify the genericity of the query. " ^
2590 "The more generic the slower.")
2591 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2593 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2597 "Suggestion: start with faster queries before moving to more generic ones."
2598 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2600 GPack.notebook ~scrollable:true
2601 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2604 let last = List.length list_of_must in
2610 (if !page = 1 then "More generic" else
2611 if !page = last then "More precise" else " ") () in
2612 let expected_height = 25 * (List.length must + 2) in
2613 let height = if expected_height > 400 then 400 else expected_height in
2614 let scrolled_window =
2615 GBin.scrolled_window ~border_width:10 ~height ~width:600
2616 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2618 GList.clist ~columns:2 ~packing:scrolled_window#add
2619 ~titles:["URI" ; "Position"] ()
2623 (function (uri,position) ->
2626 [uri; if position then "MainConclusion" else "Conclusion"]
2628 clist#set_row ~selectable:false n
2631 clist#columns_autosize ()
2634 let label = GMisc.label ~text:"User provided" () in
2636 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2638 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2641 ~text:"Select the constraints that must be satisfied and press OK."
2642 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2643 let expected_height = 25 * (List.length only + 2) in
2644 let height = if expected_height > 400 then 400 else expected_height in
2645 let scrolled_window =
2646 GBin.scrolled_window ~border_width:10 ~height ~width:600
2647 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2649 GList.clist ~columns:2 ~packing:scrolled_window#add
2650 ~selection_mode:`EXTENDED
2651 ~titles:["URI" ; "Position"] ()
2655 (function (uri,position) ->
2658 [uri; if position then "MainConclusion" else "Conclusion"]
2660 clist#set_row ~selectable:true n
2663 clist#columns_autosize () ;
2665 (clist#connect#select_row
2666 (fun ~row ~column ~event ->
2667 user_constraints := (List.nth only row)::!user_constraints)) ;
2669 (clist#connect#unselect_row
2670 (fun ~row ~column ~event ->
2673 (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2676 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2678 GButton.button ~label:"Ok"
2679 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2681 GButton.button ~label:"Abort"
2682 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2684 ignore (window#connect#destroy GMain.Main.quit) ;
2685 ignore (cancelb#connect#clicked window#destroy) ;
2687 (okb#connect#clicked
2688 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2689 window#set_position `CENTER ;
2691 GMain.Main.main () ;
2693 None -> raise NoChoice
2695 if n = List.length list_of_must then
2696 (* user provided constraints *)
2699 List.nth list_of_must n
2702 let searchPattern () =
2703 let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
2704 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2707 match !ProofEngine.proof with
2708 None -> assert false
2709 | Some (_,metasenv,_,_) -> metasenv
2711 match !ProofEngine.goal with
2714 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2715 let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2716 let must = choose_must list_of_must only in
2717 let torigth_restriction (u,b) =
2720 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2722 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2726 let rigth_must = List.map torigth_restriction must in
2727 let rigth_only = Some (List.map torigth_restriction only) in
2729 MQueryGenerator.searchPattern
2730 (rigth_must,[],[]) (rigth_only,None,None) in
2734 Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
2737 " <h1>Backward Query: </h1>" ^
2738 " <pre>" ^ get_last_query result ^ "</pre>"
2740 output_html outputhtml html ;
2742 let rec filter_out =
2746 let tl',exc = filter_out tl in
2749 ProofEngine.can_apply
2750 (term_of_cic_textual_parser_uri
2751 (Misc.cic_textual_parser_uri_of_string uri))
2759 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2760 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2767 " <h1>Objects that can actually be applied: </h1> " ^
2768 String.concat "<br>" uris' ^ exc ^
2769 " <h1>Number of false matches: " ^
2770 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2771 " <h1>Number of good matches: " ^
2772 string_of_int (List.length uris') ^ "</h1>"
2774 output_html outputhtml html' ;
2776 user_uri_choice ~title:"Ambiguous input."
2778 "Many lemmas can be successfully applied. Please, choose one:"
2781 inputt#set_term uri' ;
2785 output_html outputhtml
2786 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2789 let choose_selection mmlwidget (element : Gdome.element option) =
2790 let module G = Gdome in
2791 let rec aux element =
2792 if element#hasAttributeNS
2793 ~namespaceURI:Misc.helmns
2794 ~localName:(G.domString "xref")
2796 mmlwidget#set_selection (Some element)
2799 match element#get_parentNode with
2800 None -> assert false
2801 (*CSC: OCAML DIVERGES!
2802 | Some p -> aux (new G.element_of_node p)
2804 | Some p -> aux (new Gdome.element_of_node p)
2806 GdomeInit.DOMCastException _ ->
2808 "******* trying to select above the document root ********"
2812 | None -> mmlwidget#set_selection None
2815 (* STUFF TO BUILD THE GTK INTERFACE *)
2817 (* Stuff for the widget settings *)
2819 let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
2820 let lastdir = ref (Unix.getcwd ()) in
2823 GToolbox.select_file ~title:"Export to PostScript"
2824 ~dir:lastdir ~filename:"screenshot.ps" ()
2828 output#export_to_postscript ~filename:filename ();
2831 let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing
2832 button_set_transparency export_to_postscript_menu_item
2835 let is_set = button_t1#active in
2836 output#set_font_manager_type
2837 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2840 button_set_anti_aliasing#misc#set_sensitive true ;
2841 button_set_transparency#misc#set_sensitive true ;
2842 export_to_postscript_menu_item#misc#set_sensitive true ;
2846 button_set_anti_aliasing#misc#set_sensitive false ;
2847 button_set_transparency#misc#set_sensitive false ;
2848 export_to_postscript_menu_item#misc#set_sensitive false ;
2852 let set_anti_aliasing output button_set_anti_aliasing () =
2853 output#set_anti_aliasing button_set_anti_aliasing#active
2856 let set_transparency output button_set_transparency () =
2857 output#set_transparency button_set_transparency#active
2860 let changefont output font_size_spinb () =
2861 output#set_font_size font_size_spinb#value_as_int
2864 let set_log_verbosity output log_verbosity_spinb () =
2865 output#set_log_verbosity log_verbosity_spinb#value_as_int
2868 class settings_window (output : GMathViewAux.single_selection_math_view) sw
2869 export_to_postscript_menu_item selection_changed_callback
2871 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2873 GPack.vbox ~packing:settings_window#add () in
2876 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2877 ~border_width:5 ~packing:vbox#add () in
2879 GButton.toggle_button ~label:"activate t1 fonts"
2880 ~packing:(table#attach ~left:0 ~top:0) () in
2881 let button_set_anti_aliasing =
2882 GButton.toggle_button ~label:"set_anti_aliasing"
2883 ~packing:(table#attach ~left:0 ~top:1) () in
2884 let button_set_transparency =
2885 GButton.toggle_button ~label:"set_transparency"
2886 ~packing:(table#attach ~left:2 ~top:1) () in
2889 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2890 ~border_width:5 ~packing:vbox#add () in
2891 let font_size_label =
2892 GMisc.label ~text:"font size:"
2893 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2894 let font_size_spinb =
2896 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2899 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2900 let log_verbosity_label =
2901 GMisc.label ~text:"log verbosity:"
2902 ~packing:(table#attach ~left:0 ~top:1) () in
2903 let log_verbosity_spinb =
2905 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2908 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2910 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2912 GButton.button ~label:"Close"
2913 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2915 method show = settings_window#show
2917 button_set_anti_aliasing#misc#set_sensitive false ;
2918 button_set_transparency#misc#set_sensitive false ;
2919 (* Signals connection *)
2920 ignore(button_t1#connect#clicked
2921 (activate_t1 output button_set_anti_aliasing
2922 button_set_transparency export_to_postscript_menu_item button_t1)) ;
2923 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2924 ignore(button_set_anti_aliasing#connect#toggled
2925 (set_anti_aliasing output button_set_anti_aliasing));
2926 ignore(button_set_transparency#connect#toggled
2927 (set_transparency output button_set_transparency)) ;
2928 ignore(log_verbosity_spinb#connect#changed
2929 (set_log_verbosity output log_verbosity_spinb)) ;
2930 ignore(closeb#connect#clicked settings_window#misc#hide)
2933 (* Scratch window *)
2935 class scratch_window =
2937 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2939 GPack.vbox ~packing:window#add () in
2941 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2943 GButton.button ~label:"Whd"
2944 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2946 GButton.button ~label:"Reduce"
2947 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2949 GButton.button ~label:"Simpl"
2950 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2951 let scrolled_window =
2952 GBin.scrolled_window ~border_width:10
2953 ~packing:(vbox#pack ~expand:true ~padding:5) () in
2955 GMathViewAux.multi_selection_math_view
2956 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2958 method mmlwidget = mmlwidget
2959 method show () = window#misc#hide () ; window#show ()
2961 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2962 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2963 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2964 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2965 ignore(simplb#connect#clicked (simpl_in_scratch self))
2968 let open_contextual_menu_for_selected_terms mmlwidget infos =
2969 let button = GdkEvent.Button.button infos in
2970 let terms_selected = List.length mmlwidget#get_selections > 0 in
2973 let time = GdkEvent.Button.time infos in
2974 let menu = GMenu.menu () in
2975 let f = new GMenu.factory menu in
2977 f#add_item "Whd" ~key:GdkKeysyms._W ~callback:whd in
2978 let reduce_menu_item =
2979 f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:reduce in
2980 let simpl_menu_item =
2981 f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:simpl in
2982 let _ = f#add_separator () in
2983 let generalize_menu_item =
2984 f#add_item "Generalize" ~key:GdkKeysyms._G ~callback:generalize in
2985 let _ = f#add_separator () in
2986 let clear_menu_item =
2987 f#add_item "Clear" ~key:GdkKeysyms._C ~callback:clear in
2988 let clearbody_menu_item =
2989 f#add_item "ClearBody" ~key:GdkKeysyms._B ~callback:clearbody
2991 whd_menu_item#misc#set_sensitive terms_selected ;
2992 reduce_menu_item#misc#set_sensitive terms_selected ;
2993 simpl_menu_item#misc#set_sensitive terms_selected ;
2994 generalize_menu_item#misc#set_sensitive terms_selected ;
2995 clear_menu_item#misc#set_sensitive terms_selected ;
2996 clearbody_menu_item#misc#set_sensitive terms_selected ;
2997 menu#popup ~button ~time
3003 let vbox1 = GPack.vbox () in
3005 val mutable proofw_ref = None
3006 val mutable compute_ref = None
3008 Lazy.force self#compute ;
3009 match proofw_ref with
3010 None -> assert false
3011 | Some proofw -> proofw
3012 method content = vbox1
3014 match compute_ref with
3015 None -> assert false
3016 | Some compute -> compute
3020 let scrolled_window1 =
3021 GBin.scrolled_window ~border_width:10
3022 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3024 GMathViewAux.multi_selection_math_view ~width:400 ~height:275
3025 ~packing:(scrolled_window1#add) () in
3026 let _ = proofw_ref <- Some proofw in
3028 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3030 GButton.button ~label:"Ring"
3031 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3033 GButton.button ~label:"Fourier"
3034 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3036 GButton.button ~label:"Reflexivity"
3037 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3039 GButton.button ~label:"Symmetry"
3040 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3042 GButton.button ~label:"Assumption"
3043 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3044 let contradictionb =
3045 GButton.button ~label:"Contradiction"
3046 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3048 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3050 GButton.button ~label:"Exists"
3051 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3053 GButton.button ~label:"Split"
3054 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3056 GButton.button ~label:"Left"
3057 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3059 GButton.button ~label:"Right"
3060 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3061 let searchpatternb =
3062 GButton.button ~label:"SearchPattern_Apply"
3063 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3065 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3067 GButton.button ~label:"Exact"
3068 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3070 GButton.button ~label:"Intros"
3071 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3073 GButton.button ~label:"Apply"
3074 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3075 let elimintrossimplb =
3076 GButton.button ~label:"ElimIntrosSimpl"
3077 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3079 GButton.button ~label:"ElimType"
3080 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3082 GButton.button ~label:"Fold_whd"
3083 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3085 GButton.button ~label:"Fold_reduce"
3086 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3088 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3090 GButton.button ~label:"Fold_simpl"
3091 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3093 GButton.button ~label:"Cut"
3094 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3096 GButton.button ~label:"Change"
3097 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3099 GButton.button ~label:"Let ... In"
3100 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3102 GButton.button ~label:"RewriteSimpl ->"
3103 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3104 let rewritebacksimplb =
3105 GButton.button ~label:"RewriteSimpl <-"
3106 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3108 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3110 GButton.button ~label:"Absurd"
3111 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3113 GButton.button ~label:"Decompose"
3114 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3116 GButton.button ~label:"Transitivity"
3117 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3119 GButton.button ~label:"Replace"
3120 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3121 (* Zack: spostare in una toolbar
3123 GButton.button ~label:"Generalize"
3124 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3126 GButton.button ~label:"ClearBody"
3127 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3129 GButton.button ~label:"Clear"
3130 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3132 GButton.button ~label:"Whd"
3133 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3135 GButton.button ~label:"Reduce"
3136 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3138 GButton.button ~label:"Simpl"
3139 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3142 ignore(exactb#connect#clicked exact) ;
3143 ignore(applyb#connect#clicked apply) ;
3144 ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3145 ignore(elimtypeb#connect#clicked elimtype) ;
3146 ignore(foldwhdb#connect#clicked fold_whd) ;
3147 ignore(foldreduceb#connect#clicked fold_reduce) ;
3148 ignore(foldsimplb#connect#clicked fold_simpl) ;
3149 ignore(cutb#connect#clicked cut) ;
3150 ignore(changeb#connect#clicked change) ;
3151 ignore(letinb#connect#clicked letin) ;
3152 ignore(ringb#connect#clicked ring) ;
3153 ignore(fourierb#connect#clicked fourier) ;
3154 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3155 ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3156 ignore(replaceb#connect#clicked replace) ;
3157 ignore(reflexivityb#connect#clicked reflexivity) ;
3158 ignore(symmetryb#connect#clicked symmetry) ;
3159 ignore(transitivityb#connect#clicked transitivity) ;
3160 ignore(existsb#connect#clicked exists) ;
3161 ignore(splitb#connect#clicked split) ;
3162 ignore(leftb#connect#clicked left) ;
3163 ignore(rightb#connect#clicked right) ;
3164 ignore(assumptionb#connect#clicked assumption) ;
3165 ignore(absurdb#connect#clicked absurd) ;
3166 ignore(contradictionb#connect#clicked contradiction) ;
3167 ignore(introsb#connect#clicked intros) ;
3168 ignore(searchpatternb#connect#clicked searchPattern) ;
3169 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3171 ((new GObj.event_ops proofw#as_widget)#connect#button_press
3172 (open_contextual_menu_for_selected_terms proofw)) ;
3173 ignore(decomposeb#connect#clicked decompose) ;
3174 (* Zack: spostare in una toolbar
3175 ignore(whdb#connect#clicked whd) ;
3176 ignore(reduceb#connect#clicked reduce) ;
3177 ignore(simplb#connect#clicked simpl) ;
3178 ignore(clearbodyb#connect#clicked clearbody) ;
3179 ignore(clearb#connect#clicked clear) ;
3180 ignore(generalizeb#connect#clicked generalize) ;
3187 let vbox1 = GPack.vbox () in
3188 let scrolled_window1 =
3189 GBin.scrolled_window ~border_width:10
3190 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3192 GMathViewAux.single_selection_math_view ~width:400 ~height:275
3193 ~packing:(scrolled_window1#add) () in
3195 method proofw = (assert false : GMathViewAux.single_selection_math_view)
3196 method content = vbox1
3197 method compute = (assert false : unit)
3201 let empty_page = new empty_page;;
3205 val notebook = GPack.notebook ()
3207 val mutable skip_switch_page_event = false
3208 val mutable empty = true
3209 method notebook = notebook
3211 let new_page = new page () in
3213 pages := !pages @ [n,lazy (setgoal n),new_page] ;
3214 notebook#append_page
3215 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3216 new_page#content#coerce
3217 method remove_all_pages ~skip_switch_page_event:skip =
3219 notebook#remove_page 0 (* let's remove the empty page *)
3221 List.iter (function _ -> notebook#remove_page 0) !pages ;
3223 skip_switch_page_event <- skip
3224 method set_current_page ~may_skip_switch_page_event n =
3225 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3226 let new_page = notebook#page_num page#content#coerce in
3227 if may_skip_switch_page_event && new_page <> notebook#current_page then
3228 skip_switch_page_event <- true ;
3229 notebook#goto_page new_page
3230 method set_empty_page =
3233 notebook#append_page
3234 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3235 empty_page#content#coerce
3237 let (_,_,page) = List.nth !pages notebook#current_page in
3241 (notebook#connect#switch_page
3243 let skip = skip_switch_page_event in
3244 skip_switch_page_event <- false ;
3247 let (metano,setgoal,page) = List.nth !pages i in
3248 ProofEngine.goal := Some metano ;
3249 Lazy.force (page#compute) ;
3258 class rendering_window output (notebook : notebook) =
3259 let scratch_window = new scratch_window in
3261 GWindow.window ~title:"MathML viewer" ~border_width:0
3262 ~allow_shrink:false () in
3263 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3265 let handle_box = GBin.handle_box ~border_width:2
3266 ~packing:(vbox_for_menu#pack ~padding:0) () in
3267 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3268 let factory0 = new GMenu.factory menubar in
3269 let accel_group = factory0#accel_group in
3271 let file_menu = factory0#add_submenu "File" in
3272 let factory1 = new GMenu.factory file_menu ~accel_group in
3273 let export_to_postscript_menu_item =
3276 factory1#add_item "New Block of (Co)Inductive Definitions..."
3277 ~key:GdkKeysyms._B ~callback:new_inductive
3280 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3283 let reopen_menu_item =
3284 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3288 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3289 ignore (factory1#add_separator ()) ;
3291 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3293 let save_menu_item =
3294 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3297 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3298 ignore (!save_set_sensitive false);
3299 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3300 ignore (!qed_set_sensitive false);
3301 ignore (factory1#add_separator ()) ;
3302 let export_to_postscript_menu_item =
3303 factory1#add_item "Export to PostScript..."
3304 ~callback:(export_to_postscript output) in
3305 ignore (factory1#add_separator ()) ;
3307 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3308 export_to_postscript_menu_item
3311 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3312 let factory2 = new GMenu.factory edit_menu ~accel_group in
3313 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3314 let proveit_menu_item =
3315 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3316 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3318 let focus_menu_item =
3319 factory2#add_item "Focus" ~key:GdkKeysyms._F
3320 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3323 focus_and_proveit_set_sensitive :=
3325 proveit_menu_item#misc#set_sensitive b ;
3326 focus_menu_item#misc#set_sensitive b
3328 let _ = !focus_and_proveit_set_sensitive false in
3329 (* edit term menu *)
3330 let edit_term_menu = factory0#add_submenu "Edit Term" in
3331 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3332 let check_menu_item =
3333 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3334 ~callback:(check scratch_window) in
3335 let _ = check_menu_item#misc#set_sensitive false in
3337 let settings_menu = factory0#add_submenu "Search" in
3338 let factory4 = new GMenu.factory settings_menu ~accel_group in
3340 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3342 let searchPattern_menu_item =
3343 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3344 ~callback:completeSearchPattern in
3345 let _ = searchPattern_menu_item#misc#set_sensitive false in
3346 let show_menu_item =
3347 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3349 let insert_query_item =
3350 factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3351 ~callback:insertQuery in
3353 let settings_menu = factory0#add_submenu "Settings" in
3354 let factory3 = new GMenu.factory settings_menu ~accel_group in
3356 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3357 ~callback:edit_aliases in
3358 let _ = factory3#add_separator () in
3360 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3361 ~callback:(function _ -> (settings_window ())#show ()) in
3363 let _ = window#add_accel_group accel_group in
3367 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3369 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3370 let scrolled_window0 =
3371 GBin.scrolled_window ~border_width:10
3372 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3373 let _ = scrolled_window0#add output#coerce in
3375 GBin.frame ~label:"Insert Term"
3376 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3377 let scrolled_window1 =
3378 GBin.scrolled_window ~border_width:5
3379 ~packing:frame#add () in
3381 TermEditor'.term_editor
3382 ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3383 ~isnotempty_callback:
3385 check_menu_item#misc#set_sensitive b ;
3386 searchPattern_menu_item#misc#set_sensitive b) in
3388 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3390 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3392 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3396 ~source:"<html><body bgColor=\"white\"></body></html>"
3397 ~width:400 ~height: 100
3402 method outputhtml = outputhtml
3403 method inputt = inputt
3404 method output = (output : GMathViewAux.single_selection_math_view)
3405 method notebook = notebook
3406 method show = window#show
3408 notebook#set_empty_page ;
3409 export_to_postscript_menu_item#misc#set_sensitive false ;
3410 check_term := (check_term_in_scratch scratch_window) ;
3412 (* signal handlers here *)
3413 ignore(output#connect#selection_changed
3415 choose_selection output elem ;
3416 !focus_and_proveit_set_sensitive true
3418 ignore (output#connect#click (show_in_show_window_callback output)) ;
3419 let settings_window = new settings_window output scrolled_window0
3420 export_to_postscript_menu_item (choose_selection output) in
3421 set_settings_window settings_window ;
3422 set_outputhtml outputhtml ;
3423 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3424 Logger.log_callback :=
3425 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3430 let initialize_everything () =
3431 let module U = Unix in
3432 let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in
3433 let notebook = new notebook in
3434 let rendering_window' = new rendering_window output notebook in
3435 set_rendering_window rendering_window' ;
3436 mml_of_cic_term_ref := mml_of_cic_term ;
3437 rendering_window'#show () ;
3444 Mqint.set_database Mqint.postgres_db ;
3445 Mqint.init postgresqlconnectionstring ;
3447 ignore (GtkMain.Main.init ()) ;
3448 initialize_everything () ;
3449 if !usedb then Mqint.close ();