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