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          GMathViewAux.single_selection_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_doc ~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 : GMathViewAux.single_selection_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_doc ~dom: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_doc ~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 : GMathViewAux.single_selection_math_view)#load_doc 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 : GMathViewAux.single_selection_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   GMathViewAux.single_selection_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_doc 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        prerr_endline
1102         "'get_action' and 'action_toggle' not yet implemented in lablgtkmathview 0.3.99"
1103 (* TODO commented out because not yet implemented in lablgtkmathview 0.3.99 *)
1104 (*
1105      if mmlwidget#get_action <> None then
1106       mmlwidget#action_toggle
1107 *)
1108    in
1109     let _ =
1110      mmlwidget#connect#click (show_in_show_window_callback mmlwidget)
1111     in
1112      show_in_show_window_obj, show_in_show_window_uri,
1113       show_in_show_window_callback
1114 ;;
1115
1116 exception NoObjectsLocated;;
1117
1118 let user_uri_choice ~title ~msg uris =
1119  let uri =
1120   match uris with
1121      [] -> raise NoObjectsLocated
1122    | [uri] -> uri
1123    | uris ->
1124       match
1125        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1126       with
1127          [uri] -> uri
1128        | _ -> assert false
1129  in
1130   String.sub uri 4 (String.length uri - 4)
1131 ;;
1132
1133 let locate_callback id =
1134  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1135  let result = MQueryGenerator.locate id in
1136  let uris =
1137   List.map
1138    (function uri,_ ->
1139      Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri)
1140    result in
1141  let html =
1142   (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1143  in
1144   output_html outputhtml html ;
1145   user_uri_choice ~title:"Ambiguous input."
1146    ~msg:
1147      ("Ambiguous input \"" ^ id ^
1148       "\". Please, choose one interpetation:")
1149    uris
1150 ;;
1151
1152
1153 let input_or_locate_uri ~title =
1154  let uri = ref None in
1155  let window =
1156   GWindow.window
1157    ~width:400 ~modal:true ~title ~border_width:2 () in
1158  let vbox = GPack.vbox ~packing:window#add () in
1159  let hbox1 =
1160   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1161  let _ =
1162   GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1163  let manual_input =
1164   GEdit.entry ~editable:true
1165    ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1166  let checkb =
1167   GButton.button ~label:"Check"
1168    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1169  let _ = checkb#misc#set_sensitive false in
1170  let hbox2 =
1171   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1172  let _ =
1173   GMisc.label ~text:"You can also enter an indentifier to locate:"
1174    ~packing:(hbox2#pack ~padding:5) () in
1175  let locate_input =
1176   GEdit.entry ~editable:true
1177    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1178  let locateb =
1179   GButton.button ~label:"Locate"
1180    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1181  let _ = locateb#misc#set_sensitive false in
1182  let hbox3 =
1183   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1184  let okb =
1185   GButton.button ~label:"Ok"
1186    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1187  let _ = okb#misc#set_sensitive false in
1188  let cancelb =
1189   GButton.button ~label:"Cancel"
1190    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1191  in
1192   ignore (window#connect#destroy GMain.Main.quit) ;
1193   ignore
1194    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1195   let check_callback () =
1196    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1197    let uri = "cic:" ^ manual_input#text in
1198     try
1199       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1200       output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1201       true
1202     with
1203        Getter.Unresolved ->
1204         output_html outputhtml
1205          ("<h1 color=\"Red\">URI " ^ uri ^
1206           " does not correspond to any object.</h1>") ;
1207         false
1208      | UriManager.IllFormedUri _ ->
1209         output_html outputhtml
1210          ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1211         false
1212      | e ->
1213         output_html outputhtml
1214          ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1215         false
1216   in
1217   ignore
1218    (okb#connect#clicked
1219      (function () ->
1220        if check_callback () then
1221         begin
1222          uri := Some manual_input#text ;
1223          window#destroy ()
1224         end
1225    )) ;
1226   ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1227   ignore
1228    (manual_input#connect#changed
1229      (fun _ ->
1230        if manual_input#text = "" then
1231         begin
1232          checkb#misc#set_sensitive false ;
1233          okb#misc#set_sensitive false
1234         end
1235        else
1236         begin
1237          checkb#misc#set_sensitive true ;
1238          okb#misc#set_sensitive true
1239         end));
1240   ignore
1241    (locate_input#connect#changed
1242      (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1243   ignore
1244    (locateb#connect#clicked
1245      (function () ->
1246        let id = locate_input#text in
1247         manual_input#set_text (locate_callback id) ;
1248         locate_input#delete_text 0 (String.length id)
1249    )) ;
1250   window#show () ;
1251   GMain.Main.main () ;
1252   match !uri with
1253      None -> raise NoChoice
1254    | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1255 ;;
1256
1257 exception AmbiguousInput;;
1258
1259 (* A WIDGET TO ENTER CIC TERMS *)
1260
1261 module Callbacks =
1262  struct
1263   let output_html msg = output_html (outputhtml ()) msg;;
1264   let interactive_user_uri_choice =
1265    fun ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg ~id ->
1266     interactive_user_uri_choice ~selection_mode ?ok
1267      ?enable_button_for_non_vars ~title ~msg;;
1268   let interactive_interpretation_choice = interactive_interpretation_choice;;
1269   let input_or_locate_uri = input_or_locate_uri;;
1270  end
1271 ;;
1272
1273 module Disambiguate' = Disambiguate.Make(Callbacks);;
1274
1275 class term_editor ?packing ?width ?height ?isnotempty_callback () =
1276  let input = GEdit.text ~editable:true ?width ?height ?packing () in
1277  let _ =
1278   match isnotempty_callback with
1279      None -> ()
1280    | Some callback ->
1281       ignore(input#connect#changed (function () -> callback (input#length > 0)))
1282  in
1283 object(self)
1284  method coerce = input#coerce
1285  method reset =
1286   input#delete_text 0 input#length
1287  (* CSC: txt is now a string, but should be of type Cic.term *)
1288  method set_term txt =
1289   self#reset ;
1290   ignore ((input#insert_text txt) ~pos:0)
1291  (* CSC: this method should disappear *)
1292  method get_as_string =
1293   input#get_chars 0 input#length
1294  method get_metasenv_and_term ~context ~metasenv =
1295   let name_context =
1296    List.map
1297     (function
1298         Some (n,_) -> Some n
1299       | None -> None
1300     ) context
1301   in
1302    let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
1303     let dom,mk_metasenv_and_expr =
1304      CicTextualParserContext.main
1305       ~context:name_context ~metasenv CicTextualLexer.token lexbuf
1306     in
1307      let id_to_uris',metasenv,expr =
1308       Disambiguate'.disambiguate_input context metasenv dom mk_metasenv_and_expr
1309        ~id_to_uris:!id_to_uris
1310      in
1311       id_to_uris := id_to_uris' ;
1312       metasenv,expr
1313 end
1314 ;;
1315
1316 (* OTHER FUNCTIONS *)
1317
1318 let locate () =
1319  let inputt = ((rendering_window ())#inputt : term_editor) in
1320  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1321    try
1322     match
1323      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1324     with
1325        None -> raise NoChoice
1326      | Some input ->
1327         let uri = locate_callback input in
1328          inputt#set_term uri
1329    with
1330     e ->
1331      output_html outputhtml
1332       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1333 ;;
1334
1335
1336 exception UriAlreadyInUse;;
1337 exception NotAUriToAConstant;;
1338
1339 let new_inductive () =
1340  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1341  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1342  let notebook = (rendering_window ())#notebook in
1343
1344  let chosen = ref false in
1345  let inductive = ref true in
1346  let paramsno = ref 0 in
1347  let get_uri = ref (function _ -> assert false) in
1348  let get_base_uri = ref (function _ -> assert false) in
1349  let get_names = ref (function _ -> assert false) in
1350  let get_types_and_cons = ref (function _ -> assert false) in
1351  let get_context_and_subst = ref (function _ -> assert false) in
1352  let window =
1353   GWindow.window
1354    ~width:600 ~modal:true ~position:`CENTER
1355    ~title:"New Block of Mutual (Co)Inductive Definitions"
1356    ~border_width:2 () in
1357  let vbox = GPack.vbox ~packing:window#add () in
1358  let hbox =
1359   GPack.hbox ~border_width:0
1360    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1361  let _ =
1362   GMisc.label ~text:"Enter the URI for the new block:"
1363    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1364  let uri_entry =
1365   GEdit.entry ~editable:true
1366    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1367  let hbox0 =
1368   GPack.hbox ~border_width:0
1369    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1370  let _ =
1371   GMisc.label
1372    ~text:
1373      "Enter the number of left parameters in every arity and constructor type:"
1374    ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1375  let paramsno_entry =
1376   GEdit.entry ~editable:true ~text:"0"
1377    ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1378  let hbox1 =
1379   GPack.hbox ~border_width:0
1380    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1381  let _ =
1382   GMisc.label ~text:"Are the definitions inductive or coinductive?"
1383    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1384  let inductiveb =
1385   GButton.radio_button ~label:"Inductive"
1386    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1387  let coinductiveb =
1388   GButton.radio_button ~label:"Coinductive"
1389    ~group:inductiveb#group
1390    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1391  let hbox2 =
1392   GPack.hbox ~border_width:0
1393    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1394  let _ =
1395   GMisc.label ~text:"Enter the list of the names of the types:"
1396    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1397  let names_entry =
1398   GEdit.entry ~editable:true
1399    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1400  let hboxn =
1401   GPack.hbox ~border_width:0
1402    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1403  let okb =
1404   GButton.button ~label:"> Next"
1405    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1406  let _ = okb#misc#set_sensitive true in
1407  let cancelb =
1408   GButton.button ~label:"Abort"
1409    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1410  ignore (window#connect#destroy GMain.Main.quit) ;
1411  ignore (cancelb#connect#clicked window#destroy) ;
1412  (* First phase *)
1413  let rec phase1 () =
1414   ignore
1415    (okb#connect#clicked
1416      (function () ->
1417        try
1418         let uristr = "cic:" ^ uri_entry#text in
1419         let namesstr = names_entry#text in
1420         let paramsno' = int_of_string (paramsno_entry#text) in
1421          match Str.split (Str.regexp " +") namesstr with
1422             [] -> assert false
1423           | (he::tl) as names ->
1424              let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1425               begin
1426                try
1427                 ignore (Getter.resolve uri) ;
1428                 raise UriAlreadyInUse
1429                with
1430                 Getter.Unresolved ->
1431                  get_uri := (function () -> uri) ;
1432                  get_names := (function () -> names) ;
1433                  inductive := inductiveb#active ;
1434                  paramsno := paramsno' ;
1435                  phase2 ()
1436               end
1437        with
1438         e ->
1439          output_html outputhtml
1440           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1441      ))
1442  (* Second phase *)
1443  and phase2 () =
1444   let type_widgets =
1445    List.map
1446     (function name ->
1447       let frame =
1448        GBin.frame ~label:name
1449         ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1450       let vbox = GPack.vbox ~packing:frame#add () in
1451       let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1452       let _ =
1453        GMisc.label ~text:("Enter its type:")
1454         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1455       let scrolled_window =
1456        GBin.scrolled_window ~border_width:5
1457         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1458       let newinputt =
1459        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1460         ~isnotempty_callback:
1461          (function b ->
1462            (*non_empty_type := b ;*)
1463            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1464       in
1465       let hbox =
1466        GPack.hbox ~border_width:0
1467         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1468       let _ =
1469        GMisc.label ~text:("Enter the list of its constructors:")
1470         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1471       let cons_names_entry =
1472        GEdit.entry ~editable:true
1473         ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1474       (newinputt,cons_names_entry)
1475     ) (!get_names ())
1476   in
1477    vbox#remove hboxn#coerce ;
1478    let hboxn =
1479     GPack.hbox ~border_width:0
1480      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1481    let okb =
1482     GButton.button ~label:"> Next"
1483      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1484    let cancelb =
1485     GButton.button ~label:"Abort"
1486      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1487    ignore (cancelb#connect#clicked window#destroy) ;
1488    ignore
1489     (okb#connect#clicked
1490       (function () ->
1491         try
1492          let names = !get_names () in
1493          let types_and_cons =
1494           List.map2
1495            (fun name (newinputt,cons_names_entry) ->
1496              let consnamesstr = cons_names_entry#text in
1497              let cons_names = Str.split (Str.regexp " +") consnamesstr in
1498              let metasenv,expr =
1499               newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
1500              in
1501               match metasenv with
1502                  [] -> expr,cons_names
1503                | _ -> raise AmbiguousInput
1504            ) names type_widgets
1505          in
1506           let uri = !get_uri () in
1507           let _ =
1508            (* Let's see if so far the definition is well-typed *)
1509            let params = [] in
1510            let paramsno = 0 in
1511            (* To test if the arities of the inductive types are well *)
1512            (* typed, we check the inductive block definition where   *)
1513            (* no constructor is given to each type.                  *)
1514            let tys =
1515             List.map2
1516              (fun name (ty,cons) -> (name, !inductive, ty, []))
1517              names types_and_cons
1518            in
1519             CicTypeChecker.typecheck_mutual_inductive_defs uri
1520              (tys,params,paramsno)
1521           in
1522            get_context_and_subst :=
1523             (function () ->
1524               let i = ref 0 in
1525                List.fold_left2
1526                 (fun (context,subst) name (ty,_) ->
1527                   let res =
1528                    (Some (Cic.Name name, Cic.Decl ty))::context,
1529                     (Cic.MutInd (uri,!i,[]))::subst
1530                   in
1531                    incr i ; res
1532                 ) ([],[]) names types_and_cons) ;
1533            let types_and_cons' =
1534             List.map2
1535              (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1536              names types_and_cons
1537            in
1538             get_types_and_cons := (function () -> types_and_cons') ;
1539             chosen := true ;
1540             window#destroy ()
1541         with
1542          e ->
1543           output_html outputhtml
1544            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1545       ))
1546  (* Third phase *)
1547  and phase3 name cons =
1548   let get_cons_types = ref (function () -> assert false) in
1549   let window2 =
1550    GWindow.window
1551     ~width:600 ~modal:true ~position:`CENTER
1552     ~title:(name ^ " Constructors")
1553     ~border_width:2 () in
1554   let vbox = GPack.vbox ~packing:window2#add () in
1555   let cons_type_widgets =
1556    List.map
1557     (function consname ->
1558       let hbox =
1559        GPack.hbox ~border_width:0
1560         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1561       let _ =
1562        GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1563         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1564       let scrolled_window =
1565        GBin.scrolled_window ~border_width:5
1566         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1567       let newinputt =
1568        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1569         ~isnotempty_callback:
1570          (function b ->
1571            (* (*non_empty_type := b ;*)
1572            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1573       in
1574        newinputt
1575     ) cons in
1576   let hboxn =
1577    GPack.hbox ~border_width:0
1578     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1579   let okb =
1580    GButton.button ~label:"> Next"
1581     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1582   let _ = okb#misc#set_sensitive true in
1583   let cancelb =
1584    GButton.button ~label:"Abort"
1585     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1586   ignore (window2#connect#destroy GMain.Main.quit) ;
1587   ignore (cancelb#connect#clicked window2#destroy) ;
1588   ignore
1589    (okb#connect#clicked
1590      (function () ->
1591        try
1592         chosen := true ;
1593         let context,subst= !get_context_and_subst () in
1594         let cons_types =
1595          List.map2
1596           (fun name inputt ->
1597             let metasenv,expr =
1598              inputt#get_metasenv_and_term ~context ~metasenv:[]
1599             in
1600              match metasenv with
1601                 [] ->
1602                  let undebrujined_expr =
1603                   List.fold_left
1604                    (fun expr t -> CicSubstitution.subst t expr) expr subst
1605                  in
1606                   name, undebrujined_expr
1607               | _ -> raise AmbiguousInput
1608           ) cons cons_type_widgets
1609         in
1610          get_cons_types := (function () -> cons_types) ;
1611          window2#destroy ()
1612        with
1613         e ->
1614          output_html outputhtml
1615           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1616      )) ;
1617   window2#show () ;
1618   GMain.Main.main () ;
1619   let okb_pressed = !chosen in
1620    chosen := false ;
1621    if (not okb_pressed) then
1622     begin
1623      window#destroy () ;
1624      assert false (* The control never reaches this point *)
1625     end
1626    else
1627     (!get_cons_types ())
1628  in
1629   phase1 () ;
1630   (* No more phases left or Abort pressed *)
1631   window#show () ;
1632   GMain.Main.main () ;
1633   window#destroy () ;
1634   if !chosen then
1635    try
1636     let uri = !get_uri () in
1637 (*CSC: Da finire *)
1638     let params = [] in
1639     let tys = !get_types_and_cons () in
1640      let obj = Cic.InductiveDefinition tys params !paramsno in
1641       begin
1642        try
1643         prerr_endline (CicPp.ppobj obj) ;
1644         CicTypeChecker.typecheck_mutual_inductive_defs uri
1645          (tys,params,!paramsno) ;
1646         with
1647          e ->
1648           prerr_endline "Offending mutual (co)inductive type declaration:" ;
1649           prerr_endline (CicPp.ppobj obj) ;
1650       end ;
1651       (* We already know that obj is well-typed. We need to add it to the  *)
1652       (* environment in order to compute the inner-types without having to *)
1653       (* debrujin it or having to modify lots of other functions to avoid  *)
1654       (* asking the environment for the MUTINDs we are defining now.       *)
1655       CicEnvironment.put_inductive_definition uri obj ;
1656       save_obj uri obj ;
1657       show_in_show_window_obj uri obj
1658    with
1659     e ->
1660      output_html outputhtml
1661       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1662 ;;
1663
1664 let new_proof () =
1665  let inputt = ((rendering_window ())#inputt : term_editor) in
1666  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1667  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1668  let notebook = (rendering_window ())#notebook in
1669
1670  let chosen = ref false in
1671  let get_metasenv_and_term = ref (function _ -> assert false) in
1672  let get_uri = ref (function _ -> assert false) in
1673  let non_empty_type = ref false in
1674  let window =
1675   GWindow.window
1676    ~width:600 ~modal:true ~title:"New Proof or Definition"
1677    ~border_width:2 () in
1678  let vbox = GPack.vbox ~packing:window#add () in
1679  let hbox =
1680   GPack.hbox ~border_width:0
1681    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1682  let _ =
1683   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1684    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1685  let uri_entry =
1686   GEdit.entry ~editable:true
1687    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1688  let hbox1 =
1689   GPack.hbox ~border_width:0
1690    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1691  let _ =
1692   GMisc.label ~text:"Enter the theorem or definition type:"
1693    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1694  let scrolled_window =
1695   GBin.scrolled_window ~border_width:5
1696    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1697  (* the content of the scrolled_window is moved below (see comment) *)
1698  let hbox =
1699   GPack.hbox ~border_width:0
1700    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1701  let okb =
1702   GButton.button ~label:"Ok"
1703    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1704  let _ = okb#misc#set_sensitive false in
1705  let cancelb =
1706   GButton.button ~label:"Cancel"
1707    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1708  (* moved here to have visibility of the ok button *)
1709  let newinputt =
1710   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1711    ~isnotempty_callback:
1712     (function b ->
1713       non_empty_type := b ;
1714       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1715  in
1716  let _ =
1717   newinputt#set_term inputt#get_as_string ;
1718   inputt#reset in
1719  let _ =
1720   uri_entry#connect#changed
1721    (function () ->
1722      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1723  in
1724  ignore (window#connect#destroy GMain.Main.quit) ;
1725  ignore (cancelb#connect#clicked window#destroy) ;
1726  ignore
1727   (okb#connect#clicked
1728     (function () ->
1729       chosen := true ;
1730       try
1731        let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
1732        let uristr = "cic:" ^ uri_entry#text in
1733        let uri = UriManager.uri_of_string uristr in
1734         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1735          raise NotAUriToAConstant
1736         else
1737          begin
1738           try
1739            ignore (Getter.resolve uri) ;
1740            raise UriAlreadyInUse
1741           with
1742            Getter.Unresolved ->
1743             get_metasenv_and_term := (function () -> metasenv,parsed) ;
1744             get_uri := (function () -> uri) ;
1745             window#destroy ()
1746          end
1747       with
1748        e ->
1749         output_html outputhtml
1750          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1751   )) ;
1752  window#show () ;
1753  GMain.Main.main () ;
1754  if !chosen then
1755   try
1756    let metasenv,expr = !get_metasenv_and_term () in
1757     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1758      ProofEngine.proof :=
1759       Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1760      ProofEngine.goal := Some 1 ;
1761      refresh_sequent notebook ;
1762      refresh_proof output ;
1763      !save_set_sensitive true ;
1764      inputt#reset
1765   with
1766      RefreshSequentException e ->
1767       output_html outputhtml
1768        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1769         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1770    | RefreshProofException e ->
1771       output_html outputhtml
1772        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1773         "proof: " ^ Printexc.to_string e ^ "</h1>")
1774    | e ->
1775       output_html outputhtml
1776        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1777 ;;
1778
1779 let check_term_in_scratch scratch_window metasenv context expr =
1780  try
1781   let ty = CicTypeChecker.type_of_aux' metasenv context expr in
1782    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1783     scratch_window#show () ;
1784     scratch_window#mmlwidget#load_doc ~dom:mml
1785  with
1786   e ->
1787    print_endline ("? " ^ CicPp.ppterm expr) ;
1788    raise e
1789 ;;
1790
1791 let check scratch_window () =
1792  let inputt = ((rendering_window ())#inputt : term_editor) in
1793  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1794   let metasenv =
1795    match !ProofEngine.proof with
1796       None -> []
1797     | Some (_,metasenv,_,_) -> metasenv
1798   in
1799   let context =
1800    match !ProofEngine.goal with
1801       None -> []
1802     | Some metano ->
1803        let (_,canonical_context,_) =
1804         List.find (function (m,_,_) -> m=metano) metasenv
1805        in
1806         canonical_context
1807   in
1808    try
1809     let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
1810      check_term_in_scratch scratch_window metasenv' context expr
1811    with
1812     e ->
1813      output_html outputhtml
1814       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1815 ;;
1816
1817
1818 (***********************)
1819 (*       TACTICS       *)
1820 (***********************)
1821
1822 let call_tactic tactic () =
1823  let notebook = (rendering_window ())#notebook in
1824  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1825  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1826  let savedproof = !ProofEngine.proof in
1827  let savedgoal  = !ProofEngine.goal in
1828   begin
1829    try
1830     tactic () ;
1831     refresh_sequent notebook ;
1832     refresh_proof output
1833    with
1834       RefreshSequentException e ->
1835        output_html outputhtml
1836         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1837          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1838        ProofEngine.proof := savedproof ;
1839        ProofEngine.goal := savedgoal ;
1840        refresh_sequent notebook
1841     | RefreshProofException e ->
1842        output_html outputhtml
1843         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1844          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1845        ProofEngine.proof := savedproof ;
1846        ProofEngine.goal := savedgoal ;
1847        refresh_sequent notebook ;
1848        refresh_proof output
1849     | e ->
1850        output_html outputhtml
1851         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1852        ProofEngine.proof := savedproof ;
1853        ProofEngine.goal := savedgoal ;
1854   end
1855 ;;
1856
1857 let call_tactic_with_input tactic () =
1858  let notebook = (rendering_window ())#notebook in
1859  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1860  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1861  let inputt = ((rendering_window ())#inputt : term_editor) in
1862  let savedproof = !ProofEngine.proof in
1863  let savedgoal  = !ProofEngine.goal in
1864   let uri,metasenv,bo,ty =
1865    match !ProofEngine.proof with
1866       None -> assert false
1867     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1868   in
1869    let canonical_context =
1870     match !ProofEngine.goal with
1871        None -> assert false
1872      | Some metano ->
1873         let (_,canonical_context,_) =
1874          List.find (function (m,_,_) -> m=metano) metasenv
1875         in
1876          canonical_context
1877    in
1878     try
1879      let metasenv',expr =
1880       inputt#get_metasenv_and_term canonical_context metasenv
1881      in
1882       ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1883       tactic expr ;
1884       refresh_sequent notebook ;
1885       refresh_proof output ;
1886       inputt#reset
1887     with
1888        RefreshSequentException e ->
1889         output_html outputhtml
1890          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1891           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1892         ProofEngine.proof := savedproof ;
1893         ProofEngine.goal := savedgoal ;
1894         refresh_sequent notebook
1895      | RefreshProofException e ->
1896         output_html outputhtml
1897          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1898           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1899         ProofEngine.proof := savedproof ;
1900         ProofEngine.goal := savedgoal ;
1901         refresh_sequent notebook ;
1902         refresh_proof output
1903      | e ->
1904         output_html outputhtml
1905          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1906         ProofEngine.proof := savedproof ;
1907         ProofEngine.goal := savedgoal ;
1908 ;;
1909
1910 let call_tactic_with_goal_input tactic () =
1911  let module L = LogicalOperations in
1912  let module G = Gdome in
1913   let notebook = (rendering_window ())#notebook in
1914   let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1915   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1916   let savedproof = !ProofEngine.proof in
1917   let savedgoal  = !ProofEngine.goal in
1918    match notebook#proofw#get_selection with
1919      Some node ->
1920       let xpath =
1921        ((node : Gdome.element)#getAttributeNS
1922          ~namespaceURI:helmns
1923          ~localName:(G.domString "xref"))#to_string
1924       in
1925        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1926        else
1927         begin
1928          try
1929           match !current_goal_infos with
1930              Some (ids_to_terms, ids_to_father_ids,_) ->
1931               let id = xpath in
1932                tactic (Hashtbl.find ids_to_terms id) ;
1933                refresh_sequent notebook ;
1934                refresh_proof output
1935            | None -> assert false (* "ERROR: No current term!!!" *)
1936          with
1937             RefreshSequentException e ->
1938              output_html outputhtml
1939               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1940                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1941              ProofEngine.proof := savedproof ;
1942              ProofEngine.goal := savedgoal ;
1943              refresh_sequent notebook
1944           | RefreshProofException e ->
1945              output_html outputhtml
1946               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1947                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1948              ProofEngine.proof := savedproof ;
1949              ProofEngine.goal := savedgoal ;
1950              refresh_sequent notebook ;
1951              refresh_proof output
1952           | e ->
1953              output_html outputhtml
1954               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1955              ProofEngine.proof := savedproof ;
1956              ProofEngine.goal := savedgoal ;
1957         end
1958    | None ->
1959       output_html outputhtml
1960        ("<h1 color=\"red\">No term selected</h1>")
1961 ;;
1962
1963 let call_tactic_with_input_and_goal_input tactic () =
1964  let module L = LogicalOperations in
1965  let module G = Gdome in
1966   let notebook = (rendering_window ())#notebook in
1967   let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
1968   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1969   let inputt = ((rendering_window ())#inputt : term_editor) in
1970   let savedproof = !ProofEngine.proof in
1971   let savedgoal  = !ProofEngine.goal in
1972    match notebook#proofw#get_selection with
1973      Some node ->
1974       let xpath =
1975        ((node : Gdome.element)#getAttributeNS
1976          ~namespaceURI:helmns
1977          ~localName:(G.domString "xref"))#to_string
1978       in
1979        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1980        else
1981         begin
1982          try
1983           match !current_goal_infos with
1984              Some (ids_to_terms, ids_to_father_ids,_) ->
1985               let id = xpath in
1986                let uri,metasenv,bo,ty =
1987                 match !ProofEngine.proof with
1988                    None -> assert false
1989                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1990                in
1991                 let canonical_context =
1992                  match !ProofEngine.goal with
1993                     None -> assert false
1994                   | Some metano ->
1995                      let (_,canonical_context,_) =
1996                       List.find (function (m,_,_) -> m=metano) metasenv
1997                      in
1998                       canonical_context in
1999                 let (metasenv',expr) =
2000                  inputt#get_metasenv_and_term canonical_context metasenv
2001                 in
2002                  ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2003                  tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2004                   ~input:expr ;
2005                  refresh_sequent notebook ;
2006                  refresh_proof output ;
2007                  inputt#reset
2008            | None -> assert false (* "ERROR: No current term!!!" *)
2009          with
2010             RefreshSequentException e ->
2011              output_html outputhtml
2012               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2013                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2014              ProofEngine.proof := savedproof ;
2015              ProofEngine.goal := savedgoal ;
2016              refresh_sequent notebook
2017           | RefreshProofException e ->
2018              output_html outputhtml
2019               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2020                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2021              ProofEngine.proof := savedproof ;
2022              ProofEngine.goal := savedgoal ;
2023              refresh_sequent notebook ;
2024              refresh_proof output
2025           | e ->
2026              output_html outputhtml
2027               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2028              ProofEngine.proof := savedproof ;
2029              ProofEngine.goal := savedgoal ;
2030         end
2031    | None ->
2032       output_html outputhtml
2033        ("<h1 color=\"red\">No term selected</h1>")
2034 ;;
2035
2036 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2037  let module L = LogicalOperations in
2038  let module G = Gdome in
2039   let mmlwidget = (scratch_window#mmlwidget : GMathViewAux.single_selection_math_view) in
2040   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2041   let savedproof = !ProofEngine.proof in
2042   let savedgoal  = !ProofEngine.goal in
2043    match mmlwidget#get_selection with
2044      Some node ->
2045       let xpath =
2046        ((node : Gdome.element)#getAttributeNS
2047          ~namespaceURI:helmns
2048          ~localName:(G.domString "xref"))#to_string
2049       in
2050        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2051        else
2052         begin
2053          try
2054           match !current_scratch_infos with
2055              (* term is the whole goal in the scratch_area *)
2056              Some (term,ids_to_terms, ids_to_father_ids,_) ->
2057               let id = xpath in
2058                let expr = tactic term (Hashtbl.find ids_to_terms id) in
2059                 let mml = mml_of_cic_term 111 expr in
2060                  scratch_window#show () ;
2061                  scratch_window#mmlwidget#load_doc ~dom:mml
2062            | None -> assert false (* "ERROR: No current term!!!" *)
2063          with
2064           e ->
2065            output_html outputhtml
2066             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2067         end
2068    | None ->
2069       output_html outputhtml
2070        ("<h1 color=\"red\">No term selected</h1>")
2071 ;;
2072
2073 let call_tactic_with_hypothesis_input tactic () =
2074  let module L = LogicalOperations in
2075  let module G = Gdome in
2076   let notebook = (rendering_window ())#notebook in
2077   let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2078   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2079   let savedproof = !ProofEngine.proof in
2080   let savedgoal  = !ProofEngine.goal in
2081    match notebook#proofw#get_selection with
2082      Some node ->
2083       let xpath =
2084        ((node : Gdome.element)#getAttributeNS
2085          ~namespaceURI:helmns
2086          ~localName:(G.domString "xref"))#to_string
2087       in
2088        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2089        else
2090         begin
2091          try
2092           match !current_goal_infos with
2093              Some (_,_,ids_to_hypotheses) ->
2094               let id = xpath in
2095                tactic (Hashtbl.find ids_to_hypotheses id) ;
2096                refresh_sequent notebook ;
2097                refresh_proof output
2098            | None -> assert false (* "ERROR: No current term!!!" *)
2099          with
2100             RefreshSequentException e ->
2101              output_html outputhtml
2102               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2103                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2104              ProofEngine.proof := savedproof ;
2105              ProofEngine.goal := savedgoal ;
2106              refresh_sequent notebook
2107           | RefreshProofException e ->
2108              output_html outputhtml
2109               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2110                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2111              ProofEngine.proof := savedproof ;
2112              ProofEngine.goal := savedgoal ;
2113              refresh_sequent notebook ;
2114              refresh_proof output
2115           | e ->
2116              output_html outputhtml
2117               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2118              ProofEngine.proof := savedproof ;
2119              ProofEngine.goal := savedgoal ;
2120         end
2121    | None ->
2122       output_html outputhtml
2123        ("<h1 color=\"red\">No term selected</h1>")
2124 ;;
2125
2126
2127 let intros = call_tactic ProofEngine.intros;;
2128 let exact = call_tactic_with_input ProofEngine.exact;;
2129 let apply = call_tactic_with_input ProofEngine.apply;;
2130 let elimintrossimpl = call_tactic_with_input ProofEngine.elim_intros_simpl;;
2131 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2132 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2133 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2134 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2135 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2136 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2137 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2138 let cut = call_tactic_with_input ProofEngine.cut;;
2139 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2140 let letin = call_tactic_with_input ProofEngine.letin;;
2141 let ring = call_tactic ProofEngine.ring;;
2142 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2143 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2144 let fourier = call_tactic ProofEngine.fourier;;
2145 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2146 let rewritebacksimpl = call_tactic_with_input ProofEngine.rewrite_back_simpl;;
2147 let replace = call_tactic_with_input_and_goal_input ProofEngine.replace;;
2148 let reflexivity = call_tactic ProofEngine.reflexivity;;
2149 let symmetry = call_tactic ProofEngine.symmetry;;
2150 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2151 let exists = call_tactic ProofEngine.exists;;
2152 let split = call_tactic ProofEngine.split;;
2153 let left = call_tactic ProofEngine.left;;
2154 let right = call_tactic ProofEngine.right;;
2155 let assumption = call_tactic ProofEngine.assumption;;
2156 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2157 let absurd = call_tactic_with_input ProofEngine.absurd;;
2158 let contradiction = call_tactic ProofEngine.contradiction;;
2159 let decompose = call_tactic_with_input ProofEngine.decompose;;
2160
2161 let whd_in_scratch scratch_window =
2162  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2163   scratch_window
2164 ;;
2165 let reduce_in_scratch scratch_window =
2166  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2167   scratch_window
2168 ;;
2169 let simpl_in_scratch scratch_window =
2170  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2171   scratch_window
2172 ;;
2173
2174
2175
2176 (**********************)
2177 (*   END OF TACTICS   *)
2178 (**********************)
2179
2180
2181 let show () =
2182  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2183   try
2184    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2185   with
2186    e ->
2187     output_html outputhtml
2188      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2189 ;;
2190
2191 exception NotADefinition;;
2192
2193 let open_ () =
2194  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2195  let output = ((rendering_window ())#output : GMathViewAux.single_selection_math_view) in
2196  let notebook = (rendering_window ())#notebook in
2197    try
2198     let uri = input_or_locate_uri ~title:"Open" in
2199      CicTypeChecker.typecheck uri ;
2200      let metasenv,bo,ty =
2201       match CicEnvironment.get_cooked_obj uri with
2202          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2203        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2204        | Cic.Constant _
2205        | Cic.Variable _
2206        | Cic.InductiveDefinition _ -> raise NotADefinition
2207      in
2208       ProofEngine.proof :=
2209        Some (uri, metasenv, bo, ty) ;
2210       ProofEngine.goal := None ;
2211       refresh_sequent notebook ;
2212       refresh_proof output
2213    with
2214       RefreshSequentException e ->
2215        output_html outputhtml
2216         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2217          "sequent: " ^ Printexc.to_string e ^ "</h1>")
2218     | RefreshProofException e ->
2219        output_html outputhtml
2220         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2221          "proof: " ^ Printexc.to_string e ^ "</h1>")
2222     | e ->
2223        output_html outputhtml
2224         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2225 ;;
2226
2227 let show_query_results results =
2228  let window =
2229   GWindow.window
2230    ~modal:false ~title:"Query results." ~border_width:2 () in
2231  let vbox = GPack.vbox ~packing:window#add () in
2232  let hbox =
2233   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2234  let lMessage =
2235   GMisc.label
2236    ~text:"Click on a URI to show that object"
2237    ~packing:hbox#add () in
2238  let scrolled_window =
2239   GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2240    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2241  let clist = GList.clist ~columns:1 ~packing:scrolled_window#add () in
2242   ignore
2243    (List.map
2244      (function (uri,_) ->
2245        let n =
2246         clist#append [uri]
2247        in
2248         clist#set_row ~selectable:false n
2249      ) results
2250    ) ;
2251   clist#columns_autosize () ;
2252   ignore
2253    (clist#connect#select_row
2254      (fun ~row ~column ~event ->
2255        let (uristr,_) = List.nth results row in
2256         match
2257          Disambiguate.cic_textual_parser_uri_of_string
2258           (Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format'
2259             uristr)
2260         with
2261            CicTextualParser0.ConUri uri
2262          | CicTextualParser0.VarUri uri
2263          | CicTextualParser0.IndTyUri (uri,_)
2264          | CicTextualParser0.IndConUri (uri,_,_) ->
2265             show_in_show_window_uri uri
2266      )
2267    ) ;
2268   window#show ()
2269 ;;
2270
2271 let refine_constraints (must_obj,must_rel,must_sort) =
2272  let chosen = ref false in
2273  let use_only = ref false in
2274  let window =
2275   GWindow.window
2276    ~modal:true ~title:"Constraints refinement."
2277    ~width:800 ~border_width:2 () in
2278  let vbox = GPack.vbox ~packing:window#add () in
2279  let hbox =
2280   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2281  let lMessage =
2282   GMisc.label
2283    ~text: "\"Only\" constraints can be enforced or not."
2284    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2285  let onlyb =
2286   GButton.toggle_button ~label:"Enforce \"only\" constraints"
2287    ~active:false ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2288  in
2289   ignore
2290    (onlyb#connect#toggled (function () -> use_only := onlyb#active)) ;
2291  (* Notebook for the constraints choice *)
2292  let notebook =
2293   GPack.notebook ~scrollable:true
2294    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2295  (* Rel constraints *)
2296  let label =
2297   GMisc.label
2298    ~text: "Constraints on Rels" () in
2299  let vbox' =
2300   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2301    () in
2302  let hbox =
2303   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2304  let lMessage =
2305   GMisc.label
2306    ~text: "You can now specify the constraints on Rels."
2307    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2308  let expected_height = 25 * (List.length must_rel + 2) in
2309  let height = if expected_height > 400 then 400 else expected_height in
2310  let scrolled_window =
2311   GBin.scrolled_window ~border_width:10 ~height ~width:600
2312    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2313  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2314  let rel_constraints =
2315   List.map
2316    (function (position,depth) ->
2317      let hbox =
2318       GPack.hbox
2319        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2320      let lMessage =
2321       GMisc.label
2322        ~text:position
2323        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2324      match depth with
2325         None -> position, ref None
2326       | Some depth' ->
2327          let mutable_ref = ref (Some depth') in
2328          let depthb =
2329           GButton.toggle_button
2330            ~label:("depth = " ^ string_of_int depth') ~active:true
2331            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2332          in
2333           ignore
2334            (depthb#connect#toggled
2335              (function () ->
2336                let sel_depth = if depthb#active then Some depth' else None in
2337                 mutable_ref := sel_depth
2338             )) ;
2339           position, mutable_ref
2340    ) must_rel in
2341  (* Sort constraints *)
2342  let label =
2343   GMisc.label
2344    ~text: "Constraints on Sorts" () in
2345  let vbox' =
2346   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2347    () in
2348  let hbox =
2349   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2350  let lMessage =
2351   GMisc.label
2352    ~text: "You can now specify the constraints on Sorts."
2353    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2354  let expected_height = 25 * (List.length must_sort + 2) in
2355  let height = if expected_height > 400 then 400 else expected_height in
2356  let scrolled_window =
2357   GBin.scrolled_window ~border_width:10 ~height ~width:600
2358    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2359  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2360  let sort_constraints =
2361   List.map
2362    (function (position,depth,sort) ->
2363      let hbox =
2364       GPack.hbox
2365        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2366      let lMessage =
2367       GMisc.label
2368        ~text:(sort ^ " " ^ position)
2369        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2370      match depth with
2371         None -> position, ref None, sort
2372       | Some depth' ->
2373          let mutable_ref = ref (Some depth') in
2374          let depthb =
2375           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2376            ~active:true
2377            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2378          in
2379           ignore
2380            (depthb#connect#toggled
2381              (function () ->
2382                let sel_depth = if depthb#active then Some depth' else None in
2383                 mutable_ref := sel_depth
2384             )) ;
2385           position, mutable_ref, sort
2386    ) must_sort in
2387  (* Obj constraints *)
2388  let label =
2389   GMisc.label
2390    ~text: "Constraints on constants" () in
2391  let vbox' =
2392   GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce)
2393    () in
2394  let hbox =
2395   GPack.hbox ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2396  let lMessage =
2397   GMisc.label
2398    ~text: "You can now specify the constraints on constants."
2399    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2400  let expected_height = 25 * (List.length must_obj + 2) in
2401  let height = if expected_height > 400 then 400 else expected_height in
2402  let scrolled_window =
2403   GBin.scrolled_window ~border_width:10 ~height ~width:600
2404    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
2405  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
2406  let obj_constraints =
2407   List.map
2408    (function (uri,position,depth) ->
2409      let hbox =
2410       GPack.hbox
2411        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
2412      let lMessage =
2413       GMisc.label
2414        ~text:(uri ^ " " ^ position)
2415        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2416      match depth with
2417         None -> uri, position, ref None
2418       | Some depth' ->
2419          let mutable_ref = ref (Some depth') in
2420          let depthb =
2421           GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
2422            ~active:true
2423            ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2424          in
2425           ignore
2426            (depthb#connect#toggled
2427              (function () ->
2428                let sel_depth = if depthb#active then Some depth' else None in
2429                 mutable_ref := sel_depth
2430             )) ;
2431           uri, position, mutable_ref
2432    ) must_obj in
2433  (* Confirm/abort buttons *)
2434  let hbox =
2435   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2436  let okb =
2437   GButton.button ~label:"Ok"
2438    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2439  let cancelb =
2440   GButton.button ~label:"Abort"
2441    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
2442  in
2443   ignore (window#connect#destroy GMain.Main.quit) ;
2444   ignore (cancelb#connect#clicked window#destroy) ;
2445   ignore
2446    (okb#connect#clicked (function () -> chosen := true ; window#destroy ()));
2447   window#set_position `CENTER ;
2448   window#show () ;
2449   GMain.Main.main () ;
2450   if !chosen then
2451    let chosen_must_rel =
2452     List.map
2453      (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
2454    let chosen_must_sort =
2455     List.map
2456      (function (position,ref_depth,sort) -> position,!ref_depth,sort)
2457      sort_constraints
2458    in
2459    let chosen_must_obj =
2460     List.map
2461      (function (uri,position,ref_depth) -> uri,position,!ref_depth)
2462      obj_constraints
2463    in
2464     (chosen_must_obj,chosen_must_rel,chosen_must_sort),
2465      (if !use_only then
2466 (*CSC: ???????????????????????? I assume that must and only are the same... *)
2467        Some chosen_must_obj,Some chosen_must_rel,Some chosen_must_sort
2468       else
2469        None,None,None
2470      )
2471   else
2472    raise NoChoice
2473 ;;
2474
2475 let completeSearchPattern () =
2476  let inputt = ((rendering_window ())#inputt : term_editor) in
2477  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2478   try
2479    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
2480    let must = MQueryLevels2.get_constraints expr in
2481    let must',only = refine_constraints must in
2482    let results = MQueryGenerator.searchPattern must' only in
2483     show_query_results results
2484   with
2485    e ->
2486     output_html outputhtml
2487      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2488 ;;
2489
2490 let insertQuery () =
2491  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2492   try
2493    let chosen = ref None in
2494    let window =
2495     GWindow.window
2496      ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
2497    let vbox = GPack.vbox ~packing:window#add () in
2498    let label =
2499     GMisc.label ~text:"Insert Query. For Experts Only."
2500      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2501    let scrolled_window =
2502     GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
2503      ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2504    let input = GEdit.text ~editable:true
2505     ~packing:scrolled_window#add () in
2506    let hbox =
2507     GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2508    let okb =
2509     GButton.button ~label:"Ok"
2510      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2511    let loadb =
2512     GButton.button ~label:"Load from file..."
2513      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2514    let cancelb =
2515     GButton.button ~label:"Abort"
2516      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2517    ignore (window#connect#destroy GMain.Main.quit) ;
2518    ignore (cancelb#connect#clicked window#destroy) ;
2519    ignore
2520     (okb#connect#clicked
2521       (function () ->
2522         chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
2523    ignore
2524     (loadb#connect#clicked
2525       (function () ->
2526         match
2527          GToolbox.select_file ~title:"Select Query File" ()
2528         with
2529            None -> ()
2530          | Some filename ->
2531             let inch = open_in filename in
2532              let rec read_file () =
2533               try
2534                let line = input_line inch in
2535                 line ^ "\n" ^ read_file ()
2536               with
2537                End_of_file -> ""
2538              in
2539               let text = read_file () in
2540                input#delete_text 0 input#length ;
2541                ignore (input#insert_text text ~pos:0))) ;
2542    window#set_position `CENTER ;
2543    window#show () ;
2544    GMain.Main.main () ;
2545    match !chosen with
2546       None -> ()
2547     | Some q ->
2548        let results =
2549         Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
2550        in
2551         show_query_results results
2552   with
2553    e ->
2554     output_html outputhtml
2555      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2556 ;;
2557
2558 let choose_must list_of_must only =
2559  let chosen = ref None in
2560  let user_constraints = ref [] in
2561  let window =
2562   GWindow.window
2563    ~modal:true ~title:"Query refinement." ~border_width:2 () in
2564  let vbox = GPack.vbox ~packing:window#add () in
2565  let hbox =
2566   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2567  let lMessage =
2568   GMisc.label
2569    ~text:
2570     ("You can now specify the genericity of the query. " ^
2571      "The more generic the slower.")
2572    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2573  let hbox =
2574   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2575  let lMessage =
2576   GMisc.label
2577    ~text:
2578     "Suggestion: start with faster queries before moving to more generic ones."
2579    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2580  let notebook =
2581   GPack.notebook ~scrollable:true
2582    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2583  let _ =
2584   let page = ref 0 in
2585   let last = List.length list_of_must in
2586   List.map
2587    (function must ->
2588      incr page ;
2589      let label =
2590       GMisc.label ~text:
2591        (if !page = 1 then "More generic" else
2592          if !page = last then "More precise" else "          ") () in
2593      let expected_height = 25 * (List.length must + 2) in
2594      let height = if expected_height > 400 then 400 else expected_height in
2595      let scrolled_window =
2596       GBin.scrolled_window ~border_width:10 ~height ~width:600
2597        ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2598      let clist =
2599         GList.clist ~columns:2 ~packing:scrolled_window#add
2600          ~titles:["URI" ; "Position"] ()
2601      in
2602       ignore
2603        (List.map
2604          (function (uri,position) ->
2605            let n =
2606             clist#append
2607              [uri; if position then "MainConclusion" else "Conclusion"]
2608            in
2609             clist#set_row ~selectable:false n
2610          ) must
2611        ) ;
2612       clist#columns_autosize ()
2613    ) list_of_must in
2614  let _ =
2615   let label = GMisc.label ~text:"User provided" () in
2616   let vbox =
2617    GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2618   let hbox =
2619    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2620   let lMessage =
2621    GMisc.label
2622    ~text:"Select the constraints that must be satisfied and press OK."
2623    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2624   let expected_height = 25 * (List.length only + 2) in
2625   let height = if expected_height > 400 then 400 else expected_height in
2626   let scrolled_window =
2627    GBin.scrolled_window ~border_width:10 ~height ~width:600
2628     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2629   let clist =
2630    GList.clist ~columns:2 ~packing:scrolled_window#add
2631     ~selection_mode:`EXTENDED
2632     ~titles:["URI" ; "Position"] ()
2633   in
2634    ignore
2635     (List.map
2636       (function (uri,position) ->
2637         let n =
2638          clist#append
2639           [uri; if position then "MainConclusion" else "Conclusion"]
2640         in
2641          clist#set_row ~selectable:true n
2642       ) only
2643     ) ;
2644    clist#columns_autosize () ;
2645    ignore
2646     (clist#connect#select_row
2647       (fun ~row ~column ~event ->
2648         user_constraints := (List.nth only row)::!user_constraints)) ;
2649    ignore
2650     (clist#connect#unselect_row
2651       (fun ~row ~column ~event ->
2652         user_constraints :=
2653          List.filter
2654           (function uri -> uri != (List.nth only row)) !user_constraints)) ;
2655  in
2656  let hbox =
2657   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2658  let okb =
2659   GButton.button ~label:"Ok"
2660    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2661  let cancelb =
2662   GButton.button ~label:"Abort"
2663    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2664  (* actions *)
2665  ignore (window#connect#destroy GMain.Main.quit) ;
2666  ignore (cancelb#connect#clicked window#destroy) ;
2667  ignore
2668   (okb#connect#clicked
2669     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2670  window#set_position `CENTER ;
2671  window#show () ;
2672  GMain.Main.main () ;
2673  match !chosen with
2674     None -> raise NoChoice
2675   | Some n ->
2676      if n = List.length list_of_must then
2677       (* user provided constraints *)
2678       !user_constraints
2679      else
2680       List.nth list_of_must n
2681 ;;
2682
2683 let searchPattern () =
2684  let inputt = ((rendering_window ())#inputt : term_editor) in
2685  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2686   try
2687     let metasenv =
2688      match !ProofEngine.proof with
2689         None -> assert false
2690       | Some (_,metasenv,_,_) -> metasenv
2691     in
2692      match !ProofEngine.goal with
2693         None -> ()
2694       | Some metano ->
2695          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2696           let list_of_must,only = MQueryLevels.out_restr metasenv ey ty in
2697           let must = choose_must list_of_must only in
2698           let torigth_restriction (u,b) =
2699            let p =
2700             if b then
2701              "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2702             else
2703              "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion"
2704            in
2705             (u,p,None)
2706           in
2707           let rigth_must = List.map torigth_restriction must in
2708           let rigth_only = Some (List.map torigth_restriction only) in
2709           let result =
2710            MQueryGenerator.searchPattern
2711             (rigth_must,[],[]) (rigth_only,None,None) in
2712           let uris =
2713            List.map
2714             (function uri,_ ->
2715               Disambiguate.wrong_xpointer_format_from_wrong_xpointer_format' uri
2716             ) result in
2717           let html =
2718            " <h1>Backward Query: </h1>" ^
2719            " <pre>" ^ get_last_query result ^ "</pre>"
2720           in
2721            output_html outputhtml html ;
2722            let uris',exc =
2723             let rec filter_out =
2724              function
2725                 [] -> [],""
2726               | uri::tl ->
2727                  let tl',exc = filter_out tl in
2728                   try
2729                    if
2730                     ProofEngine.can_apply
2731                      (term_of_cic_textual_parser_uri
2732                       (Disambiguate.cic_textual_parser_uri_of_string uri))
2733                    then
2734                     uri::tl',exc
2735                    else
2736                     tl',exc
2737                   with
2738                    e ->
2739                     let exc' =
2740                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2741                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2742                     in
2743                      tl',exc'
2744             in
2745              filter_out uris
2746            in
2747             let html' =
2748              " <h1>Objects that can actually be applied: </h1> " ^
2749              String.concat "<br>" uris' ^ exc ^
2750              " <h1>Number of false matches: " ^
2751               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2752              " <h1>Number of good matches: " ^
2753               string_of_int (List.length uris') ^ "</h1>"
2754             in
2755              output_html outputhtml html' ;
2756              let uri' =
2757               user_uri_choice ~title:"Ambiguous input."
2758               ~msg:
2759                 "Many lemmas can be successfully applied. Please, choose one:"
2760                uris'
2761              in
2762               inputt#set_term uri' ;
2763               apply ()
2764   with
2765    e ->
2766     output_html outputhtml
2767      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2768 ;;
2769
2770 let choose_selection
2771      (mmlwidget : GMathViewAux.single_selection_math_view) (element : Gdome.element option)
2772 =
2773  let module G = Gdome in
2774   let rec aux element =
2775    if element#hasAttributeNS
2776        ~namespaceURI:helmns
2777        ~localName:(G.domString "xref")
2778    then
2779      mmlwidget#set_selection (Some element)
2780    else
2781     try
2782       match element#get_parentNode with
2783          None -> assert false
2784        (*CSC: OCAML DIVERGES!
2785        | Some p -> aux (new G.element_of_node p)
2786        *)
2787        | Some p -> aux (new Gdome.element_of_node p)
2788     with
2789        GdomeInit.DOMCastException _ ->
2790         Printf.printf "******* trying to select above the document root ********\n" ; flush stdout
2791
2792   in
2793    match element with
2794      Some x -> aux x
2795    | None   -> mmlwidget#set_selection None
2796 ;;
2797
2798 (* STUFF TO BUILD THE GTK INTERFACE *)
2799
2800 (* Stuff for the widget settings *)
2801
2802 let export_to_postscript (output : GMathViewAux.single_selection_math_view) =
2803  let lastdir = ref (Unix.getcwd ()) in
2804   function () ->
2805    match
2806     GToolbox.select_file ~title:"Export to PostScript"
2807      ~dir:lastdir ~filename:"screenshot.ps" ()
2808    with
2809       None -> ()
2810     | Some filename ->
2811        output#export_to_postscript ~filename:filename ();
2812 ;;
2813
2814 let activate_t1 (output : GMathViewAux.single_selection_math_view) button_set_anti_aliasing
2815  button_set_transparency export_to_postscript_menu_item
2816  button_t1 ()
2817 =
2818  let is_set = button_t1#active in
2819   output#set_font_manager_type
2820    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2821   if is_set then
2822    begin
2823     button_set_anti_aliasing#misc#set_sensitive true ;
2824     button_set_transparency#misc#set_sensitive true ;
2825     export_to_postscript_menu_item#misc#set_sensitive true ;
2826    end
2827   else
2828    begin
2829     button_set_anti_aliasing#misc#set_sensitive false ;
2830     button_set_transparency#misc#set_sensitive false ;
2831     export_to_postscript_menu_item#misc#set_sensitive false ;
2832    end
2833 ;;
2834
2835 let set_anti_aliasing output button_set_anti_aliasing () =
2836  output#set_anti_aliasing button_set_anti_aliasing#active
2837 ;;
2838
2839 let set_transparency output button_set_transparency () =
2840  output#set_transparency button_set_transparency#active
2841 ;;
2842
2843 let changefont output font_size_spinb () =
2844  output#set_font_size font_size_spinb#value_as_int
2845 ;;
2846
2847 let set_log_verbosity output log_verbosity_spinb () =
2848  output#set_log_verbosity log_verbosity_spinb#value_as_int
2849 ;;
2850
2851 class settings_window (output : GMathViewAux.single_selection_math_view) sw
2852  export_to_postscript_menu_item selection_changed_callback
2853 =
2854  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2855  let vbox =
2856   GPack.vbox ~packing:settings_window#add () in
2857  let table =
2858   GPack.table
2859    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2860    ~border_width:5 ~packing:vbox#add () in
2861  let button_t1 =
2862   GButton.toggle_button ~label:"activate t1 fonts"
2863    ~packing:(table#attach ~left:0 ~top:0) () in
2864  let button_set_anti_aliasing =
2865   GButton.toggle_button ~label:"set_anti_aliasing"
2866    ~packing:(table#attach ~left:0 ~top:1) () in
2867  let button_set_transparency =
2868   GButton.toggle_button ~label:"set_transparency"
2869    ~packing:(table#attach ~left:2 ~top:1) () in
2870  let table =
2871   GPack.table
2872    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2873    ~border_width:5 ~packing:vbox#add () in
2874  let font_size_label =
2875   GMisc.label ~text:"font size:"
2876    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2877  let font_size_spinb =
2878   let sadj =
2879    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2880   in
2881    GEdit.spin_button
2882     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2883  let log_verbosity_label =
2884   GMisc.label ~text:"log verbosity:"
2885    ~packing:(table#attach ~left:0 ~top:1) () in
2886  let log_verbosity_spinb =
2887   let sadj =
2888    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2889   in
2890    GEdit.spin_button
2891     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2892  let hbox =
2893   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2894  let closeb =
2895   GButton.button ~label:"Close"
2896    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2897 object(self)
2898  method show = settings_window#show
2899  initializer
2900   button_set_anti_aliasing#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
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_transparency#connect#toggled
2910    (set_transparency output button_set_transparency)) ;
2911   ignore(log_verbosity_spinb#connect#changed
2912    (set_log_verbosity output log_verbosity_spinb)) ;
2913   ignore(closeb#connect#clicked settings_window#misc#hide)
2914 end;;
2915
2916 (* Scratch window *)
2917
2918 class scratch_window =
2919  let window =
2920   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2921  let vbox =
2922   GPack.vbox ~packing:window#add () in
2923  let hbox =
2924   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2925  let whdb =
2926   GButton.button ~label:"Whd"
2927    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2928  let reduceb =
2929   GButton.button ~label:"Reduce"
2930    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2931  let simplb =
2932   GButton.button ~label:"Simpl"
2933    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2934  let scrolled_window =
2935   GBin.scrolled_window ~border_width:10
2936    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2937  let mmlwidget =
2938   GMathViewAux.single_selection_math_view
2939    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2940 object(self)
2941  method mmlwidget = mmlwidget
2942  method show () = window#misc#hide () ; window#show ()
2943  initializer
2944   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2945   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2946   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2947   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2948   ignore(simplb#connect#clicked (simpl_in_scratch self))
2949 end;;
2950
2951 class page () =
2952  let vbox1 = GPack.vbox () in
2953 object(self)
2954  val mutable proofw_ref = None
2955  val mutable compute_ref = None
2956  method proofw =
2957   Lazy.force self#compute ;
2958   match proofw_ref with
2959      None -> assert false
2960    | Some proofw -> proofw
2961  method content = vbox1
2962  method compute =
2963   match compute_ref with
2964      None -> assert false
2965    | Some compute -> compute
2966  initializer
2967   compute_ref <-
2968    Some (lazy (
2969    let scrolled_window1 =
2970     GBin.scrolled_window ~border_width:10
2971      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2972    let proofw =
2973     GMathViewAux.single_selection_math_view ~width:400 ~height:275
2974      ~packing:(scrolled_window1#add) () in
2975    let _ = proofw_ref <- Some proofw in
2976    let hbox3 =
2977     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2978    let exactb =
2979     GButton.button ~label:"Exact"
2980      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2981    let introsb =
2982     GButton.button ~label:"Intros"
2983      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2984    let applyb =
2985     GButton.button ~label:"Apply"
2986      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2987    let elimintrossimplb =
2988     GButton.button ~label:"ElimIntrosSimpl"
2989      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2990    let elimtypeb =
2991     GButton.button ~label:"ElimType"
2992      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2993    let whdb =
2994     GButton.button ~label:"Whd"
2995      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2996    let reduceb =
2997     GButton.button ~label:"Reduce"
2998      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2999    let simplb =
3000     GButton.button ~label:"Simpl"
3001      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
3002    let hbox4 =
3003     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3004    let foldwhdb =
3005     GButton.button ~label:"Fold_whd"
3006      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3007    let foldreduceb =
3008     GButton.button ~label:"Fold_reduce"
3009      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3010    let foldsimplb =
3011     GButton.button ~label:"Fold_simpl"
3012      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3013    let cutb =
3014     GButton.button ~label:"Cut"
3015      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3016    let changeb =
3017     GButton.button ~label:"Change"
3018      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3019    let letinb =
3020     GButton.button ~label:"Let ... In"
3021      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3022    let ringb =
3023     GButton.button ~label:"Ring"
3024      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
3025    let hbox5 =
3026     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3027    let clearbodyb =
3028     GButton.button ~label:"ClearBody"
3029      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3030    let clearb =
3031     GButton.button ~label:"Clear"
3032      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3033    let fourierb =
3034     GButton.button ~label:"Fourier"
3035      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3036    let rewritesimplb =
3037     GButton.button ~label:"RewriteSimpl ->"
3038      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3039    let rewritebacksimplb =
3040     GButton.button ~label:"RewriteSimpl <-"
3041      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3042    let replaceb =
3043     GButton.button ~label:"Replace"
3044      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
3045    let hbox6 =
3046     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3047    let reflexivityb =
3048     GButton.button ~label:"Reflexivity"
3049      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3050    let symmetryb =
3051     GButton.button ~label:"Symmetry"
3052      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3053    let transitivityb =
3054     GButton.button ~label:"Transitivity"
3055      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3056    let existsb =
3057     GButton.button ~label:"Exists"
3058      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3059    let splitb =
3060     GButton.button ~label:"Split"
3061      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3062    let leftb =
3063     GButton.button ~label:"Left"
3064      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3065    let rightb =
3066     GButton.button ~label:"Right"
3067      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3068    let assumptionb =
3069     GButton.button ~label:"Assumption"
3070      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
3071    let hbox7 =
3072     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
3073    let generalizeb =
3074     GButton.button ~label:"Generalize"
3075      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3076    let absurdb =
3077     GButton.button ~label:"Absurd"
3078      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3079    let contradictionb =
3080     GButton.button ~label:"Contradiction"
3081      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3082    let searchpatternb =
3083     GButton.button ~label:"SearchPattern_Apply"
3084      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3085    let decomposeb =
3086     GButton.button ~label:"Decompose"
3087      ~packing:(hbox7#pack ~expand:false ~fill:false ~padding:5) () in
3088
3089    ignore(exactb#connect#clicked exact) ;
3090    ignore(applyb#connect#clicked apply) ;
3091    ignore(elimintrossimplb#connect#clicked elimintrossimpl) ;
3092    ignore(elimtypeb#connect#clicked elimtype) ;
3093    ignore(whdb#connect#clicked whd) ;
3094    ignore(reduceb#connect#clicked reduce) ;
3095    ignore(simplb#connect#clicked simpl) ;
3096    ignore(foldwhdb#connect#clicked fold_whd) ;
3097    ignore(foldreduceb#connect#clicked fold_reduce) ;
3098    ignore(foldsimplb#connect#clicked fold_simpl) ;
3099    ignore(cutb#connect#clicked cut) ;
3100    ignore(changeb#connect#clicked change) ;
3101    ignore(letinb#connect#clicked letin) ;
3102    ignore(ringb#connect#clicked ring) ;
3103    ignore(clearbodyb#connect#clicked clearbody) ;
3104    ignore(clearb#connect#clicked clear) ;
3105    ignore(fourierb#connect#clicked fourier) ;
3106    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
3107    ignore(rewritebacksimplb#connect#clicked rewritebacksimpl) ;
3108    ignore(replaceb#connect#clicked replace) ;
3109    ignore(reflexivityb#connect#clicked reflexivity) ;
3110    ignore(symmetryb#connect#clicked symmetry) ;
3111    ignore(transitivityb#connect#clicked transitivity) ;
3112    ignore(existsb#connect#clicked exists) ;
3113    ignore(splitb#connect#clicked split) ;
3114    ignore(leftb#connect#clicked left) ;
3115    ignore(rightb#connect#clicked right) ;
3116    ignore(assumptionb#connect#clicked assumption) ;
3117    ignore(generalizeb#connect#clicked generalize) ;
3118    ignore(absurdb#connect#clicked absurd) ;
3119    ignore(contradictionb#connect#clicked contradiction) ;
3120    ignore(introsb#connect#clicked intros) ;
3121    ignore(searchpatternb#connect#clicked searchPattern) ;
3122    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
3123    ignore(decomposeb#connect#clicked decompose) ;
3124   ))
3125 end
3126 ;;
3127
3128 class empty_page =
3129  let vbox1 = GPack.vbox () in
3130  let scrolled_window1 =
3131   GBin.scrolled_window ~border_width:10
3132    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
3133  let proofw =
3134   GMathViewAux.single_selection_math_view ~width:400 ~height:275
3135    ~packing:(scrolled_window1#add) () in
3136 object(self)
3137  method proofw = (assert false : GMathViewAux.single_selection_math_view)
3138  method content = vbox1
3139  method compute = (assert false : unit)
3140 end
3141 ;;
3142
3143 let empty_page = new empty_page;;
3144
3145 class notebook =
3146 object(self)
3147  val notebook = GPack.notebook ()
3148  val pages = ref []
3149  val mutable skip_switch_page_event = false
3150  val mutable empty = true
3151  method notebook = notebook
3152  method add_page n =
3153   let new_page = new page () in
3154    empty <- false ;
3155    pages := !pages @ [n,lazy (setgoal n),new_page] ;
3156    notebook#append_page
3157     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
3158     new_page#content#coerce
3159  method remove_all_pages ~skip_switch_page_event:skip =
3160   if empty then
3161    notebook#remove_page 0 (* let's remove the empty page *)
3162   else
3163    List.iter (function _ -> notebook#remove_page 0) !pages ;
3164   pages := [] ;
3165   skip_switch_page_event <- skip
3166  method set_current_page ~may_skip_switch_page_event n =
3167   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
3168    let new_page = notebook#page_num page#content#coerce in
3169     if may_skip_switch_page_event && new_page <> notebook#current_page then
3170      skip_switch_page_event <- true ;
3171     notebook#goto_page new_page
3172  method set_empty_page =
3173   empty <- true ;
3174   pages := [] ;
3175   notebook#append_page
3176    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
3177    empty_page#content#coerce
3178  method proofw =
3179   let (_,_,page) = List.nth !pages notebook#current_page in
3180    page#proofw
3181  initializer
3182   ignore
3183    (notebook#connect#switch_page
3184     (function i ->
3185       let skip = skip_switch_page_event in
3186        skip_switch_page_event <- false ;
3187        if not skip then
3188         try
3189          let (metano,setgoal,page) = List.nth !pages i in
3190           ProofEngine.goal := Some metano ;
3191           Lazy.force (page#compute) ;
3192           Lazy.force setgoal
3193         with _ -> ()
3194     ))
3195 end
3196 ;;
3197
3198 (* Main window *)
3199
3200 class rendering_window output (notebook : notebook) =
3201  let scratch_window = new scratch_window in
3202  let window =
3203   GWindow.window ~title:"MathML viewer" ~border_width:0
3204    ~allow_shrink:false () in
3205  let vbox_for_menu = GPack.vbox ~packing:window#add () in
3206  (* menus *)
3207  let handle_box = GBin.handle_box ~border_width:2
3208   ~packing:(vbox_for_menu#pack ~padding:0) () in
3209  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3210  let factory0 = new GMenu.factory menubar in
3211  let accel_group = factory0#accel_group in
3212  (* file menu *)
3213  let file_menu = factory0#add_submenu "File" in
3214  let factory1 = new GMenu.factory file_menu ~accel_group in
3215  let export_to_postscript_menu_item =
3216   begin
3217    let _ =
3218     factory1#add_item "New Block of (Co)Inductive Definitions..."
3219      ~key:GdkKeysyms._B ~callback:new_inductive
3220    in
3221    let _ =
3222     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3223      ~callback:new_proof
3224    in
3225    let reopen_menu_item =
3226     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3227      ~callback:open_
3228    in
3229    let qed_menu_item =
3230     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3231    ignore (factory1#add_separator ()) ;
3232    ignore
3233     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3234       ~callback:load) ;
3235    let save_menu_item =
3236     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3237    in
3238    ignore
3239     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3240    ignore (!save_set_sensitive false);
3241    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3242    ignore (!qed_set_sensitive false);
3243    ignore (factory1#add_separator ()) ;
3244    let export_to_postscript_menu_item =
3245     factory1#add_item "Export to PostScript..."
3246      ~callback:(export_to_postscript output) in
3247    ignore (factory1#add_separator ()) ;
3248    ignore
3249     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3250    export_to_postscript_menu_item
3251   end in
3252  (* edit menu *)
3253  let edit_menu = factory0#add_submenu "Edit Current Proof" in
3254  let factory2 = new GMenu.factory edit_menu ~accel_group in
3255  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3256  let proveit_menu_item =
3257   factory2#add_item "Prove It" ~key:GdkKeysyms._I
3258    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3259  in
3260  let focus_menu_item =
3261   factory2#add_item "Focus" ~key:GdkKeysyms._F
3262    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3263  in
3264  let _ =
3265   focus_and_proveit_set_sensitive :=
3266    function b ->
3267     proveit_menu_item#misc#set_sensitive b ;
3268     focus_menu_item#misc#set_sensitive b
3269  in
3270  let _ = !focus_and_proveit_set_sensitive false in
3271  (* edit term menu *)
3272  let edit_term_menu = factory0#add_submenu "Edit Term" in
3273  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3274  let check_menu_item =
3275   factory5#add_item "Check Term" ~key:GdkKeysyms._C
3276    ~callback:(check scratch_window) in
3277  let _ = check_menu_item#misc#set_sensitive false in
3278  (* search menu *)
3279  let settings_menu = factory0#add_submenu "Search" in
3280  let factory4 = new GMenu.factory settings_menu ~accel_group in
3281  let _ =
3282   factory4#add_item "Locate..." ~key:GdkKeysyms._T
3283    ~callback:locate in
3284  let searchPattern_menu_item =
3285   factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3286    ~callback:completeSearchPattern in
3287  let _ = searchPattern_menu_item#misc#set_sensitive false in
3288  let show_menu_item =
3289   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3290  in
3291  let insert_query_item =
3292   factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
3293    ~callback:insertQuery in
3294  (* settings menu *)
3295  let settings_menu = factory0#add_submenu "Settings" in
3296  let factory3 = new GMenu.factory settings_menu ~accel_group in
3297  let _ =
3298   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3299    ~callback:edit_aliases in
3300  let _ = factory3#add_separator () in
3301  let _ =
3302   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3303    ~callback:(function _ -> (settings_window ())#show ()) in
3304  (* accel group *)
3305  let _ = window#add_accel_group accel_group in
3306  (* end of menus *)
3307  let hbox0 =
3308   GPack.hbox
3309    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3310  let vbox =
3311   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3312  let scrolled_window0 =
3313   GBin.scrolled_window ~border_width:10
3314    ~packing:(vbox#pack ~expand:true ~padding:5) () in
3315  let _ = scrolled_window0#add output#coerce in
3316  let frame =
3317   GBin.frame ~label:"Insert Term"
3318    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3319  let scrolled_window1 =
3320   GBin.scrolled_window ~border_width:5
3321    ~packing:frame#add () in
3322  let inputt =
3323   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3324    ~isnotempty_callback:
3325     (function b ->
3326       check_menu_item#misc#set_sensitive b ;
3327       searchPattern_menu_item#misc#set_sensitive b) in
3328  let vboxl =
3329   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3330  let _ =
3331   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3332  let frame =
3333   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3334  in
3335  let outputhtml =
3336   GHtml.xmhtml
3337    ~source:"<html><body bgColor=\"white\"></body></html>"
3338    ~width:400 ~height: 100
3339    ~border_width:20
3340    ~packing:frame#add
3341    ~show:true () in
3342 object
3343  method outputhtml = outputhtml
3344  method inputt = inputt
3345  method output = (output : GMathViewAux.single_selection_math_view)
3346  method notebook = notebook
3347  method show = window#show
3348  initializer
3349   notebook#set_empty_page ;
3350   export_to_postscript_menu_item#misc#set_sensitive false ;
3351   check_term := (check_term_in_scratch scratch_window) ;
3352
3353   (* signal handlers here *)
3354   ignore(output#connect#selection_changed
3355    (function elem ->
3356      choose_selection output elem ;
3357      !focus_and_proveit_set_sensitive true
3358    )) ;
3359   ignore (output#connect#click (show_in_show_window_callback output)) ;
3360   let settings_window = new settings_window output scrolled_window0
3361    export_to_postscript_menu_item (choose_selection output) in
3362   set_settings_window settings_window ;
3363   set_outputhtml outputhtml ;
3364   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3365   Logger.log_callback :=
3366    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3367 end;;
3368
3369 (* MAIN *)
3370
3371 let initialize_everything () =
3372  let module U = Unix in
3373   let output = GMathViewAux.single_selection_math_view ~width:350 ~height:280 () in
3374   let notebook = new notebook in
3375    let rendering_window' = new rendering_window output notebook in
3376     set_rendering_window rendering_window' ;
3377     mml_of_cic_term_ref := mml_of_cic_term ;
3378     rendering_window'#show () ;
3379     GMain.Main.main ()
3380 ;;
3381
3382 let _ =
3383  if !usedb then
3384   begin
3385    Mqint.set_database Mqint.postgres_db ;
3386    Mqint.init postgresqlconnectionstring ;
3387   end ;
3388  ignore (GtkMain.Main.init ()) ;
3389  initialize_everything () ;
3390  if !usedb then Mqint.close ();
3391 ;;