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