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