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