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