helm/gTopLevel/gTopLevel.ml

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