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 <natile@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\">"
63 let prooffile = "/public/sacerdot/currentproof";;
64 let prooffiletype = "/public/sacerdot/currentprooftype";;
67 let prooffile = "/public/sacerdot/currentproof";;
68 let prooffiletype = "/public/sacerdot/currentprooftype";;
72 let prooffile = "/public/natile/currentproof";;
73 let prooffiletype = "/public/natile/currentprooftype";;
77 let prooffile = "//miohelm/tmp/currentproof";;
78 let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
82 let prooffile = "/home/galata/miohelm/currentproof";;
83 let prooffiletype = "/home/galata/miohelm/currentprooftype";;
86 (*CSC: the getter should handle the innertypes, not the FS *)
88 let innertypesfile = "/public/sacerdot/innertypes";;
89 let constanttypefile = "/public/sacerdot/constanttype";;
92 let innertypesfile = "/public/sacerdot/innertypes";;
93 let constanttypefile = "/public/sacerdot/constanttype";;
97 let innertypesfile = "/public/natile/innertypes";;
98 let constanttypefile = "/public/natile/constanttype";;
102 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
103 let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
107 let innertypesfile = "/home/galata/miohelm/innertypes";;
108 let constanttypefile = "/home/galata/miohelm/constanttype";;
111 let empty_id_to_uris = ([],function _ -> None);;
114 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
116 let htmlheader_and_content = ref htmlheader;;
118 let current_cic_infos = ref None;;
119 let current_goal_infos = ref None;;
120 let current_scratch_infos = ref None;;
122 let id_to_uris = ref empty_id_to_uris;;
124 let check_term = ref (fun _ _ _ -> assert false);;
125 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
127 exception RenderingWindowsNotInitialized;;
129 let set_rendering_window,rendering_window =
130 let rendering_window_ref = ref None in
131 (function rw -> rendering_window_ref := Some rw),
133 match !rendering_window_ref with
134 None -> raise RenderingWindowsNotInitialized
139 exception SettingsWindowsNotInitialized;;
141 let set_settings_window,settings_window =
142 let settings_window_ref = ref None in
143 (function rw -> settings_window_ref := Some rw),
145 match !settings_window_ref with
146 None -> raise SettingsWindowsNotInitialized
151 exception OutputHtmlNotInitialized;;
153 let set_outputhtml,outputhtml =
154 let outputhtml_ref = ref None in
155 (function rw -> outputhtml_ref := Some rw),
157 match !outputhtml_ref with
158 None -> raise OutputHtmlNotInitialized
159 | Some outputhtml -> outputhtml
163 exception QedSetSensitiveNotInitialized;;
164 let qed_set_sensitive =
165 ref (function _ -> raise QedSetSensitiveNotInitialized)
168 exception SaveSetSensitiveNotInitialized;;
169 let save_set_sensitive =
170 ref (function _ -> raise SaveSetSensitiveNotInitialized)
173 (* COMMAND LINE OPTIONS *)
179 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
182 Arg.parse argspec ignore ""
184 (* A WIDGET TO ENTER CIC TERMS *)
186 class term_editor ?packing ?width ?height ?isnotempty_callback () =
187 let input = GEdit.text ~editable:true ?width ?height ?packing () in
189 match isnotempty_callback with
192 ignore(input#connect#changed (function () -> callback (input#length > 0)))
195 method coerce = input#coerce
197 input#delete_text 0 input#length
198 (* CSC: txt is now a string, but should be of type Cic.term *)
199 method set_term txt =
201 ignore ((input#insert_text txt) ~pos:0)
202 (* CSC: this method should disappear *)
203 method get_as_string =
204 input#get_chars 0 input#length
205 method get_term ~context ~metasenv =
206 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
207 CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
213 exception IllFormedUri of string;;
215 let cic_textual_parser_uri_of_string uri' =
218 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
219 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
221 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
222 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
226 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
227 CicTextualParser0.IndTyUri (uri'',typeno)
230 (* Constructor of an Inductive Type *)
231 let uri'',typeno,consno =
232 CicTextualLexer.indconuri_of_uri uri'
234 CicTextualParser0.IndConUri (uri'',typeno,consno)
237 _ -> raise (IllFormedUri uri')
240 let term_of_cic_textual_parser_uri uri =
241 let module C = Cic in
242 let module CTP = CicTextualParser0 in
244 CTP.ConUri uri -> C.Const (uri,[])
245 | CTP.VarUri uri -> C.Var (uri,[])
246 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
247 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
250 let string_of_cic_textual_parser_uri uri =
251 let module C = Cic in
252 let module CTP = CicTextualParser0 in
255 CTP.ConUri uri -> UriManager.string_of_uri uri
256 | CTP.VarUri uri -> UriManager.string_of_uri uri
257 | CTP.IndTyUri (uri,tyno) ->
258 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
259 | CTP.IndConUri (uri,tyno,consno) ->
260 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
263 (* 4 = String.length "cic:" *)
264 String.sub uri' 4 (String.length uri' - 4)
267 let output_html outputhtml msg =
268 htmlheader_and_content := !htmlheader_and_content ^ msg ;
269 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
270 outputhtml#set_topline (-1)
273 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
277 let check_window outputhtml uris =
280 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
282 GPack.notebook ~scrollable:true ~packing:window#add () in
287 let scrolled_window =
288 GBin.scrolled_window ~border_width:10
290 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
296 ~packing:scrolled_window#add ~width:400 ~height:280 () in
299 term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
301 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
304 let mml = !mml_of_cic_term_ref 111 expr in
305 prerr_endline ("### " ^ CicPp.ppterm expr) ;
306 mmlwidget#load_tree ~dom:mml
309 output_html outputhtml
310 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
315 (notebook#connect#switch_page
316 (function i -> Lazy.force (List.nth render_terms i)))
322 interactive_user_uri_choice ~selection_mode ?(ok="Ok")
323 ?(enable_button_for_non_vars=false) ~title ~msg uris
325 let choices = ref [] in
326 let chosen = ref false in
327 let use_only_constants = ref false in
329 GWindow.dialog ~modal:true ~title ~width:600 () in
331 GMisc.label ~text:msg
332 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
333 let scrolled_window =
334 GBin.scrolled_window ~border_width:10
335 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
337 let expected_height = 18 * List.length uris in
338 let height = if expected_height > 400 then 400 else expected_height in
339 GList.clist ~columns:1 ~packing:scrolled_window#add
340 ~height ~selection_mode () in
341 let _ = List.map (function x -> clist#append [x]) uris in
343 GPack.hbox ~border_width:0
344 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
346 GMisc.label ~text:"None of the above. Try this one:"
347 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
349 GEdit.entry ~editable:true
350 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
352 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
354 GButton.button ~label:ok
355 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
356 let _ = okb#misc#set_sensitive false in
361 if enable_button_for_non_vars then
362 hbox#pack ~expand:false ~fill:false ~padding:5 w)
363 ~label:"Try constants only" () in
365 GButton.button ~label:"Check"
366 ~packing:(hbox#pack ~padding:5) () in
367 let _ = checkb#misc#set_sensitive false in
369 GButton.button ~label:"Abort"
370 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
372 let check_callback () =
373 assert (List.length !choices > 0) ;
374 check_window (outputhtml ()) !choices
376 ignore (window#connect#destroy GMain.Main.quit) ;
377 ignore (cancelb#connect#clicked window#destroy) ;
379 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
381 (nonvarsb#connect#clicked
383 use_only_constants := true ;
387 ignore (checkb#connect#clicked check_callback) ;
389 (clist#connect#select_row
390 (fun ~row ~column ~event ->
391 checkb#misc#set_sensitive true ;
392 okb#misc#set_sensitive true ;
393 choices := (List.nth uris row)::!choices)) ;
395 (clist#connect#unselect_row
396 (fun ~row ~column ~event ->
398 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
400 (manual_input#connect#changed
402 if manual_input#text = "" then
405 checkb#misc#set_sensitive false ;
406 okb#misc#set_sensitive false ;
407 clist#misc#set_sensitive true
411 choices := [manual_input#text] ;
412 clist#unselect_all () ;
413 checkb#misc#set_sensitive true ;
414 okb#misc#set_sensitive true ;
415 clist#misc#set_sensitive false
417 window#set_position `CENTER ;
421 if !use_only_constants then
423 (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
426 if List.length !choices > 0 then !choices else raise NoChoice
431 let interactive_interpretation_choice interpretations =
432 let chosen = ref None in
435 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
436 let vbox = GPack.vbox ~packing:window#add () in
440 ("Ambiguous input since there are many well-typed interpretations." ^
441 " Please, choose one of them.")
442 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
444 GPack.notebook ~scrollable:true
445 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
448 (function interpretation ->
450 let expected_height = 18 * List.length interpretation in
451 let height = if expected_height > 400 then 400 else expected_height in
452 GList.clist ~columns:2 ~packing:notebook#append_page ~height
453 ~titles:["id" ; "URI"] ()
457 (function (id,uri) ->
458 let n = clist#append [id;uri] in
459 clist#set_row ~selectable:false n
462 clist#columns_autosize ()
465 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
467 GButton.button ~label:"Ok"
468 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
470 GButton.button ~label:"Abort"
471 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
473 ignore (window#connect#destroy GMain.Main.quit) ;
474 ignore (cancelb#connect#clicked window#destroy) ;
477 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
478 window#set_position `CENTER ;
482 None -> raise NoChoice
489 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
491 let query = ref "" in
492 MQueryGenerator.set_confirm_query
493 (function q -> query := MQueryUtil.text_of_query q ; true) ;
494 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
497 let domImpl = Gdome.domImplementation ();;
499 let parseStyle name =
501 domImpl#createDocumentFromURI
503 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
505 ~uri:("styles/" ^ name) ()
507 Gdome_xslt.processStylesheet style
510 let d_c = parseStyle "drop_coercions.xsl";;
511 let tc1 = parseStyle "objtheorycontent.xsl";;
512 let hc2 = parseStyle "content_to_html.xsl";;
513 let l = parseStyle "link.xsl";;
515 let c1 = parseStyle "rootcontent.xsl";;
516 let g = parseStyle "genmmlid.xsl";;
517 let c2 = parseStyle "annotatedpres.xsl";;
520 let getterURL = Configuration.getter_url;;
521 let processorURL = Configuration.processor_url;;
523 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
524 let mml_args ~explode_all =
525 ("explodeall",(if explode_all then "true()" else "false()"))::
526 ["processorURL", "'" ^ processorURL ^ "'" ;
527 "getterURL", "'" ^ getterURL ^ "'" ;
528 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
529 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
530 "UNICODEvsSYMBOL", "'symbol'" ;
531 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
532 "encoding", "'iso-8859-1'" ;
533 "media-type", "'text/html'" ;
534 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
535 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
536 "naturalLanguage", "'yes'" ;
537 "annotations", "'no'" ;
538 "URLs_or_URIs", "'URIs'" ;
539 "topurl", "'http://phd.cs.unibo.it/helm'" ;
540 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
543 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
545 ["processorURL", "'" ^ processorURL ^ "'" ;
546 "getterURL", "'" ^ getterURL ^ "'" ;
547 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
548 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
549 "UNICODEvsSYMBOL", "'symbol'" ;
550 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
551 "encoding", "'iso-8859-1'" ;
552 "media-type", "'text/html'" ;
553 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
554 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
555 "naturalLanguage", "'no'" ;
556 "annotations", "'no'" ;
557 "explodeall", "true()" ;
558 "URLs_or_URIs", "'URIs'" ;
559 "topurl", "'http://phd.cs.unibo.it/helm'" ;
560 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
563 let parse_file filename =
564 let inch = open_in filename in
565 let rec read_lines () =
567 let line = input_line inch in
575 let applyStylesheets input styles args =
576 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
581 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
583 (*CSC: ????????????????? *)
585 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
589 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
590 ~ask_dtd_to_the_getter:true
594 None -> Xml2Gdome.document_of_xml domImpl xml
596 Xml.pp xml (Some constanttypefile) ;
597 Xml2Gdome.document_of_xml domImpl bodyxml'
599 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
600 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
602 Xml.pp xmlinnertypes (Some innertypesfile) ;
603 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
608 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
611 let struri = UriManager.string_of_uri uri in
612 let idx = (String.rindex struri '/') + 1 in
613 String.sub struri idx (String.length struri - idx)
615 let path = pathname ^ "/" ^ name in
617 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
621 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
622 ~ask_dtd_to_the_getter:false
625 let innertypesuri = UriManager.innertypesuri_of_uri uri in
626 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
627 Getter.register innertypesuri
628 (Configuration.annotations_url ^
629 Str.replace_first (Str.regexp "^cic:") ""
630 (UriManager.string_of_uri innertypesuri) ^ ".xml"
632 (* constant type / variable / mutual inductive types definition *)
633 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
635 (Configuration.annotations_url ^
636 Str.replace_first (Str.regexp "^cic:") ""
637 (UriManager.string_of_uri uri) ^ ".xml"
644 match UriManager.bodyuri_of_uri uri with
646 | Some bodyuri -> bodyuri
648 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
649 Getter.register bodyuri
650 (Configuration.annotations_url ^
651 Str.replace_first (Str.regexp "^cic:") ""
652 (UriManager.string_of_uri bodyuri) ^ ".xml"
659 exception RefreshSequentException of exn;;
660 exception RefreshProofException of exn;;
662 let refresh_proof (output : GMathView.math_view) =
664 let uri,currentproof =
665 match !ProofEngine.proof with
667 | Some (uri,metasenv,bo,ty) ->
668 !qed_set_sensitive (List.length metasenv = 0) ;
669 (*CSC: Wrong: [] is just plainly wrong *)
670 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
673 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
674 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
676 Cic2acic.acic_object_of_cic_object currentproof
679 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
682 output#load_tree mml ;
684 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
687 match !ProofEngine.proof with
689 | Some (uri,metasenv,bo,ty) ->
690 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
691 raise (RefreshProofException e)
694 let refresh_sequent ?(empty_notebook=true) notebook =
696 match !ProofEngine.goal with
698 if empty_notebook then
700 notebook#remove_all_pages ~skip_switch_page_event:false ;
701 notebook#set_empty_page
704 notebook#proofw#unload
707 match !ProofEngine.proof with
709 | Some (_,metasenv,_,_) -> metasenv
711 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
712 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
713 SequentPp.XmlPp.print_sequent metasenv currentsequent
715 let regenerate_notebook () =
716 let skip_switch_page_event =
718 (m,_,_)::_ when m = metano -> false
721 notebook#remove_all_pages ~skip_switch_page_event ;
722 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
724 if empty_notebook then
726 regenerate_notebook () ;
727 notebook#set_current_page ~may_skip_switch_page_event:false metano
731 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
733 applyStylesheets sequent_doc sequent_styles sequent_args
735 notebook#set_current_page ~may_skip_switch_page_event:true metano;
736 notebook#proofw#load_tree ~dom:sequent_mml
738 current_goal_infos :=
739 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
743 match !ProofEngine.goal with
748 match !ProofEngine.proof with
750 | Some (_,metasenv,_,_) -> metasenv
753 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
754 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
755 raise (RefreshSequentException e)
756 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
760 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
761 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
764 let mml_of_cic_term metano term =
766 match !ProofEngine.proof with
768 | Some (_,metasenv,_,_) -> metasenv
771 match !ProofEngine.goal with
774 let (_,canonical_context,_) =
775 List.find (function (m,_,_) -> m=metano) metasenv
779 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
780 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
783 Xml2Gdome.document_of_xml domImpl sequent_gdome
786 applyStylesheets sequent_doc sequent_styles sequent_args ;
788 current_scratch_infos :=
789 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
793 exception OpenConjecturesStillThere;;
794 exception WrongProof;;
796 let pathname_of_annuri uristring =
797 Configuration.annotations_dir ^
798 Str.replace_first (Str.regexp "^cic:") "" uristring
801 let make_dirs dirpath =
802 ignore (Unix.system ("mkdir -p " ^ dirpath))
805 let save_obj uri obj =
807 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
808 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
810 Cic2acic.acic_object_of_cic_object obj
812 (* let's save the theorem and register it to the getter *)
813 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
815 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
820 match !ProofEngine.proof with
822 | Some (uri,[],bo,ty) ->
824 CicReduction.are_convertible []
825 (CicTypeChecker.type_of_aux' [] [] bo) ty
828 (*CSC: Wrong: [] is just plainly wrong *)
829 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
831 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
832 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
834 Cic2acic.acic_object_of_cic_object proof
837 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
840 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
841 !qed_set_sensitive false ;
842 (* let's save the theorem and register it to the getter *)
843 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
845 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
849 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
854 | _ -> raise OpenConjecturesStillThere
858 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
859 match !ProofEngine.proof with
861 | Some (uri, metasenv, bo, ty) ->
863 (*CSC: Wrong: [] is just plainly wrong *)
864 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
866 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
867 Cic2acic.acic_object_of_cic_object currentproof
871 Cic2Xml.print_object uri ~ids_to_inner_sorts
872 ~ask_dtd_to_the_getter:true acurrentproof
874 xml,Some bodyxml -> xml,bodyxml
875 | _,None -> assert false
877 Xml.pp ~quiet:true xml (Some prooffiletype) ;
878 output_html outputhtml
879 ("<h1 color=\"Green\">Current proof type saved to " ^
880 prooffiletype ^ "</h1>") ;
881 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
882 output_html outputhtml
883 ("<h1 color=\"Green\">Current proof body saved to " ^
887 (* Used to typecheck the loaded proofs *)
888 let typecheck_loaded_proof metasenv bo ty =
889 let module T = CicTypeChecker in
892 (fun metasenv ((_,context,ty) as conj) ->
893 ignore (T.type_of_aux' metasenv context ty) ;
896 ignore (T.type_of_aux' metasenv [] ty) ;
897 ignore (T.type_of_aux' metasenv [] bo)
901 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
902 let output = ((rendering_window ())#output : GMathView.math_view) in
903 let notebook = (rendering_window ())#notebook in
906 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
909 None -> raise NoChoice
911 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
912 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
913 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
914 typecheck_loaded_proof metasenv bo ty ;
916 Some (uri, metasenv, bo, ty) ;
920 | (metano,_,_)::_ -> Some metano
922 refresh_proof output ;
923 refresh_sequent notebook ;
924 output_html outputhtml
925 ("<h1 color=\"Green\">Current proof type loaded from " ^
926 prooffiletype ^ "</h1>") ;
927 output_html outputhtml
928 ("<h1 color=\"Green\">Current proof body loaded from " ^
929 prooffile ^ "</h1>") ;
930 !save_set_sensitive true
933 RefreshSequentException e ->
934 output_html outputhtml
935 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
936 "sequent: " ^ Printexc.to_string e ^ "</h1>")
937 | RefreshProofException e ->
938 output_html outputhtml
939 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
940 "proof: " ^ Printexc.to_string e ^ "</h1>")
942 output_html outputhtml
943 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
946 let edit_aliases () =
947 let chosen = ref false in
950 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
952 GPack.vbox ~border_width:0 ~packing:window#add () in
953 let scrolled_window =
954 GBin.scrolled_window ~border_width:10
955 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
956 let input = GEdit.text ~editable:true ~width:400 ~height:100
957 ~packing:scrolled_window#add () in
959 GPack.hbox ~border_width:0
960 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
962 GButton.button ~label:"Ok"
963 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
965 GButton.button ~label:"Cancel"
966 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
967 ignore (window#connect#destroy GMain.Main.quit) ;
968 ignore (cancelb#connect#clicked window#destroy) ;
970 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
971 let dom,resolve_id = !id_to_uris in
973 (input#insert_text ~pos:0
978 match resolve_id v with
983 (string_of_cic_textual_parser_uri uri)
989 let inputtext = input#get_chars 0 input#length in
991 let alfa = "[a-zA-Z_-]" in
992 let digit = "[0-9]" in
993 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
994 let blanks = "\( \|\t\|\n\)+" in
995 let nonblanks = "[^ \t\n]+" in
996 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
998 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
1002 let n' = Str.search_forward regexpr inputtext n in
1003 let id = Str.matched_group 2 inputtext in
1005 cic_textual_parser_uri_of_string
1006 ("cic:" ^ (Str.matched_group 5 inputtext))
1008 let dom,resolve_id = aux (n' + 1) in
1009 if List.mem id dom then
1013 (function id' -> if id = id' then Some uri else resolve_id id')
1015 Not_found -> empty_id_to_uris
1019 id_to_uris := dom,resolve_id
1023 let module L = LogicalOperations in
1024 let module G = Gdome in
1025 let notebook = (rendering_window ())#notebook in
1026 let output = (rendering_window ())#output in
1027 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1028 match (rendering_window ())#output#get_selection with
1031 ((node : Gdome.element)#getAttributeNS
1032 (*CSC: OCAML DIVERGE
1033 ((element : G.element)#getAttributeNS
1035 ~namespaceURI:helmns
1036 ~localName:(G.domString "xref"))#to_string
1038 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1042 match !current_cic_infos with
1043 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1045 L.to_sequent id ids_to_terms ids_to_father_ids ;
1046 refresh_proof output ;
1047 refresh_sequent notebook
1048 | None -> assert false (* "ERROR: No current term!!!" *)
1050 RefreshSequentException e ->
1051 output_html outputhtml
1052 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1053 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1054 | RefreshProofException e ->
1055 output_html outputhtml
1056 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1057 "proof: " ^ Printexc.to_string e ^ "</h1>")
1059 output_html outputhtml
1060 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1062 | None -> assert false (* "ERROR: No selection!!!" *)
1066 let module L = LogicalOperations in
1067 let module G = Gdome in
1068 let notebook = (rendering_window ())#notebook in
1069 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1070 match (rendering_window ())#output#get_selection with
1073 ((node : Gdome.element)#getAttributeNS
1074 (*CSC: OCAML DIVERGE
1075 ((element : G.element)#getAttributeNS
1077 ~namespaceURI:helmns
1078 ~localName:(G.domString "xref"))#to_string
1080 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1084 match !current_cic_infos with
1085 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1087 L.focus id ids_to_terms ids_to_father_ids ;
1088 refresh_sequent notebook
1089 | None -> assert false (* "ERROR: No current term!!!" *)
1091 RefreshSequentException e ->
1092 output_html outputhtml
1093 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1094 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1095 | RefreshProofException e ->
1096 output_html outputhtml
1097 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1098 "proof: " ^ Printexc.to_string e ^ "</h1>")
1100 output_html outputhtml
1101 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1103 | None -> assert false (* "ERROR: No selection!!!" *)
1106 exception NoPrevGoal;;
1107 exception NoNextGoal;;
1109 let setgoal metano =
1110 let module L = LogicalOperations in
1111 let module G = Gdome in
1112 let notebook = (rendering_window ())#notebook in
1113 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1115 match !ProofEngine.proof with
1116 None -> assert false
1117 | Some (_,metasenv,_,_) -> metasenv
1120 refresh_sequent ~empty_notebook:false notebook
1122 RefreshSequentException e ->
1123 output_html outputhtml
1124 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1125 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1127 output_html outputhtml
1128 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1132 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1135 GWindow.window ~width:800 ~border_width:2 () in
1136 let scrolled_window =
1137 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1139 GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1140 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1141 let href = Gdome.domString "href" in
1142 let show_in_show_window_obj uri obj =
1143 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1146 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1147 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1149 Cic2acic.acic_object_of_cic_object obj
1152 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1155 window#set_title (UriManager.string_of_uri uri) ;
1156 window#misc#hide () ; window#show () ;
1157 mmlwidget#load_tree mml ;
1160 output_html outputhtml
1161 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1163 let show_in_show_window_uri uri =
1164 let obj = CicEnvironment.get_obj uri in
1165 show_in_show_window_obj uri obj
1167 let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1168 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1170 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1172 show_in_show_window_uri (UriManager.uri_of_string uri)
1174 if mmlwidget#get_action <> None then
1175 mmlwidget#action_toggle
1178 mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1180 show_in_show_window_obj, show_in_show_window_uri,
1181 show_in_show_window_callback
1184 exception NoObjectsLocated;;
1186 let user_uri_choice ~title ~msg uris =
1189 [] -> raise NoObjectsLocated
1193 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1198 String.sub uri 4 (String.length uri - 4)
1201 let locate_callback id =
1202 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1203 let result = MQueryGenerator.locate id in
1206 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1209 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1211 output_html outputhtml html ;
1212 user_uri_choice ~title:"Ambiguous input."
1214 ("Ambiguous input \"" ^ id ^
1215 "\". Please, choose one interpetation:")
1220 let inputt = ((rendering_window ())#inputt : term_editor) in
1221 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1224 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1226 None -> raise NoChoice
1228 let uri = locate_callback input in
1232 output_html outputhtml
1233 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1236 let input_or_locate_uri ~title =
1237 let uri = ref None in
1240 ~width:400 ~modal:true ~title ~border_width:2 () in
1241 let vbox = GPack.vbox ~packing:window#add () in
1243 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1245 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1247 GEdit.entry ~editable:true
1248 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1250 GButton.button ~label:"Check"
1251 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1252 let _ = checkb#misc#set_sensitive false in
1254 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1256 GMisc.label ~text:"You can also enter an indentifier to locate:"
1257 ~packing:(hbox2#pack ~padding:5) () in
1259 GEdit.entry ~editable:true
1260 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1262 GButton.button ~label:"Locate"
1263 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1264 let _ = locateb#misc#set_sensitive false in
1266 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1268 GButton.button ~label:"Ok"
1269 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1270 let _ = okb#misc#set_sensitive false in
1272 GButton.button ~label:"Cancel"
1273 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1275 ignore (window#connect#destroy GMain.Main.quit) ;
1277 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1278 let check_callback () =
1279 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1280 let uri = "cic:" ^ manual_input#text in
1282 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1283 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1286 Getter.Unresolved ->
1287 output_html outputhtml
1288 ("<h1 color=\"Red\">URI " ^ uri ^
1289 " does not correspond to any object.</h1>") ;
1291 | UriManager.IllFormedUri _ ->
1292 output_html outputhtml
1293 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1296 output_html outputhtml
1297 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1301 (okb#connect#clicked
1303 if check_callback () then
1305 uri := Some manual_input#text ;
1309 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1311 (manual_input#connect#changed
1313 if manual_input#text = "" then
1315 checkb#misc#set_sensitive false ;
1316 okb#misc#set_sensitive false
1320 checkb#misc#set_sensitive true ;
1321 okb#misc#set_sensitive true
1324 (locate_input#connect#changed
1325 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1327 (locateb#connect#clicked
1329 let id = locate_input#text in
1330 manual_input#set_text (locate_callback id) ;
1331 locate_input#delete_text 0 (String.length id)
1334 GMain.Main.main () ;
1336 None -> raise NoChoice
1337 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1340 let locate_one_id id =
1341 let result = MQueryGenerator.locate id in
1345 wrong_xpointer_format_from_wrong_xpointer_format' uri
1347 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1348 output_html (rendering_window ())#outputhtml html ;
1352 [UriManager.string_of_uri
1353 (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1356 interactive_user_uri_choice
1357 ~selection_mode:`EXTENDED
1358 ~ok:"Try every selection."
1359 ~enable_button_for_non_vars:true
1360 ~title:"Ambiguous input."
1362 ("Ambiguous input \"" ^ id ^
1363 "\". Please, choose one or more interpretations:")
1366 List.map cic_textual_parser_uri_of_string uris'
1369 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1370 exception AmbiguousInput;;
1372 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1373 let known_ids,resolve_id = !id_to_uris in
1379 if List.mem he known_ids then filter tl else he::(filter tl)
1383 (* for each id in dom' we get the list of uris associated to it *)
1384 let list_of_uris = List.map locate_one_id dom' in
1385 (* and now we compute the list of all possible assignments from id to uris *)
1387 let rec aux ids list_of_uris =
1388 match ids,list_of_uris with
1389 [],[] -> [resolve_id]
1390 | id::idtl,uris::uristl ->
1391 let resolves = aux idtl uristl in
1397 function id' -> if id = id' then Some uri else f id'
1401 | _,_ -> assert false
1403 aux dom' list_of_uris
1405 let tests_no = List.length resolve_ids in
1406 if tests_no > 1 then
1407 output_html (outputhtml ())
1408 ("<h1>Disambiguation phase started: " ^
1409 string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1410 (* now we select only the ones that generates well-typed terms *)
1416 let metasenv',expr = mk_metasenv_and_expr resolve in
1418 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1420 (CicTypeChecker.type_of_aux' metasenv context expr) ;
1421 resolve::(filter tl)
1428 match resolve_ids' with
1429 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1430 | [resolve_id] -> resolve_id
1434 (function resolve ->
1438 match resolve id with
1439 None -> assert false
1442 CicTextualParser0.ConUri uri
1443 | CicTextualParser0.VarUri uri ->
1444 UriManager.string_of_uri uri
1445 | CicTextualParser0.IndTyUri (uri,tyno) ->
1446 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1447 string_of_int (tyno+1) ^ ")"
1448 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1449 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1450 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
1454 let index = interactive_interpretation_choice choices in
1455 List.nth resolve_ids' index
1457 id_to_uris := known_ids @ dom', resolve_id' ;
1458 mk_metasenv_and_expr resolve_id'
1461 exception UriAlreadyInUse;;
1462 exception NotAUriToAConstant;;
1464 let new_inductive () =
1465 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1466 let output = ((rendering_window ())#output : GMathView.math_view) in
1467 let notebook = (rendering_window ())#notebook in
1469 let chosen = ref false in
1470 let inductive = ref true in
1471 let paramsno = ref 0 in
1472 let get_uri = ref (function _ -> assert false) in
1473 let get_base_uri = ref (function _ -> assert false) in
1474 let get_names = ref (function _ -> assert false) in
1475 let get_types_and_cons = ref (function _ -> assert false) in
1476 let get_name_context_context_and_subst = ref (function _ -> assert false) in
1479 ~width:600 ~modal:true ~position:`CENTER
1480 ~title:"New Block of Mutual (Co)Inductive Definitions"
1481 ~border_width:2 () in
1482 let vbox = GPack.vbox ~packing:window#add () in
1484 GPack.hbox ~border_width:0
1485 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1487 GMisc.label ~text:"Enter the URI for the new block:"
1488 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1490 GEdit.entry ~editable:true
1491 ~packing:(hbox#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
1498 "Enter the number of left parameters in every arity and constructor type:"
1499 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1500 let paramsno_entry =
1501 GEdit.entry ~editable:true ~text:"0"
1502 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1504 GPack.hbox ~border_width:0
1505 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1507 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1508 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1510 GButton.radio_button ~label:"Inductive"
1511 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1513 GButton.radio_button ~label:"Coinductive"
1514 ~group:inductiveb#group
1515 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1517 GPack.hbox ~border_width:0
1518 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1520 GMisc.label ~text:"Enter the list of the names of the types:"
1521 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1523 GEdit.entry ~editable:true
1524 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1526 GPack.hbox ~border_width:0
1527 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1529 GButton.button ~label:"> Next"
1530 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1531 let _ = okb#misc#set_sensitive true in
1533 GButton.button ~label:"Abort"
1534 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1535 ignore (window#connect#destroy GMain.Main.quit) ;
1536 ignore (cancelb#connect#clicked window#destroy) ;
1540 (okb#connect#clicked
1543 let uristr = "cic:" ^ uri_entry#text in
1544 let namesstr = names_entry#text in
1545 let paramsno' = int_of_string (paramsno_entry#text) in
1546 match Str.split (Str.regexp " +") namesstr with
1548 | (he::tl) as names ->
1549 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1552 ignore (Getter.resolve uri) ;
1553 raise UriAlreadyInUse
1555 Getter.Unresolved ->
1556 get_uri := (function () -> uri) ;
1557 get_names := (function () -> names) ;
1558 inductive := inductiveb#active ;
1559 paramsno := paramsno' ;
1564 output_html outputhtml
1565 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1573 GBin.frame ~label:name
1574 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1575 let vbox = GPack.vbox ~packing:frame#add () in
1576 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1578 GMisc.label ~text:("Enter its type:")
1579 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1580 let scrolled_window =
1581 GBin.scrolled_window ~border_width:5
1582 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1584 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1585 ~isnotempty_callback:
1587 (*non_empty_type := b ;*)
1588 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1591 GPack.hbox ~border_width:0
1592 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1594 GMisc.label ~text:("Enter the list of its constructors:")
1595 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1596 let cons_names_entry =
1597 GEdit.entry ~editable:true
1598 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1599 (newinputt,cons_names_entry)
1602 vbox#remove hboxn#coerce ;
1604 GPack.hbox ~border_width:0
1605 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1607 GButton.button ~label:"> Next"
1608 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1610 GButton.button ~label:"Abort"
1611 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1612 ignore (cancelb#connect#clicked window#destroy) ;
1614 (okb#connect#clicked
1617 let names = !get_names () in
1618 let types_and_cons =
1620 (fun name (newinputt,cons_names_entry) ->
1621 let dom,mk_metasenv_and_expr =
1622 newinputt#get_term ~context:[] ~metasenv:[] in
1623 let consnamesstr = cons_names_entry#text in
1624 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1626 disambiguate_input [] [] dom mk_metasenv_and_expr
1629 [] -> expr,cons_names
1630 | _ -> raise AmbiguousInput
1631 ) names type_widgets
1633 (* Let's see if so far the definition is well-typed *)
1634 let uri = !get_uri () in
1640 (fun name (ty,cons) ->
1643 (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in
1644 let res = (name, !inductive, ty, cons') in
1647 ) names types_and_cons
1649 (*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi
1650 anche quando paramsno > 0 ;-((((
1651 CicTypeChecker.typecheck_mutual_inductive_defs uri
1652 (tys,params,paramsno) ;
1654 get_name_context_context_and_subst :=
1658 (fun (namecontext,context,subst) name (ty,_) ->
1660 (Some (Cic.Name name))::namecontext,
1661 (Some (Cic.Name name, Cic.Decl ty))::context,
1662 (Cic.MutInd (uri,!i,[]))::subst
1665 ) ([],[],[]) names types_and_cons) ;
1666 let types_and_cons' =
1668 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1669 names types_and_cons
1671 get_types_and_cons := (function () -> types_and_cons') ;
1676 output_html outputhtml
1677 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1680 and phase3 name cons =
1681 let get_cons_types = ref (function () -> assert false) in
1684 ~width:600 ~modal:true ~position:`CENTER
1685 ~title:(name ^ " Constructors")
1686 ~border_width:2 () in
1687 let vbox = GPack.vbox ~packing:window2#add () in
1688 let cons_type_widgets =
1690 (function consname ->
1692 GPack.hbox ~border_width:0
1693 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1695 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1696 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1697 let scrolled_window =
1698 GBin.scrolled_window ~border_width:5
1699 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1701 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1702 ~isnotempty_callback:
1704 (* (*non_empty_type := b ;*)
1705 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1710 GPack.hbox ~border_width:0
1711 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1713 GButton.button ~label:"> Next"
1714 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1715 let _ = okb#misc#set_sensitive true in
1717 GButton.button ~label:"Abort"
1718 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1719 ignore (window2#connect#destroy GMain.Main.quit) ;
1720 ignore (cancelb#connect#clicked window2#destroy) ;
1722 (okb#connect#clicked
1726 let namecontext,context,subst= !get_name_context_context_and_subst () in
1730 let dom,mk_metasenv_and_expr =
1731 inputt#get_term ~context:namecontext ~metasenv:[]
1734 disambiguate_input context [] dom mk_metasenv_and_expr
1738 let undebrujined_expr =
1740 (fun expr t -> CicSubstitution.subst t expr) expr subst
1742 name, undebrujined_expr
1743 | _ -> raise AmbiguousInput
1744 ) cons cons_type_widgets
1746 get_cons_types := (function () -> cons_types) ;
1750 output_html outputhtml
1751 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1754 GMain.Main.main () ;
1755 let okb_pressed = !chosen in
1757 if (not okb_pressed) then
1760 assert false (* The control never reaches this point *)
1763 (!get_cons_types ())
1766 (* No more phases left or Abort pressed *)
1768 GMain.Main.main () ;
1772 let uri = !get_uri () in
1775 let tys = !get_types_and_cons () in
1776 let obj = Cic.InductiveDefinition tys params !paramsno in
1779 prerr_endline (CicPp.ppobj obj) ;
1780 CicTypeChecker.typecheck_mutual_inductive_defs uri
1781 (tys,params,!paramsno) ;
1784 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1785 prerr_endline (CicPp.ppobj obj) ;
1787 (* We already know that obj is well-typed. We need to add it to the *)
1788 (* environment in order to compute the inner-types without having to *)
1789 (* debrujin it or having to modify lots of other functions to avoid *)
1790 (* asking the environment for the MUTINDs we are defining now. *)
1791 CicEnvironment.put_inductive_definition uri obj ;
1793 show_in_show_window_obj uri obj
1796 output_html outputhtml
1797 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1801 let inputt = ((rendering_window ())#inputt : term_editor) in
1802 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1803 let output = ((rendering_window ())#output : GMathView.math_view) in
1804 let notebook = (rendering_window ())#notebook in
1806 let chosen = ref false in
1807 let get_parsed = ref (function _ -> assert false) in
1808 let get_uri = ref (function _ -> assert false) in
1809 let non_empty_type = ref false in
1812 ~width:600 ~modal:true ~title:"New Proof or Definition"
1813 ~border_width:2 () in
1814 let vbox = GPack.vbox ~packing:window#add () in
1816 GPack.hbox ~border_width:0
1817 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1819 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1820 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1822 GEdit.entry ~editable:true
1823 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1825 GPack.hbox ~border_width:0
1826 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1828 GMisc.label ~text:"Enter the theorem or definition type:"
1829 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1830 let scrolled_window =
1831 GBin.scrolled_window ~border_width:5
1832 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1833 (* the content of the scrolled_window is moved below (see comment) *)
1835 GPack.hbox ~border_width:0
1836 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1838 GButton.button ~label:"Ok"
1839 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1840 let _ = okb#misc#set_sensitive false in
1842 GButton.button ~label:"Cancel"
1843 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1844 (* moved here to have visibility of the ok button *)
1846 new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1847 ~isnotempty_callback:
1849 non_empty_type := b ;
1850 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1853 newinputt#set_term inputt#get_as_string ;
1856 uri_entry#connect#changed
1858 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1860 ignore (window#connect#destroy GMain.Main.quit) ;
1861 ignore (cancelb#connect#clicked window#destroy) ;
1863 (okb#connect#clicked
1867 let parsed = newinputt#get_term [] [] in
1868 let uristr = "cic:" ^ uri_entry#text in
1869 let uri = UriManager.uri_of_string uristr in
1870 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1871 raise NotAUriToAConstant
1875 ignore (Getter.resolve uri) ;
1876 raise UriAlreadyInUse
1878 Getter.Unresolved ->
1879 get_parsed := (function () -> parsed) ;
1880 get_uri := (function () -> uri) ;
1885 output_html outputhtml
1886 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1889 GMain.Main.main () ;
1892 let dom,mk_metasenv_and_expr = !get_parsed () in
1894 disambiguate_input [] [] dom mk_metasenv_and_expr
1896 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1897 ProofEngine.proof :=
1898 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1899 ProofEngine.goal := Some 1 ;
1900 refresh_sequent notebook ;
1901 refresh_proof output ;
1902 !save_set_sensitive true ;
1905 RefreshSequentException e ->
1906 output_html outputhtml
1907 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1908 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1909 | RefreshProofException e ->
1910 output_html outputhtml
1911 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1912 "proof: " ^ Printexc.to_string e ^ "</h1>")
1914 output_html outputhtml
1915 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1918 let check_term_in_scratch scratch_window metasenv context expr =
1920 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1921 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1922 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1923 scratch_window#show () ;
1924 scratch_window#mmlwidget#load_tree ~dom:mml
1927 print_endline ("? " ^ CicPp.ppterm expr) ;
1931 let check scratch_window () =
1932 let inputt = ((rendering_window ())#inputt : term_editor) in
1933 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1935 match !ProofEngine.proof with
1937 | Some (_,metasenv,_,_) -> metasenv
1939 let context,names_context =
1941 match !ProofEngine.goal with
1944 let (_,canonical_context,_) =
1945 List.find (function (m,_,_) -> m=metano) metasenv
1952 Some (n,_) -> Some n
1957 let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1958 let (metasenv',expr) =
1959 disambiguate_input context metasenv dom mk_metasenv_and_expr
1961 check_term_in_scratch scratch_window metasenv' context expr
1964 output_html outputhtml
1965 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1969 (***********************)
1971 (***********************)
1973 let call_tactic tactic () =
1974 let notebook = (rendering_window ())#notebook in
1975 let output = ((rendering_window ())#output : GMathView.math_view) in
1976 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1977 let savedproof = !ProofEngine.proof in
1978 let savedgoal = !ProofEngine.goal in
1982 refresh_sequent notebook ;
1983 refresh_proof output
1985 RefreshSequentException e ->
1986 output_html outputhtml
1987 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1988 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1989 ProofEngine.proof := savedproof ;
1990 ProofEngine.goal := savedgoal ;
1991 refresh_sequent notebook
1992 | RefreshProofException e ->
1993 output_html outputhtml
1994 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1995 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1996 ProofEngine.proof := savedproof ;
1997 ProofEngine.goal := savedgoal ;
1998 refresh_sequent notebook ;
1999 refresh_proof output
2001 output_html outputhtml
2002 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2003 ProofEngine.proof := savedproof ;
2004 ProofEngine.goal := savedgoal ;
2008 let call_tactic_with_input tactic () =
2009 let notebook = (rendering_window ())#notebook in
2010 let output = ((rendering_window ())#output : GMathView.math_view) in
2011 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2012 let inputt = ((rendering_window ())#inputt : term_editor) in
2013 let savedproof = !ProofEngine.proof in
2014 let savedgoal = !ProofEngine.goal in
2015 let uri,metasenv,bo,ty =
2016 match !ProofEngine.proof with
2017 None -> assert false
2018 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2020 let canonical_context =
2021 match !ProofEngine.goal with
2022 None -> assert false
2024 let (_,canonical_context,_) =
2025 List.find (function (m,_,_) -> m=metano) metasenv
2032 Some (n,_) -> Some n
2037 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
2038 let (metasenv',expr) =
2039 disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
2041 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2043 refresh_sequent notebook ;
2044 refresh_proof output ;
2047 RefreshSequentException e ->
2048 output_html outputhtml
2049 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2050 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2051 ProofEngine.proof := savedproof ;
2052 ProofEngine.goal := savedgoal ;
2053 refresh_sequent notebook
2054 | RefreshProofException e ->
2055 output_html outputhtml
2056 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2057 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2058 ProofEngine.proof := savedproof ;
2059 ProofEngine.goal := savedgoal ;
2060 refresh_sequent notebook ;
2061 refresh_proof output
2063 output_html outputhtml
2064 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2065 ProofEngine.proof := savedproof ;
2066 ProofEngine.goal := savedgoal ;
2069 let call_tactic_with_goal_input tactic () =
2070 let module L = LogicalOperations in
2071 let module G = Gdome in
2072 let notebook = (rendering_window ())#notebook in
2073 let output = ((rendering_window ())#output : GMathView.math_view) in
2074 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2075 let savedproof = !ProofEngine.proof in
2076 let savedgoal = !ProofEngine.goal in
2077 match notebook#proofw#get_selection with
2080 ((node : Gdome.element)#getAttributeNS
2081 ~namespaceURI:helmns
2082 ~localName:(G.domString "xref"))#to_string
2084 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2088 match !current_goal_infos with
2089 Some (ids_to_terms, ids_to_father_ids,_) ->
2091 tactic (Hashtbl.find ids_to_terms id) ;
2092 refresh_sequent notebook ;
2093 refresh_proof output
2094 | None -> assert false (* "ERROR: No current term!!!" *)
2096 RefreshSequentException e ->
2097 output_html outputhtml
2098 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2099 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2100 ProofEngine.proof := savedproof ;
2101 ProofEngine.goal := savedgoal ;
2102 refresh_sequent notebook
2103 | RefreshProofException e ->
2104 output_html outputhtml
2105 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2106 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2107 ProofEngine.proof := savedproof ;
2108 ProofEngine.goal := savedgoal ;
2109 refresh_sequent notebook ;
2110 refresh_proof output
2112 output_html outputhtml
2113 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2114 ProofEngine.proof := savedproof ;
2115 ProofEngine.goal := savedgoal ;
2118 output_html outputhtml
2119 ("<h1 color=\"red\">No term selected</h1>")
2122 let call_tactic_with_input_and_goal_input tactic () =
2123 let module L = LogicalOperations in
2124 let module G = Gdome in
2125 let notebook = (rendering_window ())#notebook in
2126 let output = ((rendering_window ())#output : GMathView.math_view) in
2127 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2128 let inputt = ((rendering_window ())#inputt : term_editor) in
2129 let savedproof = !ProofEngine.proof in
2130 let savedgoal = !ProofEngine.goal in
2131 match notebook#proofw#get_selection with
2134 ((node : Gdome.element)#getAttributeNS
2135 ~namespaceURI:helmns
2136 ~localName:(G.domString "xref"))#to_string
2138 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2142 match !current_goal_infos with
2143 Some (ids_to_terms, ids_to_father_ids,_) ->
2145 let uri,metasenv,bo,ty =
2146 match !ProofEngine.proof with
2147 None -> assert false
2148 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2150 let canonical_context =
2151 match !ProofEngine.goal with
2152 None -> assert false
2154 let (_,canonical_context,_) =
2155 List.find (function (m,_,_) -> m=metano) metasenv
2157 canonical_context in
2161 Some (n,_) -> Some n
2165 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
2167 let (metasenv',expr) =
2168 disambiguate_input canonical_context metasenv dom
2169 mk_metasenv_and_expr
2171 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2172 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2174 refresh_sequent notebook ;
2175 refresh_proof output ;
2177 | None -> assert false (* "ERROR: No current term!!!" *)
2179 RefreshSequentException e ->
2180 output_html outputhtml
2181 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2182 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2183 ProofEngine.proof := savedproof ;
2184 ProofEngine.goal := savedgoal ;
2185 refresh_sequent notebook
2186 | RefreshProofException e ->
2187 output_html outputhtml
2188 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2189 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2190 ProofEngine.proof := savedproof ;
2191 ProofEngine.goal := savedgoal ;
2192 refresh_sequent notebook ;
2193 refresh_proof output
2195 output_html outputhtml
2196 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2197 ProofEngine.proof := savedproof ;
2198 ProofEngine.goal := savedgoal ;
2201 output_html outputhtml
2202 ("<h1 color=\"red\">No term selected</h1>")
2205 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2206 let module L = LogicalOperations in
2207 let module G = Gdome in
2208 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2209 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2210 let savedproof = !ProofEngine.proof in
2211 let savedgoal = !ProofEngine.goal in
2212 match mmlwidget#get_selection with
2215 ((node : Gdome.element)#getAttributeNS
2216 ~namespaceURI:helmns
2217 ~localName:(G.domString "xref"))#to_string
2219 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2223 match !current_scratch_infos with
2224 (* term is the whole goal in the scratch_area *)
2225 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2227 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2228 let mml = mml_of_cic_term 111 expr in
2229 scratch_window#show () ;
2230 scratch_window#mmlwidget#load_tree ~dom:mml
2231 | None -> assert false (* "ERROR: No current term!!!" *)
2234 output_html outputhtml
2235 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2238 output_html outputhtml
2239 ("<h1 color=\"red\">No term selected</h1>")
2242 let call_tactic_with_hypothesis_input tactic () =
2243 let module L = LogicalOperations in
2244 let module G = Gdome in
2245 let notebook = (rendering_window ())#notebook in
2246 let output = ((rendering_window ())#output : GMathView.math_view) in
2247 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2248 let savedproof = !ProofEngine.proof in
2249 let savedgoal = !ProofEngine.goal in
2250 match notebook#proofw#get_selection with
2253 ((node : Gdome.element)#getAttributeNS
2254 ~namespaceURI:helmns
2255 ~localName:(G.domString "xref"))#to_string
2257 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2261 match !current_goal_infos with
2262 Some (_,_,ids_to_hypotheses) ->
2264 tactic (Hashtbl.find ids_to_hypotheses id) ;
2265 refresh_sequent notebook ;
2266 refresh_proof output
2267 | None -> assert false (* "ERROR: No current term!!!" *)
2269 RefreshSequentException e ->
2270 output_html outputhtml
2271 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2272 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2273 ProofEngine.proof := savedproof ;
2274 ProofEngine.goal := savedgoal ;
2275 refresh_sequent notebook
2276 | RefreshProofException e ->
2277 output_html outputhtml
2278 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2279 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2280 ProofEngine.proof := savedproof ;
2281 ProofEngine.goal := savedgoal ;
2282 refresh_sequent notebook ;
2283 refresh_proof output
2285 output_html outputhtml
2286 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2287 ProofEngine.proof := savedproof ;
2288 ProofEngine.goal := savedgoal ;
2291 output_html outputhtml
2292 ("<h1 color=\"red\">No term selected</h1>")
2296 let intros = call_tactic ProofEngine.intros;;
2297 let exact = call_tactic_with_input ProofEngine.exact;;
2298 let apply = call_tactic_with_input ProofEngine.apply;;
2299 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2300 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2301 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2302 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2303 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2304 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2305 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2306 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2307 let cut = call_tactic_with_input ProofEngine.cut;;
2308 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2309 let letin = call_tactic_with_input ProofEngine.letin;;
2310 let ring = call_tactic ProofEngine.ring;;
2311 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2312 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2313 let fourier = call_tactic ProofEngine.fourier;;
2314 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2315 let reflexivity = call_tactic ProofEngine.reflexivity;;
2316 let symmetry = call_tactic ProofEngine.symmetry;;
2317 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2318 let exists = call_tactic ProofEngine.exists;;
2319 let split = call_tactic ProofEngine.split;;
2320 let left = call_tactic ProofEngine.left;;
2321 let right = call_tactic ProofEngine.right;;
2322 let assumption = call_tactic ProofEngine.assumption;;
2323 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2324 let absurd = call_tactic_with_input ProofEngine.absurd;;
2325 let contradiction = call_tactic ProofEngine.contradiction;;
2326 (* Galla: come dare alla tattica la lista di termini da decomporre?
2327 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
2330 let whd_in_scratch scratch_window =
2331 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2334 let reduce_in_scratch scratch_window =
2335 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2338 let simpl_in_scratch scratch_window =
2339 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2345 (**********************)
2346 (* END OF TACTICS *)
2347 (**********************)
2351 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2353 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2356 output_html outputhtml
2357 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2360 exception NotADefinition;;
2363 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2364 let output = ((rendering_window ())#output : GMathView.math_view) in
2365 let notebook = (rendering_window ())#notebook in
2367 let uri = input_or_locate_uri ~title:"Open" in
2368 CicTypeChecker.typecheck uri ;
2369 let metasenv,bo,ty =
2370 match CicEnvironment.get_cooked_obj uri with
2371 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2372 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2375 | Cic.InductiveDefinition _ -> raise NotADefinition
2377 ProofEngine.proof :=
2378 Some (uri, metasenv, bo, ty) ;
2379 ProofEngine.goal := None ;
2380 refresh_sequent notebook ;
2381 refresh_proof output
2383 RefreshSequentException e ->
2384 output_html outputhtml
2385 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2386 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2387 | RefreshProofException e ->
2388 output_html outputhtml
2389 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2390 "proof: " ^ Printexc.to_string e ^ "</h1>")
2392 output_html outputhtml
2393 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2396 let show_query_results results =
2399 ~modal:false ~title:"Query results." ~border_width:2 () in
2400 let vbox = GPack.vbox ~packing:window#add () in
2402 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2405 ~text:"Click on a URI to show that object"
2406 ~packing:hbox#add () in
2407 let scrolled_window =
2408 GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2409 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2410 let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2413 (function (uri,_) ->
2417 clist#set_row ~selectable:false n
2420 clist#columns_autosize () ;
2422 (clist#connect#select_row
2423 (fun ~row ~column ~event ->
2424 let (uristr,_) = List.nth results row in
2426 cic_textual_parser_uri_of_string
2427 (wrong_xpointer_format_from_wrong_xpointer_format' uristr)
2429 CicTextualParser0.ConUri uri
2430 | CicTextualParser0.VarUri uri
2431 | CicTextualParser0.IndTyUri (uri,_)
2432 | CicTextualParser0.IndConUri (uri,_,_) ->
2433 show_in_show_window_uri uri
2439 let refine_constraints (must_obj,must_rel,must_sort) =
2440 let chosen = ref false in
2441 let use_only = ref false in
2444 ~modal:true ~title:"Constraints refinement."
2445 ~width:800 ~border_width:2 () in
2446 let vbox = GPack.vbox ~packing:window#add () in
2448 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2451 ~text: "\"Only\" constraints can be enforced or not."
2452 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2454 GButton.toggle_button ~label:"Enforce \"only\" constraints"
2455 ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2458 (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2459 (* Notebook for the constraints choice *)
2461 GPack.notebook ~scrollable:true
2462 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2463 (* Rel constraints *)
2466 ~text: "Constraints on Rels" () in
2468 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2471 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2474 ~text: "You can now specify the constraints on Rels."
2475 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2476 let expected_height = 25 * (List.length must_rel + 2) in
2477 let height = if expected_height > 400 then 400 else expected_height in
2478 let scrolled_window =
2479 GBin.scrolled_window ~border_width:10 ~height ~width:600
2480 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2481 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2482 let rel_constraints =
2484 (function (position,depth) ->
2487 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2491 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2493 None -> position, ref None
2495 let mutable_ref = ref (Some depth') in
2497 GButton.toggle_button
2498 ~label:("depth = " ^ string_of_int depth') ~active:true
2499 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2502 (depthb#connect#toggled
2504 let sel_depth = if depthb#active then Some depth' else None in
2505 mutable_ref := sel_depth
2507 position, mutable_ref
2509 (* Sort constraints *)
2512 ~text: "Constraints on Sorts" () in
2514 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2517 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2520 ~text: "You can now specify the constraints on Sorts."
2521 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2522 let expected_height = 25 * (List.length must_sort + 2) in
2523 let height = if expected_height > 400 then 400 else expected_height in
2524 let scrolled_window =
2525 GBin.scrolled_window ~border_width:10 ~height ~width:600
2526 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2527 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2528 let sort_constraints =
2530 (function (position,depth,sort) ->
2533 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2536 ~text:(sort ^ " " ^ position)
2537 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2539 None -> position, ref None, sort
2541 let mutable_ref = ref (Some depth') in
2543 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2545 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2548 (depthb#connect#toggled
2550 let sel_depth = if depthb#active then Some depth' else None in
2551 mutable_ref := sel_depth
2553 position, mutable_ref, sort
2555 (* Obj constraints *)
2558 ~text: "Constraints on constants" () in
2560 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2563 GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2566 ~text: "You can now specify the constraints on constants."
2567 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2568 let expected_height = 25 * (List.length must_obj + 2) in
2569 let height = if expected_height > 400 then 400 else expected_height in
2570 let scrolled_window =
2571 GBin.scrolled_window ~border_width:10 ~height ~width:600
2572 ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2573 let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2574 let obj_constraints =
2576 (function (uri,position,depth) ->
2579 ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2582 ~text:(uri ^ " " ^ position)
2583 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2585 None -> uri, position, ref None
2587 let mutable_ref = ref (Some depth') in
2589 GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2591 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2594 (depthb#connect#toggled
2596 let sel_depth = if depthb#active then Some depth' else None in
2597 mutable_ref := sel_depth
2599 uri, position, mutable_ref
2601 (* Confirm/abort buttons *)
2603 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2605 GButton.button ~label:"Ok"
2606 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2608 GButton.button ~label:"Abort"
2609 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2611 ignore (window#connect#destroy GMain.Main.quit) ;
2612 ignore (cancelb#connect#clicked window#destroy) ;
2614 (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2615 window#set_position `CENTER ;
2617 GMain.Main.main () ;
2619 let chosen_must_rel =
2621 (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2622 let chosen_must_sort =
2624 (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2627 let chosen_must_obj =
2629 (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2632 (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2634 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2635 Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2643 let completeSearchPattern () =
2644 let inputt = ((rendering_window ())#inputt : term_editor) in
2645 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2647 let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
2648 let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
2649 let must = MQueryLevels2.get_constraints expr in
2650 let must',only = refine_constraints must in
2651 let results = MQueryGenerator.searchPattern must' only in
2652 show_query_results results
2655 output_html outputhtml
2656 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2659 let choose_must list_of_must only =
2660 let chosen = ref None in
2661 let user_constraints = ref [] in
2664 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2665 let vbox = GPack.vbox ~packing:window#add () in
2667 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2671 ("You can now specify the genericity of the query. " ^
2672 "The more generic the slower.")
2673 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2675 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2679 "Suggestion: start with faster queries before moving to more generic ones."
2680 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2682 GPack.notebook ~scrollable:true
2683 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2686 let last = List.length list_of_must in
2692 (if !page = 1 then "More generic" else
2693 if !page = last then "More precise" else " ") () in
2694 let expected_height = 25 * (List.length must + 2) in
2695 let height = if expected_height > 400 then 400 else expected_height in
2696 let scrolled_window =
2697 GBin.scrolled_window ~border_width:10 ~height ~width:600
2698 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2700 GList.clist ~columns:2 ~packing:scrolled_window#add
2701 ~titles:["URI" ; "Position"] ()
2705 (function (uri,position) ->
2708 [uri; if position then "MainConclusion" else "Conclusion"]
2710 clist#set_row ~selectable:false n
2713 clist#columns_autosize ()
2716 let label = GMisc.label ~text:"User provided" () in
2718 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2720 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2723 ~text:"Select the constraints that must be satisfied and press OK."
2724 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2725 let expected_height = 25 * (List.length only + 2) in
2726 let height = if expected_height > 400 then 400 else expected_height in
2727 let scrolled_window =
2728 GBin.scrolled_window ~border_width:10 ~height ~width:600
2729 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2731 GList.clist ~columns:2 ~packing:scrolled_window#add
2732 ~selection_mode:`EXTENDED
2733 ~titles:["URI" ; "Position"] ()
2737 (function (uri,position) ->
2740 [uri; if position then "MainConclusion" else "Conclusion"]
2742 clist#set_row ~selectable:true n
2745 clist#columns_autosize () ;
2747 (clist#connect#select_row
2748 (fun ~row ~column ~event ->
2749 user_constraints := (List.nth only row)::!user_constraints)) ;
2751 (clist#connect#unselect_row
2752 (fun ~row ~column ~event ->
2755 (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2758 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2760 GButton.button ~label:"Ok"
2761 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2763 GButton.button ~label:"Abort"
2764 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2766 ignore (window#connect#destroy GMain.Main.quit) ;
2767 ignore (cancelb#connect#clicked window#destroy) ;
2769 (okb#connect#clicked
2770 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2771 window#set_position `CENTER ;
2773 GMain.Main.main () ;
2775 None -> raise NoChoice
2777 if n = List.length list_of_must then
2778 (* user provided constraints *)
2781 List.nth list_of_must n
2784 let searchPattern () =
2785 let inputt = ((rendering_window ())#inputt : term_editor) in
2786 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2789 match !ProofEngine.proof with
2790 None -> assert false
2791 | Some (_,metasenv,_,_) -> metasenv
2793 match !ProofEngine.goal with
2796 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2797 let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2798 let must = choose_must list_of_must only in
2799 let torigth_restriction (u,b) =
2802 "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2804 "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2808 let rigth_must = List.map torigth_restriction must in
2809 let rigth_only = Some (List.map torigth_restriction only) in
2811 MQueryGenerator.searchPattern
2812 (rigth_must,[],[]) (rigth_only,None,None) in
2816 wrong_xpointer_format_from_wrong_xpointer_format' uri
2819 " <h1>Backward Query: </h1>" ^
2820 " <pre>" ^ get_last_query result ^ "</pre>"
2822 output_html outputhtml html ;
2824 let rec filter_out =
2828 let tl',exc = filter_out tl in
2831 ProofEngine.can_apply
2832 (term_of_cic_textual_parser_uri
2833 (cic_textual_parser_uri_of_string uri))
2841 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2842 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2849 " <h1>Objects that can actually be applied: </h1> " ^
2850 String.concat "<br>" uris' ^ exc ^
2851 " <h1>Number of false matches: " ^
2852 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2853 " <h1>Number of good matches: " ^
2854 string_of_int (List.length uris') ^ "</h1>"
2856 output_html outputhtml html' ;
2858 user_uri_choice ~title:"Ambiguous input."
2860 "Many lemmas can be successfully applied. Please, choose one:"
2863 inputt#set_term uri' ;
2867 output_html outputhtml
2868 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2871 let choose_selection
2872 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2874 let module G = Gdome in
2875 let rec aux element =
2876 if element#hasAttributeNS
2877 ~namespaceURI:helmns
2878 ~localName:(G.domString "xref")
2880 mmlwidget#set_selection (Some element)
2882 match element#get_parentNode with
2883 None -> assert false
2884 (*CSC: OCAML DIVERGES!
2885 | Some p -> aux (new G.element_of_node p)
2887 | Some p -> aux (new Gdome.element_of_node p)
2891 | None -> mmlwidget#set_selection None
2894 (* STUFF TO BUILD THE GTK INTERFACE *)
2896 (* Stuff for the widget settings *)
2898 let export_to_postscript (output : GMathView.math_view) =
2899 let lastdir = ref (Unix.getcwd ()) in
2902 GToolbox.select_file ~title:"Export to PostScript"
2903 ~dir:lastdir ~filename:"screenshot.ps" ()
2907 output#export_to_postscript ~filename:filename ();
2910 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2911 button_set_kerning button_set_transparency export_to_postscript_menu_item
2914 let is_set = button_t1#active in
2915 output#set_font_manager_type
2916 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2919 button_set_anti_aliasing#misc#set_sensitive true ;
2920 button_set_kerning#misc#set_sensitive true ;
2921 button_set_transparency#misc#set_sensitive true ;
2922 export_to_postscript_menu_item#misc#set_sensitive true ;
2926 button_set_anti_aliasing#misc#set_sensitive false ;
2927 button_set_kerning#misc#set_sensitive false ;
2928 button_set_transparency#misc#set_sensitive false ;
2929 export_to_postscript_menu_item#misc#set_sensitive false ;
2933 let set_anti_aliasing output button_set_anti_aliasing () =
2934 output#set_anti_aliasing button_set_anti_aliasing#active
2937 let set_kerning output button_set_kerning () =
2938 output#set_kerning button_set_kerning#active
2941 let set_transparency output button_set_transparency () =
2942 output#set_transparency button_set_transparency#active
2945 let changefont output font_size_spinb () =
2946 output#set_font_size font_size_spinb#value_as_int
2949 let set_log_verbosity output log_verbosity_spinb () =
2950 output#set_log_verbosity log_verbosity_spinb#value_as_int
2953 class settings_window (output : GMathView.math_view) sw
2954 export_to_postscript_menu_item selection_changed_callback
2956 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2958 GPack.vbox ~packing:settings_window#add () in
2961 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2962 ~border_width:5 ~packing:vbox#add () in
2964 GButton.toggle_button ~label:"activate t1 fonts"
2965 ~packing:(table#attach ~left:0 ~top:0) () in
2966 let button_set_anti_aliasing =
2967 GButton.toggle_button ~label:"set_anti_aliasing"
2968 ~packing:(table#attach ~left:0 ~top:1) () in
2969 let button_set_kerning =
2970 GButton.toggle_button ~label:"set_kerning"
2971 ~packing:(table#attach ~left:1 ~top:1) () in
2972 let button_set_transparency =
2973 GButton.toggle_button ~label:"set_transparency"
2974 ~packing:(table#attach ~left:2 ~top:1) () in
2977 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2978 ~border_width:5 ~packing:vbox#add () in
2979 let font_size_label =
2980 GMisc.label ~text:"font size:"
2981 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2982 let font_size_spinb =
2984 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2987 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2988 let log_verbosity_label =
2989 GMisc.label ~text:"log verbosity:"
2990 ~packing:(table#attach ~left:0 ~top:1) () in
2991 let log_verbosity_spinb =
2993 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2996 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2998 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3000 GButton.button ~label:"Close"
3001 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3003 method show = settings_window#show
3005 button_set_anti_aliasing#misc#set_sensitive false ;
3006 button_set_kerning#misc#set_sensitive false ;
3007 button_set_transparency#misc#set_sensitive false ;
3008 (* Signals connection *)
3009 ignore(button_t1#connect#clicked
3010 (activate_t1 output button_set_anti_aliasing button_set_kerning
3011 button_set_transparency export_to_postscript_menu_item button_t1)) ;
3012 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
3013 ignore(button_set_anti_aliasing#connect#toggled
3014 (set_anti_aliasing output button_set_anti_aliasing));
3015 ignore(button_set_kerning#connect#toggled
3016 (set_kerning output button_set_kerning)) ;
3017 ignore(button_set_transparency#connect#toggled
3018 (set_transparency output button_set_transparency)) ;
3019 ignore(log_verbosity_spinb#connect#changed
3020 (set_log_verbosity output log_verbosity_spinb)) ;
3021 ignore(closeb#connect#clicked settings_window#misc#hide)
3024 (* Scratch window *)
3026 class scratch_window =
3028 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
3030 GPack.vbox ~packing:window#add () in
3032 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
3034 GButton.button ~label:"Whd"
3035 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3037 GButton.button ~label:"Reduce"
3038 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3040 GButton.button ~label:"Simpl"
3041 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
3042 let scrolled_window =
3043 GBin.scrolled_window ~border_width:10
3044 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3047 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
3049 method mmlwidget = mmlwidget
3050 method show () = window#misc#hide () ; window#show ()
3052 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
3053 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
3054 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
3055 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
3056 ignore(simplb#connect#clicked (simpl_in_scratch self))
3060 let vbox1 = GPack.vbox () in
3062 val mutable proofw_ref = None
3063 val mutable compute_ref = None
3065 Lazy.force self#compute ;
3066 match proofw_ref with
3067 None -> assert false
3068 | Some proofw -> proofw
3069 method content = vbox1
3071 match compute_ref with
3072 None -> assert false
3073 | Some compute -> compute
3077 let scrolled_window1 =
3078 GBin.scrolled_window ~border_width:10
3079 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3081 GMathView.math_view ~width:400 ~height:275
3082 ~packing:(scrolled_window1#add) () in
3083 let _ = proofw_ref <- Some proofw in
3085 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3087 GButton.button ~label:"Exact"
3088 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3090 GButton.button ~label:"Intros"
3091 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3093 GButton.button ~label:"Apply"
3094 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3095 let elimintrossimplb =
3096 GButton.button ~label:"ElimIntrosSimpl"
3097 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3099 GButton.button ~label:"ElimType"
3100 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3102 GButton.button ~label:"Whd"
3103 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3105 GButton.button ~label:"Reduce"
3106 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3108 GButton.button ~label:"Simpl"
3109 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3111 GButton.button ~label:"Fold_whd"
3112 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3114 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3116 GButton.button ~label:"Fold_reduce"
3117 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3119 GButton.button ~label:"Fold_simpl"
3120 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3122 GButton.button ~label:"Cut"
3123 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3125 GButton.button ~label:"Change"
3126 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3128 GButton.button ~label:"Let ... In"
3129 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3131 GButton.button ~label:"Ring"
3132 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3134 GButton.button ~label:"ClearBody"
3135 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3137 GButton.button ~label:"Clear"
3138 ~packing:(hbox4#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:"Fourier"
3143 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3145 GButton.button ~label:"RewriteSimpl ->"
3146 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3148 GButton.button ~label:"Reflexivity"
3149 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3151 GButton.button ~label:"Symmetry"
3152 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3154 GButton.button ~label:"Transitivity"
3155 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3157 GButton.button ~label:"Exists"
3158 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3160 GButton.button ~label:"Split"
3161 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3163 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3165 GButton.button ~label:"Left"
3166 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3168 GButton.button ~label:"Right"
3169 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3171 GButton.button ~label:"Assumption"
3172 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3174 GButton.button ~label:"Generalize"
3175 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3177 GButton.button ~label:"Absurd"
3178 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3179 let contradictionb =
3180 GButton.button ~label:"Contradiction"
3181 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3182 let searchpatternb =
3183 GButton.button ~label:"SearchPattern_Apply"
3184 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3186 ignore(exactb#connect#clicked exact) ;
3187 ignore(applyb#connect#clicked apply) ;
3188 ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3189 ignore(elimtypeb#connect#clicked elimtype) ;
3190 ignore(whdb#connect#clicked whd) ;
3191 ignore(reduceb#connect#clicked reduce) ;
3192 ignore(simplb#connect#clicked simpl) ;
3193 ignore(foldwhdb#connect#clicked fold_whd) ;
3194 ignore(foldreduceb#connect#clicked fold_reduce) ;
3195 ignore(foldsimplb#connect#clicked fold_simpl) ;
3196 ignore(cutb#connect#clicked cut) ;
3197 ignore(changeb#connect#clicked change) ;
3198 ignore(letinb#connect#clicked letin) ;
3199 ignore(ringb#connect#clicked ring) ;
3200 ignore(clearbodyb#connect#clicked clearbody) ;
3201 ignore(clearb#connect#clicked clear) ;
3202 ignore(fourierb#connect#clicked fourier) ;
3203 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3204 ignore(reflexivityb#connect#clicked reflexivity) ;
3205 ignore(symmetryb#connect#clicked symmetry) ;
3206 ignore(transitivityb#connect#clicked transitivity) ;
3207 ignore(existsb#connect#clicked exists) ;
3208 ignore(splitb#connect#clicked split) ;
3209 ignore(leftb#connect#clicked left) ;
3210 ignore(rightb#connect#clicked right) ;
3211 ignore(assumptionb#connect#clicked assumption) ;
3212 ignore(generalizeb#connect#clicked generalize) ;
3213 ignore(absurdb#connect#clicked absurd) ;
3214 ignore(contradictionb#connect#clicked contradiction) ;
3215 ignore(introsb#connect#clicked intros) ;
3216 ignore(searchpatternb#connect#clicked searchPattern) ;
3217 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3223 let vbox1 = GPack.vbox () in
3224 let scrolled_window1 =
3225 GBin.scrolled_window ~border_width:10
3226 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3228 GMathView.math_view ~width:400 ~height:275
3229 ~packing:(scrolled_window1#add) () in
3231 method proofw = (assert false : GMathView.math_view)
3232 method content = vbox1
3233 method compute = (assert false : unit)
3237 let empty_page = new empty_page;;
3241 val notebook = GPack.notebook ()
3243 val mutable skip_switch_page_event = false
3244 val mutable empty = true
3245 method notebook = notebook
3247 let new_page = new page () in
3249 pages := !pages @ [n,lazy (setgoal n),new_page] ;
3250 notebook#append_page
3251 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3252 new_page#content#coerce
3253 method remove_all_pages ~skip_switch_page_event:skip =
3255 notebook#remove_page 0 (* let's remove the empty page *)
3257 List.iter (function _ -> notebook#remove_page 0) !pages ;
3259 skip_switch_page_event <- skip
3260 method set_current_page ~may_skip_switch_page_event n =
3261 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3262 let new_page = notebook#page_num page#content#coerce in
3263 if may_skip_switch_page_event && new_page <> notebook#current_page then
3264 skip_switch_page_event <- true ;
3265 notebook#goto_page new_page
3266 method set_empty_page =
3269 notebook#append_page
3270 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3271 empty_page#content#coerce
3273 let (_,_,page) = List.nth !pages notebook#current_page in
3277 (notebook#connect#switch_page
3279 let skip = skip_switch_page_event in
3280 skip_switch_page_event <- false ;
3283 let (metano,setgoal,page) = List.nth !pages i in
3284 ProofEngine.goal := Some metano ;
3285 Lazy.force (page#compute) ;
3294 class rendering_window output (notebook : notebook) =
3295 let scratch_window = new scratch_window in
3297 GWindow.window ~title:"MathML viewer" ~border_width:0
3298 ~allow_shrink:false () in
3299 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3301 let handle_box = GBin.handle_box ~border_width:2
3302 ~packing:(vbox_for_menu#pack ~padding:0) () in
3303 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3304 let factory0 = new GMenu.factory menubar in
3305 let accel_group = factory0#accel_group in
3307 let file_menu = factory0#add_submenu "File" in
3308 let factory1 = new GMenu.factory file_menu ~accel_group in
3309 let export_to_postscript_menu_item =
3312 factory1#add_item "New Block of (Co)Inductive Definitions..."
3313 ~key:GdkKeysyms._B ~callback:new_inductive
3316 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3319 let reopen_menu_item =
3320 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3324 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3325 ignore (factory1#add_separator ()) ;
3327 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3329 let save_menu_item =
3330 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3333 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3334 ignore (!save_set_sensitive false);
3335 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3336 ignore (!qed_set_sensitive false);
3337 ignore (factory1#add_separator ()) ;
3338 let export_to_postscript_menu_item =
3339 factory1#add_item "Export to PostScript..."
3340 ~callback:(export_to_postscript output) in
3341 ignore (factory1#add_separator ()) ;
3343 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3344 export_to_postscript_menu_item
3347 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3348 let factory2 = new GMenu.factory edit_menu ~accel_group in
3349 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3350 let proveit_menu_item =
3351 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3352 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3354 let focus_menu_item =
3355 factory2#add_item "Focus" ~key:GdkKeysyms._F
3356 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3359 focus_and_proveit_set_sensitive :=
3361 proveit_menu_item#misc#set_sensitive b ;
3362 focus_menu_item#misc#set_sensitive b
3364 let _ = !focus_and_proveit_set_sensitive false in
3365 (* edit term menu *)
3366 let edit_term_menu = factory0#add_submenu "Edit Term" in
3367 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3368 let check_menu_item =
3369 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3370 ~callback:(check scratch_window) in
3371 let _ = check_menu_item#misc#set_sensitive false in
3373 let settings_menu = factory0#add_submenu "Search" in
3374 let factory4 = new GMenu.factory settings_menu ~accel_group in
3376 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3378 let searchPattern_menu_item =
3379 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3380 ~callback:completeSearchPattern in
3381 let _ = searchPattern_menu_item#misc#set_sensitive false in
3382 let show_menu_item =
3383 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3386 let settings_menu = factory0#add_submenu "Settings" in
3387 let factory3 = new GMenu.factory settings_menu ~accel_group in
3389 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3390 ~callback:edit_aliases in
3391 let _ = factory3#add_separator () in
3393 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3394 ~callback:(function _ -> (settings_window ())#show ()) in
3396 let _ = window#add_accel_group accel_group in
3400 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3402 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3403 let scrolled_window0 =
3404 GBin.scrolled_window ~border_width:10
3405 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3406 let _ = scrolled_window0#add output#coerce in
3408 GBin.frame ~label:"Insert Term"
3409 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3410 let scrolled_window1 =
3411 GBin.scrolled_window ~border_width:5
3412 ~packing:frame#add () in
3414 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3415 ~isnotempty_callback:
3417 check_menu_item#misc#set_sensitive b ;
3418 searchPattern_menu_item#misc#set_sensitive b) in
3420 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3422 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3424 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3428 ~source:"<html><body bgColor=\"white\"></body></html>"
3429 ~width:400 ~height: 100
3434 method outputhtml = outputhtml
3435 method inputt = inputt
3436 method output = (output : GMathView.math_view)
3437 method notebook = notebook
3438 method show = window#show
3440 notebook#set_empty_page ;
3441 export_to_postscript_menu_item#misc#set_sensitive false ;
3442 check_term := (check_term_in_scratch scratch_window) ;
3444 (* signal handlers here *)
3445 ignore(output#connect#selection_changed
3447 choose_selection output elem ;
3448 !focus_and_proveit_set_sensitive true
3450 ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3451 let settings_window = new settings_window output scrolled_window0
3452 export_to_postscript_menu_item (choose_selection output) in
3453 set_settings_window settings_window ;
3454 set_outputhtml outputhtml ;
3455 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3456 Logger.log_callback :=
3457 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3462 let initialize_everything () =
3463 let module U = Unix in
3464 let output = GMathView.math_view ~width:350 ~height:280 () in
3465 let notebook = new notebook in
3466 let rendering_window' = new rendering_window output notebook in
3467 set_rendering_window rendering_window' ;
3468 mml_of_cic_term_ref := mml_of_cic_term ;
3469 rendering_window'#show () ;
3476 Mqint.set_database Mqint.postgres_db ;
3477 (* Mqint.init "dbname=helm_mowgli" ; *)
3478 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
3479 Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm";
3481 ignore (GtkMain.Main.init ()) ;
3482 initialize_everything () ;
3483 if !usedb then Mqint.close ();