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