1 (* Copyright (C) 2000, 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 (******************************************************************************)
36 (* GLOBAL CONSTANTS *)
38 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
42 " <body bgColor=\"white\">"
50 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
52 let htmlheader_and_content = ref htmlheader;;
54 let current_cic_infos = ref None;;
55 let current_goal_infos = ref None;;
56 let current_scratch_infos = ref None;;
61 let domImpl = Gdome.domImplementation ();;
65 domImpl#createDocumentFromURI
67 ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
69 ~uri:("styles/" ^ name) ()
71 Gdome_xslt.processStylesheet style
74 let d_c = parseStyle "drop_coercions.xsl";;
75 let tc1 = parseStyle "objtheorycontent.xsl";;
76 let hc2 = parseStyle "content_to_html.xsl";;
77 let l = parseStyle "link.xsl";;
79 let c1 = parseStyle "rootcontent.xsl";;
80 let g = parseStyle "genmmlid.xsl";;
81 let c2 = parseStyle "annotatedpres.xsl";;
84 let getterURL = Configuration.getter_url;;
85 let processorURL = Configuration.processor_url;;
87 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
89 ["processorURL", "'" ^ processorURL ^ "'" ;
90 "getterURL", "'" ^ getterURL ^ "'" ;
91 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
92 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
93 "UNICODEvsSYMBOL", "'symbol'" ;
94 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
95 "encoding", "'iso-8859-1'" ;
96 "media-type", "'text/html'" ;
97 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
98 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
99 "naturalLanguage", "'yes'" ;
100 "annotations", "'no'" ;
101 "explodeall", "'true()'" ;
102 "topurl", "'http://phd.cs.unibo.it/helm'" ;
103 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
106 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
108 ["processorURL", "'" ^ processorURL ^ "'" ;
109 "getterURL", "'" ^ getterURL ^ "'" ;
110 "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
111 "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
112 "UNICODEvsSYMBOL", "'symbol'" ;
113 "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
114 "encoding", "'iso-8859-1'" ;
115 "media-type", "'text/html'" ;
116 "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
117 "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
118 "naturalLanguage", "'no'" ;
119 "annotations", "'no'" ;
120 "explodeall", "'true()'" ;
121 "topurl", "'http://phd.cs.unibo.it/helm'" ;
122 "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
125 let parse_file filename =
126 let inch = open_in filename in
127 let rec read_lines () =
129 let line = input_line inch in
137 let applyStylesheets input styles args =
138 List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
142 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
144 Cic2Xml.print_object uri ids_to_inner_sorts annobj
147 Cic2Xml.print_inner_types uri ids_to_inner_sorts
150 let input = Xml2Gdome.document_of_xml domImpl xml in
151 (*CSC: We save the innertypes to disk so that we can retrieve them in the *)
152 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
154 Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
155 let output = applyStylesheets input mml_styles mml_args in
162 exception RefreshSequentException of exn;;
163 exception RefreshProofException of exn;;
165 let refresh_proof (output : GMathView.math_view) =
167 let uri,currentproof =
168 match !ProofEngine.proof with
170 | Some (uri,metasenv,bo,ty) ->
171 uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
174 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
176 Cic2acic.acic_object_of_cic_object currentproof
179 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
181 output#load_tree mml ;
182 current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
185 match !ProofEngine.proof with
187 | Some (uri,metasenv,bo,ty) ->
188 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ;
189 raise (RefreshProofException e)
192 let refresh_sequent (proofw : GMathView.math_view) =
194 match !ProofEngine.goal with
195 None -> proofw#unload
198 match !ProofEngine.proof with
200 | Some (_,metasenv,_,_) -> metasenv
202 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
203 let sequent_gdome,ids_to_terms,ids_to_father_ids =
204 SequentPp.XmlPp.print_sequent metasenv currentsequent
207 Xml2Gdome.document_of_xml domImpl sequent_gdome
210 applyStylesheets sequent_doc sequent_styles sequent_args
212 proofw#load_tree ~dom:sequent_mml ;
213 current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
217 match !ProofEngine.goal with
222 match !ProofEngine.proof with
224 | Some (_,metasenv,_,_) -> metasenv
226 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
227 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
228 raise (RefreshSequentException e)
232 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
233 ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
236 let mml_of_cic_term metano term =
238 match !ProofEngine.proof with
240 | Some (_,metasenv,_,_) -> metasenv
243 match !ProofEngine.goal with
246 let (_,canonical_context,_) =
247 List.find (function (m,_,_) -> m=metano) metasenv
251 let sequent_gdome,ids_to_terms,ids_to_father_ids =
252 SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
255 Xml2Gdome.document_of_xml domImpl sequent_gdome
258 applyStylesheets sequent_doc sequent_styles sequent_args ;
260 current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
264 let output_html outputhtml msg =
265 htmlheader_and_content := !htmlheader_and_content ^ msg ;
266 outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
267 outputhtml#set_topline (-1)
270 (***********************)
272 (***********************)
274 let call_tactic tactic rendering_window () =
275 let proofw = (rendering_window#proofw : GMathView.math_view) in
276 let output = (rendering_window#output : GMathView.math_view) in
277 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
278 let savedproof = !ProofEngine.proof in
279 let savedgoal = !ProofEngine.goal in
283 refresh_sequent proofw ;
286 RefreshSequentException e ->
287 output_html outputhtml
288 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
289 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
290 ProofEngine.proof := savedproof ;
291 ProofEngine.goal := savedgoal ;
292 refresh_sequent proofw
293 | RefreshProofException e ->
294 output_html outputhtml
295 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
296 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
297 ProofEngine.proof := savedproof ;
298 ProofEngine.goal := savedgoal ;
299 refresh_sequent proofw ;
302 output_html outputhtml
303 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
304 ProofEngine.proof := savedproof ;
305 ProofEngine.goal := savedgoal ;
309 let call_tactic_with_input tactic rendering_window () =
310 let proofw = (rendering_window#proofw : GMathView.math_view) in
311 let output = (rendering_window#output : GMathView.math_view) in
312 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
313 let inputt = (rendering_window#inputt : GEdit.text) in
314 let savedproof = !ProofEngine.proof in
315 let savedgoal = !ProofEngine.goal in
316 (*CSC: Gran cut&paste da sotto... *)
317 let inputlen = inputt#length in
318 let input = inputt#get_chars 0 inputlen ^ "\n" in
319 let lexbuf = Lexing.from_string input in
321 match !ProofEngine.proof with
323 | Some (curi,_,_,_) -> curi
326 match !ProofEngine.proof with
328 | Some (_,metasenv,_,_) -> metasenv
335 (match !ProofEngine.goal with
338 let (_,canonical_context,_) =
339 List.find (function (m,_,_) -> m=metano) metasenv
347 CicTextualParserContext.main curi context CicTextualLexer.token lexbuf
352 refresh_sequent proofw ;
356 CicTextualParser0.Eof ->
357 inputt#delete_text 0 inputlen
358 | RefreshSequentException e ->
359 output_html outputhtml
360 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
361 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
362 ProofEngine.proof := savedproof ;
363 ProofEngine.goal := savedgoal ;
364 refresh_sequent proofw
365 | RefreshProofException e ->
366 output_html outputhtml
367 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
368 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
369 ProofEngine.proof := savedproof ;
370 ProofEngine.goal := savedgoal ;
371 refresh_sequent proofw ;
374 output_html outputhtml
375 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
376 ProofEngine.proof := savedproof ;
377 ProofEngine.goal := savedgoal ;
380 let call_tactic_with_goal_input tactic rendering_window () =
381 let module L = LogicalOperations in
382 let module G = Gdome in
383 let proofw = (rendering_window#proofw : GMathView.math_view) in
384 let output = (rendering_window#output : GMathView.math_view) in
385 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
386 let savedproof = !ProofEngine.proof in
387 let savedgoal = !ProofEngine.goal in
388 match proofw#get_selection with
391 ((node : Gdome.element)#getAttributeNS
393 ~localName:(G.domString "xref"))#to_string
395 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
399 match !current_goal_infos with
400 Some (ids_to_terms, ids_to_father_ids) ->
402 tactic (Hashtbl.find ids_to_terms id) ;
403 refresh_sequent rendering_window#proofw ;
404 refresh_proof rendering_window#output
405 | None -> assert false (* "ERROR: No current term!!!" *)
407 RefreshSequentException e ->
408 output_html outputhtml
409 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
410 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
411 ProofEngine.proof := savedproof ;
412 ProofEngine.goal := savedgoal ;
413 refresh_sequent proofw
414 | RefreshProofException e ->
415 output_html outputhtml
416 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
417 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
418 ProofEngine.proof := savedproof ;
419 ProofEngine.goal := savedgoal ;
420 refresh_sequent proofw ;
423 output_html outputhtml
424 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
425 ProofEngine.proof := savedproof ;
426 ProofEngine.goal := savedgoal ;
429 output_html outputhtml
430 ("<h1 color=\"red\">No term selected</h1>")
433 let call_tactic_with_input_and_goal_input tactic rendering_window () =
434 let module L = LogicalOperations in
435 let module G = Gdome in
436 let proofw = (rendering_window#proofw : GMathView.math_view) in
437 let output = (rendering_window#output : GMathView.math_view) in
438 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
439 let inputt = (rendering_window#inputt : GEdit.text) in
440 let savedproof = !ProofEngine.proof in
441 let savedgoal = !ProofEngine.goal in
442 match proofw#get_selection with
445 ((node : Gdome.element)#getAttributeNS
447 ~localName:(G.domString "xref"))#to_string
449 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
453 match !current_goal_infos with
454 Some (ids_to_terms, ids_to_father_ids) ->
456 (* Let's parse the input *)
457 let inputlen = inputt#length in
458 let input = inputt#get_chars 0 inputlen ^ "\n" in
459 let lexbuf = Lexing.from_string input in
461 match !ProofEngine.proof with
463 | Some (curi,_,_,_) -> curi
466 match !ProofEngine.proof with
468 | Some (_,metasenv,_,_) -> metasenv
475 (match !ProofEngine.goal with
478 let (_,canonical_context,_) =
479 List.find (function (m,_,_) -> m=metano) metasenv
488 CicTextualParserContext.main curi context
489 CicTextualLexer.token lexbuf
493 tactic ~goal_input:(Hashtbl.find ids_to_terms id)
495 refresh_sequent proofw ;
499 CicTextualParser0.Eof ->
500 inputt#delete_text 0 inputlen
502 | None -> assert false (* "ERROR: No current term!!!" *)
504 RefreshSequentException e ->
505 output_html outputhtml
506 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
507 "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
508 ProofEngine.proof := savedproof ;
509 ProofEngine.goal := savedgoal ;
510 refresh_sequent proofw
511 | RefreshProofException e ->
512 output_html outputhtml
513 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
514 "proof: " ^ Printexc.to_string e ^ "</h1>") ;
515 ProofEngine.proof := savedproof ;
516 ProofEngine.goal := savedgoal ;
517 refresh_sequent proofw ;
520 output_html outputhtml
521 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
522 ProofEngine.proof := savedproof ;
523 ProofEngine.goal := savedgoal ;
526 output_html outputhtml
527 ("<h1 color=\"red\">No term selected</h1>")
530 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
531 let module L = LogicalOperations in
532 let module G = Gdome in
533 let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
534 let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
535 let savedproof = !ProofEngine.proof in
536 let savedgoal = !ProofEngine.goal in
537 match mmlwidget#get_selection with
540 ((node : Gdome.element)#getAttributeNS
542 ~localName:(G.domString "xref"))#to_string
544 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
548 match !current_scratch_infos with
549 (* term is the whole goal in the scratch_area *)
550 Some (term,ids_to_terms, ids_to_father_ids) ->
552 let expr = tactic term (Hashtbl.find ids_to_terms id) in
553 let mml = mml_of_cic_term 111 expr in
554 scratch_window#show () ;
555 scratch_window#mmlwidget#load_tree ~dom:mml
556 | None -> assert false (* "ERROR: No current term!!!" *)
559 output_html outputhtml
560 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
563 output_html outputhtml
564 ("<h1 color=\"red\">No term selected</h1>")
567 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
568 let exact rendering_window =
569 call_tactic_with_input ProofEngine.exact rendering_window
571 let apply rendering_window =
572 call_tactic_with_input ProofEngine.apply rendering_window
574 let elimintrossimpl rendering_window =
575 call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
577 let whd rendering_window =
578 call_tactic_with_goal_input ProofEngine.whd rendering_window
580 let reduce rendering_window =
581 call_tactic_with_goal_input ProofEngine.reduce rendering_window
583 let simpl rendering_window =
584 call_tactic_with_goal_input ProofEngine.simpl rendering_window
586 let fold rendering_window =
587 call_tactic_with_input ProofEngine.fold rendering_window
589 let cut rendering_window =
590 call_tactic_with_input ProofEngine.cut rendering_window
592 let change rendering_window =
593 call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
595 let letin rendering_window =
596 call_tactic_with_input ProofEngine.letin rendering_window
600 let whd_in_scratch scratch_window =
601 call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
604 let reduce_in_scratch scratch_window =
605 call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
608 let simpl_in_scratch scratch_window =
609 call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
615 (**********************)
617 (**********************)
619 exception OpenConjecturesStillThere;;
620 exception WrongProof;;
622 let qed rendering_window () =
623 match !ProofEngine.proof with
625 | Some (uri,[],bo,ty) ->
627 CicReduction.are_convertible []
628 (CicTypeChecker.type_of_aux' [] [] bo) ty
631 (*CSC: Wrong: [] is just plainly wrong *)
632 let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
634 (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
637 Cic2acic.acic_object_of_cic_object proof
640 mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
642 (rendering_window#output : GMathView.math_view)#load_tree mml ;
643 current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
647 | _ -> raise OpenConjecturesStillThere
651 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
653 let dtdname = "/projects/helm/V7/dtd/cic.dtd";;
655 let save rendering_window () =
656 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
657 match !ProofEngine.proof with
659 | Some (uri, metasenv, bo, ty) ->
661 Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
663 let (acurrentproof,_,_,ids_to_inner_sorts,_) =
664 Cic2acic.acic_object_of_cic_object currentproof
666 let xml = Cic2Xml.print_object uri ids_to_inner_sorts acurrentproof in
668 [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
670 ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
674 Xml.pp ~quiet:true xml' (Some "/public/sacerdot/currentproof") ;
675 output_html outputhtml
676 ("<h1 color=\"Green\">Current proof saved to " ^
677 "/public/sacerdot/currentproof</h1>")
680 let load rendering_window () =
681 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
682 let output = (rendering_window#output : GMathView.math_view) in
683 let proofw = (rendering_window#proofw : GMathView.math_view) in
685 let uri = UriManager.uri_of_string "cic:/dummy.con" in
686 match CicParser.obj_of_xml "/public/sacerdot/currentproof" uri with
687 Cic.CurrentProof (_,metasenv,bo,ty) ->
689 Some (uri, metasenv, bo, ty) ;
693 | (metano,_,_)::_ -> Some metano
695 refresh_proof output ;
696 refresh_sequent proofw ;
697 output_html outputhtml
698 ("<h1 color=\"Green\">Current proof loaded from " ^
699 "/public/sacerdot/currentproof</h1>")
702 RefreshSequentException e ->
703 output_html outputhtml
704 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
705 "sequent: " ^ Printexc.to_string e ^ "</h1>")
706 | RefreshProofException e ->
707 output_html outputhtml
708 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
709 "proof: " ^ Printexc.to_string e ^ "</h1>")
711 output_html outputhtml
712 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
715 let proveit rendering_window () =
716 let module L = LogicalOperations in
717 let module G = Gdome in
718 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
719 match rendering_window#output#get_selection with
722 ((node : Gdome.element)#getAttributeNS
724 ((element : G.element)#getAttributeNS
727 ~localName:(G.domString "xref"))#to_string
729 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
733 match !current_cic_infos with
734 Some (ids_to_terms, ids_to_father_ids) ->
736 L.to_sequent id ids_to_terms ids_to_father_ids ;
737 refresh_proof rendering_window#output ;
738 refresh_sequent rendering_window#proofw
739 | None -> assert false (* "ERROR: No current term!!!" *)
741 RefreshSequentException e ->
742 output_html outputhtml
743 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
744 "sequent: " ^ Printexc.to_string e ^ "</h1>")
745 | RefreshProofException e ->
746 output_html outputhtml
747 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
748 "proof: " ^ Printexc.to_string e ^ "</h1>")
750 output_html outputhtml
751 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
753 | None -> assert false (* "ERROR: No selection!!!" *)
756 let focus rendering_window () =
757 let module L = LogicalOperations in
758 let module G = Gdome in
759 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
760 match rendering_window#output#get_selection with
763 ((node : Gdome.element)#getAttributeNS
765 ((element : G.element)#getAttributeNS
768 ~localName:(G.domString "xref"))#to_string
770 if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
774 match !current_cic_infos with
775 Some (ids_to_terms, ids_to_father_ids) ->
777 L.focus id ids_to_terms ids_to_father_ids ;
778 refresh_sequent rendering_window#proofw
779 | None -> assert false (* "ERROR: No current term!!!" *)
781 RefreshSequentException e ->
782 output_html outputhtml
783 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
784 "sequent: " ^ Printexc.to_string e ^ "</h1>")
785 | RefreshProofException e ->
786 output_html outputhtml
787 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
788 "proof: " ^ Printexc.to_string e ^ "</h1>")
790 output_html outputhtml
791 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
793 | None -> assert false (* "ERROR: No selection!!!" *)
796 exception NoPrevGoal;;
797 exception NoNextGoal;;
799 let prevgoal metasenv metano =
803 | [(m,_,_)] -> raise NoPrevGoal
804 | (n,_,_)::(m,_,_)::_ when m=metano -> n
810 let nextgoal metasenv metano =
814 | [(m,_,_)] when m = metano -> raise NoNextGoal
815 | (m,_,_)::(n,_,_)::_ when m=metano -> n
821 let prev_or_next_goal select_goal rendering_window () =
822 let module L = LogicalOperations in
823 let module G = Gdome in
824 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
826 match !ProofEngine.proof with
828 | Some (_,metasenv,_,_) -> metasenv
831 match !ProofEngine.goal with
836 ProofEngine.goal := Some (select_goal metasenv metano) ;
837 refresh_sequent rendering_window#proofw
839 RefreshSequentException e ->
840 output_html outputhtml
841 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
842 "sequent: " ^ Printexc.to_string e ^ "</h1>")
844 output_html outputhtml
845 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
848 exception NotADefinition;;
850 let open_ rendering_window () =
851 let inputt = (rendering_window#inputt : GEdit.text) in
852 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
853 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
854 let output = (rendering_window#output : GMathView.math_view) in
855 let proofw = (rendering_window#proofw : GMathView.math_view) in
856 let inputlen = inputt#length in
857 let input = inputt#get_chars 0 inputlen ^ "\n" in
859 let uri = UriManager.uri_of_string ("cic:" ^ input) in
860 CicTypeChecker.typecheck uri ;
862 match CicEnvironment.get_cooked_obj uri 0 with
863 Cic.Definition (_,bo,ty,_) -> [],bo,ty
864 | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
867 | Cic.InductiveDefinition _ -> raise NotADefinition
870 Some (uri, metasenv, bo, ty) ;
871 ProofEngine.goal := None ;
872 refresh_sequent proofw ;
873 refresh_proof output ;
874 inputt#delete_text 0 inputlen ;
875 ignore(oldinputt#insert_text input oldinputt#length)
877 RefreshSequentException e ->
878 output_html outputhtml
879 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
880 "sequent: " ^ Printexc.to_string e ^ "</h1>")
881 | RefreshProofException e ->
882 output_html outputhtml
883 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
884 "proof: " ^ Printexc.to_string e ^ "</h1>")
886 output_html outputhtml
887 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
890 let state rendering_window () =
891 let inputt = (rendering_window#inputt : GEdit.text) in
892 let oldinputt = (rendering_window#oldinputt : GEdit.text) in
893 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
894 let output = (rendering_window#output : GMathView.math_view) in
895 let proofw = (rendering_window#proofw : GMathView.math_view) in
896 let inputlen = inputt#length in
897 let input = inputt#get_chars 0 inputlen ^ "\n" in
898 (* Do something interesting *)
899 let lexbuf = Lexing.from_string input in
902 (* Execute the actions *)
903 match CicTextualParser.main CicTextualLexer.token lexbuf with
906 let _ = CicTypeChecker.type_of_aux' [] [] expr in
908 Some (UriManager.uri_of_string "cic:/dummy.con",
909 [1,[],expr], Cic.Meta (1,[]), expr) ;
910 ProofEngine.goal := Some 1 ;
911 refresh_sequent proofw ;
912 refresh_proof output ;
915 CicTextualParser0.Eof ->
916 inputt#delete_text 0 inputlen ;
917 ignore(oldinputt#insert_text input oldinputt#length)
918 | RefreshSequentException e ->
919 output_html outputhtml
920 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
921 "sequent: " ^ Printexc.to_string e ^ "</h1>")
922 | RefreshProofException e ->
923 output_html outputhtml
924 ("<h1 color=\"red\">Exception raised during the refresh of the " ^
925 "proof: " ^ Printexc.to_string e ^ "</h1>")
927 output_html outputhtml
928 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
931 let check rendering_window scratch_window () =
932 let inputt = (rendering_window#inputt : GEdit.text) in
933 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
934 let output = (rendering_window#output : GMathView.math_view) in
935 let proofw = (rendering_window#proofw : GMathView.math_view) in
936 let inputlen = inputt#length in
937 let input = inputt#get_chars 0 inputlen ^ "\n" in
939 match !ProofEngine.proof with
940 None -> UriManager.uri_of_string "cic:/dummy.con", []
941 | Some (curi,metasenv,_,_) -> curi,metasenv
943 let context,names_context =
945 match !ProofEngine.goal with
948 let (_,canonical_context,_) =
949 List.find (function (m,_,_) -> m=metano) metasenv
960 (* Do something interesting *)
961 let lexbuf = Lexing.from_string input in
964 (* Execute the actions *)
966 CicTextualParserContext.main curi names_context CicTextualLexer.token
972 let ty = CicTypeChecker.type_of_aux' metasenv context expr in
973 let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
974 scratch_window#show () ;
975 scratch_window#mmlwidget#load_tree ~dom:mml
978 print_endline ("? " ^ CicPp.ppterm expr) ;
982 CicTextualParser0.Eof -> ()
984 output_html outputhtml
985 ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
988 let locate rendering_window () =
989 let inputt = (rendering_window#inputt : GEdit.text) in
990 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
991 let inputlen = inputt#length in
992 let input = inputt#get_chars 0 inputlen in
993 output_html outputhtml (
995 match Str.split (Str.regexp "[ \t]+") input with
998 inputt#delete_text 0 inputlen;
1001 e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
1005 let backward rendering_window () =
1006 let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1007 let inputt = (rendering_window#inputt : GEdit.text) in
1008 let inputlen = inputt#length in
1009 let input = inputt#get_chars 0 inputlen in
1010 let level = int_of_string input in
1012 match !ProofEngine.proof with
1013 None -> assert false
1014 | Some (_,metasenv,_,_) -> metasenv
1017 match !ProofEngine.goal with
1021 List.find (function (m,_,_) -> m=metano) metasenv
1023 Mquery.backward ty level
1025 output_html outputhtml result
1027 let choose_selection
1028 (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1030 let module G = Gdome in
1031 let rec aux element =
1032 if element#hasAttributeNS
1033 ~namespaceURI:helmns
1034 ~localName:(G.domString "xref")
1036 mmlwidget#set_selection (Some element)
1038 match element#get_parentNode with
1039 None -> assert false
1040 (*CSC: OCAML DIVERGES!
1041 | Some p -> aux (new G.element_of_node p)
1043 | Some p -> aux (new Gdome.element_of_node p)
1047 | None -> mmlwidget#set_selection None
1050 (* STUFF TO BUILD THE GTK INTERFACE *)
1052 (* Stuff for the widget settings *)
1054 let export_to_postscript (output : GMathView.math_view) () =
1055 output#export_to_postscript ~filename:"output.ps" ();
1058 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1059 button_set_kerning button_set_transparency button_export_to_postscript
1062 let is_set = button_t1#active in
1063 output#set_font_manager_type
1064 (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1067 button_set_anti_aliasing#misc#set_sensitive true ;
1068 button_set_kerning#misc#set_sensitive true ;
1069 button_set_transparency#misc#set_sensitive true ;
1070 button_export_to_postscript#misc#set_sensitive true ;
1074 button_set_anti_aliasing#misc#set_sensitive false ;
1075 button_set_kerning#misc#set_sensitive false ;
1076 button_set_transparency#misc#set_sensitive false ;
1077 button_export_to_postscript#misc#set_sensitive false ;
1081 let set_anti_aliasing output button_set_anti_aliasing () =
1082 output#set_anti_aliasing button_set_anti_aliasing#active
1085 let set_kerning output button_set_kerning () =
1086 output#set_kerning button_set_kerning#active
1089 let set_transparency output button_set_transparency () =
1090 output#set_transparency button_set_transparency#active
1093 let changefont output font_size_spinb () =
1094 output#set_font_size font_size_spinb#value_as_int
1097 let set_log_verbosity output log_verbosity_spinb () =
1098 output#set_log_verbosity log_verbosity_spinb#value_as_int
1101 class settings_window (output : GMathView.math_view) sw
1102 button_export_to_postscript selection_changed_callback
1104 let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1106 GPack.vbox ~packing:settings_window#add () in
1109 ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1110 ~border_width:5 ~packing:vbox#add () in
1112 GButton.toggle_button ~label:"activate t1 fonts"
1113 ~packing:(table#attach ~left:0 ~top:0) () in
1114 let button_set_anti_aliasing =
1115 GButton.toggle_button ~label:"set_anti_aliasing"
1116 ~packing:(table#attach ~left:0 ~top:1) () in
1117 let button_set_kerning =
1118 GButton.toggle_button ~label:"set_kerning"
1119 ~packing:(table#attach ~left:1 ~top:1) () in
1120 let button_set_transparency =
1121 GButton.toggle_button ~label:"set_transparency"
1122 ~packing:(table#attach ~left:2 ~top:1) () in
1125 ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1126 ~border_width:5 ~packing:vbox#add () in
1127 let font_size_label =
1128 GMisc.label ~text:"font size:"
1129 ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1130 let font_size_spinb =
1132 GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1135 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1136 let log_verbosity_label =
1137 GMisc.label ~text:"log verbosity:"
1138 ~packing:(table#attach ~left:0 ~top:1) () in
1139 let log_verbosity_spinb =
1141 GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1144 ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1146 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1148 GButton.button ~label:"Close"
1149 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1151 method show = settings_window#show
1153 button_set_anti_aliasing#misc#set_sensitive false ;
1154 button_set_kerning#misc#set_sensitive false ;
1155 button_set_transparency#misc#set_sensitive false ;
1156 (* Signals connection *)
1157 ignore(button_t1#connect#clicked
1158 (activate_t1 output button_set_anti_aliasing button_set_kerning
1159 button_set_transparency button_export_to_postscript button_t1)) ;
1160 ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1161 ignore(button_set_anti_aliasing#connect#toggled
1162 (set_anti_aliasing output button_set_anti_aliasing));
1163 ignore(button_set_kerning#connect#toggled
1164 (set_kerning output button_set_kerning)) ;
1165 ignore(button_set_transparency#connect#toggled
1166 (set_transparency output button_set_transparency)) ;
1167 ignore(log_verbosity_spinb#connect#changed
1168 (set_log_verbosity output log_verbosity_spinb)) ;
1169 ignore(closeb#connect#clicked settings_window#misc#hide)
1172 (* Scratch window *)
1174 class scratch_window outputhtml =
1176 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1178 GPack.vbox ~packing:window#add () in
1180 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1182 GButton.button ~label:"Whd"
1183 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1185 GButton.button ~label:"Reduce"
1186 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1188 GButton.button ~label:"Simpl"
1189 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1190 let scrolled_window =
1191 GBin.scrolled_window ~border_width:10
1192 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1195 ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1197 method outputhtml = outputhtml
1198 method mmlwidget = mmlwidget
1199 method show () = window#misc#hide () ; window#show ()
1201 ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1202 ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1203 ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1204 ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1205 ignore(simplb#connect#clicked (simpl_in_scratch self))
1210 class rendering_window output proofw (label : GMisc.label) =
1212 GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1214 GPack.hbox ~packing:window#add () in
1216 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1217 let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1218 let scrolled_window0 =
1219 GBin.scrolled_window ~border_width:10
1220 ~packing:(vbox#pack ~expand:true ~padding:5) () in
1221 let _ = scrolled_window0#add output#coerce in
1223 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1225 GButton.button ~label:"Settings"
1226 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1227 let button_export_to_postscript =
1228 GButton.button ~label:"export_to_postscript"
1229 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1231 GButton.button ~label:"Qed"
1232 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1234 GButton.button ~label:"Save"
1235 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1237 GButton.button ~label:"Load"
1238 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1240 GButton.button ~label:"Close"
1241 ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1243 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1245 GButton.button ~label:"Prove It"
1246 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1248 GButton.button ~label:"Focus"
1249 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1251 GButton.button ~label:"<"
1252 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1254 GButton.button ~label:">"
1255 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1256 let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1257 ~packing:(vbox#pack ~padding:5) () in
1259 GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1261 GButton.button ~label:"State"
1262 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1264 GButton.button ~label:"Open"
1265 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1267 GButton.button ~label:"Check"
1268 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1270 GButton.button ~label:"Locate"
1271 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1273 GButton.button ~label:"Backward"
1274 ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1275 let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1276 ~packing:(vbox#pack ~padding:5) () in
1278 GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1279 let scrolled_window1 =
1280 GBin.scrolled_window ~border_width:10
1281 ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1282 let _ = scrolled_window1#add proofw#coerce in
1284 GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1286 GButton.button ~label:"Exact"
1287 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1289 GButton.button ~label:"Intros"
1290 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1292 GButton.button ~label:"Apply"
1293 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1294 let elimintrossimplb =
1295 GButton.button ~label:"ElimIntrosSimpl"
1296 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1298 GButton.button ~label:"Whd"
1299 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1301 GButton.button ~label:"Reduce"
1302 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1304 GButton.button ~label:"Simpl"
1305 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1307 GButton.button ~label:"Fold"
1308 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1310 GButton.button ~label:"Cut"
1311 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1313 GButton.button ~label:"Change"
1314 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1316 GButton.button ~label:"Let ... In"
1317 ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1320 ~source:"<html><body bgColor=\"white\"></body></html>"
1321 ~width:400 ~height: 200
1322 ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1324 let scratch_window = new scratch_window outputhtml in
1326 method outputhtml = outputhtml
1327 method oldinputt = oldinputt
1328 method inputt = inputt
1329 method output = (output : GMathView.math_view)
1330 method proofw = (proofw : GMathView.math_view)
1331 method show = window#show
1333 button_export_to_postscript#misc#set_sensitive false ;
1335 (* signal handlers here *)
1336 ignore(output#connect#selection_changed
1337 (function elem -> proofw#unload ; choose_selection output elem)) ;
1338 ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1339 ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1340 let settings_window = new settings_window output scrolled_window0
1341 button_export_to_postscript (choose_selection output) in
1342 ignore(settingsb#connect#clicked settings_window#show) ;
1343 ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1344 ignore(qedb#connect#clicked (qed self)) ;
1345 ignore(saveb#connect#clicked (save self)) ;
1346 ignore(loadb#connect#clicked (load self)) ;
1347 ignore(proveitb#connect#clicked (proveit self)) ;
1348 ignore(focusb#connect#clicked (focus self)) ;
1349 ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1350 ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1351 ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1352 ignore(stateb#connect#clicked (state self)) ;
1353 ignore(openb#connect#clicked (open_ self)) ;
1354 ignore(checkb#connect#clicked (check self scratch_window)) ;
1355 ignore(locateb#connect#clicked (locate self)) ;
1356 ignore(backwardb#connect#clicked (backward self)) ;
1357 ignore(exactb#connect#clicked (exact self)) ;
1358 ignore(applyb#connect#clicked (apply self)) ;
1359 ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
1360 ignore(whdb#connect#clicked (whd self)) ;
1361 ignore(reduceb#connect#clicked (reduce self)) ;
1362 ignore(simplb#connect#clicked (simpl self)) ;
1363 ignore(foldb#connect#clicked (fold self)) ;
1364 ignore(cutb#connect#clicked (cut self)) ;
1365 ignore(changeb#connect#clicked (change self)) ;
1366 ignore(letinb#connect#clicked (letin self)) ;
1367 ignore(introsb#connect#clicked (intros self)) ;
1368 Logger.log_callback :=
1369 (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1374 let initialize_everything () =
1375 let module U = Unix in
1376 let output = GMathView.math_view ~width:400 ~height:280 ()
1377 and proofw = GMathView.math_view ~width:400 ~height:275 ()
1378 and label = GMisc.label ~text:"gTopLevel" () in
1379 let rendering_window =
1380 new rendering_window output proofw label
1382 rendering_window#show () ;
1387 CicCooking.init () ;
1389 ignore (GtkMain.Main.init ()) ;
1390 initialize_everything () ;