]> matita.cs.unibo.it Git - helm.git/blob - helm/gTopLevel/gTopLevel.ml
Added buttons for new tactics Injection and Discriminate
[helm.git] / helm / gTopLevel / gTopLevel.ml
1 (* Copyright (C) 2000-2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (******************************************************************************)
27 (*                                                                            *)
28 (*                               PROJECT HELM                                 *)
29 (*                                                                            *)
30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
31 (*                                 06/01/2002                                 *)
32 (*                                                                            *)
33 (*                                                                            *)
34 (******************************************************************************)
35
36
37 (* GLOBAL CONSTANTS *)
38
39 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
40
41 let htmlheader =
42  "<html>" ^
43  " <body bgColor=\"white\">"
44 ;;
45
46 let htmlfooter =
47  " </body>" ^
48  "</html>"
49 ;;
50
51 let prooffile =
52  try
53   Sys.getenv "GTOPLEVEL_PROOFFILE"
54  with
55   Not_found -> "/public/currentproof"
56 ;;
57
58 let prooffiletype =
59  try
60   Sys.getenv "GTOPLEVEL_PROOFFILETYPE"
61  with
62   Not_found -> "/public/currentprooftype"
63 ;;
64
65 let postgresqlconnectionstring =
66  try
67   Sys.getenv "POSTGRESQL_CONNECTION_STRING"
68  with
69   Not_found -> "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
70 ;;
71
72 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
73
74 let htmlheader_and_content = ref htmlheader;;
75
76 let check_term = ref (fun _ _ _ -> assert false);;
77
78 exception RenderingWindowsNotInitialized;;
79
80 let set_rendering_window,rendering_window =
81  let rendering_window_ref = ref None in
82   (function rw -> rendering_window_ref := Some rw),
83   (function () ->
84     match !rendering_window_ref with
85        None -> raise RenderingWindowsNotInitialized
86      | Some rw -> rw
87   )
88 ;;
89
90 exception SettingsWindowsNotInitialized;;
91
92 let set_settings_window,settings_window =
93  let settings_window_ref = ref None in
94   (function rw -> settings_window_ref := Some rw),
95   (function () ->
96     match !settings_window_ref with
97        None -> raise SettingsWindowsNotInitialized
98      | Some rw -> rw
99   )
100 ;;
101
102 exception OutputHtmlNotInitialized;;
103
104 let set_outputhtml,outputhtml =
105  let outputhtml_ref = ref None in
106   (function rw -> outputhtml_ref := Some rw),
107   (function () ->
108     match !outputhtml_ref with
109        None -> raise OutputHtmlNotInitialized
110      | Some outputhtml -> outputhtml
111   )
112 ;;
113
114 exception QedSetSensitiveNotInitialized;;
115 let qed_set_sensitive =
116  ref (function _ -> raise QedSetSensitiveNotInitialized)
117 ;;
118
119 exception SaveSetSensitiveNotInitialized;;
120 let save_set_sensitive =
121  ref (function _ -> raise SaveSetSensitiveNotInitialized)
122 ;;
123
124 (* COMMAND LINE OPTIONS *)
125
126 let usedb = ref true
127
128 let argspec =
129   [
130     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
131   ]
132 in
133 Arg.parse argspec ignore ""
134
135 (* MISC FUNCTIONS *)
136
137 let term_of_cic_textual_parser_uri uri =
138  let module C = Cic in
139  let module CTP = CicTextualParser0 in
140   match uri with
141      CTP.ConUri uri -> C.Const (uri,[])
142    | CTP.VarUri uri -> C.Var (uri,[])
143    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
144    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
145 ;;
146
147 let string_of_cic_textual_parser_uri uri =
148  let module C = Cic in
149  let module CTP = CicTextualParser0 in
150   let uri' =
151    match uri with
152       CTP.ConUri uri -> UriManager.string_of_uri uri
153     | CTP.VarUri uri -> UriManager.string_of_uri uri
154     | CTP.IndTyUri (uri,tyno) ->
155        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
156     | CTP.IndConUri (uri,tyno,consno) ->
157        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
158         string_of_int consno
159   in
160    (* 4 = String.length "cic:" *)
161    String.sub uri' 4 (String.length uri' - 4)
162 ;;
163
164 let output_html outputhtml msg =
165  htmlheader_and_content := !htmlheader_and_content ^ msg ;
166  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
167  outputhtml#set_topline (-1)
168 ;;
169
170 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
171
172 (* Check window *)
173
174 let check_window outputhtml uris =
175  let window =
176   GWindow.window
177    ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
178  let notebook =
179   GPack.notebook ~scrollable:true ~packing:window#add () in
180  window#show () ;
181  let render_terms =
182   List.map
183    (function uri ->
184      let scrolled_window =
185       GBin.scrolled_window ~border_width:10
186        ~packing:
187          (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
188        ()
189      in
190       lazy 
191        (let mmlwidget =
192          TermViewer.sequent_viewer
193           ~packing:scrolled_window#add ~width:400 ~height:280 () in
194         let expr =
195          let term =
196           term_of_cic_textual_parser_uri
197            (Misc.cic_textual_parser_uri_of_string uri)
198          in
199           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
200         in
201          try
202           mmlwidget#load_sequent [] (111,[],expr)
203          with
204           e ->
205            output_html outputhtml
206             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
207        )
208    ) uris
209  in
210   ignore
211    (notebook#connect#switch_page
212      (function i -> Lazy.force (List.nth render_terms i)))
213 ;;
214
215 exception NoChoice;;
216
217 let
218  interactive_user_uri_choice ~(selection_mode:[`SINGLE|`EXTENDED]) ?(ok="Ok")
219   ?(enable_button_for_non_vars=false) ~title ~msg uris
220 =
221  let choices = ref [] in
222  let chosen = ref false in
223  let use_only_constants = ref false in
224  let window =
225   GWindow.dialog ~modal:true ~title ~width:600 () in
226  let lMessage =
227   GMisc.label ~text:msg
228    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
229  let scrolled_window =
230   GBin.scrolled_window ~border_width:10
231    ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
232  let clist =
233   let expected_height = 18 * List.length uris in
234    let height = if expected_height > 400 then 400 else expected_height in
235     GList.clist ~columns:1 ~packing:scrolled_window#add
236      ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
237  let _ = List.map (function x -> clist#append [x]) uris in
238  let hbox2 =
239   GPack.hbox ~border_width:0
240    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
241  let explain_label =
242   GMisc.label ~text:"None of the above. Try this one:"
243    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
244  let manual_input =
245   GEdit.entry ~editable:true
246    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
247  let hbox =
248   GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
249  let okb =
250   GButton.button ~label:ok
251    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
252  let _ = okb#misc#set_sensitive false in
253  let nonvarsb =
254   GButton.button
255    ~packing:
256     (function w ->
257       if enable_button_for_non_vars then
258        hbox#pack ~expand:false ~fill:false ~padding:5 w)
259    ~label:"Try constants only" () in
260  let checkb =
261   GButton.button ~label:"Check"
262    ~packing:(hbox#pack ~padding:5) () in
263  let _ = checkb#misc#set_sensitive false in
264  let cancelb =
265   GButton.button ~label:"Abort"
266    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
267  (* actions *)
268  let check_callback () =
269   assert (List.length !choices > 0) ;
270   check_window (outputhtml ()) !choices
271  in
272   ignore (window#connect#destroy GMain.Main.quit) ;
273   ignore (cancelb#connect#clicked window#destroy) ;
274   ignore
275    (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
276   ignore
277    (nonvarsb#connect#clicked
278      (function () ->
279        use_only_constants := true ;
280        chosen := true ;
281        window#destroy ()
282    )) ;
283   ignore (checkb#connect#clicked check_callback) ;
284   ignore
285    (clist#connect#select_row
286      (fun ~row ~column ~event ->
287        checkb#misc#set_sensitive true ;
288        okb#misc#set_sensitive true ;
289        choices := (List.nth uris row)::!choices)) ;
290   ignore
291    (clist#connect#unselect_row
292      (fun ~row ~column ~event ->
293        choices :=
294         List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
295   ignore
296    (manual_input#connect#changed
297      (fun _ ->
298        if manual_input#text = "" then
299         begin
300          choices := [] ;
301          checkb#misc#set_sensitive false ;
302          okb#misc#set_sensitive false ;
303          clist#misc#set_sensitive true
304         end
305        else
306         begin
307          choices := [manual_input#text] ;
308          clist#unselect_all () ;
309          checkb#misc#set_sensitive true ;
310          okb#misc#set_sensitive true ;
311          clist#misc#set_sensitive false
312         end));
313   window#set_position `CENTER ;
314   window#show () ;
315   GMain.Main.main () ;
316   if !chosen then
317    if !use_only_constants then
318     List.filter
319      (function uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
320      uris
321    else
322     if List.length !choices > 0 then !choices else raise NoChoice
323   else
324    raise NoChoice
325 ;;
326
327 let interactive_interpretation_choice interpretations =
328  let chosen = ref None in
329  let window =
330   GWindow.window
331    ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
332  let vbox = GPack.vbox ~packing:window#add () in
333  let lMessage =
334   GMisc.label
335    ~text:
336     ("Ambiguous input since there are many well-typed interpretations." ^
337      " Please, choose one of them.")
338    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
339  let notebook =
340   GPack.notebook ~scrollable:true
341    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
342  let _ =
343   List.map
344    (function interpretation ->
345      let clist =
346       let expected_height = 18 * List.length interpretation in
347        let height = if expected_height > 400 then 400 else expected_height in
348         GList.clist ~columns:2 ~packing:notebook#append_page ~height
349          ~titles:["id" ; "URI"] ()
350      in
351       ignore
352        (List.map
353          (function (id,uri) ->
354            let n = clist#append [id;uri] in
355             clist#set_row ~selectable:false n
356          ) interpretation
357        ) ;
358       clist#columns_autosize ()
359    ) interpretations in
360  let hbox =
361   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
362  let okb =
363   GButton.button ~label:"Ok"
364    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
365  let cancelb =
366   GButton.button ~label:"Abort"
367    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
368  (* actions *)
369  ignore (window#connect#destroy GMain.Main.quit) ;
370  ignore (cancelb#connect#clicked window#destroy) ;
371  ignore
372   (okb#connect#clicked
373     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
374  window#set_position `CENTER ;
375  window#show () ;
376  GMain.Main.main () ;
377  match !chosen with
378     None -> raise NoChoice
379   | Some n -> n
380 ;;
381
382
383 (* MISC FUNCTIONS *)
384
385 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
386 (* FG : THIS FUNCTION IS BECOMING A REAL NONSENSE                   *)
387 let get_last_query = 
388  let query = ref "" in
389   let out s = query := ! query ^ s in
390   MQueryGenerator.set_confirm_query
391    (function q -> 
392     query := ""; MQueryUtil.text_of_query out q ""; true);
393   function result ->
394    out (!query ^ " <h1>Result:</h1> "); MQueryUtil.text_of_result out result "<br>";
395    !query
396 ;;
397
398 let
399  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
400 =
401  let name =
402   let struri = UriManager.string_of_uri uri in
403   let idx = (String.rindex struri '/') + 1 in
404    String.sub struri idx (String.length struri - idx)
405  in
406   let path = pathname ^ "/" ^ name in
407   let xml, bodyxml =
408    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
409     annobj 
410   in
411   let xmlinnertypes =
412    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
413     ~ask_dtd_to_the_getter:false
414   in
415    (* innertypes *)
416    let innertypesuri = UriManager.innertypesuri_of_uri uri in
417     Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
418     Getter.register innertypesuri
419      (Configuration.annotations_url ^
420        Str.replace_first (Str.regexp "^cic:") ""
421         (UriManager.string_of_uri innertypesuri) ^ ".xml"
422      ) ;
423     (* constant type / variable / mutual inductive types definition *)
424     Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
425     Getter.register uri
426      (Configuration.annotations_url ^
427        Str.replace_first (Str.regexp "^cic:") ""
428         (UriManager.string_of_uri uri) ^ ".xml"
429      ) ;
430     match bodyxml with
431        None -> ()
432      | Some bodyxml' ->
433         (* constant body *)
434         let bodyuri =
435          match UriManager.bodyuri_of_uri uri with
436             None -> assert false
437           | Some bodyuri -> bodyuri
438         in
439          Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
440          Getter.register bodyuri
441           (Configuration.annotations_url ^
442             Str.replace_first (Str.regexp "^cic:") ""
443              (UriManager.string_of_uri bodyuri) ^ ".xml"
444           )
445 ;;
446
447
448 (* CALLBACKS *)
449
450 (*
451 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
452  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
453 *)
454
455 exception OpenConjecturesStillThere;;
456 exception WrongProof;;
457
458 let pathname_of_annuri uristring =
459  Configuration.annotations_dir ^    
460   Str.replace_first (Str.regexp "^cic:") "" uristring
461 ;;
462
463 let make_dirs dirpath =
464  ignore (Unix.system ("mkdir -p " ^ dirpath))
465 ;;
466
467 let save_obj uri obj =
468  let
469   (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
470    ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
471  =
472   Cic2acic.acic_object_of_cic_object obj
473  in
474   (* let's save the theorem and register it to the getter *) 
475   let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
476    make_dirs pathname ;
477    save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
478     pathname
479 ;;
480
481 let qed () =
482  match !ProofEngine.proof with
483     None -> assert false
484   | Some (uri,[],bo,ty) ->
485      if
486       CicReduction.are_convertible []
487        (CicTypeChecker.type_of_aux' [] [] bo) ty
488      then
489       begin
490        (*CSC: Wrong: [] is just plainly wrong *)
491        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
492        let (acic,ids_to_inner_types,ids_to_inner_sorts) =
493         (rendering_window ())#output#load_proof uri proof
494        in
495         !qed_set_sensitive false ;
496         (* let's save the theorem and register it to the getter *) 
497         let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
498          make_dirs pathname ;
499          save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
500           pathname
501       end
502      else
503       raise WrongProof
504   | _ -> raise OpenConjecturesStillThere
505 ;;
506
507 let save () =
508  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
509   match !ProofEngine.proof with
510      None -> assert false
511    | Some (uri, metasenv, bo, ty) ->
512       let currentproof =
513        (*CSC: Wrong: [] is just plainly wrong *)
514        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
515       in
516        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
517         Cic2acic.acic_object_of_cic_object currentproof
518        in
519         let xml, bodyxml =
520          match
521           Cic2Xml.print_object uri ~ids_to_inner_sorts
522            ~ask_dtd_to_the_getter:true acurrentproof
523          with
524             xml,Some bodyxml -> xml,bodyxml
525           | _,None -> assert false
526         in
527          Xml.pp ~quiet:true xml (Some prooffiletype) ;
528          output_html outputhtml
529           ("<h1 color=\"Green\">Current proof type saved to " ^
530            prooffiletype ^ "</h1>") ;
531          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
532          output_html outputhtml
533           ("<h1 color=\"Green\">Current proof body saved to " ^
534            prooffile ^ "</h1>")
535 ;;
536
537 (* Used to typecheck the loaded proofs *)
538 let typecheck_loaded_proof metasenv bo ty =
539  let module T = CicTypeChecker in
540   ignore (
541    List.fold_left
542     (fun metasenv ((_,context,ty) as conj) ->
543       ignore (T.type_of_aux' metasenv context ty) ;
544       metasenv @ [conj]
545     ) [] metasenv) ;
546   ignore (T.type_of_aux' metasenv [] ty) ;
547   ignore (T.type_of_aux' metasenv [] bo)
548 ;;
549
550 let decompose_uris_choice_callback uris = 
551 (* N.B.: in questo passaggio perdo l'informazione su exp_named_subst !!!! *)
552   let module U = UriManager in 
553    List.map 
554     (function uri ->
555       match Misc.cic_textual_parser_uri_of_string uri with
556          CicTextualParser0.IndTyUri (uri,typeno) -> (uri,typeno,[])
557        | _ -> assert false)
558     (interactive_user_uri_choice 
559       ~selection_mode:`EXTENDED ~ok:"Ok" ~enable_button_for_non_vars:false 
560       ~title:"Decompose" ~msg:"Please, select the Inductive Types to decompose" 
561       (List.map 
562         (function (uri,typeno,_) ->
563           U.string_of_uri uri ^ "#1/" ^ string_of_int (typeno+1)
564         ) uris)
565     ) 
566 ;;
567
568 let mk_fresh_name_callback context name ~typ =
569  let fresh_name =
570   match ProofEngineHelpers.mk_fresh_name context name ~typ with
571      Cic.Name fresh_name -> fresh_name
572    | Cic.Anonymous -> assert false
573  in
574   match
575    GToolbox.input_string ~title:"Enter a fresh hypothesis name" ~text:fresh_name
576     ("Enter a fresh name for the hypothesis " ^
577       CicPp.pp typ
578        (List.map (function None -> None | Some (n,_) -> Some n) context))
579   with
580      Some fresh_name' -> Cic.Name fresh_name'
581    | None -> raise NoChoice
582 ;;
583
584 let refresh_proof (output : TermViewer.proof_viewer) =
585  try
586   let uri,currentproof =
587    match !ProofEngine.proof with
588       None -> assert false
589     | Some (uri,metasenv,bo,ty) ->
590        !qed_set_sensitive (List.length metasenv = 0) ;
591        (*CSC: Wrong: [] is just plainly wrong *)
592        uri,
593         (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
594   in
595    ignore (output#load_proof uri currentproof)
596  with
597   e ->
598  match !ProofEngine.proof with
599     None -> assert false
600   | Some (uri,metasenv,bo,ty) ->
601 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
602    raise (InvokeTactics.RefreshProofException e)
603
604 let refresh_goals ?(empty_notebook=true) notebook =
605  try
606   match !ProofEngine.goal with
607      None ->
608       if empty_notebook then
609        begin 
610         notebook#remove_all_pages ~skip_switch_page_event:false ;
611         notebook#set_empty_page
612        end
613       else
614        notebook#proofw#unload
615    | Some metano ->
616       let metasenv =
617        match !ProofEngine.proof with
618           None -> assert false
619         | Some (_,metasenv,_,_) -> metasenv
620       in
621       let currentsequent =
622        List.find (function (m,_,_) -> m=metano) metasenv
623       in
624         let regenerate_notebook () = 
625          let skip_switch_page_event =
626           match metasenv with
627              (m,_,_)::_ when m = metano -> false
628            | _ -> true
629          in
630           notebook#remove_all_pages ~skip_switch_page_event ;
631           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
632         in
633           if empty_notebook then
634            begin
635             regenerate_notebook () ;
636             notebook#set_current_page
637              ~may_skip_switch_page_event:false metano
638            end
639           else
640            begin
641             notebook#set_current_page
642              ~may_skip_switch_page_event:true metano ;
643             notebook#proofw#load_sequent metasenv currentsequent
644            end
645  with
646   e ->
647 let metano =
648   match !ProofEngine.goal with
649      None -> assert false
650    | Some m -> m
651 in
652 let metasenv =
653  match !ProofEngine.proof with
654     None -> assert false
655   | Some (_,metasenv,_,_) -> metasenv
656 in
657 try
658 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
659    prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
660       raise (InvokeTactics.RefreshSequentException e)
661 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unknown."); raise (InvokeTactics.RefreshSequentException e)
662
663
664 module InvokeTacticsCallbacks =
665  struct
666   let sequent_viewer () = (rendering_window ())#notebook#proofw
667   let term_editor () = (rendering_window ())#inputt
668   let scratch_window () = (rendering_window ())#scratch_window
669
670   let refresh_proof () =
671    let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
672     refresh_proof output
673
674   let refresh_goals () =
675    let notebook = (rendering_window ())#notebook in
676     refresh_goals notebook
677
678   let decompose_uris_choice_callback = decompose_uris_choice_callback
679   let mk_fresh_name_callback = mk_fresh_name_callback
680   let output_html msg = output_html (outputhtml ()) msg
681  end
682 ;;
683
684 module InvokeTactics' = InvokeTactics.Make(InvokeTacticsCallbacks);;
685
686
687 let load () =
688  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
689  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
690  let notebook = (rendering_window ())#notebook in
691   try
692    match 
693     GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
694      "Choose an URI:"
695    with
696       None -> raise NoChoice
697     | Some uri0 ->
698        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
699         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
700            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
701             typecheck_loaded_proof metasenv bo ty ;
702             ProofEngine.proof :=
703              Some (uri, metasenv, bo, ty) ;
704             ProofEngine.goal :=
705              (match metasenv with
706                  [] -> None
707                | (metano,_,_)::_ -> Some metano
708              ) ;
709             refresh_proof output ;
710             refresh_goals notebook ;
711              output_html outputhtml
712               ("<h1 color=\"Green\">Current proof type loaded from " ^
713                 prooffiletype ^ "</h1>") ;
714              output_html outputhtml
715               ("<h1 color=\"Green\">Current proof body loaded from " ^
716                 prooffile ^ "</h1>") ;
717             !save_set_sensitive true
718          | _ -> assert false
719   with
720      InvokeTactics.RefreshSequentException e ->
721       output_html outputhtml
722        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
723         "sequent: " ^ Printexc.to_string e ^ "</h1>")
724    | InvokeTactics.RefreshProofException e ->
725       output_html outputhtml
726        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
727         "proof: " ^ Printexc.to_string e ^ "</h1>")
728    | e ->
729       output_html outputhtml
730        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
731 ;;
732
733 let edit_aliases () =
734  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
735  let id_to_uris = inputt#id_to_uris in
736  let chosen = ref false in
737  let window =
738   GWindow.window
739    ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
740  let vbox =
741   GPack.vbox ~border_width:0 ~packing:window#add () in
742  let scrolled_window =
743   GBin.scrolled_window ~border_width:10
744    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
745  let input = GEdit.text ~editable:true ~width:400 ~height:100
746    ~packing:scrolled_window#add () in
747  let hbox =
748   GPack.hbox ~border_width:0
749    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
750  let okb =
751   GButton.button ~label:"Ok"
752    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
753  let cancelb =
754   GButton.button ~label:"Cancel"
755    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
756  ignore (window#connect#destroy GMain.Main.quit) ;
757  ignore (cancelb#connect#clicked window#destroy) ;
758  ignore
759   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
760  let dom,resolve_id = !id_to_uris in
761   ignore
762    (input#insert_text ~pos:0
763     (String.concat "\n"
764       (List.map
765         (function v ->
766           let uri =
767            match resolve_id v with
768               None -> assert false
769             | Some uri -> uri
770           in
771            "alias " ^ v ^ " " ^
772              (string_of_cic_textual_parser_uri uri)
773         ) dom))) ;
774   window#show () ;
775   GMain.Main.main () ;
776   if !chosen then
777    let dom,resolve_id =
778     let inputtext = input#get_chars 0 input#length in
779     let regexpr =
780      let alfa = "[a-zA-Z_-]" in
781      let digit = "[0-9]" in
782      let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
783      let blanks = "\( \|\t\|\n\)+" in
784      let nonblanks = "[^ \t\n]+" in
785      let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
786       Str.regexp
787        ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
788     in
789      let rec aux n =
790       try
791        let n' = Str.search_forward regexpr inputtext n in
792         let id = Str.matched_group 2 inputtext in
793         let uri =
794          Misc.cic_textual_parser_uri_of_string
795           ("cic:" ^ (Str.matched_group 5 inputtext))
796         in
797          let dom,resolve_id = aux (n' + 1) in
798           if List.mem id dom then
799            dom,resolve_id
800           else
801            id::dom,
802             (function id' -> if id = id' then Some uri else resolve_id id')
803       with
804        Not_found -> TermEditor.empty_id_to_uris
805      in
806       aux 0
807    in
808     id_to_uris := (dom,resolve_id)
809 ;;
810
811 let proveit () =
812  let module L = LogicalOperations in
813  let module G = Gdome in
814  let notebook = (rendering_window ())#notebook in
815  let output = (rendering_window ())#output in
816  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
817   try
818    output#make_sequent_of_selected_term ;
819    refresh_proof output ;
820    refresh_goals notebook
821   with
822      InvokeTactics.RefreshSequentException e ->
823       output_html outputhtml
824        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
825         "sequent: " ^ Printexc.to_string e ^ "</h1>")
826    | InvokeTactics.RefreshProofException e ->
827       output_html outputhtml
828        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
829         "proof: " ^ Printexc.to_string e ^ "</h1>")
830    | e ->
831       output_html outputhtml
832        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
833 ;;
834
835 let focus () =
836  let module L = LogicalOperations in
837  let module G = Gdome in
838  let notebook = (rendering_window ())#notebook in
839  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
840  let output = (rendering_window ())#output in
841   try
842    output#focus_sequent_of_selected_term ;
843    refresh_goals notebook
844   with
845      InvokeTactics.RefreshSequentException e ->
846       output_html outputhtml
847        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
848         "sequent: " ^ Printexc.to_string e ^ "</h1>")
849    | InvokeTactics.RefreshProofException e ->
850       output_html outputhtml
851        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
852         "proof: " ^ Printexc.to_string e ^ "</h1>")
853    | e ->
854       output_html outputhtml
855        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
856 ;;
857
858 exception NoPrevGoal;;
859 exception NoNextGoal;;
860
861 let setgoal metano =
862  let module L = LogicalOperations in
863  let module G = Gdome in
864  let notebook = (rendering_window ())#notebook in
865  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
866   let metasenv =
867    match !ProofEngine.proof with
868       None -> assert false
869     | Some (_,metasenv,_,_) -> metasenv
870   in
871    try
872     refresh_goals ~empty_notebook:false notebook
873    with
874       InvokeTactics.RefreshSequentException e ->
875        output_html outputhtml
876         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
877          "sequent: " ^ Printexc.to_string e ^ "</h1>")
878     | e ->
879        output_html outputhtml
880         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
881 ;;
882
883 let
884  show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
885 =
886  let window =
887   GWindow.window ~width:800 ~border_width:2 () in
888  let scrolled_window =
889   GBin.scrolled_window ~border_width:10 ~packing:window#add () in
890  let mmlwidget =
891   GMathViewAux.single_selection_math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
892  let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
893  let href = Gdome.domString "href" in
894   let show_in_show_window_obj uri obj =
895    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
896     try
897      let
898       (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
899        ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
900      =
901       Cic2acic.acic_object_of_cic_object obj
902      in
903       let mml =
904        ApplyStylesheets.mml_of_cic_object
905         ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
906       in
907        window#set_title (UriManager.string_of_uri uri) ;
908        window#misc#hide () ; window#show () ;
909        mmlwidget#load_doc mml ;
910     with
911      e ->
912       output_html outputhtml
913        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
914   in
915   let show_in_show_window_uri uri =
916    let obj = CicEnvironment.get_obj uri in
917     show_in_show_window_obj uri obj
918   in
919    let show_in_show_window_callback mmlwidget (n : Gdome.element) _ =
920     if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
921      let uri =
922       (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
923      in 
924       show_in_show_window_uri (UriManager.uri_of_string uri)
925     else
926      ignore (mmlwidget#action_toggle n)
927    in
928     let _ =
929      mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
930     in
931      show_in_show_window_obj, show_in_show_window_uri,
932       show_in_show_window_callback
933 ;;
934
935 exception NoObjectsLocated;;
936
937 let user_uri_choice ~title ~msg uris =
938  let uri =
939   match uris with
940      [] -> raise NoObjectsLocated
941    | [uri] -> uri
942    | uris ->
943       match
944        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
945       with
946          [uri] -> uri
947        | _ -> assert false
948  in
949   String.sub uri 4 (String.length uri - 4)
950 ;;
951
952 let locate_callback id =
953  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
954  let result = MQueryGenerator.locate id in
955  let uris =
956   List.map
957    (function uri,_ ->
958      Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri)
959    result in
960  let html =
961   (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
962  in
963   output_html outputhtml html ;
964   user_uri_choice ~title:"Ambiguous input."
965    ~msg:
966      ("Ambiguous input \"" ^ id ^
967       "\". Please, choose one interpetation:")
968    uris
969 ;;
970
971
972 let input_or_locate_uri ~title =
973  let uri = ref None in
974  let window =
975   GWindow.window
976    ~width:400 ~modal:true ~title ~border_width:2 () in
977  let vbox = GPack.vbox ~packing:window#add () in
978  let hbox1 =
979   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
980  let _ =
981   GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
982  let manual_input =
983   GEdit.entry ~editable:true
984    ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
985  let checkb =
986   GButton.button ~label:"Check"
987    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
988  let _ = checkb#misc#set_sensitive false in
989  let hbox2 =
990   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
991  let _ =
992   GMisc.label ~text:"You can also enter an indentifier to locate:"
993    ~packing:(hbox2#pack ~padding:5) () in
994  let locate_input =
995   GEdit.entry ~editable:true
996    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
997  let locateb =
998   GButton.button ~label:"Locate"
999    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1000  let _ = locateb#misc#set_sensitive false in
1001  let hbox3 =
1002   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1003  let okb =
1004   GButton.button ~label:"Ok"
1005    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1006  let _ = okb#misc#set_sensitive false in
1007  let cancelb =
1008   GButton.button ~label:"Cancel"
1009    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1010  in
1011   ignore (window#connect#destroy GMain.Main.quit) ;
1012   ignore
1013    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1014   let check_callback () =
1015    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1016    let uri = "cic:" ^ manual_input#text in
1017     try
1018       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1019       output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1020       true
1021     with
1022        Getter.Unresolved ->
1023         output_html outputhtml
1024          ("<h1 color=\"Red\">URI " ^ uri ^
1025           " does not correspond to any object.</h1>") ;
1026         false
1027      | UriManager.IllFormedUri _ ->
1028         output_html outputhtml
1029          ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1030         false
1031      | e ->
1032         output_html outputhtml
1033          ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1034         false
1035   in
1036   ignore
1037    (okb#connect#clicked
1038      (function () ->
1039        if check_callback () then
1040         begin
1041          uri := Some manual_input#text ;
1042          window#destroy ()
1043         end
1044    )) ;
1045   ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1046   ignore
1047    (manual_input#connect#changed
1048      (fun _ ->
1049        if manual_input#text = "" then
1050         begin
1051          checkb#misc#set_sensitive false ;
1052          okb#misc#set_sensitive false
1053         end
1054        else
1055         begin
1056          checkb#misc#set_sensitive true ;
1057          okb#misc#set_sensitive true
1058         end));
1059   ignore
1060    (locate_input#connect#changed
1061      (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1062   ignore
1063    (locateb#connect#clicked
1064      (function () ->
1065        let id = locate_input#text in
1066         manual_input#set_text (locate_callback id) ;
1067         locate_input#delete_text 0 (String.length id)
1068    )) ;
1069   window#show () ;
1070   GMain.Main.main () ;
1071   match !uri with
1072      None -> raise NoChoice
1073    | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1074 ;;
1075
1076 exception AmbiguousInput;;
1077
1078 (* A WIDGET TO ENTER CIC TERMS *)
1079
1080 module Callbacks =
1081  struct
1082   let output_html msg = output_html (outputhtml ()) msg;;
1083   let interactive_user_uri_choice =
1084    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
1085     interactive_user_uri_choice ~selection_mode ?ok
1086      ?enable_button_for_non_vars ~title ~msg;;
1087   let interactive_interpretation_choice = interactive_interpretation_choice;;
1088   let input_or_locate_uri = input_or_locate_uri;;
1089  end
1090 ;;
1091
1092 module TermEditor' = TermEditor.Make(Callbacks);;
1093
1094 (* OTHER FUNCTIONS *)
1095
1096 let locate () =
1097  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1098  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1099    try
1100     match
1101      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1102     with
1103        None -> raise NoChoice
1104      | Some input ->
1105         let uri = locate_callback input in
1106          inputt#set_term uri
1107    with
1108     e ->
1109      output_html outputhtml
1110       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1111 ;;
1112
1113
1114 exception UriAlreadyInUse;;
1115 exception NotAUriToAConstant;;
1116
1117 let new_inductive () =
1118  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1119  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1120  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
1121  let notebook = (rendering_window ())#notebook in
1122
1123  let chosen = ref false in
1124  let inductive = ref true in
1125  let paramsno = ref 0 in
1126  let get_uri = ref (function _ -> assert false) in
1127  let get_base_uri = ref (function _ -> assert false) in
1128  let get_names = ref (function _ -> assert false) in
1129  let get_types_and_cons = ref (function _ -> assert false) in
1130  let get_context_and_subst = ref (function _ -> assert false) in 
1131  let window =
1132   GWindow.window
1133    ~width:600 ~modal:true ~position:`CENTER
1134    ~title:"New Block of Mutual (Co)Inductive Definitions"
1135    ~border_width:2 () in
1136  let vbox = GPack.vbox ~packing:window#add () in
1137  let hbox =
1138   GPack.hbox ~border_width:0
1139    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1140  let _ =
1141   GMisc.label ~text:"Enter the URI for the new block:"
1142    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1143  let uri_entry =
1144   GEdit.entry ~editable:true
1145    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1146  let hbox0 =
1147   GPack.hbox ~border_width:0
1148    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1149  let _ =
1150   GMisc.label
1151    ~text:
1152      "Enter the number of left parameters in every arity and constructor type:"
1153    ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1154  let paramsno_entry =
1155   GEdit.entry ~editable:true ~text:"0"
1156    ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1157  let hbox1 =
1158   GPack.hbox ~border_width:0
1159    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1160  let _ =
1161   GMisc.label ~text:"Are the definitions inductive or coinductive?"
1162    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1163  let inductiveb =
1164   GButton.radio_button ~label:"Inductive"
1165    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1166  let coinductiveb =
1167   GButton.radio_button ~label:"Coinductive"
1168    ~group:inductiveb#group
1169    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1170  let hbox2 =
1171   GPack.hbox ~border_width:0
1172    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1173  let _ =
1174   GMisc.label ~text:"Enter the list of the names of the types:"
1175    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1176  let names_entry =
1177   GEdit.entry ~editable:true
1178    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1179  let hboxn =
1180   GPack.hbox ~border_width:0
1181    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1182  let okb =
1183   GButton.button ~label:"> Next"
1184    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1185  let _ = okb#misc#set_sensitive true in
1186  let cancelb =
1187   GButton.button ~label:"Abort"
1188    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1189  ignore (window#connect#destroy GMain.Main.quit) ;
1190  ignore (cancelb#connect#clicked window#destroy) ;
1191  (* First phase *)
1192  let rec phase1 () =
1193   ignore
1194    (okb#connect#clicked
1195      (function () ->
1196        try
1197         let uristr = "cic:" ^ uri_entry#text in
1198         let namesstr = names_entry#text in
1199         let paramsno' = int_of_string (paramsno_entry#text) in
1200          match Str.split (Str.regexp " +") namesstr with
1201             [] -> assert false
1202           | (he::tl) as names ->
1203              let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1204               begin
1205                try
1206                 ignore (Getter.resolve uri) ;
1207                 raise UriAlreadyInUse
1208                with
1209                 Getter.Unresolved ->
1210                  get_uri := (function () -> uri) ; 
1211                  get_names := (function () -> names) ;
1212                  inductive := inductiveb#active ;
1213                  paramsno := paramsno' ;
1214                  phase2 ()
1215               end
1216        with
1217         e ->
1218          output_html outputhtml
1219           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1220      ))
1221  (* Second phase *)
1222  and phase2 () =
1223   let type_widgets =
1224    List.map
1225     (function name ->
1226       let frame =
1227        GBin.frame ~label:name
1228         ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1229       let vbox = GPack.vbox ~packing:frame#add () in
1230       let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1231       let _ =
1232        GMisc.label ~text:("Enter its type:")
1233         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1234       let scrolled_window =
1235        GBin.scrolled_window ~border_width:5
1236         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1237       let newinputt =
1238        TermEditor'.term_editor
1239         ~width:400 ~height:20 ~packing:scrolled_window#add 
1240         ~share_id_to_uris_with:inputt ()
1241         ~isnotempty_callback:
1242          (function b ->
1243            (*non_empty_type := b ;*)
1244            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1245       in
1246       let hbox =
1247        GPack.hbox ~border_width:0
1248         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1249       let _ =
1250        GMisc.label ~text:("Enter the list of its constructors:")
1251         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1252       let cons_names_entry =
1253        GEdit.entry ~editable:true
1254         ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1255       (newinputt,cons_names_entry)
1256     ) (!get_names ())
1257   in
1258    vbox#remove hboxn#coerce ;
1259    let hboxn =
1260     GPack.hbox ~border_width:0
1261      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1262    let okb =
1263     GButton.button ~label:"> Next"
1264      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1265    let cancelb =
1266     GButton.button ~label:"Abort"
1267      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1268    ignore (cancelb#connect#clicked window#destroy) ;
1269    ignore
1270     (okb#connect#clicked
1271       (function () ->
1272         try
1273          let names = !get_names () in
1274          let types_and_cons =
1275           List.map2
1276            (fun name (newinputt,cons_names_entry) ->
1277              let consnamesstr = cons_names_entry#text in
1278              let cons_names = Str.split (Str.regexp " +") consnamesstr in
1279              let metasenv,expr =
1280               newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1281              in
1282               match metasenv with
1283                  [] -> expr,cons_names
1284                | _ -> raise AmbiguousInput
1285            ) names type_widgets
1286          in
1287           let uri = !get_uri () in
1288           let _ =
1289            (* Let's see if so far the definition is well-typed *)
1290            let params = [] in
1291            let paramsno = 0 in
1292            (* To test if the arities of the inductive types are well *)
1293            (* typed, we check the inductive block definition where   *)
1294            (* no constructor is given to each type.                  *)
1295            let tys =
1296             List.map2
1297              (fun name (ty,cons) -> (name, !inductive, ty, []))
1298              names types_and_cons
1299            in
1300             CicTypeChecker.typecheck_mutual_inductive_defs uri
1301              (tys,params,paramsno)
1302           in
1303            get_context_and_subst :=
1304             (function () ->
1305               let i = ref 0 in
1306                List.fold_left2
1307                 (fun (context,subst) name (ty,_) ->
1308                   let res =
1309                    (Some (Cic.Name name, Cic.Decl ty))::context,
1310                     (Cic.MutInd (uri,!i,[]))::subst
1311                   in
1312                    incr i ; res
1313                 ) ([],[]) names types_and_cons) ;
1314            let types_and_cons' =
1315             List.map2
1316              (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1317              names types_and_cons
1318            in
1319             get_types_and_cons := (function () -> types_and_cons') ;
1320             chosen := true ;
1321             window#destroy ()
1322         with
1323          e ->
1324           output_html outputhtml
1325            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1326       ))
1327  (* Third phase *)
1328  and phase3 name cons =
1329   let get_cons_types = ref (function () -> assert false) in
1330   let window2 =
1331    GWindow.window
1332     ~width:600 ~modal:true ~position:`CENTER
1333     ~title:(name ^ " Constructors")
1334     ~border_width:2 () in
1335   let vbox = GPack.vbox ~packing:window2#add () in
1336   let cons_type_widgets =
1337    List.map
1338     (function consname ->
1339       let hbox =
1340        GPack.hbox ~border_width:0
1341         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1342       let _ =
1343        GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1344         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1345       let scrolled_window =
1346        GBin.scrolled_window ~border_width:5
1347         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1348       let newinputt =
1349        TermEditor'.term_editor
1350         ~width:400 ~height:20 ~packing:scrolled_window#add
1351         ~share_id_to_uris_with:inputt ()
1352         ~isnotempty_callback:
1353          (function b ->
1354            (* (*non_empty_type := b ;*)
1355            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1356       in
1357        newinputt
1358     ) cons in
1359   let hboxn =
1360    GPack.hbox ~border_width:0
1361     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1362   let okb =
1363    GButton.button ~label:"> Next"
1364     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1365   let _ = okb#misc#set_sensitive true in
1366   let cancelb =
1367    GButton.button ~label:"Abort"
1368     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1369   ignore (window2#connect#destroy GMain.Main.quit) ;
1370   ignore (cancelb#connect#clicked window2#destroy) ;
1371   ignore
1372    (okb#connect#clicked
1373      (function () ->
1374        try
1375         chosen := true ;
1376         let context,subst= !get_context_and_subst () in
1377         let cons_types =
1378          List.map2
1379           (fun name inputt ->
1380             let metasenv,expr =
1381              inputt#get_metasenv_and_term ~context ~metasenv:[]
1382             in
1383              match metasenv with
1384                 [] ->
1385                  let undebrujined_expr =
1386                   List.fold_left
1387                    (fun expr t -> CicSubstitution.subst t expr) expr subst
1388                  in
1389                   name, undebrujined_expr
1390               | _ -> raise AmbiguousInput
1391           ) cons cons_type_widgets
1392         in
1393          get_cons_types := (function () -> cons_types) ;
1394          window2#destroy ()
1395        with
1396         e ->
1397          output_html outputhtml
1398           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1399      )) ;
1400   window2#show () ;
1401   GMain.Main.main () ;
1402   let okb_pressed = !chosen in
1403    chosen := false ;
1404    if (not okb_pressed) then
1405     begin
1406      window#destroy () ;
1407      assert false (* The control never reaches this point *)
1408     end
1409    else
1410     (!get_cons_types ())
1411  in
1412   phase1 () ;
1413   (* No more phases left or Abort pressed *) 
1414   window#show () ;
1415   GMain.Main.main () ;
1416   window#destroy () ;
1417   if !chosen then
1418    try
1419     let uri = !get_uri () in
1420 (*CSC: Da finire *)
1421     let params = [] in
1422     let tys = !get_types_and_cons () in
1423      let obj = Cic.InductiveDefinition tys params !paramsno in
1424       begin
1425        try
1426         prerr_endline (CicPp.ppobj obj) ;
1427         CicTypeChecker.typecheck_mutual_inductive_defs uri
1428          (tys,params,!paramsno) ;
1429         with
1430          e ->
1431           prerr_endline "Offending mutual (co)inductive type declaration:" ;
1432           prerr_endline (CicPp.ppobj obj) ;
1433       end ;
1434       (* We already know that obj is well-typed. We need to add it to the  *)
1435       (* environment in order to compute the inner-types without having to *)
1436       (* debrujin it or having to modify lots of other functions to avoid  *)
1437       (* asking the environment for the MUTINDs we are defining now.       *)
1438       CicEnvironment.put_inductive_definition uri obj ;
1439       save_obj uri obj ;
1440       show_in_show_window_obj uri obj
1441    with
1442     e ->
1443      output_html outputhtml
1444       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1445 ;;
1446
1447 let new_proof () =
1448  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1449  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1450  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
1451  let notebook = (rendering_window ())#notebook in
1452
1453  let chosen = ref false in
1454  let get_metasenv_and_term = ref (function _ -> assert false) in
1455  let get_uri = ref (function _ -> assert false) in
1456  let non_empty_type = ref false in
1457  let window =
1458   GWindow.window
1459    ~width:600 ~modal:true ~title:"New Proof or Definition"
1460    ~border_width:2 () in
1461  let vbox = GPack.vbox ~packing:window#add () in
1462  let hbox =
1463   GPack.hbox ~border_width:0
1464    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1465  let _ =
1466   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1467    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1468  let uri_entry =
1469   GEdit.entry ~editable:true
1470    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1471  let hbox1 =
1472   GPack.hbox ~border_width:0
1473    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1474  let _ =
1475   GMisc.label ~text:"Enter the theorem or definition type:"
1476    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1477  let scrolled_window =
1478   GBin.scrolled_window ~border_width:5
1479    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1480  (* the content of the scrolled_window is moved below (see comment) *)
1481  let hbox =
1482   GPack.hbox ~border_width:0
1483    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1484  let okb =
1485   GButton.button ~label:"Ok"
1486    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1487  let _ = okb#misc#set_sensitive false in
1488  let cancelb =
1489   GButton.button ~label:"Cancel"
1490    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1491  (* moved here to have visibility of the ok button *)
1492  let newinputt =
1493   TermEditor'.term_editor ~width:400 ~height:100 ~packing:scrolled_window#add
1494    ~share_id_to_uris_with:inputt ()
1495    ~isnotempty_callback:
1496     (function b ->
1497       non_empty_type := b ;
1498       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1499  in
1500  let _ =
1501   newinputt#set_term inputt#get_as_string ;
1502   inputt#reset in
1503  let _ =
1504   uri_entry#connect#changed
1505    (function () ->
1506      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1507  in
1508  ignore (window#connect#destroy GMain.Main.quit) ;
1509  ignore (cancelb#connect#clicked window#destroy) ;
1510  ignore
1511   (okb#connect#clicked
1512     (function () ->
1513       chosen := true ;
1514       try
1515        let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1516        let uristr = "cic:" ^ uri_entry#text in
1517        let uri = UriManager.uri_of_string uristr in
1518         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1519          raise NotAUriToAConstant
1520         else
1521          begin
1522           try
1523            ignore (Getter.resolve uri) ;
1524            raise UriAlreadyInUse
1525           with
1526            Getter.Unresolved ->
1527             get_metasenv_and_term := (function () -> metasenv,parsed) ;
1528             get_uri := (function () -> uri) ; 
1529             window#destroy ()
1530          end
1531       with
1532        e ->
1533         output_html outputhtml
1534          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1535   )) ;
1536  window#show () ;
1537  GMain.Main.main () ;
1538  if !chosen then
1539   try
1540    let metasenv,expr = !get_metasenv_and_term () in
1541     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1542      ProofEngine.proof :=
1543       Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1544      ProofEngine.goal := Some 1 ;
1545      refresh_goals notebook ;
1546      refresh_proof output ;
1547      !save_set_sensitive true ;
1548      inputt#reset ;
1549      ProofEngine.intros ~mk_fresh_name_callback () ;
1550      refresh_goals notebook ;
1551      refresh_proof output
1552   with
1553      InvokeTactics.RefreshSequentException e ->
1554       output_html outputhtml
1555        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1556         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1557    | InvokeTactics.RefreshProofException e ->
1558       output_html outputhtml
1559        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1560         "proof: " ^ Printexc.to_string e ^ "</h1>")
1561    | e ->
1562       output_html outputhtml
1563        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1564 ;;
1565
1566 let check_term_in_scratch scratch_window metasenv context expr = 
1567  try
1568   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1569   let expr = Cic.Cast (expr,ty) in
1570    scratch_window#show () ;
1571    scratch_window#set_term expr ;
1572    scratch_window#set_context context ;
1573    scratch_window#set_metasenv metasenv ;
1574    scratch_window#sequent_viewer#load_sequent metasenv (111,context,expr)
1575  with
1576   e ->
1577    print_endline ("? " ^ CicPp.ppterm expr) ;
1578    raise e
1579 ;;
1580
1581 let check scratch_window () =
1582  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1583  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1584   let metasenv =
1585    match !ProofEngine.proof with
1586       None -> []
1587     | Some (_,metasenv,_,_) -> metasenv
1588   in
1589   let context =
1590    match !ProofEngine.goal with
1591       None -> []
1592     | Some metano ->
1593        let (_,canonical_context,_) =
1594         List.find (function (m,_,_) -> m=metano) metasenv
1595        in
1596         canonical_context
1597   in
1598    try
1599     let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
1600      check_term_in_scratch scratch_window metasenv' context expr
1601    with
1602     e ->
1603      output_html outputhtml
1604       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1605 ;;
1606
1607 let show () =
1608  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1609   try
1610    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
1611   with
1612    e ->
1613     output_html outputhtml
1614      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1615 ;;
1616
1617 exception NotADefinition;;
1618
1619 let open_ () =
1620  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1621  let output = ((rendering_window ())#output : TermViewer.proof_viewer) in
1622  let notebook = (rendering_window ())#notebook in
1623    try
1624     let uri = input_or_locate_uri ~title:"Open" in
1625      CicTypeChecker.typecheck uri ;
1626      let metasenv,bo,ty =
1627       match CicEnvironment.get_cooked_obj uri with
1628          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1629        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1630        | Cic.Constant _
1631        | Cic.Variable _
1632        | Cic.InductiveDefinition _ -> raise NotADefinition
1633      in
1634       ProofEngine.proof :=
1635        Some (uri, metasenv, bo, ty) ;
1636       ProofEngine.goal := None ;
1637       refresh_goals notebook ;
1638       refresh_proof output
1639    with
1640       InvokeTactics.RefreshSequentException e ->
1641        output_html outputhtml
1642         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1643          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1644     | InvokeTactics.RefreshProofException e ->
1645        output_html outputhtml
1646         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1647          "proof: " ^ Printexc.to_string e ^ "</h1>")
1648     | e ->
1649        output_html outputhtml
1650         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1651 ;;
1652
1653 let show_query_results results =
1654  let window =
1655   GWindow.window
1656    ~modal:false ~title:"Query results." ~border_width:2 () in
1657  let vbox = GPack.vbox ~packing:window#add () in
1658  let hbox =
1659   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1660  let lMessage =
1661   GMisc.label
1662    ~text:"Click on a URI to show that object"
1663    ~packing:hbox#add () in
1664  let scrolled_window =
1665   GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
1666    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1667  let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
1668   ignore
1669    (List.map
1670      (function (uri,_) ->
1671        let n =
1672         clist#append [uri]
1673        in
1674         clist#set_row ~selectable:false n
1675      ) results
1676    ) ;
1677   clist#columns_autosize () ;
1678   ignore
1679    (clist#connect#select_row
1680      (fun ~row ~column ~event ->
1681        let (uristr,_) = List.nth results row in
1682         match
1683          Misc.cic_textual_parser_uri_of_string
1684           (Misc.wrong_xpointer_format_from_wrong_xpointer_format'
1685             uristr)
1686         with
1687            CicTextualParser0.ConUri uri
1688          | CicTextualParser0.VarUri uri
1689          | CicTextualParser0.IndTyUri (uri,_)
1690          | CicTextualParser0.IndConUri (uri,_,_) ->
1691             show_in_show_window_uri uri
1692      )
1693    ) ;
1694   window#show ()
1695 ;;
1696
1697 let refine_constraints (must_obj,must_rel,must_sort) =
1698  let chosen = ref false in
1699  let use_only = ref false in
1700  let window =
1701   GWindow.window
1702    ~modal:true ~title:"Constraints refinement."
1703    ~width:800 ~border_width:2 () in
1704  let vbox = GPack.vbox ~packing:window#add () in
1705  let hbox =
1706   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1707  let lMessage =
1708   GMisc.label
1709    ~text: "\"Only\" constraints can be enforced or not."
1710    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1711  let onlyb =
1712   GButton.toggle_button ~label:"Enforce \"only\" constraints"
1713    ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
1714  in
1715   ignore
1716    (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
1717  (* Notebook for the constraints choice *)
1718  let notebook =
1719   GPack.notebook ~scrollable:true
1720    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1721  (* Rel constraints *)
1722  let label =
1723   GMisc.label
1724    ~text: "Constraints on Rels" () in
1725  let vbox' =
1726   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
1727    () in
1728  let hbox =
1729   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
1730  let lMessage =
1731   GMisc.label
1732    ~text: "You can now specify the constraints on Rels."
1733    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1734  let expected_height = 25 * (List.length must_rel + 2) in
1735  let height = if expected_height > 400 then 400 else expected_height in
1736  let scrolled_window =
1737   GBin.scrolled_window ~border_width:10 ~height ~width:600
1738    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
1739  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
1740  let rel_constraints =
1741   List.map
1742    (function (position,depth) ->
1743      let hbox =
1744       GPack.hbox
1745        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
1746      let lMessage =
1747       GMisc.label
1748        ~text:position
1749        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1750      match depth with
1751         None -> position, ref None
1752       | Some depth' ->
1753          let mutable_ref = ref (Some depth') in
1754          let depthb =
1755           GButton.toggle_button
1756            ~label:("depth = " ^ string_of_int depth') ~active:true
1757            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
1758          in
1759           ignore
1760            (depthb#connect#toggled
1761              (function () ->
1762                let sel_depth = if depthb#active then Some depth' else None in
1763                 mutable_ref := sel_depth
1764             )) ;
1765           position, mutable_ref
1766    ) must_rel in
1767  (* Sort constraints *)
1768  let label =
1769   GMisc.label
1770    ~text: "Constraints on Sorts" () in
1771  let vbox' =
1772   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
1773    () in
1774  let hbox =
1775   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
1776  let lMessage =
1777   GMisc.label
1778    ~text: "You can now specify the constraints on Sorts."
1779    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1780  let expected_height = 25 * (List.length must_sort + 2) in
1781  let height = if expected_height > 400 then 400 else expected_height in
1782  let scrolled_window =
1783   GBin.scrolled_window ~border_width:10 ~height ~width:600
1784    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
1785  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
1786  let sort_constraints =
1787   List.map
1788    (function (position,depth,sort) ->
1789      let hbox =
1790       GPack.hbox
1791        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
1792      let lMessage =
1793       GMisc.label
1794        ~text:(sort ^ " " ^ position)
1795        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1796      match depth with
1797         None -> position, ref None, sort
1798       | Some depth' ->
1799          let mutable_ref = ref (Some depth') in
1800          let depthb =
1801           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
1802            ~active:true
1803            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
1804          in
1805           ignore
1806            (depthb#connect#toggled
1807              (function () ->
1808                let sel_depth = if depthb#active then Some depth' else None in
1809                 mutable_ref := sel_depth
1810             )) ;
1811           position, mutable_ref, sort
1812    ) must_sort in
1813  (* Obj constraints *)
1814  let label =
1815   GMisc.label
1816    ~text: "Constraints on constants" () in
1817  let vbox' =
1818   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
1819    () in
1820  let hbox =
1821   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
1822  let lMessage =
1823   GMisc.label
1824    ~text: "You can now specify the constraints on constants."
1825    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1826  let expected_height = 25 * (List.length must_obj + 2) in
1827  let height = if expected_height > 400 then 400 else expected_height in
1828  let scrolled_window =
1829   GBin.scrolled_window ~border_width:10 ~height ~width:600
1830    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
1831  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
1832  let obj_constraints =
1833   List.map
1834    (function (uri,position,depth) ->
1835      let hbox =
1836       GPack.hbox
1837        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
1838      let lMessage =
1839       GMisc.label
1840        ~text:(uri ^ " " ^ position)
1841        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1842      match depth with
1843         None -> uri, position, ref None
1844       | Some depth' ->
1845          let mutable_ref = ref (Some depth') in
1846          let depthb =
1847           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
1848            ~active:true
1849            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
1850          in
1851           ignore
1852            (depthb#connect#toggled
1853              (function () ->
1854                let sel_depth = if depthb#active then Some depth' else None in
1855                 mutable_ref := sel_depth
1856             )) ;
1857           uri, position, mutable_ref
1858    ) must_obj in
1859  (* Confirm/abort buttons *)
1860  let hbox =
1861   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1862  let okb =
1863   GButton.button ~label:"Ok"
1864    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1865  let cancelb =
1866   GButton.button ~label:"Abort"
1867    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
1868  in
1869   ignore (window#connect#destroy GMain.Main.quit) ;
1870   ignore (cancelb#connect#clicked window#destroy) ;
1871   ignore
1872    (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
1873   window#set_position `CENTER ;
1874   window#show () ;
1875   GMain.Main.main () ;
1876   if !chosen then
1877    let chosen_must_rel =
1878     List.map
1879      (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
1880    let chosen_must_sort =
1881     List.map
1882      (function (position,ref_depth,sort) -> position,!ref_depth,sort)
1883      sort_constraints
1884    in
1885    let chosen_must_obj =
1886     List.map
1887      (function (uri,position,ref_depth) -> uri,position,!ref_depth)
1888      obj_constraints
1889    in
1890     (chosen_must_obj,chosen_must_rel,chosen_must_sort),
1891      (if !use_only then
1892 (*CSC: ???????????????????????? I assume that must and only are the same... *)
1893        Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
1894       else
1895        None,None,None
1896      )
1897   else
1898    raise NoChoice
1899 ;;
1900
1901 let completeSearchPattern () =
1902  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
1903  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1904   try
1905    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
1906    let must = MQueryLevels2.get_constraints expr in
1907    let must',only = refine_constraints must in
1908    let results = MQueryGenerator.searchPattern must' only in 
1909     show_query_results results
1910   with
1911    e ->
1912     output_html outputhtml
1913      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1914 ;;
1915
1916 let insertQuery () =
1917  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1918   try
1919    let chosen = ref None in
1920    let window =
1921     GWindow.window
1922      ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
1923    let vbox = GPack.vbox ~packing:window#add () in
1924    let label =
1925     GMisc.label ~text:"Insert Query. For Experts Only."
1926      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1927    let scrolled_window =
1928     GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
1929      ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1930    let input = GEdit.text ~editable:true
1931     ~packing:scrolled_window#add () in
1932    let hbox =
1933     GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1934    let okb =
1935     GButton.button ~label:"Ok"
1936      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1937    let loadb =
1938     GButton.button ~label:"Load from file..."
1939      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1940    let cancelb =
1941     GButton.button ~label:"Abort"
1942      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1943    ignore (window#connect#destroy GMain.Main.quit) ;
1944    ignore (cancelb#connect#clicked window#destroy) ;
1945    ignore
1946     (okb#connect#clicked
1947       (function () ->
1948         chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
1949    ignore
1950     (loadb#connect#clicked
1951       (function () ->
1952         match
1953          GToolbox.select_file ~title:"Select Query File" ()
1954         with
1955            None -> ()
1956          | Some filename ->
1957             let inch = open_in filename in
1958              let rec read_file () =
1959               try
1960                let line = input_line inch in
1961                 line ^ "\n" ^ read_file ()
1962               with
1963                End_of_file -> ""
1964              in
1965               let text = read_file () in
1966                input#delete_text 0 input#length ;
1967                ignore (input#insert_text text ~pos:0))) ;
1968    window#set_position `CENTER ;
1969    window#show () ;
1970    GMain.Main.main () ;
1971    match !chosen with
1972       None -> ()
1973     | Some q ->
1974        let results =
1975         Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
1976        in
1977         show_query_results results
1978   with
1979    e ->
1980     output_html outputhtml
1981      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1982 ;;
1983
1984 let choose_must list_of_must only =
1985  let chosen = ref None in
1986  let user_constraints = ref [] in
1987  let window =
1988   GWindow.window
1989    ~modal:true ~title:"Query refinement." ~border_width:2 () in
1990  let vbox = GPack.vbox ~packing:window#add () in
1991  let hbox =
1992   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1993  let lMessage =
1994   GMisc.label
1995    ~text:
1996     ("You can now specify the genericity of the query. " ^
1997      "The more generic the slower.")
1998    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1999  let hbox =
2000   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2001  let lMessage =
2002   GMisc.label
2003    ~text:
2004     "Suggestion: start with faster queries before moving to more generic ones."
2005    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2006  let notebook =
2007   GPack.notebook ~scrollable:true
2008    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2009  let _ =
2010   let page = ref 0 in
2011   let last = List.length list_of_must in
2012   List.map
2013    (function must ->
2014      incr page ;
2015      let label =
2016       GMisc.label ~text:
2017        (if !page = 1 then "More generic" else
2018          if !page = last then "More precise" else "          ") () in
2019      let expected_height = 25 * (List.length must + 2) in
2020      let height = if expected_height > 400 then 400 else expected_height in
2021      let scrolled_window =
2022       GBin.scrolled_window ~border_width:10 ~height ~width:600
2023        ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2024      let clist =
2025         GList.clist ~columns:2 ~packing:scrolled_window#add
2026          ~titles:["URI" ; "Position"] ()
2027      in
2028       ignore
2029        (List.map
2030          (function (uri,position) ->
2031            let n =
2032             clist#append 
2033              [uri; if position then "MainConclusion" else "Conclusion"]
2034            in
2035             clist#set_row ~selectable:false n
2036          ) must
2037        ) ;
2038       clist#columns_autosize ()
2039    ) list_of_must in
2040  let _ =
2041   let label = GMisc.label ~text:"User provided" () in
2042   let vbox =
2043    GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2044   let hbox =
2045    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2046   let lMessage =
2047    GMisc.label
2048    ~text:"Select the constraints that must be satisfied and press OK."
2049    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2050   let expected_height = 25 * (List.length only + 2) in
2051   let height = if expected_height > 400 then 400 else expected_height in
2052   let scrolled_window =
2053    GBin.scrolled_window ~border_width:10 ~height ~width:600
2054     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2055   let clist =
2056    GList.clist ~columns:2 ~packing:scrolled_window#add
2057     ~selection_mode:`EXTENDED
2058     ~titles:["URI" ; "Position"] ()
2059   in
2060    ignore
2061     (List.map
2062       (function (uri,position) ->
2063         let n =
2064          clist#append 
2065           [uri; if position then "MainConclusion" else "Conclusion"]
2066         in
2067          clist#set_row ~selectable:true n
2068       ) only
2069     ) ;
2070    clist#columns_autosize () ;
2071    ignore
2072     (clist#connect#select_row
2073       (fun ~row ~column ~event ->
2074         user_constraints := (List.nth only row)::!user_constraints)) ;
2075    ignore
2076     (clist#connect#unselect_row
2077       (fun ~row ~column ~event ->
2078         user_constraints :=
2079          List.filter
2080           (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2081  in
2082  let hbox =
2083   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2084  let okb =
2085   GButton.button ~label:"Ok"
2086    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2087  let cancelb =
2088   GButton.button ~label:"Abort"
2089    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2090  (* actions *)
2091  ignore (window#connect#destroy GMain.Main.quit) ;
2092  ignore (cancelb#connect#clicked window#destroy) ;
2093  ignore
2094   (okb#connect#clicked
2095     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2096  window#set_position `CENTER ;
2097  window#show () ;
2098  GMain.Main.main () ;
2099  match !chosen with
2100     None -> raise NoChoice
2101   | Some n ->
2102      if n = List.length list_of_must then
2103       (* user provided constraints *)
2104       !user_constraints
2105      else
2106       List.nth list_of_must n
2107 ;;
2108
2109 let searchPattern () =
2110  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
2111  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2112   try
2113     let metasenv =
2114      match !ProofEngine.proof with
2115         None -> assert false
2116       | Some (_,metasenv,_,_) -> metasenv
2117     in
2118      match !ProofEngine.goal with
2119         None -> ()
2120       | Some metano ->
2121          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2122           let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2123           let must = choose_must list_of_must only in
2124           let torigth_restriction (u,b) =
2125            let p =
2126             if b then
2127              "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" 
2128             else
2129              "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2130            in
2131             (u,p,None)
2132           in
2133           let rigth_must = List.map torigth_restriction must in
2134           let rigth_only = Some (List.map torigth_restriction only) in
2135           let result =
2136            MQueryGenerator.searchPattern
2137             (rigth_must,[],[]) (rigth_only,None,None) in 
2138           let uris =
2139            List.map
2140             (function uri,_ ->
2141               Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
2142             ) result in
2143           let html =
2144            " <h1>Backward Query: </h1>" ^
2145            " <pre>" ^ get_last_query result ^ "</pre>"
2146           in
2147            output_html outputhtml html ;
2148            let uris',exc =
2149             let rec filter_out =
2150              function
2151                 [] -> [],""
2152               | uri::tl ->
2153                  let tl',exc = filter_out tl in
2154                   try
2155                    if
2156                     ProofEngine.can_apply
2157                      (term_of_cic_textual_parser_uri
2158                       (Misc.cic_textual_parser_uri_of_string uri))
2159                    then
2160                     uri::tl',exc
2161                    else
2162                     tl',exc
2163                   with
2164                    e ->
2165                     let exc' =
2166                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2167                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2168                     in
2169                      tl',exc'
2170             in
2171              filter_out uris
2172            in
2173             let html' =
2174              " <h1>Objects that can actually be applied: </h1> " ^
2175              String.concat "<br>" uris' ^ exc ^
2176              " <h1>Number of false matches: " ^
2177               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2178              " <h1>Number of good matches: " ^
2179               string_of_int (List.length uris') ^ "</h1>"
2180             in
2181              output_html outputhtml html' ;
2182              let uri' =
2183               user_uri_choice ~title:"Ambiguous input."
2184               ~msg:
2185                 "Many lemmas can be successfully applied. Please, choose one:"
2186                uris'
2187              in
2188               inputt#set_term uri' ;
2189               InvokeTactics'.apply ()
2190   with
2191    e -> 
2192     output_html outputhtml 
2193      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2194 ;;
2195       
2196 let choose_selection mmlwidget (element : Gdome.element option) =
2197  let module G = Gdome in
2198   let rec aux element =
2199    if element#hasAttributeNS
2200        ~namespaceURI:Misc.helmns
2201        ~localName:(G.domString "xref")
2202    then
2203      mmlwidget#set_selection (Some element)
2204    else
2205     try
2206       match element#get_parentNode with
2207          None -> assert false
2208        (*CSC: OCAML DIVERGES!
2209        | Some p -> aux (new G.element_of_node p)
2210        *)
2211        | Some p -> aux (new Gdome.element_of_node p)
2212     with
2213        GdomeInit.DOMCastException _ ->
2214         prerr_endline
2215          "******* trying to select above the document root ********"
2216   in
2217    match element with
2218      Some x -> aux x
2219    | None   -> mmlwidget#set_selection None
2220 ;;
2221
2222 (* STUFF TO BUILD THE GTK INTERFACE *)
2223
2224 (* Stuff for the widget settings *)
2225
2226 let export_to_postscript output =
2227  let lastdir = ref (Unix.getcwd ()) in
2228   function () ->
2229    match
2230     GToolbox.select_file ~title:"Export to PostScript"
2231      ~dir:lastdir ~filename:"screenshot.ps" ()
2232    with
2233       None -> ()
2234     | Some filename ->
2235        (output :> GMathView.math_view)#export_to_postscript
2236          ~filename:filename ();
2237 ;;
2238
2239 let activate_t1 output button_set_anti_aliasing
2240  button_set_transparency export_to_postscript_menu_item
2241  button_t1 ()
2242 =
2243  let is_set = button_t1#active in
2244   output#set_font_manager_type
2245    ~fm_type:(if is_set then `font_manager_t1 else `font_manager_gtk) ;
2246   if is_set then
2247    begin
2248     button_set_anti_aliasing#misc#set_sensitive true ;
2249     button_set_transparency#misc#set_sensitive true ;
2250     export_to_postscript_menu_item#misc#set_sensitive true ;
2251    end
2252   else
2253    begin
2254     button_set_anti_aliasing#misc#set_sensitive false ;
2255     button_set_transparency#misc#set_sensitive false ;
2256     export_to_postscript_menu_item#misc#set_sensitive false ;
2257    end
2258 ;;
2259
2260 let set_anti_aliasing output button_set_anti_aliasing () =
2261  output#set_anti_aliasing button_set_anti_aliasing#active
2262 ;;
2263
2264 let set_transparency output button_set_transparency () =
2265  output#set_transparency button_set_transparency#active
2266 ;;
2267
2268 let changefont output font_size_spinb () =
2269  output#set_font_size font_size_spinb#value_as_int
2270 ;;
2271
2272 let set_log_verbosity output log_verbosity_spinb () =
2273  output#set_log_verbosity log_verbosity_spinb#value_as_int
2274 ;;
2275
2276 class settings_window output sw
2277  export_to_postscript_menu_item selection_changed_callback
2278 =
2279  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2280  let vbox =
2281   GPack.vbox ~packing:settings_window#add () in
2282  let table =
2283   GPack.table
2284    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2285    ~border_width:5 ~packing:vbox#add () in
2286  let button_t1 =
2287   GButton.toggle_button ~label:"activate t1 fonts"
2288    ~packing:(table#attach ~left:0 ~top:0) () in
2289  let button_set_anti_aliasing =
2290   GButton.toggle_button ~label:"set_anti_aliasing"
2291    ~packing:(table#attach ~left:0 ~top:1) () in
2292  let button_set_transparency =
2293   GButton.toggle_button ~label:"set_transparency"
2294    ~packing:(table#attach ~left:2 ~top:1) () in
2295  let table =
2296   GPack.table
2297    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2298    ~border_width:5 ~packing:vbox#add () in
2299  let font_size_label =
2300   GMisc.label ~text:"font size:"
2301    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2302  let font_size_spinb =
2303   let sadj =
2304    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2305   in
2306    GEdit.spin_button 
2307     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2308  let log_verbosity_label =
2309   GMisc.label ~text:"log verbosity:"
2310    ~packing:(table#attach ~left:0 ~top:1) () in
2311  let log_verbosity_spinb =
2312   let sadj =
2313    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2314   in
2315    GEdit.spin_button 
2316     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2317  let hbox =
2318   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2319  let closeb =
2320   GButton.button ~label:"Close"
2321    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2322 object(self)
2323  method show = settings_window#show
2324  initializer
2325   button_set_anti_aliasing#misc#set_sensitive false ;
2326   button_set_transparency#misc#set_sensitive false ;
2327   (* Signals connection *)
2328   ignore(button_t1#connect#clicked
2329    (activate_t1 output button_set_anti_aliasing
2330     button_set_transparency export_to_postscript_menu_item button_t1)) ;
2331   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2332   ignore(button_set_anti_aliasing#connect#toggled
2333    (set_anti_aliasing output button_set_anti_aliasing));
2334   ignore(button_set_transparency#connect#toggled
2335    (set_transparency output button_set_transparency)) ;
2336   ignore(log_verbosity_spinb#connect#changed
2337    (set_log_verbosity output log_verbosity_spinb)) ;
2338   ignore(closeb#connect#clicked settings_window#misc#hide)
2339 end;;
2340
2341 (* Scratch window *)
2342
2343 class scratch_window =
2344  let window =
2345   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2346  let vbox =
2347   GPack.vbox ~packing:window#add () in
2348  let hbox =
2349   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2350  let whdb =
2351   GButton.button ~label:"Whd"
2352    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2353  let reduceb =
2354   GButton.button ~label:"Reduce"
2355    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2356  let simplb =
2357   GButton.button ~label:"Simpl"
2358    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2359  let scrolled_window =
2360   GBin.scrolled_window ~border_width:10
2361    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2362  let sequent_viewer =
2363   TermViewer.sequent_viewer
2364    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2365 object(self)
2366  val mutable term = Cic.Rel 1                 (* dummy value *)
2367  val mutable context = ([] : Cic.context)     (* dummy value *)
2368  val mutable metasenv = ([] : Cic.metasenv)   (* dummy value *)
2369  method sequent_viewer = sequent_viewer
2370  method show () = window#misc#hide () ; window#show ()
2371  method term = term
2372  method set_term t = term <- t
2373  method context = context
2374  method set_context t = context <- t
2375  method metasenv = metasenv
2376  method set_metasenv t = metasenv <- t
2377  initializer
2378   ignore
2379    (sequent_viewer#connect#selection_changed (choose_selection sequent_viewer));
2380   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2381   ignore(whdb#connect#clicked InvokeTactics'.whd_in_scratch) ;
2382   ignore(reduceb#connect#clicked InvokeTactics'.reduce_in_scratch) ;
2383   ignore(simplb#connect#clicked InvokeTactics'.simpl_in_scratch)
2384 end;;
2385
2386 let open_contextual_menu_for_selected_terms mmlwidget infos =
2387  let button = GdkEvent.Button.button infos in 
2388  let terms_selected = List.length mmlwidget#get_selections > 0 in
2389   if button = 3 then
2390    begin
2391     let time = GdkEvent.Button.time infos in
2392     let menu = GMenu.menu () in
2393     let f = new GMenu.factory menu in
2394     let whd_menu_item =
2395      f#add_item "Whd" ~key:GdkKeysyms._W ~callback:InvokeTactics'.whd in
2396     let reduce_menu_item =
2397      f#add_item "Reduce" ~key:GdkKeysyms._R ~callback:InvokeTactics'.reduce in
2398     let simpl_menu_item =
2399      f#add_item "Simpl" ~key:GdkKeysyms._S ~callback:InvokeTactics'.simpl in
2400     let _ = f#add_separator () in
2401     let generalize_menu_item =
2402      f#add_item "Generalize"
2403       ~key:GdkKeysyms._G ~callback:InvokeTactics'.generalize in
2404     let _ = f#add_separator () in
2405     let clear_menu_item =
2406      f#add_item "Clear" ~key:GdkKeysyms._C ~callback:InvokeTactics'.clear in
2407     let clearbody_menu_item =
2408      f#add_item "ClearBody"
2409       ~key:GdkKeysyms._B ~callback:InvokeTactics'.clearbody
2410     in
2411      whd_menu_item#misc#set_sensitive terms_selected ; 
2412      reduce_menu_item#misc#set_sensitive terms_selected ; 
2413      simpl_menu_item#misc#set_sensitive terms_selected ;
2414      generalize_menu_item#misc#set_sensitive terms_selected ;
2415      clear_menu_item#misc#set_sensitive terms_selected ;
2416      clearbody_menu_item#misc#set_sensitive terms_selected ;
2417      menu#popup ~button ~time
2418    end ;
2419   true
2420 ;;
2421
2422 class page () =
2423  let vbox1 = GPack.vbox () in
2424 object(self)
2425  val mutable proofw_ref = None
2426  val mutable compute_ref = None
2427  method proofw =
2428   Lazy.force self#compute ;
2429   match proofw_ref with
2430      None -> assert false
2431    | Some proofw -> proofw
2432  method content = vbox1
2433  method compute =
2434   match compute_ref with
2435      None -> assert false
2436    | Some compute -> compute
2437  initializer
2438   compute_ref <-
2439    Some (lazy (
2440    let scrolled_window1 =
2441     GBin.scrolled_window ~border_width:10
2442      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2443    let proofw =
2444     TermViewer.sequent_viewer ~width:400 ~height:275
2445      ~packing:(scrolled_window1#add) () in
2446    let _ = proofw_ref <- Some proofw in
2447    let hbox3 =
2448     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2449    let ringb =
2450     GButton.button ~label:"Ring"
2451      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2452    let fourierb =
2453     GButton.button ~label:"Fourier"
2454      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2455    let reflexivityb =
2456     GButton.button ~label:"Reflexivity"
2457      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2458    let symmetryb =
2459     GButton.button ~label:"Symmetry"
2460      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2461    let assumptionb =
2462     GButton.button ~label:"Assumption"
2463      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2464    let contradictionb =
2465     GButton.button ~label:"Contradiction"
2466      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2467    let hbox4 =
2468     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2469    let existsb =
2470     GButton.button ~label:"Exists"
2471      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2472    let splitb =
2473     GButton.button ~label:"Split"
2474      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2475    let leftb =
2476     GButton.button ~label:"Left"
2477      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2478    let rightb =
2479     GButton.button ~label:"Right"
2480      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2481    let searchpatternb =
2482     GButton.button ~label:"SearchPattern_Apply"
2483      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2484    let hbox5 =
2485     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2486    let exactb =
2487     GButton.button ~label:"Exact"
2488      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2489    let introsb =
2490     GButton.button ~label:"Intros"
2491      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2492    let applyb =
2493     GButton.button ~label:"Apply"
2494      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2495    let elimintrossimplb =
2496     GButton.button ~label:"ElimIntrosSimpl"
2497      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2498    let elimtypeb =
2499     GButton.button ~label:"ElimType"
2500      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2501    let foldwhdb =
2502     GButton.button ~label:"Fold_whd"
2503      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2504    let foldreduceb =
2505     GButton.button ~label:"Fold_reduce"
2506      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2507    let hbox6 =
2508     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2509    let foldsimplb =
2510     GButton.button ~label:"Fold_simpl"
2511      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2512    let cutb =
2513     GButton.button ~label:"Cut"
2514      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2515    let changeb =
2516     GButton.button ~label:"Change"
2517      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2518    let letinb =
2519     GButton.button ~label:"Let ... In"
2520      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2521    let rewritesimplb =
2522     GButton.button ~label:"RewriteSimpl ->"
2523      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2524    let rewritebacksimplb =
2525     GButton.button ~label:"RewriteSimpl <-"
2526      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2527    let hbox7 =
2528     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2529    let absurdb =
2530     GButton.button ~label:"Absurd"
2531      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2532    let decomposeb =
2533     GButton.button ~label:"Decompose"
2534      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2535    let transitivityb =
2536     GButton.button ~label:"Transitivity"
2537      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2538    let replaceb =
2539     GButton.button ~label:"Replace"
2540      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2541    let injectionb =
2542     GButton.button ~label:"Injection"
2543      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2544    let discriminateb =
2545     GButton.button ~label:"Discriminate"
2546      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2547 (* Zack: spostare in una toolbar
2548    let generalizeb =
2549     GButton.button ~label:"Generalize"
2550      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
2551    let clearbodyb =
2552     GButton.button ~label:"ClearBody"
2553      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2554    let clearb =
2555     GButton.button ~label:"Clear"
2556      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2557    let whdb =
2558     GButton.button ~label:"Whd"
2559      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2560    let reduceb =
2561     GButton.button ~label:"Reduce"
2562      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2563    let simplb =
2564     GButton.button ~label:"Simpl"
2565      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2566 *)
2567
2568    ignore(exactb#connect#clicked InvokeTactics'.exact) ;
2569    ignore(applyb#connect#clicked InvokeTactics'.apply) ;
2570    ignore(elimintrossimplb#connect#clicked InvokeTactics'.elimintrossimpl) ;
2571    ignore(elimtypeb#connect#clicked InvokeTactics'.elimtype) ;
2572    ignore(foldwhdb#connect#clicked InvokeTactics'.fold_whd) ;
2573    ignore(foldreduceb#connect#clicked InvokeTactics'.fold_reduce) ;
2574    ignore(foldsimplb#connect#clicked InvokeTactics'.fold_simpl) ;
2575    ignore(cutb#connect#clicked InvokeTactics'.cut) ;
2576    ignore(changeb#connect#clicked InvokeTactics'.change) ;
2577    ignore(letinb#connect#clicked InvokeTactics'.letin) ;
2578    ignore(ringb#connect#clicked InvokeTactics'.ring) ;
2579    ignore(fourierb#connect#clicked InvokeTactics'.fourier) ;
2580    ignore(rewritesimplb#connect#clicked InvokeTactics'.rewritesimpl) ;
2581    ignore(rewritebacksimplb#connect#clicked InvokeTactics'.rewritebacksimpl) ;
2582    ignore(replaceb#connect#clicked InvokeTactics'.replace) ;
2583    ignore(reflexivityb#connect#clicked InvokeTactics'.reflexivity) ;
2584    ignore(symmetryb#connect#clicked InvokeTactics'.symmetry) ;
2585    ignore(transitivityb#connect#clicked InvokeTactics'.transitivity) ;
2586    ignore(existsb#connect#clicked InvokeTactics'.exists) ;
2587    ignore(splitb#connect#clicked InvokeTactics'.split) ;
2588    ignore(leftb#connect#clicked InvokeTactics'.left) ;
2589    ignore(rightb#connect#clicked InvokeTactics'.right) ;
2590    ignore(assumptionb#connect#clicked InvokeTactics'.assumption) ;
2591    ignore(absurdb#connect#clicked InvokeTactics'.absurd) ;
2592    ignore(contradictionb#connect#clicked InvokeTactics'.contradiction) ;
2593    ignore(introsb#connect#clicked InvokeTactics'.intros) ;
2594    ignore(decomposeb#connect#clicked InvokeTactics'.decompose) ;
2595    ignore(searchpatternb#connect#clicked searchPattern) ;
2596    ignore(injectionb#connect#clicked InvokeTactics'.injection) ;
2597    ignore(discriminateb#connect#clicked InvokeTactics'.discriminate) ;
2598 (* Zack: spostare in una toolbar
2599    ignore(whdb#connect#clicked whd) ;
2600    ignore(reduceb#connect#clicked reduce) ;
2601    ignore(simplb#connect#clicked simpl) ;
2602    ignore(clearbodyb#connect#clicked clearbody) ;
2603    ignore(clearb#connect#clicked clear) ;
2604    ignore(generalizeb#connect#clicked generalize) ;
2605 *)
2606    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2607    ignore
2608      ((new GObj.event_ops proofw#as_widget)#connect#button_press
2609         (open_contextual_menu_for_selected_terms proofw)) ;
2610   ))
2611 end
2612 ;;
2613
2614 class empty_page =
2615  let vbox1 = GPack.vbox () in
2616  let scrolled_window1 =
2617   GBin.scrolled_window ~border_width:10
2618    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2619  let proofw =
2620   TermViewer.sequent_viewer ~width:400 ~height:275
2621    ~packing:(scrolled_window1#add) () in
2622 object(self)
2623  method proofw = (assert false : TermViewer.sequent_viewer)
2624  method content = vbox1
2625  method compute = (assert false : unit)
2626 end
2627 ;;
2628
2629 let empty_page = new empty_page;;
2630
2631 class notebook =
2632 object(self)
2633  val notebook = GPack.notebook ()
2634  val pages = ref []
2635  val mutable skip_switch_page_event = false 
2636  val mutable empty = true
2637  method notebook = notebook
2638  method add_page n =
2639   let new_page = new page () in
2640    empty <- false ;
2641    pages := !pages @ [n,lazy (setgoal n),new_page] ;
2642    notebook#append_page
2643     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2644     new_page#content#coerce
2645  method remove_all_pages ~skip_switch_page_event:skip =
2646   if empty then
2647    notebook#remove_page 0 (* let's remove the empty page *)
2648   else
2649    List.iter (function _ -> notebook#remove_page 0) !pages ;
2650   pages := [] ;
2651   skip_switch_page_event <- skip
2652  method set_current_page ~may_skip_switch_page_event n =
2653   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2654    let new_page = notebook#page_num page#content#coerce in
2655     if may_skip_switch_page_event && new_page <> notebook#current_page then
2656      skip_switch_page_event <- true ;
2657     notebook#goto_page new_page
2658  method set_empty_page =
2659   empty <- true ;
2660   pages := [] ;
2661   notebook#append_page
2662    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2663    empty_page#content#coerce
2664  method proofw =
2665   let (_,_,page) = List.nth !pages notebook#current_page in
2666    page#proofw
2667  initializer
2668   ignore
2669    (notebook#connect#switch_page
2670     (function i ->
2671       let skip = skip_switch_page_event in
2672        skip_switch_page_event <- false ;
2673        if not skip then
2674         try
2675          let (metano,setgoal,page) = List.nth !pages i in
2676           ProofEngine.goal := Some metano ;
2677           Lazy.force (page#compute) ;
2678           Lazy.force setgoal
2679         with _ -> ()
2680     ))
2681 end
2682 ;;
2683
2684 (* Main window *)
2685
2686 class rendering_window output (notebook : notebook) =
2687  let scratch_window = new scratch_window in
2688  let window =
2689   GWindow.window ~title:"MathML viewer" ~border_width:0
2690    ~allow_shrink:false () in
2691  let vbox_for_menu = GPack.vbox ~packing:window#add () in
2692  (* menus *)
2693  let handle_box = GBin.handle_box ~border_width:2
2694   ~packing:(vbox_for_menu#pack ~padding:0) () in
2695  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
2696  let factory0 = new GMenu.factory menubar in
2697  let accel_group = factory0#accel_group in
2698  (* file menu *)
2699  let file_menu = factory0#add_submenu "File" in
2700  let factory1 = new GMenu.factory file_menu ~accel_group in
2701  let export_to_postscript_menu_item =
2702   begin
2703    let _ =
2704     factory1#add_item "New Block of (Co)Inductive Definitions..."
2705      ~key:GdkKeysyms._B ~callback:new_inductive
2706    in
2707    let _ =
2708     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
2709      ~callback:new_proof
2710    in
2711    let reopen_menu_item =
2712     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
2713      ~callback:open_
2714    in
2715    let qed_menu_item =
2716     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
2717    ignore (factory1#add_separator ()) ;
2718    ignore
2719     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
2720       ~callback:load) ;
2721    let save_menu_item =
2722     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
2723    in
2724    ignore
2725     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
2726    ignore (!save_set_sensitive false);
2727    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
2728    ignore (!qed_set_sensitive false);
2729    ignore (factory1#add_separator ()) ;
2730    let export_to_postscript_menu_item =
2731     factory1#add_item "Export to PostScript..."
2732      ~callback:(export_to_postscript output) in
2733    ignore (factory1#add_separator ()) ;
2734    ignore
2735     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
2736    export_to_postscript_menu_item
2737   end in
2738  (* edit menu *)
2739  let edit_menu = factory0#add_submenu "Edit Current Proof" in
2740  let factory2 = new GMenu.factory edit_menu ~accel_group in
2741  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
2742  let proveit_menu_item =
2743   factory2#add_item "Prove It" ~key:GdkKeysyms._I
2744    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
2745  in
2746  let focus_menu_item =
2747   factory2#add_item "Focus" ~key:GdkKeysyms._F
2748    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
2749  in
2750  let _ =
2751   focus_and_proveit_set_sensitive :=
2752    function b ->
2753     proveit_menu_item#misc#set_sensitive b ;
2754     focus_menu_item#misc#set_sensitive b
2755  in
2756  let _ = !focus_and_proveit_set_sensitive false in
2757  (* edit term menu *)
2758  let edit_term_menu = factory0#add_submenu "Edit Term" in
2759  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
2760  let check_menu_item =
2761   factory5#add_item "Check Term" ~key:GdkKeysyms._C
2762    ~callback:(check scratch_window) in
2763  let _ = check_menu_item#misc#set_sensitive false in
2764  (* search menu *)
2765  let settings_menu = factory0#add_submenu "Search" in
2766  let factory4 = new GMenu.factory settings_menu ~accel_group in
2767  let _ =
2768   factory4#add_item "Locate..." ~key:GdkKeysyms._T
2769    ~callback:locate in
2770  let searchPattern_menu_item =
2771   factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
2772    ~callback:completeSearchPattern in
2773  let _ = searchPattern_menu_item#misc#set_sensitive false in
2774  let show_menu_item =
2775   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
2776  in
2777  let insert_query_item =
2778   factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
2779    ~callback:insertQuery in
2780  (* settings menu *)
2781  let settings_menu = factory0#add_submenu "Settings" in
2782  let factory3 = new GMenu.factory settings_menu ~accel_group in
2783  let _ =
2784   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
2785    ~callback:edit_aliases in
2786  let _ = factory3#add_separator () in
2787  let _ =
2788   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
2789    ~callback:(function _ -> (settings_window ())#show ()) in
2790  (* accel group *)
2791  let _ = window#add_accel_group accel_group in
2792  (* end of menus *)
2793  let hbox0 =
2794   GPack.hbox
2795    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
2796  let vbox =
2797   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2798  let scrolled_window0 =
2799   GBin.scrolled_window ~border_width:10
2800    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2801  let _ = scrolled_window0#add output#coerce in
2802  let frame =
2803   GBin.frame ~label:"Insert Term"
2804    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2805  let scrolled_window1 =
2806   GBin.scrolled_window ~border_width:5
2807    ~packing:frame#add () in
2808  let inputt =
2809   TermEditor'.term_editor
2810    ~width:400 ~height:100 ~packing:scrolled_window1#add ()
2811    ~isnotempty_callback:
2812     (function b ->
2813       check_menu_item#misc#set_sensitive b ;
2814       searchPattern_menu_item#misc#set_sensitive b) in
2815  let vboxl =
2816   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2817  let _ =
2818   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
2819  let frame =
2820   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
2821  in
2822  let outputhtml =
2823   GHtml.xmhtml
2824    ~source:"<html><body bgColor=\"white\"></body></html>"
2825    ~width:400 ~height: 100
2826    ~border_width:20
2827    ~packing:frame#add
2828    ~show:true () in
2829 object
2830  method outputhtml = outputhtml
2831  method inputt = inputt
2832  method output = (output : TermViewer.proof_viewer)
2833  method scratch_window = scratch_window
2834  method notebook = notebook
2835  method show = window#show
2836  initializer
2837   notebook#set_empty_page ;
2838   export_to_postscript_menu_item#misc#set_sensitive false ;
2839   check_term := (check_term_in_scratch scratch_window) ;
2840
2841   (* signal handlers here *)
2842   ignore(output#connect#selection_changed
2843    (function elem ->
2844      choose_selection output elem ;
2845      !focus_and_proveit_set_sensitive true
2846    )) ;
2847   ignore (output#connect#click (show_in_show_window_callback output)) ;
2848   let settings_window = new settings_window output scrolled_window0
2849    export_to_postscript_menu_item (choose_selection output) in
2850   set_settings_window settings_window ;
2851   set_outputhtml outputhtml ;
2852   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2853   Logger.log_callback :=
2854    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2855 end;;
2856
2857 (* MAIN *)
2858
2859 let initialize_everything () =
2860  let module U = Unix in
2861   let output = TermViewer.proof_viewer ~width:350 ~height:280 () in
2862   let notebook = new notebook in
2863    let rendering_window' = new rendering_window output notebook in
2864     set_rendering_window rendering_window' ;
2865     rendering_window'#show () ;
2866     GMain.Main.main ()
2867 ;;
2868
2869 let _ =
2870  if !usedb then
2871   begin
2872    Mqint.set_database Mqint.postgres_db ;
2873    Mqint.init postgresqlconnectionstring ;
2874   end ;
2875  ignore (GtkMain.Main.init ()) ;
2876  initialize_everything () ;
2877  if !usedb then Mqint.close ();
2878 ;;