'new_mathql_before_first_merge'.
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+(* GLOBAL CONSTANTS *)
+
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
+
+let htmlheader =
+ "<html>" ^
+ " <body bgColor=\"white\">"
+;;
+
+let htmlfooter =
+ " </body>" ^
+ "</html>"
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+ | None ->
+ output_html outputhtml
+ ("<h1 color=\"red\">No term selected</h1>")
+;;
+
+
+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 "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
+ Xml.xml_cdata
+ ("<!DOCTYPE CurrentProof SYSTEM \"" ^ dtdname ^ "\">\n\n") ;
+ xml
+ >]
+ in
+ Xml.pp ~quiet:true xml' (Some prooffile) ;
+ output_html outputhtml
+ ("<h1 color=\"Green\">Current proof saved to " ^
+ prooffile ^ "</h1>")
+;;
+
+(* 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
+ ("<h1 color=\"Green\">Current proof loaded from " ^
+ prooffile ^ "</h1>")
+ | _ -> assert false
+ with
+ RefreshSequentException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+ 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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "sequent: " ^ Printexc.to_string e ^ "</h1>")
+ | RefreshProofException e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">Exception raised during the refresh of the " ^
+ "proof: " ^ Printexc.to_string e ^ "</h1>")
+ | e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
+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 -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
+ )
+;;
+
+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:"<html><body bgColor=\"white\"></body></html>"
+ ~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 ();
+;;
+++ /dev/null
-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)));
+++ /dev/null
-*.cm[iaox] *.cmxa mQueryTLexer.ml mQueryTParser.ml mQueryTParser.mli
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* raw HTML representation **************************************************)
-
-let key s = "<font color=\"blue\">" ^ s ^ " </font>"
-
-let sub s = "<font color=\"blue\"> " ^ s ^ " </font>"
-
-let sub2 s = "<font color=\"blue\">" ^ s ^ "</font>"
-
-let sym s = s
-
-let sep s = s
-
-let str s = "<font color=\"red\">'" ^ s ^ "'</font>"
-
-let pat s = "<font color=\"red\">\"" ^ s ^ "\"</font>"
-
-let res s = "<font color=\"brown\">\"" ^ s ^ "\"</font>"
-
-let nl () = "<br>\n"
-
-let par () = "<p>\n"
+++ /dev/null
-(* 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 <fguidi@cs.unibo.it> *)
-(* 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 }
+++ /dev/null
-/* 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 <fguidi@cs.unibo.it> */
-/* 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 <string> 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 <string> qstr
- %type <MathQL.query> query
- %type <MathQL.result> 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 }
+++ /dev/null
-(* 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 <fguidi@cs.unibo.it> *)
-(* 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 ^ ")"
+++ /dev/null
-(* 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 <fguidi@cs.unibo.it> *)
-(* 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
-
+++ /dev/null
-(* 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 <fguidi@cs.unibo.it> *)
-(* Irene Schena <schena@cs.unibo.it> *)
-(* 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
+++ /dev/null
-*.cm[iaox] *.cmxa
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-(* 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}
-
-
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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) ^ "$'"
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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")
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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 ()
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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 *)
+++ /dev/null
-(* 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)
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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)
-;;
-
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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
-;;
-
+++ /dev/null
-(* 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
+++ /dev/null
-(* 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))
-;;
-
+++ /dev/null
-(* 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
projects / helm.git / commitdiff