1 (* Copyright (C) 2000-2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
34 (******************************************************************************)
37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
40 let index_sharp = String.index uri '#' in
41 let index_rest = index_sharp + 10 in
42 let baseuri = String.sub uri 0 index_sharp in
43 let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
48 (* GLOBAL CONSTANTS *)
50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
51 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
55 " <body bgColor=\"white\">"
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 = "//miohelm/tmp/currentproof";;
73 let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
77 let prooffile = "/home/galata/miohelm/currentproof";;
78 let prooffiletype = "/home/galata/miohelm/currentprooftype";;
81 (*CSC: the getter should handle the innertypes, not the FS *)
83 let innertypesfile = "/public/sacerdot/innertypes";;
84 let constanttypefile = "/public/sacerdot/constanttype";;
87 let innertypesfile = "/public/sacerdot/innertypes";;
88 let constanttypefile = "/public/sacerdot/constanttype";;
92 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
93 let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
97 let innertypesfile = "/home/galata/miohelm/innertypes";;
98 let constanttypefile = "/home/galata/miohelm/constanttype";;
101 let empty_id_to_uris = ([],function _ -> None);;
104 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
106 let htmlheader_and_content = ref htmlheader;;
108 let current_cic_infos = ref None;;
109 let current_goal_infos = ref None;;
110 let current_scratch_infos = ref None;;
112 let id_to_uris = ref empty_id_to_uris;;
114 let check_term = ref (fun _ _ _ -> assert false);;
115 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
117 exception RenderingWindowsNotInitialized;;
119 let set_rendering_window,rendering_window =
120 let rendering_window_ref = ref None in
121 (function rw -> rendering_window_ref := Some rw),
123 match !rendering_window_ref with
124 None -> raise RenderingWindowsNotInitialized
129 exception SettingsWindowsNotInitialized;;
131 let set_settings_window,settings_window =
132 let settings_window_ref = ref None in
133 (function rw -> settings_window_ref := Some rw),
135 match !settings_window_ref with
136 None -> raise SettingsWindowsNotInitialized
141 exception OutputHtmlNotInitialized;;
143 let set_outputhtml,outputhtml =
144 let outputhtml_ref = ref None in
145 (function rw -> outputhtml_ref := Some rw),
147 match !outputhtml_ref with
148 None -> raise OutputHtmlNotInitialized
149 | Some outputhtml -> outputhtml
153 exception QedSetSensitiveNotInitialized;;
154 let qed_set_sensitive =
155 ref (function _ -> raise QedSetSensitiveNotInitialized)
158 exception SaveSetSensitiveNotInitialized;;
159 let save_set_sensitive =
160 ref (function _ -> raise SaveSetSensitiveNotInitialized)
163 (* COMMAND LINE OPTIONS *)
169 "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
172 Arg.parse argspec ignore ""
174 (* A WIDGET TO ENTER CIC TERMS *)
176 class term_editor ?packing ?width ?height ?isnotempty_callback () =
177 let input = GEdit.text ~editable:true ?width ?height ?packing () in
179 match isnotempty_callback with
182 ignore(input#connect#changed (function () -> callback (input#length > 0)))
185 method coerce = input#coerce
187 input#delete_text 0 input#length
188 (* CSC: txt is now a string, but should be of type Cic.term *)
189 method set_term txt =
191 ignore ((input#insert_text txt) ~pos:0)
192 (* CSC: this method should disappear *)
193 method get_as_string =
194 input#get_chars 0 input#length
195 method get_term ~context ~metasenv =
196 let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
197 CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
203 exception IllFormedUri of string;;
205 let cic_textual_parser_uri_of_string uri' =
208 if String.sub uri' (String.length uri' - 4) 4 = ".con" then
209 CicTextualParser0.ConUri (UriManager.uri_of_string uri')
211 if String.sub uri' (String.length uri' - 4) 4 = ".var" then
212 CicTextualParser0.VarUri (UriManager.uri_of_string uri')
216 let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
217 CicTextualParser0.IndTyUri (uri'',typeno)
220 (* Constructor of an Inductive Type *)
221 let uri'',typeno,consno =
222 CicTextualLexer.indconuri_of_uri uri'
224 CicTextualParser0.IndConUri (uri'',typeno,consno)
227 _ -> raise (IllFormedUri uri')
230 let term_of_cic_textual_parser_uri uri =
231 let module C = Cic in
232 let module CTP = CicTextualParser0 in
234 CTP.ConUri uri -> C.Const (uri,[])
235 | CTP.VarUri uri -> C.Var (uri,[])
236 | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
237 | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
240 let string_of_cic_textual_parser_uri uri =
241 let module C = Cic in
242 let module CTP = CicTextualParser0 in
245 CTP.ConUri uri -> UriManager.string_of_uri uri
246 | CTP.VarUri uri -> UriManager.string_of_uri uri
247 | CTP.IndTyUri (uri,tyno) ->
248 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
249 | CTP.IndConUri (uri,tyno,consno) ->
250 UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
253 (* 4 = String.length "cic:" *)
254 String.sub uri' 4 (String.length uri' - 4)
257 let output_html outputhtml msg =
258 htmlheader_and_content := !htmlheader_and_content ^ msg ;
259 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
260 outputhtml#set_topline (-1)
263 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
267 let check_window outputhtml uris =
270 ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
272 GPack.notebook ~scrollable:true ~packing:window#add () in
277 let scrolled_window =
278 GBin.scrolled_window ~border_width:10
280 (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
286 ~packing:scrolled_window#add ~width:400 ~height:280 () in
289 term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
291 (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
294 let mml = !mml_of_cic_term_ref 111 expr in
295 prerr_endline ("### " ^ CicPp.ppterm expr) ;
296 mmlwidget#load_tree ~dom:mml
299 output_html outputhtml
300 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
305 (notebook#connect#switch_page
306 (function i -> Lazy.force (List.nth render_terms i)))
312 interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
314 let choices = ref [] in
315 let chosen = ref false in
317 GWindow.dialog ~modal:true ~title ~width:600 () in
319 GMisc.label ~text:msg
320 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
321 let scrolled_window =
322 GBin.scrolled_window ~border_width:10
323 ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
325 let expected_height = 18 * List.length uris in
326 let height = if expected_height > 400 then 400 else expected_height in
327 GList.clist ~columns:1 ~packing:scrolled_window#add
328 ~height ~selection_mode () in
329 let _ = List.map (function x -> clist#append [x]) uris in
331 GPack.hbox ~border_width:0
332 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
334 GMisc.label ~text:"None of the above. Try this one:"
335 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
337 GEdit.entry ~editable:true
338 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
340 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
342 GButton.button ~label:ok
343 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
344 let _ = okb#misc#set_sensitive false in
346 GButton.button ~label:"Check"
347 ~packing:(hbox#pack ~padding:5) () in
348 let _ = checkb#misc#set_sensitive false in
350 GButton.button ~label:"Abort"
351 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
353 let check_callback () =
354 assert (List.length !choices > 0) ;
355 check_window (outputhtml ()) !choices
357 ignore (window#connect#destroy GMain.Main.quit) ;
358 ignore (cancelb#connect#clicked window#destroy) ;
360 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
361 ignore (checkb#connect#clicked check_callback) ;
363 (clist#connect#select_row
364 (fun ~row ~column ~event ->
365 checkb#misc#set_sensitive true ;
366 okb#misc#set_sensitive true ;
367 choices := (List.nth uris row)::!choices)) ;
369 (clist#connect#unselect_row
370 (fun ~row ~column ~event ->
372 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
374 (manual_input#connect#changed
376 if manual_input#text = "" then
379 checkb#misc#set_sensitive false ;
380 okb#misc#set_sensitive false ;
381 clist#misc#set_sensitive true
385 choices := [manual_input#text] ;
386 clist#unselect_all () ;
387 checkb#misc#set_sensitive true ;
388 okb#misc#set_sensitive true ;
389 clist#misc#set_sensitive false
391 window#set_position `CENTER ;
394 if !chosen && List.length !choices > 0 then
400 let interactive_interpretation_choice interpretations =
401 let chosen = ref None in
404 ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
405 let vbox = GPack.vbox ~packing:window#add () in
409 ("Ambiguous input since there are many well-typed interpretations." ^
410 " Please, choose one of them.")
411 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
413 GPack.notebook ~scrollable:true
414 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
417 (function interpretation ->
419 let expected_height = 18 * List.length interpretation in
420 let height = if expected_height > 400 then 400 else expected_height in
421 GList.clist ~columns:2 ~packing:notebook#append_page ~height
422 ~titles:["id" ; "URI"] ()
426 (function (id,uri) ->
427 let n = clist#append [id;uri] in
428 clist#set_row ~selectable:false n
431 clist#columns_autosize ()
434 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
436 GButton.button ~label:"Ok"
437 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
439 GButton.button ~label:"Abort"
440 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
442 ignore (window#connect#destroy GMain.Main.quit) ;
443 ignore (cancelb#connect#clicked window#destroy) ;
446 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
447 window#set_position `CENTER ;
451 None -> raise NoChoice
458 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
460 let query = ref "" in
461 MQueryGenerator.set_confirm_query
462 (function q -> query := MQueryUtil.text_of_query q ; true) ;
463 function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
466 let domImpl = Gdome.domImplementation ();;
468 let parseStyle name =
470 domImpl#createDocumentFromURI
472 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
474 ~uri:("styles/" ^ name) ()
476 Gdome_xslt.processStylesheet style
479 let d_c = parseStyle "drop_coercions.xsl";;
480 let tc1 = parseStyle "objtheorycontent.xsl";;
481 let hc2 = parseStyle "content_to_html.xsl";;
482 let l = parseStyle "link.xsl";;
484 let c1 = parseStyle "rootcontent.xsl";;
485 let g = parseStyle "genmmlid.xsl";;
486 let c2 = parseStyle "annotatedpres.xsl";;
489 let getterURL = Configuration.getter_url;;
490 let processorURL = Configuration.processor_url;;
492 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
493 let mml_args ~explode_all =
494 ("explodeall",(if explode_all then "true()" else "false()"))::
495 ["processorURL", "'" ^ processorURL ^ "'" ;
496 "getterURL", "'" ^ getterURL ^ "'" ;
497 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
498 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
499 "UNICODEvsSYMBOL", "'symbol'" ;
500 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
501 "encoding", "'iso-8859-1'" ;
502 "media-type", "'text/html'" ;
503 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
504 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
505 "naturalLanguage", "'yes'" ;
506 "annotations", "'no'" ;
507 "URLs_or_URIs", "'URIs'" ;
508 "topurl", "'http://phd.cs.unibo.it/helm'" ;
509 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
512 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
514 ["processorURL", "'" ^ processorURL ^ "'" ;
515 "getterURL", "'" ^ getterURL ^ "'" ;
516 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
517 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
518 "UNICODEvsSYMBOL", "'symbol'" ;
519 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
520 "encoding", "'iso-8859-1'" ;
521 "media-type", "'text/html'" ;
522 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
523 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
524 "naturalLanguage", "'no'" ;
525 "annotations", "'no'" ;
526 "explodeall", "true()" ;
527 "URLs_or_URIs", "'URIs'" ;
528 "topurl", "'http://phd.cs.unibo.it/helm'" ;
529 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
532 let parse_file filename =
533 let inch = open_in filename in
534 let rec read_lines () =
536 let line = input_line inch in
544 let applyStylesheets input styles args =
545 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
550 mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
552 (*CSC: ????????????????? *)
554 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
558 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
559 ~ask_dtd_to_the_getter:true
563 None -> Xml2Gdome.document_of_xml domImpl xml
565 Xml.pp xml (Some constanttypefile) ;
566 Xml2Gdome.document_of_xml domImpl bodyxml'
568 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
569 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
571 Xml.pp xmlinnertypes (Some innertypesfile) ;
572 let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
577 save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
580 let struri = UriManager.string_of_uri uri in
581 let idx = (String.rindex struri '/') + 1 in
582 String.sub struri idx (String.length struri - idx)
584 let path = pathname ^ "/" ^ name in
586 Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
590 Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
591 ~ask_dtd_to_the_getter:false
594 let innertypesuri = UriManager.innertypesuri_of_uri uri in
595 Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
596 Getter.register innertypesuri
597 (Configuration.annotations_url ^
598 Str.replace_first (Str.regexp "^cic:") ""
599 (UriManager.string_of_uri innertypesuri) ^ ".xml"
601 (* constant type / variable / mutual inductive types definition *)
602 Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
604 (Configuration.annotations_url ^
605 Str.replace_first (Str.regexp "^cic:") ""
606 (UriManager.string_of_uri uri) ^ ".xml"
613 match UriManager.bodyuri_of_uri uri with
615 | Some bodyuri -> bodyuri
617 Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
618 Getter.register bodyuri
619 (Configuration.annotations_url ^
620 Str.replace_first (Str.regexp "^cic:") ""
621 (UriManager.string_of_uri bodyuri) ^ ".xml"
628 exception RefreshSequentException of exn;;
629 exception RefreshProofException of exn;;
631 let refresh_proof (output : GMathView.math_view) =
633 let uri,currentproof =
634 match !ProofEngine.proof with
636 | Some (uri,metasenv,bo,ty) ->
637 !qed_set_sensitive (List.length metasenv = 0) ;
638 (*CSC: Wrong: [] is just plainly wrong *)
639 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
642 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
643 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
645 Cic2acic.acic_object_of_cic_object currentproof
648 mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
651 output#load_tree mml ;
653 Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
656 match !ProofEngine.proof with
658 | Some (uri,metasenv,bo,ty) ->
659 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
660 raise (RefreshProofException e)
663 let refresh_sequent ?(empty_notebook=true) notebook =
665 match !ProofEngine.goal with
667 if empty_notebook then
669 notebook#remove_all_pages ~skip_switch_page_event:false ;
670 notebook#set_empty_page
673 notebook#proofw#unload
676 match !ProofEngine.proof with
678 | Some (_,metasenv,_,_) -> metasenv
680 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
681 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
682 SequentPp.XmlPp.print_sequent metasenv currentsequent
684 let regenerate_notebook () =
685 let skip_switch_page_event =
687 (m,_,_)::_ when m = metano -> false
690 notebook#remove_all_pages ~skip_switch_page_event ;
691 List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
693 if empty_notebook then
695 regenerate_notebook () ;
696 notebook#set_current_page ~may_skip_switch_page_event:false metano
700 let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
702 applyStylesheets sequent_doc sequent_styles sequent_args
704 notebook#set_current_page ~may_skip_switch_page_event:true metano;
705 notebook#proofw#load_tree ~dom:sequent_mml
707 current_goal_infos :=
708 Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
712 match !ProofEngine.goal with
717 match !ProofEngine.proof with
719 | Some (_,metasenv,_,_) -> metasenv
722 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
723 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
724 raise (RefreshSequentException e)
725 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); raise (RefreshSequentException e)
729 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
730 ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
733 let mml_of_cic_term metano term =
735 match !ProofEngine.proof with
737 | Some (_,metasenv,_,_) -> metasenv
740 match !ProofEngine.goal with
743 let (_,canonical_context,_) =
744 List.find (function (m,_,_) -> m=metano) metasenv
748 let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
749 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
752 Xml2Gdome.document_of_xml domImpl sequent_gdome
755 applyStylesheets sequent_doc sequent_styles sequent_args ;
757 current_scratch_infos :=
758 Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
762 exception OpenConjecturesStillThere;;
763 exception WrongProof;;
765 let pathname_of_annuri uristring =
766 Configuration.annotations_dir ^
767 Str.replace_first (Str.regexp "^cic:") "" uristring
770 let make_dirs dirpath =
771 ignore (Unix.system ("mkdir -p " ^ dirpath))
774 let save_obj uri obj =
776 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
777 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
779 Cic2acic.acic_object_of_cic_object obj
781 (* let's save the theorem and register it to the getter *)
782 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
784 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
789 match !ProofEngine.proof with
791 | Some (uri,[],bo,ty) ->
793 CicReduction.are_convertible []
794 (CicTypeChecker.type_of_aux' [] [] bo) ty
797 (*CSC: Wrong: [] is just plainly wrong *)
798 let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
800 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
801 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
803 Cic2acic.acic_object_of_cic_object proof
806 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
809 ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
810 !qed_set_sensitive false ;
811 (* let's save the theorem and register it to the getter *)
812 let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
814 save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
818 (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
823 | _ -> raise OpenConjecturesStillThere
827 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
828 match !ProofEngine.proof with
830 | Some (uri, metasenv, bo, ty) ->
832 (*CSC: Wrong: [] is just plainly wrong *)
833 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
835 let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
836 Cic2acic.acic_object_of_cic_object currentproof
840 Cic2Xml.print_object uri ~ids_to_inner_sorts
841 ~ask_dtd_to_the_getter:true acurrentproof
843 xml,Some bodyxml -> xml,bodyxml
844 | _,None -> assert false
846 Xml.pp ~quiet:true xml (Some prooffiletype) ;
847 output_html outputhtml
848 ("<h1 color=\"Green\">Current proof type saved to " ^
849 prooffiletype ^ "</h1>") ;
850 Xml.pp ~quiet:true bodyxml (Some prooffile) ;
851 output_html outputhtml
852 ("<h1 color=\"Green\">Current proof body saved to " ^
856 (* Used to typecheck the loaded proofs *)
857 let typecheck_loaded_proof metasenv bo ty =
858 let module T = CicTypeChecker in
861 (fun metasenv ((_,context,ty) as conj) ->
862 ignore (T.type_of_aux' metasenv context ty) ;
865 ignore (T.type_of_aux' metasenv [] ty) ;
866 ignore (T.type_of_aux' metasenv [] bo)
870 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
871 let output = ((rendering_window ())#output : GMathView.math_view) in
872 let notebook = (rendering_window ())#notebook in
875 GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
878 None -> raise NoChoice
880 let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
881 match CicParser.obj_of_xml prooffiletype (Some prooffile) with
882 Cic.CurrentProof (_,metasenv,bo,ty,_) ->
883 typecheck_loaded_proof metasenv bo ty ;
885 Some (uri, metasenv, bo, ty) ;
889 | (metano,_,_)::_ -> Some metano
891 refresh_proof output ;
892 refresh_sequent notebook ;
893 output_html outputhtml
894 ("<h1 color=\"Green\">Current proof type loaded from " ^
895 prooffiletype ^ "</h1>") ;
896 output_html outputhtml
897 ("<h1 color=\"Green\">Current proof body loaded from " ^
898 prooffile ^ "</h1>") ;
899 !save_set_sensitive true
902 RefreshSequentException e ->
903 output_html outputhtml
904 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
905 "sequent: " ^ Printexc.to_string e ^ "</h1>")
906 | RefreshProofException e ->
907 output_html outputhtml
908 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
909 "proof: " ^ Printexc.to_string e ^ "</h1>")
911 output_html outputhtml
912 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
915 let edit_aliases () =
916 let chosen = ref false in
919 ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
921 GPack.vbox ~border_width:0 ~packing:window#add () in
922 let scrolled_window =
923 GBin.scrolled_window ~border_width:10
924 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
925 let input = GEdit.text ~editable:true ~width:400 ~height:100
926 ~packing:scrolled_window#add () in
928 GPack.hbox ~border_width:0
929 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
931 GButton.button ~label:"Ok"
932 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
934 GButton.button ~label:"Cancel"
935 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
936 ignore (window#connect#destroy GMain.Main.quit) ;
937 ignore (cancelb#connect#clicked window#destroy) ;
939 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
940 let dom,resolve_id = !id_to_uris in
942 (input#insert_text ~pos:0
947 match resolve_id v with
952 (string_of_cic_textual_parser_uri uri)
958 let inputtext = input#get_chars 0 input#length in
960 let alfa = "[a-zA-Z_-]" in
961 let digit = "[0-9]" in
962 let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
963 let blanks = "\( \|\t\|\n\)+" in
964 let nonblanks = "[^ \t\n]+" in
965 let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
967 ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
971 let n' = Str.search_forward regexpr inputtext n in
972 let id = Str.matched_group 2 inputtext in
974 cic_textual_parser_uri_of_string
975 ("cic:" ^ (Str.matched_group 5 inputtext))
977 let dom,resolve_id = aux (n' + 1) in
978 if List.mem id dom then
982 (function id' -> if id = id' then Some uri else resolve_id id')
984 Not_found -> empty_id_to_uris
988 id_to_uris := dom,resolve_id
992 let module L = LogicalOperations in
993 let module G = Gdome in
994 let notebook = (rendering_window ())#notebook in
995 let output = (rendering_window ())#output in
996 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
997 match (rendering_window ())#output#get_selection with
1000 ((node : Gdome.element)#getAttributeNS
1001 (*CSC: OCAML DIVERGE
1002 ((element : G.element)#getAttributeNS
1004 ~namespaceURI:helmns
1005 ~localName:(G.domString "xref"))#to_string
1007 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1011 match !current_cic_infos with
1012 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1014 L.to_sequent id ids_to_terms ids_to_father_ids ;
1015 refresh_proof output ;
1016 refresh_sequent notebook
1017 | None -> assert false (* "ERROR: No current term!!!" *)
1019 RefreshSequentException e ->
1020 output_html outputhtml
1021 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1022 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1023 | RefreshProofException e ->
1024 output_html outputhtml
1025 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1026 "proof: " ^ Printexc.to_string e ^ "</h1>")
1028 output_html outputhtml
1029 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1031 | None -> assert false (* "ERROR: No selection!!!" *)
1035 let module L = LogicalOperations in
1036 let module G = Gdome in
1037 let notebook = (rendering_window ())#notebook in
1038 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1039 match (rendering_window ())#output#get_selection with
1042 ((node : Gdome.element)#getAttributeNS
1043 (*CSC: OCAML DIVERGE
1044 ((element : G.element)#getAttributeNS
1046 ~namespaceURI:helmns
1047 ~localName:(G.domString "xref"))#to_string
1049 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1053 match !current_cic_infos with
1054 Some (ids_to_terms, ids_to_father_ids, _, _) ->
1056 L.focus id ids_to_terms ids_to_father_ids ;
1057 refresh_sequent notebook
1058 | None -> assert false (* "ERROR: No current term!!!" *)
1060 RefreshSequentException e ->
1061 output_html outputhtml
1062 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1063 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1064 | RefreshProofException e ->
1065 output_html outputhtml
1066 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1067 "proof: " ^ Printexc.to_string e ^ "</h1>")
1069 output_html outputhtml
1070 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1072 | None -> assert false (* "ERROR: No selection!!!" *)
1075 exception NoPrevGoal;;
1076 exception NoNextGoal;;
1078 let setgoal metano =
1079 let module L = LogicalOperations in
1080 let module G = Gdome in
1081 let notebook = (rendering_window ())#notebook in
1082 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1084 match !ProofEngine.proof with
1085 None -> assert false
1086 | Some (_,metasenv,_,_) -> metasenv
1089 refresh_sequent ~empty_notebook:false notebook
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>")
1096 output_html outputhtml
1097 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1101 show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1104 GWindow.window ~width:800 ~border_width:2 () in
1105 let scrolled_window =
1106 GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1108 GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1109 let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1110 let href = Gdome.domString "href" in
1111 let show_in_show_window_obj uri obj =
1112 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1115 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1116 ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1118 Cic2acic.acic_object_of_cic_object obj
1121 mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1124 window#set_title (UriManager.string_of_uri uri) ;
1125 window#misc#hide () ; window#show () ;
1126 mmlwidget#load_tree mml ;
1129 output_html outputhtml
1130 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1132 let show_in_show_window_uri uri =
1133 CicTypeChecker.typecheck uri ;
1134 let obj = CicEnvironment.get_cooked_obj uri in
1135 show_in_show_window_obj uri obj
1137 let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1138 if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1140 (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1142 show_in_show_window_uri (UriManager.uri_of_string uri)
1144 if mmlwidget#get_action <> None then
1145 mmlwidget#action_toggle
1148 mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1150 show_in_show_window_obj, show_in_show_window_uri,
1151 show_in_show_window_callback
1154 exception NoObjectsLocated;;
1156 let user_uri_choice ~title ~msg uris =
1159 [] -> raise NoObjectsLocated
1163 interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1168 String.sub uri 4 (String.length uri - 4)
1171 let locate_callback id =
1172 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1173 let result = MQueryGenerator.locate id in
1176 (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1179 (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1181 output_html outputhtml html ;
1182 user_uri_choice ~title:"Ambiguous input."
1184 ("Ambiguous input \"" ^ id ^
1185 "\". Please, choose one interpetation:")
1190 let inputt = ((rendering_window ())#inputt : term_editor) in
1191 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1194 GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1196 None -> raise NoChoice
1198 let uri = locate_callback input in
1202 output_html outputhtml
1203 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1206 let input_or_locate_uri ~title =
1207 let uri = ref None in
1210 ~width:400 ~modal:true ~title ~border_width:2 () in
1211 let vbox = GPack.vbox ~packing:window#add () in
1213 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1215 GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1217 GEdit.entry ~editable:true
1218 ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1220 GButton.button ~label:"Check"
1221 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1222 let _ = checkb#misc#set_sensitive false in
1224 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1226 GMisc.label ~text:"You can also enter an indentifier to locate:"
1227 ~packing:(hbox2#pack ~padding:5) () in
1229 GEdit.entry ~editable:true
1230 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1232 GButton.button ~label:"Locate"
1233 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1234 let _ = locateb#misc#set_sensitive false in
1236 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1238 GButton.button ~label:"Ok"
1239 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1240 let _ = okb#misc#set_sensitive false in
1242 GButton.button ~label:"Cancel"
1243 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1245 ignore (window#connect#destroy GMain.Main.quit) ;
1247 (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1248 let check_callback () =
1249 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1250 let uri = "cic:" ^ manual_input#text in
1252 ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1253 output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1256 Getter.Unresolved ->
1257 output_html outputhtml
1258 ("<h1 color=\"Red\">URI " ^ uri ^
1259 " does not correspond to any object.</h1>") ;
1261 | UriManager.IllFormedUri _ ->
1262 output_html outputhtml
1263 ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1266 output_html outputhtml
1267 ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1271 (okb#connect#clicked
1273 if check_callback () then
1275 uri := Some manual_input#text ;
1279 ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1281 (manual_input#connect#changed
1283 if manual_input#text = "" then
1285 checkb#misc#set_sensitive false ;
1286 okb#misc#set_sensitive false
1290 checkb#misc#set_sensitive true ;
1291 okb#misc#set_sensitive true
1294 (locate_input#connect#changed
1295 (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1297 (locateb#connect#clicked
1299 let id = locate_input#text in
1300 manual_input#set_text (locate_callback id) ;
1301 locate_input#delete_text 0 (String.length id)
1304 GMain.Main.main () ;
1306 None -> raise NoChoice
1307 | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1310 let locate_one_id id =
1311 let result = MQueryGenerator.locate id in
1315 wrong_xpointer_format_from_wrong_xpointer_format' uri
1317 let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1318 output_html (rendering_window ())#outputhtml html ;
1322 [UriManager.string_of_uri
1323 (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1326 interactive_user_uri_choice
1327 ~selection_mode:`EXTENDED
1328 ~ok:"Try every selection."
1329 ~title:"Ambiguous input."
1331 ("Ambiguous input \"" ^ id ^
1332 "\". Please, choose one or more interpretations:")
1335 List.map cic_textual_parser_uri_of_string uris'
1338 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1339 exception AmbiguousInput;;
1341 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1342 let known_ids,resolve_id = !id_to_uris in
1348 if List.mem he known_ids then filter tl else he::(filter tl)
1352 (* for each id in dom' we get the list of uris associated to it *)
1353 let list_of_uris = List.map locate_one_id dom' in
1354 (* and now we compute the list of all possible assignments from id to uris *)
1356 let rec aux ids list_of_uris =
1357 match ids,list_of_uris with
1358 [],[] -> [resolve_id]
1359 | id::idtl,uris::uristl ->
1360 let resolves = aux idtl uristl in
1366 function id' -> if id = id' then Some uri else f id'
1370 | _,_ -> assert false
1372 aux dom' list_of_uris
1374 let tests_no = List.length resolve_ids in
1375 if tests_no > 1 then
1376 output_html (outputhtml ())
1377 ("<h1>Disambiguation phase started: " ^
1378 string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1379 (* now we select only the ones that generates well-typed terms *)
1385 let metasenv',expr = mk_metasenv_and_expr resolve in
1387 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1389 (CicTypeChecker.type_of_aux' metasenv context expr) ;
1390 resolve::(filter tl)
1397 match resolve_ids' with
1398 [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1399 | [resolve_id] -> resolve_id
1403 (function resolve ->
1407 match resolve id with
1408 None -> assert false
1411 CicTextualParser0.ConUri uri
1412 | CicTextualParser0.VarUri uri ->
1413 UriManager.string_of_uri uri
1414 | CicTextualParser0.IndTyUri (uri,tyno) ->
1415 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1416 string_of_int (tyno+1) ^ ")"
1417 | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1418 UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1419 string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^ ")"
1423 let index = interactive_interpretation_choice choices in
1424 List.nth resolve_ids' index
1426 id_to_uris := known_ids @ dom', resolve_id' ;
1427 mk_metasenv_and_expr resolve_id'
1430 exception UriAlreadyInUse;;
1431 exception NotAUriToAConstant;;
1433 let new_inductive () =
1434 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1435 let output = ((rendering_window ())#output : GMathView.math_view) in
1436 let notebook = (rendering_window ())#notebook in
1438 let chosen = ref false in
1439 let inductive = ref true in
1440 let paramsno = ref 0 in
1441 let get_uri = ref (function _ -> assert false) in
1442 let get_base_uri = ref (function _ -> assert false) in
1443 let get_names = ref (function _ -> assert false) in
1444 let get_types_and_cons = ref (function _ -> assert false) in
1445 let get_name_context_context_and_subst = ref (function _ -> assert false) in
1448 ~width:600 ~modal:true ~position:`CENTER
1449 ~title:"New Block of Mutual (Co)Inductive Definitions"
1450 ~border_width:2 () in
1451 let vbox = GPack.vbox ~packing:window#add () in
1453 GPack.hbox ~border_width:0
1454 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1456 GMisc.label ~text:"Enter the URI for the new block:"
1457 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1459 GEdit.entry ~editable:true
1460 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1462 GPack.hbox ~border_width:0
1463 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1467 "Enter the number of left parameters in every arity and constructor type:"
1468 ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1469 let paramsno_entry =
1470 GEdit.entry ~editable:true ~text:"0"
1471 ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1473 GPack.hbox ~border_width:0
1474 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1476 GMisc.label ~text:"Are the definitions inductive or coinductive?"
1477 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1479 GButton.radio_button ~label:"Inductive"
1480 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1482 GButton.radio_button ~label:"Coinductive"
1483 ~group:inductiveb#group
1484 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1486 GPack.hbox ~border_width:0
1487 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1489 GMisc.label ~text:"Enter the list of the names of the types:"
1490 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1492 GEdit.entry ~editable:true
1493 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1495 GPack.hbox ~border_width:0
1496 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1498 GButton.button ~label:"> Next"
1499 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1500 let _ = okb#misc#set_sensitive true in
1502 GButton.button ~label:"Abort"
1503 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1504 ignore (window#connect#destroy GMain.Main.quit) ;
1505 ignore (cancelb#connect#clicked window#destroy) ;
1509 (okb#connect#clicked
1512 let uristr = "cic:" ^ uri_entry#text in
1513 let namesstr = names_entry#text in
1514 let paramsno' = int_of_string (paramsno_entry#text) in
1515 match Str.split (Str.regexp " +") namesstr with
1517 | (he::tl) as names ->
1518 let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1521 ignore (Getter.resolve uri) ;
1522 raise UriAlreadyInUse
1524 Getter.Unresolved ->
1525 get_uri := (function () -> uri) ;
1526 get_names := (function () -> names) ;
1527 inductive := inductiveb#active ;
1528 paramsno := paramsno' ;
1533 output_html outputhtml
1534 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1542 GBin.frame ~label:name
1543 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1544 let vbox = GPack.vbox ~packing:frame#add () in
1545 let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1547 GMisc.label ~text:("Enter its type:")
1548 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1549 let scrolled_window =
1550 GBin.scrolled_window ~border_width:5
1551 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1553 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1554 ~isnotempty_callback:
1556 (*non_empty_type := b ;*)
1557 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1560 GPack.hbox ~border_width:0
1561 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1563 GMisc.label ~text:("Enter the list of its constructors:")
1564 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1565 let cons_names_entry =
1566 GEdit.entry ~editable:true
1567 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1568 (newinputt,cons_names_entry)
1571 vbox#remove hboxn#coerce ;
1573 GPack.hbox ~border_width:0
1574 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1576 GButton.button ~label:"> Next"
1577 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1579 GButton.button ~label:"Abort"
1580 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1581 ignore (cancelb#connect#clicked window#destroy) ;
1583 (okb#connect#clicked
1586 let names = !get_names () in
1587 let types_and_cons =
1589 (fun name (newinputt,cons_names_entry) ->
1590 let dom,mk_metasenv_and_expr =
1591 newinputt#get_term ~context:[] ~metasenv:[] in
1592 let consnamesstr = cons_names_entry#text in
1593 let cons_names = Str.split (Str.regexp " +") consnamesstr in
1595 disambiguate_input [] [] dom mk_metasenv_and_expr
1598 [] -> expr,cons_names
1599 | _ -> raise AmbiguousInput
1600 ) names type_widgets
1602 (* Let's see if so far the definition is well-typed *)
1603 let uri = !get_uri () in
1609 (fun name (ty,cons) ->
1612 (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in
1613 let res = (name, !inductive, ty, cons') in
1616 ) names types_and_cons
1618 (*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi
1619 anche quando paramsno > 0 ;-((((
1620 CicTypeChecker.typecheck_mutual_inductive_defs uri
1621 (tys,params,paramsno) ;
1623 get_name_context_context_and_subst :=
1627 (fun (namecontext,context,subst) name (ty,_) ->
1629 (Some (Cic.Name name))::namecontext,
1630 (Some (Cic.Name name, Cic.Decl ty))::context,
1631 (Cic.MutInd (uri,!i,[]))::subst
1634 ) ([],[],[]) names types_and_cons) ;
1635 let types_and_cons' =
1637 (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1638 names types_and_cons
1640 get_types_and_cons := (function () -> types_and_cons') ;
1645 output_html outputhtml
1646 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1649 and phase3 name cons =
1650 let get_cons_types = ref (function () -> assert false) in
1653 ~width:600 ~modal:true ~position:`CENTER
1654 ~title:(name ^ " Constructors")
1655 ~border_width:2 () in
1656 let vbox = GPack.vbox ~packing:window2#add () in
1657 let cons_type_widgets =
1659 (function consname ->
1661 GPack.hbox ~border_width:0
1662 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1664 GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1665 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1666 let scrolled_window =
1667 GBin.scrolled_window ~border_width:5
1668 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1670 new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1671 ~isnotempty_callback:
1673 (* (*non_empty_type := b ;*)
1674 okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1679 GPack.hbox ~border_width:0
1680 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1682 GButton.button ~label:"> Next"
1683 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1684 let _ = okb#misc#set_sensitive true in
1686 GButton.button ~label:"Abort"
1687 ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1688 ignore (window2#connect#destroy GMain.Main.quit) ;
1689 ignore (cancelb#connect#clicked window2#destroy) ;
1691 (okb#connect#clicked
1695 let namecontext,context,subst= !get_name_context_context_and_subst () in
1699 let dom,mk_metasenv_and_expr =
1700 inputt#get_term ~context:namecontext ~metasenv:[]
1703 disambiguate_input context [] dom mk_metasenv_and_expr
1707 let undebrujined_expr =
1709 (fun expr t -> CicSubstitution.subst t expr) expr subst
1711 name, undebrujined_expr
1712 | _ -> raise AmbiguousInput
1713 ) cons cons_type_widgets
1715 get_cons_types := (function () -> cons_types) ;
1719 output_html outputhtml
1720 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1723 GMain.Main.main () ;
1724 let okb_pressed = !chosen in
1726 if (not okb_pressed) then
1729 assert false (* The control never reaches this point *)
1732 (!get_cons_types ())
1735 (* No more phases left or Abort pressed *)
1737 GMain.Main.main () ;
1741 let uri = !get_uri () in
1744 let tys = !get_types_and_cons () in
1745 let obj = Cic.InductiveDefinition tys params !paramsno in
1748 prerr_endline (CicPp.ppobj obj) ;
1749 CicTypeChecker.typecheck_mutual_inductive_defs uri
1750 (tys,params,!paramsno) ;
1753 prerr_endline "Offending mutual (co)inductive type declaration:" ;
1754 prerr_endline (CicPp.ppobj obj) ;
1756 (* We already know that obj is well-typed. We need to add it to the *)
1757 (* environment in order to compute the inner-types without having to *)
1758 (* debrujin it or having to modify lots of other functions to avoid *)
1759 (* asking the environment for the MUTINDs we are defining now. *)
1760 CicEnvironment.put_inductive_definition uri obj ;
1762 show_in_show_window_obj uri obj
1765 output_html outputhtml
1766 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1770 let inputt = ((rendering_window ())#inputt : term_editor) in
1771 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1772 let output = ((rendering_window ())#output : GMathView.math_view) in
1773 let notebook = (rendering_window ())#notebook in
1775 let chosen = ref false in
1776 let get_parsed = ref (function _ -> assert false) in
1777 let get_uri = ref (function _ -> assert false) in
1778 let non_empty_type = ref false in
1781 ~width:600 ~modal:true ~title:"New Proof or Definition"
1782 ~border_width:2 () in
1783 let vbox = GPack.vbox ~packing:window#add () in
1785 GPack.hbox ~border_width:0
1786 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1788 GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1789 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1791 GEdit.entry ~editable:true
1792 ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1794 GPack.hbox ~border_width:0
1795 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1797 GMisc.label ~text:"Enter the theorem or definition type:"
1798 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1799 let scrolled_window =
1800 GBin.scrolled_window ~border_width:5
1801 ~packing:(vbox#pack ~expand:true ~padding:0) () in
1802 (* the content of the scrolled_window is moved below (see comment) *)
1804 GPack.hbox ~border_width:0
1805 ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1807 GButton.button ~label:"Ok"
1808 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1809 let _ = okb#misc#set_sensitive false in
1811 GButton.button ~label:"Cancel"
1812 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1813 (* moved here to have visibility of the ok button *)
1815 new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1816 ~isnotempty_callback:
1818 non_empty_type := b ;
1819 okb#misc#set_sensitive (b && uri_entry#text <> ""))
1822 newinputt#set_term inputt#get_as_string ;
1825 uri_entry#connect#changed
1827 okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1829 ignore (window#connect#destroy GMain.Main.quit) ;
1830 ignore (cancelb#connect#clicked window#destroy) ;
1832 (okb#connect#clicked
1836 let parsed = newinputt#get_term [] [] in
1837 let uristr = "cic:" ^ uri_entry#text in
1838 let uri = UriManager.uri_of_string uristr in
1839 if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1840 raise NotAUriToAConstant
1844 ignore (Getter.resolve uri) ;
1845 raise UriAlreadyInUse
1847 Getter.Unresolved ->
1848 get_parsed := (function () -> parsed) ;
1849 get_uri := (function () -> uri) ;
1854 output_html outputhtml
1855 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1858 GMain.Main.main () ;
1861 let dom,mk_metasenv_and_expr = !get_parsed () in
1863 disambiguate_input [] [] dom mk_metasenv_and_expr
1865 let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
1866 ProofEngine.proof :=
1867 Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1868 ProofEngine.goal := Some 1 ;
1869 refresh_sequent notebook ;
1870 refresh_proof output ;
1871 !save_set_sensitive true ;
1874 RefreshSequentException e ->
1875 output_html outputhtml
1876 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1877 "sequent: " ^ Printexc.to_string e ^ "</h1>")
1878 | RefreshProofException e ->
1879 output_html outputhtml
1880 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1881 "proof: " ^ Printexc.to_string e ^ "</h1>")
1883 output_html outputhtml
1884 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1887 let check_term_in_scratch scratch_window metasenv context expr =
1889 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1890 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1891 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1892 scratch_window#show () ;
1893 scratch_window#mmlwidget#load_tree ~dom:mml
1896 print_endline ("? " ^ CicPp.ppterm expr) ;
1900 let check scratch_window () =
1901 let inputt = ((rendering_window ())#inputt : term_editor) in
1902 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1904 match !ProofEngine.proof with
1906 | Some (_,metasenv,_,_) -> metasenv
1908 let context,names_context =
1910 match !ProofEngine.goal with
1913 let (_,canonical_context,_) =
1914 List.find (function (m,_,_) -> m=metano) metasenv
1921 Some (n,_) -> Some n
1926 let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1927 let (metasenv',expr) =
1928 disambiguate_input context metasenv dom mk_metasenv_and_expr
1930 check_term_in_scratch scratch_window metasenv' context expr
1933 output_html outputhtml
1934 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1938 (***********************)
1940 (***********************)
1942 let call_tactic tactic () =
1943 let notebook = (rendering_window ())#notebook in
1944 let output = ((rendering_window ())#output : GMathView.math_view) in
1945 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1946 let savedproof = !ProofEngine.proof in
1947 let savedgoal = !ProofEngine.goal in
1951 refresh_sequent notebook ;
1952 refresh_proof output
1954 RefreshSequentException e ->
1955 output_html outputhtml
1956 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1957 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1958 ProofEngine.proof := savedproof ;
1959 ProofEngine.goal := savedgoal ;
1960 refresh_sequent notebook
1961 | RefreshProofException e ->
1962 output_html outputhtml
1963 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1964 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1965 ProofEngine.proof := savedproof ;
1966 ProofEngine.goal := savedgoal ;
1967 refresh_sequent notebook ;
1968 refresh_proof output
1970 output_html outputhtml
1971 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1972 ProofEngine.proof := savedproof ;
1973 ProofEngine.goal := savedgoal ;
1977 let call_tactic_with_input tactic () =
1978 let notebook = (rendering_window ())#notebook in
1979 let output = ((rendering_window ())#output : GMathView.math_view) in
1980 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1981 let inputt = ((rendering_window ())#inputt : term_editor) in
1982 let savedproof = !ProofEngine.proof in
1983 let savedgoal = !ProofEngine.goal in
1984 let uri,metasenv,bo,ty =
1985 match !ProofEngine.proof with
1986 None -> assert false
1987 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1989 let canonical_context =
1990 match !ProofEngine.goal with
1991 None -> assert false
1993 let (_,canonical_context,_) =
1994 List.find (function (m,_,_) -> m=metano) metasenv
2001 Some (n,_) -> Some n
2006 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
2007 let (metasenv',expr) =
2008 disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
2010 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2012 refresh_sequent notebook ;
2013 refresh_proof output ;
2016 RefreshSequentException e ->
2017 output_html outputhtml
2018 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2019 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2020 ProofEngine.proof := savedproof ;
2021 ProofEngine.goal := savedgoal ;
2022 refresh_sequent notebook
2023 | RefreshProofException e ->
2024 output_html outputhtml
2025 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2026 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2027 ProofEngine.proof := savedproof ;
2028 ProofEngine.goal := savedgoal ;
2029 refresh_sequent notebook ;
2030 refresh_proof output
2032 output_html outputhtml
2033 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2034 ProofEngine.proof := savedproof ;
2035 ProofEngine.goal := savedgoal ;
2038 let call_tactic_with_goal_input tactic () =
2039 let module L = LogicalOperations in
2040 let module G = Gdome in
2041 let notebook = (rendering_window ())#notebook in
2042 let output = ((rendering_window ())#output : GMathView.math_view) in
2043 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2044 let savedproof = !ProofEngine.proof in
2045 let savedgoal = !ProofEngine.goal in
2046 match notebook#proofw#get_selection with
2049 ((node : Gdome.element)#getAttributeNS
2050 ~namespaceURI:helmns
2051 ~localName:(G.domString "xref"))#to_string
2053 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2057 match !current_goal_infos with
2058 Some (ids_to_terms, ids_to_father_ids,_) ->
2060 tactic (Hashtbl.find ids_to_terms id) ;
2061 refresh_sequent notebook ;
2062 refresh_proof output
2063 | None -> assert false (* "ERROR: No current term!!!" *)
2065 RefreshSequentException e ->
2066 output_html outputhtml
2067 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2068 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2069 ProofEngine.proof := savedproof ;
2070 ProofEngine.goal := savedgoal ;
2071 refresh_sequent notebook
2072 | RefreshProofException e ->
2073 output_html outputhtml
2074 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2075 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2076 ProofEngine.proof := savedproof ;
2077 ProofEngine.goal := savedgoal ;
2078 refresh_sequent notebook ;
2079 refresh_proof output
2081 output_html outputhtml
2082 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2083 ProofEngine.proof := savedproof ;
2084 ProofEngine.goal := savedgoal ;
2087 output_html outputhtml
2088 ("<h1 color=\"red\">No term selected</h1>")
2091 let call_tactic_with_input_and_goal_input tactic () =
2092 let module L = LogicalOperations in
2093 let module G = Gdome in
2094 let notebook = (rendering_window ())#notebook in
2095 let output = ((rendering_window ())#output : GMathView.math_view) in
2096 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2097 let inputt = ((rendering_window ())#inputt : term_editor) in
2098 let savedproof = !ProofEngine.proof in
2099 let savedgoal = !ProofEngine.goal in
2100 match notebook#proofw#get_selection with
2103 ((node : Gdome.element)#getAttributeNS
2104 ~namespaceURI:helmns
2105 ~localName:(G.domString "xref"))#to_string
2107 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2111 match !current_goal_infos with
2112 Some (ids_to_terms, ids_to_father_ids,_) ->
2114 let uri,metasenv,bo,ty =
2115 match !ProofEngine.proof with
2116 None -> assert false
2117 | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2119 let canonical_context =
2120 match !ProofEngine.goal with
2121 None -> assert false
2123 let (_,canonical_context,_) =
2124 List.find (function (m,_,_) -> m=metano) metasenv
2126 canonical_context in
2130 Some (n,_) -> Some n
2134 let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
2136 let (metasenv',expr) =
2137 disambiguate_input canonical_context metasenv dom
2138 mk_metasenv_and_expr
2140 ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2141 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2143 refresh_sequent notebook ;
2144 refresh_proof output ;
2146 | None -> assert false (* "ERROR: No current term!!!" *)
2148 RefreshSequentException e ->
2149 output_html outputhtml
2150 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2151 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2152 ProofEngine.proof := savedproof ;
2153 ProofEngine.goal := savedgoal ;
2154 refresh_sequent notebook
2155 | RefreshProofException e ->
2156 output_html outputhtml
2157 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2158 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2159 ProofEngine.proof := savedproof ;
2160 ProofEngine.goal := savedgoal ;
2161 refresh_sequent notebook ;
2162 refresh_proof output
2164 output_html outputhtml
2165 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2166 ProofEngine.proof := savedproof ;
2167 ProofEngine.goal := savedgoal ;
2170 output_html outputhtml
2171 ("<h1 color=\"red\">No term selected</h1>")
2174 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2175 let module L = LogicalOperations in
2176 let module G = Gdome in
2177 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2178 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2179 let savedproof = !ProofEngine.proof in
2180 let savedgoal = !ProofEngine.goal in
2181 match mmlwidget#get_selection with
2184 ((node : Gdome.element)#getAttributeNS
2185 ~namespaceURI:helmns
2186 ~localName:(G.domString "xref"))#to_string
2188 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2192 match !current_scratch_infos with
2193 (* term is the whole goal in the scratch_area *)
2194 Some (term,ids_to_terms, ids_to_father_ids,_) ->
2196 let expr = tactic term (Hashtbl.find ids_to_terms id) in
2197 let mml = mml_of_cic_term 111 expr in
2198 scratch_window#show () ;
2199 scratch_window#mmlwidget#load_tree ~dom:mml
2200 | None -> assert false (* "ERROR: No current term!!!" *)
2203 output_html outputhtml
2204 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2207 output_html outputhtml
2208 ("<h1 color=\"red\">No term selected</h1>")
2211 let call_tactic_with_hypothesis_input tactic () =
2212 let module L = LogicalOperations in
2213 let module G = Gdome in
2214 let notebook = (rendering_window ())#notebook in
2215 let output = ((rendering_window ())#output : GMathView.math_view) in
2216 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2217 let savedproof = !ProofEngine.proof in
2218 let savedgoal = !ProofEngine.goal in
2219 match notebook#proofw#get_selection with
2222 ((node : Gdome.element)#getAttributeNS
2223 ~namespaceURI:helmns
2224 ~localName:(G.domString "xref"))#to_string
2226 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2230 match !current_goal_infos with
2231 Some (_,_,ids_to_hypotheses) ->
2233 tactic (Hashtbl.find ids_to_hypotheses id) ;
2234 refresh_sequent notebook ;
2235 refresh_proof output
2236 | None -> assert false (* "ERROR: No current term!!!" *)
2238 RefreshSequentException e ->
2239 output_html outputhtml
2240 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2241 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2242 ProofEngine.proof := savedproof ;
2243 ProofEngine.goal := savedgoal ;
2244 refresh_sequent notebook
2245 | RefreshProofException e ->
2246 output_html outputhtml
2247 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2248 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2249 ProofEngine.proof := savedproof ;
2250 ProofEngine.goal := savedgoal ;
2251 refresh_sequent notebook ;
2252 refresh_proof output
2254 output_html outputhtml
2255 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2256 ProofEngine.proof := savedproof ;
2257 ProofEngine.goal := savedgoal ;
2260 output_html outputhtml
2261 ("<h1 color=\"red\">No term selected</h1>")
2265 let intros = call_tactic ProofEngine.intros;;
2266 let exact = call_tactic_with_input ProofEngine.exact;;
2267 let apply = call_tactic_with_input ProofEngine.apply;;
2268 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
2269 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2270 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2271 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2272 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2273 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2274 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2275 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2276 let cut = call_tactic_with_input ProofEngine.cut;;
2277 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2278 let letin = call_tactic_with_input ProofEngine.letin;;
2279 let ring = call_tactic ProofEngine.ring;;
2280 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2281 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2282 let fourier = call_tactic ProofEngine.fourier;;
2283 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2284 let reflexivity = call_tactic ProofEngine.reflexivity;;
2285 let symmetry = call_tactic ProofEngine.symmetry;;
2286 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2287 let exists = call_tactic ProofEngine.exists;;
2288 let split = call_tactic ProofEngine.split;;
2289 let left = call_tactic ProofEngine.left;;
2290 let right = call_tactic ProofEngine.right;;
2291 let assumption = call_tactic ProofEngine.assumption;;
2292 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2293 let absurd = call_tactic_with_input ProofEngine.absurd;;
2294 let contradiction = call_tactic ProofEngine.contradiction;;
2295 (* Galla: come dare alla tattica la lista di termini da decomporre?
2296 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
2299 let whd_in_scratch scratch_window =
2300 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2303 let reduce_in_scratch scratch_window =
2304 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2307 let simpl_in_scratch scratch_window =
2308 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2314 (**********************)
2315 (* END OF TACTICS *)
2316 (**********************)
2320 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2322 show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2325 output_html outputhtml
2326 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2329 exception NotADefinition;;
2332 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2333 let output = ((rendering_window ())#output : GMathView.math_view) in
2334 let notebook = (rendering_window ())#notebook in
2336 let uri = input_or_locate_uri ~title:"Open" in
2337 CicTypeChecker.typecheck uri ;
2338 let metasenv,bo,ty =
2339 match CicEnvironment.get_cooked_obj uri with
2340 Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2341 | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2344 | Cic.InductiveDefinition _ -> raise NotADefinition
2346 ProofEngine.proof :=
2347 Some (uri, metasenv, bo, ty) ;
2348 ProofEngine.goal := None ;
2349 refresh_sequent notebook ;
2350 refresh_proof output
2352 RefreshSequentException e ->
2353 output_html outputhtml
2354 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2355 "sequent: " ^ Printexc.to_string e ^ "</h1>")
2356 | RefreshProofException e ->
2357 output_html outputhtml
2358 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2359 "proof: " ^ Printexc.to_string e ^ "</h1>")
2361 output_html outputhtml
2362 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2366 let completeSearchPattern () =
2367 let inputt = ((rendering_window ())#inputt : term_editor) in
2368 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2370 let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
2371 let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
2372 ignore (MQueryLevels2.get_constraints expr)
2375 output_html outputhtml
2376 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2379 let choose_must list_of_must can =
2380 let chosen = ref None in
2381 let user_constraints = ref [] in
2384 ~modal:true ~title:"Query refinement." ~border_width:2 () in
2385 let vbox = GPack.vbox ~packing:window#add () in
2387 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2391 ("You can now specify the genericity of the query. " ^
2392 "The more generic the slower.")
2393 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2395 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2399 "Suggestion: start with faster queries before moving to more generic ones."
2400 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2402 GPack.notebook ~scrollable:true
2403 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2406 let last = List.length list_of_must in
2412 (if !page = 1 then "More generic" else
2413 if !page = last then "More precise" else " ") () in
2414 let expected_height = 25 * (List.length must + 2) in
2415 let height = if expected_height > 400 then 400 else expected_height in
2416 let scrolled_window =
2417 GBin.scrolled_window ~border_width:10 ~height ~width:600
2418 ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2420 GList.clist ~columns:2 ~packing:scrolled_window#add
2421 ~titles:["URI" ; "Position"] ()
2425 (function (uri,position) ->
2428 [uri; if position then "MainConclusion" else "Conclusion"]
2430 clist#set_row ~selectable:false n
2433 clist#columns_autosize ()
2436 let label = GMisc.label ~text:"User provided" () in
2438 GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2440 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2443 ~text:"Select the constraints that must be satisfied and press OK."
2444 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2445 let expected_height = 25 * (List.length can + 2) in
2446 let height = if expected_height > 400 then 400 else expected_height in
2447 let scrolled_window =
2448 GBin.scrolled_window ~border_width:10 ~height ~width:600
2449 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2451 GList.clist ~columns:2 ~packing:scrolled_window#add
2452 ~selection_mode:`EXTENDED
2453 ~titles:["URI" ; "Position"] ()
2457 (function (uri,position) ->
2460 [uri; if position then "MainConclusion" else "Conclusion"]
2462 clist#set_row ~selectable:true n
2465 clist#columns_autosize () ;
2467 (clist#connect#select_row
2468 (fun ~row ~column ~event ->
2469 user_constraints := (List.nth can row)::!user_constraints)) ;
2471 (clist#connect#unselect_row
2472 (fun ~row ~column ~event ->
2475 (function uri -> uri != (List.nth can row)) !user_constraints)) ;
2478 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2480 GButton.button ~label:"Ok"
2481 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2483 GButton.button ~label:"Abort"
2484 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2486 ignore (window#connect#destroy GMain.Main.quit) ;
2487 ignore (cancelb#connect#clicked window#destroy) ;
2489 (okb#connect#clicked
2490 (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2491 window#set_position `CENTER ;
2493 GMain.Main.main () ;
2495 None -> raise NoChoice
2497 if n = List.length list_of_must then
2498 (* user provided constraints *)
2501 List.nth list_of_must n
2504 let searchPattern () =
2505 let inputt = ((rendering_window ())#inputt : term_editor) in
2506 let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2509 match !ProofEngine.proof with
2510 None -> assert false
2511 | Some (_,metasenv,_,_) -> metasenv
2513 match !ProofEngine.goal with
2516 let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2517 let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
2518 let must = choose_must list_of_must can in
2519 let result = MQueryGenerator.searchPattern metasenv ey ty must can in
2523 wrong_xpointer_format_from_wrong_xpointer_format' uri
2526 " <h1>Backward Query: </h1>" ^
2527 " <pre>" ^ get_last_query result ^ "</pre>"
2529 output_html outputhtml html ;
2531 let rec filter_out =
2535 let tl',exc = filter_out tl in
2538 ProofEngine.can_apply
2539 (term_of_cic_textual_parser_uri
2540 (cic_textual_parser_uri_of_string uri))
2548 "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2549 uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2556 " <h1>Objects that can actually be applied: </h1> " ^
2557 String.concat "<br>" uris' ^ exc ^
2558 " <h1>Number of false matches: " ^
2559 string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2560 " <h1>Number of good matches: " ^
2561 string_of_int (List.length uris') ^ "</h1>"
2563 output_html outputhtml html' ;
2565 user_uri_choice ~title:"Ambiguous input."
2567 "Many lemmas can be successfully applied. Please, choose one:"
2570 inputt#set_term uri' ;
2574 output_html outputhtml
2575 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2578 let choose_selection
2579 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2581 let module G = Gdome in
2582 let rec aux element =
2583 if element#hasAttributeNS
2584 ~namespaceURI:helmns
2585 ~localName:(G.domString "xref")
2587 mmlwidget#set_selection (Some element)
2589 match element#get_parentNode with
2590 None -> assert false
2591 (*CSC: OCAML DIVERGES!
2592 | Some p -> aux (new G.element_of_node p)
2594 | Some p -> aux (new Gdome.element_of_node p)
2598 | None -> mmlwidget#set_selection None
2601 (* STUFF TO BUILD THE GTK INTERFACE *)
2603 (* Stuff for the widget settings *)
2605 let export_to_postscript (output : GMathView.math_view) =
2606 let lastdir = ref (Unix.getcwd ()) in
2609 GToolbox.select_file ~title:"Export to PostScript"
2610 ~dir:lastdir ~filename:"screenshot.ps" ()
2614 output#export_to_postscript ~filename:filename ();
2617 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2618 button_set_kerning button_set_transparency export_to_postscript_menu_item
2621 let is_set = button_t1#active in
2622 output#set_font_manager_type
2623 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2626 button_set_anti_aliasing#misc#set_sensitive true ;
2627 button_set_kerning#misc#set_sensitive true ;
2628 button_set_transparency#misc#set_sensitive true ;
2629 export_to_postscript_menu_item#misc#set_sensitive true ;
2633 button_set_anti_aliasing#misc#set_sensitive false ;
2634 button_set_kerning#misc#set_sensitive false ;
2635 button_set_transparency#misc#set_sensitive false ;
2636 export_to_postscript_menu_item#misc#set_sensitive false ;
2640 let set_anti_aliasing output button_set_anti_aliasing () =
2641 output#set_anti_aliasing button_set_anti_aliasing#active
2644 let set_kerning output button_set_kerning () =
2645 output#set_kerning button_set_kerning#active
2648 let set_transparency output button_set_transparency () =
2649 output#set_transparency button_set_transparency#active
2652 let changefont output font_size_spinb () =
2653 output#set_font_size font_size_spinb#value_as_int
2656 let set_log_verbosity output log_verbosity_spinb () =
2657 output#set_log_verbosity log_verbosity_spinb#value_as_int
2660 class settings_window (output : GMathView.math_view) sw
2661 export_to_postscript_menu_item selection_changed_callback
2663 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2665 GPack.vbox ~packing:settings_window#add () in
2668 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2669 ~border_width:5 ~packing:vbox#add () in
2671 GButton.toggle_button ~label:"activate t1 fonts"
2672 ~packing:(table#attach ~left:0 ~top:0) () in
2673 let button_set_anti_aliasing =
2674 GButton.toggle_button ~label:"set_anti_aliasing"
2675 ~packing:(table#attach ~left:0 ~top:1) () in
2676 let button_set_kerning =
2677 GButton.toggle_button ~label:"set_kerning"
2678 ~packing:(table#attach ~left:1 ~top:1) () in
2679 let button_set_transparency =
2680 GButton.toggle_button ~label:"set_transparency"
2681 ~packing:(table#attach ~left:2 ~top:1) () in
2684 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2685 ~border_width:5 ~packing:vbox#add () in
2686 let font_size_label =
2687 GMisc.label ~text:"font size:"
2688 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2689 let font_size_spinb =
2691 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2694 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2695 let log_verbosity_label =
2696 GMisc.label ~text:"log verbosity:"
2697 ~packing:(table#attach ~left:0 ~top:1) () in
2698 let log_verbosity_spinb =
2700 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2703 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2705 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2707 GButton.button ~label:"Close"
2708 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2710 method show = settings_window#show
2712 button_set_anti_aliasing#misc#set_sensitive false ;
2713 button_set_kerning#misc#set_sensitive false ;
2714 button_set_transparency#misc#set_sensitive false ;
2715 (* Signals connection *)
2716 ignore(button_t1#connect#clicked
2717 (activate_t1 output button_set_anti_aliasing button_set_kerning
2718 button_set_transparency export_to_postscript_menu_item button_t1)) ;
2719 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2720 ignore(button_set_anti_aliasing#connect#toggled
2721 (set_anti_aliasing output button_set_anti_aliasing));
2722 ignore(button_set_kerning#connect#toggled
2723 (set_kerning output button_set_kerning)) ;
2724 ignore(button_set_transparency#connect#toggled
2725 (set_transparency output button_set_transparency)) ;
2726 ignore(log_verbosity_spinb#connect#changed
2727 (set_log_verbosity output log_verbosity_spinb)) ;
2728 ignore(closeb#connect#clicked settings_window#misc#hide)
2731 (* Scratch window *)
2733 class scratch_window =
2735 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2737 GPack.vbox ~packing:window#add () in
2739 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2741 GButton.button ~label:"Whd"
2742 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2744 GButton.button ~label:"Reduce"
2745 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2747 GButton.button ~label:"Simpl"
2748 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2749 let scrolled_window =
2750 GBin.scrolled_window ~border_width:10
2751 ~packing:(vbox#pack ~expand:true ~padding:5) () in
2754 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2756 method mmlwidget = mmlwidget
2757 method show () = window#misc#hide () ; window#show ()
2759 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2760 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2761 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2762 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2763 ignore(simplb#connect#clicked (simpl_in_scratch self))
2767 let vbox1 = GPack.vbox () in
2769 val mutable proofw_ref = None
2770 val mutable compute_ref = None
2772 Lazy.force self#compute ;
2773 match proofw_ref with
2774 None -> assert false
2775 | Some proofw -> proofw
2776 method content = vbox1
2778 match compute_ref with
2779 None -> assert false
2780 | Some compute -> compute
2784 let scrolled_window1 =
2785 GBin.scrolled_window ~border_width:10
2786 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2788 GMathView.math_view ~width:400 ~height:275
2789 ~packing:(scrolled_window1#add) () in
2790 let _ = proofw_ref <- Some proofw in
2792 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2794 GButton.button ~label:"Exact"
2795 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2797 GButton.button ~label:"Intros"
2798 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2800 GButton.button ~label:"Apply"
2801 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2802 let elimsimplintrosb =
2803 GButton.button ~label:"ElimSimplIntros"
2804 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2806 GButton.button ~label:"ElimType"
2807 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2809 GButton.button ~label:"Whd"
2810 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2812 GButton.button ~label:"Reduce"
2813 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2815 GButton.button ~label:"Simpl"
2816 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2818 GButton.button ~label:"Fold_whd"
2819 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2821 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2823 GButton.button ~label:"Fold_reduce"
2824 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2826 GButton.button ~label:"Fold_simpl"
2827 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2829 GButton.button ~label:"Cut"
2830 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2832 GButton.button ~label:"Change"
2833 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2835 GButton.button ~label:"Let ... In"
2836 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2838 GButton.button ~label:"Ring"
2839 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2841 GButton.button ~label:"ClearBody"
2842 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2844 GButton.button ~label:"Clear"
2845 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2847 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2849 GButton.button ~label:"Fourier"
2850 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2852 GButton.button ~label:"RewriteSimpl ->"
2853 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2855 GButton.button ~label:"Reflexivity"
2856 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2858 GButton.button ~label:"Symmetry"
2859 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2861 GButton.button ~label:"Transitivity"
2862 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2864 GButton.button ~label:"Exists"
2865 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2867 GButton.button ~label:"Split"
2868 ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2870 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2872 GButton.button ~label:"Left"
2873 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2875 GButton.button ~label:"Right"
2876 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2878 GButton.button ~label:"Assumption"
2879 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2881 GButton.button ~label:"Generalize"
2882 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2884 GButton.button ~label:"Absurd"
2885 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2886 let contradictionb =
2887 GButton.button ~label:"Contradiction"
2888 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2889 let searchpatternb =
2890 GButton.button ~label:"SearchPattern_Apply"
2891 ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2893 ignore(exactb#connect#clicked exact) ;
2894 ignore(applyb#connect#clicked apply) ;
2895 ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2896 ignore(elimtypeb#connect#clicked elimtype) ;
2897 ignore(whdb#connect#clicked whd) ;
2898 ignore(reduceb#connect#clicked reduce) ;
2899 ignore(simplb#connect#clicked simpl) ;
2900 ignore(foldwhdb#connect#clicked fold_whd) ;
2901 ignore(foldreduceb#connect#clicked fold_reduce) ;
2902 ignore(foldsimplb#connect#clicked fold_simpl) ;
2903 ignore(cutb#connect#clicked cut) ;
2904 ignore(changeb#connect#clicked change) ;
2905 ignore(letinb#connect#clicked letin) ;
2906 ignore(ringb#connect#clicked ring) ;
2907 ignore(clearbodyb#connect#clicked clearbody) ;
2908 ignore(clearb#connect#clicked clear) ;
2909 ignore(fourierb#connect#clicked fourier) ;
2910 ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2911 ignore(reflexivityb#connect#clicked reflexivity) ;
2912 ignore(symmetryb#connect#clicked symmetry) ;
2913 ignore(transitivityb#connect#clicked transitivity) ;
2914 ignore(existsb#connect#clicked exists) ;
2915 ignore(splitb#connect#clicked split) ;
2916 ignore(leftb#connect#clicked left) ;
2917 ignore(rightb#connect#clicked right) ;
2918 ignore(assumptionb#connect#clicked assumption) ;
2919 ignore(generalizeb#connect#clicked generalize) ;
2920 ignore(absurdb#connect#clicked absurd) ;
2921 ignore(contradictionb#connect#clicked contradiction) ;
2922 ignore(introsb#connect#clicked intros) ;
2923 ignore(searchpatternb#connect#clicked searchPattern) ;
2924 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2930 let vbox1 = GPack.vbox () in
2931 let scrolled_window1 =
2932 GBin.scrolled_window ~border_width:10
2933 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2935 GMathView.math_view ~width:400 ~height:275
2936 ~packing:(scrolled_window1#add) () in
2938 method proofw = (assert false : GMathView.math_view)
2939 method content = vbox1
2940 method compute = (assert false : unit)
2944 let empty_page = new empty_page;;
2948 val notebook = GPack.notebook ()
2950 val mutable skip_switch_page_event = false
2951 val mutable empty = true
2952 method notebook = notebook
2954 let new_page = new page () in
2956 pages := !pages @ [n,lazy (setgoal n),new_page] ;
2957 notebook#append_page
2958 ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2959 new_page#content#coerce
2960 method remove_all_pages ~skip_switch_page_event:skip =
2962 notebook#remove_page 0 (* let's remove the empty page *)
2964 List.iter (function _ -> notebook#remove_page 0) !pages ;
2966 skip_switch_page_event <- skip
2967 method set_current_page ~may_skip_switch_page_event n =
2968 let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2969 let new_page = notebook#page_num page#content#coerce in
2970 if may_skip_switch_page_event && new_page <> notebook#current_page then
2971 skip_switch_page_event <- true ;
2972 notebook#goto_page new_page
2973 method set_empty_page =
2976 notebook#append_page
2977 ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2978 empty_page#content#coerce
2980 let (_,_,page) = List.nth !pages notebook#current_page in
2984 (notebook#connect#switch_page
2986 let skip = skip_switch_page_event in
2987 skip_switch_page_event <- false ;
2990 let (metano,setgoal,page) = List.nth !pages i in
2991 ProofEngine.goal := Some metano ;
2992 Lazy.force (page#compute) ;
3001 class rendering_window output (notebook : notebook) =
3002 let scratch_window = new scratch_window in
3004 GWindow.window ~title:"MathML viewer" ~border_width:0
3005 ~allow_shrink:false () in
3006 let vbox_for_menu = GPack.vbox ~packing:window#add () in
3008 let handle_box = GBin.handle_box ~border_width:2
3009 ~packing:(vbox_for_menu#pack ~padding:0) () in
3010 let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3011 let factory0 = new GMenu.factory menubar in
3012 let accel_group = factory0#accel_group in
3014 let file_menu = factory0#add_submenu "File" in
3015 let factory1 = new GMenu.factory file_menu ~accel_group in
3016 let export_to_postscript_menu_item =
3019 factory1#add_item "New Block of (Co)Inductive Definitions..."
3020 ~key:GdkKeysyms._B ~callback:new_inductive
3023 factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3026 let reopen_menu_item =
3027 factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3031 factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3032 ignore (factory1#add_separator ()) ;
3034 (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3036 let save_menu_item =
3037 factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3040 (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3041 ignore (!save_set_sensitive false);
3042 ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3043 ignore (!qed_set_sensitive false);
3044 ignore (factory1#add_separator ()) ;
3045 let export_to_postscript_menu_item =
3046 factory1#add_item "Export to PostScript..."
3047 ~callback:(export_to_postscript output) in
3048 ignore (factory1#add_separator ()) ;
3050 (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3051 export_to_postscript_menu_item
3054 let edit_menu = factory0#add_submenu "Edit Current Proof" in
3055 let factory2 = new GMenu.factory edit_menu ~accel_group in
3056 let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3057 let proveit_menu_item =
3058 factory2#add_item "Prove It" ~key:GdkKeysyms._I
3059 ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3061 let focus_menu_item =
3062 factory2#add_item "Focus" ~key:GdkKeysyms._F
3063 ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3066 focus_and_proveit_set_sensitive :=
3068 proveit_menu_item#misc#set_sensitive b ;
3069 focus_menu_item#misc#set_sensitive b
3071 let _ = !focus_and_proveit_set_sensitive false in
3072 (* edit term menu *)
3073 let edit_term_menu = factory0#add_submenu "Edit Term" in
3074 let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3075 let check_menu_item =
3076 factory5#add_item "Check Term" ~key:GdkKeysyms._C
3077 ~callback:(check scratch_window) in
3078 let _ = check_menu_item#misc#set_sensitive false in
3080 let settings_menu = factory0#add_submenu "Search" in
3081 let factory4 = new GMenu.factory settings_menu ~accel_group in
3083 factory4#add_item "Locate..." ~key:GdkKeysyms._T
3085 let searchPattern_menu_item =
3086 factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3087 ~callback:completeSearchPattern in
3088 let _ = searchPattern_menu_item#misc#set_sensitive false in
3089 let show_menu_item =
3090 factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3093 let settings_menu = factory0#add_submenu "Settings" in
3094 let factory3 = new GMenu.factory settings_menu ~accel_group in
3096 factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3097 ~callback:edit_aliases in
3098 let _ = factory3#add_separator () in
3100 factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3101 ~callback:(function _ -> (settings_window ())#show ()) in
3103 let _ = window#add_accel_group accel_group in
3107 ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3109 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3110 let scrolled_window0 =
3111 GBin.scrolled_window ~border_width:10
3112 ~packing:(vbox#pack ~expand:true ~padding:5) () in
3113 let _ = scrolled_window0#add output#coerce in
3115 GBin.frame ~label:"Insert Term"
3116 ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3117 let scrolled_window1 =
3118 GBin.scrolled_window ~border_width:5
3119 ~packing:frame#add () in
3121 new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3122 ~isnotempty_callback:
3124 check_menu_item#misc#set_sensitive b ;
3125 searchPattern_menu_item#misc#set_sensitive b) in
3127 GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3129 vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3131 GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3135 ~source:"<html><body bgColor=\"white\"></body></html>"
3136 ~width:400 ~height: 100
3141 method outputhtml = outputhtml
3142 method inputt = inputt
3143 method output = (output : GMathView.math_view)
3144 method notebook = notebook
3145 method show = window#show
3147 notebook#set_empty_page ;
3148 export_to_postscript_menu_item#misc#set_sensitive false ;
3149 check_term := (check_term_in_scratch scratch_window) ;
3151 (* signal handlers here *)
3152 ignore(output#connect#selection_changed
3154 choose_selection output elem ;
3155 !focus_and_proveit_set_sensitive true
3157 ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3158 let settings_window = new settings_window output scrolled_window0
3159 export_to_postscript_menu_item (choose_selection output) in
3160 set_settings_window settings_window ;
3161 set_outputhtml outputhtml ;
3162 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3163 Logger.log_callback :=
3164 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3169 let initialize_everything () =
3170 let module U = Unix in
3171 let output = GMathView.math_view ~width:350 ~height:280 () in
3172 let notebook = new notebook in
3173 let rendering_window' = new rendering_window output notebook in
3174 set_rendering_window rendering_window' ;
3175 mml_of_cic_term_ref := mml_of_cic_term ;
3176 rendering_window'#show () ;
3183 Mqint.set_database Mqint.postgres_db ;
3184 (* Mqint.init "dbname=helm_mowgli" ; *)
3185 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
3186 Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm";
3188 ignore (GtkMain.Main.init ()) ;
3189 initialize_everything () ;
3190 if !usedb then Mqint.close ();