helm/gTopLevel/gTopLevel.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  31 (*                                 06/01/2002                                 *)
  32 (*                                                                            *)
  33 (*                                                                            *)
  34 (******************************************************************************)
  35
  36
  37 (* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
  38 let wrong_xpointer_format_from_wrong_xpointer_format' uri =
  39  try
  40   let index_sharp =  String.index uri '#' in
  41   let index_rest = index_sharp + 10 in
  42    let baseuri = String.sub uri 0 index_sharp in
  43    let rest = String.sub uri index_rest (String.length uri - index_rest - 1) in
  44     baseuri ^ "#" ^ rest
  45  with Not_found -> uri
  46 ;;
  47
  48 (* GLOBAL CONSTANTS *)
  49
  50 let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
  51
  52 let htmlheader =
  53  "<html>" ^
  54  " <body bgColor=\"white\">"
  55 ;;
  56
  57 let htmlfooter =
  58  " </body>" ^
  59  "</html>"
  60 ;;
  61
  62 (*
  63 let prooffile = "/home/tassi/miohelm/tmp/currentproof";;
  64 *)
  65 let prooffile = "/public/sacerdot/currentproof";;
  66 (*CSC: the getter should handle the innertypes, not the FS *)
  67 (*
  68 let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
  69 *)
  70 let innertypesfile = "/public/sacerdot/innertypes";;
  71
  72 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
  73
  74 let htmlheader_and_content = ref htmlheader;;
  75
  76 let current_cic_infos = ref None;;
  77 let current_goal_infos = ref None;;
  78 let current_scratch_infos = ref None;;
  79
  80 (* COMMAND LINE OPTIONS *)
  81
  82 let usedb = ref true
  83
  84 let argspec =
  85   [
  86     "-nodb", Arg.Clear usedb, "disable use of MathQL DB"
  87   ]
  88 in
  89 Arg.parse argspec ignore ""
  90
  91
  92 (* MISC FUNCTIONS *)
  93
  94 let domImpl = Gdome.domImplementation ();;
  95
  96 let parseStyle name =
  97  let style =
  98   domImpl#createDocumentFromURI
  99 (*
 100    ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None
 101 *)
 102    ~uri:("styles/" ^ name) ()
 103  in
 104   Gdome_xslt.processStylesheet style
 105 ;;
 106
 107 let d_c = parseStyle "drop_coercions.xsl";;
 108 let tc1 = parseStyle "objtheorycontent.xsl";;
 109 let hc2 = parseStyle "content_to_html.xsl";;
 110 let l   = parseStyle "link.xsl";;
 111
 112 let c1 = parseStyle "rootcontent.xsl";;
 113 let g  = parseStyle "genmmlid.xsl";;
 114 let c2 = parseStyle "annotatedpres.xsl";;
 115
 116
 117 let getterURL = Configuration.getter_url;;
 118 let processorURL = Configuration.processor_url;;
 119
 120 let mml_styles = [d_c ; c1 ; g ; c2 ; l];;
 121 let mml_args =
 122  ["processorURL", "'" ^ processorURL ^ "'" ;
 123   "getterURL", "'" ^ getterURL ^ "'" ;
 124   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 125   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 126   "UNICODEvsSYMBOL", "'symbol'" ;
 127   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 128   "encoding", "'iso-8859-1'" ;
 129   "media-type", "'text/html'" ;
 130   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 131   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 132   "naturalLanguage", "'yes'" ;
 133   "annotations", "'no'" ;
 134   "explodeall", "'true()'" ;
 135   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 136   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 137 ;;
 138
 139 let sequent_styles = [d_c ; c1 ; g ; c2 ; l];;
 140 let sequent_args =
 141  ["processorURL", "'" ^ processorURL ^ "'" ;
 142   "getterURL", "'" ^ getterURL ^ "'" ;
 143   "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ;
 144   "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ;
 145   "UNICODEvsSYMBOL", "'symbol'" ;
 146   "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ;
 147   "encoding", "'iso-8859-1'" ;
 148   "media-type", "'text/html'" ;
 149   "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
 150   "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
 151   "naturalLanguage", "'no'" ;
 152   "annotations", "'no'" ;
 153   "explodeall", "'true()'" ;
 154   "topurl", "'http://phd.cs.unibo.it/helm'" ;
 155   "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
 156 ;;
 157
 158 let parse_file filename =
 159  let inch = open_in filename in
 160   let rec read_lines () =
 161    try
 162     let line = input_line inch in
 163      line ^ read_lines ()
 164    with
 165     End_of_file -> ""
 166   in
 167    read_lines ()
 168 ;;
 169
 170 let applyStylesheets input styles args =
 171  List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args)
 172   input styles
 173 ;;
 174
 175 let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 176  let xml =
 177   Cic2Xml.print_object uri ~ids_to_inner_sorts annobj
 178  in
 179  let xmlinnertypes =
 180   Cic2Xml.print_inner_types uri ~ids_to_inner_sorts
 181    ~ids_to_inner_types
 182  in
 183   let input = Xml2Gdome.document_of_xml domImpl xml in
 184 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 185 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 186 (*CSC: local.                                                              *)
 187    Xml.pp xmlinnertypes (Some innertypesfile) ;
 188    let output = applyStylesheets input mml_styles mml_args in
 189     output
 190 ;;
 191
 192
 193 (* CALLBACKS *)
 194
 195 exception RefreshSequentException of exn;;
 196 exception RefreshProofException of exn;;
 197
 198 let refresh_proof (output : GMathView.math_view) =
 199  try
 200   let uri,currentproof =
 201    match !ProofEngine.proof with
 202       None -> assert false
 203     | Some (uri,metasenv,bo,ty) ->
 204        uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty))
 205   in
 206    let
 207     (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 208      ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 209    =
 210     Cic2acic.acic_object_of_cic_object currentproof
 211    in
 212     let mml =
 213      mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 214     in
 215      output#load_tree mml ;
 216      current_cic_infos :=
 217       Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses)
 218  with
 219   e ->
 220  match !ProofEngine.proof with
 221     None -> assert false
 222   | Some (uri,metasenv,bo,ty) ->
 223 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ;
 224    raise (RefreshProofException e)
 225 ;;
 226
 227 let refresh_sequent (proofw : GMathView.math_view) =
 228  try
 229   match !ProofEngine.goal with
 230      None -> proofw#unload
 231    | Some metano ->
 232       let metasenv =
 233        match !ProofEngine.proof with
 234           None -> assert false
 235         | Some (_,metasenv,_,_) -> metasenv
 236       in
 237       let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 238        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 239         SequentPp.XmlPp.print_sequent metasenv currentsequent
 240        in
 241         let sequent_doc =
 242          Xml2Gdome.document_of_xml domImpl sequent_gdome
 243         in
 244          let sequent_mml =
 245           applyStylesheets sequent_doc sequent_styles sequent_args
 246          in
 247           proofw#load_tree ~dom:sequent_mml ;
 248           current_goal_infos :=
 249            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
 250  with
 251   e ->
 252 let metano =
 253   match !ProofEngine.goal with
 254      None -> assert false
 255    | Some m -> m
 256 in
 257 let metasenv =
 258  match !ProofEngine.proof with
 259     None -> assert false
 260   | Some (_,metasenv,_,_) -> metasenv
 261 in
 262 let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in
 263 prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ;
 264    raise (RefreshSequentException e)
 265 ;;
 266
 267 (*
 268 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
 269  ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 270 *)
 271
 272 let mml_of_cic_term metano term =
 273  let metasenv =
 274   match !ProofEngine.proof with
 275      None -> []
 276    | Some (_,metasenv,_,_) -> metasenv
 277  in
 278  let context =
 279   match !ProofEngine.goal with
 280      None -> []
 281    | Some metano ->
 282       let (_,canonical_context,_) =
 283        List.find (function (m,_,_) -> m=metano) metasenv
 284       in
 285        canonical_context
 286  in
 287    let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
 288     SequentPp.XmlPp.print_sequent metasenv (metano,context,term)
 289    in
 290     let sequent_doc =
 291      Xml2Gdome.document_of_xml domImpl sequent_gdome
 292     in
 293      let res =
 294       applyStylesheets sequent_doc sequent_styles sequent_args ;
 295      in
 296       current_scratch_infos :=
 297        Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ;
 298       res
 299 ;;
 300
 301 let output_html outputhtml msg =
 302  htmlheader_and_content := !htmlheader_and_content ^ msg ;
 303  outputhtml#source (!htmlheader_and_content ^ htmlfooter) ;
 304  outputhtml#set_topline (-1)
 305 ;;
 306
 307 (***********************)
 308 (*       TACTICS       *)
 309 (***********************)
 310
 311 let call_tactic tactic rendering_window () =
 312  let proofw = (rendering_window#proofw : GMathView.math_view) in
 313  let output = (rendering_window#output : GMathView.math_view) in
 314  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 315  let savedproof = !ProofEngine.proof in
 316  let savedgoal  = !ProofEngine.goal in
 317   begin
 318    try
 319     tactic () ;
 320     refresh_sequent proofw ;
 321     refresh_proof output
 322    with
 323       RefreshSequentException e ->
 324        output_html outputhtml
 325         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 326          "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 327        ProofEngine.proof := savedproof ;
 328        ProofEngine.goal := savedgoal ;
 329        refresh_sequent proofw
 330     | RefreshProofException e ->
 331        output_html outputhtml
 332         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 333          "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 334        ProofEngine.proof := savedproof ;
 335        ProofEngine.goal := savedgoal ;
 336        refresh_sequent proofw ;
 337        refresh_proof output
 338     | e ->
 339        output_html outputhtml
 340         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 341        ProofEngine.proof := savedproof ;
 342        ProofEngine.goal := savedgoal ;
 343   end
 344 ;;
 345
 346 let call_tactic_with_input tactic rendering_window () =
 347  let proofw = (rendering_window#proofw : GMathView.math_view) in
 348  let output = (rendering_window#output : GMathView.math_view) in
 349  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 350  let inputt = (rendering_window#inputt : GEdit.text) in
 351  let savedproof = !ProofEngine.proof in
 352  let savedgoal  = !ProofEngine.goal in
 353 (*CSC: Gran cut&paste da sotto... *)
 354   let inputlen = inputt#length in
 355   let input = inputt#get_chars 0 inputlen ^ "\n" in
 356    let lexbuf = Lexing.from_string input in
 357    let curi =
 358     match !ProofEngine.proof with
 359        None -> assert false
 360      | Some (curi,_,_,_) -> curi
 361    in
 362    let uri,metasenv,bo,ty =
 363     match !ProofEngine.proof with
 364        None -> assert false
 365      | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 366    in
 367    let context =
 368     List.map
 369      (function
 370          Some (n,_) -> Some n
 371        | None -> None)
 372      (match !ProofEngine.goal with
 373          None -> assert false
 374        | Some metano ->
 375           let (_,canonical_context,_) =
 376            List.find (function (m,_,_) -> m=metano) metasenv
 377           in
 378            canonical_context
 379      )
 380    in
 381     try
 382      while true do
 383       match
 384        CicTextualParserContext.main
 385         curi context metasenv CicTextualLexer.token lexbuf
 386       with
 387          None -> ()
 388        | Some (metasenv',expr) ->
 389           ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 390           tactic expr ;
 391           refresh_sequent proofw ;
 392           refresh_proof output
 393      done
 394     with
 395        CicTextualParser0.Eof ->
 396         inputt#delete_text 0 inputlen
 397      | RefreshSequentException e ->
 398         output_html outputhtml
 399          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 400           "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 401         ProofEngine.proof := savedproof ;
 402         ProofEngine.goal := savedgoal ;
 403         refresh_sequent proofw
 404      | RefreshProofException e ->
 405         output_html outputhtml
 406          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 407           "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 408         ProofEngine.proof := savedproof ;
 409         ProofEngine.goal := savedgoal ;
 410         refresh_sequent proofw ;
 411         refresh_proof output
 412      | e ->
 413         output_html outputhtml
 414          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 415         ProofEngine.proof := savedproof ;
 416         ProofEngine.goal := savedgoal ;
 417 ;;
 418
 419 let call_tactic_with_goal_input tactic rendering_window () =
 420  let module L = LogicalOperations in
 421  let module G = Gdome in
 422   let proofw = (rendering_window#proofw : GMathView.math_view) in
 423   let output = (rendering_window#output : GMathView.math_view) in
 424   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 425   let savedproof = !ProofEngine.proof in
 426   let savedgoal  = !ProofEngine.goal in
 427    match proofw#get_selection with
 428      Some node ->
 429       let xpath =
 430        ((node : Gdome.element)#getAttributeNS
 431          ~namespaceURI:helmns
 432          ~localName:(G.domString "xref"))#to_string
 433       in
 434        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 435        else
 436         begin
 437          try
 438           match !current_goal_infos with
 439              Some (ids_to_terms, ids_to_father_ids,_) ->
 440               let id = xpath in
 441                tactic (Hashtbl.find ids_to_terms id) ;
 442                refresh_sequent rendering_window#proofw ;
 443                refresh_proof rendering_window#output
 444            | None -> assert false (* "ERROR: No current term!!!" *)
 445          with
 446             RefreshSequentException e ->
 447              output_html outputhtml
 448               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 449                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 450              ProofEngine.proof := savedproof ;
 451              ProofEngine.goal := savedgoal ;
 452              refresh_sequent proofw
 453           | RefreshProofException e ->
 454              output_html outputhtml
 455               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 456                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 457              ProofEngine.proof := savedproof ;
 458              ProofEngine.goal := savedgoal ;
 459              refresh_sequent proofw ;
 460              refresh_proof output
 461           | e ->
 462              output_html outputhtml
 463               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 464              ProofEngine.proof := savedproof ;
 465              ProofEngine.goal := savedgoal ;
 466         end
 467    | None ->
 468       output_html outputhtml
 469        ("<h1 color=\"red\">No term selected</h1>")
 470 ;;
 471
 472 let call_tactic_with_input_and_goal_input tactic rendering_window () =
 473  let module L = LogicalOperations in
 474  let module G = Gdome in
 475   let proofw = (rendering_window#proofw : GMathView.math_view) in
 476   let output = (rendering_window#output : GMathView.math_view) in
 477   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 478   let inputt = (rendering_window#inputt : GEdit.text) in
 479   let savedproof = !ProofEngine.proof in
 480   let savedgoal  = !ProofEngine.goal in
 481    match proofw#get_selection with
 482      Some node ->
 483       let xpath =
 484        ((node : Gdome.element)#getAttributeNS
 485          ~namespaceURI:helmns
 486          ~localName:(G.domString "xref"))#to_string
 487       in
 488        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 489        else
 490         begin
 491          try
 492           match !current_goal_infos with
 493              Some (ids_to_terms, ids_to_father_ids,_) ->
 494               let id = xpath in
 495                (* Let's parse the input *)
 496                let inputlen = inputt#length in
 497                let input = inputt#get_chars 0 inputlen ^ "\n" in
 498                 let lexbuf = Lexing.from_string input in
 499                 let curi =
 500                  match !ProofEngine.proof with
 501                     None -> assert false
 502                   | Some (curi,_,_,_) -> curi
 503                 in
 504                 let uri,metasenv,bo,ty =
 505                  match !ProofEngine.proof with
 506                     None -> assert false
 507                   | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty
 508                 in
 509                 let context =
 510                  List.map
 511                   (function
 512                       Some (n,_) -> Some n
 513                     | None -> None)
 514                   (match !ProofEngine.goal with
 515                       None -> assert false
 516                     | Some metano ->
 517                        let (_,canonical_context,_) =
 518                         List.find (function (m,_,_) -> m=metano) metasenv
 519                        in
 520                         canonical_context
 521                   )
 522                 in
 523                  begin
 524                   try
 525                    while true do
 526                     match
 527                      CicTextualParserContext.main curi context metasenv
 528                       CicTextualLexer.token lexbuf
 529                     with
 530                        None -> ()
 531                      | Some (metasenv',expr) ->
 532                         ProofEngine.proof := Some (uri,metasenv',bo,ty) ;
 533                         tactic ~goal_input:(Hashtbl.find ids_to_terms id)
 534                          ~input:expr ;
 535                         refresh_sequent proofw ;
 536                         refresh_proof output
 537                    done
 538                   with
 539                      CicTextualParser0.Eof ->
 540                       inputt#delete_text 0 inputlen
 541                  end
 542            | None -> assert false (* "ERROR: No current term!!!" *)
 543          with
 544             RefreshSequentException e ->
 545              output_html outputhtml
 546               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 547                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 548              ProofEngine.proof := savedproof ;
 549              ProofEngine.goal := savedgoal ;
 550              refresh_sequent proofw
 551           | RefreshProofException e ->
 552              output_html outputhtml
 553               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 554                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 555              ProofEngine.proof := savedproof ;
 556              ProofEngine.goal := savedgoal ;
 557              refresh_sequent proofw ;
 558              refresh_proof output
 559           | e ->
 560              output_html outputhtml
 561               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 562              ProofEngine.proof := savedproof ;
 563              ProofEngine.goal := savedgoal ;
 564         end
 565    | None ->
 566       output_html outputhtml
 567        ("<h1 color=\"red\">No term selected</h1>")
 568 ;;
 569
 570 let call_tactic_with_goal_input_in_scratch tactic scratch_window () =
 571  let module L = LogicalOperations in
 572  let module G = Gdome in
 573   let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in
 574   let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in
 575   let savedproof = !ProofEngine.proof in
 576   let savedgoal  = !ProofEngine.goal in
 577    match mmlwidget#get_selection with
 578      Some node ->
 579       let xpath =
 580        ((node : Gdome.element)#getAttributeNS
 581          ~namespaceURI:helmns
 582          ~localName:(G.domString "xref"))#to_string
 583       in
 584        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 585        else
 586         begin
 587          try
 588           match !current_scratch_infos with
 589              (* term is the whole goal in the scratch_area *)
 590              Some (term,ids_to_terms, ids_to_father_ids,_) ->
 591               let id = xpath in
 592                let expr = tactic term (Hashtbl.find ids_to_terms id) in
 593                 let mml = mml_of_cic_term 111 expr in
 594                  scratch_window#show () ;
 595                  scratch_window#mmlwidget#load_tree ~dom:mml
 596            | None -> assert false (* "ERROR: No current term!!!" *)
 597          with
 598           e ->
 599            output_html outputhtml
 600             ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 601         end
 602    | None ->
 603       output_html outputhtml
 604        ("<h1 color=\"red\">No term selected</h1>")
 605 ;;
 606
 607 let call_tactic_with_hypothesis_input tactic rendering_window () =
 608  let module L = LogicalOperations in
 609  let module G = Gdome in
 610   let proofw = (rendering_window#proofw : GMathView.math_view) in
 611   let output = (rendering_window#output : GMathView.math_view) in
 612   let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 613   let savedproof = !ProofEngine.proof in
 614   let savedgoal  = !ProofEngine.goal in
 615    match proofw#get_selection with
 616      Some node ->
 617       let xpath =
 618        ((node : Gdome.element)#getAttributeNS
 619          ~namespaceURI:helmns
 620          ~localName:(G.domString "xref"))#to_string
 621       in
 622        if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 623        else
 624         begin
 625          try
 626           match !current_goal_infos with
 627              Some (_,_,ids_to_hypotheses) ->
 628               let id = xpath in
 629                tactic (Hashtbl.find ids_to_hypotheses id) ;
 630                refresh_sequent rendering_window#proofw ;
 631                refresh_proof rendering_window#output
 632            | None -> assert false (* "ERROR: No current term!!!" *)
 633          with
 634             RefreshSequentException e ->
 635              output_html outputhtml
 636               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 637                "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
 638              ProofEngine.proof := savedproof ;
 639              ProofEngine.goal := savedgoal ;
 640              refresh_sequent proofw
 641           | RefreshProofException e ->
 642              output_html outputhtml
 643               ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 644                "proof: " ^ Printexc.to_string e ^ "</h1>") ;
 645              ProofEngine.proof := savedproof ;
 646              ProofEngine.goal := savedgoal ;
 647              refresh_sequent proofw ;
 648              refresh_proof output
 649           | e ->
 650              output_html outputhtml
 651               ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 652              ProofEngine.proof := savedproof ;
 653              ProofEngine.goal := savedgoal ;
 654         end
 655    | None ->
 656       output_html outputhtml
 657        ("<h1 color=\"red\">No term selected</h1>")
 658 ;;
 659
 660
 661 let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
 662 let exact rendering_window =
 663  call_tactic_with_input ProofEngine.exact rendering_window
 664 ;;
 665 let apply rendering_window =
 666  call_tactic_with_input ProofEngine.apply rendering_window
 667 ;;
 668 let elimintrossimpl rendering_window =
 669  call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window
 670 ;;
 671 let elimtype rendering_window =
 672  call_tactic_with_input ProofEngine.elim_type rendering_window
 673 ;;
 674 let whd rendering_window =
 675  call_tactic_with_goal_input ProofEngine.whd rendering_window
 676 ;;
 677 let reduce rendering_window =
 678  call_tactic_with_goal_input ProofEngine.reduce rendering_window
 679 ;;
 680 let simpl rendering_window =
 681  call_tactic_with_goal_input ProofEngine.simpl rendering_window
 682 ;;
 683 let fold rendering_window =
 684  call_tactic_with_input ProofEngine.fold rendering_window
 685 ;;
 686 let cut rendering_window =
 687  call_tactic_with_input ProofEngine.cut rendering_window
 688 ;;
 689 let change rendering_window =
 690  call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
 691 ;;
 692 let letin rendering_window =
 693  call_tactic_with_input ProofEngine.letin rendering_window
 694 ;;
 695 let ring rendering_window = call_tactic ProofEngine.ring rendering_window;;
 696 let clearbody rendering_window =
 697  call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window
 698 ;;
 699 let clear rendering_window =
 700  call_tactic_with_hypothesis_input ProofEngine.clear rendering_window
 701 ;;
 702 let fourier rendering_window =
 703  call_tactic ProofEngine.fourier rendering_window
 704 ;;
 705 let rewritesimpl rendering_window =
 706  call_tactic_with_input ProofEngine.rewrite_simpl rendering_window
 707 ;;
 708
 709
 710
 711 let whd_in_scratch scratch_window =
 712  call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch
 713   scratch_window
 714 ;;
 715 let reduce_in_scratch scratch_window =
 716  call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch
 717   scratch_window
 718 ;;
 719 let simpl_in_scratch scratch_window =
 720  call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch
 721   scratch_window
 722 ;;
 723
 724
 725
 726 (**********************)
 727 (*   END OF TACTICS   *)
 728 (**********************)
 729
 730 exception OpenConjecturesStillThere;;
 731 exception WrongProof;;
 732
 733 let qed rendering_window () =
 734  match !ProofEngine.proof with
 735     None -> assert false
 736   | Some (uri,[],bo,ty) ->
 737      if
 738       CicReduction.are_convertible []
 739        (CicTypeChecker.type_of_aux' [] [] bo) ty
 740      then
 741       begin
 742        (*CSC: Wrong: [] is just plainly wrong *)
 743        let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in
 744         let
 745          (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
 746           ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
 747         =
 748          Cic2acic.acic_object_of_cic_object proof
 749         in
 750          let mml =
 751           mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types
 752          in
 753           (rendering_window#output : GMathView.math_view)#load_tree mml ;
 754           current_cic_infos :=
 755            Some
 756             (ids_to_terms,ids_to_father_ids,ids_to_conjectures,
 757              ids_to_hypotheses)
 758       end
 759      else
 760       raise WrongProof
 761   | _ -> raise OpenConjecturesStillThere
 762 ;;
 763
 764 (*????
 765 let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";;
 766 *)
 767 let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";;
 768
 769 let save rendering_window () =
 770  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 771   match !ProofEngine.proof with
 772      None -> assert false
 773    | Some (uri, metasenv, bo, ty) ->
 774       let currentproof =
 775        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty)
 776       in
 777        let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
 778         Cic2acic.acic_object_of_cic_object currentproof
 779        in
 780         let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in
 781          let xml' =
 782           [< Xml.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
 783              Xml.xml_cdata
 784               ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
 785              xml
 786           >]
 787          in
 788           Xml.pp ~quiet:true xml' (Some prooffile) ;
 789           output_html outputhtml
 790            ("<h1 color=\"Green\">Current proof saved to " ^
 791             prooffile ^ "</h1>")
 792 ;;
 793
 794 (* Used to typecheck the loaded proofs *)
 795 let typecheck_loaded_proof metasenv bo ty =
 796  let module T = CicTypeChecker in
 797   (*CSC: bisogna controllare anche il metasenv!!! *)
 798   ignore (T.type_of_aux' metasenv [] ty) ;
 799   ignore (T.type_of_aux' metasenv [] bo)
 800 ;;
 801
 802 let load rendering_window () =
 803  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 804  let output = (rendering_window#output : GMathView.math_view) in
 805  let proofw = (rendering_window#proofw : GMathView.math_view) in
 806   try
 807    let uri = UriManager.uri_of_string "cic:/dummy.con" in
 808     match CicParser.obj_of_xml prooffile uri with
 809        Cic.CurrentProof (_,metasenv,bo,ty) ->
 810         typecheck_loaded_proof metasenv bo ty ;
 811         ProofEngine.proof :=
 812          Some (uri, metasenv, bo, ty) ;
 813         ProofEngine.goal :=
 814          (match metasenv with
 815              [] -> None
 816            | (metano,_,_)::_ -> Some metano
 817          ) ;
 818         refresh_proof output ;
 819         refresh_sequent proofw ;
 820          output_html outputhtml
 821           ("<h1 color=\"Green\">Current proof loaded from " ^
 822             prooffile ^ "</h1>")
 823      | _ -> assert false
 824   with
 825      RefreshSequentException e ->
 826       output_html outputhtml
 827        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 828         "sequent: " ^ Printexc.to_string e ^ "</h1>")
 829    | RefreshProofException e ->
 830       output_html outputhtml
 831        ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 832         "proof: " ^ Printexc.to_string e ^ "</h1>")
 833    | e ->
 834       output_html outputhtml
 835        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 836 ;;
 837
 838 let proveit rendering_window () =
 839  let module L = LogicalOperations in
 840  let module G = Gdome in
 841  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 842   match rendering_window#output#get_selection with
 843     Some node ->
 844      let xpath =
 845       ((node : Gdome.element)#getAttributeNS
 846       (*CSC: OCAML DIVERGE
 847       ((element : G.element)#getAttributeNS
 848       *)
 849         ~namespaceURI:helmns
 850         ~localName:(G.domString "xref"))#to_string
 851      in
 852       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 853       else
 854        begin
 855         try
 856          match !current_cic_infos with
 857             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 858              let id = xpath in
 859               L.to_sequent id ids_to_terms ids_to_father_ids ;
 860               refresh_proof rendering_window#output ;
 861               refresh_sequent rendering_window#proofw
 862           | None -> assert false (* "ERROR: No current term!!!" *)
 863         with
 864            RefreshSequentException e ->
 865             output_html outputhtml
 866              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 867               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 868          | RefreshProofException e ->
 869             output_html outputhtml
 870              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 871               "proof: " ^ Printexc.to_string e ^ "</h1>")
 872          | e ->
 873             output_html outputhtml
 874              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 875        end
 876   | None -> assert false (* "ERROR: No selection!!!" *)
 877 ;;
 878
 879 let focus rendering_window () =
 880  let module L = LogicalOperations in
 881  let module G = Gdome in
 882  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 883   match rendering_window#output#get_selection with
 884     Some node ->
 885      let xpath =
 886       ((node : Gdome.element)#getAttributeNS
 887       (*CSC: OCAML DIVERGE
 888       ((element : G.element)#getAttributeNS
 889       *)
 890         ~namespaceURI:helmns
 891         ~localName:(G.domString "xref"))#to_string
 892      in
 893       if xpath = "" then assert false (* "ERROR: No xref found!!!" *)
 894       else
 895        begin
 896         try
 897          match !current_cic_infos with
 898             Some (ids_to_terms, ids_to_father_ids, _, _) ->
 899              let id = xpath in
 900               L.focus id ids_to_terms ids_to_father_ids ;
 901               refresh_sequent rendering_window#proofw
 902           | None -> assert false (* "ERROR: No current term!!!" *)
 903         with
 904            RefreshSequentException e ->
 905             output_html outputhtml
 906              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 907               "sequent: " ^ Printexc.to_string e ^ "</h1>")
 908          | RefreshProofException e ->
 909             output_html outputhtml
 910              ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 911               "proof: " ^ Printexc.to_string e ^ "</h1>")
 912          | e ->
 913             output_html outputhtml
 914              ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 915        end
 916   | None -> assert false (* "ERROR: No selection!!!" *)
 917 ;;
 918
 919 exception NoPrevGoal;;
 920 exception NoNextGoal;;
 921
 922 let prevgoal metasenv metano =
 923  let rec aux =
 924   function
 925      [] -> assert false
 926    | [(m,_,_)] -> raise NoPrevGoal
 927    | (n,_,_)::(m,_,_)::_ when m=metano -> n
 928    | _::tl -> aux tl
 929  in
 930   aux metasenv
 931 ;;
 932
 933 let nextgoal metasenv metano =
 934  let rec aux =
 935   function
 936      [] -> assert false
 937    | [(m,_,_)] when m = metano -> raise NoNextGoal
 938    | (m,_,_)::(n,_,_)::_ when m=metano -> n
 939    | _::tl -> aux tl
 940  in
 941   aux metasenv
 942 ;;
 943
 944 let prev_or_next_goal select_goal rendering_window () =
 945  let module L = LogicalOperations in
 946  let module G = Gdome in
 947  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 948   let metasenv =
 949    match !ProofEngine.proof with
 950       None -> assert false
 951     | Some (_,metasenv,_,_) -> metasenv
 952   in
 953   let metano =
 954    match !ProofEngine.goal with
 955       None -> assert false
 956     | Some m -> m
 957   in
 958    try
 959     ProofEngine.goal := Some (select_goal metasenv metano) ;
 960     refresh_sequent rendering_window#proofw
 961    with
 962       RefreshSequentException e ->
 963        output_html outputhtml
 964         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
 965          "sequent: " ^ Printexc.to_string e ^ "</h1>")
 966     | e ->
 967        output_html outputhtml
 968         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
 969 ;;
 970
 971 exception NotADefinition;;
 972
 973 let open_ rendering_window () =
 974  let inputt = (rendering_window#inputt : GEdit.text) in
 975  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
 976  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
 977  let output = (rendering_window#output : GMathView.math_view) in
 978  let proofw = (rendering_window#proofw : GMathView.math_view) in
 979   let inputlen = inputt#length in
 980   let input = inputt#get_chars 0 inputlen ^ "\n" in
 981    try
 982     let uri = UriManager.uri_of_string ("cic:" ^ input) in
 983      CicTypeChecker.typecheck uri ;
 984      let metasenv,bo,ty =
 985       match CicEnvironment.get_cooked_obj uri 0 with
 986          Cic.Definition (_,bo,ty,_) -> [],bo,ty
 987        | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty
 988        | Cic.Axiom _
 989        | Cic.Variable _
 990        | Cic.InductiveDefinition _ -> raise NotADefinition
 991      in
 992       ProofEngine.proof :=
 993        Some (uri, metasenv, bo, ty) ;
 994       ProofEngine.goal := None ;
 995       refresh_sequent proofw ;
 996       refresh_proof output ;
 997       inputt#delete_text 0 inputlen ;
 998       ignore(oldinputt#insert_text input oldinputt#length)
 999    with
1000       RefreshSequentException e ->
1001        output_html outputhtml
1002         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1003          "sequent: " ^ Printexc.to_string e ^ "</h1>")
1004     | RefreshProofException e ->
1005        output_html outputhtml
1006         ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1007          "proof: " ^ Printexc.to_string e ^ "</h1>")
1008     | e ->
1009        output_html outputhtml
1010         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1011 ;;
1012
1013 let state rendering_window () =
1014  let inputt = (rendering_window#inputt : GEdit.text) in
1015  let oldinputt = (rendering_window#oldinputt : GEdit.text) in
1016  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1017  let output = (rendering_window#output : GMathView.math_view) in
1018  let proofw = (rendering_window#proofw : GMathView.math_view) in
1019   let inputlen = inputt#length in
1020   let input = inputt#get_chars 0 inputlen ^ "\n" in
1021    (* Do something interesting *)
1022    let lexbuf = Lexing.from_string input in
1023     try
1024      while true do
1025       (* Execute the actions *)
1026       match CicTextualParser.main CicTextualLexer.token lexbuf with
1027          None -> ()
1028        | Some expr ->
1029           let _  = CicTypeChecker.type_of_aux' [] [] expr in
1030            ProofEngine.proof :=
1031             Some (UriManager.uri_of_string "cic:/dummy.con",
1032                    [1,[],expr], Cic.Meta (1,[]), expr) ;
1033            ProofEngine.goal := Some 1 ;
1034            refresh_sequent proofw ;
1035            refresh_proof output ;
1036      done
1037     with
1038        CicTextualParser0.Eof ->
1039         inputt#delete_text 0 inputlen ;
1040         ignore(oldinputt#insert_text input oldinputt#length)
1041      | RefreshSequentException e ->
1042         output_html outputhtml
1043          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1044           "sequent: " ^ Printexc.to_string e ^ "</h1>")
1045      | RefreshProofException e ->
1046         output_html outputhtml
1047          ("<h1 color=\"red\">Exception raised during the refresh of the " ^
1048           "proof: " ^ Printexc.to_string e ^ "</h1>")
1049      | e ->
1050         output_html outputhtml
1051          ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1052 ;;
1053
1054 let check rendering_window scratch_window () =
1055  let inputt = (rendering_window#inputt : GEdit.text) in
1056  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1057  let output = (rendering_window#output : GMathView.math_view) in
1058  let proofw = (rendering_window#proofw : GMathView.math_view) in
1059   let inputlen = inputt#length in
1060   let input = inputt#get_chars 0 inputlen ^ "\n" in
1061   let curi,metasenv =
1062    match !ProofEngine.proof with
1063       None -> UriManager.uri_of_string "cic:/dummy.con", []
1064     | Some (curi,metasenv,_,_) -> curi,metasenv
1065   in
1066   let context,names_context =
1067    let context =
1068     match !ProofEngine.goal with
1069        None -> []
1070      | Some metano ->
1071         let (_,canonical_context,_) =
1072          List.find (function (m,_,_) -> m=metano) metasenv
1073         in
1074          canonical_context
1075    in
1076     context,
1077     List.map
1078      (function
1079          Some (n,_) -> Some n
1080        | None -> None
1081      ) context
1082   in
1083    (* Do something interesting *)
1084    let lexbuf = Lexing.from_string input in
1085     try
1086      while true do
1087       (* Execute the actions *)
1088       match
1089        CicTextualParserContext.main curi names_context metasenv
1090         CicTextualLexer.token lexbuf
1091       with
1092          None -> ()
1093        | Some (metasenv',expr) ->
1094           try
1095            let ty  = CicTypeChecker.type_of_aux' metasenv' context expr in
1096             let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in
1097              scratch_window#show () ;
1098              scratch_window#mmlwidget#load_tree ~dom:mml
1099           with
1100            e ->
1101             print_endline ("? " ^ CicPp.ppterm expr) ;
1102             raise e
1103      done
1104     with
1105        CicTextualParser0.Eof -> ()
1106      | e ->
1107        output_html outputhtml
1108         ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
1109 ;;
1110
1111 exception NoObjectsLocated;;
1112
1113 let user_uri_choice uris =
1114  let uri =
1115   match uris with
1116      [] -> raise NoObjectsLocated
1117    | [uri] -> uri
1118    | uris ->
1119       let choice =
1120        GToolbox.question_box ~title:"Ambiguous result."
1121         ~buttons:uris ~default:1
1122         "Ambiguous result. Please, choose one."
1123       in
1124        List.nth uris (choice-1)
1125  in
1126   String.sub uri 4 (String.length uri - 4)
1127 ;;
1128
1129 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
1130 let get_last_query =
1131  let query = ref "" in
1132   MQueryGenerator.set_confirm_query
1133    (function q -> query := MQueryUtil.text_of_query q ; true) ;
1134   function result -> !query ^ " <h1>Result:</h1> " ^ MQueryUtil.text_of_result result "<br>"
1135 ;;
1136
1137 let locate rendering_window () =
1138  let inputt = (rendering_window#inputt : GEdit.text) in
1139  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1140   let inputlen = inputt#length in
1141   let input = inputt#get_chars 0 inputlen in
1142    try
1143     match Str.split (Str.regexp "[ \t]+") input with
1144        [] -> ()
1145      | head :: tail ->
1146         inputt#delete_text 0 inputlen ;
1147         let result = MQueryGenerator.locate head in
1148         let uris =
1149          List.map
1150           (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1151           result in
1152         let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1153          output_html outputhtml html ;
1154          let uri' = user_uri_choice uris in
1155           ignore ((inputt#insert_text uri') ~pos:0)
1156    with
1157     e ->
1158      output_html outputhtml
1159       ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1160 ;;
1161
1162 let backward rendering_window () =
1163  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
1164  let inputt = (rendering_window#inputt : GEdit.text) in
1165   let inputlen = inputt#length in
1166   let input = inputt#get_chars 0 inputlen in
1167   let level = int_of_string input in
1168   let metasenv =
1169    match !ProofEngine.proof with
1170       None -> assert false
1171     | Some (_,metasenv,_,_) -> metasenv
1172   in
1173    try
1174     match !ProofEngine.goal with
1175        None -> ()
1176      | Some metano ->
1177         let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
1178          let result = MQueryGenerator.backward metasenv ey ty level in
1179          let uris =
1180           List.map
1181            (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1182            result in
1183          let html =
1184           " <h1>Backward Query: </h1>" ^
1185           " <h2>Levels: </h2> " ^
1186            MQueryGenerator.string_of_levels (MQueryGenerator.levels_of_term metasenv ey ty) "<br>" ^
1187            " <pre>" ^ get_last_query result ^ "</pre>" in
1188           output_html outputhtml html ;
1189           let uri' = user_uri_choice uris in
1190            inputt#delete_text 0 inputlen ;
1191            ignore ((inputt#insert_text uri') ~pos:0)
1192     with
1193      e ->
1194       output_html outputhtml
1195        ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
1196 ;;
1197
1198 let choose_selection
1199      (mmlwidget : GMathView.math_view) (element : Gdome.element option)
1200 =
1201  let module G = Gdome in
1202   let rec aux element =
1203    if element#hasAttributeNS
1204        ~namespaceURI:helmns
1205        ~localName:(G.domString "xref")
1206    then
1207      mmlwidget#set_selection (Some element)
1208    else
1209       match element#get_parentNode with
1210          None -> assert false
1211        (*CSC: OCAML DIVERGES!
1212        | Some p -> aux (new G.element_of_node p)
1213        *)
1214        | Some p -> aux (new Gdome.element_of_node p)
1215   in
1216    match element with
1217      Some x -> aux x
1218    | None   -> mmlwidget#set_selection None
1219 ;;
1220
1221 (* STUFF TO BUILD THE GTK INTERFACE *)
1222
1223 (* Stuff for the widget settings *)
1224
1225 let export_to_postscript (output : GMathView.math_view) () =
1226  output#export_to_postscript ~filename:"output.ps" ();
1227 ;;
1228
1229 let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing
1230  button_set_kerning button_set_transparency button_export_to_postscript
1231  button_t1 ()
1232 =
1233  let is_set = button_t1#active in
1234   output#set_font_manager_type
1235    (if is_set then `font_manager_t1 else `font_manager_gtk) ;
1236   if is_set then
1237    begin
1238     button_set_anti_aliasing#misc#set_sensitive true ;
1239     button_set_kerning#misc#set_sensitive true ;
1240     button_set_transparency#misc#set_sensitive true ;
1241     button_export_to_postscript#misc#set_sensitive true ;
1242    end
1243   else
1244    begin
1245     button_set_anti_aliasing#misc#set_sensitive false ;
1246     button_set_kerning#misc#set_sensitive false ;
1247     button_set_transparency#misc#set_sensitive false ;
1248     button_export_to_postscript#misc#set_sensitive false ;
1249    end
1250 ;;
1251
1252 let set_anti_aliasing output button_set_anti_aliasing () =
1253  output#set_anti_aliasing button_set_anti_aliasing#active
1254 ;;
1255
1256 let set_kerning output button_set_kerning () =
1257  output#set_kerning button_set_kerning#active
1258 ;;
1259
1260 let set_transparency output button_set_transparency () =
1261  output#set_transparency button_set_transparency#active
1262 ;;
1263
1264 let changefont output font_size_spinb () =
1265  output#set_font_size font_size_spinb#value_as_int
1266 ;;
1267
1268 let set_log_verbosity output log_verbosity_spinb () =
1269  output#set_log_verbosity log_verbosity_spinb#value_as_int
1270 ;;
1271
1272 class settings_window (output : GMathView.math_view) sw
1273  button_export_to_postscript selection_changed_callback
1274 =
1275  let settings_window = GWindow.window ~title:"GtkMathView settings" () in
1276  let vbox =
1277   GPack.vbox ~packing:settings_window#add () in
1278  let table =
1279   GPack.table
1280    ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1281    ~border_width:5 ~packing:vbox#add () in
1282  let button_t1 =
1283   GButton.toggle_button ~label:"activate t1 fonts"
1284    ~packing:(table#attach ~left:0 ~top:0) () in
1285  let button_set_anti_aliasing =
1286   GButton.toggle_button ~label:"set_anti_aliasing"
1287    ~packing:(table#attach ~left:0 ~top:1) () in
1288  let button_set_kerning =
1289   GButton.toggle_button ~label:"set_kerning"
1290    ~packing:(table#attach ~left:1 ~top:1) () in
1291  let button_set_transparency =
1292   GButton.toggle_button ~label:"set_transparency"
1293    ~packing:(table#attach ~left:2 ~top:1) () in
1294  let table =
1295   GPack.table
1296    ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5
1297    ~border_width:5 ~packing:vbox#add () in
1298  let font_size_label =
1299   GMisc.label ~text:"font size:"
1300    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
1301  let font_size_spinb =
1302   let sadj =
1303    GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
1304   in
1305    GEdit.spin_button
1306     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
1307  let log_verbosity_label =
1308   GMisc.label ~text:"log verbosity:"
1309    ~packing:(table#attach ~left:0 ~top:1) () in
1310  let log_verbosity_spinb =
1311   let sadj =
1312    GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 ()
1313   in
1314    GEdit.spin_button
1315     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in
1316  let hbox =
1317   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1318  let closeb =
1319   GButton.button ~label:"Close"
1320    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1321 object(self)
1322  method show = settings_window#show
1323  initializer
1324   button_set_anti_aliasing#misc#set_sensitive false ;
1325   button_set_kerning#misc#set_sensitive false ;
1326   button_set_transparency#misc#set_sensitive false ;
1327   (* Signals connection *)
1328   ignore(button_t1#connect#clicked
1329    (activate_t1 output button_set_anti_aliasing button_set_kerning
1330     button_set_transparency button_export_to_postscript button_t1)) ;
1331   ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ;
1332   ignore(button_set_anti_aliasing#connect#toggled
1333    (set_anti_aliasing output button_set_anti_aliasing));
1334   ignore(button_set_kerning#connect#toggled
1335    (set_kerning output button_set_kerning)) ;
1336   ignore(button_set_transparency#connect#toggled
1337    (set_transparency output button_set_transparency)) ;
1338   ignore(log_verbosity_spinb#connect#changed
1339    (set_log_verbosity output log_verbosity_spinb)) ;
1340   ignore(closeb#connect#clicked settings_window#misc#hide)
1341 end;;
1342
1343 (* Scratch window *)
1344
1345 class scratch_window outputhtml =
1346  let window =
1347   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1348  let vbox =
1349   GPack.vbox ~packing:window#add () in
1350  let hbox =
1351   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1352  let whdb =
1353   GButton.button ~label:"Whd"
1354    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1355  let reduceb =
1356   GButton.button ~label:"Reduce"
1357    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1358  let simplb =
1359   GButton.button ~label:"Simpl"
1360    ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
1361  let scrolled_window =
1362   GBin.scrolled_window ~border_width:10
1363    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1364  let mmlwidget =
1365   GMathView.math_view
1366    ~packing:(scrolled_window#add) ~width:400 ~height:280 () in
1367 object(self)
1368  method outputhtml = outputhtml
1369  method mmlwidget = mmlwidget
1370  method show () = window#misc#hide () ; window#show ()
1371  initializer
1372   ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ;
1373   ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ;
1374   ignore(whdb#connect#clicked (whd_in_scratch self)) ;
1375   ignore(reduceb#connect#clicked (reduce_in_scratch self)) ;
1376   ignore(simplb#connect#clicked (simpl_in_scratch self))
1377 end;;
1378
1379 (* Main window *)
1380
1381 class rendering_window output proofw (label : GMisc.label) =
1382  let window =
1383   GWindow.window ~title:"MathML viewer" ~border_width:2 () in
1384  let hbox0 =
1385   GPack.hbox ~packing:window#add () in
1386  let vbox =
1387   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1388  let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in
1389  let scrolled_window0 =
1390   GBin.scrolled_window ~border_width:10
1391    ~packing:(vbox#pack ~expand:true ~padding:5) () in
1392  let _ = scrolled_window0#add output#coerce in
1393  let hbox1 =
1394   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1395  let settingsb =
1396   GButton.button ~label:"Settings"
1397    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1398  let button_export_to_postscript =
1399   GButton.button ~label:"export_to_postscript"
1400   ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1401  let qedb =
1402   GButton.button ~label:"Qed"
1403    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1404  let saveb =
1405   GButton.button ~label:"Save"
1406    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1407  let loadb =
1408   GButton.button ~label:"Load"
1409    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1410  let closeb =
1411   GButton.button ~label:"Close"
1412    ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in
1413  let hbox2 =
1414   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1415  let proveitb =
1416   GButton.button ~label:"Prove It"
1417    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1418  let focusb =
1419   GButton.button ~label:"Focus"
1420    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1421  let prevgoalb =
1422   GButton.button ~label:"<"
1423    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1424  let nextgoalb =
1425   GButton.button ~label:">"
1426    ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
1427  let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180
1428    ~packing:(vbox#pack ~padding:5) () in
1429  let hbox4 =
1430   GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
1431  let stateb =
1432   GButton.button ~label:"State"
1433    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1434  let openb =
1435   GButton.button ~label:"Open"
1436    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1437  let checkb =
1438   GButton.button ~label:"Check"
1439    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1440  let locateb =
1441   GButton.button ~label:"Locate"
1442    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1443  let backwardb =
1444   GButton.button ~label:"Backward"
1445    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1446  let inputt = GEdit.text ~editable:true ~width:400 ~height: 100
1447    ~packing:(vbox#pack ~padding:5) () in
1448  let vbox1 =
1449   GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in
1450  let scrolled_window1 =
1451   GBin.scrolled_window ~border_width:10
1452    ~packing:(vbox1#pack ~expand:true ~padding:5) () in
1453  let _ = scrolled_window1#add proofw#coerce in
1454  let hbox3 =
1455   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1456  let exactb =
1457   GButton.button ~label:"Exact"
1458    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1459  let introsb =
1460   GButton.button ~label:"Intros"
1461    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1462  let applyb =
1463   GButton.button ~label:"Apply"
1464    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1465  let elimintrossimplb =
1466   GButton.button ~label:"ElimIntrosSimpl"
1467    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1468  let elimtypeb =
1469   GButton.button ~label:"ElimType"
1470    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1471  let whdb =
1472   GButton.button ~label:"Whd"
1473    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1474  let reduceb =
1475   GButton.button ~label:"Reduce"
1476    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1477  let simplb =
1478   GButton.button ~label:"Simpl"
1479    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1480  let foldb =
1481   GButton.button ~label:"Fold"
1482    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1483  let cutb =
1484   GButton.button ~label:"Cut"
1485    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1486  let changeb =
1487   GButton.button ~label:"Change"
1488    ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
1489  let hbox4 =
1490   GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in
1491  let letinb =
1492   GButton.button ~label:"Let ... In"
1493    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1494  let ringb =
1495   GButton.button ~label:"Ring"
1496    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1497  let clearbodyb =
1498   GButton.button ~label:"ClearBody"
1499    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1500  let clearb =
1501   GButton.button ~label:"Clear"
1502    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1503  let fourierb =
1504   GButton.button ~label:"Fourier"
1505    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1506  let rewritesimplb =
1507   GButton.button ~label:"RewriteSimpl ->"
1508    ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in
1509  let outputhtml =
1510   GHtml.xmhtml
1511    ~source:"<html><body bgColor=\"white\"></body></html>"
1512    ~width:400 ~height: 200
1513    ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5)
1514    ~show:true () in
1515  let scratch_window = new scratch_window outputhtml in
1516 object(self)
1517  method outputhtml = outputhtml
1518  method oldinputt = oldinputt
1519  method inputt = inputt
1520  method output = (output : GMathView.math_view)
1521  method proofw = (proofw : GMathView.math_view)
1522  method show = window#show
1523  initializer
1524   button_export_to_postscript#misc#set_sensitive false ;
1525
1526   (* signal handlers here *)
1527   ignore(output#connect#selection_changed
1528    (function elem -> proofw#unload ; choose_selection output elem)) ;
1529   ignore(proofw#connect#selection_changed (choose_selection proofw)) ;
1530   ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ;
1531   let settings_window = new settings_window output scrolled_window0
1532    button_export_to_postscript (choose_selection output) in
1533   ignore(settingsb#connect#clicked settings_window#show) ;
1534   ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ;
1535   ignore(qedb#connect#clicked (qed self)) ;
1536   ignore(saveb#connect#clicked (save self)) ;
1537   ignore(loadb#connect#clicked (load self)) ;
1538   ignore(proveitb#connect#clicked (proveit self)) ;
1539   ignore(focusb#connect#clicked (focus self)) ;
1540   ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ;
1541   ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ;
1542   ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
1543   ignore(stateb#connect#clicked (state self)) ;
1544   ignore(openb#connect#clicked (open_ self)) ;
1545   ignore(checkb#connect#clicked (check self scratch_window)) ;
1546   ignore(locateb#connect#clicked (locate self)) ;
1547   ignore(backwardb#connect#clicked (backward self)) ;
1548   ignore(exactb#connect#clicked (exact self)) ;
1549   ignore(applyb#connect#clicked (apply self)) ;
1550   ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ;
1551   ignore(elimtypeb#connect#clicked (elimtype self)) ;
1552   ignore(whdb#connect#clicked (whd self)) ;
1553   ignore(reduceb#connect#clicked (reduce self)) ;
1554   ignore(simplb#connect#clicked (simpl self)) ;
1555   ignore(foldb#connect#clicked (fold self)) ;
1556   ignore(cutb#connect#clicked (cut self)) ;
1557   ignore(changeb#connect#clicked (change self)) ;
1558   ignore(letinb#connect#clicked (letin self)) ;
1559   ignore(ringb#connect#clicked (ring self)) ;
1560   ignore(clearbodyb#connect#clicked (clearbody self)) ;
1561   ignore(clearb#connect#clicked (clear self)) ;
1562   ignore(fourierb#connect#clicked (fourier self)) ;
1563   ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ;
1564   ignore(introsb#connect#clicked (intros self)) ;
1565   Logger.log_callback :=
1566    (Logger.log_to_html ~print_and_flush:(output_html outputhtml))
1567 end;;
1568
1569 (* MAIN *)
1570
1571 let rendering_window = ref None;;
1572
1573 let initialize_everything () =
1574  let module U = Unix in
1575   let output = GMathView.math_view ~width:350 ~height:280 ()
1576   and proofw = GMathView.math_view ~width:400 ~height:275 ()
1577   and label = GMisc.label ~text:"gTopLevel" () in
1578     let rendering_window' =
1579      new rendering_window output proofw label
1580     in
1581      rendering_window := Some rendering_window' ;
1582      rendering_window'#show () ;
1583      GMain.Main.main ()
1584 ;;
1585
1586 let _ =
1587  CicCooking.init () ;
1588  if !usedb then
1589   begin
1590    Mqint.init "host=mowgli.cs.unibo.it dbname=helm user=helm" ;
1591    CicTextualParser0.set_locate_object
1592     (function id ->
1593       let result = MQueryGenerator.locate id in
1594       let uris =
1595        List.map
1596         (function uri,_ -> wrong_xpointer_format_from_wrong_xpointer_format' uri)
1597         result in
1598       let html = (" <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>") in
1599        begin
1600         match !rendering_window with
1601            None -> assert false
1602          | Some rw -> output_html rw#outputhtml html ;
1603        end ;
1604        let uri =
1605         match uris with
1606            [] ->
1607             (match
1608               (GToolbox.input_string ~title:"Unknown input"
1609                ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
1610              with
1611                 None -> None
1612               | Some uri -> Some ("cic:" ^ uri)
1613             )
1614          | [uri] -> Some uri
1615          | _ ->
1616            let choice =
1617             GToolbox.question_box ~title:"Ambiguous input."
1618              ~buttons:uris ~default:1 "Ambiguous input. Please, choose one."
1619            in
1620             if choice > 0 then
1621              Some (List.nth uris (choice - 1))
1622             else
1623              (* No choice from the user *)
1624              None
1625        in
1626         match uri with
1627            Some uri' ->
1628             (* Constant *)
1629             if String.sub uri' (String.length uri' - 4) 4 = ".con" then
1630 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1631              Some (Cic.Const (UriManager.uri_of_string uri',0))
1632             else
1633              (try
1634                (* Inductive Type *)
1635                let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
1636 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1637                 Some (Cic.MutInd (uri'',0,typeno))
1638               with
1639                _ ->
1640                 (* Constructor of an Inductive Type *)
1641                 let uri'',typeno,consno =
1642                  CicTextualLexer.indconuri_of_uri uri'
1643                 in
1644 (*CSC: what cooking number? Here I always use 0, which may be bugged *)
1645                  Some (Cic.MutConstruct (uri'',0,typeno,consno))
1646              )
1647          | None -> None
1648     )
1649   end ;
1650  ignore (GtkMain.Main.init ()) ;
1651  initialize_everything () ;
1652  if !usedb then Mqint.close ();
1653 ;;