helm/gTopLevel/gTopLevel.ml

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