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