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