helm/gTopLevel/gTopLevel.ml

   1 (* Copyright (C) 2000, 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 (* GLOBAL CONSTANTS *)
  37
  38 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
  39
  40 let htmlheader =
  41  "<html>" ^
  42  " <body bgColor=\"white\">"
  43 ;;
  44
  45 let htmlfooter =
  46  " </body>" ^
  47  "</html>"
  48 ;;
  49
  50 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  51
  52 let htmlheader_and_content = ref htmlheader;;
  53
  54 let current_cic_infos = ref None;;
  55 let current_goal_infos = ref None;;
  56 let current_scratch_infos = ref None;;
  57
  58
  59 (* MISC FUNCTIONS *)
  60
  61 let domImpl = Gdome.domImplementation ();;
  62
  63 let parseStyle name =
  64  let style =
  65   domImpl#createDocumentFromURI
  66 (*
  67    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
  68 *)
  69    ~uri:("styles/" ^ name) ()
  70  in
  71   Gdome_xslt.processStylesheet style
  72 ;;
  73
  74 let d_c = parseStyle "drop_coercions.xsl";;
  75 let tc1 = parseStyle "objtheorycontent.xsl";;
  76 let hc2 = parseStyle "content_to_html.xsl";;
  77 let l   = parseStyle "link.xsl";;
  78
  79 let c1 = parseStyle "rootcontent.xsl";;
  80 let g  = parseStyle "genmmlid.xsl";;
  81 let c2 = parseStyle "annotatedpres.xsl";;
  82
  83
  84 let getterURL = Configuration.getter_url;;
  85 let processorURL = Configuration.processor_url;;
  86
  87 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
  88 let mml_args =
  89  ["processorURL", "'" ^ processorURL ^ "'" ;
  90   "getterURL", "'" ^ getterURL ^ "'" ;
  91   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
  92   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
  93   "UNICODEvsSYMBOL", "'symbol'" ;
  94   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
  95   "encoding", "'iso-8859-1'" ;
  96   "media-type", "'text/html'" ;
  97   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
  98   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
  99   "naturalLanguage", "'yes'" ;
 100   "annotations", "'no'" ;
 101   "explodeall", "'true()'" ;
 102   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 103   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 104 ;;
 105
 106 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 107 let sequent_args =
 108  ["processorURL", "'" ^ processorURL ^ "'" ;
 109   "getterURL", "'" ^ getterURL ^ "'" ;
 110   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 111   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 112   "UNICODEvsSYMBOL", "'symbol'" ;
 113   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 114   "encoding", "'iso-8859-1'" ;
 115   "media-type", "'text/html'" ;
 116   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 117   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 118   "naturalLanguage", "'no'" ;
 119   "annotations", "'no'" ;
 120   "explodeall", "'true()'" ;
 121   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 122   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 123 ;;
 124
 125 let parse_file filename =
 126  let inch = open_in filename in
 127   let rec read_lines () =
 128    try
 129     let line = input_line inch in
 130      line ^ read_lines ()
 131    with
 132     End_of_file -> ""
 133   in
 134    read_lines ()
 135 ;;
 136
 137 let applyStylesheets input styles args =
 138  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 139   input styles
 140 ;;
 141
 142 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 143  let xml =
 144   Cic2Xml.print_object uri ids_to_inner_sorts annobj
 145  in
 146  let xmlinnertypes =
 147   Cic2Xml.print_inner_types uri ids_to_inner_sorts
 148    ids_to_inner_types
 149  in
 150   let input = Xml2Gdome.document_of_xml domImpl xml in
 151 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 152 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 153 (*CSC: local.                                                              *)
 154    Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
 155    let output = applyStylesheets input mml_styles mml_args in
 156     output
 157 ;;
 158
 159
 160 (* CALLBACKS *)
 161
 162 exception RefreshSequentException of exn;;
 163 exception RefreshProofException of exn;;
 164
 165 let refresh_proof (output : GMathView.math_view) =
 166  try
 167   let uri,currentproof =
 168    match !ProofEngine.proof with
 169       None -> assert false
 170     | Some (uri,metasenv,bo,ty) ->
 171        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
 172   in
 173    let
 174     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
 175    =
 176     Cic2acic.acic_object_of_cic_object currentproof
 177    in
 178     let mml =
 179      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 180     in
 181      output#load_tree mml ;
 182      current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
 183  with
 184   e -> raise (RefreshProofException e)
 185 ;;
 186
 187 let refresh_sequent (proofw : GMathView.math_view) =
 188  try
 189   match !ProofEngine.goal with
 190      None -> proofw#unload
 191    | Some (_,currentsequent) ->
 192       let metasenv =
 193        match !ProofEngine.proof with
 194           None -> assert false
 195         | Some (_,metasenv,_,_) -> metasenv
 196       in
 197        let sequent_gdome,ids_to_terms,ids_to_father_ids =
 198         SequentPp.XmlPp.print_sequent metasenv currentsequent
 199        in
 200         let sequent_doc =
 201          Xml2Gdome.document_of_xml domImpl sequent_gdome
 202         in
 203          let sequent_mml =
 204           applyStylesheets sequent_doc sequent_styles sequent_args
 205          in
 206           proofw#load_tree ~dom:sequent_mml ;
 207           current_goal_infos := Some (ids_to_terms,ids_to_father_ids)
 208  with
 209   e -> raise (RefreshSequentException e)
 210 ;;
 211
 212 (*
 213 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 214  ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
 215 *)
 216
 217 let mml_of_cic_term term =
 218  let context =
 219   match !ProofEngine.goal with
 220      None -> []
 221    | Some (_,(context,_)) -> context
 222  in
 223   let metasenv =
 224    match !ProofEngine.proof with
 225       None -> []
 226     | Some (_,metasenv,_,_) -> metasenv
 227   in
 228    let sequent_gdome,ids_to_terms,ids_to_father_ids =
 229     SequentPp.XmlPp.print_sequent metasenv (context,term)
 230    in
 231     let sequent_doc =
 232      Xml2Gdome.document_of_xml domImpl sequent_gdome
 233     in
 234      let res =
 235       applyStylesheets sequent_doc sequent_styles sequent_args ;
 236      in
 237       current_scratch_infos := Some (term,ids_to_terms,ids_to_father_ids) ;
 238       res
 239 ;;
 240
 241 let output_html outputhtml msg =
 242  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 243  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 244  outputhtml#set_topline (-1)
 245 ;;
 246
 247 (***********************)
 248 (*       TACTICS       *)
 249 (***********************)
 250
 251 let call_tactic tactic rendering_window () =
 252  let proofw = (rendering_window#proofw : GMathView.math_view) in
 253  let output = (rendering_window#output : GMathView.math_view) in
 254  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 255  let savedproof = !ProofEngine.proof in
 256  let savedgoal  = !ProofEngine.goal in
 257   begin
 258    try
 259     tactic () ;
 260     refresh_sequent proofw ;
 261     refresh_proof output
 262    with
 263       RefreshSequentException e ->
 264        output_html outputhtml
 265         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 266          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 267        ProofEngine.proof := savedproof ;
 268        ProofEngine.goal := savedgoal ;
 269        refresh_sequent proofw
 270     | RefreshProofException e ->
 271        output_html outputhtml
 272         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 273          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 274        ProofEngine.proof := savedproof ;
 275        ProofEngine.goal := savedgoal ;
 276        refresh_sequent proofw ;
 277        refresh_proof output
 278     | e ->
 279        output_html outputhtml
 280         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 281        ProofEngine.proof := savedproof ;
 282        ProofEngine.goal := savedgoal ;
 283   end
 284 ;;
 285
 286 let call_tactic_with_input tactic rendering_window () =
 287  let proofw = (rendering_window#proofw : GMathView.math_view) in
 288  let output = (rendering_window#output : GMathView.math_view) in
 289  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 290  let inputt = (rendering_window#inputt : GEdit.text) in
 291  let savedproof = !ProofEngine.proof in
 292  let savedgoal  = !ProofEngine.goal in
 293 (*CSC: Gran cut&paste da sotto... *)
 294   let inputlen = inputt#length in
 295   let input = inputt#get_chars 0 inputlen ^ "\n" in
 296    let lexbuf = Lexing.from_string input in
 297    let curi =
 298     match !ProofEngine.proof with
 299        None -> assert false
 300      | Some (curi,_,_,_) -> curi
 301    in
 302    let context =
 303     List.map
 304      (function
 305          ProofEngine.Definition (n,_)
 306        | ProofEngine.Declaration (n,_) -> n)
 307      (match !ProofEngine.goal with
 308          None -> assert false
 309        | Some (_,(ctx,_)) -> ctx
 310      )
 311    in
 312     try
 313      while true do
 314       match
 315        CicTextualParserContext.main curi context CicTextualLexer.token lexbuf
 316       with
 317          None -> ()
 318        | Some expr ->
 319           tactic expr ;
 320           refresh_sequent proofw ;
 321           refresh_proof output
 322      done
 323     with
 324        CicTextualParser0.Eof ->
 325         inputt#delete_text 0 inputlen
 326      | RefreshSequentException e ->
 327         output_html outputhtml
 328          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 329           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 330         ProofEngine.proof := savedproof ;
 331         ProofEngine.goal := savedgoal ;
 332         refresh_sequent proofw
 333      | RefreshProofException e ->
 334         output_html outputhtml
 335          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 336           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 337         ProofEngine.proof := savedproof ;
 338         ProofEngine.goal := savedgoal ;
 339         refresh_sequent proofw ;
 340         refresh_proof output
 341      | e ->
 342         output_html outputhtml
 343          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 344         ProofEngine.proof := savedproof ;
 345         ProofEngine.goal := savedgoal ;
 346 ;;
 347
 348 let call_tactic_with_goal_input tactic rendering_window () =
 349  let module L = LogicalOperations in
 350  let module G = Gdome in
 351   let proofw = (rendering_window#proofw : GMathView.math_view) in
 352   let output = (rendering_window#output : GMathView.math_view) in
 353   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 354   let savedproof = !ProofEngine.proof in
 355   let savedgoal  = !ProofEngine.goal in
 356    match proofw#get_selection with
 357      Some node ->
 358       let xpath =
 359        ((node : Gdome.element)#getAttributeNS
 360          ~namespaceURI:helmns
 361          ~localName:(G.domString "xref"))#to_string
 362       in
 363        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 364        else
 365         begin
 366          try
 367           match !current_goal_infos with
 368              Some (ids_to_terms, ids_to_father_ids) ->
 369               let id = xpath in
 370                tactic (Hashtbl.find ids_to_terms id) ;
 371                refresh_sequent rendering_window#proofw ;
 372                refresh_proof rendering_window#output
 373            | None -> assert false (* "ERROR: No current term!!!" *)
 374          with
 375             RefreshSequentException e ->
 376              output_html outputhtml
 377               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 378                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 379              ProofEngine.proof := savedproof ;
 380              ProofEngine.goal := savedgoal ;
 381              refresh_sequent proofw
 382           | RefreshProofException e ->
 383              output_html outputhtml
 384               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 385                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 386              ProofEngine.proof := savedproof ;
 387              ProofEngine.goal := savedgoal ;
 388              refresh_sequent proofw ;
 389              refresh_proof output
 390           | e ->
 391              output_html outputhtml
 392               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 393              ProofEngine.proof := savedproof ;
 394              ProofEngine.goal := savedgoal ;
 395         end
 396    | None ->
 397       output_html outputhtml
 398        ("<h1 color=\"red\">No term selected</h1>")
 399 ;;
 400
 401 let call_tactic_with_input_and_goal_input tactic rendering_window () =
 402  let module L = LogicalOperations in
 403  let module G = Gdome in
 404   let proofw = (rendering_window#proofw : GMathView.math_view) in
 405   let output = (rendering_window#output : GMathView.math_view) in
 406   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 407   let inputt = (rendering_window#inputt : GEdit.text) in
 408   let savedproof = !ProofEngine.proof in
 409   let savedgoal  = !ProofEngine.goal in
 410    match proofw#get_selection with
 411      Some node ->
 412       let xpath =
 413        ((node : Gdome.element)#getAttributeNS
 414          ~namespaceURI:helmns
 415          ~localName:(G.domString "xref"))#to_string
 416       in
 417        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 418        else
 419         begin
 420          try
 421           match !current_goal_infos with
 422              Some (ids_to_terms, ids_to_father_ids) ->
 423               let id = xpath in
 424                (* Let's parse the input *)
 425                let inputlen = inputt#length in
 426                let input = inputt#get_chars 0 inputlen ^ "\n" in
 427                 let lexbuf = Lexing.from_string input in
 428                 let curi =
 429                  match !ProofEngine.proof with
 430                     None -> assert false
 431                   | Some (curi,_,_,_) -> curi
 432                 in
 433                 let context =
 434                  List.map
 435                   (function
 436                       ProofEngine.Definition (n,_)
 437                     | ProofEngine.Declaration (n,_) -> n)
 438                   (match !ProofEngine.goal with
 439                       None -> assert false
 440                     | Some (_,(ctx,_)) -> ctx
 441                   )
 442                 in
 443                  begin
 444                   try
 445                    while true do
 446                     match
 447                      CicTextualParserContext.main curi context
 448                       CicTextualLexer.token lexbuf
 449                     with
 450                        None -> ()
 451                      | Some expr ->
 452                         tactic ~goal_input:(Hashtbl.find ids_to_terms id)
 453                          ~input:expr ;
 454                         refresh_sequent proofw ;
 455                         refresh_proof output
 456                    done
 457                   with
 458                      CicTextualParser0.Eof ->
 459                       inputt#delete_text 0 inputlen
 460                  end
 461            | None -> assert false (* "ERROR: No current term!!!" *)
 462          with
 463             RefreshSequentException e ->
 464              output_html outputhtml
 465               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 466                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 467              ProofEngine.proof := savedproof ;
 468              ProofEngine.goal := savedgoal ;
 469              refresh_sequent proofw
 470           | RefreshProofException e ->
 471              output_html outputhtml
 472               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 473                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 474              ProofEngine.proof := savedproof ;
 475              ProofEngine.goal := savedgoal ;
 476              refresh_sequent proofw ;
 477              refresh_proof output
 478           | e ->
 479              output_html outputhtml
 480               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 481              ProofEngine.proof := savedproof ;
 482              ProofEngine.goal := savedgoal ;
 483         end
 484    | None ->
 485       output_html outputhtml
 486        ("<h1 color=\"red\">No term selected</h1>")
 487 ;;
 488
 489 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
 490  let module L = LogicalOperations in
 491  let module G = Gdome in
 492   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
 493   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
 494   let savedproof = !ProofEngine.proof in
 495   let savedgoal  = !ProofEngine.goal in
 496    match mmlwidget#get_selection with
 497      Some node ->
 498       let xpath =
 499        ((node : Gdome.element)#getAttributeNS
 500          ~namespaceURI:helmns
 501          ~localName:(G.domString "xref"))#to_string
 502       in
 503        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 504        else
 505         begin
 506          try
 507           match !current_scratch_infos with
 508              (* term is the whole goal in the scratch_area *)
 509              Some (term,ids_to_terms, ids_to_father_ids) ->
 510               let id = xpath in
 511                let expr = tactic term (Hashtbl.find ids_to_terms id) in
 512                 let mml = mml_of_cic_term expr in
 513                  scratch_window#show () ;
 514                  scratch_window#mmlwidget#load_tree ~dom:mml
 515            | None -> assert false (* "ERROR: No current term!!!" *)
 516          with
 517           e ->
 518            output_html outputhtml
 519             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 520         end
 521    | None ->
 522       output_html outputhtml
 523        ("<h1 color=\"red\">No term selected</h1>")
 524 ;;
 525
 526 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
 527 let exact rendering_window =
 528  call_tactic_with_input ProofEngine.exact rendering_window
 529 ;;
 530 let apply rendering_window =
 531  call_tactic_with_input ProofEngine.apply rendering_window
 532 ;;
 533 let elimintros rendering_window =
 534  call_tactic_with_input ProofEngine.elim_intros rendering_window
 535 ;;
 536 let whd rendering_window =
 537  call_tactic_with_goal_input ProofEngine.whd rendering_window
 538 ;;
 539 let reduce rendering_window =
 540  call_tactic_with_goal_input ProofEngine.reduce rendering_window
 541 ;;
 542 let simpl rendering_window =
 543  call_tactic_with_goal_input ProofEngine.simpl rendering_window
 544 ;;
 545 let fold rendering_window =
 546  call_tactic_with_input ProofEngine.fold rendering_window
 547 ;;
 548 let cut rendering_window =
 549  call_tactic_with_input ProofEngine.cut rendering_window
 550 ;;
 551 let change rendering_window =
 552  call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
 553 ;;
 554 let letin rendering_window =
 555  call_tactic_with_input ProofEngine.letin rendering_window
 556 ;;
 557
 558
 559 let whd_in_scratch scratch_window =
 560  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
 561   scratch_window
 562 ;;
 563 let reduce_in_scratch scratch_window =
 564  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
 565   scratch_window
 566 ;;
 567 let simpl_in_scratch scratch_window =
 568  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
 569   scratch_window
 570 ;;
 571
 572
 573
 574 (**********************)
 575 (*   END OF TACTICS   *)
 576 (**********************)
 577
 578 exception OpenConjecturesStillThere;;
 579 exception WrongProof;;
 580
 581 let save rendering_window () =
 582  match !ProofEngine.proof with
 583     None -> assert false
 584   | Some (uri,[],bo,ty) ->
 585      if CicReduction.are_convertible (CicTypeChecker.type_of_aux' [] [] bo) ty then
 586       begin
 587        (*CSC: Wrong: [] is just plainly wrong *)
 588        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
 589         let
 590          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 591           ids_to_inner_types)
 592         =
 593          Cic2acic.acic_object_of_cic_object proof
 594         in
 595          let mml =
 596           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 597          in
 598           (rendering_window#output : GMathView.math_view)#load_tree mml ;
 599           current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
 600       end
 601      else
 602       raise WrongProof
 603   | _ -> raise OpenConjecturesStillThere
 604 ;;
 605
 606 let proveit rendering_window () =
 607  let module L = LogicalOperations in
 608  let module G = Gdome in
 609  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 610   match rendering_window#output#get_selection with
 611     Some node ->
 612      let xpath =
 613       ((node : Gdome.element)#getAttributeNS
 614       (*CSC: OCAML DIVERGE
 615       ((element : G.element)#getAttributeNS
 616       *)
 617         ~namespaceURI:helmns
 618         ~localName:(G.domString "xref"))#to_string
 619      in
 620       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 621       else
 622        begin
 623         try
 624          match !current_cic_infos with
 625             Some (ids_to_terms, ids_to_father_ids) ->
 626              let id = xpath in
 627               if L.to_sequent id ids_to_terms ids_to_father_ids then
 628                refresh_proof rendering_window#output ;
 629               refresh_sequent rendering_window#proofw
 630           | None -> assert false (* "ERROR: No current term!!!" *)
 631         with
 632            RefreshSequentException e ->
 633             output_html outputhtml
 634              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 635               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 636          | RefreshProofException e ->
 637             output_html outputhtml
 638              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 639               "proof: " ^ Printexc.to_string e ^ "</h1>")
 640          | e ->
 641             output_html outputhtml
 642              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 643        end
 644   | None -> assert false (* "ERROR: No selection!!!" *)
 645 ;;
 646
 647 exception NotADefinition;;
 648
 649 let open_ rendering_window () =
 650  let inputt = (rendering_window#inputt : GEdit.text) in
 651  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 652  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 653  let output = (rendering_window#output : GMathView.math_view) in
 654  let proofw = (rendering_window#proofw : GMathView.math_view) in
 655   let inputlen = inputt#length in
 656   let input = inputt#get_chars 0 inputlen ^ "\n" in
 657    try
 658     let uri = UriManager.uri_of_string ("cic:" ^ input) in
 659      CicTypeChecker.typecheck uri ;
 660      let metasenv,bo,ty =
 661       match CicEnvironment.get_cooked_obj uri 0 with
 662          Cic.Definition (_,bo,ty,_) -> [],bo,ty
 663        | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
 664        | Cic.Axiom _
 665        | Cic.Variable _
 666        | Cic.InductiveDefinition _ -> raise NotADefinition
 667      in
 668       ProofEngine.proof :=
 669        Some (uri, metasenv, bo, ty) ;
 670       ProofEngine.goal := None ;
 671       refresh_sequent proofw ;
 672       refresh_proof output ;
 673       inputt#delete_text 0 inputlen ;
 674       ignore(oldinputt#insert_text input oldinputt#length)
 675    with
 676       RefreshSequentException e ->
 677        output_html outputhtml
 678         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 679          "sequent: " ^ Printexc.to_string e ^ "</h1>")
 680     | RefreshProofException e ->
 681        output_html outputhtml
 682         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 683          "proof: " ^ Printexc.to_string e ^ "</h1>")
 684     | e ->
 685        output_html outputhtml
 686         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 687 ;;
 688
 689 let state rendering_window () =
 690  let inputt = (rendering_window#inputt : GEdit.text) in
 691  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 692  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 693  let output = (rendering_window#output : GMathView.math_view) in
 694  let proofw = (rendering_window#proofw : GMathView.math_view) in
 695   let inputlen = inputt#length in
 696   let input = inputt#get_chars 0 inputlen ^ "\n" in
 697    (* Do something interesting *)
 698    let lexbuf = Lexing.from_string input in
 699     try
 700      while true do
 701       (* Execute the actions *)
 702       match CicTextualParser.main CicTextualLexer.token lexbuf with
 703          None -> ()
 704        | Some expr ->
 705           let _  = CicTypeChecker.type_of_aux' [] [] expr in
 706            ProofEngine.proof :=
 707             Some (UriManager.uri_of_string "cic:/dummy.con",
 708                    [1,expr], Cic.Meta 1, expr) ;
 709            ProofEngine.goal := Some (1,([],expr)) ;
 710            refresh_sequent proofw ;
 711            refresh_proof output ;
 712      done
 713     with
 714        CicTextualParser0.Eof ->
 715         inputt#delete_text 0 inputlen ;
 716         ignore(oldinputt#insert_text input oldinputt#length)
 717      | RefreshSequentException e ->
 718         output_html outputhtml
 719          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 720           "sequent: " ^ Printexc.to_string e ^ "</h1>")
 721      | RefreshProofException e ->
 722         output_html outputhtml
 723          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 724           "proof: " ^ Printexc.to_string e ^ "</h1>")
 725      | e ->
 726         output_html outputhtml
 727          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 728 ;;
 729
 730 let check rendering_window scratch_window () =
 731  let inputt = (rendering_window#inputt : GEdit.text) in
 732  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 733  let output = (rendering_window#output : GMathView.math_view) in
 734  let proofw = (rendering_window#proofw : GMathView.math_view) in
 735   let inputlen = inputt#length in
 736   let input = inputt#get_chars 0 inputlen ^ "\n" in
 737   let curi,metasenv =
 738    match !ProofEngine.proof with
 739       None -> UriManager.uri_of_string "cic:/dummy.con", []
 740     | Some (curi,metasenv,_,_) -> curi,metasenv
 741   in
 742   let ciccontext,names_context =
 743    let context =
 744     match !ProofEngine.goal with
 745        None -> []
 746      | Some (_,(ctx,_)) -> ctx
 747    in
 748     ProofEngine.cic_context_of_named_context context,
 749      List.map
 750       (function
 751           ProofEngine.Declaration (n,_)
 752         | ProofEngine.Definition (n,_) -> n
 753       ) context
 754   in
 755    (* Do something interesting *)
 756    let lexbuf = Lexing.from_string input in
 757     try
 758      while true do
 759       (* Execute the actions *)
 760       match
 761        CicTextualParserContext.main curi names_context CicTextualLexer.token
 762         lexbuf
 763       with
 764          None -> ()
 765        | Some expr ->
 766           try
 767            let ty  = CicTypeChecker.type_of_aux' metasenv ciccontext expr in
 768             let mml = mml_of_cic_term (Cic.Cast (expr,ty)) in
 769              scratch_window#show () ;
 770              scratch_window#mmlwidget#load_tree ~dom:mml
 771           with
 772            e ->
 773             print_endline ("? " ^ CicPp.ppterm expr) ;
 774             raise e
 775      done
 776     with
 777        CicTextualParser0.Eof -> ()
 778      | e ->
 779        output_html outputhtml
 780         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 781 ;;
 782
 783 let choose_selection
 784      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
 785 =
 786  let module G = Gdome in
 787   let rec aux element =
 788    if element#hasAttributeNS
 789        ~namespaceURI:helmns
 790        ~localName:(G.domString "xref")
 791    then
 792      mmlwidget#set_selection (Some element)
 793    else
 794       match element#get_parentNode with
 795          None -> assert false
 796        (*CSC: OCAML DIVERGES!
 797        | Some p -> aux (new G.element_of_node p)
 798        *)
 799        | Some p -> aux (new Gdome.element_of_node p)
 800   in
 801    match element with
 802      Some x -> aux x
 803    | None   -> mmlwidget#set_selection None
 804 ;;
 805
 806 (* STUFF TO BUILD THE GTK INTERFACE *)
 807
 808 (* Stuff for the widget settings *)
 809
 810 let export_to_postscript (output : GMathView.math_view) () =
 811  output#export_to_postscript ~filename:"output.ps" ();
 812 ;;
 813
 814 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
 815  button_set_kerning button_set_transparency button_export_to_postscript
 816  button_t1 ()
 817 =
 818  let is_set = button_t1#active in
 819   output#set_font_manager_type
 820    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
 821   if is_set then
 822    begin
 823     button_set_anti_aliasing#misc#set_sensitive true ;
 824     button_set_kerning#misc#set_sensitive true ;
 825     button_set_transparency#misc#set_sensitive true ;
 826     button_export_to_postscript#misc#set_sensitive true ;
 827    end
 828   else
 829    begin
 830     button_set_anti_aliasing#misc#set_sensitive false ;
 831     button_set_kerning#misc#set_sensitive false ;
 832     button_set_transparency#misc#set_sensitive false ;
 833     button_export_to_postscript#misc#set_sensitive false ;
 834    end
 835 ;;
 836
 837 let set_anti_aliasing output button_set_anti_aliasing () =
 838  output#set_anti_aliasing button_set_anti_aliasing#active
 839 ;;
 840
 841 let set_kerning output button_set_kerning () =
 842  output#set_kerning button_set_kerning#active
 843 ;;
 844
 845 let set_transparency output button_set_transparency () =
 846  output#set_transparency button_set_transparency#active
 847 ;;
 848
 849 let changefont output font_size_spinb () =
 850  output#set_font_size font_size_spinb#value_as_int
 851 ;;
 852
 853 let set_log_verbosity output log_verbosity_spinb () =
 854  output#set_log_verbosity log_verbosity_spinb#value_as_int
 855 ;;
 856
 857 class settings_window (output : GMathView.math_view) sw
 858  button_export_to_postscript selection_changed_callback
 859 =
 860  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
 861  let vbox =
 862   GPack.vbox ~packing:settings_window#add () in
 863  let table =
 864   GPack.table
 865    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 866    ~border_width:5 ~packing:vbox#add () in
 867  let button_t1 =
 868   GButton.toggle_button ~label:"activate t1 fonts"
 869    ~packing:(table#attach ~left:0 ~top:0) () in
 870  let button_set_anti_aliasing =
 871   GButton.toggle_button ~label:"set_anti_aliasing"
 872    ~packing:(table#attach ~left:0 ~top:1) () in
 873  let button_set_kerning =
 874   GButton.toggle_button ~label:"set_kerning"
 875    ~packing:(table#attach ~left:1 ~top:1) () in
 876  let button_set_transparency =
 877   GButton.toggle_button ~label:"set_transparency"
 878    ~packing:(table#attach ~left:2 ~top:1) () in
 879  let table =
 880   GPack.table
 881    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
 882    ~border_width:5 ~packing:vbox#add () in
 883  let font_size_label =
 884   GMisc.label ~text:"font size:"
 885    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
 886  let font_size_spinb =
 887   let sadj =
 888    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
 889   in
 890    GEdit.spin_button
 891     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
 892  let log_verbosity_label =
 893   GMisc.label ~text:"log verbosity:"
 894    ~packing:(table#attach ~left:0 ~top:1) () in
 895  let log_verbosity_spinb =
 896   let sadj =
 897    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
 898   in
 899    GEdit.spin_button
 900     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
 901  let hbox =
 902   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 903  let closeb =
 904   GButton.button ~label:"Close"
 905    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 906 object(self)
 907  method show = settings_window#show
 908  initializer
 909   button_set_anti_aliasing#misc#set_sensitive false ;
 910   button_set_kerning#misc#set_sensitive false ;
 911   button_set_transparency#misc#set_sensitive false ;
 912   (* Signals connection *)
 913   ignore(button_t1#connect#clicked
 914    (activate_t1 output button_set_anti_aliasing button_set_kerning
 915     button_set_transparency button_export_to_postscript button_t1)) ;
 916   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
 917   ignore(button_set_anti_aliasing#connect#toggled
 918    (set_anti_aliasing output button_set_anti_aliasing));
 919   ignore(button_set_kerning#connect#toggled
 920    (set_kerning output button_set_kerning)) ;
 921   ignore(button_set_transparency#connect#toggled
 922    (set_transparency output button_set_transparency)) ;
 923   ignore(log_verbosity_spinb#connect#changed
 924    (set_log_verbosity output log_verbosity_spinb)) ;
 925   ignore(closeb#connect#clicked settings_window#misc#hide)
 926 end;;
 927
 928 (* Scratch window *)
 929
 930 class scratch_window outputhtml =
 931  let window =
 932   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 933  let vbox =
 934   GPack.vbox ~packing:window#add () in
 935  let hbox =
 936   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 937  let whdb =
 938   GButton.button ~label:"Whd"
 939    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 940  let reduceb =
 941   GButton.button ~label:"Reduce"
 942    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 943  let simplb =
 944   GButton.button ~label:"Simpl"
 945    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
 946  let scrolled_window =
 947   GBin.scrolled_window ~border_width:10
 948    ~packing:(vbox#pack ~expand:true ~padding:5) () in
 949  let mmlwidget =
 950   GMathView.math_view
 951    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
 952 object(self)
 953  method outputhtml = outputhtml
 954  method mmlwidget = mmlwidget
 955  method show () = window#misc#hide () ; window#show ()
 956  initializer
 957   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
 958   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
 959   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
 960   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
 961   ignore(simplb#connect#clicked (simpl_in_scratch self))
 962 end;;
 963
 964 (* Main window *)
 965
 966 class rendering_window output proofw (label : GMisc.label) =
 967  let window =
 968   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
 969  let hbox0 =
 970   GPack.hbox ~packing:window#add () in
 971  let vbox =
 972   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
 973  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
 974  let scrolled_window0 =
 975   GBin.scrolled_window ~border_width:10
 976    ~packing:(vbox#pack ~expand:true ~padding:5) () in
 977  let _ = scrolled_window0#add output#coerce in
 978  let hbox1 =
 979   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 980  let settingsb =
 981   GButton.button ~label:"Settings"
 982    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 983  let button_export_to_postscript =
 984   GButton.button ~label:"export_to_postscript"
 985   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 986  let saveb =
 987   GButton.button ~label:"Save"
 988    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 989  let closeb =
 990   GButton.button ~label:"Close"
 991    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
 992  let hbox2 =
 993   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
 994  let proveitb =
 995   GButton.button ~label:"Prove It"
 996    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
 997  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
 998    ~packing:(vbox#pack ~padding:5) () in
 999  let hbox4 =
1000   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1001  let stateb =
1002   GButton.button ~label:"State"
1003    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1004  let openb =
1005   GButton.button ~label:"Open"
1006    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1007  let checkb =
1008   GButton.button ~label:"Check"
1009    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1010  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1011    ~packing:(vbox#pack ~padding:5) () in
1012  let vbox1 =
1013   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1014  let scrolled_window1 =
1015   GBin.scrolled_window ~border_width:10
1016    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1017  let _ = scrolled_window1#add proofw#coerce in
1018  let hbox3 =
1019   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1020  let exactb =
1021   GButton.button ~label:"Exact"
1022    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1023  let introsb =
1024   GButton.button ~label:"Intros"
1025    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1026  let applyb =
1027   GButton.button ~label:"Apply"
1028    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1029  let elimintrosb =
1030   GButton.button ~label:"ElimIntros"
1031    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1032  let whdb =
1033   GButton.button ~label:"Whd"
1034    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1035  let reduceb =
1036   GButton.button ~label:"Reduce"
1037    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1038  let simplb =
1039   GButton.button ~label:"Simpl"
1040    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1041  let foldb =
1042   GButton.button ~label:"Fold"
1043    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1044  let cutb =
1045   GButton.button ~label:"Cut"
1046    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1047  let changeb =
1048   GButton.button ~label:"Change"
1049    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1050  let letinb =
1051   GButton.button ~label:"Let ... In"
1052    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1053  let outputhtml =
1054   GHtml.xmhtml
1055    ~source:"<html><body bgColor=\"white\"></body></html>"
1056    ~width:400 ~height: 200
1057    ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1058    ~show:true () in
1059  let scratch_window = new scratch_window outputhtml in
1060 object(self)
1061  method outputhtml = outputhtml
1062  method oldinputt = oldinputt
1063  method inputt = inputt
1064  method output = (output : GMathView.math_view)
1065  method proofw = (proofw : GMathView.math_view)
1066  method show = window#show
1067  initializer
1068   button_export_to_postscript#misc#set_sensitive false ;
1069
1070   (* signal handlers here *)
1071   ignore(output#connect#selection_changed
1072    (function elem -> proofw#unload ; choose_selection output elem)) ;
1073   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1074   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1075   let settings_window = new settings_window output scrolled_window0
1076    button_export_to_postscript (choose_selection output) in
1077   ignore(settingsb#connect#clicked settings_window#show) ;
1078   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1079   ignore(saveb#connect#clicked (save self)) ;
1080   ignore(proveitb#connect#clicked (proveit self)) ;
1081   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1082   ignore(stateb#connect#clicked (state self)) ;
1083   ignore(openb#connect#clicked (open_ self)) ;
1084   ignore(checkb#connect#clicked (check self scratch_window)) ;
1085   ignore(exactb#connect#clicked (exact self)) ;
1086   ignore(applyb#connect#clicked (apply self)) ;
1087   ignore(elimintrosb#connect#clicked (elimintros self)) ;
1088   ignore(whdb#connect#clicked (whd self)) ;
1089   ignore(reduceb#connect#clicked (reduce self)) ;
1090   ignore(simplb#connect#clicked (simpl self)) ;
1091   ignore(foldb#connect#clicked (fold self)) ;
1092   ignore(cutb#connect#clicked (cut self)) ;
1093   ignore(changeb#connect#clicked (change self)) ;
1094   ignore(letinb#connect#clicked (letin self)) ;
1095   ignore(introsb#connect#clicked (intros self)) ;
1096   Logger.log_callback :=
1097    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1098 end;;
1099
1100 (* MAIN *)
1101
1102 let initialize_everything () =
1103  let module U = Unix in
1104   let output = GMathView.math_view ~width:400 ~height:280 ()
1105   and proofw = GMathView.math_view ~width:400 ~height:275 ()
1106   and label = GMisc.label ~text:"gTopLevel" () in
1107     let rendering_window =
1108      new rendering_window output proofw label
1109     in
1110      rendering_window#show () ;
1111      GMain.Main.main ()
1112 ;;
1113
1114 let _ =
1115  CicCooking.init () ;
1116  ignore (GtkMain.Main.init ()) ;
1117  initialize_everything ()
1118 ;;