From: no author Date: Thu, 17 Oct 2002 17:55:17 +0000 (+0000) Subject: This commit was manufactured by cvs2svn to create tag 'mathql'. X-Git-Tag: mathql X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=434ea590617bba6fce52604b6e61d19f54389f52;p=helm.git This commit was manufactured by cvs2svn to create tag 'mathql'. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml deleted file mode 100644 index c980f723b..000000000 --- a/helm/gTopLevel/gTopLevel.ml +++ /dev/null @@ -1,1610 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) - -(* GLOBAL CONSTANTS *) - -let helmns = Gdome.domString "http://www.cs.unibo.it/helm";; - -let htmlheader = - "" ^ - " " -;; - -let htmlfooter = - " " ^ - "" -;; - -let prooffile = "/home/tassi/miohelm/tmp/currentproof";; -(*CSC: the getter should handle the innertypes, not the FS *) -let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; - -(* GLOBAL REFERENCES (USED BY CALLBACKS) *) - -let htmlheader_and_content = ref htmlheader;; - -let current_cic_infos = ref None;; -let current_goal_infos = ref None;; -let current_scratch_infos = ref None;; - -(* COMMAND LINE OPTIONS *) - -let usedb = ref true - -let argspec = - [ - "-nodb", Arg.Clear usedb, "disable use of MathQL DB" - ] -in -Arg.parse argspec ignore "" - - -(* MISC FUNCTIONS *) - -let domImpl = Gdome.domImplementation ();; - -let parseStyle name = - let style = - domImpl#createDocumentFromURI -(* - ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None -*) - ~uri:("styles/" ^ name) () - in - Gdome_xslt.processStylesheet style -;; - -let d_c = parseStyle "drop_coercions.xsl";; -let tc1 = parseStyle "objtheorycontent.xsl";; -let hc2 = parseStyle "content_to_html.xsl";; -let l = parseStyle "link.xsl";; - -let c1 = parseStyle "rootcontent.xsl";; -let g = parseStyle "genmmlid.xsl";; -let c2 = parseStyle "annotatedpres.xsl";; - - -let getterURL = Configuration.getter_url;; -let processorURL = Configuration.processor_url;; - -let mml_styles = [d_c ; c1 ; g ; c2 ; l];; -let mml_args = - ["processorURL", "'" ^ processorURL ^ "'" ; - "getterURL", "'" ^ getterURL ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'yes'" ; - "annotations", "'no'" ; - "explodeall", "'true()'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] -;; - -let sequent_styles = [d_c ; c1 ; g ; c2 ; l];; -let sequent_args = - ["processorURL", "'" ^ processorURL ^ "'" ; - "getterURL", "'" ^ getterURL ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'no'" ; - "annotations", "'no'" ; - "explodeall", "'true()'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] -;; - -let parse_file filename = - let inch = open_in filename in - let rec read_lines () = - try - let line = input_line inch in - line ^ read_lines () - with - End_of_file -> "" - in - read_lines () -;; - -let applyStylesheets input styles args = - List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i style args) - input styles -;; - -let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types = - let xml = - Cic2Xml.print_object uri ~ids_to_inner_sorts annobj - in - let xmlinnertypes = - Cic2Xml.print_inner_types uri ~ids_to_inner_sorts - ~ids_to_inner_types - in - let input = Xml2Gdome.document_of_xml domImpl xml in -(*CSC: We save the innertypes to disk so that we can retrieve them in the *) -(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) -(*CSC: local. *) - Xml.pp xmlinnertypes (Some innertypesfile) ; - let output = applyStylesheets input mml_styles mml_args in - output -;; - - -(* CALLBACKS *) - -exception RefreshSequentException of exn;; -exception RefreshProofException of exn;; - -let refresh_proof (output : GMathView.math_view) = - try - let uri,currentproof = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> - uri,(Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty)) - in - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object currentproof - in - let mml = - mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types - in - output#load_tree mml ; - current_cic_infos := - Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) - with - e -> - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> -prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty))) ; flush stderr ; - raise (RefreshProofException e) -;; - -let refresh_sequent (proofw : GMathView.math_view) = - try - match !ProofEngine.goal with - None -> proofw#unload - | Some metano -> - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in - let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = - SequentPp.XmlPp.print_sequent metasenv currentsequent - in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let sequent_mml = - applyStylesheets sequent_doc sequent_styles sequent_args - in - proofw#load_tree ~dom:sequent_mml ; - current_goal_infos := - Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses) - with - e -> -let metano = - match !ProofEngine.goal with - None -> assert false - | Some m -> m -in -let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv -in -let currentsequent = List.find (function (m,_,_) -> m=metano) metasenv in -prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent currentsequent) ; flush stderr ; - raise (RefreshSequentException e) -;; - -(* -ignore(domImpl#saveDocumentToFile ~doc:sequent_doc - ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ; -*) - -let mml_of_cic_term metano term = - let metasenv = - match !ProofEngine.proof with - None -> [] - | Some (_,metasenv,_,_) -> metasenv - in - let context = - match !ProofEngine.goal with - None -> [] - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - in - let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = - SequentPp.XmlPp.print_sequent metasenv (metano,context,term) - in - let sequent_doc = - Xml2Gdome.document_of_xml domImpl sequent_gdome - in - let res = - applyStylesheets sequent_doc sequent_styles sequent_args ; - in - current_scratch_infos := - Some (term,ids_to_terms,ids_to_father_ids,ids_to_hypotheses) ; - res -;; - -let output_html outputhtml msg = - htmlheader_and_content := !htmlheader_and_content ^ msg ; - outputhtml#source (!htmlheader_and_content ^ htmlfooter) ; - outputhtml#set_topline (-1) -;; - -(***********************) -(* TACTICS *) -(***********************) - -let call_tactic tactic rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - begin - try - tactic () ; - refresh_sequent proofw ; - refresh_proof output - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end -;; - -let call_tactic_with_input tactic rendering_window () = - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in -(*CSC: Gran cut&paste da sotto... *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in - let curi = - match !ProofEngine.proof with - None -> assert false - | Some (curi,_,_,_) -> curi - in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None) - (match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - ) - in - try - while true do - match - CicTextualParserContext.main - curi context metasenv CicTextualLexer.token lexbuf - with - None -> () - | Some (metasenv',expr) -> - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic expr ; - refresh_sequent proofw ; - refresh_proof output - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen - | RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; -;; - -let call_tactic_with_goal_input tactic rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match proofw#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_goal_infos with - Some (ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - tactic (Hashtbl.find ids_to_terms id) ; - refresh_sequent rendering_window#proofw ; - refresh_proof rendering_window#output - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end - | None -> - output_html outputhtml - ("

No term selected

") -;; - -let call_tactic_with_input_and_goal_input tactic rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match proofw#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_goal_infos with - Some (ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - (* Let's parse the input *) - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let lexbuf = Lexing.from_string input in - let curi = - match !ProofEngine.proof with - None -> assert false - | Some (curi,_,_,_) -> curi - in - let uri,metasenv,bo,ty = - match !ProofEngine.proof with - None -> assert false - | Some (uri,metasenv,bo,ty) -> uri,metasenv,bo,ty - in - let context = - List.map - (function - Some (n,_) -> Some n - | None -> None) - (match !ProofEngine.goal with - None -> assert false - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - ) - in - begin - try - while true do - match - CicTextualParserContext.main curi context metasenv - CicTextualLexer.token lexbuf - with - None -> () - | Some (metasenv',expr) -> - ProofEngine.proof := Some (uri,metasenv',bo,ty) ; - tactic ~goal_input:(Hashtbl.find ids_to_terms id) - ~input:expr ; - refresh_sequent proofw ; - refresh_proof output - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen - end - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end - | None -> - output_html outputhtml - ("

No term selected

") -;; - -let call_tactic_with_goal_input_in_scratch tactic scratch_window () = - let module L = LogicalOperations in - let module G = Gdome in - let mmlwidget = (scratch_window#mmlwidget : GMathView.math_view) in - let outputhtml = (scratch_window#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match mmlwidget#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_scratch_infos with - (* term is the whole goal in the scratch_area *) - Some (term,ids_to_terms, ids_to_father_ids,_) -> - let id = xpath in - let expr = tactic term (Hashtbl.find ids_to_terms id) in - let mml = mml_of_cic_term 111 expr in - scratch_window#show () ; - scratch_window#mmlwidget#load_tree ~dom:mml - | None -> assert false (* "ERROR: No current term!!!" *) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | None -> - output_html outputhtml - ("

No term selected

") -;; - -let call_tactic_with_hypothesis_input tactic rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let output = (rendering_window#output : GMathView.math_view) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let savedproof = !ProofEngine.proof in - let savedgoal = !ProofEngine.goal in - match proofw#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_goal_infos with - Some (_,_,ids_to_hypotheses) -> - let id = xpath in - tactic (Hashtbl.find ids_to_hypotheses id) ; - refresh_sequent rendering_window#proofw ; - refresh_proof rendering_window#output - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - refresh_sequent proofw ; - refresh_proof output - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; - ProofEngine.proof := savedproof ; - ProofEngine.goal := savedgoal ; - end - | None -> - output_html outputhtml - ("

No term selected

") -;; - - -let intros rendering_window = call_tactic ProofEngine.intros rendering_window;; -let exact rendering_window = - call_tactic_with_input ProofEngine.exact rendering_window -;; -let apply rendering_window = - call_tactic_with_input ProofEngine.apply rendering_window -;; -let elimintrossimpl rendering_window = - call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window -;; -let elimtype rendering_window = - call_tactic_with_input ProofEngine.elim_type rendering_window -;; -let whd rendering_window = - call_tactic_with_goal_input ProofEngine.whd rendering_window -;; -let reduce rendering_window = - call_tactic_with_goal_input ProofEngine.reduce rendering_window -;; -let simpl rendering_window = - call_tactic_with_goal_input ProofEngine.simpl rendering_window -;; -let fold rendering_window = - call_tactic_with_input ProofEngine.fold rendering_window -;; -let cut rendering_window = - call_tactic_with_input ProofEngine.cut rendering_window -;; -let change rendering_window = - call_tactic_with_input_and_goal_input ProofEngine.change rendering_window -;; -let letin rendering_window = - call_tactic_with_input ProofEngine.letin rendering_window -;; -let ring rendering_window = call_tactic ProofEngine.ring rendering_window;; -let clearbody rendering_window = - call_tactic_with_hypothesis_input ProofEngine.clearbody rendering_window -;; -let clear rendering_window = - call_tactic_with_hypothesis_input ProofEngine.clear rendering_window -;; -let fourier rendering_window = - call_tactic ProofEngine.fourier rendering_window -;; -let rewritesimpl rendering_window = - call_tactic_with_input ProofEngine.rewrite_simpl rendering_window -;; - - - -let whd_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch - scratch_window -;; -let reduce_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.reduce_in_scratch - scratch_window -;; -let simpl_in_scratch scratch_window = - call_tactic_with_goal_input_in_scratch ProofEngine.simpl_in_scratch - scratch_window -;; - - - -(**********************) -(* END OF TACTICS *) -(**********************) - -exception OpenConjecturesStillThere;; -exception WrongProof;; - -let qed rendering_window () = - match !ProofEngine.proof with - None -> assert false - | Some (uri,[],bo,ty) -> - if - CicReduction.are_convertible [] - (CicTypeChecker.type_of_aux' [] [] bo) ty - then - begin - (*CSC: Wrong: [] is just plainly wrong *) - let proof = Cic.Definition (UriManager.name_of_uri uri,bo,ty,[]) in - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object proof - in - let mml = - mml_of_cic_object uri acic ids_to_inner_sorts ids_to_inner_types - in - (rendering_window#output : GMathView.math_view)#load_tree mml ; - current_cic_infos := - Some - (ids_to_terms,ids_to_father_ids,ids_to_conjectures, - ids_to_hypotheses) - end - else - raise WrongProof - | _ -> raise OpenConjecturesStillThere -;; - -(*???? -let dtdname = "http://www.cs.unibo.it/helm/dtd/cic.dtd";; -*) -let dtdname = "/home/tassi/miohelm/helm/dtd/cic.dtd";; - -let save rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - match !ProofEngine.proof with - None -> assert false - | Some (uri, metasenv, bo, ty) -> - let currentproof = - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty) - in - let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = - Cic2acic.acic_object_of_cic_object currentproof - in - let xml = Cic2Xml.print_object uri ~ids_to_inner_sorts acurrentproof in - let xml' = - [< Xml.xml_cdata "\n" ; - Xml.xml_cdata - ("\n\n") ; - xml - >] - in - Xml.pp ~quiet:true xml' (Some prooffile) ; - output_html outputhtml - ("

Current proof saved to " ^ - prooffile ^ "

") -;; - -(* Used to typecheck the loaded proofs *) -let typecheck_loaded_proof metasenv bo ty = - let module T = CicTypeChecker in - (*CSC: bisogna controllare anche il metasenv!!! *) - ignore (T.type_of_aux' metasenv [] ty) ; - ignore (T.type_of_aux' metasenv [] bo) -;; - -let load rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - try - let uri = UriManager.uri_of_string "cic:/dummy.con" in - match CicParser.obj_of_xml prooffile uri with - Cic.CurrentProof (_,metasenv,bo,ty) -> - typecheck_loaded_proof metasenv bo ty ; - ProofEngine.proof := - Some (uri, metasenv, bo, ty) ; - ProofEngine.goal := - (match metasenv with - [] -> None - | (metano,_,_)::_ -> Some metano - ) ; - refresh_proof output ; - refresh_sequent proofw ; - output_html outputhtml - ("

Current proof loaded from " ^ - prooffile ^ "

") - | _ -> assert false - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; -;; - -let proveit rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - match rendering_window#output#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - (*CSC: OCAML DIVERGE - ((element : G.element)#getAttributeNS - *) - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids, _, _) -> - let id = xpath in - L.to_sequent id ids_to_terms ids_to_father_ids ; - refresh_proof rendering_window#output ; - refresh_sequent rendering_window#proofw - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | None -> assert false (* "ERROR: No selection!!!" *) -;; - -let focus rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - match rendering_window#output#get_selection with - Some node -> - let xpath = - ((node : Gdome.element)#getAttributeNS - (*CSC: OCAML DIVERGE - ((element : G.element)#getAttributeNS - *) - ~namespaceURI:helmns - ~localName:(G.domString "xref"))#to_string - in - if xpath = "" then assert false (* "ERROR: No xref found!!!" *) - else - begin - try - match !current_cic_infos with - Some (ids_to_terms, ids_to_father_ids, _, _) -> - let id = xpath in - L.focus id ids_to_terms ids_to_father_ids ; - refresh_sequent rendering_window#proofw - | None -> assert false (* "ERROR: No current term!!!" *) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") - end - | None -> assert false (* "ERROR: No selection!!!" *) -;; - -exception NoPrevGoal;; -exception NoNextGoal;; - -let prevgoal metasenv metano = - let rec aux = - function - [] -> assert false - | [(m,_,_)] -> raise NoPrevGoal - | (n,_,_)::(m,_,_)::_ when m=metano -> n - | _::tl -> aux tl - in - aux metasenv -;; - -let nextgoal metasenv metano = - let rec aux = - function - [] -> assert false - | [(m,_,_)] when m = metano -> raise NoNextGoal - | (m,_,_)::(n,_,_)::_ when m=metano -> n - | _::tl -> aux tl - in - aux metasenv -;; - -let prev_or_next_goal select_goal rendering_window () = - let module L = LogicalOperations in - let module G = Gdome in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - let metano = - match !ProofEngine.goal with - None -> assert false - | Some m -> m - in - try - ProofEngine.goal := Some (select_goal metasenv metano) ; - refresh_sequent rendering_window#proofw - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; - -exception NotADefinition;; - -let open_ rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - try - let uri = UriManager.uri_of_string ("cic:" ^ input) in - CicTypeChecker.typecheck uri ; - let metasenv,bo,ty = - match CicEnvironment.get_cooked_obj uri 0 with - Cic.Definition (_,bo,ty,_) -> [],bo,ty - | Cic.CurrentProof (_,metasenv,bo,ty) -> metasenv,bo,ty - | Cic.Axiom _ - | Cic.Variable _ - | Cic.InductiveDefinition _ -> raise NotADefinition - in - ProofEngine.proof := - Some (uri, metasenv, bo, ty) ; - ProofEngine.goal := None ; - refresh_sequent proofw ; - refresh_proof output ; - inputt#delete_text 0 inputlen ; - ignore(oldinputt#insert_text input oldinputt#length) - with - RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; -;; - -let state rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let oldinputt = (rendering_window#oldinputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - (* Do something interesting *) - let lexbuf = Lexing.from_string input in - try - while true do - (* Execute the actions *) - match CicTextualParser.main CicTextualLexer.token lexbuf with - None -> () - | Some expr -> - let _ = CicTypeChecker.type_of_aux' [] [] expr in - ProofEngine.proof := - Some (UriManager.uri_of_string "cic:/dummy.con", - [1,[],expr], Cic.Meta (1,[]), expr) ; - ProofEngine.goal := Some 1 ; - refresh_sequent proofw ; - refresh_proof output ; - done - with - CicTextualParser0.Eof -> - inputt#delete_text 0 inputlen ; - ignore(oldinputt#insert_text input oldinputt#length) - | RefreshSequentException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "sequent: " ^ Printexc.to_string e ^ "

") - | RefreshProofException e -> - output_html outputhtml - ("

Exception raised during the refresh of the " ^ - "proof: " ^ Printexc.to_string e ^ "

") - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; -;; - -let check rendering_window scratch_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let output = (rendering_window#output : GMathView.math_view) in - let proofw = (rendering_window#proofw : GMathView.math_view) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen ^ "\n" in - let curi,metasenv = - match !ProofEngine.proof with - None -> UriManager.uri_of_string "cic:/dummy.con", [] - | Some (curi,metasenv,_,_) -> curi,metasenv - in - let context,names_context = - let context = - match !ProofEngine.goal with - None -> [] - | Some metano -> - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=metano) metasenv - in - canonical_context - in - context, - List.map - (function - Some (n,_) -> Some n - | None -> None - ) context - in - (* Do something interesting *) - let lexbuf = Lexing.from_string input in - try - while true do - (* Execute the actions *) - match - CicTextualParserContext.main curi names_context metasenv - CicTextualLexer.token lexbuf - with - None -> () - | Some (metasenv',expr) -> - try - let ty = CicTypeChecker.type_of_aux' metasenv' context expr in - let mml = mml_of_cic_term 111 (Cic.Cast (expr,ty)) in - scratch_window#show () ; - scratch_window#mmlwidget#load_tree ~dom:mml - with - e -> - print_endline ("? " ^ CicPp.ppterm expr) ; - raise e - done - with - CicTextualParser0.Eof -> () - | e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") ; -;; - -exception NoObjectsLocated;; - -let user_uri_choice uris = - let uri = - match uris with - [] -> raise NoObjectsLocated - | [uri] -> uri - | uris -> - let choice = - GToolbox.question_box ~title:"Ambiguous result." - ~buttons:uris ~default:1 - "Ambiguous result. Please, choose one." - in - List.nth uris (choice-1) - in - String.sub uri 4 (String.length uri - 4) -;; - -let locate rendering_window () = - let inputt = (rendering_window#inputt : GEdit.text) in - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen in - try - match Str.split (Str.regexp "[ \t]+") input with - [] -> () - | head :: tail -> - inputt#delete_text 0 inputlen ; - let MathQL.MQRefs uris, html = MQueryGenerator.locate head in - output_html outputhtml html ; - let uri' = user_uri_choice uris in - ignore ((inputt#insert_text uri') ~pos:0) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; - -let backward rendering_window () = - let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in - let inputt = (rendering_window#inputt : GEdit.text) in - let inputlen = inputt#length in - let input = inputt#get_chars 0 inputlen in - let level = int_of_string input in - let metasenv = - match !ProofEngine.proof with - None -> assert false - | Some (_,metasenv,_,_) -> metasenv - in - try - match !ProofEngine.goal with - None -> () - | Some metano -> - let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in - let MathQL.MQRefs uris, html = - MQueryGenerator.backward metasenv ey ty level - in - output_html outputhtml html ; - let uri' = user_uri_choice uris in - inputt#delete_text 0 inputlen ; - ignore ((inputt#insert_text uri') ~pos:0) - with - e -> - output_html outputhtml - ("

" ^ Printexc.to_string e ^ "

") -;; - -let choose_selection - (mmlwidget : GMathView.math_view) (element : Gdome.element option) -= - let module G = Gdome in - let rec aux element = - if element#hasAttributeNS - ~namespaceURI:helmns - ~localName:(G.domString "xref") - then - mmlwidget#set_selection (Some element) - else - match element#get_parentNode with - None -> assert false - (*CSC: OCAML DIVERGES! - | Some p -> aux (new G.element_of_node p) - *) - | Some p -> aux (new Gdome.element_of_node p) - in - match element with - Some x -> aux x - | None -> mmlwidget#set_selection None -;; - -(* STUFF TO BUILD THE GTK INTERFACE *) - -(* Stuff for the widget settings *) - -let export_to_postscript (output : GMathView.math_view) () = - output#export_to_postscript ~filename:"output.ps" (); -;; - -let activate_t1 (output : GMathView.math_view) button_set_anti_aliasing - button_set_kerning button_set_transparency button_export_to_postscript - button_t1 () -= - let is_set = button_t1#active in - output#set_font_manager_type - (if is_set then `font_manager_t1 else `font_manager_gtk) ; - if is_set then - begin - button_set_anti_aliasing#misc#set_sensitive true ; - button_set_kerning#misc#set_sensitive true ; - button_set_transparency#misc#set_sensitive true ; - button_export_to_postscript#misc#set_sensitive true ; - end - else - begin - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; - button_set_transparency#misc#set_sensitive false ; - button_export_to_postscript#misc#set_sensitive false ; - end -;; - -let set_anti_aliasing output button_set_anti_aliasing () = - output#set_anti_aliasing button_set_anti_aliasing#active -;; - -let set_kerning output button_set_kerning () = - output#set_kerning button_set_kerning#active -;; - -let set_transparency output button_set_transparency () = - output#set_transparency button_set_transparency#active -;; - -let changefont output font_size_spinb () = - output#set_font_size font_size_spinb#value_as_int -;; - -let set_log_verbosity output log_verbosity_spinb () = - output#set_log_verbosity log_verbosity_spinb#value_as_int -;; - -class settings_window (output : GMathView.math_view) sw - button_export_to_postscript selection_changed_callback -= - let settings_window = GWindow.window ~title:"GtkMathView settings" () in - let vbox = - GPack.vbox ~packing:settings_window#add () in - let table = - GPack.table - ~rows:1 ~columns:3 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#add () in - let button_t1 = - GButton.toggle_button ~label:"activate t1 fonts" - ~packing:(table#attach ~left:0 ~top:0) () in - let button_set_anti_aliasing = - GButton.toggle_button ~label:"set_anti_aliasing" - ~packing:(table#attach ~left:0 ~top:1) () in - let button_set_kerning = - GButton.toggle_button ~label:"set_kerning" - ~packing:(table#attach ~left:1 ~top:1) () in - let button_set_transparency = - GButton.toggle_button ~label:"set_transparency" - ~packing:(table#attach ~left:2 ~top:1) () in - let table = - GPack.table - ~rows:2 ~columns:2 ~homogeneous:false ~row_spacings:5 ~col_spacings:5 - ~border_width:5 ~packing:vbox#add () in - let font_size_label = - GMisc.label ~text:"font size:" - ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in - let font_size_spinb = - let sadj = - GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in - let log_verbosity_label = - GMisc.label ~text:"log verbosity:" - ~packing:(table#attach ~left:0 ~top:1) () in - let log_verbosity_spinb = - let sadj = - GData.adjustment ~value:0.0 ~lower:0.0 ~upper:3.0 ~step_incr:1.0 () - in - GEdit.spin_button - ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:1) () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in -object(self) - method show = settings_window#show - initializer - button_set_anti_aliasing#misc#set_sensitive false ; - button_set_kerning#misc#set_sensitive false ; - button_set_transparency#misc#set_sensitive false ; - (* Signals connection *) - ignore(button_t1#connect#clicked - (activate_t1 output button_set_anti_aliasing button_set_kerning - button_set_transparency button_export_to_postscript button_t1)) ; - ignore(font_size_spinb#connect#changed (changefont output font_size_spinb)) ; - ignore(button_set_anti_aliasing#connect#toggled - (set_anti_aliasing output button_set_anti_aliasing)); - ignore(button_set_kerning#connect#toggled - (set_kerning output button_set_kerning)) ; - ignore(button_set_transparency#connect#toggled - (set_transparency output button_set_transparency)) ; - ignore(log_verbosity_spinb#connect#changed - (set_log_verbosity output log_verbosity_spinb)) ; - ignore(closeb#connect#clicked settings_window#misc#hide) -end;; - -(* Scratch window *) - -class scratch_window outputhtml = - let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 () in - let vbox = - GPack.vbox ~packing:window#add () in - let hbox = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let whdb = - GButton.button ~label:"Whd" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let reduceb = - GButton.button ~label:"Reduce" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let simplb = - GButton.button ~label:"Simpl" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in - let mmlwidget = - GMathView.math_view - ~packing:(scrolled_window#add) ~width:400 ~height:280 () in -object(self) - method outputhtml = outputhtml - method mmlwidget = mmlwidget - method show () = window#misc#hide () ; window#show () - initializer - ignore(mmlwidget#connect#selection_changed (choose_selection mmlwidget)) ; - ignore(window#event#connect#delete (fun _ -> window#misc#hide () ; true )) ; - ignore(whdb#connect#clicked (whd_in_scratch self)) ; - ignore(reduceb#connect#clicked (reduce_in_scratch self)) ; - ignore(simplb#connect#clicked (simpl_in_scratch self)) -end;; - -(* Main window *) - -class rendering_window output proofw (label : GMisc.label) = - let window = - GWindow.window ~title:"MathML viewer" ~border_width:2 () in - let hbox0 = - GPack.hbox ~packing:window#add () in - let vbox = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in - let _ = vbox#pack ~expand:false ~fill:false ~padding:5 label#coerce in - let scrolled_window0 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox#pack ~expand:true ~padding:5) () in - let _ = scrolled_window0#add output#coerce in - let hbox1 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let settingsb = - GButton.button ~label:"Settings" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let button_export_to_postscript = - GButton.button ~label:"export_to_postscript" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let qedb = - GButton.button ~label:"Qed" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let saveb = - GButton.button ~label:"Save" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let loadb = - GButton.button ~label:"Load" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let closeb = - GButton.button ~label:"Close" - ~packing:(hbox1#pack ~expand:false ~fill:false ~padding:5) () in - let hbox2 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let proveitb = - GButton.button ~label:"Prove It" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let focusb = - GButton.button ~label:"Focus" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let prevgoalb = - GButton.button ~label:"<" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let nextgoalb = - GButton.button ~label:">" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let oldinputt = GEdit.text ~editable:false ~width:400 ~height:180 - ~packing:(vbox#pack ~padding:5) () in - let hbox4 = - GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in - let stateb = - GButton.button ~label:"State" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let openb = - GButton.button ~label:"Open" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let locateb = - GButton.button ~label:"Locate" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let backwardb = - GButton.button ~label:"Backward" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let inputt = GEdit.text ~editable:true ~width:400 ~height: 100 - ~packing:(vbox#pack ~padding:5) () in - let vbox1 = - GPack.vbox ~packing:(hbox0#pack ~expand:false ~fill:false ~padding:5) () in - let scrolled_window1 = - GBin.scrolled_window ~border_width:10 - ~packing:(vbox1#pack ~expand:true ~padding:5) () in - let _ = scrolled_window1#add proofw#coerce in - let hbox3 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let exactb = - GButton.button ~label:"Exact" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let introsb = - GButton.button ~label:"Intros" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let applyb = - GButton.button ~label:"Apply" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimintrossimplb = - GButton.button ~label:"ElimIntrosSimpl" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimtypeb = - GButton.button ~label:"ElimType" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let whdb = - GButton.button ~label:"Whd" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let reduceb = - GButton.button ~label:"Reduce" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let simplb = - GButton.button ~label:"Simpl" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let foldb = - GButton.button ~label:"Fold" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let cutb = - GButton.button ~label:"Cut" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let changeb = - GButton.button ~label:"Change" - ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let hbox4 = - GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in - let letinb = - GButton.button ~label:"Let ... In" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let ringb = - GButton.button ~label:"Ring" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let clearbodyb = - GButton.button ~label:"ClearBody" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let clearb = - GButton.button ~label:"Clear" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let fourierb = - GButton.button ~label:"Fourier" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let rewritesimplb = - GButton.button ~label:"RewriteSimpl ->" - ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in - let outputhtml = - GHtml.xmhtml - ~source:"" - ~width:400 ~height: 200 - ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) - ~show:true () in - let scratch_window = new scratch_window outputhtml in -object(self) - method outputhtml = outputhtml - method oldinputt = oldinputt - method inputt = inputt - method output = (output : GMathView.math_view) - method proofw = (proofw : GMathView.math_view) - method show = window#show - initializer - button_export_to_postscript#misc#set_sensitive false ; - - (* signal handlers here *) - ignore(output#connect#selection_changed - (function elem -> proofw#unload ; choose_selection output elem)) ; - ignore(proofw#connect#selection_changed (choose_selection proofw)) ; - ignore(closeb#connect#clicked (fun _ -> GMain.Main.quit ())) ; - let settings_window = new settings_window output scrolled_window0 - button_export_to_postscript (choose_selection output) in - ignore(settingsb#connect#clicked settings_window#show) ; - ignore(button_export_to_postscript#connect#clicked (export_to_postscript output)) ; - ignore(qedb#connect#clicked (qed self)) ; - ignore(saveb#connect#clicked (save self)) ; - ignore(loadb#connect#clicked (load self)) ; - ignore(proveitb#connect#clicked (proveit self)) ; - ignore(focusb#connect#clicked (focus self)) ; - ignore(prevgoalb#connect#clicked (prev_or_next_goal prevgoal self)) ; - ignore(nextgoalb#connect#clicked (prev_or_next_goal nextgoal self)) ; - ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ; - ignore(stateb#connect#clicked (state self)) ; - ignore(openb#connect#clicked (open_ self)) ; - ignore(checkb#connect#clicked (check self scratch_window)) ; - ignore(locateb#connect#clicked (locate self)) ; - ignore(backwardb#connect#clicked (backward self)) ; - ignore(exactb#connect#clicked (exact self)) ; - ignore(applyb#connect#clicked (apply self)) ; - ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ; - ignore(elimtypeb#connect#clicked (elimtype self)) ; - ignore(whdb#connect#clicked (whd self)) ; - ignore(reduceb#connect#clicked (reduce self)) ; - ignore(simplb#connect#clicked (simpl self)) ; - ignore(foldb#connect#clicked (fold self)) ; - ignore(cutb#connect#clicked (cut self)) ; - ignore(changeb#connect#clicked (change self)) ; - ignore(letinb#connect#clicked (letin self)) ; - ignore(ringb#connect#clicked (ring self)) ; - ignore(clearbodyb#connect#clicked (clearbody self)) ; - ignore(clearb#connect#clicked (clear self)) ; - ignore(fourierb#connect#clicked (fourier self)) ; - ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; - ignore(introsb#connect#clicked (intros self)) ; - Logger.log_callback := - (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) -end;; - -(* MAIN *) - -let rendering_window = ref None;; - -let initialize_everything () = - let module U = Unix in - let output = GMathView.math_view ~width:350 ~height:280 () - and proofw = GMathView.math_view ~width:400 ~height:275 () - and label = GMisc.label ~text:"gTopLevel" () in - let rendering_window' = - new rendering_window output proofw label - in - rendering_window := Some rendering_window' ; - rendering_window'#show () ; - GMain.Main.main () -;; - -let _ = - CicCooking.init () ; - if !usedb then - begin - MQueryGenerator.init () ; - CicTextualParser0.set_locate_object - (function id -> - let MathQL.MQRefs uris, html = MQueryGenerator.locate id in - begin - match !rendering_window with - None -> assert false - | Some rw -> output_html rw#outputhtml html ; - end ; - let uri = - match uris with - [] -> - (match - (GToolbox.input_string ~title:"Unknown input" - ("No URI matching \"" ^ id ^ "\" found. Please enter its URI")) - with - None -> None - | Some uri -> Some ("cic:" ^ uri) - ) - | [uri] -> Some uri - | _ -> - let choice = - GToolbox.question_box ~title:"Ambiguous input." - ~buttons:uris ~default:1 "Ambiguous input. Please, choose one." - in - if choice > 0 then - Some (List.nth uris (choice - 1)) - else - (* No choice from the user *) - None - in - match uri with - Some uri' -> - (* Constant *) - if String.sub uri' (String.length uri' - 4) 4 = ".con" then -(*CSC: what cooking number? Here I always use 0, which may be bugged *) - Some (Cic.Const (UriManager.uri_of_string uri',0)) - else - (try - (* Inductive Type *) - let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in -(*CSC: what cooking number? Here I always use 0, which may be bugged *) - Some (Cic.MutInd (uri'',0,typeno)) - with - _ -> - (* Constructor of an Inductive Type *) - let uri'',typeno,consno = - CicTextualLexer.indconuri_of_uri uri' - in -(*CSC: what cooking number? Here I always use 0, which may be bugged *) - Some (Cic.MutConstruct (uri'',0,typeno,consno)) - ) - | None -> None - ) - end ; - ignore (GtkMain.Main.init ()) ; - initialize_everything () ; - if !usedb then MQueryGenerator.close (); -;; diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml deleted file mode 100644 index 4deaf8c7a..000000000 --- a/helm/gTopLevel/mQueryGenerator.ml +++ /dev/null @@ -1,228 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -(* level managing functions *************************************************) - -type levels_spec = (string * bool * int) list - -let levels_of_term metasenv context term = - let module TC = CicTypeChecker in - let module Red = CicReduction in - let module Util = MQueryUtil in - let degree t = - let rec degree_aux = function - | Cic.Sort _ -> 1 - | Cic.Cast (u, _) -> degree_aux u - | Cic.Prod (_, _, t) -> degree_aux t - | _ -> 2 - in - let u = TC.type_of_aux' metasenv context t in - degree_aux (Red.whd context u) - in - let entry_eq (s1, b1, v1) (s2, b2, v2) = - s1 = s2 && b1 = b2 - in - let rec entry_in e = function - | [] -> [e] - | head :: tail -> - head :: if entry_eq head e then tail else entry_in e tail - in - let inspect_uri main l uri tc v term = - let d = degree term in - entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l - in - let rec inspect_term main l v term = match term with - | Cic.Rel _ -> l - | Cic.Meta (_, _) -> l - | Cic.Sort _ -> l - | Cic.Implicit -> l - | Cic.Var u -> inspect_uri main l u [] v term - | Cic.Const (u, _) -> inspect_uri main l u [] v term - | Cic.MutInd (u, _, t) -> inspect_uri main l u [t] v term - | Cic.MutConstruct (u, _, t, c) -> inspect_uri main l u [t; c] v term - | Cic.Cast (uu, _) -> - inspect_term main l v uu - | Cic.Prod (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term main luu (v + 1) tt - | Cic.Lambda (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Cic.LetIn (_, uu, tt) -> - let luu = inspect_term false l (v + 1) uu in - inspect_term false luu (v + 1) tt - | Cic.Appl m -> inspect_list main l true v m - | Cic.MutCase (u, _, t, tt, uu, m) -> - let lu = inspect_uri main l u [t] (v + 1) term in - let ltt = inspect_term false lu (v + 1) tt in - let luu = inspect_term false ltt (v + 1) uu in - inspect_list main luu false (v + 1) m - | Cic.Fix (_, m) -> inspect_ind l (v + 1) m - | Cic.CoFix (_, m) -> inspect_coind l (v + 1) m - and inspect_list main l head v = function - | [] -> l - | tt :: m -> - let ltt = inspect_term main l (if head then v else v + 1) tt in - inspect_list false ltt false v m - and inspect_ind l v = function - | [] -> l - | (_, _, tt, uu) :: m -> - let ltt = inspect_term false l v tt in - let luu = inspect_term false ltt v uu in - inspect_ind luu v m - and inspect_coind l v = function - | [] -> l - | (_, tt, uu) :: m -> - let ltt = inspect_term false l v tt in - let luu = inspect_term false ltt v uu in - inspect_coind luu v m - in - let rec inspect_backbone = function - | Cic.Cast (uu, _) -> inspect_backbone uu - | Cic.Prod (_, _, tt) -> inspect_backbone tt - | Cic.LetIn (_, uu, tt) -> inspect_backbone tt - | t -> inspect_term true [] 0 t - in - inspect_backbone term - -let string_of_levels l sep = - let entry_out (s, b, v) = - let pos = if b then " HEAD: " else " TAIL: " in - string_of_int v ^ pos ^ s ^ sep - in - let rec levels_out = function - | [] -> "" - | head :: tail -> entry_out head ^ levels_out tail - in - levels_out l - -(* Query issuing functions **************************************************) - -exception Discard - -let nl = "

\n" - -let query_num = ref 1 - -let log_file = ref "" - -let confirm_query = ref (fun _ -> true) - -let info = ref [] - -let set_log_file f = - log_file := f - -let set_confirm_query f = - confirm_query := f - -let get_query_info () = ! info - -let execute_query query = - let module Util = MQueryUtil in - let mode = [Open_wronly; Open_append; Open_creat; Open_text] in - let perm = 64 * 6 + 8 * 6 + 4 in - let time () = - let lt = Unix.localtime (Unix.time ()) in - "NEW LOG: " ^ - string_of_int (lt.Unix.tm_mon + 1) ^ "-" ^ - string_of_int (lt.Unix.tm_mday + 1) ^ "-" ^ - string_of_int (lt.Unix.tm_year + 1900) ^ " " ^ - string_of_int (lt.Unix.tm_hour) ^ ":" ^ - string_of_int (lt.Unix.tm_min) ^ ":" ^ - string_of_int (lt.Unix.tm_sec) - in - let log q r = - let och = open_out_gen mode perm ! log_file in - if ! query_num = 1 then output_string och (time () ^ nl); - let str = "Query: " ^ string_of_int ! query_num ^ nl ^ Util.text_of_query q ^ nl ^ - "Result:" ^ nl ^ Util.text_of_result r nl in - output_string och str; - flush och - in - let execute q = - let r = Mqint.execute q in - if ! log_file <> "" then log q r; - info := string_of_int ! query_num :: ! info; - incr query_num; - r - in - if ! confirm_query query then execute query else raise Discard - -(* Query building functions ************************************************) - -let locate s = - let module M = MathQL in - let q = M.Ref (M.Fun "reference" (M.Const [s])) in - execute_query q - -let backward e c t level = - let module M = MathQL in - let v_pos = M.Const ["MainConclusion"; "InConclusion"] in - let q_where = M.Sub (M.RefOf ( - M.Select ("uri", - M.Relation (M.ExactOp, ["refObj"], M.RVar "uri0", ["pos"]), - M.Ex ["uri"] (M.Meet (M.VVar "positions", M.Record ("uri", "pos"))) - )), M.VVar "universe" - ) - in - let uri_of_entry (r, b, v) = r in - let rec restrict level = function - | [] -> [] - | (u, b, v) :: tail -> - if v <= level then (u, b, v) :: restrict level tail - else restrict level tail - in - let build_select (r, b, v) = - let pos = if b then "MainConclusion" else "InConclusion" in - M.Select ("uri", - M.Relation (M.ExactOp, ["backPointer"], M.Ref (M.Const [r]), ["pos"]), - M.Ex ["uri"] (M.Sub (M.Const [pos], M.Record ("uri", "pos"))) - ) - in - let rec build_intersect = function - | [] -> M.Pattern (M.Const [".*"]) - | [hd] -> build_select hd - | hd :: tl -> M.Intersect (build_select hd, build_intersect tl) - in - let levels = levels_of_term e c t in - let rest = restrict level levels in - info := [string_of_int (List.length rest)]; - let q_in = build_intersect rest in - let q_select = M.Select ("uri0", q_in, q_where) in - let universe = M.Const (List.map uri_of_entry levels) in - let q_let_u = M.LetVVar ("universe", universe, q_select) in - let q_let_p = M.LetVVar ("positions", v_pos, q_let_u) in - execute_query q_let_p diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli deleted file mode 100644 index 21202a2e9..000000000 --- a/helm/gTopLevel/mQueryGenerator.mli +++ /dev/null @@ -1,54 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - -exception Discard - -type levels_spec = (string * bool * int) list - -val levels_of_term : Cic.metasenv -> Cic.context -> Cic.term -> levels_spec - -val string_of_levels : levels_spec -> string -> string - -val set_log_file : string -> unit - -val set_confirm_query : (MathQL.query -> bool) -> unit - -val execute_query : MathQL.query -> MathQL.result - -val locate : string -> MathQL.result - -val backward : Cic.metasenv -> Cic.context -> Cic.term -> int -> MathQL.result - -val get_query_info : unit -> string list diff --git a/helm/gTopLevel/topLevel/.depend b/helm/gTopLevel/topLevel/.depend deleted file mode 100644 index e69de29bb..000000000 diff --git a/helm/gTopLevel/topLevel/Makefile b/helm/gTopLevel/topLevel/Makefile deleted file mode 100644 index 01dd0e173..000000000 --- a/helm/gTopLevel/topLevel/Makefile +++ /dev/null @@ -1,47 +0,0 @@ -BIN_DIR = /usr/local/bin -REQUIRES = helm-urimanager helm-cic_textual_parser helm-cic_proof_checking helm-mathql helm-mathql_interpreter -PREDICATES = -OCAMLOPTIONS = -I .. -package "$(REQUIRES)" -predicates "$(PREDICATES)" -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = ocamldep - -LIBRARIES = $(shell ocamlfind query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) -LIBRARIES_OPT = $(shell ocamlfind query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES)) - -all: topLevel -opt: topLevel.opt - -DEPOBJS = topLevel.ml - -TOPLEVELOBJS = ../mQueryGenerator.cmo topLevel.cmo - -depend: - $(OCAMLDEP) $(DEPOBJS) > .depend - -topLevel: $(TOPLEVELOBJS) $(LIBRARIES) - $(OCAMLC) -linkpkg -o topLevel $(TOPLEVELOBJS) - -topLevel.opt: $(TOPLEVELOBJS:.cmo=.cmx) $(LIBRARIES_OPT) - $(OCAMLOPT) -linkpkg -o topLevel.opt $(TOPLEVELOBJS:.cmo=.cmx) - -.SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: $(LIBRARIES) - $(OCAMLC) -c $< -.mli.cmi: $(LIBRARIES) - $(OCAMLC) -c $< -.ml.cmx: $(LIBRARIES_OPT) - $(OCAMLOPT) -c $< - -clean: - rm -f *.cm[iox] *.o topLevel topLevel.opt - -install: - cp topLevel topLevel.opt $(BIN_DIR) - -uninstall: - rm -f $(BIN_DIR)/topLevel $(BIN_DIR)/topLevel.opt - -.PHONY: install uninstall clean - -include .depend diff --git a/helm/gTopLevel/topLevel/esempi.cic b/helm/gTopLevel/topLevel/esempi.cic deleted file mode 100644 index 38e5f3333..000000000 --- a/helm/gTopLevel/topLevel/esempi.cic +++ /dev/null @@ -1,125 +0,0 @@ -alias BV /Sophia-Antipolis/HARDWARE/GENE/BV/BV.con -alias BV_increment /Sophia-Antipolis/HARDWARE/ADDER/IncrDecr/BV_increment.con -alias BV_increment_carry /Sophia-Antipolis/HARDWARE/ADDER/IncrDecr/BV_increment_carry.con -alias BV_to_nat /Sophia-Antipolis/HARDWARE/GENE/BV/BV_to_nat.con -alias Exp /Eindhoven/POCKLINGTON/exp/Exp.con -alias IZR /Coq/Reals/Raxioms/IZR.con -alias Int_part /Coq/Reals/R_Ifp/Int_part.con -alias Mod /Eindhoven/POCKLINGTON/mod/Mod.con -alias NEG /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/3 -alias O /Coq/Init/Datatypes/nat.ind#1/1/1 -alias POS /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/2 -alias Prime /Eindhoven/POCKLINGTON/prime/Prime.con -alias R /Coq/Reals/Rdefinitions/R.con -alias R0 /Coq/Reals/Rdefinitions/R0.con -alias R1 /Coq/Reals/Rdefinitions/R1.con -alias Rgt /Coq/Reals/Rdefinitions/Rgt.con -alias Rinv /Coq/Reals/Rdefinitions/Rinv.con -alias Rle /Coq/Reals/Rdefinitions/Rle.con -alias Rlt /Coq/Reals/Rdefinitions/Rlt.con -alias Rminus /Coq/Reals/Rdefinitions/Rminus.con -alias Rmult /Coq/Reals/Rdefinitions/Rmult.con -alias Ropp /Coq/Reals/Rdefinitions/Ropp.con -alias Rplus /Coq/Reals/Rdefinitions/Rplus.con -alias S /Coq/Init/Datatypes/nat.ind#1/1/2 -alias Z /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1 -alias ZERO /Coq/ZArith/fast_integer/fast_integers/Z.ind#1/1/1 -alias ZExp /Eindhoven/POCKLINGTON/exp/ZExp.con -alias Zdiv2 /Coq/ZArith/Zmisc/arith/Zdiv2.con -alias Zge /Coq/ZArith/zarith_aux/Zge.con -alias Zle /Coq/ZArith/zarith_aux/Zle.con -alias Zlt /Coq/ZArith/zarith_aux/Zlt.con -alias Zminus /Coq/ZArith/zarith_aux/Zminus.con -alias Zmult /Coq/ZArith/fast_integer/fast_integers/Zmult.con -alias Zodd /Coq/ZArith/Zmisc/arith/Zodd.con -alias Zplus /Coq/ZArith/fast_integer/fast_integers/Zplus.con -alias Zpower_nat /Coq/omega/Zpower/section1/Zpower_nat.con -alias Zpower_pos /Coq/omega/Zpower/section1/Zpower_pos.con -alias Zpred /Coq/ZArith/zarith_aux/Zpred.con -alias Zs /Coq/ZArith/zarith_aux/Zs.con -alias ad /Coq/IntMap/Addr/ad.ind#1/1 -alias ad_bit /Coq/IntMap/Addr/ad_bit.con -alias ad_double_plus_un /Coq/IntMap/Addr/ad_double_plus_un.con -alias ad_x /Coq/IntMap/Addr/ad.ind#1/1/2 -alias ad_xor /Coq/IntMap/Addr/ad_xor.con -alias allex /Eindhoven/POCKLINGTON/fermat/allex.con -alias and /Coq/Init/Logic/Conjunction/and.ind#1/1 -alias appbv /Sophia-Antipolis/HARDWARE/GENE/BV/appbv.con -alias bool /Coq/Init/Datatypes/bool.ind#1/1 -alias consbv /Sophia-Antipolis/HARDWARE/GENE/BV/consbv.con -alias convert /Coq/ZArith/fast_integer/fast_integers/convert.con -alias div2 /Coq/Arith/Div2/div2.con -alias double /Coq/Arith/Div2/double.con -alias eq /Coq/Init/Logic/Equality/eq.ind#1/1 -alias eq_ind /Coq/Init/Logic/Equality/eq_ind.con -alias eq_ind_r /Coq/Init/Logic/Logic_lemmas/eq_ind_r.con -alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 -alias even /Coq/Arith/Even/even.ind#1/1 -alias ex /Coq/Init/Logic/First_order_quantifiers/ex.ind#1/1 -alias f_equal /Coq/Init/Logic/Logic_lemmas/equality/f_equal.con -alias iff /Coq/Init/Logic/Equivalence/iff.con -alias le /Coq/Init/Peano/le.ind#1/1 -alias lengthbv /Sophia-Antipolis/HARDWARE/GENE/BV/lengthbv.con -alias lift_rec_r /Rocq/LAMBDA/Substitution/lift_rec_r.con -alias log_inf /Coq/omega/Zlogarithm/Log_pos/log_inf.con -alias log_sup /Coq/omega/Zlogarithm/Log_pos/log_sup.con -alias lt /Coq/Init/Peano/lt.con -alias mapmult /Eindhoven/POCKLINGTON/list/mapmult.con -alias minus /Coq/Arith/Minus/minus.con -alias mult /Coq/Init/Peano/mult.con -alias nat /Coq/Init/Datatypes/nat.ind#1/1 -alias nat_of_ad /Coq/IntMap/Adalloc/AdAlloc/nat_of_ad.con -alias negb /Coq/Bool/Bool/negb.con -alias nilbv /Sophia-Antipolis/HARDWARE/GENE/BV/nilbv.con -alias not /Coq/Init/Logic/not.con -alias odd /Coq/Arith/Even/even.ind#1/2 -alias or /Coq/Init/Logic/Disjunction/or.ind#1/1 -alias permmod /Eindhoven/POCKLINGTON/fermat/permmod.con -alias plus /Coq/Init/Peano/plus.con -alias positive /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1 -alias power2 /Sophia-Antipolis/HARDWARE/GENE/Arith_compl/power2.con -alias pred /Coq/Init/Peano/pred.con -alias redexes /Rocq/LAMBDA/Redexes/redexes.ind#1/1 -alias shift_nat /Coq/omega/Zpower/Powers_of_2/shift_nat.con -alias shift_pos /Coq/omega/Zpower/Powers_of_2/shift_pos.con -alias subst_rec_r /Rocq/LAMBDA/Substitution/subst_rec_r.con -alias two_p /Coq/omega/Zpower/Powers_of_2/two_p.con -alias until /Eindhoven/POCKLINGTON/fermat/until.con -alias xH /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/3 -alias xI /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/1 -alias xO /Coq/ZArith/fast_integer/fast_integers/positive.ind#1/1/2 -alias zproduct /Eindhoven/POCKLINGTON/list/zproduct.con - -!n:nat.(eq nat (mult (S (S O)) n) O); -!n:nat.(eq nat (plus O n) (plus n O)); -!n:nat.!m:nat.(le (mult (S (S O)) n) (mult (S (S O)) m)); -!p:nat.(eq nat p p)->(eq nat p p); -!p:nat.!q:nat.(le p q)->(or (le (S p) q) (eq nat p q)); -!n:nat.(eq nat (double (S n)) (S (S (double n)))); -!n:nat.(and (iff (even n) (eq nat (div2 n) (div2 (S n)))) (iff (odd n) (eq nat (S (div2 n)) (div2 (S n))))); -!n:nat.!m:nat.!p:nat.(eq nat (minus n m) (minus (plus p n) (plus p m))); -!a:Z.!n:nat.(eq Z (Exp a (pred (S n))) (Exp a n)); -!a:Z.!x:Z.(eq Z (ZExp a (Zminus (Zplus x (POS xH)) (POS xH))) (ZExp a x)); -!p:nat.!a:Z.(Prime p)->(not (Mod a ZERO p))->(allex p (until (pred p)) (mapmult a (until (pred p)))); -!a:Z.!n:nat.(eq Z (zproduct (mapmult a (until n))) (Zmult (Exp a n) (zproduct (until n)))); -!p:nat.!a:Z.(Prime p)->(not (Mod a ZERO p))->(permmod p (until (pred p)) (mapmult a (until (pred p)))); -!p:nat.(Prime p)->(not (Mod (zproduct (until (pred p))) ZERO p)); -!p:nat.!n:nat.(lt O n)->(lt n p)->(Prime p)->(not (Mod (zproduct (until n)) ZERO p)); -!p:positive.(eq nat (convert (xI p)) (S (mult (S (S O)) (convert p)))); -!a:ad.(eq nat (nat_of_ad (ad_double_plus_un a)) (S (mult (S (S O)) (nat_of_ad a)))); -!p:positive.!a:ad.(eq bool (ad_bit (ad_xor (ad_x (xI p)) a) O) (negb (ad_bit a O))); -!r:R.(and (Rle (IZR (Int_part r)) r) (Rgt (Rminus (IZR (Int_part r)) r) (Ropp R1))); -!eps:R.(Rgt eps R0)->(Rlt (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))) eps); -!x:Z.(Zge x ZERO)->(Zodd x)->(eq Z x (Zplus (Zmult (POS (xO xH)) (Zdiv2 x)) (POS xH))); -!v:Z.!l1:Z.!l2:Z.!x:positive.(eq Z (Zplus (Zplus (Zmult v (POS x)) l1) (Zplus (Zmult v (NEG x)) l2)) (Zplus l1 l2)); -!v:Z.!l1:Z.!l2:Z.!x:positive.(eq Z (Zplus (Zplus (Zmult v (NEG x)) l1) (Zplus (Zmult v (POS x)) l2)) (Zplus l1 l2)); -!p:positive.(and (Zle (two_p (log_inf p)) (POS p)) (Zlt (POS p) (two_p (Zs (log_inf p))))); -!x:positive.(and (Zlt (two_p (Zpred (log_sup x))) (POS x)) (Zle (POS x) (two_p (log_sup x)))); -!n:nat.!x:positive.(eq Z (POS (shift_nat n x)) (Zmult (Zpower_nat (POS (xO xH)) n) (POS x))); -!p:positive.!x:positive.(eq Z (POS (shift_pos p x)) (Zmult (Zpower_pos (POS (xO xH)) p) (POS x))); -!U:redexes.!V:redexes.!k:nat.!p:nat.!n:nat.(eq redexes (lift_rec_r (subst_rec_r V U p) (plus p n) k) (subst_rec_r (lift_rec_r V (S (plus p n)) k) (lift_rec_r U n k) p)); -!U:redexes.!V:redexes.!W:redexes.!n:nat.!p:nat.(eq redexes (subst_rec_r (subst_rec_r V U p) W (plus p n)) (subst_rec_r (subst_rec_r V W (S (plus p n))) (subst_rec_r U W n) p)); -!v:BV.(eq nat (BV_to_nat (appbv (BV_increment v) (consbv (BV_increment_carry v) nilbv))) (S (BV_to_nat v))); -!l:BV.!n:BV.(eq nat (BV_to_nat (appbv l n)) (plus (BV_to_nat l) (mult (power2 (lengthbv l)) (BV_to_nat n)))); -!x:Z.(Zle ZERO x)->(eq Z (Zdiv2 (Zplus (Zmult (POS (xO xH)) x) (POS xH))) x); -!n:Z.(Zle (POS xH) n)->(Zle ZERO (Zplus (Zdiv2 (Zminus n (POS (xO xH)))) (POS xH))); diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml deleted file mode 100644 index cc1b3034b..000000000 --- a/helm/gTopLevel/topLevel/topLevel.ml +++ /dev/null @@ -1,190 +0,0 @@ -let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm" - -let show_queries = ref false - -let use_db = ref true - -let db_down = ref true - -let nl = "

\n" - -let check_db () = - if ! db_down then - if ! use_db then begin Mqint.init connection_param; db_down := false; true end - else begin print_endline "Not issuing in restricted mode"; false end - else true - -let default_confirm q = - let module Util = MQueryUtil in - if ! show_queries then print_string (Util.text_of_query q ^ nl); - let b = check_db () in - if ! db_down then print_endline "db_down"; b - -let get_terms () = - let terms = ref [] in - let lexbuf = Lexing.from_channel stdin in - try - while true do - match CicTextualParserContext.main - (UriManager.uri_of_string "cic:/dummy") [] [] - CicTextualLexer.token lexbuf - with - | None -> () - | Some (_, expr) -> terms := expr :: ! terms - done; - ! terms - with - CicTextualParser0.Eof -> ! terms - -let pp_type_of uri = - let u = UriManager.uri_of_string uri in - let s = match (CicEnvironment.get_obj u) with - | Cic.Definition (_, _, ty, _) -> CicPp.ppterm ty - | Cic.Axiom (_, ty, _) -> CicPp.ppterm ty - | Cic.Variable (_, _, ty) -> CicPp.ppterm ty - | _ -> "Current proof or inductive definition." -(* - | Cic.CurrentProof (_,conjs,te,ty) -> - | C.InductiveDefinition _ -> -*) - in print_endline s; flush stdout - -let dbc () = - let on = check_db () in - if on then ignore (Mqint.check ()) - -let rec display = function - | [] -> () - | term :: tail -> - display tail; - print_string ("? " ^ CicPp.ppterm term ^ nl); - flush stdout - -let levels l = - let module Gen = MQueryGenerator in - let rec levels_aux = function - | [] -> () - | term :: tail -> - levels_aux tail; - print_string ("? " ^ CicPp.ppterm term ^ nl); - print_string (Gen.string_of_levels (Gen.levels_of_term [] [] term) nl); - flush stdout - in - levels_aux l - -let execute ich = - let module Util = MQueryUtil in - let module Gen = MQueryGenerator in - Gen.set_confirm_query default_confirm; - try - let q = Util.query_of_text (Lexing.from_channel ich) in - print_endline (Util.text_of_result (Gen.execute_query q) nl); - flush stdout - with Gen.Discard -> () - -let locate name = - let module Util = MQueryUtil in - let module Gen = MQueryGenerator in - Gen.set_confirm_query default_confirm; - try - print_endline (Util.text_of_result (Gen.locate name) nl); - flush stdout - with Gen.Discard -> () - -let mbackward n m l = - let module Util = MQueryUtil in - let module Gen = MQueryGenerator in - let queries = ref [] in - let confirm query = - if List.mem query ! queries then false - else begin queries := query :: ! queries; default_confirm query end - in - let rec backward level = function - | [] -> () - | term :: tail -> - backward level tail; - try - if Mqint.get_stat () then - print_string ("? " ^ CicPp.ppterm term ^ nl); - let t0 = Sys.time () in - let r = Gen.backward [] [] term level in - let t1 = Sys.time () -. t0 in - let info = Gen.get_query_info () in - let num = List.nth info 0 in - let gen = List.nth info 1 in - if Mqint.get_stat () then - print_string (num ^ " GEN = " ^ gen ^ ":" ^ string_of_float t1 ^ "s" ^ nl); - print_string (Util.text_of_result r nl); - flush stdout - with Gen.Discard -> () - in - Gen.set_confirm_query confirm; - for level = max m n downto min m n do - prerr_endline ("toplevel: backward: trying level " ^ - string_of_int level); - backward level l - done; - prerr_endline ("toplevel: backward: " ^ - string_of_int (List.length ! queries) ^ - " queries issued") - -let prerr_help () = - prerr_endline "\nUSAGE: toplevel.opt OPTIONS < INPUTFILE\n"; - prerr_endline "The tool provides a textual interface to the HELM Query Generator, used for"; - prerr_endline "testing purposes. Toplevel reads its input from stdin and produces ith output"; - prerr_endline "in HTML on stdout. The options can be one ore more of the following.\n"; - prerr_endline "OPTIONS:\n"; - prerr_endline "-h -help shows this help message"; - prerr_endline "-q -show-queries outputs generated queries"; - prerr_endline "-s -stat outputs interpreter statistics"; - prerr_endline "-c -db-check checks the database connection"; - prerr_endline "-r -restricted -nodb enables restricted mode: queries are not issued"; - prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object"; - prerr_endline "-x -execute issues a query given in the input file"; - prerr_endline "-d -disply outputs the CIC terms given in the input file"; - prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file"; - prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias"; - prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms"; - prerr_endline " in the input file"; - prerr_endline "-MB -multi-backward MAX issues the \"Backward\" query for each level from max to 0 on all"; - prerr_endline " CIC terms in the input file\n"; - prerr_endline "NOTES: CIC terms are read with the HELM CIC Textual Parser"; - prerr_endline " -typeof does not work with inductive types and proofs in progress\n" - -let parse_args () = - let rec parse = function - | [] -> () - | ("-h"|"-help") :: rem -> prerr_help () - | ("-d"|"-display") :: rem -> display (get_terms ()) - | ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem - | ("-l"|"-levels") :: rem -> levels (get_terms ()) - | ("-x"|"-execute") :: rem -> execute stdin; parse rem - | ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem - | ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem - | ("-r"|"-restricted"|"-nodb") :: rem -> use_db := false; parse rem - | ("-c"|"-db-check") :: rem -> dbc (); parse rem - | ("-L"|"-locate") :: arg :: rem -> locate arg; parse rem - | ("-B"|"-backward") :: arg :: rem -> - let m = (int_of_string arg) in - mbackward m m (get_terms ()) - | ("-MB"|"-multi-backward") :: arg :: rem -> - let m = (int_of_string arg) in - mbackward m 0 (get_terms ()) - | _ :: rem -> parse rem - in - parse (List.tl (Array.to_list Sys.argv)) - -let _ = - let module Gen = MQueryGenerator in - CicCooking.init () ; - Logger.log_callback := - (Logger.log_to_html - ~print_and_flush:(function s -> print_string s ; flush stdout)) ; - Mqint.set_stat false; - Gen.set_log_file "MQGenLog.htm"; - parse_args (); - if not ! db_down then Mqint.close (); - Gen.set_confirm_query (fun _ -> true); - prerr_endline ("toplevel: done in " ^ string_of_float (Sys.time ()) ^ - " seconds"); - exit 0 diff --git a/helm/ocaml/mathql/.cvsignore b/helm/ocaml/mathql/.cvsignore deleted file mode 100644 index cd9b591e3..000000000 --- a/helm/ocaml/mathql/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend deleted file mode 100644 index 769e30c89..000000000 --- a/helm/ocaml/mathql/.depend +++ /dev/null @@ -1,8 +0,0 @@ -mQueryTParser.cmi: mathQL.cmo -mQueryUtil.cmi: mathQL.cmo -mQueryTParser.cmo: mathQL.cmo mQueryTParser.cmi -mQueryTParser.cmx: mathQL.cmx mQueryTParser.cmi -mQueryTLexer.cmo: mQueryTParser.cmi -mQueryTLexer.cmx: mQueryTParser.cmx -mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi -mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile deleted file mode 100644 index c381b8dc8..000000000 --- a/helm/ocaml/mathql/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -PACKAGE = mathql -REQUIRES = helm-urimanager -PREDICATES = - -INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli - -IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \ - mQueryUtil.ml - -EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \ - mQueryTLexer.mll mQueryTParser.mly - -EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \ - mQueryTLexer.ml - -include ../Makefile.common diff --git a/helm/ocaml/mathql/mQueryHTML.ml b/helm/ocaml/mathql/mQueryHTML.ml deleted file mode 100644 index ff6cb1191..000000000 --- a/helm/ocaml/mathql/mQueryHTML.ml +++ /dev/null @@ -1,21 +0,0 @@ -(* raw HTML representation **************************************************) - -let key s = "" ^ s ^ " " - -let sub s = " " ^ s ^ " " - -let sub2 s = "" ^ s ^ "" - -let sym s = s - -let sep s = s - -let str s = "'" ^ s ^ "'" - -let pat s = "\"" ^ s ^ "\"" - -let res s = "\"" ^ s ^ "\"" - -let nl () = "
\n" - -let par () = "

\n" diff --git a/helm/ocaml/mathql/mQueryTLexer.mll b/helm/ocaml/mathql/mQueryTLexer.mll deleted file mode 100644 index a0884e79d..000000000 --- a/helm/ocaml/mathql/mQueryTLexer.mll +++ /dev/null @@ -1,104 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 23/05/2002 *) -(* *) -(* *) -(******************************************************************************) - -{ - open MQueryTParser -} - -let SPC = [' ' '\t' '\n']+ -let ALPHA = ['A'-'Z' 'a'-'z'] -let NUM = ['0'-'9'] -let IDEN = ALPHA (NUM | ALPHA)* -let QSTR = [^ '"' '\\']+ - -rule comm_token = parse - | "*)" { query_token lexbuf } - | [^ '*']* { comm_token lexbuf } -and string_token = parse - | '"' { DQ } - | '\\' _ { STR (String.sub (Lexing.lexeme lexbuf) 1 1) } - | QSTR { STR (Lexing.lexeme lexbuf) } - | eof { EOF } -and query_token = parse - | "(*" { comm_token lexbuf } - | SPC { query_token lexbuf } - | '"' { STR (qstr string_token lexbuf) } - | '(' { LP } - | ')' { RP } - | '{' { LC } - | '}' { RC } - | '@' { AT } - | '%' { PC } - | '$' { DL } - | '.' { FS } - | ',' { CM } - | '/' { SL } - | "and" { AND } - | "attr" { ATTR } - | "attribute" { ATTRIB } - | "be" { BE } - | "diff" { DIFF } - | "eq" { EQ } - | "ex" { EX } - | "false" { FALSE } - | "fun" { FUN } - | "in" { IN } - | "intersect" { INTER } - | "let" { LET } - | "meet" { MEET } - | "not" { NOT } - | "or" { OR } - | "pattern" { PAT } - | "ref" { REF } - | "refof" { REFOF } - | "relation" { REL } - | "select" { SELECT } - | "sub" { SUB } - | "super" { SUPER } - | "true" { TRUE } - | "union" { UNION } - | "where" { WHERE } - | IDEN { ID (Lexing.lexeme lexbuf) } - | eof { EOF } -and result_token = parse - | SPC { result_token lexbuf } - | '"' { STR (qstr string_token lexbuf) } - | '{' { LC } - | '}' { RC } - | ',' { CM } - | ';' { SC } - | '=' { IS } - | "attr" { ATTR } - | eof { EOF } diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly deleted file mode 100644 index f32a41187..000000000 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ /dev/null @@ -1,189 +0,0 @@ -/* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - */ - -/******************************************************************************/ -/* */ -/* PROJECT HELM */ -/* */ -/* Ferruccio Guidi */ -/* 23/05/2002 */ -/* */ -/* */ -/******************************************************************************/ - -%{ - let analyze x = - let module M = MathQL in - let rec join l1 l2 = match l1, l2 with - | [], _ -> l2 - | _, [] -> l1 - | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 - | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 - | s1 :: tl1, s2 :: tl2 -> s1 :: join tl1 tl2 - in - let rec an_val = function - | M.Const _ -> [] - | M.VVar _ -> [] - | M.Record (rv, _) -> [rv] - | M.Fun (_, x) -> an_val x - | M.Attribute (_, _, x) -> an_val x - | M.RefOf x -> an_set x - and an_boole = function - | M.False -> [] - | M.True -> [] - | M.Ex _ _ -> [] - | M.Not x -> an_boole x - | M.And (x, y) -> join (an_boole x) (an_boole y) - | M.Or (x, y) -> join (an_boole x) (an_boole y) - | M.Sub (x, y) -> join (an_val x) (an_val y) - | M.Meet (x, y) -> join (an_val x) (an_val y) - | M.Eq (x, y) -> join (an_val x) (an_val y) - and an_set = function - | M.SVar _ -> [] - | M.RVar _ -> [] - | M.Relation (_, _, x, _) -> an_set x - | M.Pattern x -> an_val x - | M.Ref x -> an_val x - | M.Union (x, y) -> join (an_set x) (an_set y) - | M.Intersect (x, y) -> join (an_set x) (an_set y) - | M.Diff (x, y) -> join (an_set x) (an_set y) - | M.LetSVar (_, x, y) -> join (an_set x) (an_set y) - | M.LetVVar (_, x, y) -> join (an_val x) (an_set y) - | M.Select (_, x, y) -> join (an_set x) (an_boole y) - in - an_boole x -%} - %token ID STR - %token SL IS LC RC CM SC LP RP AT PC DL FS DQ EOF - %token AND ATTR ATTRIB BE DIFF EQ EX FALSE FUN IN INTER LET MEET NOT OR - %token PAT REF REFOF REL SELECT SUB SUPER TRUE UNION WHERE - %left DIFF WHERE REFOF - %left OR UNION - %left AND INTER - %nonassoc REL - %nonassoc NOT EX IN ATTR - - %start qstr query result - %type qstr - %type query - %type result -%% - qstr: - | DQ { "" } - | STR qstr { $1 ^ $2 } - ; - svar: - | PC ID { $2 } - ; - rvar: - | AT ID { $2 } - ; - vvar: - | DL ID { $2 } - ; - qstr_list: - | STR CM qstr_list { $1 :: $3 } - | STR { [$1] } - ; - vvar_list: - | vvar CM vvar_list { $1 :: $3 } - | vvar { [$1] } - ; - qstr_path: - | STR SL qstr_path { $1 :: $3 } - | STR { [$1] } - ; - ref_op: - | SUB { MathQL.SubOp } - | SUPER { MathQL.SuperOp } - | { MathQL.ExactOp } - ; - val_exp: - | STR { MathQL.Const [$1] } - | FUN STR val_exp { MathQL.Fun ($2, $3) } - | ATTRIB ref_op qstr_path val_exp { MathQL.Attribute ($2, $3, $4) } - | rvar FS vvar { MathQL.Record ($1, $3) } - | vvar { MathQL.VVar $1 } - | LC qstr_list RC { MathQL.Const $2 } - | LC RC { MathQL.Const [] } - | REFOF set_exp { MathQL.RefOf $2 } - | LP val_exp RP { $2 } - ; - boole_exp: - | TRUE { MathQL.True } - | FALSE { MathQL.False } - | LP boole_exp RP { $2 } - | NOT boole_exp { MathQL.Not $2 } - | EX boole_exp { MathQL.Ex (analyze $2) $2 } - | val_exp SUB val_exp { MathQL.Sub ($1, $3) } - | val_exp MEET val_exp { MathQL.Meet ($1, $3) } - | val_exp EQ val_exp { MathQL.Eq ($1, $3) } - | boole_exp AND boole_exp { MathQL.And ($1, $3) } - | boole_exp OR boole_exp { MathQL.Or ($1, $3) } - ; - set_exp: - | REF val_exp { MathQL.Ref $2 } - | PAT val_exp { MathQL.Pattern $2 } - | LP set_exp RP { $2 } - | SELECT rvar IN set_exp WHERE boole_exp { MathQL.Select ($2, $4, $6) } - | REL ref_op qstr_path set_exp ATTR vvar_list { MathQL.Relation ($2, $3, $4, $6) } - | REL ref_op qstr_path set_exp { MathQL.Relation ($2, $3, $4, []) } - | svar { MathQL.SVar $1 } - | rvar { MathQL.RVar $1 } - | set_exp UNION set_exp { MathQL.Union ($1, $3) } - | set_exp INTER set_exp { MathQL.Intersect ($1, $3) } - | set_exp DIFF set_exp { MathQL.Diff ($1, $3) } - | LET svar BE set_exp IN set_exp { MathQL.LetSVar ($2, $4, $6) } - | LET vvar BE val_exp IN set_exp { MathQL.LetVVar ($2, $4, $6) } - ; - query: - | set_exp EOF { $1 } - ; - attribute: - | STR IS qstr_list { ($1, $3) } - | STR { ($1, []) } - ; - attr_list: - | attribute SC attr_list { $1 :: $3 } - | attribute { [$1] } - ; - group: - LC attr_list RC { $2 } - ; - group_list: - | group CM group_list { $1 :: $3 } - | group { [$1] } - ; - resource: - | STR ATTR group_list { ($1, $3) } - | STR { ($1, []) } - ; - resource_list: - | resource SC resource_list { $1 :: $3 } - | resource { [$1] } - | { [] } - ; - result: - | resource_list EOF { $1 } diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml deleted file mode 100644 index ea1829719..000000000 --- a/helm/ocaml/mathql/mQueryUtil.ml +++ /dev/null @@ -1,124 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - - -(* text linearization and parsing *******************************************) - -let rec txt_list f s = function - | [] -> "" - | [a] -> f a - | a :: tail -> f a ^ s ^ txt_list f s tail - -let txt_qstr s = "\"" ^ s ^ "\"" - -let text_of_query x = - let module M = MathQL in - let txt_svar sv = "%" ^ sv in - let txt_rvar rv = "@" ^ rv in - let txt_vvar vv = "$" ^ vv in - let txt_ref = function - | M.ExactOp -> "" - | M.SubOp -> "sub " - | M.SuperOp -> "super " - in - let txt_vvar_list l = - l - in - let rec txt_val = function - | M.Const [s] -> txt_qstr s - | M.Const l -> "{" ^ txt_list txt_qstr ", " l ^ "}" - | M.VVar vv -> txt_vvar vv - | M.Record (rv, vv) -> txt_rvar rv ^ "." ^ txt_vvar vv - | M.Fun (s, x) -> "fun " ^ txt_qstr s ^ " " ^ txt_val x - | M.Attribute (r, p, x) -> "attribute " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_val x - | M.RefOf x -> "refof " ^ txt_set x - and txt_boole = function - | M.False -> "false" - | M.True -> "true" - | M.Ex b x -> "ex " ^ txt_boole x -(* | M.Ex b x -> "ex [" ^ txt_list txt_rvar "," b ^ "] " ^ txt_boole x *) - | M.Not x -> "not " ^ txt_boole x - | M.And (x, y) -> "(" ^ txt_boole x ^ " and " ^ txt_boole y ^ ")" - | M.Or (x, y) -> "(" ^ txt_boole x ^ " or " ^ txt_boole y ^ ")" - | M.Sub (x, y) -> "(" ^ txt_val x ^ " sub " ^ txt_val y ^ ")" - | M.Meet (x, y) -> "(" ^ txt_val x ^ " meet " ^ txt_val y ^ ")" - | M.Eq (x, y) -> "(" ^ txt_val x ^ " eq " ^ txt_val y ^ ")" - and txt_set = function - | M.SVar sv -> txt_svar sv - | M.RVar rv -> txt_rvar rv - | M.Relation (r, p, x, []) -> "relation " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_set x - | M.Relation (r, p, x, l) -> "relation " ^ txt_ref r ^ txt_list txt_qstr "/" p ^ " " ^ txt_set x ^ " attr " ^ txt_list txt_vvar ", " l - | M.Union (x, y) -> "(" ^ txt_set x ^ " union " ^ txt_set y ^ ")" - | M.Intersect (x, y) -> "(" ^ txt_set x ^ " intersect " ^ txt_set y ^ ")" - | M.Diff (x, y) -> "(" ^ txt_set x ^ " diff " ^ txt_set y ^ ")" - | M.LetSVar (sv, x, y) -> "let " ^ txt_svar sv ^ " be " ^ txt_set x ^ " in " ^ txt_set y - | M.LetVVar (vv, x, y) -> "let " ^ txt_vvar vv ^ " be " ^ txt_val x ^ " in " ^ txt_set y - | M.Select (rv, x, y) -> "select " ^ txt_rvar rv ^ " in " ^ txt_set x ^ " where " ^ txt_boole y - | M.Pattern x -> "pattern " ^ txt_val x - | M.Ref x -> "ref " ^ txt_val x - in - txt_set x - -let text_of_result x sep = - let txt_attr = function - | (s, []) -> txt_qstr s - | (s, l) -> txt_qstr s ^ "=" ^ txt_list txt_qstr ", " l - in - let txt_group l = "{" ^ txt_list txt_attr "; " l ^ "}" in - let txt_res = function - | (s, []) -> txt_qstr s - | (s, l) -> txt_qstr s ^ " attr " ^ txt_list txt_group ", " l - in - let txt_set l = txt_list txt_res ("; " ^ sep) l ^ sep in - txt_set x - -let query_of_text lexbuf = - MQueryTParser.query MQueryTLexer.query_token lexbuf - -let result_of_text lexbuf = - MQueryTParser.result MQueryTLexer.result_token lexbuf - -(* conversion functions *****************************************************) - -type uriref = UriManager.uri * (int list) - -let string_of_uriref (uri, fi) = - let module UM = UriManager in - let str = UM.string_of_uri uri in - let xp t = "#xpointer(1/" ^ string_of_int (t + 1) in - match fi with - | [] -> str - | [t] -> str ^ xp t ^ ")" - | t :: c :: _ -> str ^ xp t ^ "/" ^ string_of_int c ^ ")" diff --git a/helm/ocaml/mathql/mQueryUtil.mli b/helm/ocaml/mathql/mQueryUtil.mli deleted file mode 100644 index 9881b3b54..000000000 --- a/helm/ocaml/mathql/mQueryUtil.mli +++ /dev/null @@ -1,49 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* 30/04/2002 *) -(* *) -(* *) -(******************************************************************************) - - -val text_of_query : MathQL.query -> string - -val text_of_result : MathQL.result -> string -> string - -val query_of_text : Lexing.lexbuf -> MathQL.query - -val result_of_text : Lexing.lexbuf -> MathQL.result - - -type uriref = UriManager.uri * (int list) - -val string_of_uriref : uriref -> string - diff --git a/helm/ocaml/mathql/mathQL.ml b/helm/ocaml/mathql/mathQL.ml deleted file mode 100644 index d375d92af..000000000 --- a/helm/ocaml/mathql/mathQL.ml +++ /dev/null @@ -1,100 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://www.cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Ferruccio Guidi *) -(* Irene Schena *) -(* 10/09/2002 *) -(* *) -(* *) -(******************************************************************************) - - -(* input data structures ****************************************************) - -type svar = string (* the name of a variable for a resource set *) - -type rvar = string (* the name of a variable for a resource *) - -type vvar = string (* the name of a variable for an attribute value *) - -type refine_op = ExactOp - | SubOp - | SuperOp - -type path = string list - -type vvar_list = vvar list - -type set_exp = SVar of svar - | RVar of rvar - | Ref of val_exp - | Pattern of val_exp - | Relation of refine_op * path * set_exp * vvar_list - | Select of rvar * set_exp * boole_exp - | Union of set_exp * set_exp - | Intersect of set_exp * set_exp - | Diff of set_exp * set_exp - | LetSVar of svar * set_exp * set_exp - | LetVVar of vvar * val_exp * set_exp - -and boole_exp = False - | True - | Not of boole_exp - | Ex of rvar list * boole_exp - | And of boole_exp * boole_exp - | Or of boole_exp * boole_exp - | Sub of val_exp * val_exp - | Meet of val_exp * val_exp - | Eq of val_exp * val_exp - -and val_exp = Const of string list - | RefOf of set_exp - | Record of rvar * vvar - | VVar of vvar - | Fun of string * val_exp - | Attribute of refine_op * path * val_exp - -type query = set_exp - - -(* output data structures ***************************************************) - -type value = string list (* the value of an attribute *) - -type attribute = string * value (* an attribute *) - -type attribute_group = attribute list (* a group of attributes *) - -type attribute_set = attribute_group list (* the attributes of an URI *) - -type resource = string * attribute_set (* an attributed URI *) - -type resource_set = resource list (* the query result *) - -type result = resource_set