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