helm/gTopLevel/gTopLevel.ml

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