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