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