helm/gTopLevel/gTopLevel.ml

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