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
  52 let htmlheader =
  53  "<html>" ^
  54  " <body bgColor=\"white\">"
  55 ;;
  56
  57 let htmlfooter =
  58  " </body>" ^
  59  "</html>"
  60 ;;
  61
  62 (*
  63 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
  64 let prooffile = "/public/sacerdot/currentproof";;
  65 *)
  66
  67 let prooffile = "/public/sacerdot/currentproof";;
  68 let prooffiletype = "/public/sacerdot/currentprooftype";;
  69
  70 (*CSC: the getter should handle the innertypes, not the FS *)
  71 (*
  72 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
  73 let innertypesfile = "/public/sacerdot/innertypes";;
  74 *)
  75
  76 let innertypesfile = "/public/sacerdot/innertypes";;
  77 let constanttypefile = "/public/sacerdot/constanttype";;
  78
  79 let empty_id_to_uris = ([],function _ -> None);;
  80
  81
  82 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  83
  84 let htmlheader_and_content = ref htmlheader;;
  85
  86 let current_cic_infos = ref None;;
  87 let current_goal_infos = ref None;;
  88 let current_scratch_infos = ref None;;
  89
  90 let id_to_uris = ref empty_id_to_uris;;
  91
  92 let check_term = ref (fun _ _ _ -> assert false);;
  93
  94 exception RenderingWindowsNotInitialized;;
  95
  96 let set_rendering_window,rendering_window =
  97  let rendering_window_ref = ref None in
  98   (function rw -> rendering_window_ref := Some rw),
  99   (function () ->
 100     match !rendering_window_ref with
 101        None -> raise RenderingWindowsNotInitialized
 102      | Some rw -> rw
 103   )
 104 ;;
 105
 106 exception SettingsWindowsNotInitialized;;
 107
 108 let set_settings_window,settings_window =
 109  let settings_window_ref = ref None in
 110   (function rw -> settings_window_ref := Some rw),
 111   (function () ->
 112     match !settings_window_ref with
 113        None -> raise SettingsWindowsNotInitialized
 114      | Some rw -> rw
 115   )
 116 ;;
 117
 118 (* COMMAND LINE OPTIONS *)
 119
 120 let usedb = ref true
 121
 122 let argspec =
 123   [
 124     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
 125   ]
 126 in
 127 Arg.parse argspec ignore ""
 128
 129
 130 (* MISC FUNCTIONS *)
 131
 132 let cic_textual_parser_uri_of_string uri' =
 133  (* Constant *)
 134  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
 135   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
 136  else
 137   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
 138    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
 139   else
 140    (try
 141      (* Inductive Type *)
 142      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
 143       CicTextualParser0.IndTyUri (uri'',typeno)
 144     with
 145      _ ->
 146       (* Constructor of an Inductive Type *)
 147       let uri'',typeno,consno =
 148        CicTextualLexer.indconuri_of_uri uri'
 149       in
 150        CicTextualParser0.IndConUri (uri'',typeno,consno)
 151    )
 152 ;;
 153
 154 let term_of_cic_textual_parser_uri uri =
 155  let module C = Cic in
 156  let module CTP = CicTextualParser0 in
 157   match uri with
 158      CTP.ConUri uri -> C.Const (uri,[])
 159    | CTP.VarUri uri -> C.Var (uri,[])
 160    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
 161    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 162 ;;
 163
 164 let string_of_cic_textual_parser_uri uri =
 165  let module C = Cic in
 166  let module CTP = CicTextualParser0 in
 167   let uri' =
 168    match uri with
 169       CTP.ConUri uri -> UriManager.string_of_uri uri
 170     | CTP.VarUri uri -> UriManager.string_of_uri uri
 171     | CTP.IndTyUri (uri,tyno) ->
 172        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
 173     | CTP.IndConUri (uri,tyno,consno) ->
 174        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
 175         string_of_int consno
 176   in
 177    (* 4 = String.length "cic:" *)
 178    String.sub uri' 4 (String.length uri' - 4)
 179 ;;
 180
 181 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 182
 183 exception NoChoice;;
 184
 185 let interactive_user_uri_choice ?(cancel="Cancel") ~title ~msg uris =
 186  let choice = ref None in
 187  let window = GWindow.dialog ~modal:true ~title () in
 188  let lMessage =
 189   GMisc.label ~text:msg ~packing:window#vbox#add () in
 190  let vbox = GPack.vbox ~border_width:10
 191   ~packing:(window#action_area#pack ~expand:true ~padding:4) () in
 192  let hbox1 = GPack.hbox ~border_width:10 ~packing:vbox#add () in
 193  let combo =
 194   GEdit.combo ~popdown_strings:uris ~packing:hbox1#add () in
 195  let checkb =
 196   GButton.button ~label:"Check"
 197    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 198  let hbox = GPack.hbox ~border_width:10 ~packing:vbox#add () in
 199  let okb =
 200   GButton.button ~label:"Ok"
 201    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 202  let cancelb =
 203   GButton.button ~label:cancel
 204    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 205  (* actions *)
 206  let ok_callback () =
 207   choice := Some combo#entry#text ;
 208   window#destroy ()
 209  in
 210  let check_callback () =
 211    !check_term [] []
 212     (term_of_cic_textual_parser_uri
 213      (cic_textual_parser_uri_of_string combo#entry#text))
 214  in
 215   ignore (window#connect#destroy GMain.Main.quit) ;
 216   ignore (cancelb#connect#clicked window#destroy) ;
 217   ignore (okb#connect#clicked ok_callback) ;
 218   ignore (checkb#connect#clicked check_callback) ;
 219   window#set_position `CENTER ;
 220   window#show () ;
 221   GMain.Main.main () ;
 222   match !choice with
 223      None -> raise NoChoice
 224    | Some uri -> uri
 225 ;;
 226
 227 (* MISC FUNCTIONS *)
 228
 229 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
 230 let get_last_query =
 231  let query = ref "" in
 232   MQueryGenerator.set_confirm_query
 233    (function q -> query := MQueryUtil.text_of_query q ; true) ;
 234   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 235 ;;
 236
 237 let register_alias (id,uri) =
 238  let dom,resolve_id = !id_to_uris in
 239   id_to_uris :=
 240    (if List.mem id dom then dom else id::dom),
 241     function id' -> if id' = id then Some uri else resolve_id id'
 242 ;;
 243
 244 let output_html outputhtml msg =
 245  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 246  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 247  outputhtml#set_topline (-1)
 248 ;;
 249
 250 let locate_one_id id =
 251  let result = MQueryGenerator.locate id in
 252  let uris =
 253   List.map
 254    (function uri,_ ->
 255      wrong_xpointer_format_from_wrong_xpointer_format' uri
 256    ) result in
 257  let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
 258   output_html (rendering_window ())#outputhtml html ;
 259   let uris' =
 260    match uris with
 261       [] ->
 262        (match
 263          (GToolbox.input_string ~title:"Unknown input"
 264           ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
 265         with
 266            None -> raise NoChoice
 267          | Some uri -> ["cic:" ^ uri]
 268        )
 269     | [uri] -> [uri]
 270     | _ ->
 271       try
 272        [interactive_user_uri_choice
 273          ~cancel:"Try every possibility."
 274          ~title:"Ambiguous input."
 275          ~msg:
 276            ("Ambiguous input \"" ^ id ^
 277             "\". Please, choose one interpretation:")
 278          uris
 279        ]
 280       with
 281        NoChoice -> uris
 282   in
 283    List.map cic_textual_parser_uri_of_string uris'
 284 ;;
 285
 286 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
 287 exception AmbiguousInput;;
 288
 289 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
 290  let known_ids,resolve_id = !id_to_uris in
 291  let dom' =
 292   let rec filter =
 293    function
 294       [] -> []
 295     | he::tl ->
 296        if List.mem he known_ids then filter tl else he::(filter tl)
 297   in
 298    filter dom
 299  in
 300   (* for each id in dom' we get the list of uris associated to it *)
 301   let list_of_uris = List.map locate_one_id dom' in
 302   (* and now we compute the list of all possible assignments from id to uris *)
 303   let resolve_ids =
 304    let rec aux ids list_of_uris =
 305     match ids,list_of_uris with
 306        [],[] -> [resolve_id]
 307      | id::idtl,uris::uristl ->
 308         let resolves = aux idtl uristl in
 309          List.concat
 310           (List.map
 311             (function uri ->
 312               List.map
 313                (function f ->
 314                  function id' -> if id = id' then Some uri else f id'
 315                ) resolves
 316             ) uris
 317           )
 318      | _,_ -> assert false
 319    in
 320     aux dom' list_of_uris
 321   in
 322 prerr_endline ("##### NE DISAMBIGUO: " ^ string_of_int (List.length resolve_ids)) ;
 323    (* now we select only the ones that generates well-typed terms *)
 324    let resolve_ids' =
 325     let rec filter =
 326      function
 327         [] -> []
 328       | resolve::tl ->
 329          let metasenv',expr = mk_metasenv_and_expr resolve in
 330           try
 331 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
 332            ignore
 333             (CicTypeChecker.type_of_aux' metasenv context expr) ;
 334            resolve::(filter tl)
 335           with
 336            _ -> filter tl
 337     in
 338      filter resolve_ids
 339    in
 340     let resolve_id' =
 341      match resolve_ids' with
 342         [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
 343       | [resolve_id] -> resolve_id
 344       | _ ->
 345         let choices =
 346          List.map
 347           (function resolve ->
 348             String.concat " ; "
 349              (List.map
 350               (function id ->
 351                 id ^ " := " ^
 352                  match resolve id with
 353                     None -> assert false
 354                   | Some uri ->
 355                      match uri with
 356                         CicTextualParser0.ConUri uri
 357                       | CicTextualParser0.VarUri uri ->
 358                          UriManager.string_of_uri uri
 359                       | CicTextualParser0.IndTyUri (uri,tyno) ->
 360                          UriManager.string_of_uri uri ^ "#xpointer(1/" ^
 361                           string_of_int (tyno+1) ^ ")"
 362                       | CicTextualParser0.IndConUri (uri,tyno,consno) ->
 363                          UriManager.string_of_uri uri ^ "#xpointer(1/" ^
 364                           string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
 365               ) dom
 366              )
 367           ) resolve_ids'
 368         in
 369         let choice =
 370          GToolbox.question_box ~title:"Ambiguous input."
 371           ~buttons:choices
 372           ~default:1 "Ambiguous input. Please, choose one interpretation."
 373         in
 374          if choice > 0 then
 375           List.nth resolve_ids' (choice - 1)
 376          else
 377           (* No choice from the user *)
 378           raise NoChoice
 379     in
 380      id_to_uris := known_ids @ dom', resolve_id' ;
 381      mk_metasenv_and_expr resolve_id'
 382 ;;
 383
 384 let domImpl = Gdome.domImplementation ();;
 385
 386 let parseStyle name =
 387  let style =
 388   domImpl#createDocumentFromURI
 389 (*
 390    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 391 *)
 392    ~uri:("styles/" ^ name) ()
 393  in
 394   Gdome_xslt.processStylesheet style
 395 ;;
 396
 397 let d_c = parseStyle "drop_coercions.xsl";;
 398 let tc1 = parseStyle "objtheorycontent.xsl";;
 399 let hc2 = parseStyle "content_to_html.xsl";;
 400 let l   = parseStyle "link.xsl";;
 401
 402 let c1 = parseStyle "rootcontent.xsl";;
 403 let g  = parseStyle "genmmlid.xsl";;
 404 let c2 = parseStyle "annotatedpres.xsl";;
 405
 406
 407 let getterURL = Configuration.getter_url;;
 408 let processorURL = Configuration.processor_url;;
 409
 410 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 411 let mml_args =
 412  ["processorURL", "'" ^ processorURL ^ "'" ;
 413   "getterURL", "'" ^ getterURL ^ "'" ;
 414   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 415   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 416   "UNICODEvsSYMBOL", "'symbol'" ;
 417   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 418   "encoding", "'iso-8859-1'" ;
 419   "media-type", "'text/html'" ;
 420   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 421   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 422   "naturalLanguage", "'yes'" ;
 423   "annotations", "'no'" ;
 424   "explodeall", "'true()'" ;
 425   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 426   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 427 ;;
 428
 429 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 430 let sequent_args =
 431  ["processorURL", "'" ^ processorURL ^ "'" ;
 432   "getterURL", "'" ^ getterURL ^ "'" ;
 433   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 434   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 435   "UNICODEvsSYMBOL", "'symbol'" ;
 436   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 437   "encoding", "'iso-8859-1'" ;
 438   "media-type", "'text/html'" ;
 439   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 440   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 441   "naturalLanguage", "'no'" ;
 442   "annotations", "'no'" ;
 443   "explodeall", "'true()'" ;
 444   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 445   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 446 ;;
 447
 448 let parse_file filename =
 449  let inch = open_in filename in
 450   let rec read_lines () =
 451    try
 452     let line = input_line inch in
 453      line ^ read_lines ()
 454    with
 455     End_of_file -> ""
 456   in
 457    read_lines ()
 458 ;;
 459
 460 let applyStylesheets input styles args =
 461  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 462   input styles
 463 ;;
 464
 465 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 466 (*CSC: ????????????????? *)
 467  let xml, bodyxml =
 468   Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
 469  in
 470  let xmlinnertypes =
 471   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
 472    ~ids_to_inner_types
 473  in
 474   let input =
 475    match bodyxml with
 476       None -> Xml2Gdome.document_of_xml domImpl xml
 477     | Some bodyxml' ->
 478        Xml.pp xml (Some constanttypefile) ;
 479        Xml2Gdome.document_of_xml domImpl bodyxml'
 480   in
 481 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 482 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 483 (*CSC: local.                                                              *)
 484    Xml.pp xmlinnertypes (Some innertypesfile) ;
 485    let output = applyStylesheets input mml_styles mml_args in
 486     output
 487 ;;
 488
 489
 490 (* CALLBACKS *)
 491
 492 exception RefreshSequentException of exn;;
 493 exception RefreshProofException of exn;;
 494
 495 let refresh_proof (output : GMathView.math_view) =
 496  try
 497   let uri,currentproof =
 498    match !ProofEngine.proof with
 499       None -> assert false
 500     | Some (uri,metasenv,bo,ty) ->
 501        (*CSC: Wrong: [] is just plainly wrong *)
 502        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 503   in
 504    let
 505     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 506      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 507    =
 508     Cic2acic.acic_object_of_cic_object currentproof
 509    in
 510     let mml =
 511      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 512     in
 513      output#load_tree mml ;
 514      current_cic_infos :=
 515       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 516  with
 517   e ->
 518  match !ProofEngine.proof with
 519     None -> assert false
 520   | Some (uri,metasenv,bo,ty) ->
 521 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 522    raise (RefreshProofException e)
 523 ;;
 524
 525 let refresh_sequent ?(empty_notebook=true) notebook =
 526  try
 527   match !ProofEngine.goal with
 528      None ->
 529       if empty_notebook then
 530        begin
 531         notebook#remove_all_pages ;
 532         notebook#set_empty_page
 533        end
 534       else
 535        notebook#proofw#unload
 536    | Some metano ->
 537       let metasenv =
 538        match !ProofEngine.proof with
 539           None -> assert false
 540         | Some (_,metasenv,_,_) -> metasenv
 541       in
 542       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 543        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 544         SequentPp.XmlPp.print_sequent metasenv currentsequent
 545        in
 546         let sequent_doc =
 547          Xml2Gdome.document_of_xml domImpl sequent_gdome
 548         in
 549          let sequent_mml =
 550           applyStylesheets sequent_doc sequent_styles sequent_args
 551          in
 552           if empty_notebook then
 553            begin
 554             notebook#remove_all_pages ;
 555             List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
 556            end ;
 557           notebook#set_current_page metano ;
 558           notebook#proofw#load_tree ~dom:sequent_mml ;
 559           current_goal_infos :=
 560            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 561  with
 562   e ->
 563 let metano =
 564   match !ProofEngine.goal with
 565      None -> assert false
 566    | Some m -> m
 567 in
 568 let metasenv =
 569  match !ProofEngine.proof with
 570     None -> assert false
 571   | Some (_,metasenv,_,_) -> metasenv
 572 in
 573 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 574 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 575    raise (RefreshSequentException e)
 576 ;;
 577
 578 (*
 579 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 580  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 581 *)
 582
 583 let mml_of_cic_term metano term =
 584  let metasenv =
 585   match !ProofEngine.proof with
 586      None -> []
 587    | Some (_,metasenv,_,_) -> metasenv
 588  in
 589  let context =
 590   match !ProofEngine.goal with
 591      None -> []
 592    | Some metano ->
 593       let (_,canonical_context,_) =
 594        List.find (function (m,_,_) -> m=metano) metasenv
 595       in
 596        canonical_context
 597  in
 598    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 599     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 600    in
 601     let sequent_doc =
 602      Xml2Gdome.document_of_xml domImpl sequent_gdome
 603     in
 604      let res =
 605       applyStylesheets sequent_doc sequent_styles sequent_args ;
 606      in
 607       current_scratch_infos :=
 608        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 609       res
 610 ;;
 611
 612 (***********************)
 613 (*       TACTICS       *)
 614 (***********************)
 615
 616 let call_tactic tactic () =
 617  let notebook = (rendering_window ())#notebook in
 618  let output = ((rendering_window ())#output : GMathView.math_view) in
 619  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 620  let savedproof = !ProofEngine.proof in
 621  let savedgoal  = !ProofEngine.goal in
 622   begin
 623    try
 624     tactic () ;
 625     refresh_sequent notebook ;
 626     refresh_proof output
 627    with
 628       RefreshSequentException e ->
 629        output_html outputhtml
 630         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 631          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 632        ProofEngine.proof := savedproof ;
 633        ProofEngine.goal := savedgoal ;
 634        refresh_sequent notebook
 635     | RefreshProofException e ->
 636        output_html outputhtml
 637         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 638          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 639        ProofEngine.proof := savedproof ;
 640        ProofEngine.goal := savedgoal ;
 641        refresh_sequent notebook ;
 642        refresh_proof output
 643     | e ->
 644        output_html outputhtml
 645         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 646        ProofEngine.proof := savedproof ;
 647        ProofEngine.goal := savedgoal ;
 648   end
 649 ;;
 650
 651 let call_tactic_with_input tactic () =
 652  let notebook = (rendering_window ())#notebook in
 653  let output = ((rendering_window ())#output : GMathView.math_view) in
 654  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 655  let inputt = ((rendering_window ())#inputt : GEdit.text) in
 656  let savedproof = !ProofEngine.proof in
 657  let savedgoal  = !ProofEngine.goal in
 658 (*CSC: Gran cut&paste da sotto... *)
 659   let inputlen = inputt#length in
 660   let input = inputt#get_chars 0 inputlen ^ "\n" in
 661    let lexbuf = Lexing.from_string input in
 662    let curi =
 663     match !ProofEngine.proof with
 664        None -> assert false
 665      | Some (curi,_,_,_) -> curi
 666    in
 667    let uri,metasenv,bo,ty =
 668     match !ProofEngine.proof with
 669        None -> assert false
 670      | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 671    in
 672    let canonical_context =
 673     match !ProofEngine.goal with
 674        None -> assert false
 675      | Some metano ->
 676         let (_,canonical_context,_) =
 677          List.find (function (m,_,_) -> m=metano) metasenv
 678         in
 679          canonical_context
 680    in
 681    let context =
 682     List.map
 683      (function
 684          Some (n,_) -> Some n
 685        | None -> None
 686      ) canonical_context
 687    in
 688     try
 689      while true do
 690       match
 691        CicTextualParserContext.main context metasenv CicTextualLexer.token
 692         lexbuf register_alias
 693       with
 694          None -> ()
 695        | Some (dom,mk_metasenv_and_expr) ->
 696           let (metasenv',expr) =
 697            disambiguate_input canonical_context metasenv dom
 698             mk_metasenv_and_expr
 699           in
 700            ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 701            tactic expr ;
 702            refresh_sequent notebook ;
 703            refresh_proof output
 704      done
 705     with
 706        CicTextualParser0.Eof ->
 707         inputt#delete_text 0 inputlen
 708      | RefreshSequentException e ->
 709         output_html outputhtml
 710          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 711           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 712         ProofEngine.proof := savedproof ;
 713         ProofEngine.goal := savedgoal ;
 714         refresh_sequent notebook
 715      | RefreshProofException e ->
 716         output_html outputhtml
 717          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 718           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 719         ProofEngine.proof := savedproof ;
 720         ProofEngine.goal := savedgoal ;
 721         refresh_sequent notebook ;
 722         refresh_proof output
 723      | e ->
 724         output_html outputhtml
 725          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 726         ProofEngine.proof := savedproof ;
 727         ProofEngine.goal := savedgoal ;
 728 ;;
 729
 730 let call_tactic_with_goal_input tactic () =
 731  let module L = LogicalOperations in
 732  let module G = Gdome in
 733   let notebook = (rendering_window ())#notebook in
 734   let output = ((rendering_window ())#output : GMathView.math_view) in
 735   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 736   let savedproof = !ProofEngine.proof in
 737   let savedgoal  = !ProofEngine.goal in
 738    match notebook#proofw#get_selection with
 739      Some node ->
 740       let xpath =
 741        ((node : Gdome.element)#getAttributeNS
 742          ~namespaceURI:helmns
 743          ~localName:(G.domString "xref"))#to_string
 744       in
 745        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 746        else
 747         begin
 748          try
 749           match !current_goal_infos with
 750              Some (ids_to_terms, ids_to_father_ids,_) ->
 751               let id = xpath in
 752                tactic (Hashtbl.find ids_to_terms id) ;
 753                refresh_sequent notebook ;
 754                refresh_proof output
 755            | None -> assert false (* "ERROR: No current term!!!" *)
 756          with
 757             RefreshSequentException e ->
 758              output_html outputhtml
 759               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 760                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 761              ProofEngine.proof := savedproof ;
 762              ProofEngine.goal := savedgoal ;
 763              refresh_sequent notebook
 764           | RefreshProofException e ->
 765              output_html outputhtml
 766               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 767                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 768              ProofEngine.proof := savedproof ;
 769              ProofEngine.goal := savedgoal ;
 770              refresh_sequent notebook ;
 771              refresh_proof output
 772           | e ->
 773              output_html outputhtml
 774               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 775              ProofEngine.proof := savedproof ;
 776              ProofEngine.goal := savedgoal ;
 777         end
 778    | None ->
 779       output_html outputhtml
 780        ("<h1 color=\"red\">No term selected</h1>")
 781 ;;
 782
 783 let call_tactic_with_input_and_goal_input tactic () =
 784  let module L = LogicalOperations in
 785  let module G = Gdome in
 786   let notebook = (rendering_window ())#notebook in
 787   let output = ((rendering_window ())#output : GMathView.math_view) in
 788   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 789   let inputt = ((rendering_window ())#inputt : GEdit.text) in
 790   let savedproof = !ProofEngine.proof in
 791   let savedgoal  = !ProofEngine.goal in
 792    match notebook#proofw#get_selection with
 793      Some node ->
 794       let xpath =
 795        ((node : Gdome.element)#getAttributeNS
 796          ~namespaceURI:helmns
 797          ~localName:(G.domString "xref"))#to_string
 798       in
 799        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 800        else
 801         begin
 802          try
 803           match !current_goal_infos with
 804              Some (ids_to_terms, ids_to_father_ids,_) ->
 805               let id = xpath in
 806                (* Let's parse the input *)
 807                let inputlen = inputt#length in
 808                let input = inputt#get_chars 0 inputlen ^ "\n" in
 809                 let lexbuf = Lexing.from_string input in
 810                 let curi =
 811                  match !ProofEngine.proof with
 812                     None -> assert false
 813                   | Some (curi,_,_,_) -> curi
 814                 in
 815                 let uri,metasenv,bo,ty =
 816                  match !ProofEngine.proof with
 817                     None -> assert false
 818                   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 819                 in
 820                 let canonical_context =
 821                  match !ProofEngine.goal with
 822                     None -> assert false
 823                   | Some metano ->
 824                      let (_,canonical_context,_) =
 825                       List.find (function (m,_,_) -> m=metano) metasenv
 826                      in
 827                       canonical_context in
 828                 let context =
 829                  List.map
 830                   (function
 831                       Some (n,_) -> Some n
 832                     | None -> None
 833                   ) canonical_context
 834                 in
 835                  begin
 836                   try
 837                    while true do
 838                     match
 839                      CicTextualParserContext.main context metasenv
 840                       CicTextualLexer.token lexbuf register_alias
 841                     with
 842                        None -> ()
 843                      | Some (dom,mk_metasenv_and_expr) ->
 844                         let (metasenv',expr) =
 845                          disambiguate_input canonical_context metasenv dom
 846                           mk_metasenv_and_expr
 847                         in
 848                          ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 849                          tactic ~goal_input:(Hashtbl.find ids_to_terms id)
 850                           ~input:expr ;
 851                          refresh_sequent notebook ;
 852                          refresh_proof output
 853                    done
 854                   with
 855                      CicTextualParser0.Eof ->
 856                       inputt#delete_text 0 inputlen
 857                  end
 858            | None -> assert false (* "ERROR: No current term!!!" *)
 859          with
 860             RefreshSequentException e ->
 861              output_html outputhtml
 862               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 863                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 864              ProofEngine.proof := savedproof ;
 865              ProofEngine.goal := savedgoal ;
 866              refresh_sequent notebook
 867           | RefreshProofException e ->
 868              output_html outputhtml
 869               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 870                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 871              ProofEngine.proof := savedproof ;
 872              ProofEngine.goal := savedgoal ;
 873              refresh_sequent notebook ;
 874              refresh_proof output
 875           | e ->
 876              output_html outputhtml
 877               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 878              ProofEngine.proof := savedproof ;
 879              ProofEngine.goal := savedgoal ;
 880         end
 881    | None ->
 882       output_html outputhtml
 883        ("<h1 color=\"red\">No term selected</h1>")
 884 ;;
 885
 886 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
 887  let module L = LogicalOperations in
 888  let module G = Gdome in
 889   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
 890   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
 891   let savedproof = !ProofEngine.proof in
 892   let savedgoal  = !ProofEngine.goal in
 893    match mmlwidget#get_selection with
 894      Some node ->
 895       let xpath =
 896        ((node : Gdome.element)#getAttributeNS
 897          ~namespaceURI:helmns
 898          ~localName:(G.domString "xref"))#to_string
 899       in
 900        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 901        else
 902         begin
 903          try
 904           match !current_scratch_infos with
 905              (* term is the whole goal in the scratch_area *)
 906              Some (term,ids_to_terms, ids_to_father_ids,_) ->
 907               let id = xpath in
 908                let expr = tactic term (Hashtbl.find ids_to_terms id) in
 909                 let mml = mml_of_cic_term 111 expr in
 910                  scratch_window#show () ;
 911                  scratch_window#mmlwidget#load_tree ~dom:mml
 912            | None -> assert false (* "ERROR: No current term!!!" *)
 913          with
 914           e ->
 915            output_html outputhtml
 916             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 917         end
 918    | None ->
 919       output_html outputhtml
 920        ("<h1 color=\"red\">No term selected</h1>")
 921 ;;
 922
 923 let call_tactic_with_hypothesis_input tactic () =
 924  let module L = LogicalOperations in
 925  let module G = Gdome in
 926   let notebook = (rendering_window ())#notebook in
 927   let output = ((rendering_window ())#output : GMathView.math_view) in
 928   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 929   let savedproof = !ProofEngine.proof in
 930   let savedgoal  = !ProofEngine.goal in
 931    match notebook#proofw#get_selection with
 932      Some node ->
 933       let xpath =
 934        ((node : Gdome.element)#getAttributeNS
 935          ~namespaceURI:helmns
 936          ~localName:(G.domString "xref"))#to_string
 937       in
 938        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 939        else
 940         begin
 941          try
 942           match !current_goal_infos with
 943              Some (_,_,ids_to_hypotheses) ->
 944               let id = xpath in
 945                tactic (Hashtbl.find ids_to_hypotheses id) ;
 946                refresh_sequent notebook ;
 947                refresh_proof output
 948            | None -> assert false (* "ERROR: No current term!!!" *)
 949          with
 950             RefreshSequentException e ->
 951              output_html outputhtml
 952               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 953                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 954              ProofEngine.proof := savedproof ;
 955              ProofEngine.goal := savedgoal ;
 956              refresh_sequent notebook
 957           | RefreshProofException e ->
 958              output_html outputhtml
 959               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 960                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 961              ProofEngine.proof := savedproof ;
 962              ProofEngine.goal := savedgoal ;
 963              refresh_sequent notebook ;
 964              refresh_proof output
 965           | e ->
 966              output_html outputhtml
 967               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 968              ProofEngine.proof := savedproof ;
 969              ProofEngine.goal := savedgoal ;
 970         end
 971    | None ->
 972       output_html outputhtml
 973        ("<h1 color=\"red\">No term selected</h1>")
 974 ;;
 975
 976
 977 let intros = call_tactic ProofEngine.intros;;
 978 let exact = call_tactic_with_input ProofEngine.exact;;
 979 let apply = call_tactic_with_input ProofEngine.apply;;
 980 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
 981 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
 982 let whd = call_tactic_with_goal_input ProofEngine.whd;;
 983 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
 984 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
 985 let fold = call_tactic_with_input ProofEngine.fold;;
 986 let cut = call_tactic_with_input ProofEngine.cut;;
 987 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
 988 let letin = call_tactic_with_input ProofEngine.letin;;
 989 let ring = call_tactic ProofEngine.ring;;
 990 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
 991 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
 992 let fourier = call_tactic ProofEngine.fourier;;
 993 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
 994 let reflexivity = call_tactic ProofEngine.reflexivity;;
 995 let symmetry = call_tactic ProofEngine.symmetry;;
 996 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
 997 let left = call_tactic ProofEngine.left;;
 998 let right = call_tactic ProofEngine.right;;
 999 let assumption = call_tactic ProofEngine.assumption;;
1000
1001 let whd_in_scratch scratch_window =
1002  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1003   scratch_window
1004 ;;
1005 let reduce_in_scratch scratch_window =
1006  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1007   scratch_window
1008 ;;
1009 let simpl_in_scratch scratch_window =
1010  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1011   scratch_window
1012 ;;
1013
1014
1015
1016 (**********************)
1017 (*   END OF TACTICS   *)
1018 (**********************)
1019
1020 exception OpenConjecturesStillThere;;
1021 exception WrongProof;;
1022
1023 let qed () =
1024  match !ProofEngine.proof with
1025     None -> assert false
1026   | Some (uri,[],bo,ty) ->
1027      if
1028       CicReduction.are_convertible []
1029        (CicTypeChecker.type_of_aux' [] [] bo) ty
1030      then
1031       begin
1032        (*CSC: Wrong: [] is just plainly wrong *)
1033        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
1034         let
1035          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1036           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1037         =
1038          Cic2acic.acic_object_of_cic_object proof
1039         in
1040          let mml =
1041           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
1042          in
1043           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
1044           current_cic_infos :=
1045            Some
1046             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
1047              ids_to_hypotheses)
1048       end
1049      else
1050       raise WrongProof
1051   | _ -> raise OpenConjecturesStillThere
1052 ;;
1053
1054 (*????
1055 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
1056 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
1057 *)
1058 let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
1059
1060 let save () =
1061  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1062   match !ProofEngine.proof with
1063      None -> assert false
1064    | Some (uri, metasenv, bo, ty) ->
1065       let currentproof =
1066        (*CSC: Wrong: [] is just plainly wrong *)
1067        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
1068       in
1069        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
1070         Cic2acic.acic_object_of_cic_object currentproof
1071        in
1072         let xml, bodyxml =
1073          match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
1074             xml,Some bodyxml -> xml,bodyxml
1075           | _,None -> assert false
1076         in
1077          Xml.pp ~quiet:true xml (Some prooffiletype) ;
1078          output_html outputhtml
1079           ("<h1 color=\"Green\">Current proof type saved to " ^
1080            prooffiletype ^ "</h1>") ;
1081          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
1082          output_html outputhtml
1083           ("<h1 color=\"Green\">Current proof body saved to " ^
1084            prooffile ^ "</h1>")
1085 ;;
1086
1087 (* Used to typecheck the loaded proofs *)
1088 let typecheck_loaded_proof metasenv bo ty =
1089  let module T = CicTypeChecker in
1090   ignore (
1091    List.fold_left
1092     (fun metasenv ((_,context,ty) as conj) ->
1093       ignore (T.type_of_aux' metasenv context ty) ;
1094       metasenv @ [conj]
1095     ) [] metasenv) ;
1096   ignore (T.type_of_aux' metasenv [] ty) ;
1097   ignore (T.type_of_aux' metasenv [] bo)
1098 ;;
1099
1100 let load () =
1101  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1102  let output = ((rendering_window ())#output : GMathView.math_view) in
1103  let notebook = (rendering_window ())#notebook in
1104   try
1105    let uri = UriManager.uri_of_string "cic:/dummy.con" in
1106     match CicParser.obj_of_xml prooffiletype (Some prooffile) with
1107        Cic.CurrentProof (_,metasenv,bo,ty,_) ->
1108         typecheck_loaded_proof metasenv bo ty ;
1109         ProofEngine.proof :=
1110          Some (uri, metasenv, bo, ty) ;
1111         ProofEngine.goal :=
1112          (match metasenv with
1113              [] -> None
1114            | (metano,_,_)::_ -> Some metano
1115          ) ;
1116         refresh_proof output ;
1117         refresh_sequent notebook ;
1118          output_html outputhtml
1119           ("<h1 color=\"Green\">Current proof type loaded from " ^
1120             prooffiletype ^ "</h1>") ;
1121          output_html outputhtml
1122           ("<h1 color=\"Green\">Current proof body loaded from " ^
1123             prooffile ^ "</h1>")
1124      | _ -> assert false
1125   with
1126      RefreshSequentException e ->
1127       output_html outputhtml
1128        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1129         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1130    | RefreshProofException e ->
1131       output_html outputhtml
1132        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1133         "proof: " ^ Printexc.to_string e ^ "</h1>")
1134    | e ->
1135       output_html outputhtml
1136        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1137 ;;
1138
1139 let edit_aliases () =
1140  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1141  let dom,resolve_id = !id_to_uris in
1142   let inputlen = inputt#length in
1143    inputt#delete_text 0 inputlen ;
1144    let _ =
1145     inputt#insert_text ~pos:0
1146      (String.concat "\n"
1147        (List.map
1148          (function v ->
1149            let uri =
1150             match resolve_id v with
1151                None -> assert false
1152              | Some uri -> uri
1153            in
1154             "alias " ^ v ^ " " ^
1155               (string_of_cic_textual_parser_uri uri)
1156          ) dom))
1157    in
1158     id_to_uris := empty_id_to_uris
1159 ;;
1160
1161 let proveit () =
1162  let module L = LogicalOperations in
1163  let module G = Gdome in
1164  let notebook = (rendering_window ())#notebook in
1165  let output = (rendering_window ())#output in
1166  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1167   match (rendering_window ())#output#get_selection with
1168     Some node ->
1169      let xpath =
1170       ((node : Gdome.element)#getAttributeNS
1171       (*CSC: OCAML DIVERGE
1172       ((element : G.element)#getAttributeNS
1173       *)
1174         ~namespaceURI:helmns
1175         ~localName:(G.domString "xref"))#to_string
1176      in
1177       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1178       else
1179        begin
1180         try
1181          match !current_cic_infos with
1182             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1183              let id = xpath in
1184               L.to_sequent id ids_to_terms ids_to_father_ids ;
1185               refresh_proof output ;
1186               refresh_sequent notebook
1187           | None -> assert false (* "ERROR: No current term!!!" *)
1188         with
1189            RefreshSequentException e ->
1190             output_html outputhtml
1191              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1192               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1193          | RefreshProofException e ->
1194             output_html outputhtml
1195              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1196               "proof: " ^ Printexc.to_string e ^ "</h1>")
1197          | e ->
1198             output_html outputhtml
1199              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1200        end
1201   | None -> assert false (* "ERROR: No selection!!!" *)
1202 ;;
1203
1204 let focus () =
1205  let module L = LogicalOperations in
1206  let module G = Gdome in
1207  let notebook = (rendering_window ())#notebook in
1208  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1209   match (rendering_window ())#output#get_selection with
1210     Some node ->
1211      let xpath =
1212       ((node : Gdome.element)#getAttributeNS
1213       (*CSC: OCAML DIVERGE
1214       ((element : G.element)#getAttributeNS
1215       *)
1216         ~namespaceURI:helmns
1217         ~localName:(G.domString "xref"))#to_string
1218      in
1219       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1220       else
1221        begin
1222         try
1223          match !current_cic_infos with
1224             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1225              let id = xpath in
1226               L.focus id ids_to_terms ids_to_father_ids ;
1227               refresh_sequent notebook
1228           | None -> assert false (* "ERROR: No current term!!!" *)
1229         with
1230            RefreshSequentException e ->
1231             output_html outputhtml
1232              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1233               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1234          | RefreshProofException e ->
1235             output_html outputhtml
1236              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1237               "proof: " ^ Printexc.to_string e ^ "</h1>")
1238          | e ->
1239             output_html outputhtml
1240              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1241        end
1242   | None -> assert false (* "ERROR: No selection!!!" *)
1243 ;;
1244
1245 exception NoPrevGoal;;
1246 exception NoNextGoal;;
1247
1248 let setgoal metano =
1249  let module L = LogicalOperations in
1250  let module G = Gdome in
1251  let notebook = (rendering_window ())#notebook in
1252  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1253   let metasenv =
1254    match !ProofEngine.proof with
1255       None -> assert false
1256     | Some (_,metasenv,_,_) -> metasenv
1257   in
1258    try
1259     ProofEngine.goal := Some metano ;
1260     refresh_sequent ~empty_notebook:false notebook ;
1261    with
1262       RefreshSequentException e ->
1263        output_html outputhtml
1264         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1265          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1266     | e ->
1267        output_html outputhtml
1268         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1269 ;;
1270
1271 exception NotADefinition;;
1272
1273 let open_ () =
1274  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1275  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1276  let output = ((rendering_window ())#output : GMathView.math_view) in
1277  let notebook = (rendering_window ())#notebook in
1278   let inputlen = inputt#length in
1279   let input = inputt#get_chars 0 inputlen in
1280    try
1281     let uri = UriManager.uri_of_string ("cic:" ^ input) in
1282      CicTypeChecker.typecheck uri ;
1283      let metasenv,bo,ty =
1284       match CicEnvironment.get_cooked_obj uri with
1285          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1286        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1287        | Cic.Constant _
1288        | Cic.Variable _
1289        | Cic.InductiveDefinition _ -> raise NotADefinition
1290      in
1291       ProofEngine.proof :=
1292        Some (uri, metasenv, bo, ty) ;
1293       ProofEngine.goal := None ;
1294       refresh_sequent notebook ;
1295       refresh_proof output ;
1296       inputt#delete_text 0 inputlen
1297    with
1298       RefreshSequentException e ->
1299        output_html outputhtml
1300         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1301          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1302     | RefreshProofException e ->
1303        output_html outputhtml
1304         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1305          "proof: " ^ Printexc.to_string e ^ "</h1>")
1306     | e ->
1307        output_html outputhtml
1308         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1309 ;;
1310
1311 let state () =
1312  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1313  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1314  let output = ((rendering_window ())#output : GMathView.math_view) in
1315  let notebook = (rendering_window ())#notebook in
1316   let inputlen = inputt#length in
1317   let input = inputt#get_chars 0 inputlen ^ "\n" in
1318    (* Do something interesting *)
1319    let lexbuf = Lexing.from_string input in
1320     try
1321      while true do
1322       (* Execute the actions *)
1323       match
1324        CicTextualParserContext.main [] [] CicTextualLexer.token
1325         lexbuf register_alias
1326       with
1327          None -> ()
1328        | Some (dom,mk_metasenv_and_expr) ->
1329           let metasenv,expr =
1330            disambiguate_input [] [] dom mk_metasenv_and_expr
1331           in
1332            let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1333             ProofEngine.proof :=
1334              Some (UriManager.uri_of_string "cic:/dummy.con",
1335                     (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1336             ProofEngine.goal := Some 1 ;
1337             refresh_sequent notebook ;
1338             refresh_proof output ;
1339      done
1340     with
1341        CicTextualParser0.Eof ->
1342         inputt#delete_text 0 inputlen
1343      | RefreshSequentException e ->
1344         output_html outputhtml
1345          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1346           "sequent: " ^ Printexc.to_string e ^ "</h1>")
1347      | RefreshProofException e ->
1348         output_html outputhtml
1349          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1350           "proof: " ^ Printexc.to_string e ^ "</h1>")
1351      | e ->
1352         output_html outputhtml
1353          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1354 ;;
1355
1356 let check_term_in_scratch scratch_window metasenv context expr =
1357  try
1358   let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
1359    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1360 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1361     scratch_window#show () ;
1362     scratch_window#mmlwidget#load_tree ~dom:mml
1363  with
1364   e ->
1365    print_endline ("? " ^ CicPp.ppterm expr) ;
1366    raise e
1367 ;;
1368
1369 let check scratch_window () =
1370  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1371  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1372   let inputlen = inputt#length in
1373   let input = inputt#get_chars 0 inputlen ^ "\n" in
1374   let curi,metasenv =
1375    match !ProofEngine.proof with
1376       None -> UriManager.uri_of_string "cic:/dummy.con", []
1377     | Some (curi,metasenv,_,_) -> curi,metasenv
1378   in
1379   let context,names_context =
1380    let context =
1381     match !ProofEngine.goal with
1382        None -> []
1383      | Some metano ->
1384         let (_,canonical_context,_) =
1385          List.find (function (m,_,_) -> m=metano) metasenv
1386         in
1387          canonical_context
1388    in
1389     context,
1390     List.map
1391      (function
1392          Some (n,_) -> Some n
1393        | None -> None
1394      ) context
1395   in
1396    let lexbuf = Lexing.from_string input in
1397     try
1398      while true do
1399       (* Execute the actions *)
1400       match
1401        CicTextualParserContext.main names_context metasenv CicTextualLexer.token
1402         lexbuf register_alias
1403       with
1404          None -> ()
1405        | Some (dom,mk_metasenv_and_expr) ->
1406           let (metasenv',expr) =
1407            disambiguate_input context metasenv dom mk_metasenv_and_expr
1408           in
1409            check_term_in_scratch scratch_window metasenv' context expr
1410      done
1411     with
1412        CicTextualParser0.Eof -> ()
1413      | e ->
1414        output_html outputhtml
1415         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1416 ;;
1417
1418 exception NoObjectsLocated;;
1419
1420 let user_uri_choice ~title ~msg uris =
1421  let uri =
1422   match uris with
1423      [] -> raise NoObjectsLocated
1424    | [uri] -> uri
1425    | uris ->
1426       interactive_user_uri_choice ~title ~msg uris
1427  in
1428   String.sub uri 4 (String.length uri - 4)
1429 ;;
1430
1431 let locate () =
1432  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1433  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1434   let inputlen = inputt#length in
1435   let input = inputt#get_chars 0 inputlen in
1436    try
1437     match Str.split (Str.regexp "[ \t]+") input with
1438        [] -> ()
1439      | head :: tail ->
1440         inputt#delete_text 0 inputlen ;
1441         let result = MQueryGenerator.locate head in
1442         let uris =
1443          List.map
1444           (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1445           result in
1446         let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1447          output_html outputhtml html ;
1448          let uri' =
1449           user_uri_choice ~title:"Ambiguous input."
1450            ~msg:
1451              ("Ambiguous input \"" ^ head ^
1452               "\". Please, choose one interpetation:")
1453            uris
1454          in
1455           ignore ((inputt#insert_text uri') ~pos:0)
1456    with
1457     e ->
1458      output_html outputhtml
1459       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1460 ;;
1461
1462 let searchPattern () =
1463  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1464  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1465   let inputlen = inputt#length in
1466   let input = inputt#get_chars 0 inputlen in
1467   let level = int_of_string input in
1468   let metasenv =
1469    match !ProofEngine.proof with
1470       None -> assert false
1471     | Some (_,metasenv,_,_) -> metasenv
1472   in
1473    try
1474     match !ProofEngine.goal with
1475        None -> ()
1476      | Some metano ->
1477         let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1478          let result = MQueryGenerator.searchPattern metasenv ey ty level in
1479          let uris =
1480           List.map
1481            (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1482            result in
1483          let html =
1484           " <h1>Backward Query: </h1>" ^
1485           " <h2>Levels: </h2> " ^
1486            MQueryGenerator.string_of_levels
1487             (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1488            " <pre>" ^ get_last_query result ^ "</pre>"
1489          in
1490           output_html outputhtml html ;
1491           let uris',exc =
1492            let rec filter_out =
1493             function
1494                [] -> [],""
1495              | uri::tl ->
1496                 let tl',exc = filter_out tl in
1497                  try
1498                   if
1499                    ProofEngine.can_apply
1500                     (term_of_cic_textual_parser_uri
1501                      (cic_textual_parser_uri_of_string uri))
1502                   then
1503                    uri::tl',exc
1504                   else
1505                    tl',exc
1506                  with
1507                   e ->
1508                    let exc' =
1509                     "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1510                      uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1511                    in
1512                     tl',exc'
1513            in
1514             filter_out uris
1515           in
1516            let html' =
1517             " <h1>Objects that can actually be applied: </h1> " ^
1518             String.concat "<br>" uris' ^ exc ^
1519             " <h1>Number of false matches: " ^
1520              string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1521             " <h1>Number of good matches: " ^
1522              string_of_int (List.length uris') ^ "</h1>"
1523            in
1524             output_html outputhtml html' ;
1525             let uri' =
1526              user_uri_choice ~title:"Ambiguous input."
1527              ~msg:"Many lemmas can be successfully applied. Please, choose one:"
1528               uris'
1529             in
1530              inputt#delete_text 0 inputlen ;
1531              ignore ((inputt#insert_text uri') ~pos:0)
1532     with
1533      e ->
1534       output_html outputhtml
1535        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1536 ;;
1537
1538 let choose_selection
1539      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1540 =
1541  let module G = Gdome in
1542   let rec aux element =
1543    if element#hasAttributeNS
1544        ~namespaceURI:helmns
1545        ~localName:(G.domString "xref")
1546    then
1547      mmlwidget#set_selection (Some element)
1548    else
1549       match element#get_parentNode with
1550          None -> assert false
1551        (*CSC: OCAML DIVERGES!
1552        | Some p -> aux (new G.element_of_node p)
1553        *)
1554        | Some p -> aux (new Gdome.element_of_node p)
1555   in
1556    match element with
1557      Some x -> aux x
1558    | None   -> mmlwidget#set_selection None
1559 ;;
1560
1561 (* STUFF TO BUILD THE GTK INTERFACE *)
1562
1563 (* Stuff for the widget settings *)
1564
1565 let export_to_postscript (output : GMathView.math_view) =
1566  let lastdir = ref (Unix.getcwd ()) in
1567   function () ->
1568    match
1569     GToolbox.select_file ~title:"Export to PostScript"
1570      ~dir:lastdir ~filename:"screenshot.ps" ()
1571    with
1572       None -> ()
1573     | Some filename ->
1574        output#export_to_postscript ~filename:filename ();
1575 ;;
1576
1577 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1578  button_set_kerning button_set_transparency export_to_postscript_menu_item
1579  button_t1 ()
1580 =
1581  let is_set = button_t1#active in
1582   output#set_font_manager_type
1583    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1584   if is_set then
1585    begin
1586     button_set_anti_aliasing#misc#set_sensitive true ;
1587     button_set_kerning#misc#set_sensitive true ;
1588     button_set_transparency#misc#set_sensitive true ;
1589     export_to_postscript_menu_item#misc#set_sensitive true ;
1590    end
1591   else
1592    begin
1593     button_set_anti_aliasing#misc#set_sensitive false ;
1594     button_set_kerning#misc#set_sensitive false ;
1595     button_set_transparency#misc#set_sensitive false ;
1596     export_to_postscript_menu_item#misc#set_sensitive false ;
1597    end
1598 ;;
1599
1600 let set_anti_aliasing output button_set_anti_aliasing () =
1601  output#set_anti_aliasing button_set_anti_aliasing#active
1602 ;;
1603
1604 let set_kerning output button_set_kerning () =
1605  output#set_kerning button_set_kerning#active
1606 ;;
1607
1608 let set_transparency output button_set_transparency () =
1609  output#set_transparency button_set_transparency#active
1610 ;;
1611
1612 let changefont output font_size_spinb () =
1613  output#set_font_size font_size_spinb#value_as_int
1614 ;;
1615
1616 let set_log_verbosity output log_verbosity_spinb () =
1617  output#set_log_verbosity log_verbosity_spinb#value_as_int
1618 ;;
1619
1620 class settings_window (output : GMathView.math_view) sw
1621  export_to_postscript_menu_item selection_changed_callback
1622 =
1623  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1624  let vbox =
1625   GPack.vbox ~packing:settings_window#add () in
1626  let table =
1627   GPack.table
1628    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1629    ~border_width:5 ~packing:vbox#add () in
1630  let button_t1 =
1631   GButton.toggle_button ~label:"activate t1 fonts"
1632    ~packing:(table#attach ~left:0 ~top:0) () in
1633  let button_set_anti_aliasing =
1634   GButton.toggle_button ~label:"set_anti_aliasing"
1635    ~packing:(table#attach ~left:0 ~top:1) () in
1636  let button_set_kerning =
1637   GButton.toggle_button ~label:"set_kerning"
1638    ~packing:(table#attach ~left:1 ~top:1) () in
1639  let button_set_transparency =
1640   GButton.toggle_button ~label:"set_transparency"
1641    ~packing:(table#attach ~left:2 ~top:1) () in
1642  let table =
1643   GPack.table
1644    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1645    ~border_width:5 ~packing:vbox#add () in
1646  let font_size_label =
1647   GMisc.label ~text:"font size:"
1648    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1649  let font_size_spinb =
1650   let sadj =
1651    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1652   in
1653    GEdit.spin_button
1654     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1655  let log_verbosity_label =
1656   GMisc.label ~text:"log verbosity:"
1657    ~packing:(table#attach ~left:0 ~top:1) () in
1658  let log_verbosity_spinb =
1659   let sadj =
1660    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1661   in
1662    GEdit.spin_button
1663     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1664  let hbox =
1665   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1666  let closeb =
1667   GButton.button ~label:"Close"
1668    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1669 object(self)
1670  method show = settings_window#show
1671  initializer
1672   button_set_anti_aliasing#misc#set_sensitive false ;
1673   button_set_kerning#misc#set_sensitive false ;
1674   button_set_transparency#misc#set_sensitive false ;
1675   (* Signals connection *)
1676   ignore(button_t1#connect#clicked
1677    (activate_t1 output button_set_anti_aliasing button_set_kerning
1678     button_set_transparency export_to_postscript_menu_item button_t1)) ;
1679   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1680   ignore(button_set_anti_aliasing#connect#toggled
1681    (set_anti_aliasing output button_set_anti_aliasing));
1682   ignore(button_set_kerning#connect#toggled
1683    (set_kerning output button_set_kerning)) ;
1684   ignore(button_set_transparency#connect#toggled
1685    (set_transparency output button_set_transparency)) ;
1686   ignore(log_verbosity_spinb#connect#changed
1687    (set_log_verbosity output log_verbosity_spinb)) ;
1688   ignore(closeb#connect#clicked settings_window#misc#hide)
1689 end;;
1690
1691 (* Scratch window *)
1692
1693 class scratch_window outputhtml =
1694  let window =
1695   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1696  let vbox =
1697   GPack.vbox ~packing:window#add () in
1698  let hbox =
1699   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1700  let whdb =
1701   GButton.button ~label:"Whd"
1702    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1703  let reduceb =
1704   GButton.button ~label:"Reduce"
1705    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1706  let simplb =
1707   GButton.button ~label:"Simpl"
1708    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1709  let scrolled_window =
1710   GBin.scrolled_window ~border_width:10
1711    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1712  let mmlwidget =
1713   GMathView.math_view
1714    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1715 object(self)
1716  method outputhtml = outputhtml
1717  method mmlwidget = mmlwidget
1718  method show () = window#misc#hide () ; window#show ()
1719  initializer
1720   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1721   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1722   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1723   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1724   ignore(simplb#connect#clicked (simpl_in_scratch self))
1725 end;;
1726
1727 class page () =
1728  let vbox1 = GPack.vbox () in
1729  let scrolled_window1 =
1730   GBin.scrolled_window ~border_width:10
1731    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1732  let proofw =
1733   GMathView.math_view ~width:400 ~height:275
1734    ~packing:(scrolled_window1#add) () in
1735  let hbox3 =
1736   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1737  let exactb =
1738   GButton.button ~label:"Exact"
1739    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1740  let introsb =
1741   GButton.button ~label:"Intros"
1742    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1743  let applyb =
1744   GButton.button ~label:"Apply"
1745    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1746  let elimsimplintrosb =
1747   GButton.button ~label:"ElimSimplIntros"
1748    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1749  let elimtypeb =
1750   GButton.button ~label:"ElimType"
1751    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1752  let whdb =
1753   GButton.button ~label:"Whd"
1754    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1755  let reduceb =
1756   GButton.button ~label:"Reduce"
1757    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1758  let simplb =
1759   GButton.button ~label:"Simpl"
1760    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1761  let foldb =
1762   GButton.button ~label:"Fold"
1763    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1764  let cutb =
1765   GButton.button ~label:"Cut"
1766    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1767  let hbox4 =
1768   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1769  let changeb =
1770   GButton.button ~label:"Change"
1771    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1772  let letinb =
1773   GButton.button ~label:"Let ... In"
1774    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1775  let ringb =
1776   GButton.button ~label:"Ring"
1777    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1778  let clearbodyb =
1779   GButton.button ~label:"ClearBody"
1780    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1781  let clearb =
1782   GButton.button ~label:"Clear"
1783    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1784  let fourierb =
1785   GButton.button ~label:"Fourier"
1786    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1787  let rewritesimplb =
1788   GButton.button ~label:"RewriteSimpl ->"
1789    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1790  let reflexivityb =
1791   GButton.button ~label:"Reflexivity"
1792    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1793  let hbox5 =
1794   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1795  let symmetryb =
1796   GButton.button ~label:"Symmetry"
1797    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1798  let transitivityb =
1799   GButton.button ~label:"Transitivity"
1800    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1801  let leftb =
1802   GButton.button ~label:"Left"
1803    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1804  let rightb =
1805   GButton.button ~label:"Right"
1806    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1807  let assumptionb =
1808   GButton.button ~label:"Assumption"
1809    ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1810 object
1811  method proofw = proofw
1812  method content = vbox1
1813  initializer
1814   ignore(exactb#connect#clicked exact) ;
1815   ignore(applyb#connect#clicked apply) ;
1816   ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
1817   ignore(elimtypeb#connect#clicked elimtype) ;
1818   ignore(whdb#connect#clicked whd) ;
1819   ignore(reduceb#connect#clicked reduce) ;
1820   ignore(simplb#connect#clicked simpl) ;
1821   ignore(foldb#connect#clicked fold) ;
1822   ignore(cutb#connect#clicked cut) ;
1823   ignore(changeb#connect#clicked change) ;
1824   ignore(letinb#connect#clicked letin) ;
1825   ignore(ringb#connect#clicked ring) ;
1826   ignore(clearbodyb#connect#clicked clearbody) ;
1827   ignore(clearb#connect#clicked clear) ;
1828   ignore(fourierb#connect#clicked fourier) ;
1829   ignore(rewritesimplb#connect#clicked rewritesimpl) ;
1830   ignore(reflexivityb#connect#clicked reflexivity) ;
1831   ignore(symmetryb#connect#clicked symmetry) ;
1832   ignore(transitivityb#connect#clicked transitivity) ;
1833   ignore(leftb#connect#clicked left) ;
1834   ignore(rightb#connect#clicked right) ;
1835   ignore(assumptionb#connect#clicked assumption) ;
1836   ignore(introsb#connect#clicked intros) ;
1837  initializer
1838   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1839 end
1840 ;;
1841
1842 class notebook =
1843 object(self)
1844  val notebook = GPack.notebook ()
1845  val pages = ref []
1846  val mutable skip_switch_page_event = false
1847  method notebook = notebook
1848  method add_page n =
1849   let new_page = new page () in
1850    pages := !pages @ [n,new_page] ;
1851    notebook#append_page
1852     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
1853     new_page#content#coerce
1854  method remove_all_pages =
1855   List.iter (function _ -> notebook#remove_page 0) !pages ;
1856   pages := [] ;
1857  method set_current_page n =
1858   let (_,page) = List.find (function (m,_) -> m=n) !pages in
1859    let new_page = notebook#page_num page#content#coerce in
1860     if new_page <> notebook#current_page then
1861      skip_switch_page_event <- true ;
1862     notebook#goto_page new_page
1863  method set_empty_page = self#add_page (-1)
1864  method proofw =
1865   (snd (List.nth !pages notebook#current_page))#proofw
1866  initializer
1867   ignore
1868    (notebook#connect#switch_page
1869     (function i ->
1870       let skip = skip_switch_page_event in
1871        skip_switch_page_event <- false ;
1872        if not skip then
1873         try
1874          let metano = fst (List.nth !pages i) in
1875           setgoal metano
1876         with _ -> ()
1877     ))
1878 end
1879 ;;
1880
1881 (* Main window *)
1882
1883 class rendering_window output (notebook : notebook) =
1884  let window =
1885   GWindow.window ~title:"MathML viewer" ~border_width:2
1886    ~allow_shrink:false () in
1887  let vbox_for_menu = GPack.vbox ~packing:window#add () in
1888  (* menus *)
1889  let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
1890  let factory0 = new GMenu.factory menubar in
1891  let accel_group = factory0#accel_group in
1892  (* file menu *)
1893  let file_menu = factory0#add_submenu "File" in
1894  let factory1 = new GMenu.factory file_menu ~accel_group in
1895  let export_to_postscript_menu_item =
1896   begin
1897    ignore
1898     (factory1#add_item "Load" ~key:GdkKeysyms._L ~callback:load) ;
1899    ignore (factory1#add_item "Save" ~key:GdkKeysyms._S ~callback:save) ;
1900    ignore (factory1#add_separator ()) ;
1901    let export_to_postscript_menu_item =
1902     factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
1903      ~callback:(export_to_postscript output) in
1904    ignore (factory1#add_separator ()) ;
1905    ignore
1906     (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
1907    export_to_postscript_menu_item
1908   end in
1909  (* edit menu *)
1910  let edit_menu = factory0#add_submenu "Edit" in
1911  let factory2 = new GMenu.factory edit_menu ~accel_group in
1912  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
1913  let proveit_menu_item =
1914   factory2#add_item "Prove It" ~key:GdkKeysyms._I
1915    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
1916  in
1917  let focus_menu_item =
1918   factory2#add_item "Focus" ~key:GdkKeysyms._F
1919    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
1920  in
1921  let _ =
1922   focus_and_proveit_set_sensitive :=
1923    function b ->
1924     proveit_menu_item#misc#set_sensitive b ;
1925     focus_menu_item#misc#set_sensitive b
1926  in
1927  let _ = factory2#add_separator () in
1928  let _ = factory2#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
1929  let _ = !focus_and_proveit_set_sensitive false in
1930  (* settings menu *)
1931  let settings_menu = factory0#add_submenu "Settings" in
1932  let factory3 = new GMenu.factory settings_menu ~accel_group in
1933  let _ =
1934   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
1935    ~callback:edit_aliases in
1936  let _ = factory3#add_separator () in
1937  let _ =
1938   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
1939    ~callback:(function _ -> (settings_window ())#show ()) in
1940  (* accel group *)
1941  let _ = window#add_accel_group accel_group in
1942  (* end of menus *)
1943  let hbox0 =
1944   GPack.hbox
1945    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
1946  let vbox =
1947   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1948  let scrolled_window0 =
1949   GBin.scrolled_window ~border_width:10
1950    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1951  let _ = scrolled_window0#add output#coerce in
1952  let hbox4 =
1953   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1954  let stateb =
1955   GButton.button ~label:"State"
1956    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1957  let openb =
1958   GButton.button ~label:"Open"
1959    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1960  let checkb =
1961   GButton.button ~label:"Check"
1962    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1963  let locateb =
1964   GButton.button ~label:"Locate"
1965    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1966  let searchpatternb =
1967   GButton.button ~label:"SearchPattern"
1968    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1969  let scrolled_window1 =
1970   GBin.scrolled_window ~border_width:10
1971    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1972  let inputt = GEdit.text ~editable:true ~width:400 ~height:100
1973    ~packing:scrolled_window1#add () in
1974  let vboxl =
1975   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1976  let _ =
1977   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
1978  let frame = GBin.frame ~packing:(vboxl#pack ~expand:true ~padding:5) () in
1979  let outputhtml =
1980   GHtml.xmhtml
1981    ~source:"<html><body bgColor=\"white\"></body></html>"
1982    ~width:400 ~height: 100
1983    ~border_width:20
1984    ~packing:frame#add
1985    ~show:true () in
1986  let scratch_window = new scratch_window outputhtml in
1987 object
1988  method outputhtml = outputhtml
1989  method inputt = inputt
1990  method output = (output : GMathView.math_view)
1991  method notebook = notebook
1992  method show = window#show
1993  initializer
1994   notebook#set_empty_page ;
1995   export_to_postscript_menu_item#misc#set_sensitive false ;
1996   check_term := (check_term_in_scratch scratch_window) ;
1997
1998   (* signal handlers here *)
1999   ignore(output#connect#selection_changed
2000    (function elem ->
2001      notebook#proofw#unload ;
2002      choose_selection output elem ;
2003      !focus_and_proveit_set_sensitive true
2004    )) ;
2005   let settings_window = new settings_window output scrolled_window0
2006    export_to_postscript_menu_item (choose_selection output) in
2007   set_settings_window settings_window ;
2008   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2009   ignore(stateb#connect#clicked state) ;
2010   ignore(openb#connect#clicked open_) ;
2011   ignore(checkb#connect#clicked (check scratch_window)) ;
2012   ignore(locateb#connect#clicked locate) ;
2013   ignore(searchpatternb#connect#clicked searchPattern) ;
2014   Logger.log_callback :=
2015    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2016 end;;
2017
2018 (* MAIN *)
2019
2020 let initialize_everything () =
2021  let module U = Unix in
2022   let output = GMathView.math_view ~width:350 ~height:280 () in
2023   let notebook = new notebook in
2024    let rendering_window' = new rendering_window output notebook in
2025     set_rendering_window rendering_window' ;
2026     rendering_window'#show () ;
2027     GMain.Main.main ()
2028 ;;
2029
2030 let _ =
2031  if !usedb then
2032  Mqint.init "dbname=helm_mowgli" ;
2033 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2034  ignore (GtkMain.Main.init ()) ;
2035  initialize_everything () ;
2036  if !usedb then Mqint.close ();
2037 ;;