helm/gTopLevel/gTopLevel.ml

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