1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
40 let index_sharp = String.index uri '#' in
41 let index_rest = index_sharp + 10 in
42 let baseuri = String.sub uri 0 index_sharp in
43 let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
48 (* GLOBAL CONSTANTS *)
50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
51 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
55 " <body bgColor=\"white\">"
65 Sys.getenv "GTOPLEVEL_PROOFFILE"
67 Not_found -> "/public/currentproof"
72 Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
74 Not_found -> "/public/currentprooftype"
77 (*CSC: the getter should handle the innertypes, not the FS *)
81 Sys.getenv "GTOPLEVEL_INNERTYPESFILE"
83 Not_found -> "/public/innertypes"
86 let constanttypefile =
88 Sys.getenv "GTOPLEVEL_CONSTANTTYPEFILE"
90 Not_found -> "/public/constanttype"
93 let postgresqlconnectionstring =
95 Sys.getenv "POSTGRESQL_CONNECTION_STRING"
97 Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
100 let empty_id_to_uris = ([],function _ -> None);;
103 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
105 let htmlheader_and_content = ref htmlheader;;
107 let current_cic_infos = ref None;;
108 let current_goal_infos = ref None;;
109 let current_scratch_infos = ref None;;
111 let id_to_uris = ref empty_id_to_uris;;
113 let check_term = ref (fun _ _ _ -> assert false);;
114 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
116 exception RenderingWindowsNotInitialized;;
118 let set_rendering_window,rendering_window =
119 let rendering_window_ref = ref None in
120 (function rw -> rendering_window_ref := Some rw),
122 match !rendering_window_ref with
123 None -> raise RenderingWindowsNotInitialized
128 exception SettingsWindowsNotInitialized;;
130 let set_settings_window,settings_window =
131 let settings_window_ref = ref None in
132 (function rw -> settings_window_ref := Some rw),
134 match !settings_window_ref with
135 None -> raise SettingsWindowsNotInitialized
140 exception OutputHtmlNotInitialized;;
142 let set_outputhtml,outputhtml =
143 let outputhtml_ref = ref None in
144 (function rw -> outputhtml_ref := Some rw),
146 match !outputhtml_ref with
147 None -> raise OutputHtmlNotInitialized
148 | Some outputhtml -> outputhtml
152 exception QedSetSensitiveNotInitialized;;
153 let qed_set_sensitive =
154 ref (function _ -> raise QedSetSensitiveNotInitialized)
157 exception SaveSetSensitiveNotInitialized;;
158 let save_set_sensitive =
159 ref (function _ -> raise SaveSetSensitiveNotInitialized)
162 (* COMMAND LINE OPTIONS *)
168 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
171 Arg.parse argspec ignore ""
173 (* A WIDGET TO ENTER CIC TERMS *)
175 class term_editor ?packing ?width ?height ?isnotempty_callback () =
176 let input = GEdit.text ~editable:true ?width ?height ?packing () in
178 match isnotempty_callback with
181 ignore(input#connect#changed (function () -> callback (input#length > 0)))
184 method coerce = input#coerce
186 input#delete_text 0 input#length
187 (* CSC: txt is now a string, but should be of type Cic.term *)
188 method set_term txt =
190 ignore ((input#insert_text txt) ~pos:0)
191 (* CSC: this method should disappear *)
192 method get_as_string =
193 input#get_chars 0 input#length
194 method get_term ~context ~metasenv =
195 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
196 CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
202 exception IllFormedUri of string;;
204 let cic_textual_parser_uri_of_string uri' =
207 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
208 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
210 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
211 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
215 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
216 CicTextualParser0.IndTyUri (uri'',typeno)
219 (* Constructor of an Inductive Type *)
220 let uri'',typeno,consno =
221 CicTextualLexer.indconuri_of_uri uri'
223 CicTextualParser0.IndConUri (uri'',typeno,consno)
226 _ -> raise (IllFormedUri uri')
229 let term_of_cic_textual_parser_uri uri =
230 let module C = Cic in
231 let module CTP = CicTextualParser0 in
233 CTP.ConUri uri -> C.Const (uri,[])
234 | CTP.VarUri uri -> C.Var (uri,[])
235 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
236 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
239 let string_of_cic_textual_parser_uri uri =
240 let module C = Cic in
241 let module CTP = CicTextualParser0 in
244 CTP.ConUri uri -> UriManager.string_of_uri uri
245 | CTP.VarUri uri -> UriManager.string_of_uri uri
246 | CTP.IndTyUri (uri,tyno) ->
247 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
248 | CTP.IndConUri (uri,tyno,consno) ->
249 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
252 (* 4 = String.length "cic:" *)
253 String.sub uri' 4 (String.length uri' - 4)
256 let output_html outputhtml msg =
257 htmlheader_and_content := !htmlheader_and_content ^ msg ;
258 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
259 outputhtml#set_topline (-1)
262 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
266 let check_window outputhtml uris =
269 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
271 GPack.notebook ~scrollable:true ~packing:window#add () in
276 let scrolled_window =
277 GBin.scrolled_window ~border_width:10
279 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
285 ~packing:scrolled_window#add ~width:400 ~height:280 () in
288 term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
290 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
293 let mml = !mml_of_cic_term_ref 111 expr in
294 prerr_endline ("### " ^ CicPp.ppterm expr) ;
295 mmlwidget#load_tree ~dom:mml
298 output_html outputhtml
299 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
304 (notebook#connect#switch_page
305 (function i -> Lazy.force (List.nth render_terms i)))
311 interactive_user_uri_choice ~selection_mode ?(ok="Ok")
312 ?(enable_button_for_non_vars=false) ~title ~msg uris
314 let choices = ref [] in
315 let chosen = ref false in
316 let use_only_constants = ref false in
318 GWindow.dialog ~modal:true ~title ~width:600 () in
320 GMisc.label ~text:msg
321 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
322 let scrolled_window =
323 GBin.scrolled_window ~border_width:10
324 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
326 let expected_height = 18 * List.length uris in
327 let height = if expected_height > 400 then 400 else expected_height in
328 GList.clist ~columns:1 ~packing:scrolled_window#add
329 ~height ~selection_mode () in
330 let _ = List.map (function x -> clist#append [x]) uris in
332 GPack.hbox ~border_width:0
333 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
335 GMisc.label ~text:"None of the above. Try this one:"
336 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
338 GEdit.entry ~editable:true
339 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
341 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
343 GButton.button ~label:ok
344 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
345 let _ = okb#misc#set_sensitive false in
350 if enable_button_for_non_vars then
351 hbox#pack ~expand:false ~fill:false ~padding:5 w)
352 ~label:"Try constants only" () in
354 GButton.button ~label:"Check"
355 ~packing:(hbox#pack ~padding:5) () in
356 let _ = checkb#misc#set_sensitive false in
358 GButton.button ~label:"Abort"
359 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
361 let check_callback () =
362 assert (List.length !choices > 0) ;
363 check_window (outputhtml ()) !choices
365 ignore (window#connect#destroy GMain.Main.quit) ;
366 ignore (cancelb#connect#clicked window#destroy) ;
368 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
370 (nonvarsb#connect#clicked
372 use_only_constants := true ;
376 ignore (checkb#connect#clicked check_callback) ;
378 (clist#connect#select_row
379 (fun ~row ~column ~event ->
380 checkb#misc#set_sensitive true ;
381 okb#misc#set_sensitive true ;
382 choices := (List.nth uris row)::!choices)) ;
384 (clist#connect#unselect_row
385 (fun ~row ~column ~event ->
387 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
389 (manual_input#connect#changed
391 if manual_input#text = "" then
394 checkb#misc#set_sensitive false ;
395 okb#misc#set_sensitive false ;
396 clist#misc#set_sensitive true
400 choices := [manual_input#text] ;
401 clist#unselect_all () ;
402 checkb#misc#set_sensitive true ;
403 okb#misc#set_sensitive true ;
404 clist#misc#set_sensitive false
406 window#set_position `CENTER ;
410 if !use_only_constants then
412 (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
415 if List.length !choices > 0 then !choices else raise NoChoice
420 let interactive_interpretation_choice interpretations =
421 let chosen = ref None in
424 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
425 let vbox = GPack.vbox ~packing:window#add () in
429 ("Ambiguous input since there are many well-typed interpretations." ^
430 " Please, choose one of them.")
431 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
433 GPack.notebook ~scrollable:true
434 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
437 (function interpretation ->
439 let expected_height = 18 * List.length interpretation in
440 let height = if expected_height > 400 then 400 else expected_height in
441 GList.clist ~columns:2 ~packing:notebook#append_page ~height
442 ~titles:["id" ; "URI"] ()
446 (function (id,uri) ->
447 let n = clist#append [id;uri] in
448 clist#set_row ~selectable:false n
451 clist#columns_autosize ()
454 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
456 GButton.button ~label:"Ok"
457 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
459 GButton.button ~label:"Abort"
460 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
462 ignore (window#connect#destroy GMain.Main.quit) ;
463 ignore (cancelb#connect#clicked window#destroy) ;
466 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
467 window#set_position `CENTER ;
471 None -> raise NoChoice
478 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
480 let query = ref "" in
481 MQueryGenerator.set_confirm_query
482 (function q -> query := MQueryUtil.text_of_query q ; true) ;
483 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
486 let domImpl = Gdome.domImplementation ();;
488 let parseStyle name =
490 domImpl#createDocumentFromURI
492 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
494 ~uri:("styles/" ^ name) ()
496 Gdome_xslt.processStylesheet style
499 let d_c = parseStyle "drop_coercions.xsl";;
500 let tc1 = parseStyle "objtheorycontent.xsl";;
501 let hc2 = parseStyle "content_to_html.xsl";;
502 let l = parseStyle "link.xsl";;
504 let c1 = parseStyle "rootcontent.xsl";;
505 let g = parseStyle "genmmlid.xsl";;
506 let c2 = parseStyle "annotatedpres.xsl";;
509 let getterURL = Configuration.getter_url;;
510 let processorURL = Configuration.processor_url;;
512 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
513 let mml_args ~explode_all =
514 ("explodeall",(if explode_all then "true()" else "false()"))::
515 ["processorURL", "'" ^ processorURL ^ "'" ;
516 "getterURL", "'" ^ getterURL ^ "'" ;
517 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
518 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
519 "UNICODEvsSYMBOL", "'symbol'" ;
520 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
521 "encoding", "'iso-8859-1'" ;
522 "media-type", "'text/html'" ;
523 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
524 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
525 "naturalLanguage", "'yes'" ;
526 "annotations", "'no'" ;
527 "URLs_or_URIs", "'URIs'" ;
528 "topurl", "'http://phd.cs.unibo.it/helm'" ;
529 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
532 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
534 ["processorURL", "'" ^ processorURL ^ "'" ;
535 "getterURL", "'" ^ getterURL ^ "'" ;
536 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
537 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
538 "UNICODEvsSYMBOL", "'symbol'" ;
539 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
540 "encoding", "'iso-8859-1'" ;
541 "media-type", "'text/html'" ;
542 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
543 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
544 "naturalLanguage", "'no'" ;
545 "annotations", "'no'" ;
546 "explodeall", "true()" ;
547 "URLs_or_URIs", "'URIs'" ;
548 "topurl", "'http://phd.cs.unibo.it/helm'" ;
549 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
552 let parse_file filename =
553 let inch = open_in filename in
554 let rec read_lines () =
556 let line = input_line inch in
564 let applyStylesheets input styles args =
565 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
570 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
572 (*CSC: ????????????????? *)
574 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
578 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
579 ~ask_dtd_to_the_getter:true
583 None -> Xml2Gdome.document_of_xml domImpl xml
585 Xml.pp xml (Some constanttypefile) ;
586 Xml2Gdome.document_of_xml domImpl bodyxml'
588 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
589 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
591 Xml.pp xmlinnertypes (Some innertypesfile) ;
592 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
597 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
600 let struri = UriManager.string_of_uri uri in
601 let idx = (String.rindex struri '/') + 1 in
602 String.sub struri idx (String.length struri - idx)
604 let path = pathname ^ "/" ^ name in
606 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
610 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
611 ~ask_dtd_to_the_getter:false
614 let innertypesuri = UriManager.innertypesuri_of_uri uri in
615 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
616 Getter.register innertypesuri
617 (Configuration.annotations_url ^
618 Str.replace_first (Str.regexp "^cic:") ""
619 (UriManager.string_of_uri innertypesuri) ^ ".xml"
621 (* constant type / variable / mutual inductive types definition *)
622 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
624 (Configuration.annotations_url ^
625 Str.replace_first (Str.regexp "^cic:") ""
626 (UriManager.string_of_uri uri) ^ ".xml"
633 match UriManager.bodyuri_of_uri uri with
635 | Some bodyuri -> bodyuri
637 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
638 Getter.register bodyuri
639 (Configuration.annotations_url ^
640 Str.replace_first (Str.regexp "^cic:") ""
641 (UriManager.string_of_uri bodyuri) ^ ".xml"
648 exception RefreshSequentException of exn;;
649 exception RefreshProofException of exn;;
651 let refresh_proof (output : GMathView.math_view) =
653 let uri,currentproof =
654 match !ProofEngine.proof with
656 | Some (uri,metasenv,bo,ty) ->
657 !qed_set_sensitive (List.length metasenv = 0) ;
658 (*CSC: Wrong: [] is just plainly wrong *)
659 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
662 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
663 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
665 Cic2acic.acic_object_of_cic_object currentproof
668 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
671 output#load_tree mml ;
673 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
676 match !ProofEngine.proof with
678 | Some (uri,metasenv,bo,ty) ->
679 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
680 raise (RefreshProofException e)
683 let refresh_sequent ?(empty_notebook=true) notebook =
685 match !ProofEngine.goal with
687 if empty_notebook then
689 notebook#remove_all_pages ~skip_switch_page_event:false ;
690 notebook#set_empty_page
693 notebook#proofw#unload
696 match !ProofEngine.proof with
698 | Some (_,metasenv,_,_) -> metasenv
700 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
701 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
702 SequentPp.XmlPp.print_sequent metasenv currentsequent
704 let regenerate_notebook () =
705 let skip_switch_page_event =
707 (m,_,_)::_ when m = metano -> false
710 notebook#remove_all_pages ~skip_switch_page_event ;
711 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
713 if empty_notebook then
715 regenerate_notebook () ;
716 notebook#set_current_page ~may_skip_switch_page_event:false metano
720 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
722 applyStylesheets sequent_doc sequent_styles sequent_args
724 notebook#set_current_page ~may_skip_switch_page_event:true metano;
725 notebook#proofw#load_tree ~dom:sequent_mml
727 current_goal_infos :=
728 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
732 match !ProofEngine.goal with
737 match !ProofEngine.proof with
739 | Some (_,metasenv,_,_) -> metasenv
742 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
743 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
744 raise (RefreshSequentException e)
745 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
749 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
750 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
753 let mml_of_cic_term metano term =
755 match !ProofEngine.proof with
757 | Some (_,metasenv,_,_) -> metasenv
760 match !ProofEngine.goal with
763 let (_,canonical_context,_) =
764 List.find (function (m,_,_) -> m=metano) metasenv
768 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
769 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
772 Xml2Gdome.document_of_xml domImpl sequent_gdome
775 applyStylesheets sequent_doc sequent_styles sequent_args ;
777 current_scratch_infos :=
778 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
782 exception OpenConjecturesStillThere;;
783 exception WrongProof;;
785 let pathname_of_annuri uristring =
786 Configuration.annotations_dir ^
787 Str.replace_first (Str.regexp "^cic:") "" uristring
790 let make_dirs dirpath =
791 ignore (Unix.system ("mkdir -p " ^ dirpath))
794 let save_obj uri obj =
796 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
797 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
799 Cic2acic.acic_object_of_cic_object obj
801 (* let's save the theorem and register it to the getter *)
802 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
804 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
809 match !ProofEngine.proof with
811 | Some (uri,[],bo,ty) ->
813 CicReduction.are_convertible []
814 (CicTypeChecker.type_of_aux' [] [] bo) ty
817 (*CSC: Wrong: [] is just plainly wrong *)
818 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
820 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
821 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
823 Cic2acic.acic_object_of_cic_object proof
826 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
829 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
830 !qed_set_sensitive false ;
831 (* let's save the theorem and register it to the getter *)
832 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
834 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
838 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
843 | _ -> raise OpenConjecturesStillThere
847 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
848 match !ProofEngine.proof with
850 | Some (uri, metasenv, bo, ty) ->
852 (*CSC: Wrong: [] is just plainly wrong *)
853 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
855 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
856 Cic2acic.acic_object_of_cic_object currentproof
860 Cic2Xml.print_object uri ~ids_to_inner_sorts
861 ~ask_dtd_to_the_getter:true acurrentproof
863 xml,Some bodyxml -> xml,bodyxml
864 | _,None -> assert false
866 Xml.pp ~quiet:true xml (Some prooffiletype) ;
867 output_html outputhtml
868 ("<h1 color=\"Green\">Current proof type saved to " ^
869 prooffiletype ^ "</h1>") ;
870 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
871 output_html outputhtml
872 ("<h1 color=\"Green\">Current proof body saved to " ^
876 (* Used to typecheck the loaded proofs *)
877 let typecheck_loaded_proof metasenv bo ty =
878 let module T = CicTypeChecker in
881 (fun metasenv ((_,context,ty) as conj) ->
882 ignore (T.type_of_aux' metasenv context ty) ;
885 ignore (T.type_of_aux' metasenv [] ty) ;
886 ignore (T.type_of_aux' metasenv [] bo)
890 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
891 let output = ((rendering_window ())#output : GMathView.math_view) in
892 let notebook = (rendering_window ())#notebook in
895 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
898 None -> raise NoChoice
900 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
901 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
902 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
903 typecheck_loaded_proof metasenv bo ty ;
905 Some (uri, metasenv, bo, ty) ;
909 | (metano,_,_)::_ -> Some metano
911 refresh_proof output ;
912 refresh_sequent notebook ;
913 output_html outputhtml
914 ("<h1 color=\"Green\">Current proof type loaded from " ^
915 prooffiletype ^ "</h1>") ;
916 output_html outputhtml
917 ("<h1 color=\"Green\">Current proof body loaded from " ^
918 prooffile ^ "</h1>") ;
919 !save_set_sensitive true
922 RefreshSequentException e ->
923 output_html outputhtml
924 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
925 "sequent: " ^ Printexc.to_string e ^ "</h1>")
926 | RefreshProofException e ->
927 output_html outputhtml
928 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
929 "proof: " ^ Printexc.to_string e ^ "</h1>")
931 output_html outputhtml
932 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
935 let edit_aliases () =
936 let chosen = ref false in
939 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
941 GPack.vbox ~border_width:0 ~packing:window#add () in
942 let scrolled_window =
943 GBin.scrolled_window ~border_width:10
944 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
945 let input = GEdit.text ~editable:true ~width:400 ~height:100
946 ~packing:scrolled_window#add () in
948 GPack.hbox ~border_width:0
949 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
951 GButton.button ~label:"Ok"
952 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
954 GButton.button ~label:"Cancel"
955 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
956 ignore (window#connect#destroy GMain.Main.quit) ;
957 ignore (cancelb#connect#clicked window#destroy) ;
959 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
960 let dom,resolve_id = !id_to_uris in
962 (input#insert_text ~pos:0
967 match resolve_id v with
972 (string_of_cic_textual_parser_uri uri)
978 let inputtext = input#get_chars 0 input#length in
980 let alfa = "[a-zA-Z_-]" in
981 let digit = "[0-9]" in
982 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
983 let blanks = "\( \|\t\|\n\)+" in
984 let nonblanks = "[^ \t\n]+" in
985 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
987 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
991 let n' = Str.search_forward regexpr inputtext n in
992 let id = Str.matched_group 2 inputtext in
994 cic_textual_parser_uri_of_string
995 ("cic:" ^ (Str.matched_group 5 inputtext))
997 let dom,resolve_id = aux (n' + 1) in
998 if List.mem id dom then
1002 (function id' -> if id = id' then Some uri else resolve_id id')
1004 Not_found -> empty_id_to_uris
1008 id_to_uris := dom,resolve_id
1012 let module L = LogicalOperations in
1013 let module G = Gdome in
1014 let notebook = (rendering_window ())#notebook in
1015 let output = (rendering_window ())#output in
1016 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1017 match (rendering_window ())#output#get_selection with
1020 ((node : Gdome.element)#getAttributeNS
1021 (*CSC: OCAML DIVERGE
1022 ((element : G.element)#getAttributeNS
1024 ~namespaceURI:helmns
1025 ~localName:(G.domString "xref"))#to_string
1027 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1031 match !current_cic_infos with
1032 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1034 L.to_sequent id ids_to_terms ids_to_father_ids ;
1035 refresh_proof output ;
1036 refresh_sequent notebook
1037 | None -> assert false (* "ERROR: No current term!!!" *)
1039 RefreshSequentException e ->
1040 output_html outputhtml
1041 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1042 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1043 | RefreshProofException e ->
1044 output_html outputhtml
1045 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1046 "proof: " ^ Printexc.to_string e ^ "</h1>")
1048 output_html outputhtml
1049 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1051 | None -> assert false (* "ERROR: No selection!!!" *)
1055 let module L = LogicalOperations in
1056 let module G = Gdome in
1057 let notebook = (rendering_window ())#notebook in
1058 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1059 match (rendering_window ())#output#get_selection with
1062 ((node : Gdome.element)#getAttributeNS
1063 (*CSC: OCAML DIVERGE
1064 ((element : G.element)#getAttributeNS
1066 ~namespaceURI:helmns
1067 ~localName:(G.domString "xref"))#to_string
1069 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1073 match !current_cic_infos with
1074 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1076 L.focus id ids_to_terms ids_to_father_ids ;
1077 refresh_sequent notebook
1078 | None -> assert false (* "ERROR: No current term!!!" *)
1080 RefreshSequentException e ->
1081 output_html outputhtml
1082 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1083 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1084 | RefreshProofException e ->
1085 output_html outputhtml
1086 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1087 "proof: " ^ Printexc.to_string e ^ "</h1>")
1089 output_html outputhtml
1090 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1092 | None -> assert false (* "ERROR: No selection!!!" *)
1095 exception NoPrevGoal;;
1096 exception NoNextGoal;;
1098 let setgoal metano =
1099 let module L = LogicalOperations in
1100 let module G = Gdome in
1101 let notebook = (rendering_window ())#notebook in
1102 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1104 match !ProofEngine.proof with
1105 None -> assert false
1106 | Some (_,metasenv,_,_) -> metasenv
1109 refresh_sequent ~empty_notebook:false notebook
1111 RefreshSequentException e ->
1112 output_html outputhtml
1113 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1114 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1116 output_html outputhtml
1117 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1121 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1124 GWindow.window ~width:800 ~border_width:2 () in
1125 let scrolled_window =
1126 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1128 GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1129 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1130 let href = Gdome.domString "href" in
1131 let show_in_show_window_obj uri obj =
1132 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1135 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1136 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1138 Cic2acic.acic_object_of_cic_object obj
1141 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1144 window#set_title (UriManager.string_of_uri uri) ;
1145 window#misc#hide () ; window#show () ;
1146 mmlwidget#load_tree mml ;
1149 output_html outputhtml
1150 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1152 let show_in_show_window_uri uri =
1153 let obj = CicEnvironment.get_obj uri in
1154 show_in_show_window_obj uri obj
1156 let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1157 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1159 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1161 show_in_show_window_uri (UriManager.uri_of_string uri)
1163 if mmlwidget#get_action <> None then
1164 mmlwidget#action_toggle
1167 mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1169 show_in_show_window_obj, show_in_show_window_uri,
1170 show_in_show_window_callback
1173 exception NoObjectsLocated;;
1175 let user_uri_choice ~title ~msg uris =
1178 [] -> raise NoObjectsLocated
1182 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1187 String.sub uri 4 (String.length uri - 4)
1190 let locate_callback id =
1191 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1192 let result = MQueryGenerator.locate id in
1195 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1198 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1200 output_html outputhtml html ;
1201 user_uri_choice ~title:"Ambiguous input."
1203 ("Ambiguous input \"" ^ id ^
1204 "\". Please, choose one interpetation:")
1209 let inputt = ((rendering_window ())#inputt : term_editor) in
1210 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1213 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1215 None -> raise NoChoice
1217 let uri = locate_callback input in
1221 output_html outputhtml
1222 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1225 let input_or_locate_uri ~title =
1226 let uri = ref None in
1229 ~width:400 ~modal:true ~title ~border_width:2 () in
1230 let vbox = GPack.vbox ~packing:window#add () in
1232 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1234 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1236 GEdit.entry ~editable:true
1237 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1239 GButton.button ~label:"Check"
1240 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1241 let _ = checkb#misc#set_sensitive false in
1243 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1245 GMisc.label ~text:"You can also enter an indentifier to locate:"
1246 ~packing:(hbox2#pack ~padding:5) () in
1248 GEdit.entry ~editable:true
1249 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1251 GButton.button ~label:"Locate"
1252 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1253 let _ = locateb#misc#set_sensitive false in
1255 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1257 GButton.button ~label:"Ok"
1258 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1259 let _ = okb#misc#set_sensitive false in
1261 GButton.button ~label:"Cancel"
1262 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1264 ignore (window#connect#destroy GMain.Main.quit) ;
1266 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1267 let check_callback () =
1268 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1269 let uri = "cic:" ^ manual_input#text in
1271 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1272 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1275 Getter.Unresolved ->
1276 output_html outputhtml
1277 ("<h1 color=\"Red\">URI " ^ uri ^
1278 " does not correspond to any object.</h1>") ;
1280 | UriManager.IllFormedUri _ ->
1281 output_html outputhtml
1282 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1285 output_html outputhtml
1286 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1290 (okb#connect#clicked
1292 if check_callback () then
1294 uri := Some manual_input#text ;
1298 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1300 (manual_input#connect#changed
1302 if manual_input#text = "" then
1304 checkb#misc#set_sensitive false ;
1305 okb#misc#set_sensitive false
1309 checkb#misc#set_sensitive true ;
1310 okb#misc#set_sensitive true
1313 (locate_input#connect#changed
1314 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1316 (locateb#connect#clicked
1318 let id = locate_input#text in
1319 manual_input#set_text (locate_callback id) ;
1320 locate_input#delete_text 0 (String.length id)
1323 GMain.Main.main () ;
1325 None -> raise NoChoice
1326 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1329 let locate_one_id id =
1330 let result = MQueryGenerator.locate id in
1334 wrong_xpointer_format_from_wrong_xpointer_format' uri
1336 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1337 output_html (rendering_window ())#outputhtml html ;
1341 [UriManager.string_of_uri
1342 (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1345 interactive_user_uri_choice
1346 ~selection_mode:`EXTENDED
1347 ~ok:"Try every selection."
1348 ~enable_button_for_non_vars:true
1349 ~title:"Ambiguous input."
1351 ("Ambiguous input \"" ^ id ^
1352 "\". Please, choose one or more interpretations:")
1355 List.map cic_textual_parser_uri_of_string uris'
1358 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1359 exception AmbiguousInput;;
1361 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1362 let known_ids,resolve_id = !id_to_uris in
1368 if List.mem he known_ids then filter tl else he::(filter tl)
1372 (* for each id in dom' we get the list of uris associated to it *)
1373 let list_of_uris = List.map locate_one_id dom' in
1374 (* and now we compute the list of all possible assignments from id to uris *)
1376 let rec aux ids list_of_uris =
1377 match ids,list_of_uris with
1378 [],[] -> [resolve_id]
1379 | id::idtl,uris::uristl ->
1380 let resolves = aux idtl uristl in
1386 function id' -> if id = id' then Some uri else f id'
1390 | _,_ -> assert false
1392 aux dom' list_of_uris
1394 let tests_no = List.length resolve_ids in
1395 if tests_no > 1 then
1396 output_html (outputhtml ())
1397 ("<h1>Disambiguation phase started: " ^
1398 string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1399 (* now we select only the ones that generates well-typed terms *)
1405 let metasenv',expr = mk_metasenv_and_expr resolve in
1407 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1409 (CicTypeChecker.type_of_aux' metasenv context expr) ;
1410 resolve::(filter tl)
1417 match resolve_ids' with
1418 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1419 | [resolve_id] -> resolve_id
1423 (function resolve ->
1427 match resolve id with
1428 None -> assert false
1431 CicTextualParser0.ConUri uri
1432 | CicTextualParser0.VarUri uri ->
1433 UriManager.string_of_uri uri
1434 | CicTextualParser0.IndTyUri (uri,tyno) ->
1435 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1436 string_of_int (tyno+1) ^ ")"
1437 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1438 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1439 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
1443 let index = interactive_interpretation_choice choices in
1444 List.nth resolve_ids' index
1446 id_to_uris := known_ids @ dom', resolve_id' ;
1447 mk_metasenv_and_expr resolve_id'
1450 exception UriAlreadyInUse;;
1451 exception NotAUriToAConstant;;
1453 let new_inductive () =
1454 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1455 let output = ((rendering_window ())#output : GMathView.math_view) in
1456 let notebook = (rendering_window ())#notebook in
1458 let chosen = ref false in
1459 let inductive = ref true in
1460 let paramsno = ref 0 in
1461 let get_uri = ref (function _ -> assert false) in
1462 let get_base_uri = ref (function _ -> assert false) in
1463 let get_names = ref (function _ -> assert false) in
1464 let get_types_and_cons = ref (function _ -> assert false) in
1465 let get_name_context_context_and_subst = ref (function _ -> assert false) in
1468 ~width:600 ~modal:true ~position:`CENTER
1469 ~title:"New Block of Mutual (Co)Inductive Definitions"
1470 ~border_width:2 () in
1471 let vbox = GPack.vbox ~packing:window#add () in
1473 GPack.hbox ~border_width:0
1474 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1476 GMisc.label ~text:"Enter the URI for the new block:"
1477 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1479 GEdit.entry ~editable:true
1480 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1482 GPack.hbox ~border_width:0
1483 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1487 "Enter the number of left parameters in every arity and constructor type:"
1488 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1489 let paramsno_entry =
1490 GEdit.entry ~editable:true ~text:"0"
1491 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1493 GPack.hbox ~border_width:0
1494 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1496 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1497 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1499 GButton.radio_button ~label:"Inductive"
1500 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1502 GButton.radio_button ~label:"Coinductive"
1503 ~group:inductiveb#group
1504 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1506 GPack.hbox ~border_width:0
1507 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1509 GMisc.label ~text:"Enter the list of the names of the types:"
1510 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1512 GEdit.entry ~editable:true
1513 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1515 GPack.hbox ~border_width:0
1516 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1518 GButton.button ~label:"> Next"
1519 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1520 let _ = okb#misc#set_sensitive true in
1522 GButton.button ~label:"Abort"
1523 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1524 ignore (window#connect#destroy GMain.Main.quit) ;
1525 ignore (cancelb#connect#clicked window#destroy) ;
1529 (okb#connect#clicked
1532 let uristr = "cic:" ^ uri_entry#text in
1533 let namesstr = names_entry#text in
1534 let paramsno' = int_of_string (paramsno_entry#text) in
1535 match Str.split (Str.regexp " +") namesstr with
1537 | (he::tl) as names ->
1538 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1541 ignore (Getter.resolve uri) ;
1542 raise UriAlreadyInUse
1544 Getter.Unresolved ->
1545 get_uri := (function () -> uri) ;
1546 get_names := (function () -> names) ;
1547 inductive := inductiveb#active ;
1548 paramsno := paramsno' ;
1553 output_html outputhtml
1554 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1562 GBin.frame ~label:name
1563 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1564 let vbox = GPack.vbox ~packing:frame#add () in
1565 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1567 GMisc.label ~text:("Enter its type:")
1568 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1569 let scrolled_window =
1570 GBin.scrolled_window ~border_width:5
1571 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1573 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1574 ~isnotempty_callback:
1576 (*non_empty_type := b ;*)
1577 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1580 GPack.hbox ~border_width:0
1581 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1583 GMisc.label ~text:("Enter the list of its constructors:")
1584 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1585 let cons_names_entry =
1586 GEdit.entry ~editable:true
1587 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1588 (newinputt,cons_names_entry)
1591 vbox#remove hboxn#coerce ;
1593 GPack.hbox ~border_width:0
1594 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1596 GButton.button ~label:"> Next"
1597 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1599 GButton.button ~label:"Abort"
1600 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1601 ignore (cancelb#connect#clicked window#destroy) ;
1603 (okb#connect#clicked
1606 let names = !get_names () in
1607 let types_and_cons =
1609 (fun name (newinputt,cons_names_entry) ->
1610 let dom,mk_metasenv_and_expr =
1611 newinputt#get_term ~context:[] ~metasenv:[] in
1612 let consnamesstr = cons_names_entry#text in
1613 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1615 disambiguate_input [] [] dom mk_metasenv_and_expr
1618 [] -> expr,cons_names
1619 | _ -> raise AmbiguousInput
1620 ) names type_widgets
1622 let uri = !get_uri () in
1624 (* Let's see if so far the definition is well-typed *)
1627 (* To test if the arities of the inductive types are well *)
1628 (* typed, we check the inductive block definition where *)
1629 (* no constructor is given to each type. *)
1632 (fun name (ty,cons) -> (name, !inductive, ty, []))
1633 names types_and_cons
1635 CicTypeChecker.typecheck_mutual_inductive_defs uri
1636 (tys,params,paramsno)
1638 get_name_context_context_and_subst :=
1642 (fun (namecontext,context,subst) name (ty,_) ->
1644 (Some (Cic.Name name))::namecontext,
1645 (Some (Cic.Name name, Cic.Decl ty))::context,
1646 (Cic.MutInd (uri,!i,[]))::subst
1649 ) ([],[],[]) names types_and_cons) ;
1650 let types_and_cons' =
1652 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1653 names types_and_cons
1655 get_types_and_cons := (function () -> types_and_cons') ;
1660 output_html outputhtml
1661 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1664 and phase3 name cons =
1665 let get_cons_types = ref (function () -> assert false) in
1668 ~width:600 ~modal:true ~position:`CENTER
1669 ~title:(name ^ " Constructors")
1670 ~border_width:2 () in
1671 let vbox = GPack.vbox ~packing:window2#add () in
1672 let cons_type_widgets =
1674 (function consname ->
1676 GPack.hbox ~border_width:0
1677 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1679 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1680 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1681 let scrolled_window =
1682 GBin.scrolled_window ~border_width:5
1683 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1685 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1686 ~isnotempty_callback:
1688 (* (*non_empty_type := b ;*)
1689 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1694 GPack.hbox ~border_width:0
1695 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1697 GButton.button ~label:"> Next"
1698 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1699 let _ = okb#misc#set_sensitive true in
1701 GButton.button ~label:"Abort"
1702 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1703 ignore (window2#connect#destroy GMain.Main.quit) ;
1704 ignore (cancelb#connect#clicked window2#destroy) ;
1706 (okb#connect#clicked
1710 let namecontext,context,subst= !get_name_context_context_and_subst () in
1714 let dom,mk_metasenv_and_expr =
1715 inputt#get_term ~context:namecontext ~metasenv:[]
1718 disambiguate_input context [] dom mk_metasenv_and_expr
1722 let undebrujined_expr =
1724 (fun expr t -> CicSubstitution.subst t expr) expr subst
1726 name, undebrujined_expr
1727 | _ -> raise AmbiguousInput
1728 ) cons cons_type_widgets
1730 get_cons_types := (function () -> cons_types) ;
1734 output_html outputhtml
1735 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1738 GMain.Main.main () ;
1739 let okb_pressed = !chosen in
1741 if (not okb_pressed) then
1744 assert false (* The control never reaches this point *)
1747 (!get_cons_types ())
1750 (* No more phases left or Abort pressed *)
1752 GMain.Main.main () ;
1756 let uri = !get_uri () in
1759 let tys = !get_types_and_cons () in
1760 let obj = Cic.InductiveDefinition tys params !paramsno in
1763 prerr_endline (CicPp.ppobj obj) ;
1764 CicTypeChecker.typecheck_mutual_inductive_defs uri
1765 (tys,params,!paramsno) ;
1768 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1769 prerr_endline (CicPp.ppobj obj) ;
1771 (* We already know that obj is well-typed. We need to add it to the *)
1772 (* environment in order to compute the inner-types without having to *)
1773 (* debrujin it or having to modify lots of other functions to avoid *)
1774 (* asking the environment for the MUTINDs we are defining now. *)
1775 CicEnvironment.put_inductive_definition uri obj ;
1777 show_in_show_window_obj uri obj
1780 output_html outputhtml
1781 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1785 let inputt = ((rendering_window ())#inputt : term_editor) in
1786 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1787 let output = ((rendering_window ())#output : GMathView.math_view) in
1788 let notebook = (rendering_window ())#notebook in
1790 let chosen = ref false in
1791 let get_parsed = ref (function _ -> assert false) in
1792 let get_uri = ref (function _ -> assert false) in
1793 let non_empty_type = ref false in
1796 ~width:600 ~modal:true ~title:"New Proof or Definition"
1797 ~border_width:2 () in
1798 let vbox = GPack.vbox ~packing:window#add () in
1800 GPack.hbox ~border_width:0
1801 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1803 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1804 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1806 GEdit.entry ~editable:true
1807 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1809 GPack.hbox ~border_width:0
1810 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1812 GMisc.label ~text:"Enter the theorem or definition type:"
1813 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1814 let scrolled_window =
1815 GBin.scrolled_window ~border_width:5
1816 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1817 (* the content of the scrolled_window is moved below (see comment) *)
1819 GPack.hbox ~border_width:0
1820 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1822 GButton.button ~label:"Ok"
1823 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1824 let _ = okb#misc#set_sensitive false in
1826 GButton.button ~label:"Cancel"
1827 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1828 (* moved here to have visibility of the ok button *)
1830 new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1831 ~isnotempty_callback:
1833 non_empty_type := b ;
1834 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1837 newinputt#set_term inputt#get_as_string ;
1840 uri_entry#connect#changed
1842 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1844 ignore (window#connect#destroy GMain.Main.quit) ;
1845 ignore (cancelb#connect#clicked window#destroy) ;
1847 (okb#connect#clicked
1851 let parsed = newinputt#get_term [] [] in
1852 let uristr = "cic:" ^ uri_entry#text in
1853 let uri = UriManager.uri_of_string uristr in
1854 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1855 raise NotAUriToAConstant
1859 ignore (Getter.resolve uri) ;
1860 raise UriAlreadyInUse
1862 Getter.Unresolved ->
1863 get_parsed := (function () -> parsed) ;
1864 get_uri := (function () -> uri) ;
1869 output_html outputhtml
1870 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1873 GMain.Main.main () ;
1876 let dom,mk_metasenv_and_expr = !get_parsed () in
1878 disambiguate_input [] [] dom mk_metasenv_and_expr
1880 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1881 ProofEngine.proof :=
1882 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1883 ProofEngine.goal := Some 1 ;
1884 refresh_sequent notebook ;
1885 refresh_proof output ;
1886 !save_set_sensitive true ;
1889 RefreshSequentException e ->
1890 output_html outputhtml
1891 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1892 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1893 | RefreshProofException e ->
1894 output_html outputhtml
1895 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1896 "proof: " ^ Printexc.to_string e ^ "</h1>")
1898 output_html outputhtml
1899 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1902 let check_term_in_scratch scratch_window metasenv context expr =
1904 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1905 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1906 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1907 scratch_window#show () ;
1908 scratch_window#mmlwidget#load_tree ~dom:mml
1911 print_endline ("? " ^ CicPp.ppterm expr) ;
1915 let check scratch_window () =
1916 let inputt = ((rendering_window ())#inputt : term_editor) in
1917 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1919 match !ProofEngine.proof with
1921 | Some (_,metasenv,_,_) -> metasenv
1923 let context,names_context =
1925 match !ProofEngine.goal with
1928 let (_,canonical_context,_) =
1929 List.find (function (m,_,_) -> m=metano) metasenv
1936 Some (n,_) -> Some n
1941 let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1942 let (metasenv',expr) =
1943 disambiguate_input context metasenv dom mk_metasenv_and_expr
1945 check_term_in_scratch scratch_window metasenv' context expr
1948 output_html outputhtml
1949 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1953 (***********************)
1955 (***********************)
1957 let call_tactic tactic () =
1958 let notebook = (rendering_window ())#notebook in
1959 let output = ((rendering_window ())#output : GMathView.math_view) in
1960 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1961 let savedproof = !ProofEngine.proof in
1962 let savedgoal = !ProofEngine.goal in
1966 refresh_sequent notebook ;
1967 refresh_proof output
1969 RefreshSequentException e ->
1970 output_html outputhtml
1971 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1972 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1973 ProofEngine.proof := savedproof ;
1974 ProofEngine.goal := savedgoal ;
1975 refresh_sequent notebook
1976 | RefreshProofException e ->
1977 output_html outputhtml
1978 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1979 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1980 ProofEngine.proof := savedproof ;
1981 ProofEngine.goal := savedgoal ;
1982 refresh_sequent notebook ;
1983 refresh_proof output
1985 output_html outputhtml
1986 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1987 ProofEngine.proof := savedproof ;
1988 ProofEngine.goal := savedgoal ;
1992 let call_tactic_with_input tactic () =
1993 let notebook = (rendering_window ())#notebook in
1994 let output = ((rendering_window ())#output : GMathView.math_view) in
1995 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1996 let inputt = ((rendering_window ())#inputt : term_editor) in
1997 let savedproof = !ProofEngine.proof in
1998 let savedgoal = !ProofEngine.goal in
1999 let uri,metasenv,bo,ty =
2000 match !ProofEngine.proof with
2001 None -> assert false
2002 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2004 let canonical_context =
2005 match !ProofEngine.goal with
2006 None -> assert false
2008 let (_,canonical_context,_) =
2009 List.find (function (m,_,_) -> m=metano) metasenv
2016 Some (n,_) -> Some n
2021 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
2022 let (metasenv',expr) =
2023 disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
2025 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2027 refresh_sequent notebook ;
2028 refresh_proof output ;
2031 RefreshSequentException e ->
2032 output_html outputhtml
2033 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2034 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2035 ProofEngine.proof := savedproof ;
2036 ProofEngine.goal := savedgoal ;
2037 refresh_sequent notebook
2038 | RefreshProofException e ->
2039 output_html outputhtml
2040 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2041 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2042 ProofEngine.proof := savedproof ;
2043 ProofEngine.goal := savedgoal ;
2044 refresh_sequent notebook ;
2045 refresh_proof output
2047 output_html outputhtml
2048 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2049 ProofEngine.proof := savedproof ;
2050 ProofEngine.goal := savedgoal ;
2053 let call_tactic_with_goal_input tactic () =
2054 let module L = LogicalOperations in
2055 let module G = Gdome in
2056 let notebook = (rendering_window ())#notebook in
2057 let output = ((rendering_window ())#output : GMathView.math_view) in
2058 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2059 let savedproof = !ProofEngine.proof in
2060 let savedgoal = !ProofEngine.goal in
2061 match notebook#proofw#get_selection with
2064 ((node : Gdome.element)#getAttributeNS
2065 ~namespaceURI:helmns
2066 ~localName:(G.domString "xref"))#to_string
2068 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2072 match !current_goal_infos with
2073 Some (ids_to_terms, ids_to_father_ids,_) ->
2075 tactic (Hashtbl.find ids_to_terms id) ;
2076 refresh_sequent notebook ;
2077 refresh_proof output
2078 | None -> assert false (* "ERROR: No current term!!!" *)
2080 RefreshSequentException e ->
2081 output_html outputhtml
2082 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2083 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2084 ProofEngine.proof := savedproof ;
2085 ProofEngine.goal := savedgoal ;
2086 refresh_sequent notebook
2087 | RefreshProofException e ->
2088 output_html outputhtml
2089 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2090 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2091 ProofEngine.proof := savedproof ;
2092 ProofEngine.goal := savedgoal ;
2093 refresh_sequent notebook ;
2094 refresh_proof output
2096 output_html outputhtml
2097 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2098 ProofEngine.proof := savedproof ;
2099 ProofEngine.goal := savedgoal ;
2102 output_html outputhtml
2103 ("<h1 color=\"red\">No term selected</h1>")
2106 let call_tactic_with_input_and_goal_input tactic () =
2107 let module L = LogicalOperations in
2108 let module G = Gdome in
2109 let notebook = (rendering_window ())#notebook in
2110 let output = ((rendering_window ())#output : GMathView.math_view) in
2111 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2112 let inputt = ((rendering_window ())#inputt : term_editor) in
2113 let savedproof = !ProofEngine.proof in
2114 let savedgoal = !ProofEngine.goal in
2115 match notebook#proofw#get_selection with
2118 ((node : Gdome.element)#getAttributeNS
2119 ~namespaceURI:helmns
2120 ~localName:(G.domString "xref"))#to_string
2122 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2126 match !current_goal_infos with
2127 Some (ids_to_terms, ids_to_father_ids,_) ->
2129 let uri,metasenv,bo,ty =
2130 match !ProofEngine.proof with
2131 None -> assert false
2132 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2134 let canonical_context =
2135 match !ProofEngine.goal with
2136 None -> assert false
2138 let (_,canonical_context,_) =
2139 List.find (function (m,_,_) -> m=metano) metasenv
2141 canonical_context in
2145 Some (n,_) -> Some n
2149 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
2151 let (metasenv',expr) =
2152 disambiguate_input canonical_context metasenv dom
2153 mk_metasenv_and_expr
2155 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2156 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2158 refresh_sequent notebook ;
2159 refresh_proof output ;
2161 | None -> assert false (* "ERROR: No current term!!!" *)
2163 RefreshSequentException e ->
2164 output_html outputhtml
2165 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2166 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2167 ProofEngine.proof := savedproof ;
2168 ProofEngine.goal := savedgoal ;
2169 refresh_sequent notebook
2170 | RefreshProofException e ->
2171 output_html outputhtml
2172 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2173 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2174 ProofEngine.proof := savedproof ;
2175 ProofEngine.goal := savedgoal ;
2176 refresh_sequent notebook ;
2177 refresh_proof output
2179 output_html outputhtml
2180 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2181 ProofEngine.proof := savedproof ;
2182 ProofEngine.goal := savedgoal ;
2185 output_html outputhtml
2186 ("<h1 color=\"red\">No term selected</h1>")
2189 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2190 let module L = LogicalOperations in
2191 let module G = Gdome in
2192 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2193 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2194 let savedproof = !ProofEngine.proof in
2195 let savedgoal = !ProofEngine.goal in
2196 match mmlwidget#get_selection with
2199 ((node : Gdome.element)#getAttributeNS
2200 ~namespaceURI:helmns
2201 ~localName:(G.domString "xref"))#to_string
2203 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2207 match !current_scratch_infos with
2208 (* term is the whole goal in the scratch_area *)
2209 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2211 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2212 let mml = mml_of_cic_term 111 expr in
2213 scratch_window#show () ;
2214 scratch_window#mmlwidget#load_tree ~dom:mml
2215 | None -> assert false (* "ERROR: No current term!!!" *)
2218 output_html outputhtml
2219 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2222 output_html outputhtml
2223 ("<h1 color=\"red\">No term selected</h1>")
2226 let call_tactic_with_hypothesis_input tactic () =
2227 let module L = LogicalOperations in
2228 let module G = Gdome in
2229 let notebook = (rendering_window ())#notebook in
2230 let output = ((rendering_window ())#output : GMathView.math_view) in
2231 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2232 let savedproof = !ProofEngine.proof in
2233 let savedgoal = !ProofEngine.goal in
2234 match notebook#proofw#get_selection with
2237 ((node : Gdome.element)#getAttributeNS
2238 ~namespaceURI:helmns
2239 ~localName:(G.domString "xref"))#to_string
2241 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2245 match !current_goal_infos with
2246 Some (_,_,ids_to_hypotheses) ->
2248 tactic (Hashtbl.find ids_to_hypotheses id) ;
2249 refresh_sequent notebook ;
2250 refresh_proof output
2251 | None -> assert false (* "ERROR: No current term!!!" *)
2253 RefreshSequentException e ->
2254 output_html outputhtml
2255 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2256 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2257 ProofEngine.proof := savedproof ;
2258 ProofEngine.goal := savedgoal ;
2259 refresh_sequent notebook
2260 | RefreshProofException e ->
2261 output_html outputhtml
2262 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2263 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2264 ProofEngine.proof := savedproof ;
2265 ProofEngine.goal := savedgoal ;
2266 refresh_sequent notebook ;
2267 refresh_proof output
2269 output_html outputhtml
2270 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2271 ProofEngine.proof := savedproof ;
2272 ProofEngine.goal := savedgoal ;
2275 output_html outputhtml
2276 ("<h1 color=\"red\">No term selected</h1>")
2280 let intros = call_tactic ProofEngine.intros;;
2281 let exact = call_tactic_with_input ProofEngine.exact;;
2282 let apply = call_tactic_with_input ProofEngine.apply;;
2283 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2284 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2285 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2286 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2287 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2288 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2289 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2290 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2291 let cut = call_tactic_with_input ProofEngine.cut;;
2292 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2293 let letin = call_tactic_with_input ProofEngine.letin;;
2294 let ring = call_tactic ProofEngine.ring;;
2295 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2296 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2297 let fourier = call_tactic ProofEngine.fourier;;
2298 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2299 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2300 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2301 let reflexivity = call_tactic ProofEngine.reflexivity;;
2302 let symmetry = call_tactic ProofEngine.symmetry;;
2303 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2304 let exists = call_tactic ProofEngine.exists;;
2305 let split = call_tactic ProofEngine.split;;
2306 let left = call_tactic ProofEngine.left;;
2307 let right = call_tactic ProofEngine.right;;
2308 let assumption = call_tactic ProofEngine.assumption;;
2309 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2310 let absurd = call_tactic_with_input ProofEngine.absurd;;
2311 let contradiction = call_tactic ProofEngine.contradiction;;
2312 (* Galla chiede: come dare alla tattica la lista di termini da decomporre?
2313 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
2316 let whd_in_scratch scratch_window =
2317 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2320 let reduce_in_scratch scratch_window =
2321 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2324 let simpl_in_scratch scratch_window =
2325 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2331 (**********************)
2332 (* END OF TACTICS *)
2333 (**********************)
2337 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2339 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2342 output_html outputhtml
2343 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2346 exception NotADefinition;;
2349 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2350 let output = ((rendering_window ())#output : GMathView.math_view) in
2351 let notebook = (rendering_window ())#notebook in
2353 let uri = input_or_locate_uri ~title:"Open" in
2354 CicTypeChecker.typecheck uri ;
2355 let metasenv,bo,ty =
2356 match CicEnvironment.get_cooked_obj uri with
2357 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2358 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2361 | Cic.InductiveDefinition _ -> raise NotADefinition
2363 ProofEngine.proof :=
2364 Some (uri, metasenv, bo, ty) ;
2365 ProofEngine.goal := None ;
2366 refresh_sequent notebook ;
2367 refresh_proof output
2369 RefreshSequentException e ->
2370 output_html outputhtml
2371 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2372 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2373 | RefreshProofException e ->
2374 output_html outputhtml
2375 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2376 "proof: " ^ Printexc.to_string e ^ "</h1>")
2378 output_html outputhtml
2379 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2382 let show_query_results results =
2385 ~modal:false ~title:"Query results." ~border_width:2 () in
2386 let vbox = GPack.vbox ~packing:window#add () in
2388 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2391 ~text:"Click on a URI to show that object"
2392 ~packing:hbox#add () in
2393 let scrolled_window =
2394 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2395 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2396 let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2399 (function (uri,_) ->
2403 clist#set_row ~selectable:false n
2406 clist#columns_autosize () ;
2408 (clist#connect#select_row
2409 (fun ~row ~column ~event ->
2410 let (uristr,_) = List.nth results row in
2412 cic_textual_parser_uri_of_string
2413 (wrong_xpointer_format_from_wrong_xpointer_format' uristr)
2415 CicTextualParser0.ConUri uri
2416 | CicTextualParser0.VarUri uri
2417 | CicTextualParser0.IndTyUri (uri,_)
2418 | CicTextualParser0.IndConUri (uri,_,_) ->
2419 show_in_show_window_uri uri
2425 let refine_constraints (must_obj,must_rel,must_sort) =
2426 let chosen = ref false in
2427 let use_only = ref false in
2430 ~modal:true ~title:"Constraints refinement."
2431 ~width:800 ~border_width:2 () in
2432 let vbox = GPack.vbox ~packing:window#add () in
2434 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2437 ~text: "\"Only\" constraints can be enforced or not."
2438 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2440 GButton.toggle_button ~label:"Enforce \"only\" constraints"
2441 ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2444 (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2445 (* Notebook for the constraints choice *)
2447 GPack.notebook ~scrollable:true
2448 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2449 (* Rel constraints *)
2452 ~text: "Constraints on Rels" () in
2454 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2457 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2460 ~text: "You can now specify the constraints on Rels."
2461 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2462 let expected_height = 25 * (List.length must_rel + 2) in
2463 let height = if expected_height > 400 then 400 else expected_height in
2464 let scrolled_window =
2465 GBin.scrolled_window ~border_width:10 ~height ~width:600
2466 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2467 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2468 let rel_constraints =
2470 (function (position,depth) ->
2473 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2477 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2479 None -> position, ref None
2481 let mutable_ref = ref (Some depth') in
2483 GButton.toggle_button
2484 ~label:("depth = " ^ string_of_int depth') ~active:true
2485 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2488 (depthb#connect#toggled
2490 let sel_depth = if depthb#active then Some depth' else None in
2491 mutable_ref := sel_depth
2493 position, mutable_ref
2495 (* Sort constraints *)
2498 ~text: "Constraints on Sorts" () in
2500 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2503 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2506 ~text: "You can now specify the constraints on Sorts."
2507 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2508 let expected_height = 25 * (List.length must_sort + 2) in
2509 let height = if expected_height > 400 then 400 else expected_height in
2510 let scrolled_window =
2511 GBin.scrolled_window ~border_width:10 ~height ~width:600
2512 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2513 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2514 let sort_constraints =
2516 (function (position,depth,sort) ->
2519 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2522 ~text:(sort ^ " " ^ position)
2523 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2525 None -> position, ref None, sort
2527 let mutable_ref = ref (Some depth') in
2529 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2531 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2534 (depthb#connect#toggled
2536 let sel_depth = if depthb#active then Some depth' else None in
2537 mutable_ref := sel_depth
2539 position, mutable_ref, sort
2541 (* Obj constraints *)
2544 ~text: "Constraints on constants" () in
2546 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2549 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2552 ~text: "You can now specify the constraints on constants."
2553 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2554 let expected_height = 25 * (List.length must_obj + 2) in
2555 let height = if expected_height > 400 then 400 else expected_height in
2556 let scrolled_window =
2557 GBin.scrolled_window ~border_width:10 ~height ~width:600
2558 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2559 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2560 let obj_constraints =
2562 (function (uri,position,depth) ->
2565 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2568 ~text:(uri ^ " " ^ position)
2569 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2571 None -> uri, position, ref None
2573 let mutable_ref = ref (Some depth') in
2575 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2577 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2580 (depthb#connect#toggled
2582 let sel_depth = if depthb#active then Some depth' else None in
2583 mutable_ref := sel_depth
2585 uri, position, mutable_ref
2587 (* Confirm/abort buttons *)
2589 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2591 GButton.button ~label:"Ok"
2592 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2594 GButton.button ~label:"Abort"
2595 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2597 ignore (window#connect#destroy GMain.Main.quit) ;
2598 ignore (cancelb#connect#clicked window#destroy) ;
2600 (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2601 window#set_position `CENTER ;
2603 GMain.Main.main () ;
2605 let chosen_must_rel =
2607 (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2608 let chosen_must_sort =
2610 (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2613 let chosen_must_obj =
2615 (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2618 (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2620 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2621 Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2629 let completeSearchPattern () =
2630 let inputt = ((rendering_window ())#inputt : term_editor) in
2631 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2633 let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
2634 let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
2635 let must = MQueryLevels2.get_constraints expr in
2636 let must',only = refine_constraints must in
2637 let results = MQueryGenerator.searchPattern must' only in
2638 show_query_results results
2641 output_html outputhtml
2642 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2645 let choose_must list_of_must only =
2646 let chosen = ref None in
2647 let user_constraints = ref [] in
2650 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2651 let vbox = GPack.vbox ~packing:window#add () in
2653 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2657 ("You can now specify the genericity of the query. " ^
2658 "The more generic the slower.")
2659 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2661 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2665 "Suggestion: start with faster queries before moving to more generic ones."
2666 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2668 GPack.notebook ~scrollable:true
2669 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2672 let last = List.length list_of_must in
2678 (if !page = 1 then "More generic" else
2679 if !page = last then "More precise" else " ") () in
2680 let expected_height = 25 * (List.length must + 2) in
2681 let height = if expected_height > 400 then 400 else expected_height in
2682 let scrolled_window =
2683 GBin.scrolled_window ~border_width:10 ~height ~width:600
2684 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2686 GList.clist ~columns:2 ~packing:scrolled_window#add
2687 ~titles:["URI" ; "Position"] ()
2691 (function (uri,position) ->
2694 [uri; if position then "MainConclusion" else "Conclusion"]
2696 clist#set_row ~selectable:false n
2699 clist#columns_autosize ()
2702 let label = GMisc.label ~text:"User provided" () in
2704 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2706 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2709 ~text:"Select the constraints that must be satisfied and press OK."
2710 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2711 let expected_height = 25 * (List.length only + 2) in
2712 let height = if expected_height > 400 then 400 else expected_height in
2713 let scrolled_window =
2714 GBin.scrolled_window ~border_width:10 ~height ~width:600
2715 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2717 GList.clist ~columns:2 ~packing:scrolled_window#add
2718 ~selection_mode:`EXTENDED
2719 ~titles:["URI" ; "Position"] ()
2723 (function (uri,position) ->
2726 [uri; if position then "MainConclusion" else "Conclusion"]
2728 clist#set_row ~selectable:true n
2731 clist#columns_autosize () ;
2733 (clist#connect#select_row
2734 (fun ~row ~column ~event ->
2735 user_constraints := (List.nth only row)::!user_constraints)) ;
2737 (clist#connect#unselect_row
2738 (fun ~row ~column ~event ->
2741 (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2744 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2746 GButton.button ~label:"Ok"
2747 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2749 GButton.button ~label:"Abort"
2750 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2752 ignore (window#connect#destroy GMain.Main.quit) ;
2753 ignore (cancelb#connect#clicked window#destroy) ;
2755 (okb#connect#clicked
2756 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2757 window#set_position `CENTER ;
2759 GMain.Main.main () ;
2761 None -> raise NoChoice
2763 if n = List.length list_of_must then
2764 (* user provided constraints *)
2767 List.nth list_of_must n
2770 let searchPattern () =
2771 let inputt = ((rendering_window ())#inputt : term_editor) in
2772 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2775 match !ProofEngine.proof with
2776 None -> assert false
2777 | Some (_,metasenv,_,_) -> metasenv
2779 match !ProofEngine.goal with
2782 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2783 let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2784 let must = choose_must list_of_must only in
2785 let torigth_restriction (u,b) =
2788 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2790 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2794 let rigth_must = List.map torigth_restriction must in
2795 let rigth_only = Some (List.map torigth_restriction only) in
2797 MQueryGenerator.searchPattern
2798 (rigth_must,[],[]) (rigth_only,None,None) in
2802 wrong_xpointer_format_from_wrong_xpointer_format' uri
2805 " <h1>Backward Query: </h1>" ^
2806 " <pre>" ^ get_last_query result ^ "</pre>"
2808 output_html outputhtml html ;
2810 let rec filter_out =
2814 let tl',exc = filter_out tl in
2817 ProofEngine.can_apply
2818 (term_of_cic_textual_parser_uri
2819 (cic_textual_parser_uri_of_string uri))
2827 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2828 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2835 " <h1>Objects that can actually be applied: </h1> " ^
2836 String.concat "<br>" uris' ^ exc ^
2837 " <h1>Number of false matches: " ^
2838 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2839 " <h1>Number of good matches: " ^
2840 string_of_int (List.length uris') ^ "</h1>"
2842 output_html outputhtml html' ;
2844 user_uri_choice ~title:"Ambiguous input."
2846 "Many lemmas can be successfully applied. Please, choose one:"
2849 inputt#set_term uri' ;
2853 output_html outputhtml
2854 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2857 let choose_selection
2858 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2860 let module G = Gdome in
2861 let rec aux element =
2862 if element#hasAttributeNS
2863 ~namespaceURI:helmns
2864 ~localName:(G.domString "xref")
2866 mmlwidget#set_selection (Some element)
2868 match element#get_parentNode with
2869 None -> assert false
2870 (*CSC: OCAML DIVERGES!
2871 | Some p -> aux (new G.element_of_node p)
2873 | Some p -> aux (new Gdome.element_of_node p)
2877 | None -> mmlwidget#set_selection None
2880 (* STUFF TO BUILD THE GTK INTERFACE *)
2882 (* Stuff for the widget settings *)
2884 let export_to_postscript (output : GMathView.math_view) =
2885 let lastdir = ref (Unix.getcwd ()) in
2888 GToolbox.select_file ~title:"Export to PostScript"
2889 ~dir:lastdir ~filename:"screenshot.ps" ()
2893 output#export_to_postscript ~filename:filename ();
2896 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2897 button_set_kerning button_set_transparency export_to_postscript_menu_item
2900 let is_set = button_t1#active in
2901 output#set_font_manager_type
2902 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2905 button_set_anti_aliasing#misc#set_sensitive true ;
2906 button_set_kerning#misc#set_sensitive true ;
2907 button_set_transparency#misc#set_sensitive true ;
2908 export_to_postscript_menu_item#misc#set_sensitive true ;
2912 button_set_anti_aliasing#misc#set_sensitive false ;
2913 button_set_kerning#misc#set_sensitive false ;
2914 button_set_transparency#misc#set_sensitive false ;
2915 export_to_postscript_menu_item#misc#set_sensitive false ;
2919 let set_anti_aliasing output button_set_anti_aliasing () =
2920 output#set_anti_aliasing button_set_anti_aliasing#active
2923 let set_kerning output button_set_kerning () =
2924 output#set_kerning button_set_kerning#active
2927 let set_transparency output button_set_transparency () =
2928 output#set_transparency button_set_transparency#active
2931 let changefont output font_size_spinb () =
2932 output#set_font_size font_size_spinb#value_as_int
2935 let set_log_verbosity output log_verbosity_spinb () =
2936 output#set_log_verbosity log_verbosity_spinb#value_as_int
2939 class settings_window (output : GMathView.math_view) sw
2940 export_to_postscript_menu_item selection_changed_callback
2942 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2944 GPack.vbox ~packing:settings_window#add () in
2947 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2948 ~border_width:5 ~packing:vbox#add () in
2950 GButton.toggle_button ~label:"activate t1 fonts"
2951 ~packing:(table#attach ~left:0 ~top:0) () in
2952 let button_set_anti_aliasing =
2953 GButton.toggle_button ~label:"set_anti_aliasing"
2954 ~packing:(table#attach ~left:0 ~top:1) () in
2955 let button_set_kerning =
2956 GButton.toggle_button ~label:"set_kerning"
2957 ~packing:(table#attach ~left:1 ~top:1) () in
2958 let button_set_transparency =
2959 GButton.toggle_button ~label:"set_transparency"
2960 ~packing:(table#attach ~left:2 ~top:1) () in
2963 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2964 ~border_width:5 ~packing:vbox#add () in
2965 let font_size_label =
2966 GMisc.label ~text:"font size:"
2967 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2968 let font_size_spinb =
2970 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2973 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2974 let log_verbosity_label =
2975 GMisc.label ~text:"log verbosity:"
2976 ~packing:(table#attach ~left:0 ~top:1) () in
2977 let log_verbosity_spinb =
2979 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2982 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2984 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2986 GButton.button ~label:"Close"
2987 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2989 method show = settings_window#show
2991 button_set_anti_aliasing#misc#set_sensitive false ;
2992 button_set_kerning#misc#set_sensitive false ;
2993 button_set_transparency#misc#set_sensitive false ;
2994 (* Signals connection *)
2995 ignore(button_t1#connect#clicked
2996 (activate_t1 output button_set_anti_aliasing button_set_kerning
2997 button_set_transparency export_to_postscript_menu_item button_t1)) ;
2998 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2999 ignore(button_set_anti_aliasing#connect#toggled
3000 (set_anti_aliasing output button_set_anti_aliasing));
3001 ignore(button_set_kerning#connect#toggled
3002 (set_kerning output button_set_kerning)) ;
3003 ignore(button_set_transparency#connect#toggled
3004 (set_transparency output button_set_transparency)) ;
3005 ignore(log_verbosity_spinb#connect#changed
3006 (set_log_verbosity output log_verbosity_spinb)) ;
3007 ignore(closeb#connect#clicked settings_window#misc#hide)
3010 (* Scratch window *)
3012 class scratch_window =
3014 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
3016 GPack.vbox ~packing:window#add () in
3018 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3020 GButton.button ~label:"Whd"
3021 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3023 GButton.button ~label:"Reduce"
3024 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3026 GButton.button ~label:"Simpl"
3027 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3028 let scrolled_window =
3029 GBin.scrolled_window ~border_width:10
3030 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3033 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
3035 method mmlwidget = mmlwidget
3036 method show () = window#misc#hide () ; window#show ()
3038 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
3039 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
3040 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
3041 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
3042 ignore(simplb#connect#clicked (simpl_in_scratch self))
3046 let vbox1 = GPack.vbox () in
3048 val mutable proofw_ref = None
3049 val mutable compute_ref = None
3051 Lazy.force self#compute ;
3052 match proofw_ref with
3053 None -> assert false
3054 | Some proofw -> proofw
3055 method content = vbox1
3057 match compute_ref with
3058 None -> assert false
3059 | Some compute -> compute
3063 let scrolled_window1 =
3064 GBin.scrolled_window ~border_width:10
3065 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3067 GMathView.math_view ~width:400 ~height:275
3068 ~packing:(scrolled_window1#add) () in
3069 let _ = proofw_ref <- Some proofw in
3071 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3073 GButton.button ~label:"Exact"
3074 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3076 GButton.button ~label:"Intros"
3077 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3079 GButton.button ~label:"Apply"
3080 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3081 let elimintrossimplb =
3082 GButton.button ~label:"ElimIntrosSimpl"
3083 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3085 GButton.button ~label:"ElimType"
3086 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3088 GButton.button ~label:"Whd"
3089 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3091 GButton.button ~label:"Reduce"
3092 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3094 GButton.button ~label:"Simpl"
3095 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3097 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3099 GButton.button ~label:"Fold_whd"
3100 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3102 GButton.button ~label:"Fold_reduce"
3103 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3105 GButton.button ~label:"Fold_simpl"
3106 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3108 GButton.button ~label:"Cut"
3109 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3111 GButton.button ~label:"Change"
3112 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3114 GButton.button ~label:"Let ... In"
3115 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3117 GButton.button ~label:"Ring"
3118 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3120 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3122 GButton.button ~label:"ClearBody"
3123 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3125 GButton.button ~label:"Clear"
3126 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3128 GButton.button ~label:"Fourier"
3129 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3131 GButton.button ~label:"RewriteSimpl ->"
3132 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3133 let rewritebacksimplb =
3134 GButton.button ~label:"RewriteSimpl <-"
3135 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3137 GButton.button ~label:"Replace"
3138 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3140 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3142 GButton.button ~label:"Reflexivity"
3143 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3145 GButton.button ~label:"Symmetry"
3146 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3148 GButton.button ~label:"Transitivity"
3149 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3151 GButton.button ~label:"Exists"
3152 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3154 GButton.button ~label:"Split"
3155 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3157 GButton.button ~label:"Left"
3158 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3160 GButton.button ~label:"Right"
3161 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3163 GButton.button ~label:"Assumption"
3164 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3166 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3168 GButton.button ~label:"Generalize"
3169 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3171 GButton.button ~label:"Absurd"
3172 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3173 let contradictionb =
3174 GButton.button ~label:"Contradiction"
3175 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3176 let searchpatternb =
3177 GButton.button ~label:"SearchPattern_Apply"
3178 ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3180 ignore(exactb#connect#clicked exact) ;
3181 ignore(applyb#connect#clicked apply) ;
3182 ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3183 ignore(elimtypeb#connect#clicked elimtype) ;
3184 ignore(whdb#connect#clicked whd) ;
3185 ignore(reduceb#connect#clicked reduce) ;
3186 ignore(simplb#connect#clicked simpl) ;
3187 ignore(foldwhdb#connect#clicked fold_whd) ;
3188 ignore(foldreduceb#connect#clicked fold_reduce) ;
3189 ignore(foldsimplb#connect#clicked fold_simpl) ;
3190 ignore(cutb#connect#clicked cut) ;
3191 ignore(changeb#connect#clicked change) ;
3192 ignore(letinb#connect#clicked letin) ;
3193 ignore(ringb#connect#clicked ring) ;
3194 ignore(clearbodyb#connect#clicked clearbody) ;
3195 ignore(clearb#connect#clicked clear) ;
3196 ignore(fourierb#connect#clicked fourier) ;
3197 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3198 ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3199 ignore(replaceb#connect#clicked replace) ;
3200 ignore(reflexivityb#connect#clicked reflexivity) ;
3201 ignore(symmetryb#connect#clicked symmetry) ;
3202 ignore(transitivityb#connect#clicked transitivity) ;
3203 ignore(existsb#connect#clicked exists) ;
3204 ignore(splitb#connect#clicked split) ;
3205 ignore(leftb#connect#clicked left) ;
3206 ignore(rightb#connect#clicked right) ;
3207 ignore(assumptionb#connect#clicked assumption) ;
3208 ignore(generalizeb#connect#clicked generalize) ;
3209 ignore(absurdb#connect#clicked absurd) ;
3210 ignore(contradictionb#connect#clicked contradiction) ;
3211 ignore(introsb#connect#clicked intros) ;
3212 ignore(searchpatternb#connect#clicked searchPattern) ;
3213 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3219 let vbox1 = GPack.vbox () in
3220 let scrolled_window1 =
3221 GBin.scrolled_window ~border_width:10
3222 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3224 GMathView.math_view ~width:400 ~height:275
3225 ~packing:(scrolled_window1#add) () in
3227 method proofw = (assert false : GMathView.math_view)
3228 method content = vbox1
3229 method compute = (assert false : unit)
3233 let empty_page = new empty_page;;
3237 val notebook = GPack.notebook ()
3239 val mutable skip_switch_page_event = false
3240 val mutable empty = true
3241 method notebook = notebook
3243 let new_page = new page () in
3245 pages := !pages @ [n,lazy (setgoal n),new_page] ;
3246 notebook#append_page
3247 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3248 new_page#content#coerce
3249 method remove_all_pages ~skip_switch_page_event:skip =
3251 notebook#remove_page 0 (* let's remove the empty page *)
3253 List.iter (function _ -> notebook#remove_page 0) !pages ;
3255 skip_switch_page_event <- skip
3256 method set_current_page ~may_skip_switch_page_event n =
3257 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3258 let new_page = notebook#page_num page#content#coerce in
3259 if may_skip_switch_page_event && new_page <> notebook#current_page then
3260 skip_switch_page_event <- true ;
3261 notebook#goto_page new_page
3262 method set_empty_page =
3265 notebook#append_page
3266 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3267 empty_page#content#coerce
3269 let (_,_,page) = List.nth !pages notebook#current_page in
3273 (notebook#connect#switch_page
3275 let skip = skip_switch_page_event in
3276 skip_switch_page_event <- false ;
3279 let (metano,setgoal,page) = List.nth !pages i in
3280 ProofEngine.goal := Some metano ;
3281 Lazy.force (page#compute) ;
3290 class rendering_window output (notebook : notebook) =
3291 let scratch_window = new scratch_window in
3293 GWindow.window ~title:"MathML viewer" ~border_width:0
3294 ~allow_shrink:false () in
3295 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3297 let handle_box = GBin.handle_box ~border_width:2
3298 ~packing:(vbox_for_menu#pack ~padding:0) () in
3299 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3300 let factory0 = new GMenu.factory menubar in
3301 let accel_group = factory0#accel_group in
3303 let file_menu = factory0#add_submenu "File" in
3304 let factory1 = new GMenu.factory file_menu ~accel_group in
3305 let export_to_postscript_menu_item =
3308 factory1#add_item "New Block of (Co)Inductive Definitions..."
3309 ~key:GdkKeysyms._B ~callback:new_inductive
3312 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3315 let reopen_menu_item =
3316 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3320 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3321 ignore (factory1#add_separator ()) ;
3323 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3325 let save_menu_item =
3326 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3329 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3330 ignore (!save_set_sensitive false);
3331 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3332 ignore (!qed_set_sensitive false);
3333 ignore (factory1#add_separator ()) ;
3334 let export_to_postscript_menu_item =
3335 factory1#add_item "Export to PostScript..."
3336 ~callback:(export_to_postscript output) in
3337 ignore (factory1#add_separator ()) ;
3339 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3340 export_to_postscript_menu_item
3343 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3344 let factory2 = new GMenu.factory edit_menu ~accel_group in
3345 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3346 let proveit_menu_item =
3347 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3348 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3350 let focus_menu_item =
3351 factory2#add_item "Focus" ~key:GdkKeysyms._F
3352 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3355 focus_and_proveit_set_sensitive :=
3357 proveit_menu_item#misc#set_sensitive b ;
3358 focus_menu_item#misc#set_sensitive b
3360 let _ = !focus_and_proveit_set_sensitive false in
3361 (* edit term menu *)
3362 let edit_term_menu = factory0#add_submenu "Edit Term" in
3363 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3364 let check_menu_item =
3365 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3366 ~callback:(check scratch_window) in
3367 let _ = check_menu_item#misc#set_sensitive false in
3369 let settings_menu = factory0#add_submenu "Search" in
3370 let factory4 = new GMenu.factory settings_menu ~accel_group in
3372 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3374 let searchPattern_menu_item =
3375 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3376 ~callback:completeSearchPattern in
3377 let _ = searchPattern_menu_item#misc#set_sensitive false in
3378 let show_menu_item =
3379 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3382 let settings_menu = factory0#add_submenu "Settings" in
3383 let factory3 = new GMenu.factory settings_menu ~accel_group in
3385 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3386 ~callback:edit_aliases in
3387 let _ = factory3#add_separator () in
3389 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3390 ~callback:(function _ -> (settings_window ())#show ()) in
3392 let _ = window#add_accel_group accel_group in
3396 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3398 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3399 let scrolled_window0 =
3400 GBin.scrolled_window ~border_width:10
3401 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3402 let _ = scrolled_window0#add output#coerce in
3404 GBin.frame ~label:"Insert Term"
3405 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3406 let scrolled_window1 =
3407 GBin.scrolled_window ~border_width:5
3408 ~packing:frame#add () in
3410 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3411 ~isnotempty_callback:
3413 check_menu_item#misc#set_sensitive b ;
3414 searchPattern_menu_item#misc#set_sensitive b) in
3416 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3418 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3420 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3424 ~source:"<html><body bgColor=\"white\"></body></html>"
3425 ~width:400 ~height: 100
3430 method outputhtml = outputhtml
3431 method inputt = inputt
3432 method output = (output : GMathView.math_view)
3433 method notebook = notebook
3434 method show = window#show
3436 notebook#set_empty_page ;
3437 export_to_postscript_menu_item#misc#set_sensitive false ;
3438 check_term := (check_term_in_scratch scratch_window) ;
3440 (* signal handlers here *)
3441 ignore(output#connect#selection_changed
3443 choose_selection output elem ;
3444 !focus_and_proveit_set_sensitive true
3446 ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3447 let settings_window = new settings_window output scrolled_window0
3448 export_to_postscript_menu_item (choose_selection output) in
3449 set_settings_window settings_window ;
3450 set_outputhtml outputhtml ;
3451 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3452 Logger.log_callback :=
3453 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3458 let initialize_everything () =
3459 let module U = Unix in
3460 let output = GMathView.math_view ~width:350 ~height:280 () in
3461 let notebook = new notebook in
3462 let rendering_window' = new rendering_window output notebook in
3463 set_rendering_window rendering_window' ;
3464 mml_of_cic_term_ref := mml_of_cic_term ;
3465 rendering_window'#show () ;
3472 Mqint.set_database Mqint.postgres_db ;
3473 Mqint.init postgresqlconnectionstring ;
3475 ignore (GtkMain.Main.init ()) ;
3476 initialize_everything () ;
3477 if !usedb then Mqint.close ();