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