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    output_html (outputhtml ())
 489     ("<h1>Disambiguation phase started: " ^
 490       string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
 491    (* now we select only the ones that generates well-typed terms *)
 492    let resolve_ids' =
 493     let rec filter =
 494      function
 495         [] -> []
 496       | resolve::tl ->
 497          let metasenv',expr = mk_metasenv_and_expr resolve in
 498           try
 499 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
 500            ignore
 501             (CicTypeChecker.type_of_aux' metasenv context expr) ;
 502            resolve::(filter tl)
 503           with
 504            _ -> filter tl
 505     in
 506      filter resolve_ids
 507    in
 508     let resolve_id' =
 509      match resolve_ids' with
 510         [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
 511       | [resolve_id] -> resolve_id
 512       | _ ->
 513         let choices =
 514          List.map
 515           (function resolve ->
 516             List.map
 517              (function id ->
 518                id,
 519                 match resolve id with
 520                    None -> assert false
 521                  | Some uri ->
 522                     match uri with
 523                        CicTextualParser0.ConUri uri
 524                      | CicTextualParser0.VarUri uri ->
 525                         UriManager.string_of_uri uri
 526                      | CicTextualParser0.IndTyUri (uri,tyno) ->
 527                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
 528                          string_of_int (tyno+1) ^ ")"
 529                      | CicTextualParser0.IndConUri (uri,tyno,consno) ->
 530                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
 531                          string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
 532              ) dom
 533           ) resolve_ids'
 534         in
 535          let index = interactive_interpretation_choice choices in
 536           List.nth resolve_ids' index
 537     in
 538      id_to_uris := known_ids @ dom', resolve_id' ;
 539      mk_metasenv_and_expr resolve_id'
 540 ;;
 541
 542 let domImpl = Gdome.domImplementation ();;
 543
 544 let parseStyle name =
 545  let style =
 546   domImpl#createDocumentFromURI
 547 (*
 548    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 549 *)
 550    ~uri:("styles/" ^ name) ()
 551  in
 552   Gdome_xslt.processStylesheet style
 553 ;;
 554
 555 let d_c = parseStyle "drop_coercions.xsl";;
 556 let tc1 = parseStyle "objtheorycontent.xsl";;
 557 let hc2 = parseStyle "content_to_html.xsl";;
 558 let l   = parseStyle "link.xsl";;
 559
 560 let c1 = parseStyle "rootcontent.xsl";;
 561 let g  = parseStyle "genmmlid.xsl";;
 562 let c2 = parseStyle "annotatedpres.xsl";;
 563
 564
 565 let getterURL = Configuration.getter_url;;
 566 let processorURL = Configuration.processor_url;;
 567
 568 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 569 let mml_args =
 570  ["processorURL", "'" ^ processorURL ^ "'" ;
 571   "getterURL", "'" ^ getterURL ^ "'" ;
 572   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 573   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 574   "UNICODEvsSYMBOL", "'symbol'" ;
 575   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 576   "encoding", "'iso-8859-1'" ;
 577   "media-type", "'text/html'" ;
 578   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 579   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 580   "naturalLanguage", "'yes'" ;
 581   "annotations", "'no'" ;
 582   "explodeall", "'true()'" ;
 583   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 584   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 585 ;;
 586
 587 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 588 let sequent_args =
 589  ["processorURL", "'" ^ processorURL ^ "'" ;
 590   "getterURL", "'" ^ getterURL ^ "'" ;
 591   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 592   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 593   "UNICODEvsSYMBOL", "'symbol'" ;
 594   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 595   "encoding", "'iso-8859-1'" ;
 596   "media-type", "'text/html'" ;
 597   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 598   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 599   "naturalLanguage", "'no'" ;
 600   "annotations", "'no'" ;
 601   "explodeall", "'true()'" ;
 602   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 603   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 604 ;;
 605
 606 let parse_file filename =
 607  let inch = open_in filename in
 608   let rec read_lines () =
 609    try
 610     let line = input_line inch in
 611      line ^ read_lines ()
 612    with
 613     End_of_file -> ""
 614   in
 615    read_lines ()
 616 ;;
 617
 618 let applyStylesheets input styles args =
 619  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 620   input styles
 621 ;;
 622
 623 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 624 (*CSC: ????????????????? *)
 625  let xml, bodyxml =
 626   Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
 627  in
 628  let xmlinnertypes =
 629   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
 630    ~ids_to_inner_types
 631  in
 632   let input =
 633    match bodyxml with
 634       None -> Xml2Gdome.document_of_xml domImpl xml
 635     | Some bodyxml' ->
 636        Xml.pp xml (Some constanttypefile) ;
 637        Xml2Gdome.document_of_xml domImpl bodyxml'
 638   in
 639 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 640 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 641 (*CSC: local.                                                              *)
 642    Xml.pp xmlinnertypes (Some innertypesfile) ;
 643    let output = applyStylesheets input mml_styles mml_args in
 644     output
 645 ;;
 646
 647
 648 (* CALLBACKS *)
 649
 650 exception RefreshSequentException of exn;;
 651 exception RefreshProofException of exn;;
 652
 653 let refresh_proof (output : GMathView.math_view) =
 654  try
 655   let uri,currentproof =
 656    match !ProofEngine.proof with
 657       None -> assert false
 658     | Some (uri,metasenv,bo,ty) ->
 659        !qed_set_sensitive (List.length metasenv = 0) ;
 660        (*CSC: Wrong: [] is just plainly wrong *)
 661        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 662   in
 663    let
 664     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 665      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 666    =
 667     Cic2acic.acic_object_of_cic_object currentproof
 668    in
 669     let mml =
 670      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 671     in
 672      output#load_tree mml ;
 673      current_cic_infos :=
 674       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 675  with
 676   e ->
 677  match !ProofEngine.proof with
 678     None -> assert false
 679   | Some (uri,metasenv,bo,ty) ->
 680 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 681    raise (RefreshProofException e)
 682 ;;
 683
 684 let refresh_sequent ?(empty_notebook=true) notebook =
 685  try
 686   match !ProofEngine.goal with
 687      None ->
 688       if empty_notebook then
 689        begin
 690         notebook#remove_all_pages ~skip_switch_page_event:false ;
 691         notebook#set_empty_page
 692        end
 693       else
 694        notebook#proofw#unload
 695    | Some metano ->
 696       let metasenv =
 697        match !ProofEngine.proof with
 698           None -> assert false
 699         | Some (_,metasenv,_,_) -> metasenv
 700       in
 701       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 702        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 703         SequentPp.XmlPp.print_sequent metasenv currentsequent
 704        in
 705         let regenerate_notebook () =
 706          let skip_switch_page_event =
 707           match metasenv with
 708              (m,_,_)::_ when m = metano -> false
 709            | _ -> true
 710          in
 711           notebook#remove_all_pages ~skip_switch_page_event ;
 712           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
 713         in
 714           if empty_notebook then
 715            begin
 716             regenerate_notebook () ;
 717             notebook#set_current_page ~may_skip_switch_page_event:false metano
 718            end
 719           else
 720            begin
 721             let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
 722             let sequent_mml =
 723              applyStylesheets sequent_doc sequent_styles sequent_args
 724             in
 725              notebook#set_current_page ~may_skip_switch_page_event:true metano;
 726              notebook#proofw#load_tree ~dom:sequent_mml
 727            end ;
 728           current_goal_infos :=
 729            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 730  with
 731   e ->
 732 let metano =
 733   match !ProofEngine.goal with
 734      None -> assert false
 735    | Some m -> m
 736 in
 737 let metasenv =
 738  match !ProofEngine.proof with
 739     None -> assert false
 740   | Some (_,metasenv,_,_) -> metasenv
 741 in
 742 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 743 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 744    raise (RefreshSequentException e)
 745 ;;
 746
 747 (*
 748 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 749  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 750 *)
 751
 752 let mml_of_cic_term metano term =
 753  let metasenv =
 754   match !ProofEngine.proof with
 755      None -> []
 756    | Some (_,metasenv,_,_) -> metasenv
 757  in
 758  let context =
 759   match !ProofEngine.goal with
 760      None -> []
 761    | Some metano ->
 762       let (_,canonical_context,_) =
 763        List.find (function (m,_,_) -> m=metano) metasenv
 764       in
 765        canonical_context
 766  in
 767    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 768     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 769    in
 770     let sequent_doc =
 771      Xml2Gdome.document_of_xml domImpl sequent_gdome
 772     in
 773      let res =
 774       applyStylesheets sequent_doc sequent_styles sequent_args ;
 775      in
 776       current_scratch_infos :=
 777        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 778       res
 779 ;;
 780
 781 (***********************)
 782 (*       TACTICS       *)
 783 (***********************)
 784
 785 let call_tactic tactic () =
 786  let notebook = (rendering_window ())#notebook in
 787  let output = ((rendering_window ())#output : GMathView.math_view) in
 788  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 789  let savedproof = !ProofEngine.proof in
 790  let savedgoal  = !ProofEngine.goal in
 791   begin
 792    try
 793     tactic () ;
 794     refresh_sequent notebook ;
 795     refresh_proof output
 796    with
 797       RefreshSequentException e ->
 798        output_html outputhtml
 799         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 800          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 801        ProofEngine.proof := savedproof ;
 802        ProofEngine.goal := savedgoal ;
 803        refresh_sequent notebook
 804     | RefreshProofException e ->
 805        output_html outputhtml
 806         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 807          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 808        ProofEngine.proof := savedproof ;
 809        ProofEngine.goal := savedgoal ;
 810        refresh_sequent notebook ;
 811        refresh_proof output
 812     | e ->
 813        output_html outputhtml
 814         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 815        ProofEngine.proof := savedproof ;
 816        ProofEngine.goal := savedgoal ;
 817   end
 818 ;;
 819
 820 let call_tactic_with_input tactic () =
 821  let notebook = (rendering_window ())#notebook in
 822  let output = ((rendering_window ())#output : GMathView.math_view) in
 823  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 824  let inputt = ((rendering_window ())#inputt : GEdit.text) in
 825  let savedproof = !ProofEngine.proof in
 826  let savedgoal  = !ProofEngine.goal in
 827 (*CSC: Gran cut&paste da sotto... *)
 828   let inputlen = inputt#length in
 829   let input = inputt#get_chars 0 inputlen ^ "\n" in
 830    let lexbuf = Lexing.from_string input in
 831    let curi =
 832     match !ProofEngine.proof with
 833        None -> assert false
 834      | Some (curi,_,_,_) -> curi
 835    in
 836    let uri,metasenv,bo,ty =
 837     match !ProofEngine.proof with
 838        None -> assert false
 839      | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 840    in
 841    let canonical_context =
 842     match !ProofEngine.goal with
 843        None -> assert false
 844      | Some metano ->
 845         let (_,canonical_context,_) =
 846          List.find (function (m,_,_) -> m=metano) metasenv
 847         in
 848          canonical_context
 849    in
 850    let context =
 851     List.map
 852      (function
 853          Some (n,_) -> Some n
 854        | None -> None
 855      ) canonical_context
 856    in
 857     try
 858      while true do
 859       match
 860        CicTextualParserContext.main context metasenv CicTextualLexer.token
 861         lexbuf register_alias
 862       with
 863          None -> ()
 864        | Some (dom,mk_metasenv_and_expr) ->
 865           let (metasenv',expr) =
 866            disambiguate_input canonical_context metasenv dom
 867             mk_metasenv_and_expr
 868           in
 869            ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 870            tactic expr ;
 871            refresh_sequent notebook ;
 872            refresh_proof output
 873      done
 874     with
 875        CicTextualParser0.Eof ->
 876         inputt#delete_text 0 inputlen
 877      | RefreshSequentException e ->
 878         output_html outputhtml
 879          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 880           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 881         ProofEngine.proof := savedproof ;
 882         ProofEngine.goal := savedgoal ;
 883         refresh_sequent notebook
 884      | RefreshProofException e ->
 885         output_html outputhtml
 886          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 887           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 888         ProofEngine.proof := savedproof ;
 889         ProofEngine.goal := savedgoal ;
 890         refresh_sequent notebook ;
 891         refresh_proof output
 892      | e ->
 893         output_html outputhtml
 894          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 895         ProofEngine.proof := savedproof ;
 896         ProofEngine.goal := savedgoal ;
 897 ;;
 898
 899 let call_tactic_with_goal_input tactic () =
 900  let module L = LogicalOperations in
 901  let module G = Gdome in
 902   let notebook = (rendering_window ())#notebook in
 903   let output = ((rendering_window ())#output : GMathView.math_view) in
 904   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 905   let savedproof = !ProofEngine.proof in
 906   let savedgoal  = !ProofEngine.goal in
 907    match notebook#proofw#get_selection with
 908      Some node ->
 909       let xpath =
 910        ((node : Gdome.element)#getAttributeNS
 911          ~namespaceURI:helmns
 912          ~localName:(G.domString "xref"))#to_string
 913       in
 914        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 915        else
 916         begin
 917          try
 918           match !current_goal_infos with
 919              Some (ids_to_terms, ids_to_father_ids,_) ->
 920               let id = xpath in
 921                tactic (Hashtbl.find ids_to_terms id) ;
 922                refresh_sequent notebook ;
 923                refresh_proof output
 924            | None -> assert false (* "ERROR: No current term!!!" *)
 925          with
 926             RefreshSequentException e ->
 927              output_html outputhtml
 928               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 929                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 930              ProofEngine.proof := savedproof ;
 931              ProofEngine.goal := savedgoal ;
 932              refresh_sequent notebook
 933           | RefreshProofException e ->
 934              output_html outputhtml
 935               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 936                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 937              ProofEngine.proof := savedproof ;
 938              ProofEngine.goal := savedgoal ;
 939              refresh_sequent notebook ;
 940              refresh_proof output
 941           | e ->
 942              output_html outputhtml
 943               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 944              ProofEngine.proof := savedproof ;
 945              ProofEngine.goal := savedgoal ;
 946         end
 947    | None ->
 948       output_html outputhtml
 949        ("<h1 color=\"red\">No term selected</h1>")
 950 ;;
 951
 952 let call_tactic_with_input_and_goal_input tactic () =
 953  let module L = LogicalOperations in
 954  let module G = Gdome in
 955   let notebook = (rendering_window ())#notebook in
 956   let output = ((rendering_window ())#output : GMathView.math_view) in
 957   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 958   let inputt = ((rendering_window ())#inputt : GEdit.text) in
 959   let savedproof = !ProofEngine.proof in
 960   let savedgoal  = !ProofEngine.goal in
 961    match notebook#proofw#get_selection with
 962      Some node ->
 963       let xpath =
 964        ((node : Gdome.element)#getAttributeNS
 965          ~namespaceURI:helmns
 966          ~localName:(G.domString "xref"))#to_string
 967       in
 968        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 969        else
 970         begin
 971          try
 972           match !current_goal_infos with
 973              Some (ids_to_terms, ids_to_father_ids,_) ->
 974               let id = xpath in
 975                (* Let's parse the input *)
 976                let inputlen = inputt#length in
 977                let input = inputt#get_chars 0 inputlen ^ "\n" in
 978                 let lexbuf = Lexing.from_string input in
 979                 let curi =
 980                  match !ProofEngine.proof with
 981                     None -> assert false
 982                   | Some (curi,_,_,_) -> curi
 983                 in
 984                 let uri,metasenv,bo,ty =
 985                  match !ProofEngine.proof with
 986                     None -> assert false
 987                   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 988                 in
 989                 let canonical_context =
 990                  match !ProofEngine.goal with
 991                     None -> assert false
 992                   | Some metano ->
 993                      let (_,canonical_context,_) =
 994                       List.find (function (m,_,_) -> m=metano) metasenv
 995                      in
 996                       canonical_context in
 997                 let context =
 998                  List.map
 999                   (function
1000                       Some (n,_) -> Some n
1001                     | None -> None
1002                   ) canonical_context
1003                 in
1004                  begin
1005                   try
1006                    while true do
1007                     match
1008                      CicTextualParserContext.main context metasenv
1009                       CicTextualLexer.token lexbuf register_alias
1010                     with
1011                        None -> ()
1012                      | Some (dom,mk_metasenv_and_expr) ->
1013                         let (metasenv',expr) =
1014                          disambiguate_input canonical_context metasenv dom
1015                           mk_metasenv_and_expr
1016                         in
1017                          ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
1018                          tactic ~goal_input:(Hashtbl.find ids_to_terms id)
1019                           ~input:expr ;
1020                          refresh_sequent notebook ;
1021                          refresh_proof output
1022                    done
1023                   with
1024                      CicTextualParser0.Eof ->
1025                       inputt#delete_text 0 inputlen
1026                  end
1027            | None -> assert false (* "ERROR: No current term!!!" *)
1028          with
1029             RefreshSequentException e ->
1030              output_html outputhtml
1031               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1032                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1033              ProofEngine.proof := savedproof ;
1034              ProofEngine.goal := savedgoal ;
1035              refresh_sequent notebook
1036           | RefreshProofException e ->
1037              output_html outputhtml
1038               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1039                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1040              ProofEngine.proof := savedproof ;
1041              ProofEngine.goal := savedgoal ;
1042              refresh_sequent notebook ;
1043              refresh_proof output
1044           | e ->
1045              output_html outputhtml
1046               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1047              ProofEngine.proof := savedproof ;
1048              ProofEngine.goal := savedgoal ;
1049         end
1050    | None ->
1051       output_html outputhtml
1052        ("<h1 color=\"red\">No term selected</h1>")
1053 ;;
1054
1055 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
1056  let module L = LogicalOperations in
1057  let module G = Gdome in
1058   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
1059   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
1060   let savedproof = !ProofEngine.proof in
1061   let savedgoal  = !ProofEngine.goal in
1062    match mmlwidget#get_selection with
1063      Some node ->
1064       let xpath =
1065        ((node : Gdome.element)#getAttributeNS
1066          ~namespaceURI:helmns
1067          ~localName:(G.domString "xref"))#to_string
1068       in
1069        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1070        else
1071         begin
1072          try
1073           match !current_scratch_infos with
1074              (* term is the whole goal in the scratch_area *)
1075              Some (term,ids_to_terms, ids_to_father_ids,_) ->
1076               let id = xpath in
1077                let expr = tactic term (Hashtbl.find ids_to_terms id) in
1078                 let mml = mml_of_cic_term 111 expr in
1079                  scratch_window#show () ;
1080                  scratch_window#mmlwidget#load_tree ~dom:mml
1081            | None -> assert false (* "ERROR: No current term!!!" *)
1082          with
1083           e ->
1084            output_html outputhtml
1085             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1086         end
1087    | None ->
1088       output_html outputhtml
1089        ("<h1 color=\"red\">No term selected</h1>")
1090 ;;
1091
1092 let call_tactic_with_hypothesis_input tactic () =
1093  let module L = LogicalOperations in
1094  let module G = Gdome in
1095   let notebook = (rendering_window ())#notebook in
1096   let output = ((rendering_window ())#output : GMathView.math_view) in
1097   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1098   let savedproof = !ProofEngine.proof in
1099   let savedgoal  = !ProofEngine.goal in
1100    match notebook#proofw#get_selection with
1101      Some node ->
1102       let xpath =
1103        ((node : Gdome.element)#getAttributeNS
1104          ~namespaceURI:helmns
1105          ~localName:(G.domString "xref"))#to_string
1106       in
1107        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1108        else
1109         begin
1110          try
1111           match !current_goal_infos with
1112              Some (_,_,ids_to_hypotheses) ->
1113               let id = xpath in
1114                tactic (Hashtbl.find ids_to_hypotheses id) ;
1115                refresh_sequent notebook ;
1116                refresh_proof output
1117            | None -> assert false (* "ERROR: No current term!!!" *)
1118          with
1119             RefreshSequentException e ->
1120              output_html outputhtml
1121               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1122                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1123              ProofEngine.proof := savedproof ;
1124              ProofEngine.goal := savedgoal ;
1125              refresh_sequent notebook
1126           | RefreshProofException e ->
1127              output_html outputhtml
1128               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1129                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1130              ProofEngine.proof := savedproof ;
1131              ProofEngine.goal := savedgoal ;
1132              refresh_sequent notebook ;
1133              refresh_proof output
1134           | e ->
1135              output_html outputhtml
1136               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1137              ProofEngine.proof := savedproof ;
1138              ProofEngine.goal := savedgoal ;
1139         end
1140    | None ->
1141       output_html outputhtml
1142        ("<h1 color=\"red\">No term selected</h1>")
1143 ;;
1144
1145
1146 let intros = call_tactic ProofEngine.intros;;
1147 let exact = call_tactic_with_input ProofEngine.exact;;
1148 let apply = call_tactic_with_input ProofEngine.apply;;
1149 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
1150 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
1151 let whd = call_tactic_with_goal_input ProofEngine.whd;;
1152 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
1153 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
1154 let fold = call_tactic_with_input ProofEngine.fold;;
1155 let cut = call_tactic_with_input ProofEngine.cut;;
1156 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
1157 let letin = call_tactic_with_input ProofEngine.letin;;
1158 let ring = call_tactic ProofEngine.ring;;
1159 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
1160 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
1161 let fourier = call_tactic ProofEngine.fourier;;
1162 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
1163 let reflexivity = call_tactic ProofEngine.reflexivity;;
1164 let symmetry = call_tactic ProofEngine.symmetry;;
1165 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
1166 let left = call_tactic ProofEngine.left;;
1167 let right = call_tactic ProofEngine.right;;
1168 let assumption = call_tactic ProofEngine.assumption;;
1169
1170 let whd_in_scratch scratch_window =
1171  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
1172   scratch_window
1173 ;;
1174 let reduce_in_scratch scratch_window =
1175  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
1176   scratch_window
1177 ;;
1178 let simpl_in_scratch scratch_window =
1179  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
1180   scratch_window
1181 ;;
1182
1183
1184
1185 (**********************)
1186 (*   END OF TACTICS   *)
1187 (**********************)
1188
1189 exception OpenConjecturesStillThere;;
1190 exception WrongProof;;
1191
1192 let qed () =
1193  match !ProofEngine.proof with
1194     None -> assert false
1195   | Some (uri,[],bo,ty) ->
1196      if
1197       CicReduction.are_convertible []
1198        (CicTypeChecker.type_of_aux' [] [] bo) ty
1199      then
1200       begin
1201        (*CSC: Wrong: [] is just plainly wrong *)
1202        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
1203         let
1204          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1205           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1206         =
1207          Cic2acic.acic_object_of_cic_object proof
1208         in
1209          let mml =
1210           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
1211          in
1212           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
1213           current_cic_infos :=
1214            Some
1215             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
1216              ids_to_hypotheses)
1217       end
1218      else
1219       raise WrongProof
1220   | _ -> raise OpenConjecturesStillThere
1221 ;;
1222
1223 (*????
1224 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
1225 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
1226 *)
1227 let dtdname = "/projects/helm/V7_mowgli/dtd/cic.dtd";;
1228
1229 let save () =
1230  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1231   match !ProofEngine.proof with
1232      None -> assert false
1233    | Some (uri, metasenv, bo, ty) ->
1234       let currentproof =
1235        (*CSC: Wrong: [] is just plainly wrong *)
1236        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
1237       in
1238        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
1239         Cic2acic.acic_object_of_cic_object currentproof
1240        in
1241         let xml, bodyxml =
1242          match Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof with
1243             xml,Some bodyxml -> xml,bodyxml
1244           | _,None -> assert false
1245         in
1246          Xml.pp ~quiet:true xml (Some prooffiletype) ;
1247          output_html outputhtml
1248           ("<h1 color=\"Green\">Current proof type saved to " ^
1249            prooffiletype ^ "</h1>") ;
1250          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
1251          output_html outputhtml
1252           ("<h1 color=\"Green\">Current proof body saved to " ^
1253            prooffile ^ "</h1>")
1254 ;;
1255
1256 (* Used to typecheck the loaded proofs *)
1257 let typecheck_loaded_proof metasenv bo ty =
1258  let module T = CicTypeChecker in
1259   ignore (
1260    List.fold_left
1261     (fun metasenv ((_,context,ty) as conj) ->
1262       ignore (T.type_of_aux' metasenv context ty) ;
1263       metasenv @ [conj]
1264     ) [] metasenv) ;
1265   ignore (T.type_of_aux' metasenv [] ty) ;
1266   ignore (T.type_of_aux' metasenv [] bo)
1267 ;;
1268
1269 let load () =
1270  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1271  let output = ((rendering_window ())#output : GMathView.math_view) in
1272  let notebook = (rendering_window ())#notebook in
1273   try
1274    let uri = UriManager.uri_of_string "cic:/dummy.con" in
1275     match CicParser.obj_of_xml prooffiletype (Some prooffile) with
1276        Cic.CurrentProof (_,metasenv,bo,ty,_) ->
1277         typecheck_loaded_proof metasenv bo ty ;
1278         ProofEngine.proof :=
1279          Some (uri, metasenv, bo, ty) ;
1280         ProofEngine.goal :=
1281          (match metasenv with
1282              [] -> None
1283            | (metano,_,_)::_ -> Some metano
1284          ) ;
1285         refresh_proof output ;
1286         refresh_sequent notebook ;
1287          output_html outputhtml
1288           ("<h1 color=\"Green\">Current proof type loaded from " ^
1289             prooffiletype ^ "</h1>") ;
1290          output_html outputhtml
1291           ("<h1 color=\"Green\">Current proof body loaded from " ^
1292             prooffile ^ "</h1>") ;
1293         !save_set_sensitive true
1294      | _ -> assert false
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 edit_aliases () =
1310  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1311  let dom,resolve_id = !id_to_uris in
1312   let inputlen = inputt#length in
1313    inputt#delete_text 0 inputlen ;
1314    let _ =
1315     inputt#insert_text ~pos:0
1316      (String.concat "\n"
1317        (List.map
1318          (function v ->
1319            let uri =
1320             match resolve_id v with
1321                None -> assert false
1322              | Some uri -> uri
1323            in
1324             "alias " ^ v ^ " " ^
1325               (string_of_cic_textual_parser_uri uri)
1326          ) dom))
1327    in
1328     id_to_uris := empty_id_to_uris
1329 ;;
1330
1331 let proveit () =
1332  let module L = LogicalOperations in
1333  let module G = Gdome in
1334  let notebook = (rendering_window ())#notebook in
1335  let output = (rendering_window ())#output in
1336  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1337   match (rendering_window ())#output#get_selection with
1338     Some node ->
1339      let xpath =
1340       ((node : Gdome.element)#getAttributeNS
1341       (*CSC: OCAML DIVERGE
1342       ((element : G.element)#getAttributeNS
1343       *)
1344         ~namespaceURI:helmns
1345         ~localName:(G.domString "xref"))#to_string
1346      in
1347       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1348       else
1349        begin
1350         try
1351          match !current_cic_infos with
1352             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1353              let id = xpath in
1354               L.to_sequent id ids_to_terms ids_to_father_ids ;
1355               refresh_proof output ;
1356               refresh_sequent notebook
1357           | None -> assert false (* "ERROR: No current term!!!" *)
1358         with
1359            RefreshSequentException e ->
1360             output_html outputhtml
1361              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1362               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1363          | RefreshProofException e ->
1364             output_html outputhtml
1365              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1366               "proof: " ^ Printexc.to_string e ^ "</h1>")
1367          | e ->
1368             output_html outputhtml
1369              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1370        end
1371   | None -> assert false (* "ERROR: No selection!!!" *)
1372 ;;
1373
1374 let focus () =
1375  let module L = LogicalOperations in
1376  let module G = Gdome in
1377  let notebook = (rendering_window ())#notebook in
1378  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1379   match (rendering_window ())#output#get_selection with
1380     Some node ->
1381      let xpath =
1382       ((node : Gdome.element)#getAttributeNS
1383       (*CSC: OCAML DIVERGE
1384       ((element : G.element)#getAttributeNS
1385       *)
1386         ~namespaceURI:helmns
1387         ~localName:(G.domString "xref"))#to_string
1388      in
1389       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1390       else
1391        begin
1392         try
1393          match !current_cic_infos with
1394             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1395              let id = xpath in
1396               L.focus id ids_to_terms ids_to_father_ids ;
1397               refresh_sequent notebook
1398           | None -> assert false (* "ERROR: No current term!!!" *)
1399         with
1400            RefreshSequentException e ->
1401             output_html outputhtml
1402              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1403               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1404          | RefreshProofException e ->
1405             output_html outputhtml
1406              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1407               "proof: " ^ Printexc.to_string e ^ "</h1>")
1408          | e ->
1409             output_html outputhtml
1410              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1411        end
1412   | None -> assert false (* "ERROR: No selection!!!" *)
1413 ;;
1414
1415 exception NoPrevGoal;;
1416 exception NoNextGoal;;
1417
1418 let setgoal metano =
1419  let module L = LogicalOperations in
1420  let module G = Gdome in
1421  let notebook = (rendering_window ())#notebook in
1422  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1423   let metasenv =
1424    match !ProofEngine.proof with
1425       None -> assert false
1426     | Some (_,metasenv,_,_) -> metasenv
1427   in
1428    try
1429     refresh_sequent ~empty_notebook:false notebook
1430    with
1431       RefreshSequentException e ->
1432        output_html outputhtml
1433         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1434          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1435     | e ->
1436        output_html outputhtml
1437         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1438 ;;
1439
1440 exception NotADefinition;;
1441
1442 let open_ () =
1443  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1444  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1445  let output = ((rendering_window ())#output : GMathView.math_view) in
1446  let notebook = (rendering_window ())#notebook in
1447   let inputlen = inputt#length in
1448   let input = inputt#get_chars 0 inputlen in
1449    try
1450     let uri = UriManager.uri_of_string ("cic:" ^ input) in
1451      CicTypeChecker.typecheck uri ;
1452      let metasenv,bo,ty =
1453       match CicEnvironment.get_cooked_obj uri with
1454          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
1455        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
1456        | Cic.Constant _
1457        | Cic.Variable _
1458        | Cic.InductiveDefinition _ -> raise NotADefinition
1459      in
1460       ProofEngine.proof :=
1461        Some (uri, metasenv, bo, ty) ;
1462       ProofEngine.goal := None ;
1463       refresh_sequent notebook ;
1464       refresh_proof output ;
1465       inputt#delete_text 0 inputlen
1466    with
1467       RefreshSequentException e ->
1468        output_html outputhtml
1469         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1470          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1471     | RefreshProofException e ->
1472        output_html outputhtml
1473         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1474          "proof: " ^ Printexc.to_string e ^ "</h1>")
1475     | e ->
1476        output_html outputhtml
1477         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1478 ;;
1479
1480 let state () =
1481  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1482  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1483  let output = ((rendering_window ())#output : GMathView.math_view) in
1484  let notebook = (rendering_window ())#notebook in
1485   let inputlen = inputt#length in
1486   let input = inputt#get_chars 0 inputlen ^ "\n" in
1487    (* Do something interesting *)
1488    let lexbuf = Lexing.from_string input in
1489     try
1490      while true do
1491       (* Execute the actions *)
1492       match
1493        CicTextualParserContext.main [] [] CicTextualLexer.token
1494         lexbuf register_alias
1495       with
1496          None -> ()
1497        | Some (dom,mk_metasenv_and_expr) ->
1498           let metasenv,expr =
1499            disambiguate_input [] [] dom mk_metasenv_and_expr
1500           in
1501            let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1502             ProofEngine.proof :=
1503              Some (UriManager.uri_of_string "cic:/dummy.con",
1504                     (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1505             ProofEngine.goal := Some 1 ;
1506             refresh_sequent notebook ;
1507             refresh_proof output ;
1508             !save_set_sensitive true
1509      done
1510     with
1511        CicTextualParser0.Eof ->
1512         inputt#delete_text 0 inputlen
1513      | RefreshSequentException e ->
1514         output_html outputhtml
1515          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1516           "sequent: " ^ Printexc.to_string e ^ "</h1>")
1517      | RefreshProofException e ->
1518         output_html outputhtml
1519          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1520           "proof: " ^ Printexc.to_string e ^ "</h1>")
1521      | e ->
1522         output_html outputhtml
1523          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1524 ;;
1525
1526 let check_term_in_scratch scratch_window metasenv context expr =
1527  try
1528   let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
1529    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1530 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1531     scratch_window#show () ;
1532     scratch_window#mmlwidget#load_tree ~dom:mml
1533  with
1534   e ->
1535    print_endline ("? " ^ CicPp.ppterm expr) ;
1536    raise e
1537 ;;
1538
1539 let check scratch_window () =
1540  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1541  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1542   let inputlen = inputt#length in
1543   let input = inputt#get_chars 0 inputlen ^ "\n" in
1544   let curi,metasenv =
1545    match !ProofEngine.proof with
1546       None -> UriManager.uri_of_string "cic:/dummy.con", []
1547     | Some (curi,metasenv,_,_) -> curi,metasenv
1548   in
1549   let context,names_context =
1550    let context =
1551     match !ProofEngine.goal with
1552        None -> []
1553      | Some metano ->
1554         let (_,canonical_context,_) =
1555          List.find (function (m,_,_) -> m=metano) metasenv
1556         in
1557          canonical_context
1558    in
1559     context,
1560     List.map
1561      (function
1562          Some (n,_) -> Some n
1563        | None -> None
1564      ) context
1565   in
1566    let lexbuf = Lexing.from_string input in
1567     try
1568      while true do
1569       (* Execute the actions *)
1570       match
1571        CicTextualParserContext.main names_context metasenv CicTextualLexer.token
1572         lexbuf register_alias
1573       with
1574          None -> ()
1575        | Some (dom,mk_metasenv_and_expr) ->
1576           let (metasenv',expr) =
1577            disambiguate_input context metasenv dom mk_metasenv_and_expr
1578           in
1579            check_term_in_scratch scratch_window metasenv' context expr
1580      done
1581     with
1582        CicTextualParser0.Eof -> ()
1583      | e ->
1584        output_html outputhtml
1585         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1586 ;;
1587
1588 exception NoObjectsLocated;;
1589
1590 let user_uri_choice ~title ~msg uris =
1591  let uri =
1592   match uris with
1593      [] -> raise NoObjectsLocated
1594    | [uri] -> uri
1595    | uris ->
1596       match
1597        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1598       with
1599          [uri] -> uri
1600        | _ -> assert false
1601  in
1602   String.sub uri 4 (String.length uri - 4)
1603 ;;
1604
1605 let locate () =
1606  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1607  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1608   let inputlen = inputt#length in
1609   let input = inputt#get_chars 0 inputlen in
1610    try
1611     match Str.split (Str.regexp "[ \t]+") input with
1612        [] -> ()
1613      | head :: tail ->
1614         inputt#delete_text 0 inputlen ;
1615         let result = MQueryGenerator.locate head in
1616         let uris =
1617          List.map
1618           (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1619           result in
1620         let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1621          output_html outputhtml html ;
1622          let uri' =
1623           user_uri_choice ~title:"Ambiguous input."
1624            ~msg:
1625              ("Ambiguous input \"" ^ head ^
1626               "\". Please, choose one interpetation:")
1627            uris
1628          in
1629           ignore ((inputt#insert_text uri') ~pos:0)
1630    with
1631     e ->
1632      output_html outputhtml
1633       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1634 ;;
1635
1636 let searchPattern () =
1637  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1638  let inputt = ((rendering_window ())#inputt : GEdit.text) in
1639   let inputlen = inputt#length in
1640   let input = inputt#get_chars 0 inputlen in
1641   let level = int_of_string input in
1642   let metasenv =
1643    match !ProofEngine.proof with
1644       None -> assert false
1645     | Some (_,metasenv,_,_) -> metasenv
1646   in
1647    try
1648     match !ProofEngine.goal with
1649        None -> ()
1650      | Some metano ->
1651         let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1652          let result = MQueryGenerator.searchPattern metasenv ey ty level in
1653          let uris =
1654           List.map
1655            (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1656            result in
1657          let html =
1658           " <h1>Backward Query: </h1>" ^
1659           " <h2>Levels: </h2> " ^
1660            MQueryGenerator.string_of_levels
1661             (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1662            " <pre>" ^ get_last_query result ^ "</pre>"
1663          in
1664           output_html outputhtml html ;
1665           let uris',exc =
1666            let rec filter_out =
1667             function
1668                [] -> [],""
1669              | uri::tl ->
1670                 let tl',exc = filter_out tl in
1671                  try
1672                   if
1673                    ProofEngine.can_apply
1674                     (term_of_cic_textual_parser_uri
1675                      (cic_textual_parser_uri_of_string uri))
1676                   then
1677                    uri::tl',exc
1678                   else
1679                    tl',exc
1680                  with
1681                   e ->
1682                    let exc' =
1683                     "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
1684                      uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
1685                    in
1686                     tl',exc'
1687            in
1688             filter_out uris
1689           in
1690            let html' =
1691             " <h1>Objects that can actually be applied: </h1> " ^
1692             String.concat "<br>" uris' ^ exc ^
1693             " <h1>Number of false matches: " ^
1694              string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
1695             " <h1>Number of good matches: " ^
1696              string_of_int (List.length uris') ^ "</h1>"
1697            in
1698             output_html outputhtml html' ;
1699             let uri' =
1700              user_uri_choice ~title:"Ambiguous input."
1701              ~msg:"Many lemmas can be successfully applied. Please, choose one:"
1702               uris'
1703             in
1704              inputt#delete_text 0 inputlen ;
1705              ignore ((inputt#insert_text uri') ~pos:0)
1706     with
1707      e ->
1708       output_html outputhtml
1709        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1710 ;;
1711
1712 let choose_selection
1713      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1714 =
1715  let module G = Gdome in
1716   let rec aux element =
1717    if element#hasAttributeNS
1718        ~namespaceURI:helmns
1719        ~localName:(G.domString "xref")
1720    then
1721      mmlwidget#set_selection (Some element)
1722    else
1723       match element#get_parentNode with
1724          None -> assert false
1725        (*CSC: OCAML DIVERGES!
1726        | Some p -> aux (new G.element_of_node p)
1727        *)
1728        | Some p -> aux (new Gdome.element_of_node p)
1729   in
1730    match element with
1731      Some x -> aux x
1732    | None   -> mmlwidget#set_selection None
1733 ;;
1734
1735 (* STUFF TO BUILD THE GTK INTERFACE *)
1736
1737 (* Stuff for the widget settings *)
1738
1739 let export_to_postscript (output : GMathView.math_view) =
1740  let lastdir = ref (Unix.getcwd ()) in
1741   function () ->
1742    match
1743     GToolbox.select_file ~title:"Export to PostScript"
1744      ~dir:lastdir ~filename:"screenshot.ps" ()
1745    with
1746       None -> ()
1747     | Some filename ->
1748        output#export_to_postscript ~filename:filename ();
1749 ;;
1750
1751 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1752  button_set_kerning button_set_transparency export_to_postscript_menu_item
1753  button_t1 ()
1754 =
1755  let is_set = button_t1#active in
1756   output#set_font_manager_type
1757    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1758   if is_set then
1759    begin
1760     button_set_anti_aliasing#misc#set_sensitive true ;
1761     button_set_kerning#misc#set_sensitive true ;
1762     button_set_transparency#misc#set_sensitive true ;
1763     export_to_postscript_menu_item#misc#set_sensitive true ;
1764    end
1765   else
1766    begin
1767     button_set_anti_aliasing#misc#set_sensitive false ;
1768     button_set_kerning#misc#set_sensitive false ;
1769     button_set_transparency#misc#set_sensitive false ;
1770     export_to_postscript_menu_item#misc#set_sensitive false ;
1771    end
1772 ;;
1773
1774 let set_anti_aliasing output button_set_anti_aliasing () =
1775  output#set_anti_aliasing button_set_anti_aliasing#active
1776 ;;
1777
1778 let set_kerning output button_set_kerning () =
1779  output#set_kerning button_set_kerning#active
1780 ;;
1781
1782 let set_transparency output button_set_transparency () =
1783  output#set_transparency button_set_transparency#active
1784 ;;
1785
1786 let changefont output font_size_spinb () =
1787  output#set_font_size font_size_spinb#value_as_int
1788 ;;
1789
1790 let set_log_verbosity output log_verbosity_spinb () =
1791  output#set_log_verbosity log_verbosity_spinb#value_as_int
1792 ;;
1793
1794 class settings_window (output : GMathView.math_view) sw
1795  export_to_postscript_menu_item selection_changed_callback
1796 =
1797  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1798  let vbox =
1799   GPack.vbox ~packing:settings_window#add () in
1800  let table =
1801   GPack.table
1802    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1803    ~border_width:5 ~packing:vbox#add () in
1804  let button_t1 =
1805   GButton.toggle_button ~label:"activate t1 fonts"
1806    ~packing:(table#attach ~left:0 ~top:0) () in
1807  let button_set_anti_aliasing =
1808   GButton.toggle_button ~label:"set_anti_aliasing"
1809    ~packing:(table#attach ~left:0 ~top:1) () in
1810  let button_set_kerning =
1811   GButton.toggle_button ~label:"set_kerning"
1812    ~packing:(table#attach ~left:1 ~top:1) () in
1813  let button_set_transparency =
1814   GButton.toggle_button ~label:"set_transparency"
1815    ~packing:(table#attach ~left:2 ~top:1) () in
1816  let table =
1817   GPack.table
1818    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1819    ~border_width:5 ~packing:vbox#add () in
1820  let font_size_label =
1821   GMisc.label ~text:"font size:"
1822    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1823  let font_size_spinb =
1824   let sadj =
1825    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1826   in
1827    GEdit.spin_button
1828     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1829  let log_verbosity_label =
1830   GMisc.label ~text:"log verbosity:"
1831    ~packing:(table#attach ~left:0 ~top:1) () in
1832  let log_verbosity_spinb =
1833   let sadj =
1834    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1835   in
1836    GEdit.spin_button
1837     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1838  let hbox =
1839   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1840  let closeb =
1841   GButton.button ~label:"Close"
1842    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1843 object(self)
1844  method show = settings_window#show
1845  initializer
1846   button_set_anti_aliasing#misc#set_sensitive false ;
1847   button_set_kerning#misc#set_sensitive false ;
1848   button_set_transparency#misc#set_sensitive false ;
1849   (* Signals connection *)
1850   ignore(button_t1#connect#clicked
1851    (activate_t1 output button_set_anti_aliasing button_set_kerning
1852     button_set_transparency export_to_postscript_menu_item button_t1)) ;
1853   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1854   ignore(button_set_anti_aliasing#connect#toggled
1855    (set_anti_aliasing output button_set_anti_aliasing));
1856   ignore(button_set_kerning#connect#toggled
1857    (set_kerning output button_set_kerning)) ;
1858   ignore(button_set_transparency#connect#toggled
1859    (set_transparency output button_set_transparency)) ;
1860   ignore(log_verbosity_spinb#connect#changed
1861    (set_log_verbosity output log_verbosity_spinb)) ;
1862   ignore(closeb#connect#clicked settings_window#misc#hide)
1863 end;;
1864
1865 (* Scratch window *)
1866
1867 class scratch_window outputhtml =
1868  let window =
1869   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1870  let vbox =
1871   GPack.vbox ~packing:window#add () in
1872  let hbox =
1873   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1874  let whdb =
1875   GButton.button ~label:"Whd"
1876    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1877  let reduceb =
1878   GButton.button ~label:"Reduce"
1879    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1880  let simplb =
1881   GButton.button ~label:"Simpl"
1882    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1883  let scrolled_window =
1884   GBin.scrolled_window ~border_width:10
1885    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1886  let mmlwidget =
1887   GMathView.math_view
1888    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1889 object(self)
1890  method outputhtml = outputhtml
1891  method mmlwidget = mmlwidget
1892  method show () = window#misc#hide () ; window#show ()
1893  initializer
1894   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1895   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1896   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1897   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1898   ignore(simplb#connect#clicked (simpl_in_scratch self))
1899 end;;
1900
1901 class page () =
1902  let vbox1 = GPack.vbox () in
1903 object(self)
1904  val mutable proofw_ref = None
1905  val mutable compute_ref = None
1906  method proofw =
1907   Lazy.force self#compute ;
1908   match proofw_ref with
1909      None -> assert false
1910    | Some proofw -> proofw
1911  method content = vbox1
1912  method compute =
1913   match compute_ref with
1914      None -> assert false
1915    | Some compute -> compute
1916  initializer
1917   compute_ref <-
1918    Some (lazy (
1919    let scrolled_window1 =
1920     GBin.scrolled_window ~border_width:10
1921      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1922    let proofw =
1923     GMathView.math_view ~width:400 ~height:275
1924      ~packing:(scrolled_window1#add) () in
1925    let _ = proofw_ref <- Some proofw in
1926    let hbox3 =
1927     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1928    let exactb =
1929     GButton.button ~label:"Exact"
1930      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1931    let introsb =
1932     GButton.button ~label:"Intros"
1933      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1934    let applyb =
1935     GButton.button ~label:"Apply"
1936      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1937    let elimsimplintrosb =
1938     GButton.button ~label:"ElimSimplIntros"
1939      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1940    let elimtypeb =
1941     GButton.button ~label:"ElimType"
1942      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1943    let whdb =
1944     GButton.button ~label:"Whd"
1945      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1946    let reduceb =
1947     GButton.button ~label:"Reduce"
1948      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1949    let simplb =
1950     GButton.button ~label:"Simpl"
1951      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1952    let foldb =
1953     GButton.button ~label:"Fold"
1954      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1955    let cutb =
1956     GButton.button ~label:"Cut"
1957      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1958    let hbox4 =
1959     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1960    let changeb =
1961     GButton.button ~label:"Change"
1962      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1963    let letinb =
1964     GButton.button ~label:"Let ... In"
1965      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1966    let ringb =
1967     GButton.button ~label:"Ring"
1968      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1969    let clearbodyb =
1970     GButton.button ~label:"ClearBody"
1971      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1972    let clearb =
1973     GButton.button ~label:"Clear"
1974      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1975    let fourierb =
1976     GButton.button ~label:"Fourier"
1977      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1978    let rewritesimplb =
1979     GButton.button ~label:"RewriteSimpl ->"
1980      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1981    let reflexivityb =
1982     GButton.button ~label:"Reflexivity"
1983      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1984    let hbox5 =
1985     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1986    let symmetryb =
1987     GButton.button ~label:"Symmetry"
1988      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1989    let transitivityb =
1990     GButton.button ~label:"Transitivity"
1991      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1992    let leftb =
1993     GButton.button ~label:"Left"
1994      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1995    let rightb =
1996     GButton.button ~label:"Right"
1997      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
1998    let assumptionb =
1999     GButton.button ~label:"Assumption"
2000      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2001    ignore(exactb#connect#clicked exact) ;
2002    ignore(applyb#connect#clicked apply) ;
2003    ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2004    ignore(elimtypeb#connect#clicked elimtype) ;
2005    ignore(whdb#connect#clicked whd) ;
2006    ignore(reduceb#connect#clicked reduce) ;
2007    ignore(simplb#connect#clicked simpl) ;
2008    ignore(foldb#connect#clicked fold) ;
2009    ignore(cutb#connect#clicked cut) ;
2010    ignore(changeb#connect#clicked change) ;
2011    ignore(letinb#connect#clicked letin) ;
2012    ignore(ringb#connect#clicked ring) ;
2013    ignore(clearbodyb#connect#clicked clearbody) ;
2014    ignore(clearb#connect#clicked clear) ;
2015    ignore(fourierb#connect#clicked fourier) ;
2016    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2017    ignore(reflexivityb#connect#clicked reflexivity) ;
2018    ignore(symmetryb#connect#clicked symmetry) ;
2019    ignore(transitivityb#connect#clicked transitivity) ;
2020    ignore(leftb#connect#clicked left) ;
2021    ignore(rightb#connect#clicked right) ;
2022    ignore(assumptionb#connect#clicked assumption) ;
2023    ignore(introsb#connect#clicked intros) ;
2024    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2025   ))
2026 end
2027 ;;
2028
2029 class notebook =
2030 object(self)
2031  val notebook = GPack.notebook ()
2032  val pages = ref []
2033  val mutable skip_switch_page_event = false
2034  method notebook = notebook
2035  method add_page n =
2036   let new_page = new page () in
2037    pages := !pages @ [n,lazy (setgoal n),new_page] ;
2038    notebook#append_page
2039     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2040     new_page#content#coerce
2041  method remove_all_pages ~skip_switch_page_event:skip =
2042   List.iter (function _ -> notebook#remove_page 0) !pages ;
2043   pages := [] ;
2044   skip_switch_page_event <- skip
2045  method set_current_page ~may_skip_switch_page_event n =
2046   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2047    let new_page = notebook#page_num page#content#coerce in
2048     if may_skip_switch_page_event && new_page <> notebook#current_page then
2049      skip_switch_page_event <- true ;
2050     notebook#goto_page new_page
2051  method set_empty_page = self#add_page (-1)
2052  method proofw =
2053   let (_,_,page) = List.nth !pages notebook#current_page in
2054    page#proofw
2055  initializer
2056   ignore
2057    (notebook#connect#switch_page
2058     (function i ->
2059       let skip = skip_switch_page_event in
2060        skip_switch_page_event <- false ;
2061        if not skip then
2062         try
2063          let (metano,setgoal,page) = List.nth !pages i in
2064           ProofEngine.goal := Some metano ;
2065           Lazy.force (page#compute) ;
2066           Lazy.force setgoal
2067         with _ -> ()
2068     ))
2069 end
2070 ;;
2071
2072 (* Main window *)
2073
2074 class rendering_window output (notebook : notebook) =
2075  let window =
2076   GWindow.window ~title:"MathML viewer" ~border_width:2
2077    ~allow_shrink:false () in
2078  let vbox_for_menu = GPack.vbox ~packing:window#add () in
2079  (* menus *)
2080  let menubar = GMenu.menu_bar ~packing:vbox_for_menu#pack () in
2081  let factory0 = new GMenu.factory menubar in
2082  let accel_group = factory0#accel_group in
2083  (* file menu *)
2084  let file_menu = factory0#add_submenu "File" in
2085  let factory1 = new GMenu.factory file_menu ~accel_group in
2086  let export_to_postscript_menu_item =
2087   begin
2088    ignore
2089     (factory1#add_item "Load Unfinished Proof" ~key:GdkKeysyms._L
2090       ~callback:load) ;
2091    let save_menu_item =
2092     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
2093    in
2094    let qed_menu_item =
2095     factory1#add_item "Qed" ~key:GdkKeysyms._Q ~callback:qed in
2096    ignore
2097     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
2098    ignore (!save_set_sensitive false);
2099    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
2100    ignore (!qed_set_sensitive false);
2101    ignore (factory1#add_separator ()) ;
2102    let export_to_postscript_menu_item =
2103     factory1#add_item "Export to PostScript..." ~key:GdkKeysyms._E
2104      ~callback:(export_to_postscript output) in
2105    ignore (factory1#add_separator ()) ;
2106    ignore
2107     (factory1#add_item "Exit" ~key:GdkKeysyms._C ~callback:GMain.Main.quit) ;
2108    export_to_postscript_menu_item
2109   end in
2110  (* edit menu *)
2111  let edit_menu = factory0#add_submenu "Edit" in
2112  let factory2 = new GMenu.factory edit_menu ~accel_group in
2113  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
2114  let proveit_menu_item =
2115   factory2#add_item "Prove It" ~key:GdkKeysyms._I
2116    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
2117  in
2118  let focus_menu_item =
2119   factory2#add_item "Focus" ~key:GdkKeysyms._F
2120    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
2121  in
2122  let _ =
2123   focus_and_proveit_set_sensitive :=
2124    function b ->
2125     proveit_menu_item#misc#set_sensitive b ;
2126     focus_menu_item#misc#set_sensitive b
2127  in
2128  let _ = !focus_and_proveit_set_sensitive false in
2129  (* settings menu *)
2130  let settings_menu = factory0#add_submenu "Settings" in
2131  let factory3 = new GMenu.factory settings_menu ~accel_group in
2132  let _ =
2133   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
2134    ~callback:edit_aliases in
2135  let _ = factory3#add_separator () in
2136  let _ =
2137   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
2138    ~callback:(function _ -> (settings_window ())#show ()) in
2139  (* accel group *)
2140  let _ = window#add_accel_group accel_group in
2141  (* end of menus *)
2142  let hbox0 =
2143   GPack.hbox
2144    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
2145  let vbox =
2146   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2147  let scrolled_window0 =
2148   GBin.scrolled_window ~border_width:10
2149    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2150  let _ = scrolled_window0#add output#coerce in
2151  let frame =
2152   GBin.frame ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2153  let vbox' =
2154   GPack.vbox ~packing:frame#add () in
2155  let hbox4 =
2156   GPack.hbox ~border_width:5 ~packing:(vbox'#pack ~expand:false ~fill:false ~padding:5) () in
2157  let stateb =
2158   GButton.button ~label:"State"
2159    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2160  let openb =
2161   GButton.button ~label:"Open"
2162    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2163  let checkb =
2164   GButton.button ~label:"Check"
2165    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2166  let locateb =
2167   GButton.button ~label:"Locate"
2168    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2169  let searchpatternb =
2170   GButton.button ~label:"SearchPattern"
2171    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2172  let scrolled_window1 =
2173   GBin.scrolled_window ~border_width:5
2174    ~packing:(vbox'#pack ~expand:true ~padding:0) () in
2175  let inputt = GEdit.text ~editable:true ~width:400 ~height:100
2176    ~packing:scrolled_window1#add () in
2177  let vboxl =
2178   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
2179  let _ =
2180   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
2181  let frame =
2182   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
2183  in
2184  let outputhtml =
2185   GHtml.xmhtml
2186    ~source:"<html><body bgColor=\"white\"></body></html>"
2187    ~width:400 ~height: 100
2188    ~border_width:20
2189    ~packing:frame#add
2190    ~show:true () in
2191  let scratch_window = new scratch_window outputhtml in
2192 object
2193  method outputhtml = outputhtml
2194  method inputt = inputt
2195  method output = (output : GMathView.math_view)
2196  method notebook = notebook
2197  method show = window#show
2198  initializer
2199   notebook#set_empty_page ;
2200   export_to_postscript_menu_item#misc#set_sensitive false ;
2201   check_term := (check_term_in_scratch scratch_window) ;
2202
2203   (* signal handlers here *)
2204   ignore(output#connect#selection_changed
2205    (function elem ->
2206      choose_selection output elem ;
2207      !focus_and_proveit_set_sensitive true
2208    )) ;
2209   let settings_window = new settings_window output scrolled_window0
2210    export_to_postscript_menu_item (choose_selection output) in
2211   set_settings_window settings_window ;
2212   set_outputhtml outputhtml ;
2213   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
2214   ignore(stateb#connect#clicked state) ;
2215   ignore(openb#connect#clicked open_) ;
2216   ignore(checkb#connect#clicked (check scratch_window)) ;
2217   ignore(locateb#connect#clicked locate) ;
2218   ignore(searchpatternb#connect#clicked searchPattern) ;
2219   Logger.log_callback :=
2220    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
2221 end;;
2222
2223 (* MAIN *)
2224
2225 let initialize_everything () =
2226  let module U = Unix in
2227   let output = GMathView.math_view ~width:350 ~height:280 () in
2228   let notebook = new notebook in
2229    let rendering_window' = new rendering_window output notebook in
2230     set_rendering_window rendering_window' ;
2231     mml_of_cic_term_ref := mml_of_cic_term ;
2232     rendering_window'#show () ;
2233     GMain.Main.main ()
2234 ;;
2235
2236 let _ =
2237  if !usedb then
2238  Mqint.init "dbname=helm_mowgli" ;
2239 (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
2240  ignore (GtkMain.Main.init ()) ;
2241  initialize_everything () ;
2242  if !usedb then Mqint.close ();
2243 ;;