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 <natile@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 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
  52
  53 let htmlheader =
  54  "<html>" ^
  55  " <body bgColor=\"white\">"
  56 ;;
  57
  58 let htmlfooter =
  59  " </body>" ^
  60  "</html>"
  61 ;;
  62
  63 let prooffile = "/public/natile/currentproof";;
  64 let prooffiletype = "/public/natile/currentprooftype";;
  65
  66 (* SACERDOT
  67 let prooffile = "/public/natile/currentproof";;
  68 let prooffiletype = "/public/natile/currentprooftype";;
  69 *)
  70
  71 (* TASSI
  72 let prooffile = "//miohelm/tmp/currentproof";;
  73 let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";;
  74 *)
  75
  76 (* GALATA
  77 let prooffile = "/home/galata/miohelm/currentproof";;
  78 let prooffiletype = "/home/galata/miohelm/currentprooftype";;
  79 *)
  80
  81 (*CSC: the getter should handle the innertypes, not the FS *)
  82
  83 let innertypesfile = "/public/natile/innertypes";;
  84 let constanttypefile = "/public/natile/constanttype";;
  85
  86 (* SACERDOT
  87 let innertypesfile = "/public/natile/innertypes";;
  88 let constanttypefile = "/public/natile/constanttype";;
  89 *)
  90
  91 (* TASSI
  92 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
  93 let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";;
  94 *)
  95
  96 (* GALATA
  97 let innertypesfile = "/home/galata/miohelm/innertypes";;
  98 let constanttypefile = "/home/galata/miohelm/constanttype";;
  99 *)
 100
 101 let empty_id_to_uris = ([],function _ -> None);;
 102
 103
 104 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 105
 106 let htmlheader_and_content = ref htmlheader;;
 107
 108 let current_cic_infos = ref None;;
 109 let current_goal_infos = ref None;;
 110 let current_scratch_infos = ref None;;
 111
 112 let id_to_uris = ref empty_id_to_uris;;
 113
 114 let check_term = ref (fun _ _ _ -> assert false);;
 115 let mml_of_cic_term_ref = ref (fun _ _ -> assert false);;
 116
 117 exception RenderingWindowsNotInitialized;;
 118
 119 let set_rendering_window,rendering_window =
 120  let rendering_window_ref = ref None in
 121   (function rw -> rendering_window_ref := Some rw),
 122   (function () ->
 123     match !rendering_window_ref with
 124        None -> raise RenderingWindowsNotInitialized
 125      | Some rw -> rw
 126   )
 127 ;;
 128
 129 exception SettingsWindowsNotInitialized;;
 130
 131 let set_settings_window,settings_window =
 132  let settings_window_ref = ref None in
 133   (function rw -> settings_window_ref := Some rw),
 134   (function () ->
 135     match !settings_window_ref with
 136        None -> raise SettingsWindowsNotInitialized
 137      | Some rw -> rw
 138   )
 139 ;;
 140
 141 exception OutputHtmlNotInitialized;;
 142
 143 let set_outputhtml,outputhtml =
 144  let outputhtml_ref = ref None in
 145   (function rw -> outputhtml_ref := Some rw),
 146   (function () ->
 147     match !outputhtml_ref with
 148        None -> raise OutputHtmlNotInitialized
 149      | Some outputhtml -> outputhtml
 150   )
 151 ;;
 152
 153 exception QedSetSensitiveNotInitialized;;
 154 let qed_set_sensitive =
 155  ref (function _ -> raise QedSetSensitiveNotInitialized)
 156 ;;
 157
 158 exception SaveSetSensitiveNotInitialized;;
 159 let save_set_sensitive =
 160  ref (function _ -> raise SaveSetSensitiveNotInitialized)
 161 ;;
 162
 163 (* COMMAND LINE OPTIONS *)
 164
 165 let usedb = ref true
 166
 167 let argspec =
 168   [
 169     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
 170   ]
 171 in
 172 Arg.parse argspec ignore ""
 173
 174 (* A WIDGET TO ENTER CIC TERMS *)
 175
 176 class term_editor ?packing ?width ?height ?isnotempty_callback () =
 177  let input = GEdit.text ~editable:true ?width ?height ?packing () in
 178  let _ =
 179   match isnotempty_callback with
 180      None -> ()
 181    | Some callback ->
 182       ignore(input#connect#changed (function () -> callback (input#length > 0)))
 183  in
 184 object(self)
 185  method coerce = input#coerce
 186  method reset =
 187   input#delete_text 0 input#length
 188  (* CSC: txt is now a string, but should be of type Cic.term *)
 189  method set_term txt =
 190   self#reset ;
 191   ignore ((input#insert_text txt) ~pos:0)
 192  (* CSC: this method should disappear *)
 193  method get_as_string =
 194   input#get_chars 0 input#length
 195  method get_term ~context ~metasenv =
 196   let lexbuf = Lexing.from_string (input#get_chars 0 input#length) in
 197    CicTextualParserContext.main ~context ~metasenv CicTextualLexer.token lexbuf
 198 end
 199 ;;
 200
 201 (* MISC FUNCTIONS *)
 202
 203 exception IllFormedUri of string;;
 204
 205 let cic_textual_parser_uri_of_string uri' =
 206  try
 207   (* Constant *)
 208   if String.sub uri' (String.length uri' - 4) 4 = ".con" then
 209    CicTextualParser0.ConUri (UriManager.uri_of_string uri')
 210   else
 211    if String.sub uri' (String.length uri' - 4) 4 = ".var" then
 212     CicTextualParser0.VarUri (UriManager.uri_of_string uri')
 213    else
 214     (try
 215       (* Inductive Type *)
 216       let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
 217        CicTextualParser0.IndTyUri (uri'',typeno)
 218      with
 219       _ ->
 220        (* Constructor of an Inductive Type *)
 221        let uri'',typeno,consno =
 222         CicTextualLexer.indconuri_of_uri uri'
 223        in
 224         CicTextualParser0.IndConUri (uri'',typeno,consno)
 225     )
 226  with
 227   _ -> raise (IllFormedUri uri')
 228 ;;
 229
 230 let term_of_cic_textual_parser_uri uri =
 231  let module C = Cic in
 232  let module CTP = CicTextualParser0 in
 233   match uri with
 234      CTP.ConUri uri -> C.Const (uri,[])
 235    | CTP.VarUri uri -> C.Var (uri,[])
 236    | CTP.IndTyUri (uri,tyno) -> C.MutInd (uri,tyno,[])
 237    | CTP.IndConUri (uri,tyno,consno) -> C.MutConstruct (uri,tyno,consno,[])
 238 ;;
 239
 240 let string_of_cic_textual_parser_uri uri =
 241  let module C = Cic in
 242  let module CTP = CicTextualParser0 in
 243   let uri' =
 244    match uri with
 245       CTP.ConUri uri -> UriManager.string_of_uri uri
 246     | CTP.VarUri uri -> UriManager.string_of_uri uri
 247     | CTP.IndTyUri (uri,tyno) ->
 248        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
 249     | CTP.IndConUri (uri,tyno,consno) ->
 250        UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
 251         string_of_int consno
 252   in
 253    (* 4 = String.length "cic:" *)
 254    String.sub uri' 4 (String.length uri' - 4)
 255 ;;
 256
 257 let output_html outputhtml msg =
 258  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 259  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 260  outputhtml#set_topline (-1)
 261 ;;
 262
 263 (* UTILITY FUNCTIONS TO DISAMBIGUATE AN URI *)
 264
 265 (* Check window *)
 266
 267 let check_window outputhtml uris =
 268  let window =
 269   GWindow.window
 270    ~width:800 ~modal:true ~title:"Check" ~border_width:2 () in
 271  let notebook =
 272   GPack.notebook ~scrollable:true ~packing:window#add () in
 273  window#show () ;
 274  let render_terms =
 275   List.map
 276    (function uri ->
 277      let scrolled_window =
 278       GBin.scrolled_window ~border_width:10
 279        ~packing:
 280          (notebook#append_page ~tab_label:((GMisc.label ~text:uri ())#coerce))
 281        ()
 282      in
 283       lazy
 284        (let mmlwidget =
 285          GMathView.math_view
 286           ~packing:scrolled_window#add ~width:400 ~height:280 () in
 287         let expr =
 288          let term =
 289           term_of_cic_textual_parser_uri (cic_textual_parser_uri_of_string uri)
 290          in
 291           (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
 292         in
 293          try
 294           let mml = !mml_of_cic_term_ref 111 expr in
 295 prerr_endline ("### " ^ CicPp.ppterm expr) ;
 296            mmlwidget#load_tree ~dom:mml
 297          with
 298           e ->
 299            output_html outputhtml
 300             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 301        )
 302    ) uris
 303  in
 304   ignore
 305    (notebook#connect#switch_page
 306      (function i -> Lazy.force (List.nth render_terms i)))
 307 ;;
 308
 309 exception NoChoice;;
 310
 311 let
 312  interactive_user_uri_choice ~selection_mode ?(ok="Ok") ~title ~msg uris
 313 =
 314  let choices = ref [] in
 315  let chosen = ref false in
 316  let window =
 317   GWindow.dialog ~modal:true ~title ~width:600 () in
 318  let lMessage =
 319   GMisc.label ~text:msg
 320    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 321  let scrolled_window =
 322   GBin.scrolled_window ~border_width:10
 323    ~packing:(window#vbox#pack ~expand:true ~fill:true ~padding:5) () in
 324  let clist =
 325   let expected_height = 18 * List.length uris in
 326    let height = if expected_height > 400 then 400 else expected_height in
 327     GList.clist ~columns:1 ~packing:scrolled_window#add
 328      ~height ~selection_mode () in
 329  let _ = List.map (function x -> clist#append [x]) uris in
 330  let hbox2 =
 331   GPack.hbox ~border_width:0
 332    ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
 333  let explain_label =
 334   GMisc.label ~text:"None of the above. Try this one:"
 335    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 336  let manual_input =
 337   GEdit.entry ~editable:true
 338    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
 339  let hbox =
 340   GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
 341  let okb =
 342   GButton.button ~label:ok
 343    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 344  let _ = okb#misc#set_sensitive false in
 345  let checkb =
 346   GButton.button ~label:"Check"
 347    ~packing:(hbox#pack ~padding:5) () in
 348  let _ = checkb#misc#set_sensitive false in
 349  let cancelb =
 350   GButton.button ~label:"Abort"
 351    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 352  (* actions *)
 353  let check_callback () =
 354   assert (List.length !choices > 0) ;
 355   check_window (outputhtml ()) !choices
 356  in
 357   ignore (window#connect#destroy GMain.Main.quit) ;
 358   ignore (cancelb#connect#clicked window#destroy) ;
 359   ignore
 360    (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 361   ignore (checkb#connect#clicked check_callback) ;
 362   ignore
 363    (clist#connect#select_row
 364      (fun ~row ~column ~event ->
 365        checkb#misc#set_sensitive true ;
 366        okb#misc#set_sensitive true ;
 367        choices := (List.nth uris row)::!choices)) ;
 368   ignore
 369    (clist#connect#unselect_row
 370      (fun ~row ~column ~event ->
 371        choices :=
 372         List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
 373   ignore
 374    (manual_input#connect#changed
 375      (fun _ ->
 376        if manual_input#text = "" then
 377         begin
 378          choices := [] ;
 379          checkb#misc#set_sensitive false ;
 380          okb#misc#set_sensitive false ;
 381          clist#misc#set_sensitive true
 382         end
 383        else
 384         begin
 385          choices := [manual_input#text] ;
 386          clist#unselect_all () ;
 387          checkb#misc#set_sensitive true ;
 388          okb#misc#set_sensitive true ;
 389          clist#misc#set_sensitive false
 390         end));
 391   window#set_position `CENTER ;
 392   window#show () ;
 393   GMain.Main.main () ;
 394   if !chosen && List.length !choices > 0 then
 395    !choices
 396   else
 397    raise NoChoice
 398 ;;
 399
 400 let interactive_interpretation_choice interpretations =
 401  let chosen = ref None in
 402  let window =
 403   GWindow.window
 404    ~modal:true ~title:"Ambiguous well-typed input." ~border_width:2 () in
 405  let vbox = GPack.vbox ~packing:window#add () in
 406  let lMessage =
 407   GMisc.label
 408    ~text:
 409     ("Ambiguous input since there are many well-typed interpretations." ^
 410      " Please, choose one of them.")
 411    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 412  let notebook =
 413   GPack.notebook ~scrollable:true
 414    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 415  let _ =
 416   List.map
 417    (function interpretation ->
 418      let clist =
 419       let expected_height = 18 * List.length interpretation in
 420        let height = if expected_height > 400 then 400 else expected_height in
 421         GList.clist ~columns:2 ~packing:notebook#append_page ~height
 422          ~titles:["id" ; "URI"] ()
 423      in
 424       ignore
 425        (List.map
 426          (function (id,uri) ->
 427            let n = clist#append [id;uri] in
 428             clist#set_row ~selectable:false n
 429          ) interpretation
 430        ) ;
 431       clist#columns_autosize ()
 432    ) interpretations in
 433  let hbox =
 434   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 435  let okb =
 436   GButton.button ~label:"Ok"
 437    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 438  let cancelb =
 439   GButton.button ~label:"Abort"
 440    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 441  (* actions *)
 442  ignore (window#connect#destroy GMain.Main.quit) ;
 443  ignore (cancelb#connect#clicked window#destroy) ;
 444  ignore
 445   (okb#connect#clicked
 446     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
 447  window#set_position `CENTER ;
 448  window#show () ;
 449  GMain.Main.main () ;
 450  match !chosen with
 451     None -> raise NoChoice
 452   | Some n -> n
 453 ;;
 454
 455
 456 (* MISC FUNCTIONS *)
 457
 458 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
 459 let get_last_query =
 460  let query = ref "" in
 461   MQueryGenerator.set_confirm_query
 462    (function q -> query := MQueryUtil.text_of_query q ; true) ;
 463   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
 464 ;;
 465
 466 let domImpl = Gdome.domImplementation ();;
 467
 468 let parseStyle name =
 469  let style =
 470   domImpl#createDocumentFromURI
 471 (*
 472    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 473 *)
 474    ~uri:("styles/" ^ name) ()
 475  in
 476   Gdome_xslt.processStylesheet style
 477 ;;
 478
 479 let d_c = parseStyle "drop_coercions.xsl";;
 480 let tc1 = parseStyle "objtheorycontent.xsl";;
 481 let hc2 = parseStyle "content_to_html.xsl";;
 482 let l   = parseStyle "link.xsl";;
 483
 484 let c1 = parseStyle "rootcontent.xsl";;
 485 let g  = parseStyle "genmmlid.xsl";;
 486 let c2 = parseStyle "annotatedpres.xsl";;
 487
 488
 489 let getterURL = Configuration.getter_url;;
 490 let processorURL = Configuration.processor_url;;
 491
 492 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 493 let mml_args ~explode_all =
 494  ("explodeall",(if explode_all then "true()" else "false()"))::
 495   ["processorURL", "'" ^ processorURL ^ "'" ;
 496    "getterURL", "'" ^ getterURL ^ "'" ;
 497    "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 498    "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 499    "UNICODEvsSYMBOL", "'symbol'" ;
 500    "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 501    "encoding", "'iso-8859-1'" ;
 502    "media-type", "'text/html'" ;
 503    "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 504    "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 505    "naturalLanguage", "'yes'" ;
 506    "annotations", "'no'" ;
 507    "URLs_or_URIs", "'URIs'" ;
 508    "topurl", "'http://phd.cs.unibo.it/helm'" ;
 509    "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 510 ;;
 511
 512 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 513 let sequent_args =
 514  ["processorURL", "'" ^ processorURL ^ "'" ;
 515   "getterURL", "'" ^ getterURL ^ "'" ;
 516   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 517   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 518   "UNICODEvsSYMBOL", "'symbol'" ;
 519   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 520   "encoding", "'iso-8859-1'" ;
 521   "media-type", "'text/html'" ;
 522   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 523   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 524   "naturalLanguage", "'no'" ;
 525   "annotations", "'no'" ;
 526   "explodeall", "true()" ;
 527   "URLs_or_URIs", "'URIs'" ;
 528   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 529   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 530 ;;
 531
 532 let parse_file filename =
 533  let inch = open_in filename in
 534   let rec read_lines () =
 535    try
 536     let line = input_line inch in
 537      line ^ read_lines ()
 538    with
 539     End_of_file -> ""
 540   in
 541    read_lines ()
 542 ;;
 543
 544 let applyStylesheets input styles args =
 545  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 546   input styles
 547 ;;
 548
 549 let
 550  mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types
 551 =
 552 (*CSC: ????????????????? *)
 553  let xml, bodyxml =
 554   Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true
 555    annobj
 556  in
 557  let xmlinnertypes =
 558   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 559    ~ask_dtd_to_the_getter:true
 560  in
 561   let input =
 562    match bodyxml with
 563       None -> Xml2Gdome.document_of_xml domImpl xml
 564     | Some bodyxml' ->
 565        Xml.pp xml (Some constanttypefile) ;
 566        Xml2Gdome.document_of_xml domImpl bodyxml'
 567   in
 568 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 569 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 570 (*CSC: local.                                                              *)
 571    Xml.pp xmlinnertypes (Some innertypesfile) ;
 572    let output = applyStylesheets input mml_styles (mml_args ~explode_all) in
 573     output
 574 ;;
 575
 576 let
 577  save_object_to_disk uri annobj ids_to_inner_sorts ids_to_inner_types pathname
 578 =
 579  let name =
 580   let struri = UriManager.string_of_uri uri in
 581   let idx = (String.rindex struri '/') + 1 in
 582    String.sub struri idx (String.length struri - idx)
 583  in
 584   let path = pathname ^ "/" ^ name in
 585   let xml, bodyxml =
 586    Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:false
 587     annobj
 588   in
 589   let xmlinnertypes =
 590    Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types
 591     ~ask_dtd_to_the_getter:false
 592   in
 593    (* innertypes *)
 594    let innertypesuri = UriManager.innertypesuri_of_uri uri in
 595     Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
 596     Getter.register innertypesuri
 597      (Configuration.annotations_url ^
 598        Str.replace_first (Str.regexp "^cic:") ""
 599         (UriManager.string_of_uri innertypesuri) ^ ".xml"
 600      ) ;
 601     (* constant type / variable / mutual inductive types definition *)
 602     Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
 603     Getter.register uri
 604      (Configuration.annotations_url ^
 605        Str.replace_first (Str.regexp "^cic:") ""
 606         (UriManager.string_of_uri uri) ^ ".xml"
 607      ) ;
 608     match bodyxml with
 609        None -> ()
 610      | Some bodyxml' ->
 611         (* constant body *)
 612         let bodyuri =
 613          match UriManager.bodyuri_of_uri uri with
 614             None -> assert false
 615           | Some bodyuri -> bodyuri
 616         in
 617          Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
 618          Getter.register bodyuri
 619           (Configuration.annotations_url ^
 620             Str.replace_first (Str.regexp "^cic:") ""
 621              (UriManager.string_of_uri bodyuri) ^ ".xml"
 622           )
 623 ;;
 624
 625
 626 (* CALLBACKS *)
 627
 628 exception RefreshSequentException of exn;;
 629 exception RefreshProofException of exn;;
 630
 631 let refresh_proof (output : GMathView.math_view) =
 632  try
 633   let uri,currentproof =
 634    match !ProofEngine.proof with
 635       None -> assert false
 636     | Some (uri,metasenv,bo,ty) ->
 637        !qed_set_sensitive (List.length metasenv = 0) ;
 638        (*CSC: Wrong: [] is just plainly wrong *)
 639        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
 640   in
 641    let
 642     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 643      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 644    =
 645     Cic2acic.acic_object_of_cic_object currentproof
 646    in
 647     let mml =
 648      mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts
 649       ids_to_inner_types
 650     in
 651      output#load_tree mml ;
 652      current_cic_infos :=
 653       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 654  with
 655   e ->
 656  match !ProofEngine.proof with
 657     None -> assert false
 658   | Some (uri,metasenv,bo,ty) ->
 659 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
 660    raise (RefreshProofException e)
 661 ;;
 662
 663 let refresh_sequent ?(empty_notebook=true) notebook =
 664  try
 665   match !ProofEngine.goal with
 666      None ->
 667       if empty_notebook then
 668        begin
 669         notebook#remove_all_pages ~skip_switch_page_event:false ;
 670         notebook#set_empty_page
 671        end
 672       else
 673        notebook#proofw#unload
 674    | Some metano ->
 675       let metasenv =
 676        match !ProofEngine.proof with
 677           None -> assert false
 678         | Some (_,metasenv,_,_) -> metasenv
 679       in
 680       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 681        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 682         SequentPp.XmlPp.print_sequent metasenv currentsequent
 683        in
 684         let regenerate_notebook () =
 685          let skip_switch_page_event =
 686           match metasenv with
 687              (m,_,_)::_ when m = metano -> false
 688            | _ -> true
 689          in
 690           notebook#remove_all_pages ~skip_switch_page_event ;
 691           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
 692         in
 693           if empty_notebook then
 694            begin
 695             regenerate_notebook () ;
 696             notebook#set_current_page ~may_skip_switch_page_event:false metano
 697            end
 698           else
 699            begin
 700             let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
 701             let sequent_mml =
 702              applyStylesheets sequent_doc sequent_styles sequent_args
 703             in
 704              notebook#set_current_page ~may_skip_switch_page_event:true metano;
 705              notebook#proofw#load_tree ~dom:sequent_mml
 706            end ;
 707           current_goal_infos :=
 708            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 709  with
 710   e ->
 711 let metano =
 712   match !ProofEngine.goal with
 713      None -> assert false
 714    | Some m -> m
 715 in
 716 let metasenv =
 717  match !ProofEngine.proof with
 718     None -> assert false
 719   | Some (_,metasenv,_,_) -> metasenv
 720 in
 721 try
 722 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 723 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 724    raise (RefreshSequentException e)
 725 with Not_found -> prerr_endline ("Offending sequent " ^ string_of_int metano ^ " unkown."); 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 exception OpenConjecturesStillThere;;
 763 exception WrongProof;;
 764
 765 let pathname_of_annuri uristring =
 766  Configuration.annotations_dir ^
 767   Str.replace_first (Str.regexp "^cic:") "" uristring
 768 ;;
 769
 770 let make_dirs dirpath =
 771  ignore (Unix.system ("mkdir -p " ^ dirpath))
 772 ;;
 773
 774 let save_obj uri obj =
 775  let
 776   (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 777    ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 778  =
 779   Cic2acic.acic_object_of_cic_object obj
 780  in
 781   (* let's save the theorem and register it to the getter *)
 782   let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
 783    make_dirs pathname ;
 784    save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
 785     pathname
 786 ;;
 787
 788 let qed () =
 789  match !ProofEngine.proof with
 790     None -> assert false
 791   | Some (uri,[],bo,ty) ->
 792      if
 793       CicReduction.are_convertible []
 794        (CicTypeChecker.type_of_aux' [] [] bo) ty
 795      then
 796       begin
 797        (*CSC: Wrong: [] is just plainly wrong *)
 798        let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
 799         let
 800          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 801           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 802         =
 803          Cic2acic.acic_object_of_cic_object proof
 804         in
 805          let mml =
 806           mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
 807            ids_to_inner_types
 808          in
 809           ((rendering_window ())#output : GMathView.math_view)#load_tree mml ;
 810           !qed_set_sensitive false ;
 811           (* let's save the theorem and register it to the getter *)
 812           let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
 813           make_dirs pathname ;
 814           save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
 815            pathname ;
 816           current_cic_infos :=
 817            Some
 818             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
 819              ids_to_hypotheses)
 820       end
 821      else
 822       raise WrongProof
 823   | _ -> raise OpenConjecturesStillThere
 824 ;;
 825
 826 let save () =
 827  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 828   match !ProofEngine.proof with
 829      None -> assert false
 830    | Some (uri, metasenv, bo, ty) ->
 831       let currentproof =
 832        (*CSC: Wrong: [] is just plainly wrong *)
 833        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
 834       in
 835        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
 836         Cic2acic.acic_object_of_cic_object currentproof
 837        in
 838         let xml, bodyxml =
 839          match
 840           Cic2Xml.print_object uri ~ids_to_inner_sorts
 841            ~ask_dtd_to_the_getter:true acurrentproof
 842          with
 843             xml,Some bodyxml -> xml,bodyxml
 844           | _,None -> assert false
 845         in
 846          Xml.pp ~quiet:true xml (Some prooffiletype) ;
 847          output_html outputhtml
 848           ("<h1 color=\"Green\">Current proof type saved to " ^
 849            prooffiletype ^ "</h1>") ;
 850          Xml.pp ~quiet:true bodyxml (Some prooffile) ;
 851          output_html outputhtml
 852           ("<h1 color=\"Green\">Current proof body saved to " ^
 853            prooffile ^ "</h1>")
 854 ;;
 855
 856 (* Used to typecheck the loaded proofs *)
 857 let typecheck_loaded_proof metasenv bo ty =
 858  let module T = CicTypeChecker in
 859   ignore (
 860    List.fold_left
 861     (fun metasenv ((_,context,ty) as conj) ->
 862       ignore (T.type_of_aux' metasenv context ty) ;
 863       metasenv @ [conj]
 864     ) [] metasenv) ;
 865   ignore (T.type_of_aux' metasenv [] ty) ;
 866   ignore (T.type_of_aux' metasenv [] bo)
 867 ;;
 868
 869 let load () =
 870  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 871  let output = ((rendering_window ())#output : GMathView.math_view) in
 872  let notebook = (rendering_window ())#notebook in
 873   try
 874    match
 875     GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
 876      "Choose an URI:"
 877    with
 878       None -> raise NoChoice
 879     | Some uri0 ->
 880        let uri = UriManager.uri_of_string ("cic:" ^ uri0) in
 881         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
 882            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
 883             typecheck_loaded_proof metasenv bo ty ;
 884             ProofEngine.proof :=
 885              Some (uri, metasenv, bo, ty) ;
 886             ProofEngine.goal :=
 887              (match metasenv with
 888                  [] -> None
 889                | (metano,_,_)::_ -> Some metano
 890              ) ;
 891             refresh_proof output ;
 892             refresh_sequent notebook ;
 893              output_html outputhtml
 894               ("<h1 color=\"Green\">Current proof type loaded from " ^
 895                 prooffiletype ^ "</h1>") ;
 896              output_html outputhtml
 897               ("<h1 color=\"Green\">Current proof body loaded from " ^
 898                 prooffile ^ "</h1>") ;
 899             !save_set_sensitive true
 900          | _ -> assert false
 901   with
 902      RefreshSequentException e ->
 903       output_html outputhtml
 904        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 905         "sequent: " ^ Printexc.to_string e ^ "</h1>")
 906    | RefreshProofException e ->
 907       output_html outputhtml
 908        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 909         "proof: " ^ Printexc.to_string e ^ "</h1>")
 910    | e ->
 911       output_html outputhtml
 912        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 913 ;;
 914
 915 let edit_aliases () =
 916  let chosen = ref false in
 917  let window =
 918   GWindow.window
 919    ~width:400 ~modal:true ~title:"Edit Aliases..." ~border_width:2 () in
 920  let vbox =
 921   GPack.vbox ~border_width:0 ~packing:window#add () in
 922  let scrolled_window =
 923   GBin.scrolled_window ~border_width:10
 924    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
 925  let input = GEdit.text ~editable:true ~width:400 ~height:100
 926    ~packing:scrolled_window#add () in
 927  let hbox =
 928   GPack.hbox ~border_width:0
 929    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 930  let okb =
 931   GButton.button ~label:"Ok"
 932    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 933  let cancelb =
 934   GButton.button ~label:"Cancel"
 935    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 936  ignore (window#connect#destroy GMain.Main.quit) ;
 937  ignore (cancelb#connect#clicked window#destroy) ;
 938  ignore
 939   (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
 940  let dom,resolve_id = !id_to_uris in
 941   ignore
 942    (input#insert_text ~pos:0
 943     (String.concat "\n"
 944       (List.map
 945         (function v ->
 946           let uri =
 947            match resolve_id v with
 948               None -> assert false
 949             | Some uri -> uri
 950           in
 951            "alias " ^ v ^ " " ^
 952              (string_of_cic_textual_parser_uri uri)
 953         ) dom))) ;
 954   window#show () ;
 955   GMain.Main.main () ;
 956   if !chosen then
 957    let dom,resolve_id =
 958     let inputtext = input#get_chars 0 input#length in
 959     let regexpr =
 960      let alfa = "[a-zA-Z_-]" in
 961      let digit = "[0-9]" in
 962      let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in
 963      let blanks = "\( \|\t\|\n\)+" in
 964      let nonblanks = "[^ \t\n]+" in
 965      let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *)
 966       Str.regexp
 967        ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)")
 968     in
 969      let rec aux n =
 970       try
 971        let n' = Str.search_forward regexpr inputtext n in
 972         let id = Str.matched_group 2 inputtext in
 973         let uri =
 974          cic_textual_parser_uri_of_string
 975           ("cic:" ^ (Str.matched_group 5 inputtext))
 976         in
 977          let dom,resolve_id = aux (n' + 1) in
 978           if List.mem id dom then
 979            dom,resolve_id
 980           else
 981            id::dom,
 982             (function id' -> if id = id' then Some uri else resolve_id id')
 983       with
 984        Not_found -> empty_id_to_uris
 985      in
 986       aux 0
 987    in
 988     id_to_uris := dom,resolve_id
 989 ;;
 990
 991 let proveit () =
 992  let module L = LogicalOperations in
 993  let module G = Gdome in
 994  let notebook = (rendering_window ())#notebook in
 995  let output = (rendering_window ())#output in
 996  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
 997   match (rendering_window ())#output#get_selection with
 998     Some node ->
 999      let xpath =
1000       ((node : Gdome.element)#getAttributeNS
1001       (*CSC: OCAML DIVERGE
1002       ((element : G.element)#getAttributeNS
1003       *)
1004         ~namespaceURI:helmns
1005         ~localName:(G.domString "xref"))#to_string
1006      in
1007       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1008       else
1009        begin
1010         try
1011          match !current_cic_infos with
1012             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1013              let id = xpath in
1014               L.to_sequent id ids_to_terms ids_to_father_ids ;
1015               refresh_proof output ;
1016               refresh_sequent notebook
1017           | None -> assert false (* "ERROR: No current term!!!" *)
1018         with
1019            RefreshSequentException e ->
1020             output_html outputhtml
1021              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1022               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1023          | RefreshProofException e ->
1024             output_html outputhtml
1025              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1026               "proof: " ^ Printexc.to_string e ^ "</h1>")
1027          | e ->
1028             output_html outputhtml
1029              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1030        end
1031   | None -> assert false (* "ERROR: No selection!!!" *)
1032 ;;
1033
1034 let focus () =
1035  let module L = LogicalOperations in
1036  let module G = Gdome in
1037  let notebook = (rendering_window ())#notebook in
1038  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1039   match (rendering_window ())#output#get_selection with
1040     Some node ->
1041      let xpath =
1042       ((node : Gdome.element)#getAttributeNS
1043       (*CSC: OCAML DIVERGE
1044       ((element : G.element)#getAttributeNS
1045       *)
1046         ~namespaceURI:helmns
1047         ~localName:(G.domString "xref"))#to_string
1048      in
1049       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
1050       else
1051        begin
1052         try
1053          match !current_cic_infos with
1054             Some (ids_to_terms, ids_to_father_ids, _, _) ->
1055              let id = xpath in
1056               L.focus id ids_to_terms ids_to_father_ids ;
1057               refresh_sequent notebook
1058           | None -> assert false (* "ERROR: No current term!!!" *)
1059         with
1060            RefreshSequentException e ->
1061             output_html outputhtml
1062              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1063               "sequent: " ^ Printexc.to_string e ^ "</h1>")
1064          | RefreshProofException e ->
1065             output_html outputhtml
1066              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1067               "proof: " ^ Printexc.to_string e ^ "</h1>")
1068          | e ->
1069             output_html outputhtml
1070              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1071        end
1072   | None -> assert false (* "ERROR: No selection!!!" *)
1073 ;;
1074
1075 exception NoPrevGoal;;
1076 exception NoNextGoal;;
1077
1078 let setgoal metano =
1079  let module L = LogicalOperations in
1080  let module G = Gdome in
1081  let notebook = (rendering_window ())#notebook in
1082  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1083   let metasenv =
1084    match !ProofEngine.proof with
1085       None -> assert false
1086     | Some (_,metasenv,_,_) -> metasenv
1087   in
1088    try
1089     refresh_sequent ~empty_notebook:false notebook
1090    with
1091       RefreshSequentException e ->
1092        output_html outputhtml
1093         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1094          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1095     | e ->
1096        output_html outputhtml
1097         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1098 ;;
1099
1100 let
1101  show_in_show_window_obj, show_in_show_window_uri, show_in_show_window_callback
1102 =
1103  let window =
1104   GWindow.window ~width:800 ~border_width:2 () in
1105  let scrolled_window =
1106   GBin.scrolled_window ~border_width:10 ~packing:window#add () in
1107  let mmlwidget =
1108   GMathView.math_view ~packing:scrolled_window#add ~width:600 ~height:400 () in
1109  let _ = window#event#connect#delete (fun _ -> window#misc#hide () ; true ) in
1110  let href = Gdome.domString "href" in
1111   let show_in_show_window_obj uri obj =
1112    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1113     try
1114      let
1115       (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
1116        ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
1117      =
1118       Cic2acic.acic_object_of_cic_object obj
1119      in
1120       let mml =
1121        mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts
1122         ids_to_inner_types
1123       in
1124        window#set_title (UriManager.string_of_uri uri) ;
1125        window#misc#hide () ; window#show () ;
1126        mmlwidget#load_tree mml ;
1127     with
1128      e ->
1129       output_html outputhtml
1130        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1131   in
1132   let show_in_show_window_uri uri =
1133    CicTypeChecker.typecheck uri ;
1134    let obj = CicEnvironment.get_cooked_obj uri in
1135     show_in_show_window_obj uri obj
1136   in
1137    let show_in_show_window_callback mmlwidget (n : Gdome.element) =
1138     if n#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
1139      let uri =
1140       (n#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
1141      in
1142       show_in_show_window_uri (UriManager.uri_of_string uri)
1143     else
1144      if mmlwidget#get_action <> None then
1145       mmlwidget#action_toggle
1146    in
1147     let _ =
1148      mmlwidget#connect#clicked (show_in_show_window_callback mmlwidget)
1149     in
1150      show_in_show_window_obj, show_in_show_window_uri,
1151       show_in_show_window_callback
1152 ;;
1153
1154 exception NoObjectsLocated;;
1155
1156 let user_uri_choice ~title ~msg uris =
1157  let uri =
1158   match uris with
1159      [] -> raise NoObjectsLocated
1160    | [uri] -> uri
1161    | uris ->
1162       match
1163        interactive_user_uri_choice ~selection_mode:`SINGLE ~title ~msg uris
1164       with
1165          [uri] -> uri
1166        | _ -> assert false
1167  in
1168   String.sub uri 4 (String.length uri - 4)
1169 ;;
1170
1171 let locate_callback id =
1172  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1173  let result = MQueryGenerator.locate id in
1174  let uris =
1175   List.map
1176    (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1177    result in
1178  let html =
1179   (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>")
1180  in
1181   output_html outputhtml html ;
1182   user_uri_choice ~title:"Ambiguous input."
1183    ~msg:
1184      ("Ambiguous input \"" ^ id ^
1185       "\". Please, choose one interpetation:")
1186    uris
1187 ;;
1188
1189 let locate () =
1190  let inputt = ((rendering_window ())#inputt : term_editor) in
1191  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1192    try
1193     match
1194      GToolbox.input_string ~title:"Locate" "Enter an identifier to locate:"
1195     with
1196        None -> raise NoChoice
1197      | Some input ->
1198         let uri = locate_callback input in
1199          inputt#set_term uri
1200    with
1201     e ->
1202      output_html outputhtml
1203       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1204 ;;
1205
1206 let input_or_locate_uri ~title =
1207  let uri = ref None in
1208  let window =
1209   GWindow.window
1210    ~width:400 ~modal:true ~title ~border_width:2 () in
1211  let vbox = GPack.vbox ~packing:window#add () in
1212  let hbox1 =
1213   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1214  let _ =
1215   GMisc.label ~text:"Enter a valid URI:" ~packing:(hbox1#pack ~padding:5) () in
1216  let manual_input =
1217   GEdit.entry ~editable:true
1218    ~packing:(hbox1#pack ~expand:true ~fill:true ~padding:5) () in
1219  let checkb =
1220   GButton.button ~label:"Check"
1221    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1222  let _ = checkb#misc#set_sensitive false in
1223  let hbox2 =
1224   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1225  let _ =
1226   GMisc.label ~text:"You can also enter an indentifier to locate:"
1227    ~packing:(hbox2#pack ~padding:5) () in
1228  let locate_input =
1229   GEdit.entry ~editable:true
1230    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1231  let locateb =
1232   GButton.button ~label:"Locate"
1233    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1234  let _ = locateb#misc#set_sensitive false in
1235  let hbox3 =
1236   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1237  let okb =
1238   GButton.button ~label:"Ok"
1239    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1240  let _ = okb#misc#set_sensitive false in
1241  let cancelb =
1242   GButton.button ~label:"Cancel"
1243    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) ()
1244  in
1245   ignore (window#connect#destroy GMain.Main.quit) ;
1246   ignore
1247    (cancelb#connect#clicked (function () -> uri := None ; window#destroy ())) ;
1248   let check_callback () =
1249    let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1250    let uri = "cic:" ^ manual_input#text in
1251     try
1252       ignore (Getter.resolve (UriManager.uri_of_string uri)) ;
1253       output_html outputhtml "<h1 color=\"Green\">OK</h1>" ;
1254       true
1255     with
1256        Getter.Unresolved ->
1257         output_html outputhtml
1258          ("<h1 color=\"Red\">URI " ^ uri ^
1259           " does not correspond to any object.</h1>") ;
1260         false
1261      | UriManager.IllFormedUri _ ->
1262         output_html outputhtml
1263          ("<h1 color=\"Red\">URI " ^ uri ^ " is not well-formed.</h1>") ;
1264         false
1265      | e ->
1266         output_html outputhtml
1267          ("<h1 color=\"Red\">" ^ Printexc.to_string e ^ "</h1>") ;
1268         false
1269   in
1270   ignore
1271    (okb#connect#clicked
1272      (function () ->
1273        if check_callback () then
1274         begin
1275          uri := Some manual_input#text ;
1276          window#destroy ()
1277         end
1278    )) ;
1279   ignore (checkb#connect#clicked (function () -> ignore (check_callback ()))) ;
1280   ignore
1281    (manual_input#connect#changed
1282      (fun _ ->
1283        if manual_input#text = "" then
1284         begin
1285          checkb#misc#set_sensitive false ;
1286          okb#misc#set_sensitive false
1287         end
1288        else
1289         begin
1290          checkb#misc#set_sensitive true ;
1291          okb#misc#set_sensitive true
1292         end));
1293   ignore
1294    (locate_input#connect#changed
1295      (fun _ -> locateb#misc#set_sensitive (locate_input#text <> ""))) ;
1296   ignore
1297    (locateb#connect#clicked
1298      (function () ->
1299        let id = locate_input#text in
1300         manual_input#set_text (locate_callback id) ;
1301         locate_input#delete_text 0 (String.length id)
1302    )) ;
1303   window#show () ;
1304   GMain.Main.main () ;
1305   match !uri with
1306      None -> raise NoChoice
1307    | Some uri -> UriManager.uri_of_string ("cic:" ^ uri)
1308 ;;
1309
1310 let locate_one_id id =
1311  let result = MQueryGenerator.locate id in
1312  let uris =
1313   List.map
1314    (function uri,_ ->
1315      wrong_xpointer_format_from_wrong_xpointer_format' uri
1316    ) result in
1317  let html= " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>" in
1318   output_html (rendering_window ())#outputhtml html ;
1319   let uris' =
1320    match uris with
1321       [] ->
1322        [UriManager.string_of_uri
1323          (input_or_locate_uri ~title:("URI matching \"" ^ id ^ "\" unknown."))]
1324     | [uri] -> [uri]
1325     | _ ->
1326       interactive_user_uri_choice
1327        ~selection_mode:`EXTENDED
1328        ~ok:"Try every selection."
1329        ~title:"Ambiguous input."
1330        ~msg:
1331          ("Ambiguous input \"" ^ id ^
1332           "\". Please, choose one or more interpretations:")
1333        uris
1334   in
1335    List.map cic_textual_parser_uri_of_string uris'
1336 ;;
1337
1338 exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput;;
1339 exception AmbiguousInput;;
1340
1341 let disambiguate_input context metasenv dom mk_metasenv_and_expr =
1342  let known_ids,resolve_id = !id_to_uris in
1343  let dom' =
1344   let rec filter =
1345    function
1346       [] -> []
1347     | he::tl ->
1348        if List.mem he known_ids then filter tl else he::(filter tl)
1349   in
1350    filter dom
1351  in
1352   (* for each id in dom' we get the list of uris associated to it *)
1353   let list_of_uris = List.map locate_one_id dom' in
1354   (* and now we compute the list of all possible assignments from id to uris *)
1355   let resolve_ids =
1356    let rec aux ids list_of_uris =
1357     match ids,list_of_uris with
1358        [],[] -> [resolve_id]
1359      | id::idtl,uris::uristl ->
1360         let resolves = aux idtl uristl in
1361          List.concat
1362           (List.map
1363             (function uri ->
1364               List.map
1365                (function f ->
1366                  function id' -> if id = id' then Some uri else f id'
1367                ) resolves
1368             ) uris
1369           )
1370      | _,_ -> assert false
1371    in
1372     aux dom' list_of_uris
1373   in
1374    let tests_no = List.length resolve_ids in
1375     if tests_no > 1 then
1376      output_html (outputhtml ())
1377       ("<h1>Disambiguation phase started: " ^
1378         string_of_int (List.length resolve_ids) ^ " cases will be tried.") ;
1379    (* now we select only the ones that generates well-typed terms *)
1380    let resolve_ids' =
1381     let rec filter =
1382      function
1383         [] -> []
1384       | resolve::tl ->
1385          let metasenv',expr = mk_metasenv_and_expr resolve in
1386           try
1387 (*CSC: Bug here: we do not try to typecheck also the metasenv' *)
1388            ignore
1389             (CicTypeChecker.type_of_aux' metasenv context expr) ;
1390            resolve::(filter tl)
1391           with
1392            _ -> filter tl
1393     in
1394      filter resolve_ids
1395    in
1396     let resolve_id' =
1397      match resolve_ids' with
1398         [] -> raise ThereDoesNotExistAnyWellTypedInterpretationOfTheInput
1399       | [resolve_id] -> resolve_id
1400       | _ ->
1401         let choices =
1402          List.map
1403           (function resolve ->
1404             List.map
1405              (function id ->
1406                id,
1407                 match resolve id with
1408                    None -> assert false
1409                  | Some uri ->
1410                     match uri with
1411                        CicTextualParser0.ConUri uri
1412                      | CicTextualParser0.VarUri uri ->
1413                         UriManager.string_of_uri uri
1414                      | CicTextualParser0.IndTyUri (uri,tyno) ->
1415                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1416                          string_of_int (tyno+1) ^ ")"
1417                      | CicTextualParser0.IndConUri (uri,tyno,consno) ->
1418                         UriManager.string_of_uri uri ^ "#xpointer(1/" ^
1419                          string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^                           ")"
1420              ) dom
1421           ) resolve_ids'
1422         in
1423          let index = interactive_interpretation_choice choices in
1424           List.nth resolve_ids' index
1425     in
1426      id_to_uris := known_ids @ dom', resolve_id' ;
1427      mk_metasenv_and_expr resolve_id'
1428 ;;
1429
1430 exception UriAlreadyInUse;;
1431 exception NotAUriToAConstant;;
1432
1433 let new_inductive () =
1434  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1435  let output = ((rendering_window ())#output : GMathView.math_view) in
1436  let notebook = (rendering_window ())#notebook in
1437
1438  let chosen = ref false in
1439  let inductive = ref true in
1440  let paramsno = ref 0 in
1441  let get_uri = ref (function _ -> assert false) in
1442  let get_base_uri = ref (function _ -> assert false) in
1443  let get_names = ref (function _ -> assert false) in
1444  let get_types_and_cons = ref (function _ -> assert false) in
1445  let get_name_context_context_and_subst = ref (function _ -> assert false) in
1446  let window =
1447   GWindow.window
1448    ~width:600 ~modal:true ~position:`CENTER
1449    ~title:"New Block of Mutual (Co)Inductive Definitions"
1450    ~border_width:2 () in
1451  let vbox = GPack.vbox ~packing:window#add () in
1452  let hbox =
1453   GPack.hbox ~border_width:0
1454    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1455  let _ =
1456   GMisc.label ~text:"Enter the URI for the new block:"
1457    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1458  let uri_entry =
1459   GEdit.entry ~editable:true
1460    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1461  let hbox0 =
1462   GPack.hbox ~border_width:0
1463    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1464  let _ =
1465   GMisc.label
1466    ~text:
1467      "Enter the number of left parameters in every arity and constructor type:"
1468    ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1469  let paramsno_entry =
1470   GEdit.entry ~editable:true ~text:"0"
1471    ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
1472  let hbox1 =
1473   GPack.hbox ~border_width:0
1474    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1475  let _ =
1476   GMisc.label ~text:"Are the definitions inductive or coinductive?"
1477    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1478  let inductiveb =
1479   GButton.radio_button ~label:"Inductive"
1480    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1481  let coinductiveb =
1482   GButton.radio_button ~label:"Coinductive"
1483    ~group:inductiveb#group
1484    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1485  let hbox2 =
1486   GPack.hbox ~border_width:0
1487    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1488  let _ =
1489   GMisc.label ~text:"Enter the list of the names of the types:"
1490    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1491  let names_entry =
1492   GEdit.entry ~editable:true
1493    ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
1494  let hboxn =
1495   GPack.hbox ~border_width:0
1496    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1497  let okb =
1498   GButton.button ~label:"> Next"
1499    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1500  let _ = okb#misc#set_sensitive true in
1501  let cancelb =
1502   GButton.button ~label:"Abort"
1503    ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1504  ignore (window#connect#destroy GMain.Main.quit) ;
1505  ignore (cancelb#connect#clicked window#destroy) ;
1506  (* First phase *)
1507  let rec phase1 () =
1508   ignore
1509    (okb#connect#clicked
1510      (function () ->
1511        try
1512         let uristr = "cic:" ^ uri_entry#text in
1513         let namesstr = names_entry#text in
1514         let paramsno' = int_of_string (paramsno_entry#text) in
1515          match Str.split (Str.regexp " +") namesstr with
1516             [] -> assert false
1517           | (he::tl) as names ->
1518              let uri = UriManager.uri_of_string (uristr ^ "/" ^ he ^ ".ind") in
1519               begin
1520                try
1521                 ignore (Getter.resolve uri) ;
1522                 raise UriAlreadyInUse
1523                with
1524                 Getter.Unresolved ->
1525                  get_uri := (function () -> uri) ;
1526                  get_names := (function () -> names) ;
1527                  inductive := inductiveb#active ;
1528                  paramsno := paramsno' ;
1529                  phase2 ()
1530               end
1531        with
1532         e ->
1533          output_html outputhtml
1534           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1535      ))
1536  (* Second phase *)
1537  and phase2 () =
1538   let type_widgets =
1539    List.map
1540     (function name ->
1541       let frame =
1542        GBin.frame ~label:name
1543         ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
1544       let vbox = GPack.vbox ~packing:frame#add () in
1545       let hbox = GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false) () in
1546       let _ =
1547        GMisc.label ~text:("Enter its type:")
1548         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1549       let scrolled_window =
1550        GBin.scrolled_window ~border_width:5
1551         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1552       let newinputt =
1553        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1554         ~isnotempty_callback:
1555          (function b ->
1556            (*non_empty_type := b ;*)
1557            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*)
1558       in
1559       let hbox =
1560        GPack.hbox ~border_width:0
1561         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1562       let _ =
1563        GMisc.label ~text:("Enter the list of its constructors:")
1564         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1565       let cons_names_entry =
1566        GEdit.entry ~editable:true
1567         ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1568       (newinputt,cons_names_entry)
1569     ) (!get_names ())
1570   in
1571    vbox#remove hboxn#coerce ;
1572    let hboxn =
1573     GPack.hbox ~border_width:0
1574      ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1575    let okb =
1576     GButton.button ~label:"> Next"
1577      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1578    let cancelb =
1579     GButton.button ~label:"Abort"
1580      ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1581    ignore (cancelb#connect#clicked window#destroy) ;
1582    ignore
1583     (okb#connect#clicked
1584       (function () ->
1585         try
1586          let names = !get_names () in
1587          let types_and_cons =
1588           List.map2
1589            (fun name (newinputt,cons_names_entry) ->
1590              let dom,mk_metasenv_and_expr =
1591               newinputt#get_term ~context:[] ~metasenv:[] in
1592              let consnamesstr = cons_names_entry#text in
1593              let cons_names = Str.split (Str.regexp " +") consnamesstr in
1594              let metasenv,expr =
1595               disambiguate_input [] [] dom mk_metasenv_and_expr
1596              in
1597               match metasenv with
1598                  [] -> expr,cons_names
1599                | _ -> raise AmbiguousInput
1600            ) names type_widgets
1601          in
1602           (* Let's see if so far the definition is well-typed *)
1603           let uri = !get_uri () in
1604           let params = [] in
1605           let paramsno = 0 in
1606           let tys =
1607            let i = ref 0 in
1608             List.map2
1609              (fun name (ty,cons) ->
1610                let cons' =
1611                 List.map
1612                  (function consname -> consname, Cic.MutInd (uri,!i,[])) cons in
1613                let res = (name, !inductive, ty, cons') in
1614                 incr i ;
1615                 res
1616              ) names types_and_cons
1617           in
1618 (*CSC: test momentaneamente disattivato. Debbo generare dei costruttori validi
1619   anche quando paramsno > 0 ;-((((
1620            CicTypeChecker.typecheck_mutual_inductive_defs uri
1621             (tys,params,paramsno) ;
1622 *)
1623            get_name_context_context_and_subst :=
1624             (function () ->
1625               let i = ref 0 in
1626                List.fold_left2
1627                 (fun (namecontext,context,subst) name (ty,_) ->
1628                   let res =
1629                    (Some (Cic.Name name))::namecontext,
1630                     (Some (Cic.Name name, Cic.Decl ty))::context,
1631                     (Cic.MutInd (uri,!i,[]))::subst
1632                   in
1633                    incr i ; res
1634                 ) ([],[],[]) names types_and_cons) ;
1635            let types_and_cons' =
1636             List.map2
1637              (fun name (ty,cons) -> (name, !inductive, ty, phase3 name cons))
1638              names types_and_cons
1639            in
1640             get_types_and_cons := (function () -> types_and_cons') ;
1641             chosen := true ;
1642             window#destroy ()
1643         with
1644          e ->
1645           output_html outputhtml
1646            ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1647       ))
1648  (* Third phase *)
1649  and phase3 name cons =
1650   let get_cons_types = ref (function () -> assert false) in
1651   let window2 =
1652    GWindow.window
1653     ~width:600 ~modal:true ~position:`CENTER
1654     ~title:(name ^ " Constructors")
1655     ~border_width:2 () in
1656   let vbox = GPack.vbox ~packing:window2#add () in
1657   let cons_type_widgets =
1658    List.map
1659     (function consname ->
1660       let hbox =
1661        GPack.hbox ~border_width:0
1662         ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1663       let _ =
1664        GMisc.label ~text:("Enter the type of " ^ consname ^ ":")
1665         ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1666       let scrolled_window =
1667        GBin.scrolled_window ~border_width:5
1668         ~packing:(vbox#pack ~expand:true ~padding:0) () in
1669       let newinputt =
1670        new term_editor ~width:400 ~height:20 ~packing:scrolled_window#add ()
1671         ~isnotempty_callback:
1672          (function b ->
1673            (* (*non_empty_type := b ;*)
1674            okb#misc#set_sensitive true) (*(b && uri_entry#text <> ""))*) *)())
1675       in
1676        newinputt
1677     ) cons in
1678   let hboxn =
1679    GPack.hbox ~border_width:0
1680     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1681   let okb =
1682    GButton.button ~label:"> Next"
1683     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1684   let _ = okb#misc#set_sensitive true in
1685   let cancelb =
1686    GButton.button ~label:"Abort"
1687     ~packing:(hboxn#pack ~expand:false ~fill:false ~padding:5) () in
1688   ignore (window2#connect#destroy GMain.Main.quit) ;
1689   ignore (cancelb#connect#clicked window2#destroy) ;
1690   ignore
1691    (okb#connect#clicked
1692      (function () ->
1693        try
1694         chosen := true ;
1695         let namecontext,context,subst= !get_name_context_context_and_subst () in
1696         let cons_types =
1697          List.map2
1698           (fun name inputt ->
1699             let dom,mk_metasenv_and_expr =
1700              inputt#get_term ~context:namecontext ~metasenv:[]
1701             in
1702              let metasenv,expr =
1703               disambiguate_input context [] dom mk_metasenv_and_expr
1704              in
1705               match metasenv with
1706                  [] ->
1707                   let undebrujined_expr =
1708                    List.fold_left
1709                     (fun expr t -> CicSubstitution.subst t expr) expr subst
1710                   in
1711                    name, undebrujined_expr
1712                | _ -> raise AmbiguousInput
1713           ) cons cons_type_widgets
1714         in
1715          get_cons_types := (function () -> cons_types) ;
1716          window2#destroy ()
1717        with
1718         e ->
1719          output_html outputhtml
1720           ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1721      )) ;
1722   window2#show () ;
1723   GMain.Main.main () ;
1724   let okb_pressed = !chosen in
1725    chosen := false ;
1726    if (not okb_pressed) then
1727     begin
1728      window#destroy () ;
1729      assert false (* The control never reaches this point *)
1730     end
1731    else
1732     (!get_cons_types ())
1733  in
1734   phase1 () ;
1735   (* No more phases left or Abort pressed *)
1736   window#show () ;
1737   GMain.Main.main () ;
1738   window#destroy () ;
1739   if !chosen then
1740    try
1741     let uri = !get_uri () in
1742 (*CSC: Da finire *)
1743     let params = [] in
1744     let tys = !get_types_and_cons () in
1745      let obj = Cic.InductiveDefinition tys params !paramsno in
1746       begin
1747        try
1748         prerr_endline (CicPp.ppobj obj) ;
1749         CicTypeChecker.typecheck_mutual_inductive_defs uri
1750          (tys,params,!paramsno) ;
1751         with
1752          e ->
1753           prerr_endline "Offending mutual (co)inductive type declaration:" ;
1754           prerr_endline (CicPp.ppobj obj) ;
1755       end ;
1756       (* We already know that obj is well-typed. We need to add it to the  *)
1757       (* environment in order to compute the inner-types without having to *)
1758       (* debrujin it or having to modify lots of other functions to avoid  *)
1759       (* asking the environment for the MUTINDs we are defining now.       *)
1760       CicEnvironment.put_inductive_definition uri obj ;
1761       save_obj uri obj ;
1762       show_in_show_window_obj uri obj
1763    with
1764     e ->
1765      output_html outputhtml
1766       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1767 ;;
1768
1769 let new_proof () =
1770  let inputt = ((rendering_window ())#inputt : term_editor) in
1771  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1772  let output = ((rendering_window ())#output : GMathView.math_view) in
1773  let notebook = (rendering_window ())#notebook in
1774
1775  let chosen = ref false in
1776  let get_parsed = ref (function _ -> assert false) in
1777  let get_uri = ref (function _ -> assert false) in
1778  let non_empty_type = ref false in
1779  let window =
1780   GWindow.window
1781    ~width:600 ~modal:true ~title:"New Proof or Definition"
1782    ~border_width:2 () in
1783  let vbox = GPack.vbox ~packing:window#add () in
1784  let hbox =
1785   GPack.hbox ~border_width:0
1786    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1787  let _ =
1788   GMisc.label ~text:"Enter the URI for the new theorem or definition:"
1789    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1790  let uri_entry =
1791   GEdit.entry ~editable:true
1792    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
1793  let hbox1 =
1794   GPack.hbox ~border_width:0
1795    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1796  let _ =
1797   GMisc.label ~text:"Enter the theorem or definition type:"
1798    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1799  let scrolled_window =
1800   GBin.scrolled_window ~border_width:5
1801    ~packing:(vbox#pack ~expand:true ~padding:0) () in
1802  (* the content of the scrolled_window is moved below (see comment) *)
1803  let hbox =
1804   GPack.hbox ~border_width:0
1805    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1806  let okb =
1807   GButton.button ~label:"Ok"
1808    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1809  let _ = okb#misc#set_sensitive false in
1810  let cancelb =
1811   GButton.button ~label:"Cancel"
1812    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1813  (* moved here to have visibility of the ok button *)
1814  let newinputt =
1815   new term_editor ~width:400 ~height:100 ~packing:scrolled_window#add ()
1816    ~isnotempty_callback:
1817     (function b ->
1818       non_empty_type := b ;
1819       okb#misc#set_sensitive (b && uri_entry#text <> ""))
1820  in
1821  let _ =
1822   newinputt#set_term inputt#get_as_string ;
1823   inputt#reset in
1824  let _ =
1825   uri_entry#connect#changed
1826    (function () ->
1827      okb#misc#set_sensitive (!non_empty_type && uri_entry#text <> ""))
1828  in
1829  ignore (window#connect#destroy GMain.Main.quit) ;
1830  ignore (cancelb#connect#clicked window#destroy) ;
1831  ignore
1832   (okb#connect#clicked
1833     (function () ->
1834       chosen := true ;
1835       try
1836        let parsed = newinputt#get_term [] [] in
1837        let uristr = "cic:" ^ uri_entry#text in
1838        let uri = UriManager.uri_of_string uristr in
1839         if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
1840          raise NotAUriToAConstant
1841         else
1842          begin
1843           try
1844            ignore (Getter.resolve uri) ;
1845            raise UriAlreadyInUse
1846           with
1847            Getter.Unresolved ->
1848             get_parsed := (function () -> parsed) ;
1849             get_uri := (function () -> uri) ;
1850             window#destroy ()
1851          end
1852       with
1853        e ->
1854         output_html outputhtml
1855          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1856   )) ;
1857  window#show () ;
1858  GMain.Main.main () ;
1859  if !chosen then
1860   try
1861    let dom,mk_metasenv_and_expr = !get_parsed () in
1862     let metasenv,expr =
1863      disambiguate_input [] [] dom mk_metasenv_and_expr
1864     in
1865      let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
1866       ProofEngine.proof :=
1867        Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
1868       ProofEngine.goal := Some 1 ;
1869       refresh_sequent notebook ;
1870       refresh_proof output ;
1871       !save_set_sensitive true ;
1872       inputt#reset
1873   with
1874      RefreshSequentException e ->
1875       output_html outputhtml
1876        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1877         "sequent: " ^ Printexc.to_string e ^ "</h1>")
1878    | RefreshProofException e ->
1879       output_html outputhtml
1880        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1881         "proof: " ^ Printexc.to_string e ^ "</h1>")
1882    | e ->
1883       output_html outputhtml
1884        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1885 ;;
1886
1887 let check_term_in_scratch scratch_window metasenv context expr =
1888  try
1889   let ty  = CicTypeChecker.type_of_aux' metasenv context expr in
1890    let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1891 prerr_endline ("### " ^ CicPp.ppterm expr ^ " ==> " ^ CicPp.ppterm ty) ;
1892     scratch_window#show () ;
1893     scratch_window#mmlwidget#load_tree ~dom:mml
1894  with
1895   e ->
1896    print_endline ("? " ^ CicPp.ppterm expr) ;
1897    raise e
1898 ;;
1899
1900 let check scratch_window () =
1901  let inputt = ((rendering_window ())#inputt : term_editor) in
1902  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1903   let metasenv =
1904    match !ProofEngine.proof with
1905       None -> []
1906     | Some (_,metasenv,_,_) -> metasenv
1907   in
1908   let context,names_context =
1909    let context =
1910     match !ProofEngine.goal with
1911        None -> []
1912      | Some metano ->
1913         let (_,canonical_context,_) =
1914          List.find (function (m,_,_) -> m=metano) metasenv
1915         in
1916          canonical_context
1917    in
1918     context,
1919     List.map
1920      (function
1921          Some (n,_) -> Some n
1922        | None -> None
1923      ) context
1924   in
1925    try
1926     let dom,mk_metasenv_and_expr = inputt#get_term names_context metasenv in
1927      let (metasenv',expr) =
1928       disambiguate_input context metasenv dom mk_metasenv_and_expr
1929      in
1930       check_term_in_scratch scratch_window metasenv' context expr
1931    with
1932     e ->
1933      output_html outputhtml
1934       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1935 ;;
1936
1937
1938 (***********************)
1939 (*       TACTICS       *)
1940 (***********************)
1941
1942 let call_tactic tactic () =
1943  let notebook = (rendering_window ())#notebook in
1944  let output = ((rendering_window ())#output : GMathView.math_view) in
1945  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1946  let savedproof = !ProofEngine.proof in
1947  let savedgoal  = !ProofEngine.goal in
1948   begin
1949    try
1950     tactic () ;
1951     refresh_sequent notebook ;
1952     refresh_proof output
1953    with
1954       RefreshSequentException e ->
1955        output_html outputhtml
1956         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1957          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
1958        ProofEngine.proof := savedproof ;
1959        ProofEngine.goal := savedgoal ;
1960        refresh_sequent notebook
1961     | RefreshProofException e ->
1962        output_html outputhtml
1963         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1964          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
1965        ProofEngine.proof := savedproof ;
1966        ProofEngine.goal := savedgoal ;
1967        refresh_sequent notebook ;
1968        refresh_proof output
1969     | e ->
1970        output_html outputhtml
1971         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1972        ProofEngine.proof := savedproof ;
1973        ProofEngine.goal := savedgoal ;
1974   end
1975 ;;
1976
1977 let call_tactic_with_input tactic () =
1978  let notebook = (rendering_window ())#notebook in
1979  let output = ((rendering_window ())#output : GMathView.math_view) in
1980  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
1981  let inputt = ((rendering_window ())#inputt : term_editor) in
1982  let savedproof = !ProofEngine.proof in
1983  let savedgoal  = !ProofEngine.goal in
1984   let uri,metasenv,bo,ty =
1985    match !ProofEngine.proof with
1986       None -> assert false
1987     | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
1988   in
1989    let canonical_context =
1990     match !ProofEngine.goal with
1991        None -> assert false
1992      | Some metano ->
1993         let (_,canonical_context,_) =
1994          List.find (function (m,_,_) -> m=metano) metasenv
1995         in
1996          canonical_context
1997    in
1998    let context =
1999     List.map
2000      (function
2001          Some (n,_) -> Some n
2002        | None -> None
2003      ) canonical_context
2004    in
2005     try
2006      let dom,mk_metasenv_and_expr = inputt#get_term context metasenv in
2007       let (metasenv',expr) =
2008        disambiguate_input canonical_context metasenv dom mk_metasenv_and_expr
2009       in
2010        ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2011        tactic expr ;
2012        refresh_sequent notebook ;
2013        refresh_proof output ;
2014        inputt#reset
2015     with
2016        RefreshSequentException e ->
2017         output_html outputhtml
2018          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2019           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2020         ProofEngine.proof := savedproof ;
2021         ProofEngine.goal := savedgoal ;
2022         refresh_sequent notebook
2023      | RefreshProofException e ->
2024         output_html outputhtml
2025          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2026           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2027         ProofEngine.proof := savedproof ;
2028         ProofEngine.goal := savedgoal ;
2029         refresh_sequent notebook ;
2030         refresh_proof output
2031      | e ->
2032         output_html outputhtml
2033          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2034         ProofEngine.proof := savedproof ;
2035         ProofEngine.goal := savedgoal ;
2036 ;;
2037
2038 let call_tactic_with_goal_input tactic () =
2039  let module L = LogicalOperations in
2040  let module G = Gdome in
2041   let notebook = (rendering_window ())#notebook in
2042   let output = ((rendering_window ())#output : GMathView.math_view) in
2043   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2044   let savedproof = !ProofEngine.proof in
2045   let savedgoal  = !ProofEngine.goal in
2046    match notebook#proofw#get_selection with
2047      Some node ->
2048       let xpath =
2049        ((node : Gdome.element)#getAttributeNS
2050          ~namespaceURI:helmns
2051          ~localName:(G.domString "xref"))#to_string
2052       in
2053        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2054        else
2055         begin
2056          try
2057           match !current_goal_infos with
2058              Some (ids_to_terms, ids_to_father_ids,_) ->
2059               let id = xpath in
2060                tactic (Hashtbl.find ids_to_terms id) ;
2061                refresh_sequent notebook ;
2062                refresh_proof output
2063            | None -> assert false (* "ERROR: No current term!!!" *)
2064          with
2065             RefreshSequentException e ->
2066              output_html outputhtml
2067               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2068                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2069              ProofEngine.proof := savedproof ;
2070              ProofEngine.goal := savedgoal ;
2071              refresh_sequent notebook
2072           | RefreshProofException e ->
2073              output_html outputhtml
2074               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2075                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2076              ProofEngine.proof := savedproof ;
2077              ProofEngine.goal := savedgoal ;
2078              refresh_sequent notebook ;
2079              refresh_proof output
2080           | e ->
2081              output_html outputhtml
2082               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2083              ProofEngine.proof := savedproof ;
2084              ProofEngine.goal := savedgoal ;
2085         end
2086    | None ->
2087       output_html outputhtml
2088        ("<h1 color=\"red\">No term selected</h1>")
2089 ;;
2090
2091 let call_tactic_with_input_and_goal_input tactic () =
2092  let module L = LogicalOperations in
2093  let module G = Gdome in
2094   let notebook = (rendering_window ())#notebook in
2095   let output = ((rendering_window ())#output : GMathView.math_view) in
2096   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2097   let inputt = ((rendering_window ())#inputt : term_editor) in
2098   let savedproof = !ProofEngine.proof in
2099   let savedgoal  = !ProofEngine.goal in
2100    match notebook#proofw#get_selection with
2101      Some node ->
2102       let xpath =
2103        ((node : Gdome.element)#getAttributeNS
2104          ~namespaceURI:helmns
2105          ~localName:(G.domString "xref"))#to_string
2106       in
2107        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2108        else
2109         begin
2110          try
2111           match !current_goal_infos with
2112              Some (ids_to_terms, ids_to_father_ids,_) ->
2113               let id = xpath in
2114                let uri,metasenv,bo,ty =
2115                 match !ProofEngine.proof with
2116                    None -> assert false
2117                  | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
2118                in
2119                 let canonical_context =
2120                  match !ProofEngine.goal with
2121                     None -> assert false
2122                   | Some metano ->
2123                      let (_,canonical_context,_) =
2124                       List.find (function (m,_,_) -> m=metano) metasenv
2125                      in
2126                       canonical_context in
2127                 let context =
2128                  List.map
2129                   (function
2130                       Some (n,_) -> Some n
2131                     | None -> None
2132                   ) canonical_context
2133                 in
2134                  let dom,mk_metasenv_and_expr = inputt#get_term context metasenv
2135                  in
2136                   let (metasenv',expr) =
2137                    disambiguate_input canonical_context metasenv dom
2138                     mk_metasenv_and_expr
2139                   in
2140                    ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
2141                    tactic ~goal_input:(Hashtbl.find ids_to_terms id)
2142                     ~input:expr ;
2143                    refresh_sequent notebook ;
2144                    refresh_proof output ;
2145                    inputt#reset
2146            | None -> assert false (* "ERROR: No current term!!!" *)
2147          with
2148             RefreshSequentException e ->
2149              output_html outputhtml
2150               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2151                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2152              ProofEngine.proof := savedproof ;
2153              ProofEngine.goal := savedgoal ;
2154              refresh_sequent notebook
2155           | RefreshProofException e ->
2156              output_html outputhtml
2157               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2158                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2159              ProofEngine.proof := savedproof ;
2160              ProofEngine.goal := savedgoal ;
2161              refresh_sequent notebook ;
2162              refresh_proof output
2163           | e ->
2164              output_html outputhtml
2165               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2166              ProofEngine.proof := savedproof ;
2167              ProofEngine.goal := savedgoal ;
2168         end
2169    | None ->
2170       output_html outputhtml
2171        ("<h1 color=\"red\">No term selected</h1>")
2172 ;;
2173
2174 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
2175  let module L = LogicalOperations in
2176  let module G = Gdome in
2177   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
2178   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2179   let savedproof = !ProofEngine.proof in
2180   let savedgoal  = !ProofEngine.goal in
2181    match mmlwidget#get_selection with
2182      Some node ->
2183       let xpath =
2184        ((node : Gdome.element)#getAttributeNS
2185          ~namespaceURI:helmns
2186          ~localName:(G.domString "xref"))#to_string
2187       in
2188        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2189        else
2190         begin
2191          try
2192           match !current_scratch_infos with
2193              (* term is the whole goal in the scratch_area *)
2194              Some (term,ids_to_terms, ids_to_father_ids,_) ->
2195               let id = xpath in
2196                let expr = tactic term (Hashtbl.find ids_to_terms id) in
2197                 let mml = mml_of_cic_term 111 expr in
2198                  scratch_window#show () ;
2199                  scratch_window#mmlwidget#load_tree ~dom:mml
2200            | None -> assert false (* "ERROR: No current term!!!" *)
2201          with
2202           e ->
2203            output_html outputhtml
2204             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2205         end
2206    | None ->
2207       output_html outputhtml
2208        ("<h1 color=\"red\">No term selected</h1>")
2209 ;;
2210
2211 let call_tactic_with_hypothesis_input tactic () =
2212  let module L = LogicalOperations in
2213  let module G = Gdome in
2214   let notebook = (rendering_window ())#notebook in
2215   let output = ((rendering_window ())#output : GMathView.math_view) in
2216   let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2217   let savedproof = !ProofEngine.proof in
2218   let savedgoal  = !ProofEngine.goal in
2219    match notebook#proofw#get_selection with
2220      Some node ->
2221       let xpath =
2222        ((node : Gdome.element)#getAttributeNS
2223          ~namespaceURI:helmns
2224          ~localName:(G.domString "xref"))#to_string
2225       in
2226        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
2227        else
2228         begin
2229          try
2230           match !current_goal_infos with
2231              Some (_,_,ids_to_hypotheses) ->
2232               let id = xpath in
2233                tactic (Hashtbl.find ids_to_hypotheses id) ;
2234                refresh_sequent notebook ;
2235                refresh_proof output
2236            | None -> assert false (* "ERROR: No current term!!!" *)
2237          with
2238             RefreshSequentException e ->
2239              output_html outputhtml
2240               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2241                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
2242              ProofEngine.proof := savedproof ;
2243              ProofEngine.goal := savedgoal ;
2244              refresh_sequent notebook
2245           | RefreshProofException e ->
2246              output_html outputhtml
2247               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2248                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
2249              ProofEngine.proof := savedproof ;
2250              ProofEngine.goal := savedgoal ;
2251              refresh_sequent notebook ;
2252              refresh_proof output
2253           | e ->
2254              output_html outputhtml
2255               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2256              ProofEngine.proof := savedproof ;
2257              ProofEngine.goal := savedgoal ;
2258         end
2259    | None ->
2260       output_html outputhtml
2261        ("<h1 color=\"red\">No term selected</h1>")
2262 ;;
2263
2264
2265 let intros = call_tactic ProofEngine.intros;;
2266 let exact = call_tactic_with_input ProofEngine.exact;;
2267 let apply = call_tactic_with_input ProofEngine.apply;;
2268 let elimsimplintros = call_tactic_with_input ProofEngine.elim_simpl_intros;;
2269 let elimtype = call_tactic_with_input ProofEngine.elim_type;;
2270 let whd = call_tactic_with_goal_input ProofEngine.whd;;
2271 let reduce = call_tactic_with_goal_input ProofEngine.reduce;;
2272 let simpl = call_tactic_with_goal_input ProofEngine.simpl;;
2273 let fold_whd = call_tactic_with_input ProofEngine.fold_whd;;
2274 let fold_reduce = call_tactic_with_input ProofEngine.fold_reduce;;
2275 let fold_simpl = call_tactic_with_input ProofEngine.fold_simpl;;
2276 let cut = call_tactic_with_input ProofEngine.cut;;
2277 let change = call_tactic_with_input_and_goal_input ProofEngine.change;;
2278 let letin = call_tactic_with_input ProofEngine.letin;;
2279 let ring = call_tactic ProofEngine.ring;;
2280 let clearbody = call_tactic_with_hypothesis_input ProofEngine.clearbody;;
2281 let clear = call_tactic_with_hypothesis_input ProofEngine.clear;;
2282 let fourier = call_tactic ProofEngine.fourier;;
2283 let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;;
2284 let reflexivity = call_tactic ProofEngine.reflexivity;;
2285 let symmetry = call_tactic ProofEngine.symmetry;;
2286 let transitivity = call_tactic_with_input ProofEngine.transitivity;;
2287 let exists = call_tactic ProofEngine.exists;;
2288 let split = call_tactic ProofEngine.split;;
2289 let left = call_tactic ProofEngine.left;;
2290 let right = call_tactic ProofEngine.right;;
2291 let assumption = call_tactic ProofEngine.assumption;;
2292 let generalize = call_tactic_with_goal_input ProofEngine.generalize;;
2293 let absurd = call_tactic_with_input ProofEngine.absurd;;
2294 let contradiction = call_tactic ProofEngine.contradiction;;
2295 (* Galla: come dare alla tattica la lista di termini da decomporre?
2296 let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;;
2297 *)
2298
2299 let whd_in_scratch scratch_window =
2300  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
2301   scratch_window
2302 ;;
2303 let reduce_in_scratch scratch_window =
2304  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
2305   scratch_window
2306 ;;
2307 let simpl_in_scratch scratch_window =
2308  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
2309   scratch_window
2310 ;;
2311
2312
2313
2314 (**********************)
2315 (*   END OF TACTICS   *)
2316 (**********************)
2317
2318
2319 let show () =
2320  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2321   try
2322    show_in_show_window_uri (input_or_locate_uri ~title:"Show")
2323   with
2324    e ->
2325     output_html outputhtml
2326      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2327 ;;
2328
2329 exception NotADefinition;;
2330
2331 let open_ () =
2332  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2333  let output = ((rendering_window ())#output : GMathView.math_view) in
2334  let notebook = (rendering_window ())#notebook in
2335    try
2336     let uri = input_or_locate_uri ~title:"Open" in
2337      CicTypeChecker.typecheck uri ;
2338      let metasenv,bo,ty =
2339       match CicEnvironment.get_cooked_obj uri with
2340          Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
2341        | Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
2342        | Cic.Constant _
2343        | Cic.Variable _
2344        | Cic.InductiveDefinition _ -> raise NotADefinition
2345      in
2346       ProofEngine.proof :=
2347        Some (uri, metasenv, bo, ty) ;
2348       ProofEngine.goal := None ;
2349       refresh_sequent notebook ;
2350       refresh_proof output
2351    with
2352       RefreshSequentException e ->
2353        output_html outputhtml
2354         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2355          "sequent: " ^ Printexc.to_string e ^ "</h1>")
2356     | RefreshProofException e ->
2357        output_html outputhtml
2358         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
2359          "proof: " ^ Printexc.to_string e ^ "</h1>")
2360     | e ->
2361        output_html outputhtml
2362         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2363 ;;
2364
2365
2366 let completeSearchPattern () =
2367  let inputt = ((rendering_window ())#inputt : term_editor) in
2368  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2369   try
2370    let dom,mk_metasenv_and_expr = inputt#get_term ~context:[] ~metasenv:[] in
2371    let metasenv,expr = disambiguate_input [] [] dom mk_metasenv_and_expr in
2372    let must,can = MQueryLevels2.get_constraints expr in
2373    let result = MQueryGenerator.searchPattern must can in
2374     output_html outputhtml
2375      ("<h1 color=\"maroon\"><pre>" ^ MQueryUtil.text_of_result result "\n" ^ "</pre></h1>")
2376   with
2377    e ->
2378     output_html outputhtml
2379      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
2380 ;;
2381
2382 let choose_must list_of_must can =
2383  let chosen = ref None in
2384  let user_constraints = ref [] in
2385  let window =
2386   GWindow.window
2387    ~modal:true ~title:"Query refinement." ~border_width:2 () in
2388  let vbox = GPack.vbox ~packing:window#add () in
2389  let hbox =
2390   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2391  let lMessage =
2392   GMisc.label
2393    ~text:
2394     ("You can now specify the genericity of the query. " ^
2395      "The more generic the slower.")
2396    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2397  let hbox =
2398   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2399  let lMessage =
2400   GMisc.label
2401    ~text:
2402     "Suggestion: start with faster queries before moving to more generic ones."
2403    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2404  let notebook =
2405   GPack.notebook ~scrollable:true
2406    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2407  let _ =
2408   let page = ref 0 in
2409   let last = List.length list_of_must in
2410   List.map
2411    (function must ->
2412      incr page ;
2413      let label =
2414       GMisc.label ~text:
2415        (if !page = 1 then "More generic" else
2416          if !page = last then "More precise" else "          ") () in
2417      let expected_height = 25 * (List.length must + 2) in
2418      let height = if expected_height > 400 then 400 else expected_height in
2419      let scrolled_window =
2420       GBin.scrolled_window ~border_width:10 ~height ~width:600
2421        ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2422      let clist =
2423         GList.clist ~columns:2 ~packing:scrolled_window#add
2424          ~titles:["URI" ; "Position"] ()
2425      in
2426       ignore
2427        (List.map
2428          (function (uri,position) ->
2429            let n =
2430             clist#append
2431              [uri; if position then "MainConclusion" else "Conclusion"]
2432            in
2433             clist#set_row ~selectable:false n
2434          ) must
2435        ) ;
2436       clist#columns_autosize ()
2437    ) list_of_must in
2438  let _ =
2439   let label = GMisc.label ~text:"User provided" () in
2440   let vbox =
2441    GPack.vbox ~packing:(notebook#append_page ~tab_label:label#coerce) () in
2442   let hbox =
2443    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2444   let lMessage =
2445    GMisc.label
2446    ~text:"Select the constraints that must be satisfied and press OK."
2447    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2448   let expected_height = 25 * (List.length can + 2) in
2449   let height = if expected_height > 400 then 400 else expected_height in
2450   let scrolled_window =
2451    GBin.scrolled_window ~border_width:10 ~height ~width:600
2452     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
2453   let clist =
2454    GList.clist ~columns:2 ~packing:scrolled_window#add
2455     ~selection_mode:`EXTENDED
2456     ~titles:["URI" ; "Position"] ()
2457   in
2458    ignore
2459     (List.map
2460       (function (uri,position) ->
2461         let n =
2462          clist#append
2463           [uri; if position then "MainConclusion" else "Conclusion"]
2464         in
2465          clist#set_row ~selectable:true n
2466       ) can
2467     ) ;
2468    clist#columns_autosize () ;
2469    ignore
2470     (clist#connect#select_row
2471       (fun ~row ~column ~event ->
2472         user_constraints := (List.nth can row)::!user_constraints)) ;
2473    ignore
2474     (clist#connect#unselect_row
2475       (fun ~row ~column ~event ->
2476         user_constraints :=
2477          List.filter
2478           (function uri -> uri != (List.nth can row)) !user_constraints)) ;
2479  in
2480  let hbox =
2481   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2482  let okb =
2483   GButton.button ~label:"Ok"
2484    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2485  let cancelb =
2486   GButton.button ~label:"Abort"
2487    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2488  (* actions *)
2489  ignore (window#connect#destroy GMain.Main.quit) ;
2490  ignore (cancelb#connect#clicked window#destroy) ;
2491  ignore
2492   (okb#connect#clicked
2493     (function () -> chosen := Some notebook#current_page ; window#destroy ())) ;
2494  window#set_position `CENTER ;
2495  window#show () ;
2496  GMain.Main.main () ;
2497  match !chosen with
2498     None -> raise NoChoice
2499   | Some n ->
2500      if n = List.length list_of_must then
2501       (* user provided constraints *)
2502       !user_constraints
2503      else
2504       List.nth list_of_must n
2505 ;;
2506
2507 let searchPattern () =
2508  let inputt = ((rendering_window ())#inputt : term_editor) in
2509  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
2510   try
2511     let metasenv =
2512      match !ProofEngine.proof with
2513         None -> assert false
2514       | Some (_,metasenv,_,_) -> metasenv
2515     in
2516      match !ProofEngine.goal with
2517         None -> ()
2518       | Some metano ->
2519          let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
2520           let list_of_must,can = MQueryLevels.out_restr metasenv ey ty in
2521           let must = choose_must list_of_must can in
2522           let torigth_restriction (u,b) =
2523              let p = if b then "http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion"
2524                      else "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" in
2525                (u,p,None)
2526           in
2527           let rigth_must = List.map torigth_restriction must in
2528           let rigth_can = Some (List.map torigth_restriction can) in
2529           let result = MQueryGenerator.searchPattern (rigth_must,[],[]) (rigth_can,None,None) in
2530           let uris =
2531            List.map
2532             (function uri,_ ->
2533               wrong_xpointer_format_from_wrong_xpointer_format' uri
2534             ) result in
2535           let html =
2536            " <h1>Backward Query: </h1>" ^
2537            " <pre>" ^ get_last_query result ^ "</pre>"
2538           in
2539            output_html outputhtml html ;
2540            let uris',exc =
2541             let rec filter_out =
2542              function
2543                 [] -> [],""
2544               | uri::tl ->
2545                  let tl',exc = filter_out tl in
2546                   try
2547                    if
2548                     ProofEngine.can_apply
2549                      (term_of_cic_textual_parser_uri
2550                       (cic_textual_parser_uri_of_string uri))
2551                    then
2552                     uri::tl',exc
2553                    else
2554                     tl',exc
2555                   with
2556                    e ->
2557                     let exc' =
2558                      "<h1 color=\"red\"> ^ Exception raised trying to apply " ^
2559                       uri ^ ": " ^ Printexc.to_string e ^ " </h1>" ^ exc
2560                     in
2561                      tl',exc'
2562             in
2563              filter_out uris
2564            in
2565             let html' =
2566              " <h1>Objects that can actually be applied: </h1> " ^
2567              String.concat "<br>" uris' ^ exc ^
2568              " <h1>Number of false matches: " ^
2569               string_of_int (List.length uris - List.length uris') ^ "</h1>" ^
2570              " <h1>Number of good matches: " ^
2571               string_of_int (List.length uris') ^ "</h1>"
2572             in
2573              output_html outputhtml html' ;
2574              let uri' =
2575               user_uri_choice ~title:"Ambiguous input."
2576               ~msg:
2577                 "Many lemmas can be successfully applied. Please, choose one:"
2578                uris'
2579              in
2580               inputt#set_term uri' ;
2581               apply ()
2582   with
2583    e ->
2584     output_html outputhtml
2585      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
2586 ;;
2587
2588 let choose_selection
2589      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
2590 =
2591  let module G = Gdome in
2592   let rec aux element =
2593    if element#hasAttributeNS
2594        ~namespaceURI:helmns
2595        ~localName:(G.domString "xref")
2596    then
2597      mmlwidget#set_selection (Some element)
2598    else
2599       match element#get_parentNode with
2600          None -> assert false
2601        (*CSC: OCAML DIVERGES!
2602        | Some p -> aux (new G.element_of_node p)
2603        *)
2604        | Some p -> aux (new Gdome.element_of_node p)
2605   in
2606    match element with
2607      Some x -> aux x
2608    | None   -> mmlwidget#set_selection None
2609 ;;
2610
2611 (* STUFF TO BUILD THE GTK INTERFACE *)
2612
2613 (* Stuff for the widget settings *)
2614
2615 let export_to_postscript (output : GMathView.math_view) =
2616  let lastdir = ref (Unix.getcwd ()) in
2617   function () ->
2618    match
2619     GToolbox.select_file ~title:"Export to PostScript"
2620      ~dir:lastdir ~filename:"screenshot.ps" ()
2621    with
2622       None -> ()
2623     | Some filename ->
2624        output#export_to_postscript ~filename:filename ();
2625 ;;
2626
2627 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
2628  button_set_kerning button_set_transparency export_to_postscript_menu_item
2629  button_t1 ()
2630 =
2631  let is_set = button_t1#active in
2632   output#set_font_manager_type
2633    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
2634   if is_set then
2635    begin
2636     button_set_anti_aliasing#misc#set_sensitive true ;
2637     button_set_kerning#misc#set_sensitive true ;
2638     button_set_transparency#misc#set_sensitive true ;
2639     export_to_postscript_menu_item#misc#set_sensitive true ;
2640    end
2641   else
2642    begin
2643     button_set_anti_aliasing#misc#set_sensitive false ;
2644     button_set_kerning#misc#set_sensitive false ;
2645     button_set_transparency#misc#set_sensitive false ;
2646     export_to_postscript_menu_item#misc#set_sensitive false ;
2647    end
2648 ;;
2649
2650 let set_anti_aliasing output button_set_anti_aliasing () =
2651  output#set_anti_aliasing button_set_anti_aliasing#active
2652 ;;
2653
2654 let set_kerning output button_set_kerning () =
2655  output#set_kerning button_set_kerning#active
2656 ;;
2657
2658 let set_transparency output button_set_transparency () =
2659  output#set_transparency button_set_transparency#active
2660 ;;
2661
2662 let changefont output font_size_spinb () =
2663  output#set_font_size font_size_spinb#value_as_int
2664 ;;
2665
2666 let set_log_verbosity output log_verbosity_spinb () =
2667  output#set_log_verbosity log_verbosity_spinb#value_as_int
2668 ;;
2669
2670 class settings_window (output : GMathView.math_view) sw
2671  export_to_postscript_menu_item selection_changed_callback
2672 =
2673  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
2674  let vbox =
2675   GPack.vbox ~packing:settings_window#add () in
2676  let table =
2677   GPack.table
2678    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2679    ~border_width:5 ~packing:vbox#add () in
2680  let button_t1 =
2681   GButton.toggle_button ~label:"activate t1 fonts"
2682    ~packing:(table#attach ~left:0 ~top:0) () in
2683  let button_set_anti_aliasing =
2684   GButton.toggle_button ~label:"set_anti_aliasing"
2685    ~packing:(table#attach ~left:0 ~top:1) () in
2686  let button_set_kerning =
2687   GButton.toggle_button ~label:"set_kerning"
2688    ~packing:(table#attach ~left:1 ~top:1) () in
2689  let button_set_transparency =
2690   GButton.toggle_button ~label:"set_transparency"
2691    ~packing:(table#attach ~left:2 ~top:1) () in
2692  let table =
2693   GPack.table
2694    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
2695    ~border_width:5 ~packing:vbox#add () in
2696  let font_size_label =
2697   GMisc.label ~text:"font size:"
2698    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
2699  let font_size_spinb =
2700   let sadj =
2701    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
2702   in
2703    GEdit.spin_button
2704     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
2705  let log_verbosity_label =
2706   GMisc.label ~text:"log verbosity:"
2707    ~packing:(table#attach ~left:0 ~top:1) () in
2708  let log_verbosity_spinb =
2709   let sadj =
2710    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
2711   in
2712    GEdit.spin_button
2713     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
2714  let hbox =
2715   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2716  let closeb =
2717   GButton.button ~label:"Close"
2718    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2719 object(self)
2720  method show = settings_window#show
2721  initializer
2722   button_set_anti_aliasing#misc#set_sensitive false ;
2723   button_set_kerning#misc#set_sensitive false ;
2724   button_set_transparency#misc#set_sensitive false ;
2725   (* Signals connection *)
2726   ignore(button_t1#connect#clicked
2727    (activate_t1 output button_set_anti_aliasing button_set_kerning
2728     button_set_transparency export_to_postscript_menu_item button_t1)) ;
2729   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
2730   ignore(button_set_anti_aliasing#connect#toggled
2731    (set_anti_aliasing output button_set_anti_aliasing));
2732   ignore(button_set_kerning#connect#toggled
2733    (set_kerning output button_set_kerning)) ;
2734   ignore(button_set_transparency#connect#toggled
2735    (set_transparency output button_set_transparency)) ;
2736   ignore(log_verbosity_spinb#connect#changed
2737    (set_log_verbosity output log_verbosity_spinb)) ;
2738   ignore(closeb#connect#clicked settings_window#misc#hide)
2739 end;;
2740
2741 (* Scratch window *)
2742
2743 class scratch_window =
2744  let window =
2745   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
2746  let vbox =
2747   GPack.vbox ~packing:window#add () in
2748  let hbox =
2749   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
2750  let whdb =
2751   GButton.button ~label:"Whd"
2752    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2753  let reduceb =
2754   GButton.button ~label:"Reduce"
2755    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2756  let simplb =
2757   GButton.button ~label:"Simpl"
2758    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
2759  let scrolled_window =
2760   GBin.scrolled_window ~border_width:10
2761    ~packing:(vbox#pack ~expand:true ~padding:5) () in
2762  let mmlwidget =
2763   GMathView.math_view
2764    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
2765 object(self)
2766  method mmlwidget = mmlwidget
2767  method show () = window#misc#hide () ; window#show ()
2768  initializer
2769   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
2770   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
2771   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
2772   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
2773   ignore(simplb#connect#clicked (simpl_in_scratch self))
2774 end;;
2775
2776 class page () =
2777  let vbox1 = GPack.vbox () in
2778 object(self)
2779  val mutable proofw_ref = None
2780  val mutable compute_ref = None
2781  method proofw =
2782   Lazy.force self#compute ;
2783   match proofw_ref with
2784      None -> assert false
2785    | Some proofw -> proofw
2786  method content = vbox1
2787  method compute =
2788   match compute_ref with
2789      None -> assert false
2790    | Some compute -> compute
2791  initializer
2792   compute_ref <-
2793    Some (lazy (
2794    let scrolled_window1 =
2795     GBin.scrolled_window ~border_width:10
2796      ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2797    let proofw =
2798     GMathView.math_view ~width:400 ~height:275
2799      ~packing:(scrolled_window1#add) () in
2800    let _ = proofw_ref <- Some proofw in
2801    let hbox3 =
2802     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2803    let exactb =
2804     GButton.button ~label:"Exact"
2805      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2806    let introsb =
2807     GButton.button ~label:"Intros"
2808      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2809    let applyb =
2810     GButton.button ~label:"Apply"
2811      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2812    let elimsimplintrosb =
2813     GButton.button ~label:"ElimSimplIntros"
2814      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2815    let elimtypeb =
2816     GButton.button ~label:"ElimType"
2817      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2818    let whdb =
2819     GButton.button ~label:"Whd"
2820      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2821    let reduceb =
2822     GButton.button ~label:"Reduce"
2823      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2824    let simplb =
2825     GButton.button ~label:"Simpl"
2826      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2827    let foldwhdb =
2828     GButton.button ~label:"Fold_whd"
2829      ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
2830    let hbox4 =
2831     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2832    let foldreduceb =
2833     GButton.button ~label:"Fold_reduce"
2834      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2835    let foldsimplb =
2836     GButton.button ~label:"Fold_simpl"
2837      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2838    let cutb =
2839     GButton.button ~label:"Cut"
2840      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2841    let changeb =
2842     GButton.button ~label:"Change"
2843      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2844    let letinb =
2845     GButton.button ~label:"Let ... In"
2846      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2847    let ringb =
2848     GButton.button ~label:"Ring"
2849      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2850    let clearbodyb =
2851     GButton.button ~label:"ClearBody"
2852      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2853    let clearb =
2854     GButton.button ~label:"Clear"
2855      ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
2856    let hbox5 =
2857     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2858    let fourierb =
2859     GButton.button ~label:"Fourier"
2860      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2861    let rewritesimplb =
2862     GButton.button ~label:"RewriteSimpl ->"
2863      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2864    let reflexivityb =
2865     GButton.button ~label:"Reflexivity"
2866      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2867    let symmetryb =
2868     GButton.button ~label:"Symmetry"
2869      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2870    let transitivityb =
2871     GButton.button ~label:"Transitivity"
2872      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2873    let existsb =
2874     GButton.button ~label:"Exists"
2875      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2876    let splitb =
2877     GButton.button ~label:"Split"
2878      ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in
2879    let hbox6 =
2880     GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
2881    let leftb =
2882     GButton.button ~label:"Left"
2883      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2884    let rightb =
2885     GButton.button ~label:"Right"
2886      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2887    let assumptionb =
2888     GButton.button ~label:"Assumption"
2889      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2890    let generalizeb =
2891     GButton.button ~label:"Generalize"
2892      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2893    let absurdb =
2894     GButton.button ~label:"Absurd"
2895      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2896    let contradictionb =
2897     GButton.button ~label:"Contradiction"
2898      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2899    let searchpatternb =
2900     GButton.button ~label:"SearchPattern_Apply"
2901      ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in
2902
2903    ignore(exactb#connect#clicked exact) ;
2904    ignore(applyb#connect#clicked apply) ;
2905    ignore(elimsimplintrosb#connect#clicked elimsimplintros) ;
2906    ignore(elimtypeb#connect#clicked elimtype) ;
2907    ignore(whdb#connect#clicked whd) ;
2908    ignore(reduceb#connect#clicked reduce) ;
2909    ignore(simplb#connect#clicked simpl) ;
2910    ignore(foldwhdb#connect#clicked fold_whd) ;
2911    ignore(foldreduceb#connect#clicked fold_reduce) ;
2912    ignore(foldsimplb#connect#clicked fold_simpl) ;
2913    ignore(cutb#connect#clicked cut) ;
2914    ignore(changeb#connect#clicked change) ;
2915    ignore(letinb#connect#clicked letin) ;
2916    ignore(ringb#connect#clicked ring) ;
2917    ignore(clearbodyb#connect#clicked clearbody) ;
2918    ignore(clearb#connect#clicked clear) ;
2919    ignore(fourierb#connect#clicked fourier) ;
2920    ignore(rewritesimplb#connect#clicked rewritesimpl) ;
2921    ignore(reflexivityb#connect#clicked reflexivity) ;
2922    ignore(symmetryb#connect#clicked symmetry) ;
2923    ignore(transitivityb#connect#clicked transitivity) ;
2924    ignore(existsb#connect#clicked exists) ;
2925    ignore(splitb#connect#clicked split) ;
2926    ignore(leftb#connect#clicked left) ;
2927    ignore(rightb#connect#clicked right) ;
2928    ignore(assumptionb#connect#clicked assumption) ;
2929    ignore(generalizeb#connect#clicked generalize) ;
2930    ignore(absurdb#connect#clicked absurd) ;
2931    ignore(contradictionb#connect#clicked contradiction) ;
2932    ignore(introsb#connect#clicked intros) ;
2933    ignore(searchpatternb#connect#clicked searchPattern) ;
2934    ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
2935   ))
2936 end
2937 ;;
2938
2939 class empty_page =
2940  let vbox1 = GPack.vbox () in
2941  let scrolled_window1 =
2942   GBin.scrolled_window ~border_width:10
2943    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
2944  let proofw =
2945   GMathView.math_view ~width:400 ~height:275
2946    ~packing:(scrolled_window1#add) () in
2947 object(self)
2948  method proofw = (assert false : GMathView.math_view)
2949  method content = vbox1
2950  method compute = (assert false : unit)
2951 end
2952 ;;
2953
2954 let empty_page = new empty_page;;
2955
2956 class notebook =
2957 object(self)
2958  val notebook = GPack.notebook ()
2959  val pages = ref []
2960  val mutable skip_switch_page_event = false
2961  val mutable empty = true
2962  method notebook = notebook
2963  method add_page n =
2964   let new_page = new page () in
2965    empty <- false ;
2966    pages := !pages @ [n,lazy (setgoal n),new_page] ;
2967    notebook#append_page
2968     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
2969     new_page#content#coerce
2970  method remove_all_pages ~skip_switch_page_event:skip =
2971   if empty then
2972    notebook#remove_page 0 (* let's remove the empty page *)
2973   else
2974    List.iter (function _ -> notebook#remove_page 0) !pages ;
2975   pages := [] ;
2976   skip_switch_page_event <- skip
2977  method set_current_page ~may_skip_switch_page_event n =
2978   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
2979    let new_page = notebook#page_num page#content#coerce in
2980     if may_skip_switch_page_event && new_page <> notebook#current_page then
2981      skip_switch_page_event <- true ;
2982     notebook#goto_page new_page
2983  method set_empty_page =
2984   empty <- true ;
2985   pages := [] ;
2986   notebook#append_page
2987    ~tab_label:((GMisc.label ~text:"No proof in progress" ())#coerce)
2988    empty_page#content#coerce
2989  method proofw =
2990   let (_,_,page) = List.nth !pages notebook#current_page in
2991    page#proofw
2992  initializer
2993   ignore
2994    (notebook#connect#switch_page
2995     (function i ->
2996       let skip = skip_switch_page_event in
2997        skip_switch_page_event <- false ;
2998        if not skip then
2999         try
3000          let (metano,setgoal,page) = List.nth !pages i in
3001           ProofEngine.goal := Some metano ;
3002           Lazy.force (page#compute) ;
3003           Lazy.force setgoal
3004         with _ -> ()
3005     ))
3006 end
3007 ;;
3008
3009 (* Main window *)
3010
3011 class rendering_window output (notebook : notebook) =
3012  let scratch_window = new scratch_window in
3013  let window =
3014   GWindow.window ~title:"MathML viewer" ~border_width:0
3015    ~allow_shrink:false () in
3016  let vbox_for_menu = GPack.vbox ~packing:window#add () in
3017  (* menus *)
3018  let handle_box = GBin.handle_box ~border_width:2
3019   ~packing:(vbox_for_menu#pack ~padding:0) () in
3020  let menubar = GMenu.menu_bar ~packing:handle_box#add () in
3021  let factory0 = new GMenu.factory menubar in
3022  let accel_group = factory0#accel_group in
3023  (* file menu *)
3024  let file_menu = factory0#add_submenu "File" in
3025  let factory1 = new GMenu.factory file_menu ~accel_group in
3026  let export_to_postscript_menu_item =
3027   begin
3028    let _ =
3029     factory1#add_item "New Block of (Co)Inductive Definitions..."
3030      ~key:GdkKeysyms._B ~callback:new_inductive
3031    in
3032    let _ =
3033     factory1#add_item "New Proof or Definition..." ~key:GdkKeysyms._N
3034      ~callback:new_proof
3035    in
3036    let reopen_menu_item =
3037     factory1#add_item "Reopen a Finished Proof..." ~key:GdkKeysyms._R
3038      ~callback:open_
3039    in
3040    let qed_menu_item =
3041     factory1#add_item "Qed" ~key:GdkKeysyms._E ~callback:qed in
3042    ignore (factory1#add_separator ()) ;
3043    ignore
3044     (factory1#add_item "Load Unfinished Proof..." ~key:GdkKeysyms._L
3045       ~callback:load) ;
3046    let save_menu_item =
3047     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S ~callback:save
3048    in
3049    ignore
3050     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
3051    ignore (!save_set_sensitive false);
3052    ignore (qed_set_sensitive:=function b -> qed_menu_item#misc#set_sensitive b);
3053    ignore (!qed_set_sensitive false);
3054    ignore (factory1#add_separator ()) ;
3055    let export_to_postscript_menu_item =
3056     factory1#add_item "Export to PostScript..."
3057      ~callback:(export_to_postscript output) in
3058    ignore (factory1#add_separator ()) ;
3059    ignore
3060     (factory1#add_item "Exit" ~key:GdkKeysyms._Q ~callback:GMain.Main.quit) ;
3061    export_to_postscript_menu_item
3062   end in
3063  (* edit menu *)
3064  let edit_menu = factory0#add_submenu "Edit Current Proof" in
3065  let factory2 = new GMenu.factory edit_menu ~accel_group in
3066  let focus_and_proveit_set_sensitive = ref (function _ -> assert false) in
3067  let proveit_menu_item =
3068   factory2#add_item "Prove It" ~key:GdkKeysyms._I
3069    ~callback:(function () -> proveit ();!focus_and_proveit_set_sensitive false)
3070  in
3071  let focus_menu_item =
3072   factory2#add_item "Focus" ~key:GdkKeysyms._F
3073    ~callback:(function () -> focus () ; !focus_and_proveit_set_sensitive false)
3074  in
3075  let _ =
3076   focus_and_proveit_set_sensitive :=
3077    function b ->
3078     proveit_menu_item#misc#set_sensitive b ;
3079     focus_menu_item#misc#set_sensitive b
3080  in
3081  let _ = !focus_and_proveit_set_sensitive false in
3082  (* edit term menu *)
3083  let edit_term_menu = factory0#add_submenu "Edit Term" in
3084  let factory5 = new GMenu.factory edit_term_menu ~accel_group in
3085  let check_menu_item =
3086   factory5#add_item "Check Term" ~key:GdkKeysyms._C
3087    ~callback:(check scratch_window) in
3088  let _ = check_menu_item#misc#set_sensitive false in
3089  (* search menu *)
3090  let settings_menu = factory0#add_submenu "Search" in
3091  let factory4 = new GMenu.factory settings_menu ~accel_group in
3092  let _ =
3093   factory4#add_item "Locate..." ~key:GdkKeysyms._T
3094    ~callback:locate in
3095  let searchPattern_menu_item =
3096   factory4#add_item "SearchPattern..." ~key:GdkKeysyms._D
3097    ~callback:completeSearchPattern in
3098  let _ = searchPattern_menu_item#misc#set_sensitive false in
3099  let show_menu_item =
3100   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
3101  in
3102  (* settings menu *)
3103  let settings_menu = factory0#add_submenu "Settings" in
3104  let factory3 = new GMenu.factory settings_menu ~accel_group in
3105  let _ =
3106   factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
3107    ~callback:edit_aliases in
3108  let _ = factory3#add_separator () in
3109  let _ =
3110   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
3111    ~callback:(function _ -> (settings_window ())#show ()) in
3112  (* accel group *)
3113  let _ = window#add_accel_group accel_group in
3114  (* end of menus *)
3115  let hbox0 =
3116   GPack.hbox
3117    ~packing:(vbox_for_menu#pack ~expand:true ~fill:true ~padding:5) () in
3118  let vbox =
3119   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3120  let scrolled_window0 =
3121   GBin.scrolled_window ~border_width:10
3122    ~packing:(vbox#pack ~expand:true ~padding:5) () in
3123  let _ = scrolled_window0#add output#coerce in
3124  let frame =
3125   GBin.frame ~label:"Insert Term"
3126    ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
3127  let scrolled_window1 =
3128   GBin.scrolled_window ~border_width:5
3129    ~packing:frame#add () in
3130  let inputt =
3131   new term_editor ~width:400 ~height:100 ~packing:scrolled_window1#add ()
3132    ~isnotempty_callback:
3133     (function b ->
3134       check_menu_item#misc#set_sensitive b ;
3135       searchPattern_menu_item#misc#set_sensitive b) in
3136  let vboxl =
3137   GPack.vbox ~packing:(hbox0#pack ~expand:true ~fill:true ~padding:5) () in
3138  let _ =
3139   vboxl#pack ~expand:true ~fill:true ~padding:5 notebook#notebook#coerce in
3140  let frame =
3141   GBin.frame ~shadow_type:`IN ~packing:(vboxl#pack ~expand:true ~padding:5) ()
3142  in
3143  let outputhtml =
3144   GHtml.xmhtml
3145    ~source:"<html><body bgColor=\"white\"></body></html>"
3146    ~width:400 ~height: 100
3147    ~border_width:20
3148    ~packing:frame#add
3149    ~show:true () in
3150 object
3151  method outputhtml = outputhtml
3152  method inputt = inputt
3153  method output = (output : GMathView.math_view)
3154  method notebook = notebook
3155  method show = window#show
3156  initializer
3157   notebook#set_empty_page ;
3158   export_to_postscript_menu_item#misc#set_sensitive false ;
3159   check_term := (check_term_in_scratch scratch_window) ;
3160
3161   (* signal handlers here *)
3162   ignore(output#connect#selection_changed
3163    (function elem ->
3164      choose_selection output elem ;
3165      !focus_and_proveit_set_sensitive true
3166    )) ;
3167   ignore (output#connect#clicked (show_in_show_window_callback output)) ;
3168   let settings_window = new settings_window output scrolled_window0
3169    export_to_postscript_menu_item (choose_selection output) in
3170   set_settings_window settings_window ;
3171   set_outputhtml outputhtml ;
3172   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
3173   Logger.log_callback :=
3174    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
3175 end;;
3176
3177 (* MAIN *)
3178
3179 let initialize_everything () =
3180  let module U = Unix in
3181   let output = GMathView.math_view ~width:350 ~height:280 () in
3182   let notebook = new notebook in
3183    let rendering_window' = new rendering_window output notebook in
3184     set_rendering_window rendering_window' ;
3185     mml_of_cic_term_ref := mml_of_cic_term ;
3186     rendering_window'#show () ;
3187     GMain.Main.main ()
3188 ;;
3189
3190 let _ =
3191  if !usedb then
3192   begin
3193    Mqint.set_database Mqint.postgres_db ;
3194    (* Mqint.init "dbname=helm_mowgli" ; *)
3195    (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *)
3196    Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm";
3197   end ;
3198  ignore (GtkMain.Main.init ()) ;
3199  initialize_everything () ;
3200  if !usedb then Mqint.close ();
3201 ;;