helm/gTopLevel/gTopLevel.ml

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