1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
37 (* GLOBAL CONSTANTS *)
39 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
40 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
44 " <body bgColor=\"white\">"
54 Sys.getenv "GTOPLEVEL_PROOFFILE"
56 Not_found -> "/public/currentproof"
61 Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
63 Not_found -> "/public/currentprooftype"
66 (*CSC: the getter should handle the innertypes, not the FS *)
70 Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
72 Not_found -> "/public/innertypes"
75 let constanttypefile =
77 Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
79 Not_found -> "/public/constanttype"
82 let postgresqlconnectionstring =
84 Sys.getenv "POSTGRESQL_CONNECTION_STRING"
86 Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
89 let empty_id_to_uris = ([],function _ -> None);;
92 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
94 let htmlheader_and_content = ref htmlheader;;
96 let current_cic_infos = ref None;;
97 let current_goal_infos = ref None;;
98 let current_scratch_infos = ref None;;
100 let id_to_uris = ref empty_id_to_uris;;
102 let check_term = ref (fun _ _ _ -> assert false);;
103 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
105 exception RenderingWindowsNotInitialized;;
107 let set_rendering_window,rendering_window =
108 let rendering_window_ref = ref None in
109 (function rw -> rendering_window_ref := Some rw),
111 match !rendering_window_ref with
112 None -> raise RenderingWindowsNotInitialized
117 exception SettingsWindowsNotInitialized;;
119 let set_settings_window,settings_window =
120 let settings_window_ref = ref None in
121 (function rw -> settings_window_ref := Some rw),
123 match !settings_window_ref with
124 None -> raise SettingsWindowsNotInitialized
129 exception OutputHtmlNotInitialized;;
131 let set_outputhtml,outputhtml =
132 let outputhtml_ref = ref None in
133 (function rw -> outputhtml_ref := Some rw),
135 match !outputhtml_ref with
136 None -> raise OutputHtmlNotInitialized
137 | Some outputhtml -> outputhtml
141 exception QedSetSensitiveNotInitialized;;
142 let qed_set_sensitive =
143 ref (function _ -> raise QedSetSensitiveNotInitialized)
146 exception SaveSetSensitiveNotInitialized;;
147 let save_set_sensitive =
148 ref (function _ -> raise SaveSetSensitiveNotInitialized)
151 (* COMMAND LINE OPTIONS *)
157 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
160 Arg.parse argspec ignore ""
164 let term_of_cic_textual_parser_uri uri =
165 let module C = Cic in
166 let module CTP = CicTextualParser0 in
168 CTP.ConUri uri -> C.Const (uri,[])
169 | CTP.VarUri uri -> C.Var (uri,[])
170 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
171 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
174 let string_of_cic_textual_parser_uri uri =
175 let module C = Cic in
176 let module CTP = CicTextualParser0 in
179 CTP.ConUri uri -> UriManager.string_of_uri uri
180 | CTP.VarUri uri -> UriManager.string_of_uri uri
181 | CTP.IndTyUri (uri,tyno) ->
182 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
183 | CTP.IndConUri (uri,tyno,consno) ->
184 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
187 (* 4 = String.length "cic:" *)
188 String.sub uri' 4 (String.length uri' - 4)
191 let output_html outputhtml msg =
192 htmlheader_and_content := !htmlheader_and_content ^ msg ;
193 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
194 outputhtml#set_topline (-1)
197 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
201 let check_window outputhtml uris =
204 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
206 GPack.notebook ~scrollable:true ~packing:window#add () in
211 let scrolled_window =
212 GBin.scrolled_window ~border_width:10
214 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
220 ~packing:scrolled_window#add ~width:400 ~height:280 () in
223 term_of_cic_textual_parser_uri
224 (Disambiguate.cic_textual_parser_uri_of_string uri)
226 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
229 let mml = !mml_of_cic_term_ref 111 expr in
230 mmlwidget#load_tree ~dom:mml
233 output_html outputhtml
234 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
239 (notebook#connect#switch_page
240 (function i -> Lazy.force (List.nth render_terms i)))
246 interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
247 ?(enable_button_for_non_vars=false) ~title ~msg uris
249 let choices = ref [] in
250 let chosen = ref false in
251 let use_only_constants = ref false in
253 GWindow.dialog ~modal:true ~title ~width:600 () in
255 GMisc.label ~text:msg
256 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
257 let scrolled_window =
258 GBin.scrolled_window ~border_width:10
259 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
261 let expected_height = 18 * List.length uris in
262 let height = if expected_height > 400 then 400 else expected_height in
263 GList.clist ~columns:1 ~packing:scrolled_window#add
264 ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
265 let _ = List.map (function x -> clist#append [x]) uris in
267 GPack.hbox ~border_width:0
268 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
270 GMisc.label ~text:"None of the above. Try this one:"
271 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
273 GEdit.entry ~editable:true
274 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
276 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
278 GButton.button ~label:ok
279 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
280 let _ = okb#misc#set_sensitive false in
285 if enable_button_for_non_vars then
286 hbox#pack ~expand:false ~fill:false ~padding:5 w)
287 ~label:"Try constants only" () in
289 GButton.button ~label:"Check"
290 ~packing:(hbox#pack ~padding:5) () in
291 let _ = checkb#misc#set_sensitive false in
293 GButton.button ~label:"Abort"
294 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
296 let check_callback () =
297 assert (List.length !choices > 0) ;
298 check_window (outputhtml ()) !choices
300 ignore (window#connect#destroy GMain.Main.quit) ;
301 ignore (cancelb#connect#clicked window#destroy) ;
303 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
305 (nonvarsb#connect#clicked
307 use_only_constants := true ;
311 ignore (checkb#connect#clicked check_callback) ;
313 (clist#connect#select_row
314 (fun ~row ~column ~event ->
315 checkb#misc#set_sensitive true ;
316 okb#misc#set_sensitive true ;
317 choices := (List.nth uris row)::!choices)) ;
319 (clist#connect#unselect_row
320 (fun ~row ~column ~event ->
322 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
324 (manual_input#connect#changed
326 if manual_input#text = "" then
329 checkb#misc#set_sensitive false ;
330 okb#misc#set_sensitive false ;
331 clist#misc#set_sensitive true
335 choices := [manual_input#text] ;
336 clist#unselect_all () ;
337 checkb#misc#set_sensitive true ;
338 okb#misc#set_sensitive true ;
339 clist#misc#set_sensitive false
341 window#set_position `CENTER ;
345 if !use_only_constants then
347 (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
350 if List.length !choices > 0 then !choices else raise NoChoice
355 EliminationTactics.interactive_user_uri_choice :=
356 (fun ~selection_mode -> interactive_user_uri_choice ~selection_mode:selection_mode);;
358 let interactive_interpretation_choice interpretations =
359 let chosen = ref None in
362 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
363 let vbox = GPack.vbox ~packing:window#add () in
367 ("Ambiguous input since there are many well-typed interpretations." ^
368 " Please, choose one of them.")
369 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
371 GPack.notebook ~scrollable:true
372 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
375 (function interpretation ->
377 let expected_height = 18 * List.length interpretation in
378 let height = if expected_height > 400 then 400 else expected_height in
379 GList.clist ~columns:2 ~packing:notebook#append_page ~height
380 ~titles:["id" ; "URI"] ()
384 (function (id,uri) ->
385 let n = clist#append [id;uri] in
386 clist#set_row ~selectable:false n
389 clist#columns_autosize ()
392 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
394 GButton.button ~label:"Ok"
395 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
397 GButton.button ~label:"Abort"
398 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
400 ignore (window#connect#destroy GMain.Main.quit) ;
401 ignore (cancelb#connect#clicked window#destroy) ;
404 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
405 window#set_position `CENTER ;
409 None -> raise NoChoice
416 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
418 let query = ref "" in
419 MQueryGenerator.set_confirm_query
420 (function q -> query := MQueryUtil.text_of_query q ; true) ;
421 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
424 let domImpl = Gdome.domImplementation ();;
426 let parseStyle name =
428 domImpl#createDocumentFromURI
430 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
432 ~uri:("styles/" ^ name) ()
434 Gdome_xslt.processStylesheet style
437 let d_c = parseStyle "drop_coercions.xsl";;
438 let tc1 = parseStyle "objtheorycontent.xsl";;
439 let hc2 = parseStyle "content_to_html.xsl";;
440 let l = parseStyle "link.xsl";;
442 let c1 = parseStyle "rootcontent.xsl";;
443 let g = parseStyle "genmmlid.xsl";;
444 let c2 = parseStyle "annotatedpres.xsl";;
447 let getterURL = Configuration.getter_url;;
448 let processorURL = Configuration.processor_url;;
450 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
451 let mml_args ~explode_all =
452 ("explodeall",(if explode_all then "true()" else "false()"))::
453 ["processorURL", "'" ^ processorURL ^ "'" ;
454 "getterURL", "'" ^ getterURL ^ "'" ;
455 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
456 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
457 "UNICODEvsSYMBOL", "'symbol'" ;
458 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
459 "encoding", "'iso-8859-1'" ;
460 "media-type", "'text/html'" ;
461 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
462 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
463 "naturalLanguage", "'yes'" ;
464 "annotations", "'no'" ;
465 "URLs_or_URIs", "'URIs'" ;
466 "topurl", "'http://phd.cs.unibo.it/helm'" ;
467 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
470 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
472 ["processorURL", "'" ^ processorURL ^ "'" ;
473 "getterURL", "'" ^ getterURL ^ "'" ;
474 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
475 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
476 "UNICODEvsSYMBOL", "'symbol'" ;
477 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
478 "encoding", "'iso-8859-1'" ;
479 "media-type", "'text/html'" ;
480 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
481 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
482 "naturalLanguage", "'no'" ;
483 "annotations", "'no'" ;
484 "explodeall", "true()" ;
485 "URLs_or_URIs", "'URIs'" ;
486 "topurl", "'http://phd.cs.unibo.it/helm'" ;
487 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
490 let parse_file filename =
491 let inch = open_in filename in
492 let rec read_lines () =
494 let line = input_line inch in
502 let applyStylesheets input styles args =
503 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
508 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
510 (*CSC: ????????????????? *)
512 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
516 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
517 ~ask_dtd_to_the_getter:true
521 None -> Xml2Gdome.document_of_xml domImpl xml
523 Xml.pp xml (Some constanttypefile) ;
524 Xml2Gdome.document_of_xml domImpl bodyxml'
526 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
527 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
529 Xml.pp xmlinnertypes (Some innertypesfile) ;
530 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
535 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
538 let struri = UriManager.string_of_uri uri in
539 let idx = (String.rindex struri '/') + 1 in
540 String.sub struri idx (String.length struri - idx)
542 let path = pathname ^ "/" ^ name in
544 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
548 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
549 ~ask_dtd_to_the_getter:false
552 let innertypesuri = UriManager.innertypesuri_of_uri uri in
553 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
554 Getter.register innertypesuri
555 (Configuration.annotations_url ^
556 Str.replace_first (Str.regexp "^cic:") ""
557 (UriManager.string_of_uri innertypesuri) ^ ".xml"
559 (* constant type / variable / mutual inductive types definition *)
560 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
562 (Configuration.annotations_url ^
563 Str.replace_first (Str.regexp "^cic:") ""
564 (UriManager.string_of_uri uri) ^ ".xml"
571 match UriManager.bodyuri_of_uri uri with
573 | Some bodyuri -> bodyuri
575 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
576 Getter.register bodyuri
577 (Configuration.annotations_url ^
578 Str.replace_first (Str.regexp "^cic:") ""
579 (UriManager.string_of_uri bodyuri) ^ ".xml"
586 exception RefreshSequentException of exn;;
587 exception RefreshProofException of exn;;
589 let refresh_proof (output : GMathView.math_view) =
591 let uri,currentproof =
592 match !ProofEngine.proof with
594 | Some (uri,metasenv,bo,ty) ->
595 !qed_set_sensitive (List.length metasenv = 0) ;
596 (*CSC: Wrong: [] is just plainly wrong *)
597 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
600 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
601 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
603 Cic2acic.acic_object_of_cic_object currentproof
606 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
609 output#load_tree mml ;
611 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
614 match !ProofEngine.proof with
616 | Some (uri,metasenv,bo,ty) ->
617 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
618 raise (RefreshProofException e)
621 let refresh_sequent ?(empty_notebook=true) notebook =
623 match !ProofEngine.goal with
625 if empty_notebook then
627 notebook#remove_all_pages ~skip_switch_page_event:false ;
628 notebook#set_empty_page
631 notebook#proofw#unload
634 match !ProofEngine.proof with
636 | Some (_,metasenv,_,_) -> metasenv
638 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
639 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
640 SequentPp.XmlPp.print_sequent metasenv currentsequent
642 let regenerate_notebook () =
643 let skip_switch_page_event =
645 (m,_,_)::_ when m = metano -> false
648 notebook#remove_all_pages ~skip_switch_page_event ;
649 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
651 if empty_notebook then
653 regenerate_notebook () ;
654 notebook#set_current_page ~may_skip_switch_page_event:false metano
658 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
660 applyStylesheets sequent_doc sequent_styles sequent_args
662 notebook#set_current_page ~may_skip_switch_page_event:true metano;
663 notebook#proofw#load_tree ~dom:sequent_mml
665 current_goal_infos :=
666 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
670 match !ProofEngine.goal with
675 match !ProofEngine.proof with
677 | Some (_,metasenv,_,_) -> metasenv
680 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
681 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
682 raise (RefreshSequentException e)
683 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
687 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
688 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
691 let mml_of_cic_term metano term =
693 match !ProofEngine.proof with
695 | Some (_,metasenv,_,_) -> metasenv
698 match !ProofEngine.goal with
701 let (_,canonical_context,_) =
702 List.find (function (m,_,_) -> m=metano) metasenv
706 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
707 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
710 Xml2Gdome.document_of_xml domImpl sequent_gdome
713 applyStylesheets sequent_doc sequent_styles sequent_args ;
715 current_scratch_infos :=
716 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
720 exception OpenConjecturesStillThere;;
721 exception WrongProof;;
723 let pathname_of_annuri uristring =
724 Configuration.annotations_dir ^
725 Str.replace_first (Str.regexp "^cic:") "" uristring
728 let make_dirs dirpath =
729 ignore (Unix.system ("mkdir -p " ^ dirpath))
732 let save_obj uri obj =
734 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
735 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
737 Cic2acic.acic_object_of_cic_object obj
739 (* let's save the theorem and register it to the getter *)
740 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
742 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
747 match !ProofEngine.proof with
749 | Some (uri,[],bo,ty) ->
751 CicReduction.are_convertible []
752 (CicTypeChecker.type_of_aux' [] [] bo) ty
755 (*CSC: Wrong: [] is just plainly wrong *)
756 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
758 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
759 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
761 Cic2acic.acic_object_of_cic_object proof
764 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
767 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
768 !qed_set_sensitive false ;
769 (* let's save the theorem and register it to the getter *)
770 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
772 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
776 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
781 | _ -> raise OpenConjecturesStillThere
785 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
786 match !ProofEngine.proof with
788 | Some (uri, metasenv, bo, ty) ->
790 (*CSC: Wrong: [] is just plainly wrong *)
791 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
793 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
794 Cic2acic.acic_object_of_cic_object currentproof
798 Cic2Xml.print_object uri ~ids_to_inner_sorts
799 ~ask_dtd_to_the_getter:true acurrentproof
801 xml,Some bodyxml -> xml,bodyxml
802 | _,None -> assert false
804 Xml.pp ~quiet:true xml (Some prooffiletype) ;
805 output_html outputhtml
806 ("<h1 color=\"Green\">Current proof type saved to " ^
807 prooffiletype ^ "</h1>") ;
808 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
809 output_html outputhtml
810 ("<h1 color=\"Green\">Current proof body saved to " ^
814 (* Used to typecheck the loaded proofs *)
815 let typecheck_loaded_proof metasenv bo ty =
816 let module T = CicTypeChecker in
819 (fun metasenv ((_,context,ty) as conj) ->
820 ignore (T.type_of_aux' metasenv context ty) ;
823 ignore (T.type_of_aux' metasenv [] ty) ;
824 ignore (T.type_of_aux' metasenv [] bo)
828 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
829 let output = ((rendering_window ())#output : GMathView.math_view) in
830 let notebook = (rendering_window ())#notebook in
833 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
836 None -> raise NoChoice
838 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
839 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
840 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
841 typecheck_loaded_proof metasenv bo ty ;
843 Some (uri, metasenv, bo, ty) ;
847 | (metano,_,_)::_ -> Some metano
849 refresh_proof output ;
850 refresh_sequent notebook ;
851 output_html outputhtml
852 ("<h1 color=\"Green\">Current proof type loaded from " ^
853 prooffiletype ^ "</h1>") ;
854 output_html outputhtml
855 ("<h1 color=\"Green\">Current proof body loaded from " ^
856 prooffile ^ "</h1>") ;
857 !save_set_sensitive true
860 RefreshSequentException e ->
861 output_html outputhtml
862 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
863 "sequent: " ^ Printexc.to_string e ^ "</h1>")
864 | RefreshProofException e ->
865 output_html outputhtml
866 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
867 "proof: " ^ Printexc.to_string e ^ "</h1>")
869 output_html outputhtml
870 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
873 let edit_aliases () =
874 let chosen = ref false in
877 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
879 GPack.vbox ~border_width:0 ~packing:window#add () in
880 let scrolled_window =
881 GBin.scrolled_window ~border_width:10
882 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
883 let input = GEdit.text ~editable:true ~width:400 ~height:100
884 ~packing:scrolled_window#add () in
886 GPack.hbox ~border_width:0
887 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
889 GButton.button ~label:"Ok"
890 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
892 GButton.button ~label:"Cancel"
893 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
894 ignore (window#connect#destroy GMain.Main.quit) ;
895 ignore (cancelb#connect#clicked window#destroy) ;
897 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
898 let dom,resolve_id = !id_to_uris in
900 (input#insert_text ~pos:0
905 match resolve_id v with
910 (string_of_cic_textual_parser_uri uri)
916 let inputtext = input#get_chars 0 input#length in
918 let alfa = "[a-zA-Z_-]" in
919 let digit = "[0-9]" in
920 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
921 let blanks = "\( \|\t\|\n\)+" in
922 let nonblanks = "[^ \t\n]+" in
923 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
925 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
929 let n' = Str.search_forward regexpr inputtext n in
930 let id = Str.matched_group 2 inputtext in
932 Disambiguate.cic_textual_parser_uri_of_string
933 ("cic:" ^ (Str.matched_group 5 inputtext))
935 let dom,resolve_id = aux (n' + 1) in
936 if List.mem id dom then
940 (function id' -> if id = id' then Some uri else resolve_id id')
942 Not_found -> empty_id_to_uris
946 id_to_uris := dom,resolve_id
950 let module L = LogicalOperations in
951 let module G = Gdome in
952 let notebook = (rendering_window ())#notebook in
953 let output = (rendering_window ())#output in
954 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
955 match (rendering_window ())#output#get_selection with
958 ((node : Gdome.element)#getAttributeNS
960 ((element : G.element)#getAttributeNS
963 ~localName:(G.domString "xref"))#to_string
965 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
969 match !current_cic_infos with
970 Some (ids_to_terms, ids_to_father_ids, _, _) ->
972 L.to_sequent id ids_to_terms ids_to_father_ids ;
973 refresh_proof output ;
974 refresh_sequent notebook
975 | None -> assert false (* "ERROR: No current term!!!" *)
977 RefreshSequentException e ->
978 output_html outputhtml
979 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
980 "sequent: " ^ Printexc.to_string e ^ "</h1>")
981 | RefreshProofException e ->
982 output_html outputhtml
983 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
984 "proof: " ^ Printexc.to_string e ^ "</h1>")
986 output_html outputhtml
987 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
989 | None -> assert false (* "ERROR: No selection!!!" *)
993 let module L = LogicalOperations in
994 let module G = Gdome in
995 let notebook = (rendering_window ())#notebook in
996 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
997 match (rendering_window ())#output#get_selection with
1000 ((node : Gdome.element)#getAttributeNS
1001 (*CSC: OCAML DIVERGE
1002 ((element : G.element)#getAttributeNS
1004 ~namespaceURI:helmns
1005 ~localName:(G.domString "xref"))#to_string
1007 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1011 match !current_cic_infos with
1012 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1014 L.focus id ids_to_terms ids_to_father_ids ;
1015 refresh_sequent notebook
1016 | None -> assert false (* "ERROR: No current term!!!" *)
1018 RefreshSequentException e ->
1019 output_html outputhtml
1020 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1021 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1022 | RefreshProofException e ->
1023 output_html outputhtml
1024 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1025 "proof: " ^ Printexc.to_string e ^ "</h1>")
1027 output_html outputhtml
1028 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1030 | None -> assert false (* "ERROR: No selection!!!" *)
1033 exception NoPrevGoal;;
1034 exception NoNextGoal;;
1036 let setgoal metano =
1037 let module L = LogicalOperations in
1038 let module G = Gdome in
1039 let notebook = (rendering_window ())#notebook in
1040 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1042 match !ProofEngine.proof with
1043 None -> assert false
1044 | Some (_,metasenv,_,_) -> metasenv
1047 refresh_sequent ~empty_notebook:false notebook
1049 RefreshSequentException e ->
1050 output_html outputhtml
1051 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1052 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1054 output_html outputhtml
1055 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1059 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1062 GWindow.window ~width:800 ~border_width:2 () in
1063 let scrolled_window =
1064 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1066 GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1067 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1068 let href = Gdome.domString "href" in
1069 let show_in_show_window_obj uri obj =
1070 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1073 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1074 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1076 Cic2acic.acic_object_of_cic_object obj
1079 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1082 window#set_title (UriManager.string_of_uri uri) ;
1083 window#misc#hide () ; window#show () ;
1084 mmlwidget#load_tree mml ;
1087 output_html outputhtml
1088 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1090 let show_in_show_window_uri uri =
1091 let obj = CicEnvironment.get_obj uri in
1092 show_in_show_window_obj uri obj
1094 let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1095 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1097 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1099 show_in_show_window_uri (UriManager.uri_of_string uri)
1101 if mmlwidget#get_action <> None then
1102 mmlwidget#action_toggle
1105 mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1107 show_in_show_window_obj, show_in_show_window_uri,
1108 show_in_show_window_callback
1111 exception NoObjectsLocated;;
1113 let user_uri_choice ~title ~msg uris =
1116 [] -> raise NoObjectsLocated
1120 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1125 String.sub uri 4 (String.length uri - 4)
1128 let locate_callback id =
1129 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1130 let result = MQueryGenerator.locate id in
1134 Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
1137 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1139 output_html outputhtml html ;
1140 user_uri_choice ~title:"Ambiguous input."
1142 ("Ambiguous input \"" ^ id ^
1143 "\". Please, choose one interpetation:")
1148 let input_or_locate_uri ~title =
1149 let uri = ref None in
1152 ~width:400 ~modal:true ~title ~border_width:2 () in
1153 let vbox = GPack.vbox ~packing:window#add () in
1155 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1157 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1159 GEdit.entry ~editable:true
1160 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1162 GButton.button ~label:"Check"
1163 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1164 let _ = checkb#misc#set_sensitive false in
1166 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1168 GMisc.label ~text:"You can also enter an indentifier to locate:"
1169 ~packing:(hbox2#pack ~padding:5) () in
1171 GEdit.entry ~editable:true
1172 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1174 GButton.button ~label:"Locate"
1175 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1176 let _ = locateb#misc#set_sensitive false in
1178 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1180 GButton.button ~label:"Ok"
1181 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1182 let _ = okb#misc#set_sensitive false in
1184 GButton.button ~label:"Cancel"
1185 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1187 ignore (window#connect#destroy GMain.Main.quit) ;
1189 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1190 let check_callback () =
1191 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1192 let uri = "cic:" ^ manual_input#text in
1194 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1195 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1198 Getter.Unresolved ->
1199 output_html outputhtml
1200 ("<h1 color=\"Red\">URI " ^ uri ^
1201 " does not correspond to any object.</h1>") ;
1203 | UriManager.IllFormedUri _ ->
1204 output_html outputhtml
1205 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1208 output_html outputhtml
1209 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1213 (okb#connect#clicked
1215 if check_callback () then
1217 uri := Some manual_input#text ;
1221 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1223 (manual_input#connect#changed
1225 if manual_input#text = "" then
1227 checkb#misc#set_sensitive false ;
1228 okb#misc#set_sensitive false
1232 checkb#misc#set_sensitive true ;
1233 okb#misc#set_sensitive true
1236 (locate_input#connect#changed
1237 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1239 (locateb#connect#clicked
1241 let id = locate_input#text in
1242 manual_input#set_text (locate_callback id) ;
1243 locate_input#delete_text 0 (String.length id)
1246 GMain.Main.main () ;
1248 None -> raise NoChoice
1249 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1252 exception AmbiguousInput;;
1254 (* A WIDGET TO ENTER CIC TERMS *)
1258 let output_html msg = output_html (outputhtml ()) msg;;
1259 let interactive_user_uri_choice =
1260 fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
1261 interactive_user_uri_choice ~selection_mode ?ok
1262 ?enable_button_for_non_vars ~title ~msg;;
1263 let interactive_interpretation_choice = interactive_interpretation_choice;;
1264 let input_or_locate_uri = input_or_locate_uri;;
1268 module Disambiguate' = Disambiguate.Make(Callbacks);;
1270 class term_editor ?packing ?width ?height ?isnotempty_callback () =
1271 let input = GEdit.text ~editable:true ?width ?height ?packing () in
1273 match isnotempty_callback with
1276 ignore(input#connect#changed (function () -> callback (input#length > 0)))
1279 method coerce = input#coerce
1281 input#delete_text 0 input#length
1282 (* CSC: txt is now a string, but should be of type Cic.term *)
1283 method set_term txt =
1285 ignore ((input#insert_text txt) ~pos:0)
1286 (* CSC: this method should disappear *)
1287 method get_as_string =
1288 input#get_chars 0 input#length
1289 method get_metasenv_and_term ~context ~metasenv =
1293 Some (n,_) -> Some n
1297 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
1298 let dom,mk_metasenv_and_expr =
1299 CicTextualParserContext.main
1300 ~context:name_context ~metasenv CicTextualLexer.token lexbuf
1302 let id_to_uris',metasenv,expr =
1303 Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
1304 ~id_to_uris:!id_to_uris
1306 id_to_uris := id_to_uris' ;
1311 (* OTHER FUNCTIONS *)
1314 let inputt = ((rendering_window ())#inputt : term_editor) in
1315 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1318 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1320 None -> raise NoChoice
1322 let uri = locate_callback input in
1326 output_html outputhtml
1327 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1331 exception UriAlreadyInUse;;
1332 exception NotAUriToAConstant;;
1334 let new_inductive () =
1335 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1336 let output = ((rendering_window ())#output : GMathView.math_view) in
1337 let notebook = (rendering_window ())#notebook in
1339 let chosen = ref false in
1340 let inductive = ref true in
1341 let paramsno = ref 0 in
1342 let get_uri = ref (function _ -> assert false) in
1343 let get_base_uri = ref (function _ -> assert false) in
1344 let get_names = ref (function _ -> assert false) in
1345 let get_types_and_cons = ref (function _ -> assert false) in
1346 let get_context_and_subst = ref (function _ -> assert false) in
1349 ~width:600 ~modal:true ~position:`CENTER
1350 ~title:"New Block of Mutual (Co)Inductive Definitions"
1351 ~border_width:2 () in
1352 let vbox = GPack.vbox ~packing:window#add () in
1354 GPack.hbox ~border_width:0
1355 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1357 GMisc.label ~text:"Enter the URI for the new block:"
1358 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1360 GEdit.entry ~editable:true
1361 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1363 GPack.hbox ~border_width:0
1364 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1368 "Enter the number of left parameters in every arity and constructor type:"
1369 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1370 let paramsno_entry =
1371 GEdit.entry ~editable:true ~text:"0"
1372 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1374 GPack.hbox ~border_width:0
1375 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1377 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1378 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1380 GButton.radio_button ~label:"Inductive"
1381 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1383 GButton.radio_button ~label:"Coinductive"
1384 ~group:inductiveb#group
1385 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1387 GPack.hbox ~border_width:0
1388 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1390 GMisc.label ~text:"Enter the list of the names of the types:"
1391 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1393 GEdit.entry ~editable:true
1394 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1396 GPack.hbox ~border_width:0
1397 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1399 GButton.button ~label:"> Next"
1400 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1401 let _ = okb#misc#set_sensitive true in
1403 GButton.button ~label:"Abort"
1404 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1405 ignore (window#connect#destroy GMain.Main.quit) ;
1406 ignore (cancelb#connect#clicked window#destroy) ;
1410 (okb#connect#clicked
1413 let uristr = "cic:" ^ uri_entry#text in
1414 let namesstr = names_entry#text in
1415 let paramsno' = int_of_string (paramsno_entry#text) in
1416 match Str.split (Str.regexp " +") namesstr with
1418 | (he::tl) as names ->
1419 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1422 ignore (Getter.resolve uri) ;
1423 raise UriAlreadyInUse
1425 Getter.Unresolved ->
1426 get_uri := (function () -> uri) ;
1427 get_names := (function () -> names) ;
1428 inductive := inductiveb#active ;
1429 paramsno := paramsno' ;
1434 output_html outputhtml
1435 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1443 GBin.frame ~label:name
1444 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1445 let vbox = GPack.vbox ~packing:frame#add () in
1446 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1448 GMisc.label ~text:("Enter its type:")
1449 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1450 let scrolled_window =
1451 GBin.scrolled_window ~border_width:5
1452 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1454 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1455 ~isnotempty_callback:
1457 (*non_empty_type := b ;*)
1458 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1461 GPack.hbox ~border_width:0
1462 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1464 GMisc.label ~text:("Enter the list of its constructors:")
1465 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1466 let cons_names_entry =
1467 GEdit.entry ~editable:true
1468 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1469 (newinputt,cons_names_entry)
1472 vbox#remove hboxn#coerce ;
1474 GPack.hbox ~border_width:0
1475 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1477 GButton.button ~label:"> Next"
1478 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1480 GButton.button ~label:"Abort"
1481 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1482 ignore (cancelb#connect#clicked window#destroy) ;
1484 (okb#connect#clicked
1487 let names = !get_names () in
1488 let types_and_cons =
1490 (fun name (newinputt,cons_names_entry) ->
1491 let consnamesstr = cons_names_entry#text in
1492 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1494 newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1497 [] -> expr,cons_names
1498 | _ -> raise AmbiguousInput
1499 ) names type_widgets
1501 let uri = !get_uri () in
1503 (* Let's see if so far the definition is well-typed *)
1506 (* To test if the arities of the inductive types are well *)
1507 (* typed, we check the inductive block definition where *)
1508 (* no constructor is given to each type. *)
1511 (fun name (ty,cons) -> (name, !inductive, ty, []))
1512 names types_and_cons
1514 CicTypeChecker.typecheck_mutual_inductive_defs uri
1515 (tys,params,paramsno)
1517 get_context_and_subst :=
1521 (fun (context,subst) name (ty,_) ->
1523 (Some (Cic.Name name, Cic.Decl ty))::context,
1524 (Cic.MutInd (uri,!i,[]))::subst
1527 ) ([],[]) names types_and_cons) ;
1528 let types_and_cons' =
1530 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1531 names types_and_cons
1533 get_types_and_cons := (function () -> types_and_cons') ;
1538 output_html outputhtml
1539 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1542 and phase3 name cons =
1543 let get_cons_types = ref (function () -> assert false) in
1546 ~width:600 ~modal:true ~position:`CENTER
1547 ~title:(name ^ " Constructors")
1548 ~border_width:2 () in
1549 let vbox = GPack.vbox ~packing:window2#add () in
1550 let cons_type_widgets =
1552 (function consname ->
1554 GPack.hbox ~border_width:0
1555 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1557 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1558 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1559 let scrolled_window =
1560 GBin.scrolled_window ~border_width:5
1561 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1563 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1564 ~isnotempty_callback:
1566 (* (*non_empty_type := b ;*)
1567 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1572 GPack.hbox ~border_width:0
1573 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1575 GButton.button ~label:"> Next"
1576 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1577 let _ = okb#misc#set_sensitive true in
1579 GButton.button ~label:"Abort"
1580 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1581 ignore (window2#connect#destroy GMain.Main.quit) ;
1582 ignore (cancelb#connect#clicked window2#destroy) ;
1584 (okb#connect#clicked
1588 let context,subst= !get_context_and_subst () in
1593 inputt#get_metasenv_and_term ~context ~metasenv:[]
1597 let undebrujined_expr =
1599 (fun expr t -> CicSubstitution.subst t expr) expr subst
1601 name, undebrujined_expr
1602 | _ -> raise AmbiguousInput
1603 ) cons cons_type_widgets
1605 get_cons_types := (function () -> cons_types) ;
1609 output_html outputhtml
1610 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1613 GMain.Main.main () ;
1614 let okb_pressed = !chosen in
1616 if (not okb_pressed) then
1619 assert false (* The control never reaches this point *)
1622 (!get_cons_types ())
1625 (* No more phases left or Abort pressed *)
1627 GMain.Main.main () ;
1631 let uri = !get_uri () in
1634 let tys = !get_types_and_cons () in
1635 let obj = Cic.InductiveDefinition tys params !paramsno in
1638 prerr_endline (CicPp.ppobj obj) ;
1639 CicTypeChecker.typecheck_mutual_inductive_defs uri
1640 (tys,params,!paramsno) ;
1643 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1644 prerr_endline (CicPp.ppobj obj) ;
1646 (* We already know that obj is well-typed. We need to add it to the *)
1647 (* environment in order to compute the inner-types without having to *)
1648 (* debrujin it or having to modify lots of other functions to avoid *)
1649 (* asking the environment for the MUTINDs we are defining now. *)
1650 CicEnvironment.put_inductive_definition uri obj ;
1652 show_in_show_window_obj uri obj
1655 output_html outputhtml
1656 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1660 let inputt = ((rendering_window ())#inputt : term_editor) in
1661 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1662 let output = ((rendering_window ())#output : GMathView.math_view) in
1663 let notebook = (rendering_window ())#notebook in
1665 let chosen = ref false in
1666 let get_metasenv_and_term = ref (function _ -> assert false) in
1667 let get_uri = ref (function _ -> assert false) in
1668 let non_empty_type = ref false in
1671 ~width:600 ~modal:true ~title:"New Proof or Definition"
1672 ~border_width:2 () in
1673 let vbox = GPack.vbox ~packing:window#add () in
1675 GPack.hbox ~border_width:0
1676 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1678 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1679 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1681 GEdit.entry ~editable:true
1682 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1684 GPack.hbox ~border_width:0
1685 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1687 GMisc.label ~text:"Enter the theorem or definition type:"
1688 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1689 let scrolled_window =
1690 GBin.scrolled_window ~border_width:5
1691 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1692 (* the content of the scrolled_window is moved below (see comment) *)
1694 GPack.hbox ~border_width:0
1695 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1697 GButton.button ~label:"Ok"
1698 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1699 let _ = okb#misc#set_sensitive false in
1701 GButton.button ~label:"Cancel"
1702 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1703 (* moved here to have visibility of the ok button *)
1705 new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1706 ~isnotempty_callback:
1708 non_empty_type := b ;
1709 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1712 newinputt#set_term inputt#get_as_string ;
1715 uri_entry#connect#changed
1717 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1719 ignore (window#connect#destroy GMain.Main.quit) ;
1720 ignore (cancelb#connect#clicked window#destroy) ;
1722 (okb#connect#clicked
1726 let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1727 let uristr = "cic:" ^ uri_entry#text in
1728 let uri = UriManager.uri_of_string uristr in
1729 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1730 raise NotAUriToAConstant
1734 ignore (Getter.resolve uri) ;
1735 raise UriAlreadyInUse
1737 Getter.Unresolved ->
1738 get_metasenv_and_term := (function () -> metasenv,parsed) ;
1739 get_uri := (function () -> uri) ;
1744 output_html outputhtml
1745 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1748 GMain.Main.main () ;
1751 let metasenv,expr = !get_metasenv_and_term () in
1752 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1753 ProofEngine.proof :=
1754 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1755 ProofEngine.goal := Some 1 ;
1756 refresh_sequent notebook ;
1757 refresh_proof output ;
1758 !save_set_sensitive true ;
1761 RefreshSequentException e ->
1762 output_html outputhtml
1763 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1764 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1765 | RefreshProofException e ->
1766 output_html outputhtml
1767 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1768 "proof: " ^ Printexc.to_string e ^ "</h1>")
1770 output_html outputhtml
1771 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1774 let check_term_in_scratch scratch_window metasenv context expr =
1776 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1777 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1778 scratch_window#show () ;
1779 scratch_window#mmlwidget#load_tree ~dom:mml
1782 print_endline ("? " ^ CicPp.ppterm expr) ;
1786 let check scratch_window () =
1787 let inputt = ((rendering_window ())#inputt : term_editor) in
1788 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1790 match !ProofEngine.proof with
1792 | Some (_,metasenv,_,_) -> metasenv
1795 match !ProofEngine.goal with
1798 let (_,canonical_context,_) =
1799 List.find (function (m,_,_) -> m=metano) metasenv
1804 let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
1805 check_term_in_scratch scratch_window metasenv' context expr
1808 output_html outputhtml
1809 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1813 (***********************)
1815 (***********************)
1817 let call_tactic tactic () =
1818 let notebook = (rendering_window ())#notebook in
1819 let output = ((rendering_window ())#output : GMathView.math_view) in
1820 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1821 let savedproof = !ProofEngine.proof in
1822 let savedgoal = !ProofEngine.goal in
1826 refresh_sequent notebook ;
1827 refresh_proof output
1829 RefreshSequentException e ->
1830 output_html outputhtml
1831 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1832 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1833 ProofEngine.proof := savedproof ;
1834 ProofEngine.goal := savedgoal ;
1835 refresh_sequent notebook
1836 | RefreshProofException e ->
1837 output_html outputhtml
1838 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1839 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1840 ProofEngine.proof := savedproof ;
1841 ProofEngine.goal := savedgoal ;
1842 refresh_sequent notebook ;
1843 refresh_proof output
1845 output_html outputhtml
1846 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1847 ProofEngine.proof := savedproof ;
1848 ProofEngine.goal := savedgoal ;
1852 let call_tactic_with_input tactic () =
1853 let notebook = (rendering_window ())#notebook in
1854 let output = ((rendering_window ())#output : GMathView.math_view) in
1855 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1856 let inputt = ((rendering_window ())#inputt : term_editor) in
1857 let savedproof = !ProofEngine.proof in
1858 let savedgoal = !ProofEngine.goal in
1859 let uri,metasenv,bo,ty =
1860 match !ProofEngine.proof with
1861 None -> assert false
1862 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1864 let canonical_context =
1865 match !ProofEngine.goal with
1866 None -> assert false
1868 let (_,canonical_context,_) =
1869 List.find (function (m,_,_) -> m=metano) metasenv
1874 let metasenv',expr =
1875 inputt#get_metasenv_and_term canonical_context metasenv
1877 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1879 refresh_sequent notebook ;
1880 refresh_proof output ;
1883 RefreshSequentException e ->
1884 output_html outputhtml
1885 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1886 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1887 ProofEngine.proof := savedproof ;
1888 ProofEngine.goal := savedgoal ;
1889 refresh_sequent notebook
1890 | RefreshProofException e ->
1891 output_html outputhtml
1892 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1893 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1894 ProofEngine.proof := savedproof ;
1895 ProofEngine.goal := savedgoal ;
1896 refresh_sequent notebook ;
1897 refresh_proof output
1899 output_html outputhtml
1900 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1901 ProofEngine.proof := savedproof ;
1902 ProofEngine.goal := savedgoal ;
1905 let call_tactic_with_goal_input tactic () =
1906 let module L = LogicalOperations in
1907 let module G = Gdome in
1908 let notebook = (rendering_window ())#notebook in
1909 let output = ((rendering_window ())#output : GMathView.math_view) in
1910 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1911 let savedproof = !ProofEngine.proof in
1912 let savedgoal = !ProofEngine.goal in
1913 match notebook#proofw#get_selection with
1916 ((node : Gdome.element)#getAttributeNS
1917 ~namespaceURI:helmns
1918 ~localName:(G.domString "xref"))#to_string
1920 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1924 match !current_goal_infos with
1925 Some (ids_to_terms, ids_to_father_ids,_) ->
1927 tactic (Hashtbl.find ids_to_terms id) ;
1928 refresh_sequent notebook ;
1929 refresh_proof output
1930 | None -> assert false (* "ERROR: No current term!!!" *)
1932 RefreshSequentException e ->
1933 output_html outputhtml
1934 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1935 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1936 ProofEngine.proof := savedproof ;
1937 ProofEngine.goal := savedgoal ;
1938 refresh_sequent notebook
1939 | RefreshProofException e ->
1940 output_html outputhtml
1941 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1942 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1943 ProofEngine.proof := savedproof ;
1944 ProofEngine.goal := savedgoal ;
1945 refresh_sequent notebook ;
1946 refresh_proof output
1948 output_html outputhtml
1949 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1950 ProofEngine.proof := savedproof ;
1951 ProofEngine.goal := savedgoal ;
1954 output_html outputhtml
1955 ("<h1 color=\"red\">No term selected</h1>")
1958 let call_tactic_with_input_and_goal_input tactic () =
1959 let module L = LogicalOperations in
1960 let module G = Gdome in
1961 let notebook = (rendering_window ())#notebook in
1962 let output = ((rendering_window ())#output : GMathView.math_view) in
1963 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1964 let inputt = ((rendering_window ())#inputt : term_editor) in
1965 let savedproof = !ProofEngine.proof in
1966 let savedgoal = !ProofEngine.goal in
1967 match notebook#proofw#get_selection with
1970 ((node : Gdome.element)#getAttributeNS
1971 ~namespaceURI:helmns
1972 ~localName:(G.domString "xref"))#to_string
1974 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1978 match !current_goal_infos with
1979 Some (ids_to_terms, ids_to_father_ids,_) ->
1981 let uri,metasenv,bo,ty =
1982 match !ProofEngine.proof with
1983 None -> assert false
1984 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1986 let canonical_context =
1987 match !ProofEngine.goal with
1988 None -> assert false
1990 let (_,canonical_context,_) =
1991 List.find (function (m,_,_) -> m=metano) metasenv
1993 canonical_context in
1994 let (metasenv',expr) =
1995 inputt#get_metasenv_and_term canonical_context metasenv
1997 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1998 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2000 refresh_sequent notebook ;
2001 refresh_proof output ;
2003 | None -> assert false (* "ERROR: No current term!!!" *)
2005 RefreshSequentException e ->
2006 output_html outputhtml
2007 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2008 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2009 ProofEngine.proof := savedproof ;
2010 ProofEngine.goal := savedgoal ;
2011 refresh_sequent notebook
2012 | RefreshProofException e ->
2013 output_html outputhtml
2014 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2015 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2016 ProofEngine.proof := savedproof ;
2017 ProofEngine.goal := savedgoal ;
2018 refresh_sequent notebook ;
2019 refresh_proof output
2021 output_html outputhtml
2022 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2023 ProofEngine.proof := savedproof ;
2024 ProofEngine.goal := savedgoal ;
2027 output_html outputhtml
2028 ("<h1 color=\"red\">No term selected</h1>")
2031 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2032 let module L = LogicalOperations in
2033 let module G = Gdome in
2034 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2035 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2036 let savedproof = !ProofEngine.proof in
2037 let savedgoal = !ProofEngine.goal in
2038 match mmlwidget#get_selection with
2041 ((node : Gdome.element)#getAttributeNS
2042 ~namespaceURI:helmns
2043 ~localName:(G.domString "xref"))#to_string
2045 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2049 match !current_scratch_infos with
2050 (* term is the whole goal in the scratch_area *)
2051 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2053 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2054 let mml = mml_of_cic_term 111 expr in
2055 scratch_window#show () ;
2056 scratch_window#mmlwidget#load_tree ~dom:mml
2057 | None -> assert false (* "ERROR: No current term!!!" *)
2060 output_html outputhtml
2061 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2064 output_html outputhtml
2065 ("<h1 color=\"red\">No term selected</h1>")
2068 let call_tactic_with_hypothesis_input tactic () =
2069 let module L = LogicalOperations in
2070 let module G = Gdome in
2071 let notebook = (rendering_window ())#notebook in
2072 let output = ((rendering_window ())#output : GMathView.math_view) in
2073 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2074 let savedproof = !ProofEngine.proof in
2075 let savedgoal = !ProofEngine.goal in
2076 match notebook#proofw#get_selection with
2079 ((node : Gdome.element)#getAttributeNS
2080 ~namespaceURI:helmns
2081 ~localName:(G.domString "xref"))#to_string
2083 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2087 match !current_goal_infos with
2088 Some (_,_,ids_to_hypotheses) ->
2090 tactic (Hashtbl.find ids_to_hypotheses id) ;
2091 refresh_sequent notebook ;
2092 refresh_proof output
2093 | None -> assert false (* "ERROR: No current term!!!" *)
2095 RefreshSequentException e ->
2096 output_html outputhtml
2097 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2098 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2099 ProofEngine.proof := savedproof ;
2100 ProofEngine.goal := savedgoal ;
2101 refresh_sequent notebook
2102 | RefreshProofException e ->
2103 output_html outputhtml
2104 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2105 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2106 ProofEngine.proof := savedproof ;
2107 ProofEngine.goal := savedgoal ;
2108 refresh_sequent notebook ;
2109 refresh_proof output
2111 output_html outputhtml
2112 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2113 ProofEngine.proof := savedproof ;
2114 ProofEngine.goal := savedgoal ;
2117 output_html outputhtml
2118 ("<h1 color=\"red\">No term selected</h1>")
2122 let intros = call_tactic ProofEngine.intros;;
2123 let exact = call_tactic_with_input ProofEngine.exact;;
2124 let apply = call_tactic_with_input ProofEngine.apply;;
2125 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2126 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2127 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2128 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2129 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2130 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2131 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2132 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2133 let cut = call_tactic_with_input ProofEngine.cut;;
2134 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2135 let letin = call_tactic_with_input ProofEngine.letin;;
2136 let ring = call_tactic ProofEngine.ring;;
2137 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2138 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2139 let fourier = call_tactic ProofEngine.fourier;;
2140 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2141 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2142 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2143 let reflexivity = call_tactic ProofEngine.reflexivity;;
2144 let symmetry = call_tactic ProofEngine.symmetry;;
2145 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2146 let exists = call_tactic ProofEngine.exists;;
2147 let split = call_tactic ProofEngine.split;;
2148 let left = call_tactic ProofEngine.left;;
2149 let right = call_tactic ProofEngine.right;;
2150 let assumption = call_tactic ProofEngine.assumption;;
2151 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2152 let absurd = call_tactic_with_input ProofEngine.absurd;;
2153 let contradiction = call_tactic ProofEngine.contradiction;;
2154 let decompose = call_tactic_with_input ProofEngine.decompose;;
2156 let whd_in_scratch scratch_window =
2157 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2160 let reduce_in_scratch scratch_window =
2161 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2164 let simpl_in_scratch scratch_window =
2165 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2171 (**********************)
2172 (* END OF TACTICS *)
2173 (**********************)
2177 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2179 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2182 output_html outputhtml
2183 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2186 exception NotADefinition;;
2189 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2190 let output = ((rendering_window ())#output : GMathView.math_view) in
2191 let notebook = (rendering_window ())#notebook in
2193 let uri = input_or_locate_uri ~title:"Open" in
2194 CicTypeChecker.typecheck uri ;
2195 let metasenv,bo,ty =
2196 match CicEnvironment.get_cooked_obj uri with
2197 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2198 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2201 | Cic.InductiveDefinition _ -> raise NotADefinition
2203 ProofEngine.proof :=
2204 Some (uri, metasenv, bo, ty) ;
2205 ProofEngine.goal := None ;
2206 refresh_sequent notebook ;
2207 refresh_proof output
2209 RefreshSequentException e ->
2210 output_html outputhtml
2211 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2212 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2213 | RefreshProofException e ->
2214 output_html outputhtml
2215 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2216 "proof: " ^ Printexc.to_string e ^ "</h1>")
2218 output_html outputhtml
2219 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2222 let show_query_results results =
2225 ~modal:false ~title:"Query results." ~border_width:2 () in
2226 let vbox = GPack.vbox ~packing:window#add () in
2228 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2231 ~text:"Click on a URI to show that object"
2232 ~packing:hbox#add () in
2233 let scrolled_window =
2234 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2235 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2236 let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2239 (function (uri,_) ->
2243 clist#set_row ~selectable:false n
2246 clist#columns_autosize () ;
2248 (clist#connect#select_row
2249 (fun ~row ~column ~event ->
2250 let (uristr,_) = List.nth results row in
2252 Disambiguate.cic_textual_parser_uri_of_string
2253 (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
2256 CicTextualParser0.ConUri uri
2257 | CicTextualParser0.VarUri uri
2258 | CicTextualParser0.IndTyUri (uri,_)
2259 | CicTextualParser0.IndConUri (uri,_,_) ->
2260 show_in_show_window_uri uri
2266 let refine_constraints (must_obj,must_rel,must_sort) =
2267 let chosen = ref false in
2268 let use_only = ref false in
2271 ~modal:true ~title:"Constraints refinement."
2272 ~width:800 ~border_width:2 () in
2273 let vbox = GPack.vbox ~packing:window#add () in
2275 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2278 ~text: "\"Only\" constraints can be enforced or not."
2279 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2281 GButton.toggle_button ~label:"Enforce \"only\" constraints"
2282 ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2285 (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2286 (* Notebook for the constraints choice *)
2288 GPack.notebook ~scrollable:true
2289 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2290 (* Rel constraints *)
2293 ~text: "Constraints on Rels" () in
2295 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2298 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2301 ~text: "You can now specify the constraints on Rels."
2302 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2303 let expected_height = 25 * (List.length must_rel + 2) in
2304 let height = if expected_height > 400 then 400 else expected_height in
2305 let scrolled_window =
2306 GBin.scrolled_window ~border_width:10 ~height ~width:600
2307 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2308 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2309 let rel_constraints =
2311 (function (position,depth) ->
2314 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2318 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2320 None -> position, ref None
2322 let mutable_ref = ref (Some depth') in
2324 GButton.toggle_button
2325 ~label:("depth = " ^ string_of_int depth') ~active:true
2326 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2329 (depthb#connect#toggled
2331 let sel_depth = if depthb#active then Some depth' else None in
2332 mutable_ref := sel_depth
2334 position, mutable_ref
2336 (* Sort constraints *)
2339 ~text: "Constraints on Sorts" () in
2341 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2344 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2347 ~text: "You can now specify the constraints on Sorts."
2348 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2349 let expected_height = 25 * (List.length must_sort + 2) in
2350 let height = if expected_height > 400 then 400 else expected_height in
2351 let scrolled_window =
2352 GBin.scrolled_window ~border_width:10 ~height ~width:600
2353 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2354 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2355 let sort_constraints =
2357 (function (position,depth,sort) ->
2360 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2363 ~text:(sort ^ " " ^ position)
2364 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2366 None -> position, ref None, sort
2368 let mutable_ref = ref (Some depth') in
2370 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2372 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2375 (depthb#connect#toggled
2377 let sel_depth = if depthb#active then Some depth' else None in
2378 mutable_ref := sel_depth
2380 position, mutable_ref, sort
2382 (* Obj constraints *)
2385 ~text: "Constraints on constants" () in
2387 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2390 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2393 ~text: "You can now specify the constraints on constants."
2394 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2395 let expected_height = 25 * (List.length must_obj + 2) in
2396 let height = if expected_height > 400 then 400 else expected_height in
2397 let scrolled_window =
2398 GBin.scrolled_window ~border_width:10 ~height ~width:600
2399 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2400 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2401 let obj_constraints =
2403 (function (uri,position,depth) ->
2406 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2409 ~text:(uri ^ " " ^ position)
2410 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2412 None -> uri, position, ref None
2414 let mutable_ref = ref (Some depth') in
2416 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2418 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2421 (depthb#connect#toggled
2423 let sel_depth = if depthb#active then Some depth' else None in
2424 mutable_ref := sel_depth
2426 uri, position, mutable_ref
2428 (* Confirm/abort buttons *)
2430 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2432 GButton.button ~label:"Ok"
2433 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2435 GButton.button ~label:"Abort"
2436 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2438 ignore (window#connect#destroy GMain.Main.quit) ;
2439 ignore (cancelb#connect#clicked window#destroy) ;
2441 (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2442 window#set_position `CENTER ;
2444 GMain.Main.main () ;
2446 let chosen_must_rel =
2448 (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2449 let chosen_must_sort =
2451 (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2454 let chosen_must_obj =
2456 (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2459 (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2461 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2462 Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2470 let completeSearchPattern () =
2471 let inputt = ((rendering_window ())#inputt : term_editor) in
2472 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2474 let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2475 let must = MQueryLevels2.get_constraints expr in
2476 let must',only = refine_constraints must in
2477 let results = MQueryGenerator.searchPattern must' only in
2478 show_query_results results
2481 output_html outputhtml
2482 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2485 let insertQuery () =
2486 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2488 let chosen = ref None in
2491 ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2492 let vbox = GPack.vbox ~packing:window#add () in
2494 GMisc.label ~text:"Insert Query. For Experts Only."
2495 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2496 let scrolled_window =
2497 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2498 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2499 let input = GEdit.text ~editable:true
2500 ~packing:scrolled_window#add () in
2502 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2504 GButton.button ~label:"Ok"
2505 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2507 GButton.button ~label:"Load from file..."
2508 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2510 GButton.button ~label:"Abort"
2511 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2512 ignore (window#connect#destroy GMain.Main.quit) ;
2513 ignore (cancelb#connect#clicked window#destroy) ;
2515 (okb#connect#clicked
2517 chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2519 (loadb#connect#clicked
2522 GToolbox.select_file ~title:"Select Query File" ()
2526 let inch = open_in filename in
2527 let rec read_file () =
2529 let line = input_line inch in
2530 line ^ "\n" ^ read_file ()
2534 let text = read_file () in
2535 input#delete_text 0 input#length ;
2536 ignore (input#insert_text text ~pos:0))) ;
2537 window#set_position `CENTER ;
2539 GMain.Main.main () ;
2544 Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2546 show_query_results results
2549 output_html outputhtml
2550 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2553 let choose_must list_of_must only =
2554 let chosen = ref None in
2555 let user_constraints = ref [] in
2558 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2559 let vbox = GPack.vbox ~packing:window#add () in
2561 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2565 ("You can now specify the genericity of the query. " ^
2566 "The more generic the slower.")
2567 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2569 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2573 "Suggestion: start with faster queries before moving to more generic ones."
2574 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2576 GPack.notebook ~scrollable:true
2577 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2580 let last = List.length list_of_must in
2586 (if !page = 1 then "More generic" else
2587 if !page = last then "More precise" else " ") () in
2588 let expected_height = 25 * (List.length must + 2) in
2589 let height = if expected_height > 400 then 400 else expected_height in
2590 let scrolled_window =
2591 GBin.scrolled_window ~border_width:10 ~height ~width:600
2592 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2594 GList.clist ~columns:2 ~packing:scrolled_window#add
2595 ~titles:["URI" ; "Position"] ()
2599 (function (uri,position) ->
2602 [uri; if position then "MainConclusion" else "Conclusion"]
2604 clist#set_row ~selectable:false n
2607 clist#columns_autosize ()
2610 let label = GMisc.label ~text:"User provided" () in
2612 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2614 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2617 ~text:"Select the constraints that must be satisfied and press OK."
2618 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2619 let expected_height = 25 * (List.length only + 2) in
2620 let height = if expected_height > 400 then 400 else expected_height in
2621 let scrolled_window =
2622 GBin.scrolled_window ~border_width:10 ~height ~width:600
2623 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2625 GList.clist ~columns:2 ~packing:scrolled_window#add
2626 ~selection_mode:`EXTENDED
2627 ~titles:["URI" ; "Position"] ()
2631 (function (uri,position) ->
2634 [uri; if position then "MainConclusion" else "Conclusion"]
2636 clist#set_row ~selectable:true n
2639 clist#columns_autosize () ;
2641 (clist#connect#select_row
2642 (fun ~row ~column ~event ->
2643 user_constraints := (List.nth only row)::!user_constraints)) ;
2645 (clist#connect#unselect_row
2646 (fun ~row ~column ~event ->
2649 (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2652 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2654 GButton.button ~label:"Ok"
2655 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2657 GButton.button ~label:"Abort"
2658 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2660 ignore (window#connect#destroy GMain.Main.quit) ;
2661 ignore (cancelb#connect#clicked window#destroy) ;
2663 (okb#connect#clicked
2664 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2665 window#set_position `CENTER ;
2667 GMain.Main.main () ;
2669 None -> raise NoChoice
2671 if n = List.length list_of_must then
2672 (* user provided constraints *)
2675 List.nth list_of_must n
2678 let searchPattern () =
2679 let inputt = ((rendering_window ())#inputt : term_editor) in
2680 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2683 match !ProofEngine.proof with
2684 None -> assert false
2685 | Some (_,metasenv,_,_) -> metasenv
2687 match !ProofEngine.goal with
2690 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2691 let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2692 let must = choose_must list_of_must only in
2693 let torigth_restriction (u,b) =
2696 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2698 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2702 let rigth_must = List.map torigth_restriction must in
2703 let rigth_only = Some (List.map torigth_restriction only) in
2705 MQueryGenerator.searchPattern
2706 (rigth_must,[],[]) (rigth_only,None,None) in
2710 Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
2713 " <h1>Backward Query: </h1>" ^
2714 " <pre>" ^ get_last_query result ^ "</pre>"
2716 output_html outputhtml html ;
2718 let rec filter_out =
2722 let tl',exc = filter_out tl in
2725 ProofEngine.can_apply
2726 (term_of_cic_textual_parser_uri
2727 (Disambiguate.cic_textual_parser_uri_of_string uri))
2735 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2736 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2743 " <h1>Objects that can actually be applied: </h1> " ^
2744 String.concat "<br>" uris' ^ exc ^
2745 " <h1>Number of false matches: " ^
2746 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2747 " <h1>Number of good matches: " ^
2748 string_of_int (List.length uris') ^ "</h1>"
2750 output_html outputhtml html' ;
2752 user_uri_choice ~title:"Ambiguous input."
2754 "Many lemmas can be successfully applied. Please, choose one:"
2757 inputt#set_term uri' ;
2761 output_html outputhtml
2762 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2765 let choose_selection
2766 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2768 let module G = Gdome in
2769 let rec aux element =
2770 if element#hasAttributeNS
2771 ~namespaceURI:helmns
2772 ~localName:(G.domString "xref")
2774 mmlwidget#set_selection (Some element)
2776 match element#get_parentNode with
2777 None -> assert false
2778 (*CSC: OCAML DIVERGES!
2779 | Some p -> aux (new G.element_of_node p)
2781 | Some p -> aux (new Gdome.element_of_node p)
2785 | None -> mmlwidget#set_selection None
2788 (* STUFF TO BUILD THE GTK INTERFACE *)
2790 (* Stuff for the widget settings *)
2792 let export_to_postscript (output : GMathView.math_view) =
2793 let lastdir = ref (Unix.getcwd ()) in
2796 GToolbox.select_file ~title:"Export to PostScript"
2797 ~dir:lastdir ~filename:"screenshot.ps" ()
2801 output#export_to_postscript ~filename:filename ();
2804 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2805 button_set_kerning button_set_transparency export_to_postscript_menu_item
2808 let is_set = button_t1#active in
2809 output#set_font_manager_type
2810 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2813 button_set_anti_aliasing#misc#set_sensitive true ;
2814 button_set_kerning#misc#set_sensitive true ;
2815 button_set_transparency#misc#set_sensitive true ;
2816 export_to_postscript_menu_item#misc#set_sensitive true ;
2820 button_set_anti_aliasing#misc#set_sensitive false ;
2821 button_set_kerning#misc#set_sensitive false ;
2822 button_set_transparency#misc#set_sensitive false ;
2823 export_to_postscript_menu_item#misc#set_sensitive false ;
2827 let set_anti_aliasing output button_set_anti_aliasing () =
2828 output#set_anti_aliasing button_set_anti_aliasing#active
2831 let set_kerning output button_set_kerning () =
2832 output#set_kerning button_set_kerning#active
2835 let set_transparency output button_set_transparency () =
2836 output#set_transparency button_set_transparency#active
2839 let changefont output font_size_spinb () =
2840 output#set_font_size font_size_spinb#value_as_int
2843 let set_log_verbosity output log_verbosity_spinb () =
2844 output#set_log_verbosity log_verbosity_spinb#value_as_int
2847 class settings_window (output : GMathView.math_view) sw
2848 export_to_postscript_menu_item selection_changed_callback
2850 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2852 GPack.vbox ~packing:settings_window#add () in
2855 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2856 ~border_width:5 ~packing:vbox#add () in
2858 GButton.toggle_button ~label:"activate t1 fonts"
2859 ~packing:(table#attach ~left:0 ~top:0) () in
2860 let button_set_anti_aliasing =
2861 GButton.toggle_button ~label:"set_anti_aliasing"
2862 ~packing:(table#attach ~left:0 ~top:1) () in
2863 let button_set_kerning =
2864 GButton.toggle_button ~label:"set_kerning"
2865 ~packing:(table#attach ~left:1 ~top:1) () in
2866 let button_set_transparency =
2867 GButton.toggle_button ~label:"set_transparency"
2868 ~packing:(table#attach ~left:2 ~top:1) () in
2871 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2872 ~border_width:5 ~packing:vbox#add () in
2873 let font_size_label =
2874 GMisc.label ~text:"font size:"
2875 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2876 let font_size_spinb =
2878 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2881 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2882 let log_verbosity_label =
2883 GMisc.label ~text:"log verbosity:"
2884 ~packing:(table#attach ~left:0 ~top:1) () in
2885 let log_verbosity_spinb =
2887 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2890 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2892 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2894 GButton.button ~label:"Close"
2895 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2897 method show = settings_window#show
2899 button_set_anti_aliasing#misc#set_sensitive false ;
2900 button_set_kerning#misc#set_sensitive false ;
2901 button_set_transparency#misc#set_sensitive false ;
2902 (* Signals connection *)
2903 ignore(button_t1#connect#clicked
2904 (activate_t1 output button_set_anti_aliasing button_set_kerning
2905 button_set_transparency export_to_postscript_menu_item button_t1)) ;
2906 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2907 ignore(button_set_anti_aliasing#connect#toggled
2908 (set_anti_aliasing output button_set_anti_aliasing));
2909 ignore(button_set_kerning#connect#toggled
2910 (set_kerning output button_set_kerning)) ;
2911 ignore(button_set_transparency#connect#toggled
2912 (set_transparency output button_set_transparency)) ;
2913 ignore(log_verbosity_spinb#connect#changed
2914 (set_log_verbosity output log_verbosity_spinb)) ;
2915 ignore(closeb#connect#clicked settings_window#misc#hide)
2918 (* Scratch window *)
2920 class scratch_window =
2922 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2924 GPack.vbox ~packing:window#add () in
2926 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2928 GButton.button ~label:"Whd"
2929 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2931 GButton.button ~label:"Reduce"
2932 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2934 GButton.button ~label:"Simpl"
2935 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2936 let scrolled_window =
2937 GBin.scrolled_window ~border_width:10
2938 ~packing:(vbox#pack ~expand:true ~padding:5) () in
2941 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2943 method mmlwidget = mmlwidget
2944 method show () = window#misc#hide () ; window#show ()
2946 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2947 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2948 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2949 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2950 ignore(simplb#connect#clicked (simpl_in_scratch self))
2954 let vbox1 = GPack.vbox () in
2956 val mutable proofw_ref = None
2957 val mutable compute_ref = None
2959 Lazy.force self#compute ;
2960 match proofw_ref with
2961 None -> assert false
2962 | Some proofw -> proofw
2963 method content = vbox1
2965 match compute_ref with
2966 None -> assert false
2967 | Some compute -> compute
2971 let scrolled_window1 =
2972 GBin.scrolled_window ~border_width:10
2973 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2975 GMathView.math_view ~width:400 ~height:275
2976 ~packing:(scrolled_window1#add) () in
2977 let _ = proofw_ref <- Some proofw in
2979 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2981 GButton.button ~label:"Exact"
2982 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2984 GButton.button ~label:"Intros"
2985 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2987 GButton.button ~label:"Apply"
2988 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2989 let elimintrossimplb =
2990 GButton.button ~label:"ElimIntrosSimpl"
2991 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2993 GButton.button ~label:"ElimType"
2994 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2996 GButton.button ~label:"Whd"
2997 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2999 GButton.button ~label:"Reduce"
3000 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3002 GButton.button ~label:"Simpl"
3003 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3005 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3007 GButton.button ~label:"Fold_whd"
3008 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3010 GButton.button ~label:"Fold_reduce"
3011 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3013 GButton.button ~label:"Fold_simpl"
3014 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3016 GButton.button ~label:"Cut"
3017 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3019 GButton.button ~label:"Change"
3020 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3022 GButton.button ~label:"Let ... In"
3023 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3025 GButton.button ~label:"Ring"
3026 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3028 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3030 GButton.button ~label:"ClearBody"
3031 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3033 GButton.button ~label:"Clear"
3034 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3036 GButton.button ~label:"Fourier"
3037 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3039 GButton.button ~label:"RewriteSimpl ->"
3040 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3041 let rewritebacksimplb =
3042 GButton.button ~label:"RewriteSimpl <-"
3043 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3045 GButton.button ~label:"Replace"
3046 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3048 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3050 GButton.button ~label:"Reflexivity"
3051 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3053 GButton.button ~label:"Symmetry"
3054 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3056 GButton.button ~label:"Transitivity"
3057 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3059 GButton.button ~label:"Exists"
3060 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3062 GButton.button ~label:"Split"
3063 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3065 GButton.button ~label:"Left"
3066 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3068 GButton.button ~label:"Right"
3069 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3071 GButton.button ~label:"Assumption"
3072 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3074 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3076 GButton.button ~label:"Generalize"
3077 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3079 GButton.button ~label:"Absurd"
3080 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3081 let contradictionb =
3082 GButton.button ~label:"Contradiction"
3083 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3084 let searchpatternb =
3085 GButton.button ~label:"SearchPattern_Apply"
3086 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3088 GButton.button ~label:"Decompose"
3089 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3091 ignore(exactb#connect#clicked exact) ;
3092 ignore(applyb#connect#clicked apply) ;
3093 ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3094 ignore(elimtypeb#connect#clicked elimtype) ;
3095 ignore(whdb#connect#clicked whd) ;
3096 ignore(reduceb#connect#clicked reduce) ;
3097 ignore(simplb#connect#clicked simpl) ;
3098 ignore(foldwhdb#connect#clicked fold_whd) ;
3099 ignore(foldreduceb#connect#clicked fold_reduce) ;
3100 ignore(foldsimplb#connect#clicked fold_simpl) ;
3101 ignore(cutb#connect#clicked cut) ;
3102 ignore(changeb#connect#clicked change) ;
3103 ignore(letinb#connect#clicked letin) ;
3104 ignore(ringb#connect#clicked ring) ;
3105 ignore(clearbodyb#connect#clicked clearbody) ;
3106 ignore(clearb#connect#clicked clear) ;
3107 ignore(fourierb#connect#clicked fourier) ;
3108 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3109 ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3110 ignore(replaceb#connect#clicked replace) ;
3111 ignore(reflexivityb#connect#clicked reflexivity) ;
3112 ignore(symmetryb#connect#clicked symmetry) ;
3113 ignore(transitivityb#connect#clicked transitivity) ;
3114 ignore(existsb#connect#clicked exists) ;
3115 ignore(splitb#connect#clicked split) ;
3116 ignore(leftb#connect#clicked left) ;
3117 ignore(rightb#connect#clicked right) ;
3118 ignore(assumptionb#connect#clicked assumption) ;
3119 ignore(generalizeb#connect#clicked generalize) ;
3120 ignore(absurdb#connect#clicked absurd) ;
3121 ignore(contradictionb#connect#clicked contradiction) ;
3122 ignore(introsb#connect#clicked intros) ;
3123 ignore(searchpatternb#connect#clicked searchPattern) ;
3124 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3125 ignore(decomposeb#connect#clicked decompose) ;
3131 let vbox1 = GPack.vbox () in
3132 let scrolled_window1 =
3133 GBin.scrolled_window ~border_width:10
3134 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3136 GMathView.math_view ~width:400 ~height:275
3137 ~packing:(scrolled_window1#add) () in
3139 method proofw = (assert false : GMathView.math_view)
3140 method content = vbox1
3141 method compute = (assert false : unit)
3145 let empty_page = new empty_page;;
3149 val notebook = GPack.notebook ()
3151 val mutable skip_switch_page_event = false
3152 val mutable empty = true
3153 method notebook = notebook
3155 let new_page = new page () in
3157 pages := !pages @ [n,lazy (setgoal n),new_page] ;
3158 notebook#append_page
3159 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3160 new_page#content#coerce
3161 method remove_all_pages ~skip_switch_page_event:skip =
3163 notebook#remove_page 0 (* let's remove the empty page *)
3165 List.iter (function _ -> notebook#remove_page 0) !pages ;
3167 skip_switch_page_event <- skip
3168 method set_current_page ~may_skip_switch_page_event n =
3169 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3170 let new_page = notebook#page_num page#content#coerce in
3171 if may_skip_switch_page_event && new_page <> notebook#current_page then
3172 skip_switch_page_event <- true ;
3173 notebook#goto_page new_page
3174 method set_empty_page =
3177 notebook#append_page
3178 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3179 empty_page#content#coerce
3181 let (_,_,page) = List.nth !pages notebook#current_page in
3185 (notebook#connect#switch_page
3187 let skip = skip_switch_page_event in
3188 skip_switch_page_event <- false ;
3191 let (metano,setgoal,page) = List.nth !pages i in
3192 ProofEngine.goal := Some metano ;
3193 Lazy.force (page#compute) ;
3202 class rendering_window output (notebook : notebook) =
3203 let scratch_window = new scratch_window in
3205 GWindow.window ~title:"MathML viewer" ~border_width:0
3206 ~allow_shrink:false () in
3207 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3209 let handle_box = GBin.handle_box ~border_width:2
3210 ~packing:(vbox_for_menu#pack ~padding:0) () in
3211 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3212 let factory0 = new GMenu.factory menubar in
3213 let accel_group = factory0#accel_group in
3215 let file_menu = factory0#add_submenu "File" in
3216 let factory1 = new GMenu.factory file_menu ~accel_group in
3217 let export_to_postscript_menu_item =
3220 factory1#add_item "New Block of (Co)Inductive Definitions..."
3221 ~key:GdkKeysyms._B ~callback:new_inductive
3224 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3227 let reopen_menu_item =
3228 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3232 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3233 ignore (factory1#add_separator ()) ;
3235 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3237 let save_menu_item =
3238 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3241 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3242 ignore (!save_set_sensitive false);
3243 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3244 ignore (!qed_set_sensitive false);
3245 ignore (factory1#add_separator ()) ;
3246 let export_to_postscript_menu_item =
3247 factory1#add_item "Export to PostScript..."
3248 ~callback:(export_to_postscript output) in
3249 ignore (factory1#add_separator ()) ;
3251 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3252 export_to_postscript_menu_item
3255 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3256 let factory2 = new GMenu.factory edit_menu ~accel_group in
3257 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3258 let proveit_menu_item =
3259 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3260 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3262 let focus_menu_item =
3263 factory2#add_item "Focus" ~key:GdkKeysyms._F
3264 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3267 focus_and_proveit_set_sensitive :=
3269 proveit_menu_item#misc#set_sensitive b ;
3270 focus_menu_item#misc#set_sensitive b
3272 let _ = !focus_and_proveit_set_sensitive false in
3273 (* edit term menu *)
3274 let edit_term_menu = factory0#add_submenu "Edit Term" in
3275 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3276 let check_menu_item =
3277 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3278 ~callback:(check scratch_window) in
3279 let _ = check_menu_item#misc#set_sensitive false in
3281 let settings_menu = factory0#add_submenu "Search" in
3282 let factory4 = new GMenu.factory settings_menu ~accel_group in
3284 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3286 let searchPattern_menu_item =
3287 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3288 ~callback:completeSearchPattern in
3289 let _ = searchPattern_menu_item#misc#set_sensitive false in
3290 let show_menu_item =
3291 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3293 let insert_query_item =
3294 factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3295 ~callback:insertQuery in
3297 let settings_menu = factory0#add_submenu "Settings" in
3298 let factory3 = new GMenu.factory settings_menu ~accel_group in
3300 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3301 ~callback:edit_aliases in
3302 let _ = factory3#add_separator () in
3304 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3305 ~callback:(function _ -> (settings_window ())#show ()) in
3307 let _ = window#add_accel_group accel_group in
3311 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3313 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3314 let scrolled_window0 =
3315 GBin.scrolled_window ~border_width:10
3316 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3317 let _ = scrolled_window0#add output#coerce in
3319 GBin.frame ~label:"Insert Term"
3320 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3321 let scrolled_window1 =
3322 GBin.scrolled_window ~border_width:5
3323 ~packing:frame#add () in
3325 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3326 ~isnotempty_callback:
3328 check_menu_item#misc#set_sensitive b ;
3329 searchPattern_menu_item#misc#set_sensitive b) in
3331 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3333 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3335 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3339 ~source:"<html><body bgColor=\"white\"></body></html>"
3340 ~width:400 ~height: 100
3345 method outputhtml = outputhtml
3346 method inputt = inputt
3347 method output = (output : GMathView.math_view)
3348 method notebook = notebook
3349 method show = window#show
3351 notebook#set_empty_page ;
3352 export_to_postscript_menu_item#misc#set_sensitive false ;
3353 check_term := (check_term_in_scratch scratch_window) ;
3355 (* signal handlers here *)
3356 ignore(output#connect#selection_changed
3358 choose_selection output elem ;
3359 !focus_and_proveit_set_sensitive true
3361 ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3362 let settings_window = new settings_window output scrolled_window0
3363 export_to_postscript_menu_item (choose_selection output) in
3364 set_settings_window settings_window ;
3365 set_outputhtml outputhtml ;
3366 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3367 Logger.log_callback :=
3368 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3373 let initialize_everything () =
3374 let module U = Unix in
3375 let output = GMathView.math_view ~width:350 ~height:280 () in
3376 let notebook = new notebook in
3377 let rendering_window' = new rendering_window output notebook in
3378 set_rendering_window rendering_window' ;
3379 mml_of_cic_term_ref := mml_of_cic_term ;
3380 rendering_window'#show () ;
3387 Mqint.set_database Mqint.postgres_db ;
3388 Mqint.init postgresqlconnectionstring ;
3390 ignore (GtkMain.Main.init ()) ;
3391 initialize_everything () ;
3392 if !usedb then Mqint.close ();