1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
40 let index_sharp = String.index uri '#' in
41 let index_rest = index_sharp + 10 in
42 let baseuri = String.sub uri 0 index_sharp in
43 let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
48 (* GLOBAL CONSTANTS *)
50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
51 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
55 " <body bgColor=\"white\">"
65 Sys.getenv "GTOPLEVEL_PROOFFILE"
67 Not_found -> "/public/currentproof"
72 Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
74 Not_found -> "/public/currentprooftype"
77 (*CSC: the getter should handle the innertypes, not the FS *)
81 Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
83 Not_found -> "/public/innertypes"
86 let constanttypefile =
88 Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
90 Not_found -> "/public/constanttype"
93 let postgresqlconnectionstring =
95 Sys.getenv "POSTGRESQL_CONNECTION_STRING"
97 Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
100 let empty_id_to_uris = ([],function _ -> None);;
103 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
105 let htmlheader_and_content = ref htmlheader;;
107 let current_cic_infos = ref None;;
108 let current_goal_infos = ref None;;
109 let current_scratch_infos = ref None;;
111 let id_to_uris = ref empty_id_to_uris;;
113 let check_term = ref (fun _ _ _ -> assert false);;
114 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
116 exception RenderingWindowsNotInitialized;;
118 let set_rendering_window,rendering_window =
119 let rendering_window_ref = ref None in
120 (function rw -> rendering_window_ref := Some rw),
122 match !rendering_window_ref with
123 None -> raise RenderingWindowsNotInitialized
128 exception SettingsWindowsNotInitialized;;
130 let set_settings_window,settings_window =
131 let settings_window_ref = ref None in
132 (function rw -> settings_window_ref := Some rw),
134 match !settings_window_ref with
135 None -> raise SettingsWindowsNotInitialized
140 exception OutputHtmlNotInitialized;;
142 let set_outputhtml,outputhtml =
143 let outputhtml_ref = ref None in
144 (function rw -> outputhtml_ref := Some rw),
146 match !outputhtml_ref with
147 None -> raise OutputHtmlNotInitialized
148 | Some outputhtml -> outputhtml
152 exception QedSetSensitiveNotInitialized;;
153 let qed_set_sensitive =
154 ref (function _ -> raise QedSetSensitiveNotInitialized)
157 exception SaveSetSensitiveNotInitialized;;
158 let save_set_sensitive =
159 ref (function _ -> raise SaveSetSensitiveNotInitialized)
162 (* COMMAND LINE OPTIONS *)
168 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
171 Arg.parse argspec ignore ""
175 exception IllFormedUri of string;;
177 let cic_textual_parser_uri_of_string uri' =
180 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
181 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
183 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
184 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
188 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
189 CicTextualParser0.IndTyUri (uri'',typeno)
192 (* Constructor of an Inductive Type *)
193 let uri'',typeno,consno =
194 CicTextualLexer.indconuri_of_uri uri'
196 CicTextualParser0.IndConUri (uri'',typeno,consno)
199 _ -> raise (IllFormedUri uri')
202 let term_of_cic_textual_parser_uri uri =
203 let module C = Cic in
204 let module CTP = CicTextualParser0 in
206 CTP.ConUri uri -> C.Const (uri,[])
207 | CTP.VarUri uri -> C.Var (uri,[])
208 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
209 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
212 let string_of_cic_textual_parser_uri uri =
213 let module C = Cic in
214 let module CTP = CicTextualParser0 in
217 CTP.ConUri uri -> UriManager.string_of_uri uri
218 | CTP.VarUri uri -> UriManager.string_of_uri uri
219 | CTP.IndTyUri (uri,tyno) ->
220 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
221 | CTP.IndConUri (uri,tyno,consno) ->
222 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
225 (* 4 = String.length "cic:" *)
226 String.sub uri' 4 (String.length uri' - 4)
229 let output_html outputhtml msg =
230 htmlheader_and_content := !htmlheader_and_content ^ msg ;
231 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
232 outputhtml#set_topline (-1)
235 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
239 let check_window outputhtml uris =
242 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
244 GPack.notebook ~scrollable:true ~packing:window#add () in
249 let scrolled_window =
250 GBin.scrolled_window ~border_width:10
252 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
258 ~packing:scrolled_window#add ~width:400 ~height:280 () in
261 term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
263 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
266 let mml = !mml_of_cic_term_ref 111 expr in
267 mmlwidget#load_tree ~dom:mml
270 output_html outputhtml
271 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
276 (notebook#connect#switch_page
277 (function i -> Lazy.force (List.nth render_terms i)))
283 interactive_user_uri_choice ~selection_mode ?(ok="Ok")
284 ?(enable_button_for_non_vars=false) ~title ~msg uris
286 let choices = ref [] in
287 let chosen = ref false in
288 let use_only_constants = ref false in
290 GWindow.dialog ~modal:true ~title ~width:600 () in
292 GMisc.label ~text:msg
293 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
294 let scrolled_window =
295 GBin.scrolled_window ~border_width:10
296 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
298 let expected_height = 18 * List.length uris in
299 let height = if expected_height > 400 then 400 else expected_height in
300 GList.clist ~columns:1 ~packing:scrolled_window#add
301 ~height ~selection_mode () in
302 let _ = List.map (function x -> clist#append [x]) uris in
304 GPack.hbox ~border_width:0
305 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
307 GMisc.label ~text:"None of the above. Try this one:"
308 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
310 GEdit.entry ~editable:true
311 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
313 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
315 GButton.button ~label:ok
316 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
317 let _ = okb#misc#set_sensitive false in
322 if enable_button_for_non_vars then
323 hbox#pack ~expand:false ~fill:false ~padding:5 w)
324 ~label:"Try constants only" () in
326 GButton.button ~label:"Check"
327 ~packing:(hbox#pack ~padding:5) () in
328 let _ = checkb#misc#set_sensitive false in
330 GButton.button ~label:"Abort"
331 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
333 let check_callback () =
334 assert (List.length !choices > 0) ;
335 check_window (outputhtml ()) !choices
337 ignore (window#connect#destroy GMain.Main.quit) ;
338 ignore (cancelb#connect#clicked window#destroy) ;
340 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
342 (nonvarsb#connect#clicked
344 use_only_constants := true ;
348 ignore (checkb#connect#clicked check_callback) ;
350 (clist#connect#select_row
351 (fun ~row ~column ~event ->
352 checkb#misc#set_sensitive true ;
353 okb#misc#set_sensitive true ;
354 choices := (List.nth uris row)::!choices)) ;
356 (clist#connect#unselect_row
357 (fun ~row ~column ~event ->
359 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
361 (manual_input#connect#changed
363 if manual_input#text = "" then
366 checkb#misc#set_sensitive false ;
367 okb#misc#set_sensitive false ;
368 clist#misc#set_sensitive true
372 choices := [manual_input#text] ;
373 clist#unselect_all () ;
374 checkb#misc#set_sensitive true ;
375 okb#misc#set_sensitive true ;
376 clist#misc#set_sensitive false
378 window#set_position `CENTER ;
382 if !use_only_constants then
384 (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
387 if List.length !choices > 0 then !choices else raise NoChoice
392 let interactive_interpretation_choice interpretations =
393 let chosen = ref None in
396 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
397 let vbox = GPack.vbox ~packing:window#add () in
401 ("Ambiguous input since there are many well-typed interpretations." ^
402 " Please, choose one of them.")
403 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
405 GPack.notebook ~scrollable:true
406 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
409 (function interpretation ->
411 let expected_height = 18 * List.length interpretation in
412 let height = if expected_height > 400 then 400 else expected_height in
413 GList.clist ~columns:2 ~packing:notebook#append_page ~height
414 ~titles:["id" ; "URI"] ()
418 (function (id,uri) ->
419 let n = clist#append [id;uri] in
420 clist#set_row ~selectable:false n
423 clist#columns_autosize ()
426 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
428 GButton.button ~label:"Ok"
429 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
431 GButton.button ~label:"Abort"
432 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
434 ignore (window#connect#destroy GMain.Main.quit) ;
435 ignore (cancelb#connect#clicked window#destroy) ;
438 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
439 window#set_position `CENTER ;
443 None -> raise NoChoice
450 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
452 let query = ref "" in
453 MQueryGenerator.set_confirm_query
454 (function q -> query := MQueryUtil.text_of_query q ; true) ;
455 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
458 let domImpl = Gdome.domImplementation ();;
460 let parseStyle name =
462 domImpl#createDocumentFromURI
464 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
466 ~uri:("styles/" ^ name) ()
468 Gdome_xslt.processStylesheet style
471 let d_c = parseStyle "drop_coercions.xsl";;
472 let tc1 = parseStyle "objtheorycontent.xsl";;
473 let hc2 = parseStyle "content_to_html.xsl";;
474 let l = parseStyle "link.xsl";;
476 let c1 = parseStyle "rootcontent.xsl";;
477 let g = parseStyle "genmmlid.xsl";;
478 let c2 = parseStyle "annotatedpres.xsl";;
481 let getterURL = Configuration.getter_url;;
482 let processorURL = Configuration.processor_url;;
484 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
485 let mml_args ~explode_all =
486 ("explodeall",(if explode_all then "true()" else "false()"))::
487 ["processorURL", "'" ^ processorURL ^ "'" ;
488 "getterURL", "'" ^ getterURL ^ "'" ;
489 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
490 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
491 "UNICODEvsSYMBOL", "'symbol'" ;
492 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
493 "encoding", "'iso-8859-1'" ;
494 "media-type", "'text/html'" ;
495 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
496 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
497 "naturalLanguage", "'yes'" ;
498 "annotations", "'no'" ;
499 "URLs_or_URIs", "'URIs'" ;
500 "topurl", "'http://phd.cs.unibo.it/helm'" ;
501 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
504 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
506 ["processorURL", "'" ^ processorURL ^ "'" ;
507 "getterURL", "'" ^ getterURL ^ "'" ;
508 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
509 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
510 "UNICODEvsSYMBOL", "'symbol'" ;
511 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
512 "encoding", "'iso-8859-1'" ;
513 "media-type", "'text/html'" ;
514 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
515 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
516 "naturalLanguage", "'no'" ;
517 "annotations", "'no'" ;
518 "explodeall", "true()" ;
519 "URLs_or_URIs", "'URIs'" ;
520 "topurl", "'http://phd.cs.unibo.it/helm'" ;
521 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
524 let parse_file filename =
525 let inch = open_in filename in
526 let rec read_lines () =
528 let line = input_line inch in
536 let applyStylesheets input styles args =
537 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
542 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
544 (*CSC: ????????????????? *)
546 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
550 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
551 ~ask_dtd_to_the_getter:true
555 None -> Xml2Gdome.document_of_xml domImpl xml
557 Xml.pp xml (Some constanttypefile) ;
558 Xml2Gdome.document_of_xml domImpl bodyxml'
560 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
561 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
563 Xml.pp xmlinnertypes (Some innertypesfile) ;
564 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
569 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
572 let struri = UriManager.string_of_uri uri in
573 let idx = (String.rindex struri '/') + 1 in
574 String.sub struri idx (String.length struri - idx)
576 let path = pathname ^ "/" ^ name in
578 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
582 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
583 ~ask_dtd_to_the_getter:false
586 let innertypesuri = UriManager.innertypesuri_of_uri uri in
587 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
588 Getter.register innertypesuri
589 (Configuration.annotations_url ^
590 Str.replace_first (Str.regexp "^cic:") ""
591 (UriManager.string_of_uri innertypesuri) ^ ".xml"
593 (* constant type / variable / mutual inductive types definition *)
594 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
596 (Configuration.annotations_url ^
597 Str.replace_first (Str.regexp "^cic:") ""
598 (UriManager.string_of_uri uri) ^ ".xml"
605 match UriManager.bodyuri_of_uri uri with
607 | Some bodyuri -> bodyuri
609 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
610 Getter.register bodyuri
611 (Configuration.annotations_url ^
612 Str.replace_first (Str.regexp "^cic:") ""
613 (UriManager.string_of_uri bodyuri) ^ ".xml"
620 exception RefreshSequentException of exn;;
621 exception RefreshProofException of exn;;
623 let refresh_proof (output : GMathView.math_view) =
625 let uri,currentproof =
626 match !ProofEngine.proof with
628 | Some (uri,metasenv,bo,ty) ->
629 !qed_set_sensitive (List.length metasenv = 0) ;
630 (*CSC: Wrong: [] is just plainly wrong *)
631 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
634 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
635 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
637 Cic2acic.acic_object_of_cic_object currentproof
640 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
643 output#load_tree mml ;
645 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
648 match !ProofEngine.proof with
650 | Some (uri,metasenv,bo,ty) ->
651 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
652 raise (RefreshProofException e)
655 let refresh_sequent ?(empty_notebook=true) notebook =
657 match !ProofEngine.goal with
659 if empty_notebook then
661 notebook#remove_all_pages ~skip_switch_page_event:false ;
662 notebook#set_empty_page
665 notebook#proofw#unload
668 match !ProofEngine.proof with
670 | Some (_,metasenv,_,_) -> metasenv
672 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
673 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
674 SequentPp.XmlPp.print_sequent metasenv currentsequent
676 let regenerate_notebook () =
677 let skip_switch_page_event =
679 (m,_,_)::_ when m = metano -> false
682 notebook#remove_all_pages ~skip_switch_page_event ;
683 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
685 if empty_notebook then
687 regenerate_notebook () ;
688 notebook#set_current_page ~may_skip_switch_page_event:false metano
692 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
694 applyStylesheets sequent_doc sequent_styles sequent_args
696 notebook#set_current_page ~may_skip_switch_page_event:true metano;
697 notebook#proofw#load_tree ~dom:sequent_mml
699 current_goal_infos :=
700 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
704 match !ProofEngine.goal with
709 match !ProofEngine.proof with
711 | Some (_,metasenv,_,_) -> metasenv
714 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
715 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
716 raise (RefreshSequentException e)
717 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
721 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
722 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
725 let mml_of_cic_term metano term =
727 match !ProofEngine.proof with
729 | Some (_,metasenv,_,_) -> metasenv
732 match !ProofEngine.goal with
735 let (_,canonical_context,_) =
736 List.find (function (m,_,_) -> m=metano) metasenv
740 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
741 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
744 Xml2Gdome.document_of_xml domImpl sequent_gdome
747 applyStylesheets sequent_doc sequent_styles sequent_args ;
749 current_scratch_infos :=
750 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
754 exception OpenConjecturesStillThere;;
755 exception WrongProof;;
757 let pathname_of_annuri uristring =
758 Configuration.annotations_dir ^
759 Str.replace_first (Str.regexp "^cic:") "" uristring
762 let make_dirs dirpath =
763 ignore (Unix.system ("mkdir -p " ^ dirpath))
766 let save_obj uri obj =
768 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
769 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
771 Cic2acic.acic_object_of_cic_object obj
773 (* let's save the theorem and register it to the getter *)
774 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
776 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
781 match !ProofEngine.proof with
783 | Some (uri,[],bo,ty) ->
785 CicReduction.are_convertible []
786 (CicTypeChecker.type_of_aux' [] [] bo) ty
789 (*CSC: Wrong: [] is just plainly wrong *)
790 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
792 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
793 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
795 Cic2acic.acic_object_of_cic_object proof
798 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
801 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
802 !qed_set_sensitive false ;
803 (* let's save the theorem and register it to the getter *)
804 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
806 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
810 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
815 | _ -> raise OpenConjecturesStillThere
819 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
820 match !ProofEngine.proof with
822 | Some (uri, metasenv, bo, ty) ->
824 (*CSC: Wrong: [] is just plainly wrong *)
825 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
827 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
828 Cic2acic.acic_object_of_cic_object currentproof
832 Cic2Xml.print_object uri ~ids_to_inner_sorts
833 ~ask_dtd_to_the_getter:true acurrentproof
835 xml,Some bodyxml -> xml,bodyxml
836 | _,None -> assert false
838 Xml.pp ~quiet:true xml (Some prooffiletype) ;
839 output_html outputhtml
840 ("<h1 color=\"Green\">Current proof type saved to " ^
841 prooffiletype ^ "</h1>") ;
842 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
843 output_html outputhtml
844 ("<h1 color=\"Green\">Current proof body saved to " ^
848 (* Used to typecheck the loaded proofs *)
849 let typecheck_loaded_proof metasenv bo ty =
850 let module T = CicTypeChecker in
853 (fun metasenv ((_,context,ty) as conj) ->
854 ignore (T.type_of_aux' metasenv context ty) ;
857 ignore (T.type_of_aux' metasenv [] ty) ;
858 ignore (T.type_of_aux' metasenv [] bo)
862 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
863 let output = ((rendering_window ())#output : GMathView.math_view) in
864 let notebook = (rendering_window ())#notebook in
867 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
870 None -> raise NoChoice
872 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
873 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
874 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
875 typecheck_loaded_proof metasenv bo ty ;
877 Some (uri, metasenv, bo, ty) ;
881 | (metano,_,_)::_ -> Some metano
883 refresh_proof output ;
884 refresh_sequent notebook ;
885 output_html outputhtml
886 ("<h1 color=\"Green\">Current proof type loaded from " ^
887 prooffiletype ^ "</h1>") ;
888 output_html outputhtml
889 ("<h1 color=\"Green\">Current proof body loaded from " ^
890 prooffile ^ "</h1>") ;
891 !save_set_sensitive true
894 RefreshSequentException e ->
895 output_html outputhtml
896 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
897 "sequent: " ^ Printexc.to_string e ^ "</h1>")
898 | RefreshProofException e ->
899 output_html outputhtml
900 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
901 "proof: " ^ Printexc.to_string e ^ "</h1>")
903 output_html outputhtml
904 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
907 let edit_aliases () =
908 let chosen = ref false in
911 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
913 GPack.vbox ~border_width:0 ~packing:window#add () in
914 let scrolled_window =
915 GBin.scrolled_window ~border_width:10
916 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
917 let input = GEdit.text ~editable:true ~width:400 ~height:100
918 ~packing:scrolled_window#add () in
920 GPack.hbox ~border_width:0
921 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
923 GButton.button ~label:"Ok"
924 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
926 GButton.button ~label:"Cancel"
927 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
928 ignore (window#connect#destroy GMain.Main.quit) ;
929 ignore (cancelb#connect#clicked window#destroy) ;
931 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
932 let dom,resolve_id = !id_to_uris in
934 (input#insert_text ~pos:0
939 match resolve_id v with
944 (string_of_cic_textual_parser_uri uri)
950 let inputtext = input#get_chars 0 input#length in
952 let alfa = "[a-zA-Z_-]" in
953 let digit = "[0-9]" in
954 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
955 let blanks = "\( \|\t\|\n\)+" in
956 let nonblanks = "[^ \t\n]+" in
957 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
959 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
963 let n' = Str.search_forward regexpr inputtext n in
964 let id = Str.matched_group 2 inputtext in
966 cic_textual_parser_uri_of_string
967 ("cic:" ^ (Str.matched_group 5 inputtext))
969 let dom,resolve_id = aux (n' + 1) in
970 if List.mem id dom then
974 (function id' -> if id = id' then Some uri else resolve_id id')
976 Not_found -> empty_id_to_uris
980 id_to_uris := dom,resolve_id
984 let module L = LogicalOperations in
985 let module G = Gdome in
986 let notebook = (rendering_window ())#notebook in
987 let output = (rendering_window ())#output in
988 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
989 match (rendering_window ())#output#get_selection with
992 ((node : Gdome.element)#getAttributeNS
994 ((element : G.element)#getAttributeNS
997 ~localName:(G.domString "xref"))#to_string
999 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1003 match !current_cic_infos with
1004 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1006 L.to_sequent id ids_to_terms ids_to_father_ids ;
1007 refresh_proof output ;
1008 refresh_sequent notebook
1009 | None -> assert false (* "ERROR: No current term!!!" *)
1011 RefreshSequentException e ->
1012 output_html outputhtml
1013 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1014 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1015 | RefreshProofException e ->
1016 output_html outputhtml
1017 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1018 "proof: " ^ Printexc.to_string e ^ "</h1>")
1020 output_html outputhtml
1021 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1023 | None -> assert false (* "ERROR: No selection!!!" *)
1027 let module L = LogicalOperations in
1028 let module G = Gdome in
1029 let notebook = (rendering_window ())#notebook in
1030 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1031 match (rendering_window ())#output#get_selection with
1034 ((node : Gdome.element)#getAttributeNS
1035 (*CSC: OCAML DIVERGE
1036 ((element : G.element)#getAttributeNS
1038 ~namespaceURI:helmns
1039 ~localName:(G.domString "xref"))#to_string
1041 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1045 match !current_cic_infos with
1046 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1048 L.focus id ids_to_terms ids_to_father_ids ;
1049 refresh_sequent notebook
1050 | None -> assert false (* "ERROR: No current term!!!" *)
1052 RefreshSequentException e ->
1053 output_html outputhtml
1054 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1055 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1056 | RefreshProofException e ->
1057 output_html outputhtml
1058 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1059 "proof: " ^ Printexc.to_string e ^ "</h1>")
1061 output_html outputhtml
1062 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1064 | None -> assert false (* "ERROR: No selection!!!" *)
1067 exception NoPrevGoal;;
1068 exception NoNextGoal;;
1070 let setgoal metano =
1071 let module L = LogicalOperations in
1072 let module G = Gdome in
1073 let notebook = (rendering_window ())#notebook in
1074 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1076 match !ProofEngine.proof with
1077 None -> assert false
1078 | Some (_,metasenv,_,_) -> metasenv
1081 refresh_sequent ~empty_notebook:false notebook
1083 RefreshSequentException e ->
1084 output_html outputhtml
1085 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1086 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1088 output_html outputhtml
1089 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1093 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1096 GWindow.window ~width:800 ~border_width:2 () in
1097 let scrolled_window =
1098 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1100 GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1101 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1102 let href = Gdome.domString "href" in
1103 let show_in_show_window_obj uri obj =
1104 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1107 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1108 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1110 Cic2acic.acic_object_of_cic_object obj
1113 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1116 window#set_title (UriManager.string_of_uri uri) ;
1117 window#misc#hide () ; window#show () ;
1118 mmlwidget#load_tree mml ;
1121 output_html outputhtml
1122 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1124 let show_in_show_window_uri uri =
1125 let obj = CicEnvironment.get_obj uri in
1126 show_in_show_window_obj uri obj
1128 let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1129 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1131 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1133 show_in_show_window_uri (UriManager.uri_of_string uri)
1135 if mmlwidget#get_action <> None then
1136 mmlwidget#action_toggle
1139 mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1141 show_in_show_window_obj, show_in_show_window_uri,
1142 show_in_show_window_callback
1145 exception NoObjectsLocated;;
1147 let user_uri_choice ~title ~msg uris =
1150 [] -> raise NoObjectsLocated
1154 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1159 String.sub uri 4 (String.length uri - 4)
1162 let locate_callback id =
1163 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1164 let result = MQueryGenerator.locate id in
1167 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1170 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1172 output_html outputhtml html ;
1173 user_uri_choice ~title:"Ambiguous input."
1175 ("Ambiguous input \"" ^ id ^
1176 "\". Please, choose one interpetation:")
1181 let input_or_locate_uri ~title =
1182 let uri = ref None in
1185 ~width:400 ~modal:true ~title ~border_width:2 () in
1186 let vbox = GPack.vbox ~packing:window#add () in
1188 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1190 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1192 GEdit.entry ~editable:true
1193 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1195 GButton.button ~label:"Check"
1196 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1197 let _ = checkb#misc#set_sensitive false in
1199 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1201 GMisc.label ~text:"You can also enter an indentifier to locate:"
1202 ~packing:(hbox2#pack ~padding:5) () in
1204 GEdit.entry ~editable:true
1205 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1207 GButton.button ~label:"Locate"
1208 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1209 let _ = locateb#misc#set_sensitive false in
1211 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1213 GButton.button ~label:"Ok"
1214 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1215 let _ = okb#misc#set_sensitive false in
1217 GButton.button ~label:"Cancel"
1218 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1220 ignore (window#connect#destroy GMain.Main.quit) ;
1222 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1223 let check_callback () =
1224 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1225 let uri = "cic:" ^ manual_input#text in
1227 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1228 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1231 Getter.Unresolved ->
1232 output_html outputhtml
1233 ("<h1 color=\"Red\">URI " ^ uri ^
1234 " does not correspond to any object.</h1>") ;
1236 | UriManager.IllFormedUri _ ->
1237 output_html outputhtml
1238 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1241 output_html outputhtml
1242 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1246 (okb#connect#clicked
1248 if check_callback () then
1250 uri := Some manual_input#text ;
1254 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1256 (manual_input#connect#changed
1258 if manual_input#text = "" then
1260 checkb#misc#set_sensitive false ;
1261 okb#misc#set_sensitive false
1265 checkb#misc#set_sensitive true ;
1266 okb#misc#set_sensitive true
1269 (locate_input#connect#changed
1270 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1272 (locateb#connect#clicked
1274 let id = locate_input#text in
1275 manual_input#set_text (locate_callback id) ;
1276 locate_input#delete_text 0 (String.length id)
1279 GMain.Main.main () ;
1281 None -> raise NoChoice
1282 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1285 let locate_one_id id =
1286 let result = MQueryGenerator.locate id in
1290 wrong_xpointer_format_from_wrong_xpointer_format' uri
1292 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1293 output_html (rendering_window ())#outputhtml html ;
1297 [UriManager.string_of_uri
1298 (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1301 interactive_user_uri_choice
1302 ~selection_mode:`EXTENDED
1303 ~ok:"Try every selection."
1304 ~enable_button_for_non_vars:true
1305 ~title:"Ambiguous input."
1307 ("Ambiguous input \"" ^ id ^
1308 "\". Please, choose one or more interpretations:")
1311 List.map cic_textual_parser_uri_of_string uris'
1315 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1316 exception AmbiguousInput;;
1319 Ok of Cic.term * Cic.metasenv
1323 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1324 let known_ids,resolve_id = !id_to_uris in
1330 if List.mem he known_ids then filter tl else he::(filter tl)
1334 (* for each id in dom' we get the list of uris associated to it *)
1335 let list_of_uris = List.map locate_one_id dom' in
1337 List.fold_left (fun i uris -> i * List.length uris) 1 list_of_uris
1339 if tests_no > 1 then
1340 output_html (outputhtml ())
1341 ("<h1>Disambiguation phase started: " ^
1342 string_of_int tests_no ^ " cases will be tried.") ;
1343 (* and now we compute the list of all possible assignments from *)
1344 (* id to uris that generate well-typed terms *)
1346 (* function to test if a partial interpretation is so far correct *)
1347 let test resolve_id residual_dom =
1348 (* We put implicits in place of every identifier that is not *)
1349 (* resolved by resolve_id *)
1353 match resolve_id id with
1355 | Some uri -> Some (CicTextualParser0.Uri uri)
1360 if id = id' then Some (CicTextualParser0.Implicit) else f id'
1361 ) resolve_id' residual_dom
1363 (* and we try to refine the term *)
1364 let saved_status = !CicTextualParser0.metasenv in
1365 let metasenv',expr = mk_metasenv_and_expr resolve_id'' in
1366 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1367 (* The parser is imperative ==> we must restore the old status ;-(( *)
1368 CicTextualParser0.metasenv := saved_status ;
1370 let term,_,_,metasenv'' =
1371 CicRefine.type_of_aux' metasenv' context expr
1373 Ok (term,metasenv'')
1375 CicRefine.MutCaseFixAndCofixRefineNotImplemented ->
1377 let term = CicTypeChecker.type_of_aux' metasenv' context expr in
1381 | CicRefine.Uncertain _ ->
1382 prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
1385 prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ;
1388 let rec aux resolve_id ids list_of_uris =
1389 match ids,list_of_uris with
1391 (match test resolve_id [] with
1392 Ok (term,metasenv) -> [resolve_id,term,metasenv]
1393 | Ko | Uncertain -> [])
1394 | id::idtl,uris::uristl ->
1400 function id' -> if id = id' then Some uri else resolve_id id'
1402 (match test resolve_id' idtl with
1403 Ok (term,metasenv) ->
1404 (* the next three ``if''s are used to avoid the base *)
1405 (* case where the term would be refined a second time. *)
1406 (if uristl = [] then
1407 [resolve_id',term,metasenv]
1409 (aux resolve_id' idtl uristl)
1412 (if uristl = [] then []
1414 (aux resolve_id' idtl uristl)
1421 | _,_ -> assert false
1423 aux resolve_id dom' list_of_uris
1426 (function (resolve,term,newmetasenv) ->
1427 (* If metasen <> newmetasenv is a normal condition, we should *)
1428 (* be prepared to apply the returned substitution to the *)
1429 (* whole current proof. *)
1430 if metasenv <> newmetasenv then
1433 ("+++++ ASSERTION FAILED: " ^
1434 "a refine operation should not modify the metasenv") ;
1435 (* an assert would raise an exception that could be caught *)
1439 let resolve_id',term,metasenv' =
1440 match resolve_ids with
1441 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1442 | [resolve_id] -> resolve_id
1446 (function (resolve,_,_) ->
1450 match resolve id with
1451 None -> assert false
1454 CicTextualParser0.ConUri uri
1455 | CicTextualParser0.VarUri uri ->
1456 UriManager.string_of_uri uri
1457 | CicTextualParser0.IndTyUri (uri,tyno) ->
1458 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1459 string_of_int (tyno+1) ^ ")"
1460 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1461 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1462 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
1466 let index = interactive_interpretation_choice choices in
1467 List.nth resolve_ids index
1469 id_to_uris := known_ids @ dom', resolve_id' ;
1473 (* A WIDGET TO ENTER CIC TERMS *)
1475 class term_editor ?packing ?width ?height ?isnotempty_callback () =
1476 let input = GEdit.text ~editable:true ?width ?height ?packing () in
1478 match isnotempty_callback with
1481 ignore(input#connect#changed (function () -> callback (input#length > 0)))
1484 method coerce = input#coerce
1486 input#delete_text 0 input#length
1487 (* CSC: txt is now a string, but should be of type Cic.term *)
1488 method set_term txt =
1490 ignore ((input#insert_text txt) ~pos:0)
1491 (* CSC: this method should disappear *)
1492 method get_as_string =
1493 input#get_chars 0 input#length
1494 method get_metasenv_and_term ~context ~metasenv =
1498 Some (n,_) -> Some n
1502 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
1503 let dom,mk_metasenv_and_expr =
1504 CicTextualParserContext.main
1505 ~context:name_context ~metasenv CicTextualLexer.token lexbuf
1507 disambiguate_input context metasenv dom mk_metasenv_and_expr
1511 (* OTHER FUNCTIONS *)
1514 let inputt = ((rendering_window ())#inputt : term_editor) in
1515 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1518 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1520 None -> raise NoChoice
1522 let uri = locate_callback input in
1526 output_html outputhtml
1527 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1531 exception UriAlreadyInUse;;
1532 exception NotAUriToAConstant;;
1534 let new_inductive () =
1535 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1536 let output = ((rendering_window ())#output : GMathView.math_view) in
1537 let notebook = (rendering_window ())#notebook in
1539 let chosen = ref false in
1540 let inductive = ref true in
1541 let paramsno = ref 0 in
1542 let get_uri = ref (function _ -> assert false) in
1543 let get_base_uri = ref (function _ -> assert false) in
1544 let get_names = ref (function _ -> assert false) in
1545 let get_types_and_cons = ref (function _ -> assert false) in
1546 let get_context_and_subst = ref (function _ -> assert false) in
1549 ~width:600 ~modal:true ~position:`CENTER
1550 ~title:"New Block of Mutual (Co)Inductive Definitions"
1551 ~border_width:2 () in
1552 let vbox = GPack.vbox ~packing:window#add () in
1554 GPack.hbox ~border_width:0
1555 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1557 GMisc.label ~text:"Enter the URI for the new block:"
1558 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1560 GEdit.entry ~editable:true
1561 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1563 GPack.hbox ~border_width:0
1564 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1568 "Enter the number of left parameters in every arity and constructor type:"
1569 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1570 let paramsno_entry =
1571 GEdit.entry ~editable:true ~text:"0"
1572 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1574 GPack.hbox ~border_width:0
1575 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1577 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1578 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1580 GButton.radio_button ~label:"Inductive"
1581 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1583 GButton.radio_button ~label:"Coinductive"
1584 ~group:inductiveb#group
1585 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1587 GPack.hbox ~border_width:0
1588 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1590 GMisc.label ~text:"Enter the list of the names of the types:"
1591 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1593 GEdit.entry ~editable:true
1594 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1596 GPack.hbox ~border_width:0
1597 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1599 GButton.button ~label:"> Next"
1600 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1601 let _ = okb#misc#set_sensitive true in
1603 GButton.button ~label:"Abort"
1604 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1605 ignore (window#connect#destroy GMain.Main.quit) ;
1606 ignore (cancelb#connect#clicked window#destroy) ;
1610 (okb#connect#clicked
1613 let uristr = "cic:" ^ uri_entry#text in
1614 let namesstr = names_entry#text in
1615 let paramsno' = int_of_string (paramsno_entry#text) in
1616 match Str.split (Str.regexp " +") namesstr with
1618 | (he::tl) as names ->
1619 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1622 ignore (Getter.resolve uri) ;
1623 raise UriAlreadyInUse
1625 Getter.Unresolved ->
1626 get_uri := (function () -> uri) ;
1627 get_names := (function () -> names) ;
1628 inductive := inductiveb#active ;
1629 paramsno := paramsno' ;
1634 output_html outputhtml
1635 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1643 GBin.frame ~label:name
1644 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1645 let vbox = GPack.vbox ~packing:frame#add () in
1646 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1648 GMisc.label ~text:("Enter its type:")
1649 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1650 let scrolled_window =
1651 GBin.scrolled_window ~border_width:5
1652 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1654 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1655 ~isnotempty_callback:
1657 (*non_empty_type := b ;*)
1658 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1661 GPack.hbox ~border_width:0
1662 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1664 GMisc.label ~text:("Enter the list of its constructors:")
1665 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1666 let cons_names_entry =
1667 GEdit.entry ~editable:true
1668 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1669 (newinputt,cons_names_entry)
1672 vbox#remove hboxn#coerce ;
1674 GPack.hbox ~border_width:0
1675 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1677 GButton.button ~label:"> Next"
1678 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1680 GButton.button ~label:"Abort"
1681 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1682 ignore (cancelb#connect#clicked window#destroy) ;
1684 (okb#connect#clicked
1687 let names = !get_names () in
1688 let types_and_cons =
1690 (fun name (newinputt,cons_names_entry) ->
1691 let consnamesstr = cons_names_entry#text in
1692 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1694 newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1697 [] -> expr,cons_names
1698 | _ -> raise AmbiguousInput
1699 ) names type_widgets
1701 let uri = !get_uri () in
1703 (* Let's see if so far the definition is well-typed *)
1706 (* To test if the arities of the inductive types are well *)
1707 (* typed, we check the inductive block definition where *)
1708 (* no constructor is given to each type. *)
1711 (fun name (ty,cons) -> (name, !inductive, ty, []))
1712 names types_and_cons
1714 CicTypeChecker.typecheck_mutual_inductive_defs uri
1715 (tys,params,paramsno)
1717 get_context_and_subst :=
1721 (fun (context,subst) name (ty,_) ->
1723 (Some (Cic.Name name, Cic.Decl ty))::context,
1724 (Cic.MutInd (uri,!i,[]))::subst
1727 ) ([],[]) names types_and_cons) ;
1728 let types_and_cons' =
1730 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1731 names types_and_cons
1733 get_types_and_cons := (function () -> types_and_cons') ;
1738 output_html outputhtml
1739 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1742 and phase3 name cons =
1743 let get_cons_types = ref (function () -> assert false) in
1746 ~width:600 ~modal:true ~position:`CENTER
1747 ~title:(name ^ " Constructors")
1748 ~border_width:2 () in
1749 let vbox = GPack.vbox ~packing:window2#add () in
1750 let cons_type_widgets =
1752 (function consname ->
1754 GPack.hbox ~border_width:0
1755 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1757 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1758 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1759 let scrolled_window =
1760 GBin.scrolled_window ~border_width:5
1761 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1763 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1764 ~isnotempty_callback:
1766 (* (*non_empty_type := b ;*)
1767 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1772 GPack.hbox ~border_width:0
1773 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1775 GButton.button ~label:"> Next"
1776 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1777 let _ = okb#misc#set_sensitive true in
1779 GButton.button ~label:"Abort"
1780 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1781 ignore (window2#connect#destroy GMain.Main.quit) ;
1782 ignore (cancelb#connect#clicked window2#destroy) ;
1784 (okb#connect#clicked
1788 let context,subst= !get_context_and_subst () in
1793 inputt#get_metasenv_and_term ~context ~metasenv:[]
1797 let undebrujined_expr =
1799 (fun expr t -> CicSubstitution.subst t expr) expr subst
1801 name, undebrujined_expr
1802 | _ -> raise AmbiguousInput
1803 ) cons cons_type_widgets
1805 get_cons_types := (function () -> cons_types) ;
1809 output_html outputhtml
1810 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1813 GMain.Main.main () ;
1814 let okb_pressed = !chosen in
1816 if (not okb_pressed) then
1819 assert false (* The control never reaches this point *)
1822 (!get_cons_types ())
1825 (* No more phases left or Abort pressed *)
1827 GMain.Main.main () ;
1831 let uri = !get_uri () in
1834 let tys = !get_types_and_cons () in
1835 let obj = Cic.InductiveDefinition tys params !paramsno in
1838 prerr_endline (CicPp.ppobj obj) ;
1839 CicTypeChecker.typecheck_mutual_inductive_defs uri
1840 (tys,params,!paramsno) ;
1843 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1844 prerr_endline (CicPp.ppobj obj) ;
1846 (* We already know that obj is well-typed. We need to add it to the *)
1847 (* environment in order to compute the inner-types without having to *)
1848 (* debrujin it or having to modify lots of other functions to avoid *)
1849 (* asking the environment for the MUTINDs we are defining now. *)
1850 CicEnvironment.put_inductive_definition uri obj ;
1852 show_in_show_window_obj uri obj
1855 output_html outputhtml
1856 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1860 let inputt = ((rendering_window ())#inputt : term_editor) in
1861 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1862 let output = ((rendering_window ())#output : GMathView.math_view) in
1863 let notebook = (rendering_window ())#notebook in
1865 let chosen = ref false in
1866 let get_metasenv_and_term = ref (function _ -> assert false) in
1867 let get_uri = ref (function _ -> assert false) in
1868 let non_empty_type = ref false in
1871 ~width:600 ~modal:true ~title:"New Proof or Definition"
1872 ~border_width:2 () in
1873 let vbox = GPack.vbox ~packing:window#add () in
1875 GPack.hbox ~border_width:0
1876 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1878 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1879 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1881 GEdit.entry ~editable:true
1882 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1884 GPack.hbox ~border_width:0
1885 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1887 GMisc.label ~text:"Enter the theorem or definition type:"
1888 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1889 let scrolled_window =
1890 GBin.scrolled_window ~border_width:5
1891 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1892 (* the content of the scrolled_window is moved below (see comment) *)
1894 GPack.hbox ~border_width:0
1895 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1897 GButton.button ~label:"Ok"
1898 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1899 let _ = okb#misc#set_sensitive false in
1901 GButton.button ~label:"Cancel"
1902 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1903 (* moved here to have visibility of the ok button *)
1905 new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1906 ~isnotempty_callback:
1908 non_empty_type := b ;
1909 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1912 newinputt#set_term inputt#get_as_string ;
1915 uri_entry#connect#changed
1917 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1919 ignore (window#connect#destroy GMain.Main.quit) ;
1920 ignore (cancelb#connect#clicked window#destroy) ;
1922 (okb#connect#clicked
1926 let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1927 let uristr = "cic:" ^ uri_entry#text in
1928 let uri = UriManager.uri_of_string uristr in
1929 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1930 raise NotAUriToAConstant
1934 ignore (Getter.resolve uri) ;
1935 raise UriAlreadyInUse
1937 Getter.Unresolved ->
1938 get_metasenv_and_term := (function () -> metasenv,parsed) ;
1939 get_uri := (function () -> uri) ;
1944 output_html outputhtml
1945 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1948 GMain.Main.main () ;
1951 let metasenv,expr = !get_metasenv_and_term () in
1952 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1953 ProofEngine.proof :=
1954 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1955 ProofEngine.goal := Some 1 ;
1956 refresh_sequent notebook ;
1957 refresh_proof output ;
1958 !save_set_sensitive true ;
1961 RefreshSequentException e ->
1962 output_html outputhtml
1963 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1964 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1965 | RefreshProofException e ->
1966 output_html outputhtml
1967 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1968 "proof: " ^ Printexc.to_string e ^ "</h1>")
1970 output_html outputhtml
1971 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1974 let check_term_in_scratch scratch_window metasenv context expr =
1976 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1977 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1978 scratch_window#show () ;
1979 scratch_window#mmlwidget#load_tree ~dom:mml
1982 print_endline ("? " ^ CicPp.ppterm expr) ;
1986 let check scratch_window () =
1987 let inputt = ((rendering_window ())#inputt : term_editor) in
1988 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1990 match !ProofEngine.proof with
1992 | Some (_,metasenv,_,_) -> metasenv
1995 match !ProofEngine.goal with
1998 let (_,canonical_context,_) =
1999 List.find (function (m,_,_) -> m=metano) metasenv
2004 let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
2005 check_term_in_scratch scratch_window metasenv' context expr
2008 output_html outputhtml
2009 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2013 (***********************)
2015 (***********************)
2017 let call_tactic tactic () =
2018 let notebook = (rendering_window ())#notebook in
2019 let output = ((rendering_window ())#output : GMathView.math_view) in
2020 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2021 let savedproof = !ProofEngine.proof in
2022 let savedgoal = !ProofEngine.goal in
2026 refresh_sequent notebook ;
2027 refresh_proof output
2029 RefreshSequentException e ->
2030 output_html outputhtml
2031 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2032 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2033 ProofEngine.proof := savedproof ;
2034 ProofEngine.goal := savedgoal ;
2035 refresh_sequent notebook
2036 | RefreshProofException e ->
2037 output_html outputhtml
2038 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2039 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2040 ProofEngine.proof := savedproof ;
2041 ProofEngine.goal := savedgoal ;
2042 refresh_sequent notebook ;
2043 refresh_proof output
2045 output_html outputhtml
2046 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2047 ProofEngine.proof := savedproof ;
2048 ProofEngine.goal := savedgoal ;
2052 let call_tactic_with_input tactic () =
2053 let notebook = (rendering_window ())#notebook in
2054 let output = ((rendering_window ())#output : GMathView.math_view) in
2055 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2056 let inputt = ((rendering_window ())#inputt : term_editor) in
2057 let savedproof = !ProofEngine.proof in
2058 let savedgoal = !ProofEngine.goal in
2059 let uri,metasenv,bo,ty =
2060 match !ProofEngine.proof with
2061 None -> assert false
2062 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2064 let canonical_context =
2065 match !ProofEngine.goal with
2066 None -> assert false
2068 let (_,canonical_context,_) =
2069 List.find (function (m,_,_) -> m=metano) metasenv
2074 let metasenv',expr =
2075 inputt#get_metasenv_and_term canonical_context metasenv
2077 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2079 refresh_sequent notebook ;
2080 refresh_proof output ;
2083 RefreshSequentException e ->
2084 output_html outputhtml
2085 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2086 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2087 ProofEngine.proof := savedproof ;
2088 ProofEngine.goal := savedgoal ;
2089 refresh_sequent notebook
2090 | RefreshProofException e ->
2091 output_html outputhtml
2092 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2093 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2094 ProofEngine.proof := savedproof ;
2095 ProofEngine.goal := savedgoal ;
2096 refresh_sequent notebook ;
2097 refresh_proof output
2099 output_html outputhtml
2100 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2101 ProofEngine.proof := savedproof ;
2102 ProofEngine.goal := savedgoal ;
2105 let call_tactic_with_goal_input tactic () =
2106 let module L = LogicalOperations in
2107 let module G = Gdome in
2108 let notebook = (rendering_window ())#notebook in
2109 let output = ((rendering_window ())#output : GMathView.math_view) in
2110 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2111 let savedproof = !ProofEngine.proof in
2112 let savedgoal = !ProofEngine.goal in
2113 match notebook#proofw#get_selection with
2116 ((node : Gdome.element)#getAttributeNS
2117 ~namespaceURI:helmns
2118 ~localName:(G.domString "xref"))#to_string
2120 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2124 match !current_goal_infos with
2125 Some (ids_to_terms, ids_to_father_ids,_) ->
2127 tactic (Hashtbl.find ids_to_terms id) ;
2128 refresh_sequent notebook ;
2129 refresh_proof output
2130 | None -> assert false (* "ERROR: No current term!!!" *)
2132 RefreshSequentException e ->
2133 output_html outputhtml
2134 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2135 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2136 ProofEngine.proof := savedproof ;
2137 ProofEngine.goal := savedgoal ;
2138 refresh_sequent notebook
2139 | RefreshProofException e ->
2140 output_html outputhtml
2141 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2142 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2143 ProofEngine.proof := savedproof ;
2144 ProofEngine.goal := savedgoal ;
2145 refresh_sequent notebook ;
2146 refresh_proof output
2148 output_html outputhtml
2149 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2150 ProofEngine.proof := savedproof ;
2151 ProofEngine.goal := savedgoal ;
2154 output_html outputhtml
2155 ("<h1 color=\"red\">No term selected</h1>")
2158 let call_tactic_with_input_and_goal_input tactic () =
2159 let module L = LogicalOperations in
2160 let module G = Gdome in
2161 let notebook = (rendering_window ())#notebook in
2162 let output = ((rendering_window ())#output : GMathView.math_view) in
2163 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2164 let inputt = ((rendering_window ())#inputt : term_editor) in
2165 let savedproof = !ProofEngine.proof in
2166 let savedgoal = !ProofEngine.goal in
2167 match notebook#proofw#get_selection with
2170 ((node : Gdome.element)#getAttributeNS
2171 ~namespaceURI:helmns
2172 ~localName:(G.domString "xref"))#to_string
2174 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2178 match !current_goal_infos with
2179 Some (ids_to_terms, ids_to_father_ids,_) ->
2181 let uri,metasenv,bo,ty =
2182 match !ProofEngine.proof with
2183 None -> assert false
2184 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2186 let canonical_context =
2187 match !ProofEngine.goal with
2188 None -> assert false
2190 let (_,canonical_context,_) =
2191 List.find (function (m,_,_) -> m=metano) metasenv
2193 canonical_context in
2194 let (metasenv',expr) =
2195 inputt#get_metasenv_and_term canonical_context metasenv
2197 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2198 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2200 refresh_sequent notebook ;
2201 refresh_proof output ;
2203 | None -> assert false (* "ERROR: No current term!!!" *)
2205 RefreshSequentException e ->
2206 output_html outputhtml
2207 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2208 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2209 ProofEngine.proof := savedproof ;
2210 ProofEngine.goal := savedgoal ;
2211 refresh_sequent notebook
2212 | RefreshProofException e ->
2213 output_html outputhtml
2214 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2215 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2216 ProofEngine.proof := savedproof ;
2217 ProofEngine.goal := savedgoal ;
2218 refresh_sequent notebook ;
2219 refresh_proof output
2221 output_html outputhtml
2222 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2223 ProofEngine.proof := savedproof ;
2224 ProofEngine.goal := savedgoal ;
2227 output_html outputhtml
2228 ("<h1 color=\"red\">No term selected</h1>")
2231 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2232 let module L = LogicalOperations in
2233 let module G = Gdome in
2234 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2235 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2236 let savedproof = !ProofEngine.proof in
2237 let savedgoal = !ProofEngine.goal in
2238 match mmlwidget#get_selection with
2241 ((node : Gdome.element)#getAttributeNS
2242 ~namespaceURI:helmns
2243 ~localName:(G.domString "xref"))#to_string
2245 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2249 match !current_scratch_infos with
2250 (* term is the whole goal in the scratch_area *)
2251 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2253 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2254 let mml = mml_of_cic_term 111 expr in
2255 scratch_window#show () ;
2256 scratch_window#mmlwidget#load_tree ~dom:mml
2257 | None -> assert false (* "ERROR: No current term!!!" *)
2260 output_html outputhtml
2261 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2264 output_html outputhtml
2265 ("<h1 color=\"red\">No term selected</h1>")
2268 let call_tactic_with_hypothesis_input tactic () =
2269 let module L = LogicalOperations in
2270 let module G = Gdome in
2271 let notebook = (rendering_window ())#notebook in
2272 let output = ((rendering_window ())#output : GMathView.math_view) in
2273 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2274 let savedproof = !ProofEngine.proof in
2275 let savedgoal = !ProofEngine.goal in
2276 match notebook#proofw#get_selection with
2279 ((node : Gdome.element)#getAttributeNS
2280 ~namespaceURI:helmns
2281 ~localName:(G.domString "xref"))#to_string
2283 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2287 match !current_goal_infos with
2288 Some (_,_,ids_to_hypotheses) ->
2290 tactic (Hashtbl.find ids_to_hypotheses id) ;
2291 refresh_sequent notebook ;
2292 refresh_proof output
2293 | None -> assert false (* "ERROR: No current term!!!" *)
2295 RefreshSequentException e ->
2296 output_html outputhtml
2297 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2298 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2299 ProofEngine.proof := savedproof ;
2300 ProofEngine.goal := savedgoal ;
2301 refresh_sequent notebook
2302 | RefreshProofException e ->
2303 output_html outputhtml
2304 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2305 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2306 ProofEngine.proof := savedproof ;
2307 ProofEngine.goal := savedgoal ;
2308 refresh_sequent notebook ;
2309 refresh_proof output
2311 output_html outputhtml
2312 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2313 ProofEngine.proof := savedproof ;
2314 ProofEngine.goal := savedgoal ;
2317 output_html outputhtml
2318 ("<h1 color=\"red\">No term selected</h1>")
2322 let intros = call_tactic ProofEngine.intros;;
2323 let exact = call_tactic_with_input ProofEngine.exact;;
2324 let apply = call_tactic_with_input ProofEngine.apply;;
2325 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2326 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2327 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2328 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2329 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2330 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2331 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2332 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2333 let cut = call_tactic_with_input ProofEngine.cut;;
2334 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2335 let letin = call_tactic_with_input ProofEngine.letin;;
2336 let ring = call_tactic ProofEngine.ring;;
2337 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2338 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2339 let fourier = call_tactic ProofEngine.fourier;;
2340 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2341 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2342 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2343 let reflexivity = call_tactic ProofEngine.reflexivity;;
2344 let symmetry = call_tactic ProofEngine.symmetry;;
2345 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2346 let exists = call_tactic ProofEngine.exists;;
2347 let split = call_tactic ProofEngine.split;;
2348 let left = call_tactic ProofEngine.left;;
2349 let right = call_tactic ProofEngine.right;;
2350 let assumption = call_tactic ProofEngine.assumption;;
2351 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2352 let absurd = call_tactic_with_input ProofEngine.absurd;;
2353 let contradiction = call_tactic ProofEngine.contradiction;;
2354 (* Galla chiede: come dare alla tattica la lista di termini da decomporre?
2355 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
2358 let whd_in_scratch scratch_window =
2359 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2362 let reduce_in_scratch scratch_window =
2363 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2366 let simpl_in_scratch scratch_window =
2367 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2373 (**********************)
2374 (* END OF TACTICS *)
2375 (**********************)
2379 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2381 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2384 output_html outputhtml
2385 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2388 exception NotADefinition;;
2391 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2392 let output = ((rendering_window ())#output : GMathView.math_view) in
2393 let notebook = (rendering_window ())#notebook in
2395 let uri = input_or_locate_uri ~title:"Open" in
2396 CicTypeChecker.typecheck uri ;
2397 let metasenv,bo,ty =
2398 match CicEnvironment.get_cooked_obj uri with
2399 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2400 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2403 | Cic.InductiveDefinition _ -> raise NotADefinition
2405 ProofEngine.proof :=
2406 Some (uri, metasenv, bo, ty) ;
2407 ProofEngine.goal := None ;
2408 refresh_sequent notebook ;
2409 refresh_proof output
2411 RefreshSequentException e ->
2412 output_html outputhtml
2413 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2414 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2415 | RefreshProofException e ->
2416 output_html outputhtml
2417 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2418 "proof: " ^ Printexc.to_string e ^ "</h1>")
2420 output_html outputhtml
2421 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2424 let show_query_results results =
2427 ~modal:false ~title:"Query results." ~border_width:2 () in
2428 let vbox = GPack.vbox ~packing:window#add () in
2430 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2433 ~text:"Click on a URI to show that object"
2434 ~packing:hbox#add () in
2435 let scrolled_window =
2436 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2437 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2438 let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2441 (function (uri,_) ->
2445 clist#set_row ~selectable:false n
2448 clist#columns_autosize () ;
2450 (clist#connect#select_row
2451 (fun ~row ~column ~event ->
2452 let (uristr,_) = List.nth results row in
2454 cic_textual_parser_uri_of_string
2455 (wrong_xpointer_format_from_wrong_xpointer_format' uristr)
2457 CicTextualParser0.ConUri uri
2458 | CicTextualParser0.VarUri uri
2459 | CicTextualParser0.IndTyUri (uri,_)
2460 | CicTextualParser0.IndConUri (uri,_,_) ->
2461 show_in_show_window_uri uri
2467 let refine_constraints (must_obj,must_rel,must_sort) =
2468 let chosen = ref false in
2469 let use_only = ref false in
2472 ~modal:true ~title:"Constraints refinement."
2473 ~width:800 ~border_width:2 () in
2474 let vbox = GPack.vbox ~packing:window#add () in
2476 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2479 ~text: "\"Only\" constraints can be enforced or not."
2480 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2482 GButton.toggle_button ~label:"Enforce \"only\" constraints"
2483 ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2486 (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2487 (* Notebook for the constraints choice *)
2489 GPack.notebook ~scrollable:true
2490 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2491 (* Rel constraints *)
2494 ~text: "Constraints on Rels" () in
2496 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2499 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2502 ~text: "You can now specify the constraints on Rels."
2503 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2504 let expected_height = 25 * (List.length must_rel + 2) in
2505 let height = if expected_height > 400 then 400 else expected_height in
2506 let scrolled_window =
2507 GBin.scrolled_window ~border_width:10 ~height ~width:600
2508 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2509 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2510 let rel_constraints =
2512 (function (position,depth) ->
2515 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2519 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2521 None -> position, ref None
2523 let mutable_ref = ref (Some depth') in
2525 GButton.toggle_button
2526 ~label:("depth = " ^ string_of_int depth') ~active:true
2527 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2530 (depthb#connect#toggled
2532 let sel_depth = if depthb#active then Some depth' else None in
2533 mutable_ref := sel_depth
2535 position, mutable_ref
2537 (* Sort constraints *)
2540 ~text: "Constraints on Sorts" () in
2542 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2545 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2548 ~text: "You can now specify the constraints on Sorts."
2549 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2550 let expected_height = 25 * (List.length must_sort + 2) in
2551 let height = if expected_height > 400 then 400 else expected_height in
2552 let scrolled_window =
2553 GBin.scrolled_window ~border_width:10 ~height ~width:600
2554 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2555 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2556 let sort_constraints =
2558 (function (position,depth,sort) ->
2561 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2564 ~text:(sort ^ " " ^ position)
2565 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2567 None -> position, ref None, sort
2569 let mutable_ref = ref (Some depth') in
2571 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2573 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2576 (depthb#connect#toggled
2578 let sel_depth = if depthb#active then Some depth' else None in
2579 mutable_ref := sel_depth
2581 position, mutable_ref, sort
2583 (* Obj constraints *)
2586 ~text: "Constraints on constants" () in
2588 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2591 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2594 ~text: "You can now specify the constraints on constants."
2595 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2596 let expected_height = 25 * (List.length must_obj + 2) in
2597 let height = if expected_height > 400 then 400 else expected_height in
2598 let scrolled_window =
2599 GBin.scrolled_window ~border_width:10 ~height ~width:600
2600 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2601 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2602 let obj_constraints =
2604 (function (uri,position,depth) ->
2607 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2610 ~text:(uri ^ " " ^ position)
2611 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2613 None -> uri, position, ref None
2615 let mutable_ref = ref (Some depth') in
2617 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2619 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2622 (depthb#connect#toggled
2624 let sel_depth = if depthb#active then Some depth' else None in
2625 mutable_ref := sel_depth
2627 uri, position, mutable_ref
2629 (* Confirm/abort buttons *)
2631 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2633 GButton.button ~label:"Ok"
2634 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2636 GButton.button ~label:"Abort"
2637 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2639 ignore (window#connect#destroy GMain.Main.quit) ;
2640 ignore (cancelb#connect#clicked window#destroy) ;
2642 (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2643 window#set_position `CENTER ;
2645 GMain.Main.main () ;
2647 let chosen_must_rel =
2649 (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2650 let chosen_must_sort =
2652 (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2655 let chosen_must_obj =
2657 (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2660 (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2662 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2663 Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2671 let completeSearchPattern () =
2672 let inputt = ((rendering_window ())#inputt : term_editor) in
2673 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2675 let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2676 let must = MQueryLevels2.get_constraints expr in
2677 let must',only = refine_constraints must in
2678 let results = MQueryGenerator.searchPattern must' only in
2679 show_query_results results
2682 output_html outputhtml
2683 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2686 let insertQuery () =
2687 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2689 let chosen = ref None in
2692 ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2693 let vbox = GPack.vbox ~packing:window#add () in
2695 GMisc.label ~text:"Insert Query. For Experts Only."
2696 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2697 let scrolled_window =
2698 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2699 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2700 let input = GEdit.text ~editable:true
2701 ~packing:scrolled_window#add () in
2703 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2705 GButton.button ~label:"Ok"
2706 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2708 GButton.button ~label:"Load from file..."
2709 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2711 GButton.button ~label:"Abort"
2712 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2713 ignore (window#connect#destroy GMain.Main.quit) ;
2714 ignore (cancelb#connect#clicked window#destroy) ;
2716 (okb#connect#clicked
2718 chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2720 (loadb#connect#clicked
2723 GToolbox.select_file ~title:"Select Query File" ()
2727 let inch = open_in filename in
2728 let rec read_file () =
2730 let line = input_line inch in
2731 line ^ "\n" ^ read_file ()
2735 let text = read_file () in
2736 input#delete_text 0 input#length ;
2737 ignore (input#insert_text text ~pos:0))) ;
2738 window#set_position `CENTER ;
2740 GMain.Main.main () ;
2745 Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2747 show_query_results results
2750 output_html outputhtml
2751 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2754 let choose_must list_of_must only =
2755 let chosen = ref None in
2756 let user_constraints = ref [] in
2759 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2760 let vbox = GPack.vbox ~packing:window#add () in
2762 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2766 ("You can now specify the genericity of the query. " ^
2767 "The more generic the slower.")
2768 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2770 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2774 "Suggestion: start with faster queries before moving to more generic ones."
2775 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2777 GPack.notebook ~scrollable:true
2778 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2781 let last = List.length list_of_must in
2787 (if !page = 1 then "More generic" else
2788 if !page = last then "More precise" else " ") () in
2789 let expected_height = 25 * (List.length must + 2) in
2790 let height = if expected_height > 400 then 400 else expected_height in
2791 let scrolled_window =
2792 GBin.scrolled_window ~border_width:10 ~height ~width:600
2793 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2795 GList.clist ~columns:2 ~packing:scrolled_window#add
2796 ~titles:["URI" ; "Position"] ()
2800 (function (uri,position) ->
2803 [uri; if position then "MainConclusion" else "Conclusion"]
2805 clist#set_row ~selectable:false n
2808 clist#columns_autosize ()
2811 let label = GMisc.label ~text:"User provided" () in
2813 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2815 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2818 ~text:"Select the constraints that must be satisfied and press OK."
2819 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2820 let expected_height = 25 * (List.length only + 2) in
2821 let height = if expected_height > 400 then 400 else expected_height in
2822 let scrolled_window =
2823 GBin.scrolled_window ~border_width:10 ~height ~width:600
2824 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2826 GList.clist ~columns:2 ~packing:scrolled_window#add
2827 ~selection_mode:`EXTENDED
2828 ~titles:["URI" ; "Position"] ()
2832 (function (uri,position) ->
2835 [uri; if position then "MainConclusion" else "Conclusion"]
2837 clist#set_row ~selectable:true n
2840 clist#columns_autosize () ;
2842 (clist#connect#select_row
2843 (fun ~row ~column ~event ->
2844 user_constraints := (List.nth only row)::!user_constraints)) ;
2846 (clist#connect#unselect_row
2847 (fun ~row ~column ~event ->
2850 (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2853 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2855 GButton.button ~label:"Ok"
2856 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2858 GButton.button ~label:"Abort"
2859 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2861 ignore (window#connect#destroy GMain.Main.quit) ;
2862 ignore (cancelb#connect#clicked window#destroy) ;
2864 (okb#connect#clicked
2865 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2866 window#set_position `CENTER ;
2868 GMain.Main.main () ;
2870 None -> raise NoChoice
2872 if n = List.length list_of_must then
2873 (* user provided constraints *)
2876 List.nth list_of_must n
2879 let searchPattern () =
2880 let inputt = ((rendering_window ())#inputt : term_editor) in
2881 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2884 match !ProofEngine.proof with
2885 None -> assert false
2886 | Some (_,metasenv,_,_) -> metasenv
2888 match !ProofEngine.goal with
2891 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2892 let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2893 let must = choose_must list_of_must only in
2894 let torigth_restriction (u,b) =
2897 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2899 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2903 let rigth_must = List.map torigth_restriction must in
2904 let rigth_only = Some (List.map torigth_restriction only) in
2906 MQueryGenerator.searchPattern
2907 (rigth_must,[],[]) (rigth_only,None,None) in
2911 wrong_xpointer_format_from_wrong_xpointer_format' uri
2914 " <h1>Backward Query: </h1>" ^
2915 " <pre>" ^ get_last_query result ^ "</pre>"
2917 output_html outputhtml html ;
2919 let rec filter_out =
2923 let tl',exc = filter_out tl in
2926 ProofEngine.can_apply
2927 (term_of_cic_textual_parser_uri
2928 (cic_textual_parser_uri_of_string uri))
2936 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2937 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2944 " <h1>Objects that can actually be applied: </h1> " ^
2945 String.concat "<br>" uris' ^ exc ^
2946 " <h1>Number of false matches: " ^
2947 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2948 " <h1>Number of good matches: " ^
2949 string_of_int (List.length uris') ^ "</h1>"
2951 output_html outputhtml html' ;
2953 user_uri_choice ~title:"Ambiguous input."
2955 "Many lemmas can be successfully applied. Please, choose one:"
2958 inputt#set_term uri' ;
2962 output_html outputhtml
2963 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2966 let choose_selection
2967 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2969 let module G = Gdome in
2970 let rec aux element =
2971 if element#hasAttributeNS
2972 ~namespaceURI:helmns
2973 ~localName:(G.domString "xref")
2975 mmlwidget#set_selection (Some element)
2977 match element#get_parentNode with
2978 None -> assert false
2979 (*CSC: OCAML DIVERGES!
2980 | Some p -> aux (new G.element_of_node p)
2982 | Some p -> aux (new Gdome.element_of_node p)
2986 | None -> mmlwidget#set_selection None
2989 (* STUFF TO BUILD THE GTK INTERFACE *)
2991 (* Stuff for the widget settings *)
2993 let export_to_postscript (output : GMathView.math_view) =
2994 let lastdir = ref (Unix.getcwd ()) in
2997 GToolbox.select_file ~title:"Export to PostScript"
2998 ~dir:lastdir ~filename:"screenshot.ps" ()
3002 output#export_to_postscript ~filename:filename ();
3005 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
3006 button_set_kerning button_set_transparency export_to_postscript_menu_item
3009 let is_set = button_t1#active in
3010 output#set_font_manager_type
3011 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
3014 button_set_anti_aliasing#misc#set_sensitive true ;
3015 button_set_kerning#misc#set_sensitive true ;
3016 button_set_transparency#misc#set_sensitive true ;
3017 export_to_postscript_menu_item#misc#set_sensitive true ;
3021 button_set_anti_aliasing#misc#set_sensitive false ;
3022 button_set_kerning#misc#set_sensitive false ;
3023 button_set_transparency#misc#set_sensitive false ;
3024 export_to_postscript_menu_item#misc#set_sensitive false ;
3028 let set_anti_aliasing output button_set_anti_aliasing () =
3029 output#set_anti_aliasing button_set_anti_aliasing#active
3032 let set_kerning output button_set_kerning () =
3033 output#set_kerning button_set_kerning#active
3036 let set_transparency output button_set_transparency () =
3037 output#set_transparency button_set_transparency#active
3040 let changefont output font_size_spinb () =
3041 output#set_font_size font_size_spinb#value_as_int
3044 let set_log_verbosity output log_verbosity_spinb () =
3045 output#set_log_verbosity log_verbosity_spinb#value_as_int
3048 class settings_window (output : GMathView.math_view) sw
3049 export_to_postscript_menu_item selection_changed_callback
3051 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
3053 GPack.vbox ~packing:settings_window#add () in
3056 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3057 ~border_width:5 ~packing:vbox#add () in
3059 GButton.toggle_button ~label:"activate t1 fonts"
3060 ~packing:(table#attach ~left:0 ~top:0) () in
3061 let button_set_anti_aliasing =
3062 GButton.toggle_button ~label:"set_anti_aliasing"
3063 ~packing:(table#attach ~left:0 ~top:1) () in
3064 let button_set_kerning =
3065 GButton.toggle_button ~label:"set_kerning"
3066 ~packing:(table#attach ~left:1 ~top:1) () in
3067 let button_set_transparency =
3068 GButton.toggle_button ~label:"set_transparency"
3069 ~packing:(table#attach ~left:2 ~top:1) () in
3072 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
3073 ~border_width:5 ~packing:vbox#add () in
3074 let font_size_label =
3075 GMisc.label ~text:"font size:"
3076 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
3077 let font_size_spinb =
3079 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
3082 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
3083 let log_verbosity_label =
3084 GMisc.label ~text:"log verbosity:"
3085 ~packing:(table#attach ~left:0 ~top:1) () in
3086 let log_verbosity_spinb =
3088 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
3091 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
3093 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3095 GButton.button ~label:"Close"
3096 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3098 method show = settings_window#show
3100 button_set_anti_aliasing#misc#set_sensitive false ;
3101 button_set_kerning#misc#set_sensitive false ;
3102 button_set_transparency#misc#set_sensitive false ;
3103 (* Signals connection *)
3104 ignore(button_t1#connect#clicked
3105 (activate_t1 output button_set_anti_aliasing button_set_kerning
3106 button_set_transparency export_to_postscript_menu_item button_t1)) ;
3107 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
3108 ignore(button_set_anti_aliasing#connect#toggled
3109 (set_anti_aliasing output button_set_anti_aliasing));
3110 ignore(button_set_kerning#connect#toggled
3111 (set_kerning output button_set_kerning)) ;
3112 ignore(button_set_transparency#connect#toggled
3113 (set_transparency output button_set_transparency)) ;
3114 ignore(log_verbosity_spinb#connect#changed
3115 (set_log_verbosity output log_verbosity_spinb)) ;
3116 ignore(closeb#connect#clicked settings_window#misc#hide)
3119 (* Scratch window *)
3121 class scratch_window =
3123 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
3125 GPack.vbox ~packing:window#add () in
3127 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3129 GButton.button ~label:"Whd"
3130 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3132 GButton.button ~label:"Reduce"
3133 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3135 GButton.button ~label:"Simpl"
3136 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3137 let scrolled_window =
3138 GBin.scrolled_window ~border_width:10
3139 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3142 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
3144 method mmlwidget = mmlwidget
3145 method show () = window#misc#hide () ; window#show ()
3147 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
3148 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
3149 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
3150 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
3151 ignore(simplb#connect#clicked (simpl_in_scratch self))
3155 let vbox1 = GPack.vbox () in
3157 val mutable proofw_ref = None
3158 val mutable compute_ref = None
3160 Lazy.force self#compute ;
3161 match proofw_ref with
3162 None -> assert false
3163 | Some proofw -> proofw
3164 method content = vbox1
3166 match compute_ref with
3167 None -> assert false
3168 | Some compute -> compute
3172 let scrolled_window1 =
3173 GBin.scrolled_window ~border_width:10
3174 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3176 GMathView.math_view ~width:400 ~height:275
3177 ~packing:(scrolled_window1#add) () in
3178 let _ = proofw_ref <- Some proofw in
3180 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3182 GButton.button ~label:"Exact"
3183 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3185 GButton.button ~label:"Intros"
3186 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3188 GButton.button ~label:"Apply"
3189 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3190 let elimintrossimplb =
3191 GButton.button ~label:"ElimIntrosSimpl"
3192 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3194 GButton.button ~label:"ElimType"
3195 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3197 GButton.button ~label:"Whd"
3198 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3200 GButton.button ~label:"Reduce"
3201 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3203 GButton.button ~label:"Simpl"
3204 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3206 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3208 GButton.button ~label:"Fold_whd"
3209 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3211 GButton.button ~label:"Fold_reduce"
3212 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3214 GButton.button ~label:"Fold_simpl"
3215 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3217 GButton.button ~label:"Cut"
3218 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3220 GButton.button ~label:"Change"
3221 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3223 GButton.button ~label:"Let ... In"
3224 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3226 GButton.button ~label:"Ring"
3227 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3229 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3231 GButton.button ~label:"ClearBody"
3232 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3234 GButton.button ~label:"Clear"
3235 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3237 GButton.button ~label:"Fourier"
3238 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3240 GButton.button ~label:"RewriteSimpl ->"
3241 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3242 let rewritebacksimplb =
3243 GButton.button ~label:"RewriteSimpl <-"
3244 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3246 GButton.button ~label:"Replace"
3247 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3249 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3251 GButton.button ~label:"Reflexivity"
3252 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3254 GButton.button ~label:"Symmetry"
3255 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3257 GButton.button ~label:"Transitivity"
3258 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3260 GButton.button ~label:"Exists"
3261 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3263 GButton.button ~label:"Split"
3264 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3266 GButton.button ~label:"Left"
3267 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3269 GButton.button ~label:"Right"
3270 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3272 GButton.button ~label:"Assumption"
3273 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3275 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3277 GButton.button ~label:"Generalize"
3278 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3280 GButton.button ~label:"Absurd"
3281 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3282 let contradictionb =
3283 GButton.button ~label:"Contradiction"
3284 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3285 let searchpatternb =
3286 GButton.button ~label:"SearchPattern_Apply"
3287 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3289 ignore(exactb#connect#clicked exact) ;
3290 ignore(applyb#connect#clicked apply) ;
3291 ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3292 ignore(elimtypeb#connect#clicked elimtype) ;
3293 ignore(whdb#connect#clicked whd) ;
3294 ignore(reduceb#connect#clicked reduce) ;
3295 ignore(simplb#connect#clicked simpl) ;
3296 ignore(foldwhdb#connect#clicked fold_whd) ;
3297 ignore(foldreduceb#connect#clicked fold_reduce) ;
3298 ignore(foldsimplb#connect#clicked fold_simpl) ;
3299 ignore(cutb#connect#clicked cut) ;
3300 ignore(changeb#connect#clicked change) ;
3301 ignore(letinb#connect#clicked letin) ;
3302 ignore(ringb#connect#clicked ring) ;
3303 ignore(clearbodyb#connect#clicked clearbody) ;
3304 ignore(clearb#connect#clicked clear) ;
3305 ignore(fourierb#connect#clicked fourier) ;
3306 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3307 ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3308 ignore(replaceb#connect#clicked replace) ;
3309 ignore(reflexivityb#connect#clicked reflexivity) ;
3310 ignore(symmetryb#connect#clicked symmetry) ;
3311 ignore(transitivityb#connect#clicked transitivity) ;
3312 ignore(existsb#connect#clicked exists) ;
3313 ignore(splitb#connect#clicked split) ;
3314 ignore(leftb#connect#clicked left) ;
3315 ignore(rightb#connect#clicked right) ;
3316 ignore(assumptionb#connect#clicked assumption) ;
3317 ignore(generalizeb#connect#clicked generalize) ;
3318 ignore(absurdb#connect#clicked absurd) ;
3319 ignore(contradictionb#connect#clicked contradiction) ;
3320 ignore(introsb#connect#clicked intros) ;
3321 ignore(searchpatternb#connect#clicked searchPattern) ;
3322 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3328 let vbox1 = GPack.vbox () in
3329 let scrolled_window1 =
3330 GBin.scrolled_window ~border_width:10
3331 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3333 GMathView.math_view ~width:400 ~height:275
3334 ~packing:(scrolled_window1#add) () in
3336 method proofw = (assert false : GMathView.math_view)
3337 method content = vbox1
3338 method compute = (assert false : unit)
3342 let empty_page = new empty_page;;
3346 val notebook = GPack.notebook ()
3348 val mutable skip_switch_page_event = false
3349 val mutable empty = true
3350 method notebook = notebook
3352 let new_page = new page () in
3354 pages := !pages @ [n,lazy (setgoal n),new_page] ;
3355 notebook#append_page
3356 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3357 new_page#content#coerce
3358 method remove_all_pages ~skip_switch_page_event:skip =
3360 notebook#remove_page 0 (* let's remove the empty page *)
3362 List.iter (function _ -> notebook#remove_page 0) !pages ;
3364 skip_switch_page_event <- skip
3365 method set_current_page ~may_skip_switch_page_event n =
3366 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3367 let new_page = notebook#page_num page#content#coerce in
3368 if may_skip_switch_page_event && new_page <> notebook#current_page then
3369 skip_switch_page_event <- true ;
3370 notebook#goto_page new_page
3371 method set_empty_page =
3374 notebook#append_page
3375 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3376 empty_page#content#coerce
3378 let (_,_,page) = List.nth !pages notebook#current_page in
3382 (notebook#connect#switch_page
3384 let skip = skip_switch_page_event in
3385 skip_switch_page_event <- false ;
3388 let (metano,setgoal,page) = List.nth !pages i in
3389 ProofEngine.goal := Some metano ;
3390 Lazy.force (page#compute) ;
3399 class rendering_window output (notebook : notebook) =
3400 let scratch_window = new scratch_window in
3402 GWindow.window ~title:"MathML viewer" ~border_width:0
3403 ~allow_shrink:false () in
3404 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3406 let handle_box = GBin.handle_box ~border_width:2
3407 ~packing:(vbox_for_menu#pack ~padding:0) () in
3408 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3409 let factory0 = new GMenu.factory menubar in
3410 let accel_group = factory0#accel_group in
3412 let file_menu = factory0#add_submenu "File" in
3413 let factory1 = new GMenu.factory file_menu ~accel_group in
3414 let export_to_postscript_menu_item =
3417 factory1#add_item "New Block of (Co)Inductive Definitions..."
3418 ~key:GdkKeysyms._B ~callback:new_inductive
3421 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3424 let reopen_menu_item =
3425 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3429 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3430 ignore (factory1#add_separator ()) ;
3432 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3434 let save_menu_item =
3435 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3438 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3439 ignore (!save_set_sensitive false);
3440 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3441 ignore (!qed_set_sensitive false);
3442 ignore (factory1#add_separator ()) ;
3443 let export_to_postscript_menu_item =
3444 factory1#add_item "Export to PostScript..."
3445 ~callback:(export_to_postscript output) in
3446 ignore (factory1#add_separator ()) ;
3448 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3449 export_to_postscript_menu_item
3452 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3453 let factory2 = new GMenu.factory edit_menu ~accel_group in
3454 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3455 let proveit_menu_item =
3456 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3457 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3459 let focus_menu_item =
3460 factory2#add_item "Focus" ~key:GdkKeysyms._F
3461 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3464 focus_and_proveit_set_sensitive :=
3466 proveit_menu_item#misc#set_sensitive b ;
3467 focus_menu_item#misc#set_sensitive b
3469 let _ = !focus_and_proveit_set_sensitive false in
3470 (* edit term menu *)
3471 let edit_term_menu = factory0#add_submenu "Edit Term" in
3472 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3473 let check_menu_item =
3474 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3475 ~callback:(check scratch_window) in
3476 let _ = check_menu_item#misc#set_sensitive false in
3478 let settings_menu = factory0#add_submenu "Search" in
3479 let factory4 = new GMenu.factory settings_menu ~accel_group in
3481 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3483 let searchPattern_menu_item =
3484 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3485 ~callback:completeSearchPattern in
3486 let _ = searchPattern_menu_item#misc#set_sensitive false in
3487 let show_menu_item =
3488 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3490 let insert_query_item =
3491 factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3492 ~callback:insertQuery in
3494 let settings_menu = factory0#add_submenu "Settings" in
3495 let factory3 = new GMenu.factory settings_menu ~accel_group in
3497 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3498 ~callback:edit_aliases in
3499 let _ = factory3#add_separator () in
3501 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3502 ~callback:(function _ -> (settings_window ())#show ()) in
3504 let _ = window#add_accel_group accel_group in
3508 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3510 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3511 let scrolled_window0 =
3512 GBin.scrolled_window ~border_width:10
3513 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3514 let _ = scrolled_window0#add output#coerce in
3516 GBin.frame ~label:"Insert Term"
3517 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3518 let scrolled_window1 =
3519 GBin.scrolled_window ~border_width:5
3520 ~packing:frame#add () in
3522 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3523 ~isnotempty_callback:
3525 check_menu_item#misc#set_sensitive b ;
3526 searchPattern_menu_item#misc#set_sensitive b) in
3528 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3530 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3532 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3536 ~source:"<html><body bgColor=\"white\"></body></html>"
3537 ~width:400 ~height: 100
3542 method outputhtml = outputhtml
3543 method inputt = inputt
3544 method output = (output : GMathView.math_view)
3545 method notebook = notebook
3546 method show = window#show
3548 notebook#set_empty_page ;
3549 export_to_postscript_menu_item#misc#set_sensitive false ;
3550 check_term := (check_term_in_scratch scratch_window) ;
3552 (* signal handlers here *)
3553 ignore(output#connect#selection_changed
3555 choose_selection output elem ;
3556 !focus_and_proveit_set_sensitive true
3558 ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3559 let settings_window = new settings_window output scrolled_window0
3560 export_to_postscript_menu_item (choose_selection output) in
3561 set_settings_window settings_window ;
3562 set_outputhtml outputhtml ;
3563 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3564 Logger.log_callback :=
3565 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3570 let initialize_everything () =
3571 let module U = Unix in
3572 let output = GMathView.math_view ~width:350 ~height:280 () in
3573 let notebook = new notebook in
3574 let rendering_window' = new rendering_window output notebook in
3575 set_rendering_window rendering_window' ;
3576 mml_of_cic_term_ref := mml_of_cic_term ;
3577 rendering_window'#show () ;
3584 Mqint.set_database Mqint.postgres_db ;
3585 Mqint.init postgresqlconnectionstring ;
3587 ignore (GtkMain.Main.init ()) ;
3588 initialize_everything () ;
3589 if !usedb then Mqint.close ();