From: no author Date: Thu, 17 Oct 2002 15:02:52 +0000 (+0000) Subject: This commit was manufactured by cvs2svn to create tag X-Git-Tag: new_mathql_before_first_merge X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=de211e50e79877a910eb85a63e47105108a7173d;p=helm.git This commit was manufactured by cvs2svn to create tag 'new_mathql_before_first_merge'. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml new file mode 100644 index 000000000..2b476a674 --- /dev/null +++ b/helm/gTopLevel/gTopLevel.ml @@ -0,0 +1,1561 @@ +(* 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 = "/public/sacerdot/currentproof";; +(*CSC: the getter should handle the innertypes, not the FS *) +let innertypesfile = "/public/sacerdot/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 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 = "/projects/helm/V7/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 ^ "

") ; +;; + +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 + output_html outputhtml ( + try + match Str.split (Str.regexp "[ \t]+") input with + | [] -> "" + | head :: tail -> + inputt#delete_text 0 inputlen; + MQueryGenerator.locate_html head + with + e -> "

" ^ 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 + let result = + match !ProofEngine.goal with + | None -> "" + | Some metano -> + let (_, ey ,ty) = + List.find (function (m,_,_) -> m=metano) metasenv + in + MQueryGenerator.backward metasenv ey ty level + in + output_html outputhtml result +;; + +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 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(introsb#connect#clicked (intros self)) ; + Logger.log_callback := + (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) +end;; + +(* MAIN *) + +let initialize_everything () = + let module U = Unix in + let output = GMathView.math_view ~width:400 ~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#show () ; + GMain.Main.main () +;; + +let _ = + CicCooking.init () ; + if !usedb then + begin + MQueryGenerator.init () ; + CicTextualParser0.set_locate_object + (function id -> + let MathQL.MQRefs uris = MQueryGenerator.locate id in + let uri = + match uris with + [] -> + (GToolbox.input_string ~title:"Unknown input" + ("No URI matching \"" ^ id ^ "\" found. Please enter its 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/topLevel/.depend b/helm/gTopLevel/topLevel/.depend deleted file mode 100644 index e69de29bb..000000000 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/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 diff --git a/helm/ocaml/mathql_interpreter/.cvsignore b/helm/ocaml/mathql_interpreter/.cvsignore deleted file mode 100644 index 6b3eba302..000000000 --- a/helm/ocaml/mathql_interpreter/.cvsignore +++ /dev/null @@ -1 +0,0 @@ -*.cm[iaox] *.cmxa diff --git a/helm/ocaml/mathql_interpreter/.depend b/helm/ocaml/mathql_interpreter/.depend deleted file mode 100644 index 8106a0f5e..000000000 --- a/helm/ocaml/mathql_interpreter/.depend +++ /dev/null @@ -1,20 +0,0 @@ -dbconn.cmo: dbconn.cmi -dbconn.cmx: dbconn.cmi -utility.cmo: dbconn.cmi utility.cmi -utility.cmx: dbconn.cmx utility.cmi -union.cmo: union.cmi -union.cmx: union.cmi -relation.cmo: dbconn.cmi union.cmi utility.cmi relation.cmi -relation.cmx: dbconn.cmx union.cmx utility.cmx relation.cmi -diff.cmo: diff.cmi -diff.cmx: diff.cmi -meet.cmo: meet.cmi -meet.cmx: meet.cmi -sub.cmo: sub.cmi -sub.cmx: sub.cmi -intersect.cmo: intersect.cmi -intersect.cmx: intersect.cmi -mqint.cmo: context.cmo dbconn.cmi diff.cmi intersect.cmi meet.cmi \ - relation.cmi sub.cmi union.cmi mqint.cmi -mqint.cmx: context.cmx dbconn.cmx diff.cmx intersect.cmx meet.cmx \ - relation.cmx sub.cmx union.cmx mqint.cmi diff --git a/helm/ocaml/mathql_interpreter/Makefile b/helm/ocaml/mathql_interpreter/Makefile deleted file mode 100644 index 7a45ecdf2..000000000 --- a/helm/ocaml/mathql_interpreter/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -PACKAGE = mathql_interpreter -REQUIRES = helm-urimanager postgres unix helm-mathql -PREDICATES = - -INTERFACE_FILES = dbconn.mli utility.mli union.mli relation.mli diff.mli meet.mli sub.mli intersect.mli mqint.mli - -IMPLEMENTATION_FILES = dbconn.ml utility.ml union.ml relation.ml diff.ml meet.ml sub.ml intersect.ml context.ml mqint.ml - -# $(INTERFACE_FILES:%.mli=%.ml) - -EXTRA_OBJECTS_TO_INSTALL = context.ml - -EXTRA_OBJECTS_TO_CLEAN = - -include ../Makefile.common diff --git a/helm/ocaml/mathql_interpreter/context.ml b/helm/ocaml/mathql_interpreter/context.ml deleted file mode 100644 index c9431d1af..000000000 --- a/helm/ocaml/mathql_interpreter/context.ml +++ /dev/null @@ -1,30 +0,0 @@ -(* contexts *****************************************************************) - -type svar_context = (MathQL.svar * MathQL.resource_set) list - -type rvar_context = (MathQL.rvar * MathQL.resource) list - -type group_context = (MathQL.rvar * MathQL.attribute_group) list - -type vvar_context = (MathQL.vvar * MathQL.value) list - - -type context = {svars: svar_context; (* contesto delle svar *) - rvars: rvar_context; (* contesto delle rvar *) - groups: group_context; (* contesto dei gruppi *) - vvars: vvar_context (* contesto delle vvar introdotte con let-in *) - } - -let upd_svars c s = - {svars = s; rvars = c.rvars; groups = c.groups; vvars = c.vvars} - -let upd_rvars c s = - {svars = c.svars; rvars = s; groups = c.groups; vvars = c.vvars} - -let upd_groups c s = - {svars = c.svars; rvars = c.rvars; groups = s; vvars = c.vvars} - -let upd_vvars c s = - {svars = c.svars; rvars = c.rvars; groups = c.groups; vvars = s} - - diff --git a/helm/ocaml/mathql_interpreter/dbconn.ml b/helm/ocaml/mathql_interpreter/dbconn.ml deleted file mode 100644 index b38eabe87..000000000 --- a/helm/ocaml/mathql_interpreter/dbconn.ml +++ /dev/null @@ -1,74 +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/. - *) - -(* - * gestione della connessione al database - *) - -(* - * le eccezioni lanciate dalle funzioni init e pgc sono - * definite nel modulo Mathql - *) -open MathQL;; - -exception InvalidURI of string -exception ConnectionFailed of string -exception InvalidConnection - -(* - * connessione al db - *) -let conn = ref None - -(* - * controllo sulla connessione - *) -let pgc () = - match !conn with - None -> raise InvalidConnection - | Some c -> c -;; - -(* - * inizializzazione della connessione - * - * TODO - * passare i parametri della connessione come argomento di init - *) -let init connection_param = - try ( - conn := Some (new Postgres.connection connection_param); - ) with - _ -> raise (ConnectionFailed ("init: " ^ connection_param)) -;; - -(* - * chiusura della connessione - *) -let close () = - match !conn with - None -> () - | Some c -> c#close -;; diff --git a/helm/ocaml/mathql_interpreter/dbconn.mli b/helm/ocaml/mathql_interpreter/dbconn.mli deleted file mode 100644 index ecfbcd66a..000000000 --- a/helm/ocaml/mathql_interpreter/dbconn.mli +++ /dev/null @@ -1,28 +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/. - *) - -val pgc : unit -> Postgres.connection -val init : string -> unit -val close : unit -> unit diff --git a/helm/ocaml/mathql_interpreter/diff.ml b/helm/ocaml/mathql_interpreter/diff.ml deleted file mode 100644 index b4e09196e..000000000 --- a/helm/ocaml/mathql_interpreter/diff.ml +++ /dev/null @@ -1,98 +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/. - *) - -(* - * vecchia implementazione del comando DIFF - - -exception NotCompatible;; - -(* intersect_attributes is successful iff there is no attribute with *) -(* two different values in the two lists. The returned list is the *) -(* union of the two lists. *) -let rec intersect_attributes (attr1, attr2) = - match attr1, attr2 with - [],_ -> attr2 - | _,[] -> attr1 - | (key1,value1)::tl1, (key2,_)::_ when key1 < key2 -> - (key1,value1)::(intersect_attributes (tl1,attr2)) - | (key1,_)::_, (key2,value2)::tl2 when key2 < key1 -> - (key2,value2)::(intersect_attributes (attr1,tl2)) - | entry1::tl1, entry2::tl2 when entry1 = entry2 -> - entry1::(intersect_attributes (tl1,tl2)) - | _, _ -> raise NotCompatible (* same keys, different values *) -;; - - -let rec diff_ex l1 l2 = - let module S = Mathql_semantics in - match (l1, l2) with - [],_ -> [] - | l,[] -> l - | {S.uri = uri1}::_, {S.uri = uri2}::tl2 when uri2 < uri1 -> - (diff_ex l1 tl2) - | {S.uri = uri1 ; S.attributes = attributes1}::tl1, - {S.uri = uri2}::_ when uri1 < uri2 -> - {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 l2) - | {S.uri = uri1 ; S.attributes = attributes1}::tl1, - {S.uri = uri2 ; S.attributes = attributes2}::tl2 -> - try - let attributes' = intersect_attributes (attributes1, attributes2) in - diff_ex tl1 tl2 - with - NotCompatible -> - {S.uri = uri1 ; S.attributes = attributes1 ; S.extra = ""}::(diff_ex tl1 tl2) -;; -*) - -(* - * implementazione del comando DIFF - *) -let rec diff_ex rs1 rs2 = - match (rs1, rs2) with - [],_ -> [] - | l,[] -> l - | (uri1,l)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l)::(diff_ex tl1 rs2) - | (uri1,_)::_,(uri2,_)::tl2 when uri2 < uri1 -> (diff_ex rs1 tl2) - | (uri1,_)::tl1, (uri2,_)::tl2 -> (diff_ex tl1 tl2) -;; - - - - -let diff_ex l1 l2 = - let before = Sys.time () in - let res = diff_ex l1 l2 in - let after = Sys.time () in - let ll1 = string_of_int (List.length l1) in - let ll2 = string_of_int (List.length l2) in - let diff = string_of_float (after -. before) in - print_endline - ("DIFF(" ^ ll1 ^ ", " ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ - ": " ^ diff ^ "s") ; - flush stdout ; - res -;; - diff --git a/helm/ocaml/mathql_interpreter/diff.mli b/helm/ocaml/mathql_interpreter/diff.mli deleted file mode 100644 index 1cd9cf4de..000000000 --- a/helm/ocaml/mathql_interpreter/diff.mli +++ /dev/null @@ -1,27 +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/. - *) - -val diff_ex : - MathQL.resource_set -> MathQL.resource_set -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/eval.ml b/helm/ocaml/mathql_interpreter/eval.ml deleted file mode 100644 index 43296cd07..000000000 --- a/helm/ocaml/mathql_interpreter/eval.ml +++ /dev/null @@ -1,98 +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/. - *) - -(* - * - *) - -open MathQL;; - -(* - * conversione di un pattern - *) -let rec patterneval p = - match p with - [] -> "" - | head::tail -> - let h = match head with - MQBC s -> Str.global_replace (Str.regexp "\.") "\\\\\." s - | MQBD -> "/" - | MQBQ -> "[^/#]?" - | MQBS -> "[^/#]*" - | MQBSS -> "[^#]*" - in - h ^ (patterneval tail) -;; - -let rec fieval fi = - match fi with - [] -> "" - | MQFC i :: tail -> "/" ^ (string_of_int i) ^ (fieval tail) - | MQFS :: tail -> "[^/]*" ^ (fieval tail) - | MQFSS :: tail -> ".*" ^ (fieval tail) -;; - -(* - * conversione di un fragment identifier - *) -let fieval fi = - if fi = [] then - "" - else - "#xpointer\\\$1" ^ fieval fi ^ "\\\$" -;; - -(* - * valuta l'estensione - * - * 20/05/2002: non piu' necessario: l'estensione fa eventualmente - * parte del pattern precedente - *) -let exteval ext = - match ext with - "" -> "" - | _ -> ("\." ^ ext) -;; - -(* - * valuta il preambolo - *) -let preeval p = - match p with - Some s -> s - | None -> "[^/]*" -;; - -(* - * trasforma un pattern MathQL in un pattern postgresql - * - * si utilizzano espressioni regolari POSIX anziche' l'operatore - * SQL standard LIKE perche' MathQL prevede esperssioni con "*" - * e con "**". - *) -let pattern_match (preamble, pattern, fragid) = - " ~ '^" ^ (preeval preamble) ^ ":/" ^ (patterneval pattern) ^ (fieval fragid) ^ "$'" -;; - diff --git a/helm/ocaml/mathql_interpreter/eval.mli b/helm/ocaml/mathql_interpreter/eval.mli deleted file mode 100644 index 00b64ed95..000000000 --- a/helm/ocaml/mathql_interpreter/eval.mli +++ /dev/null @@ -1,27 +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/. - *) - -val pattern_match : - MathQL.mqtref -> string diff --git a/helm/ocaml/mathql_interpreter/func.ml b/helm/ocaml/mathql_interpreter/func.ml deleted file mode 100644 index 857a4c698..000000000 --- a/helm/ocaml/mathql_interpreter/func.ml +++ /dev/null @@ -1,93 +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/. - *) - -(* - * - *) - -open Dbconn;; -open Utility;; -open MathQL;; - -(* - * implementazione della funzione NAME - * - * esempio: - * name "cic:/Algebra/CC_Props/CC_CauchySeq.ind#xpointer(1/1/1)" = CC_CauchySeq - *) -let func_name value = - try ( - let i = Str.search_forward (Str.regexp "[^/]*\.") value 0 in - let s = Str.matched_string value in - let retVal = Str.string_before s ((String.length s) - 1) in - retVal - ) with - Not_found -> "" -;; - -(* - * - *) -let func_theory value = - "" -;; - -(* - * implementazione delle funzioni dublin core - *) -let func_dc (value, name) = - let c = pgc () - and p = helm_property_id name in - pgresult_to_string (c#exec ("select t" ^ p ^ ".att1 from t" ^ p ^ " where " ^ "t" ^ p ^ ".att0 = '" ^ value ^ "'")) -;; - -(* - * - *) -let apply_func f value = - match f with - MQName -> func_name value - | MQTheory -> func_theory value - | MQTitle -> func_dc (value, "title") - | MQContributor -> func_dc (value, "contributor") - | MQCreator -> func_dc (value, "creator") - | MQPublisher -> func_dc (value, "publisher") - | MQSubject -> func_dc (value, "subject") - | MQDescription -> func_dc (value, "description") - | MQDate -> func_dc (value, "date") - | MQType -> func_dc (value, "type") - | MQFormat -> func_dc (value, "format") - | MQIdentifier -> func_dc (value, "identifier") - | MQLanguage -> func_dc (value, "language") - | MQRelation -> func_dc (value, "relation") - | MQSource -> func_dc (value, "source") - | MQCoverage -> func_dc (value, "coverage") - | MQRights -> func_dc (value, "rights") - | MQInstitution -> func_dc (value, "institution") - | MQContact -> func_dc (value, "contact") - | MQFirstVersion -> func_dc (value, "firstversion") - | MQModified -> func_dc (value, "modified") -;; - diff --git a/helm/ocaml/mathql_interpreter/func.mli b/helm/ocaml/mathql_interpreter/func.mli deleted file mode 100644 index fb68df82a..000000000 --- a/helm/ocaml/mathql_interpreter/func.mli +++ /dev/null @@ -1,26 +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/. - *) - -val apply_func: MathQL.mqfunc -> string -> string diff --git a/helm/ocaml/mathql_interpreter/intersect.ml b/helm/ocaml/mathql_interpreter/intersect.ml deleted file mode 100644 index 73bebaa50..000000000 --- a/helm/ocaml/mathql_interpreter/intersect.ml +++ /dev/null @@ -1,75 +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/. - *) - - -(* Catenates two lists preserving order and getting rid of duplicates *) -let rec append (l1,l2) = - match l1,l2 with - [],_ -> l2 - | _,[] -> l1 - | s1::tl1, s2::_ when s1 < s2 -> s1::append (tl1,l2) - | s1::_, s2::tl2 when s2 < s1 -> s2::append (l1,tl2) - | s1::tl1, s2::tl2 -> s1::append (tl1,tl2) - -;; - - -(* Sums two attribute groups preserving order *) -let rec sum_groups(gr1, gr2) = - match gr1, gr2 with - [],_ -> gr2 - | _,[] -> gr1 - | gr1, gr2 when gr1 = gr2 -> gr1 - | (key1,l1)::tl1, (key2,l2)::_ when key1 < key2 -> (key1,l1)::(sum_groups (tl1,gr2)) - | (key1,l1)::_, (key2,l2)::tl2 when key2 < key1 -> (key2,l2)::(sum_groups (gr1,tl2)) - | (key1,l1)::tl1, (key2,l2)::tl2 -> (key1,(append (l1,l2)))::(sum_groups (tl1,tl2)) - -;; - -(* Product between an attribute set and a group of attributes *) -let rec sub_prod (aset, gr) = (*prende un aset e un gr, fa la somma tra tutti i gruppi di aset e gr*) - match aset with - [] -> [] - | gr1::tl1 -> sum_groups (gr1, gr)::(sub_prod(tl1, gr)) -;; - - -(* Cartesian product between two attribute sets*) -let rec prod (as1, as2) = - match as1, as2 with - [],_ -> [] - | _,[] -> [] - | gr1::tl1, _ -> append((sub_prod (as2, gr1)), (prod (tl1, as2))) (* chiamo la sub_prod con un el. as1 e as2 *) -;; - -(* Intersection between two resource sets, preserves order and gets rid of duplicates *) -let rec intersect_ex rs1 rs2 = - match (rs1, rs2) with - [],_ - | _,[] -> [] - | (uri1,_)::tl1, (uri2,_)::_ when uri1 < uri2 -> intersect_ex tl1 rs2 - | (uri1,_)::_, (uri2,_)::tl2 when uri2 < uri1 -> intersect_ex rs1 tl2 - | (uri1,as1)::tl1, (uri2,as2)::tl2 -> (uri1, prod(as1,as2))::intersect_ex tl1 tl2 -;; diff --git a/helm/ocaml/mathql_interpreter/intersect.mli b/helm/ocaml/mathql_interpreter/intersect.mli deleted file mode 100644 index 956a05922..000000000 --- a/helm/ocaml/mathql_interpreter/intersect.mli +++ /dev/null @@ -1,27 +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/. - *) - -val intersect_ex : - MathQL.result -> MathQL.result -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/letin.ml b/helm/ocaml/mathql_interpreter/letin.ml deleted file mode 100644 index 160a7a164..000000000 --- a/helm/ocaml/mathql_interpreter/letin.ml +++ /dev/null @@ -1,65 +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/. - *) - -(* - * implementazione dei comandi LETIN e REF - *) - -open MathQL;; - -let letin_pool = ref None;; - -let see_pool () = - match !letin_pool with - None -> print_endline "None" - | Some c -> List.iter (fun elem -> print_endline (fst elem)) c -;; - -let letin_ex rvar alist = - let _ = - match !letin_pool with - Some pool -> letin_pool := Some ((rvar,alist)::(List.remove_assoc rvar pool)) - | None -> letin_pool := Some ([(rvar,alist)]) - in -(* let _ = see_pool () in*) - [] -;; - -let letref_ex rvar = - match !letin_pool with - None -> [] - | Some pool -> - ( - try - List.assoc rvar pool - with - Not_found -> [] - ) -;; - -let letdispose () = - let _ = letin_pool = ref None in () -;; - diff --git a/helm/ocaml/mathql_interpreter/letin.mli b/helm/ocaml/mathql_interpreter/letin.mli deleted file mode 100644 index d221ddd2e..000000000 --- a/helm/ocaml/mathql_interpreter/letin.mli +++ /dev/null @@ -1,28 +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/. - *) - -val letin_ex : MathQL.mqlvar -> Mathql_semantics.result -> Mathql_semantics.result -val letref_ex : MathQL.mqlvar -> Mathql_semantics.result -val letdispose : unit -> unit diff --git a/helm/ocaml/mathql_interpreter/mathql_semantics.ml b/helm/ocaml/mathql_interpreter/mathql_semantics.ml deleted file mode 100644 index 49896a220..000000000 --- a/helm/ocaml/mathql_interpreter/mathql_semantics.ml +++ /dev/null @@ -1,34 +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/. - *) - -(* attributes are sorted w.r.t. their name in increasing order *) -type attributed_uri = - { uri: string ; attributes : (MathQL.mqsvar * string) list ; extra : string} - -type attributed_uri_env = - (MathQL.mqrvar * attributed_uri) list - -(* invariant: the result is ordered on the uri component of every item *) -type result = attributed_uri list diff --git a/helm/ocaml/mathql_interpreter/meet.ml b/helm/ocaml/mathql_interpreter/meet.ml deleted file mode 100644 index bf0b5d780..000000000 --- a/helm/ocaml/mathql_interpreter/meet.ml +++ /dev/null @@ -1,34 +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/. - *) - - -let rec meet_ex v1 v2 = - match v1,v2 with - [],_ - | _,[] -> false - | s1::tl1, s2::_ when s1 < s2 -> meet_ex tl1 v2 - | s1::_, s2::tl2 when s2 < s1 -> meet_ex v1 tl2 - | _, _ -> true -;; diff --git a/helm/ocaml/mathql_interpreter/meet.mli b/helm/ocaml/mathql_interpreter/meet.mli deleted file mode 100644 index 366abd7fd..000000000 --- a/helm/ocaml/mathql_interpreter/meet.mli +++ /dev/null @@ -1,27 +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/. - *) - - -val meet_ex: MathQL.value -> MathQL.value -> bool diff --git a/helm/ocaml/mathql_interpreter/mqint.ml b/helm/ocaml/mathql_interpreter/mqint.ml deleted file mode 100644 index c45f9dee8..000000000 --- a/helm/ocaml/mathql_interpreter/mqint.ml +++ /dev/null @@ -1,190 +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/. - *) - - - - -(* - * implementazione del'interprete MathQL - *) - - - - -open Dbconn;; -open Union;; -open Intersect;; -open Meet;; -open Sub;; -open Context;; -open Diff;; -open Relation;; - - -let init connection_param = Dbconn.init connection_param - -let close () = Dbconn.close () - -let check () = Dbconn.pgc () - -exception BooleExpTrue - -let stat = ref false - -let set_stat b = stat := b - -let get_stat () = ! stat - -(* valuta una MathQL.set_exp e ritorna un MathQL.resource_set *) - -let rec exec_set_exp c = function - |MathQL.SVar svar -> List.assoc svar c.svars - |MathQL.RVar rvar -> [List.assoc rvar c.rvars] - | MathQL.Ref vexp -> List.map (fun s -> (s,[])) (exec_val_exp c vexp) - | MathQL.Intersect (sexp1, sexp2) -> - let before = Sys.time() in - let rs1 = exec_set_exp c sexp1 in - let rs2 = exec_set_exp c sexp2 in - let res = intersect_ex rs1 rs2 in - let after = Sys.time() in - let ll1 = string_of_int (List.length rs1) in - let ll2 = string_of_int (List.length rs2) in - let diff = string_of_float (after -. before) in - if !stat then - (print_endline("INTERSECT(" ^ ll1 ^ "," ^ ll2 ^ ") = " ^ string_of_int (List.length res) ^ - ": " ^ diff ^ "s"); - flush stdout); - res - | MathQL.Union (sexp1, sexp2) -> - let before = Sys.time () in - let res = union_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) in - let after = Sys.time() in - let diff = string_of_float (after -. before) in - if !stat then - (print_endline ("UNION: " ^ diff ^ "s"); - flush stdout); - res - | MathQL.LetSVar (svar, sexp1, sexp2) -> - let before = Sys.time() in - let c1 = upd_svars c ((svar, exec_set_exp c sexp1) :: c.svars) in - let res = exec_set_exp c1 sexp2 in - if !stat then - (print_string ("LETIN " ^ svar ^ " = " ^ string_of_int (List.length res) ^ ": "); - print_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.LetVVar (vvar, vexp, sexp) -> - let before = Sys.time() in - let c1 = upd_vvars c ((vvar, exec_val_exp c vexp) :: c.vvars) in - let res = exec_set_exp c1 sexp in - if !stat then - (print_string ("LETIN " ^ vvar ^ " = " ^ string_of_int (List.length res) ^ ": "); - print_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.Relation (rop, path, sexp, attl) -> - let before = Sys.time() in - let res = relation_ex rop path (exec_set_exp c sexp) attl in - if !stat then - (print_string ("RELATION " ^ (List.hd path) ^ " = " ^ string_of_int(List.length res) ^ ": "); - print_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.Select (rvar, sexp, bexp) -> - let before = Sys.time() in - let rset = (exec_set_exp c sexp) in - let rec select_ex rset = - match rset with - [] -> [] - | r::tl -> let c1 = upd_rvars c ((rvar,r)::c.rvars) in - if (exec_boole_exp c1 bexp) then r::(select_ex tl) - else select_ex tl - in - let res = select_ex rset in - if !stat then - (print_string ("SELECT " ^ rvar ^ " = " ^ string_of_int (List.length res) ^ ": "); - print_endline (string_of_float (Sys.time() -. before) ^ "s"); - flush stdout); - res - | MathQL.Diff (sexp1, sexp2) -> diff_ex (exec_set_exp c sexp1) (exec_set_exp c sexp2) - | _ -> assert false - -(* valuta una MathQL.boole_exp e ritorna un boole *) - -and exec_boole_exp c = function - | MathQL.False -> false - | MathQL.True -> true - | MathQL.Not x -> not (exec_boole_exp c x) - | MathQL.And (x, y) -> (exec_boole_exp c x) && (exec_boole_exp c y) - | MathQL.Or (x, y) -> (exec_boole_exp c x) || (exec_boole_exp c y) - | MathQL.Sub (vexp1, vexp2) -> sub_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) - | MathQL.Meet (vexp1, vexp2) -> meet_ex (exec_val_exp c vexp1) (exec_val_exp c vexp2) - | MathQL.Eq (vexp1, vexp2) -> (exec_val_exp c vexp1) = (exec_val_exp c vexp2) - | MathQL.Ex l bexp -> - if l = [] then (exec_boole_exp c bexp) - else - let latt = List.map (fun uri -> - let (r,attl) = List.assoc uri c.rvars in (uri,attl)) l (*latt = l + attributi*) - in - try - let rec prod c = function - [] -> if (exec_boole_exp c bexp) then raise BooleExpTrue - | (uri,attl)::tail1 -> let rec sub_prod attl = - match attl with -(*per ogni el. di attl *) [] -> () -(*devo andare in ric. su tail1*) | att::tail2 -> let c1 = upd_groups c ((uri,att)::c.groups) in - prod c1 tail1; sub_prod tail2 - in - sub_prod attl - in - prod c latt; false - with BooleExpTrue -> true - -(* valuta una MathQL.val_exp e ritorna un MathQL.value *) - -and exec_val_exp c = function - | MathQL.Const x -> let - ol = List.sort compare x in - let rec edup = function - - [] -> [] - | s::tl -> if tl <> [] then - if s = (List.hd tl) then edup tl - else s::(edup tl) - else s::[] - in - edup ol - | MathQL.Record (rvar, vvar) -> List.assoc vvar (List.assoc rvar c.groups) - - | MathQL.VVar s -> List.assoc s c.vvars - | MathQL.RefOf sexp -> List.map (fun (s,_) -> s) (exec_set_exp c sexp) - - | _ -> assert false - - -(* valuta una MathQL.set_exp nel contesto vuoto e ritorna un MathQL.resource_set *) - -and execute x = - exec_set_exp {svars = []; rvars = []; groups = []; vvars = []} x diff --git a/helm/ocaml/mathql_interpreter/mqint.mli b/helm/ocaml/mathql_interpreter/mqint.mli deleted file mode 100644 index e969e5c66..000000000 --- a/helm/ocaml/mathql_interpreter/mqint.mli +++ /dev/null @@ -1,36 +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/. - *) - -val init : string -> unit (* open database *) - -val execute : MathQL.query -> MathQL.result (* execute query *) - -val close : unit -> unit (* close database *) - -val check : unit -> Postgres.connection (* check connection *) - -val set_stat : bool -> unit (* set stat emission *) - -val get_stat : unit -> bool (* check stat emission *) diff --git a/helm/ocaml/mathql_interpreter/pattern.ml b/helm/ocaml/mathql_interpreter/pattern.ml deleted file mode 100644 index 993617bb8..000000000 --- a/helm/ocaml/mathql_interpreter/pattern.ml +++ /dev/null @@ -1,60 +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/. - *) - -(* - * implementazione del comando PATTERN - *) - -open Dbconn;; -open Utility;; -open Eval;; -open Mathql_semantics;; - -let pattern_ex (apreamble, apattern, afragid) = - let c = pgc () in - (*let _ = print_string ("USE ") - and t = Sys.time () in*) - (*let r1 = helm_class_id "MathResource" in*) - (*let qq = "select att0 from t" ^ r1 ^ " where att0 " ^ (pattern_match apreamble apattern afragid) ^ " order by t" ^ r1 ^ ".att0 asc" in*) - (*PRE-CLAUDIO - let qq = "select uri from registry where uri " ^ (pattern_match apreamble apattern afragid) ^ " order by registry.uri asc" in - let result = - let res = - c#exec (qq) - in - [["retVal"]] @ List.map (fun l -> [l]) (pgresult_to_string_list res)*) - let qq = "select uri from registry where uri " ^ (pattern_match (apreamble, apattern, afragid)) ^ " order by registry.uri asc" in -print_endline qq ; flush stderr ; - (*let _ = print_endline qq in*) - let res = - c#exec (qq) - in -(* PRE-CLAUDIO - (*let _ = print_endline (string_of_float (Sys.time () -. t)); flush stdout in*) - result*) - List.map - (function uri -> {uri = uri ; attributes = [] ; extra = ""}) - (pgresult_to_string_list res) -;; diff --git a/helm/ocaml/mathql_interpreter/pattern.mli b/helm/ocaml/mathql_interpreter/pattern.mli deleted file mode 100644 index 1fd21bdba..000000000 --- a/helm/ocaml/mathql_interpreter/pattern.mli +++ /dev/null @@ -1,28 +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/. - *) - -val pattern_ex : - MathQL.mqtref -> - Mathql_semantics.result diff --git a/helm/ocaml/mathql_interpreter/relation.ml b/helm/ocaml/mathql_interpreter/relation.ml deleted file mode 100644 index 159369ad2..000000000 --- a/helm/ocaml/mathql_interpreter/relation.ml +++ /dev/null @@ -1,76 +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/. - *) - - -(* - * implementazione del comando Relation - *) - - - - -open Union;; -open Dbconn;; -open Utility;; - - - - -let get_prop_id propl = - let prop = List.hd propl in - if prop="refObj" then "F" - else if prop="backPointer" then "B" - else assert false -;; - - -let relation_ex rop path rset attl = - if path = [] then [] - else - let usek = get_prop_id path in - let vvar = if attl = [] then "position" - else List.hd attl - in - let c = pgc () in - let rset_list = (* lista di singoletti:resource_set di un elemento *) - (List.fold_left (fun acc (uri,l) -> - let tv = pgresult_to_string (c#exec ("select id from registry where uri='" ^ uri ^ "'")) in - let qq = "select uri, context from t" ^ tv ^ " where prop_id='" ^ usek ^ "' order by uri asc" in - let res = c#exec qq in - (List.map - (function - [uri;context] -> [(uri,[[(vvar,[context])]])] - | _ -> assert false ) - res#get_list) @ acc - ) - [] rset - ) - in - let rec edup = function - [] -> [] - | rs1::tl -> union_ex rs1 (edup tl) - in - edup rset_list -;; diff --git a/helm/ocaml/mathql_interpreter/relation.mli b/helm/ocaml/mathql_interpreter/relation.mli deleted file mode 100644 index 392d670cf..000000000 --- a/helm/ocaml/mathql_interpreter/relation.mli +++ /dev/null @@ -1,27 +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/. - *) - -val relation_ex : - MathQL.refine_op -> MathQL.path -> MathQL.resource_set -> MathQL.vvar_list -> MathQL.resource_set diff --git a/helm/ocaml/mathql_interpreter/select.ml b/helm/ocaml/mathql_interpreter/select.ml deleted file mode 100644 index ee9f329ba..000000000 --- a/helm/ocaml/mathql_interpreter/select.ml +++ /dev/null @@ -1,153 +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/. - *) - -(* - * implementazione del comando SELECT - *) -(* -open MathQL;; -open Func;; -open Utility;; - -exception ExecuteFunctionNotInitialized;; -let execute = - ref - (function _ -> raise ExecuteFunctionNotInitialized) -;; - -(* - * valutazione di una stringa - *) -let stringeval env = - let module S = Mathql_semantics in - function - MQCons s -> - s - | MQFunc (f, rvar) -> - let {S.uri = uri} = List.assoc rvar env in - apply_func f uri - | MQStringRVar rvar -> - let {S.uri = uri} = List.assoc rvar env in - uri - | MQStringSVar svar -> - let (_,{S.attributes = attributes}) = List.hd env in - List.assoc svar attributes - | MQMConclusion -> - "MainConclusion" - | MQConclusion -> - "InConclusion" -;; - -(* - * - *) -let rec is_good env = - let module S = Mathql_semantics in - function - MQAnd (b1, b2) -> - (is_good env b1) && (is_good env b2) - | MQOr (b1, b2) -> - (is_good env b1) || (is_good env b2) - | MQNot b1 -> - not (is_good env b1) - | MQTrue -> - true - | MQFalse -> - false - | MQIs (s1, s2) -> - (stringeval env s1) = (stringeval env s2) -(*CSC: magari le prossime funzioni dovrebbero andare in un file a parte, *) -(*CSC: insieme alla [execute] che utilizzano *) - | MQSetEqual (q1,q2) -> - (* set_of_result returns an ordered list of uris without duplicates *) - let rec set_of_result = - function - _,[] -> [] - | (Some olduri as v),{S.uri = uri}::tl when uri = olduri -> - set_of_result (v,tl) - | _,{S.uri = uri}::tl -> - uri::(set_of_result (Some uri, tl)) - in - let ul1 = set_of_result (None,!execute env q1) in - let ul2 = set_of_result (None,!execute env q2) in - print_endline ("MQSETEQUAL(" ^ - string_of_int (List.length (!execute env q1)) ^ ">" ^ - string_of_int (List.length ul1) ^ "," ^ - string_of_int (List.length (!execute env q2)) ^ ">" ^ - string_of_int (List.length ul2) ^ ")") ; - flush stdout ; - (try - List.fold_left2 (fun b uri1 uri2 -> b && uri1=uri2) true ul1 ul2 - with - _ -> false) - | MQSubset (q1,q2) -> -(*CSC: codice cut&paste da sopra: ridurlo facendo un'unica funzione h.o. *) - (* set_of_result returns an ordered list of uris without duplicates *) - let rec set_of_result = - function - _,[] -> [] - | (Some olduri as v),{S.uri = uri}::tl when uri = olduri -> - set_of_result (v,tl) - | _,{S.uri = uri}::tl -> - uri::(set_of_result (Some uri, tl)) - in - let ul1 = set_of_result (None,!execute env q1) in - let ul2 = set_of_result (None,!execute env q2) in - print_endline ("MQSUBSET(" ^ - string_of_int (List.length (!execute env q1)) ^ ">" ^ - string_of_int (List.length ul1) ^ "," ^ - string_of_int (List.length (!execute env q2)) ^ ">" ^ - string_of_int (List.length ul2) ^ ")") ; - flush stdout ; - let rec is_subset s1 s2 = - match s1,s2 with - [],_ -> true - | _,[] -> false - | uri1::tl1,uri2::tl2 when uri1 = uri2 -> - is_subset tl1 tl2 - | uri1::_,uri2::tl2 when uri1 > uri2 -> - is_subset s1 tl2 - | _,_ -> false - in - is_subset ul1 ul2 -;; - -(* - * implementazione del comando SELECT - *) -let select_ex env avar alist abool = - let _ = print_string ("SELECT = ") - and t = Sys.time () in - let result = - List.filter (function entry -> is_good ((avar,entry)::env) abool) alist - in - print_string (string_of_int (List.length result) ^ ": ") ; - print_endline (string_of_float (Sys.time () -. t) ^ "s") ; - flush stdout ; - result -;; *) - -let select_ex rvar rset bexp - diff --git a/helm/ocaml/mathql_interpreter/select.mli b/helm/ocaml/mathql_interpreter/select.mli deleted file mode 100644 index 7c2fe9ddf..000000000 --- a/helm/ocaml/mathql_interpreter/select.mli +++ /dev/null @@ -1,34 +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/. - *) - -exception ExecuteFunctionNotInitialized;; -val execute: - (Mathql_semantics.attributed_uri_env -> - MathQL.mqlist -> Mathql_semantics.result) ref - -val select_ex : - Mathql_semantics.attributed_uri_env -> - MathQL.mqrvar -> Mathql_semantics.result -> MathQL.mqbool -> - Mathql_semantics.result diff --git a/helm/ocaml/mathql_interpreter/sortedby.ml b/helm/ocaml/mathql_interpreter/sortedby.ml deleted file mode 100644 index b9a05a002..000000000 --- a/helm/ocaml/mathql_interpreter/sortedby.ml +++ /dev/null @@ -1,62 +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/. - *) - -(* - * implementazione del comando SORTEDBY - *) - -open MathQL;; -open Func;; -open Utility;; - -(* - * implementazione del comando SORTEDBY - *) -let sortedby_ex alist order afunc = - let before = Sys.time () in - let res = - let module S = Mathql_semantics in - (Sort.list - (fun {S.extra = e1} {S.extra = e2} -> - match order with - MQAsc -> e1 < e2 - | MQDesc -> e1 > e2 - ) - (List.map - (fun {S.uri = u ; S.attributes = attr} -> {S.uri = u ; S.attributes = attr ; S.extra = (apply_func afunc u)}) - alist - ) - ) - in - let after = Sys.time () - and ll1 = string_of_int (List.length alist) in - let diff = string_of_float (after -. before) in - print_endline - ("SORTEDBY(" ^ ll1 ^ ") = " ^ string_of_int (List.length res) ^ - ": " ^ diff ^ "s") ; - flush stdout ; - res -;; - diff --git a/helm/ocaml/mathql_interpreter/sortedby.mli b/helm/ocaml/mathql_interpreter/sortedby.mli deleted file mode 100644 index 863581a09..000000000 --- a/helm/ocaml/mathql_interpreter/sortedby.mli +++ /dev/null @@ -1,27 +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/. - *) - -val sortedby_ex : - Mathql_semantics.result -> MathQL.mqorder -> MathQL.mqfunc -> Mathql_semantics.result diff --git a/helm/ocaml/mathql_interpreter/sub.ml b/helm/ocaml/mathql_interpreter/sub.ml deleted file mode 100644 index e59bf049d..000000000 --- a/helm/ocaml/mathql_interpreter/sub.ml +++ /dev/null @@ -1,34 +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/. - *) - - -let rec sub_ex v1 v2 = - match v1,v2 with - [],_ -> true - | _,[] -> false - | s1::_, s2::_ when s1 < s2 -> false - | s1::_, s2::tl2 when s2 < s1 -> sub_ex v1 tl2 - | s1::tl1, s2::tl2 -> sub_ex tl1 tl2 -;; diff --git a/helm/ocaml/mathql_interpreter/sub.mli b/helm/ocaml/mathql_interpreter/sub.mli deleted file mode 100644 index b81f542c4..000000000 --- a/helm/ocaml/mathql_interpreter/sub.mli +++ /dev/null @@ -1,27 +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/. - *) - - -val sub_ex: MathQL.value -> MathQL.value -> bool diff --git a/helm/ocaml/mathql_interpreter/union.ml b/helm/ocaml/mathql_interpreter/union.ml deleted file mode 100644 index e2d9fcb01..000000000 --- a/helm/ocaml/mathql_interpreter/union.ml +++ /dev/null @@ -1,52 +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/. - *) - -(* - * implementazione del comando UNION - *) - - -(* Merges two attribute group lists preserves order and gets rid of duplicates*) -let rec merge l1 l2 = - match (l1,l2) with - [],l - | l,[] -> l - | g1::tl1,g2::_ when g1 < g2 -> g1::(merge tl1 l2) - | g1::_,g2::tl2 when g2 < g1 -> g2::(merge l1 tl2) - | g1::tl1,g2::tl2 -> g1::(merge tl1 tl2) -;; - -(* preserves order and gets rid of duplicates *) -let rec union_ex rs1 rs2 = - match (rs1, rs2) with - [],l - | l,[] -> l - | (uri1,l1)::tl1,(uri2,_)::_ when uri1 < uri2 -> (uri1,l1)::(union_ex tl1 rs2) - | (uri1,_)::_,(uri2,l2)::tl2 when uri2 < uri1 -> (uri2,l2)::(union_ex rs1 tl2) - | (uri1,l1)::tl1,(uri2,l2)::tl2 -> if l1 = l2 then (uri1,l1)::(union_ex tl1 tl2) - else (uri1,merge l1 l2)::(union_ex tl1 tl2) -;; - - diff --git a/helm/ocaml/mathql_interpreter/union.mli b/helm/ocaml/mathql_interpreter/union.mli deleted file mode 100644 index 6890bdb0c..000000000 --- a/helm/ocaml/mathql_interpreter/union.mli +++ /dev/null @@ -1,27 +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/. - *) - -val union_ex : -MathQL.result -> MathQL.result -> MathQL.result diff --git a/helm/ocaml/mathql_interpreter/use.ml b/helm/ocaml/mathql_interpreter/use.ml deleted file mode 100644 index f5648cab1..000000000 --- a/helm/ocaml/mathql_interpreter/use.ml +++ /dev/null @@ -1,90 +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/. - *) - -(* - * implementazione dei comandi USE/USED BY - *) - -open Utility;; -open Dbconn;; - -(* - * implementazione dei comandi USE/USED BY - * - * parametri: - * alist: string list list; lista su cui eseguire il comando USE/USED BY - * asvar: string; nome della variabile del comando use - * usek: string; nome della tabella in cui ricercare le occorrenze; - * la distinzione fra l'esecuzione del comando USE e USED BY - * sta nell'utilizzo della tabella 'backPointer' per USE - * e 'refObj' per USED BY - * - * output: string list list; lista su cui e' stato eseguito il - * comando USE/USED BY - *) -let get_prop_id prop = - if prop="refObj" then "F" - else if prop="backPointer" then "B" - else assert false - ;; - - -let relation_ex rop path rset attl = - let usek = get_prop_id (List.hd path) in - -let _ = print_string ("RELATION "^usek) -and t = Sys.time () in -let result = - let c = pgc () in - Sort.list - (fun (uri1-> uri1 < uri2) - (List.fold_left - (fun parziale (uri,aset)-> - print_string uri ; - let tv = - pgresult_to_string - (c#exec ("select id from registry where uri='" ^ uri ^ "'")) - in - let qq = - "select uri, context from t" ^ tv ^ " where prop_id='" ^ usek ^ - "' order by uri asc" - in - let res = c#exec qq in - (List.map - (function - [uri;context] -> {S.uri = uri ; S.attributes = [asvar, context] ; S.extra = ""} - | _ -> assert false - ) res#get_list - ) @ - parziale - ) [] rset - ) -in -print_string (" = " ^ string_of_int (List.length result) ^ ": ") ; -print_endline (string_of_float (Sys.time () -. t) ^ "s") ; -flush stdout ; - result -;; - diff --git a/helm/ocaml/mathql_interpreter/use.mli b/helm/ocaml/mathql_interpreter/use.mli deleted file mode 100644 index 0572ad5ac..000000000 --- a/helm/ocaml/mathql_interpreter/use.mli +++ /dev/null @@ -1,27 +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/. - *) - -val use_ex : - Mathql_semantics.result -> MathQL.mqsvar -> string -> Mathql_semantics.result diff --git a/helm/ocaml/mathql_interpreter/utility.ml b/helm/ocaml/mathql_interpreter/utility.ml deleted file mode 100644 index 5ea9b7e67..000000000 --- a/helm/ocaml/mathql_interpreter/utility.ml +++ /dev/null @@ -1,119 +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/. - *) - -(* - * funzioni di utilita' generale - *) - -open Dbconn;; - -(* - * converte il risultato di una query in una lista di stringhe - * - * parametri: - * l: Postgres.result; risultato della query - * - * output: string list; lista di stringhe (una per tupla) - * - * assumo che il risultato della query sia - * costituito da un solo valore per tupla - * - * TODO - * verificare che l sia effettivamente costruita come richiesto - *) -let pgresult_to_string_list l = List.map (List.hd) l#get_list;; - -(* - * converte il risultato di una query in una stringa - * - * paramteri: - * l: Postgres.result; risultato della query - * - * output: string; valore dell'unica tupla del risultato - * - * mi aspetto che il risultato contenga una sola tupla - * formata da un solo valore - * - * TODO - * verificare che l sia costruita come richiesto - *) -let pgresult_to_string l = - match l#get_list with - [] -> "" - | t -> List.hd (List.hd t) -;; - -(* - * parametri: - * x: 'a; chiave di cui settare il valore - * v: 'b; valore da assegnare alla chiave - * l: ('a * 'b) list; lista di coppie in cui effettuare - * l'assegnamento - * - * output: ('a * 'b) list; lista di coppie contenente (x, v) - * - * TODO - * gestire i casi in cui in l compaiono piu' coppie (x, _) - * si sostituiscono tutte? se ne sostituisce una e si eliminano - * le altre? - *) -let set_assoc x v l = - let rec spila testa key value lista = - match lista with - [] -> testa @ [(key, value)] - | (j, _)::tl when j = key -> testa @ [(key, value)] @ tl - | hd::tl -> spila (testa @ [hd]) key value tl - in - spila [] x v l -;; - -(* - * parametri: - * p: string; nome della proprieta' - * - * output: string; id interno associato alla proprieta' - *) -let helm_property_id p = - let c = pgc () in - let q1 = "select att0 from namespace where att1='http://www.cs.unibo.it/helm/schemas/mattone.rdf#'" in - let ns = pgresult_to_string (c#exec q1) in - let q2 = ("select att0 from property where att2='" ^ p ^ "' and att1=" ^ ns) in - let retval = pgresult_to_string (c#exec q2) in - (*let _ = print_endline ("utility:q2: " ^ q2 ^ " : " ^ retval) in*) - retval -;; - -(* - * parametri: - * c: string; nome della classe - * - * output: string; id interno associato alla classe - *) -let helm_class_id cl = - let c = pgc () in - let ns = pgresult_to_string (c#exec ("select att0 from namespace where att1='http://www.cs.unibo.it/helm/schemas/mattone.rdf#'")) in - pgresult_to_string (c#exec ("select att0 from class where att2='" ^ cl ^ "' and att1=" ^ ns)) -;; - diff --git a/helm/ocaml/mathql_interpreter/utility.mli b/helm/ocaml/mathql_interpreter/utility.mli deleted file mode 100644 index 9e9e8290d..000000000 --- a/helm/ocaml/mathql_interpreter/utility.mli +++ /dev/null @@ -1,30 +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/. - *) - -val pgresult_to_string_list : < get_list : string list list; .. > -> string list -val pgresult_to_string : < get_list : string list list; .. > -> string -val set_assoc : 'a -> 'b -> ('a * 'b) list -> ('a * 'b) list -val helm_property_id: string -> string -val helm_class_id: string -> string