From 978a25d9392e5fc1a19fa37c86339c5d0b67ddd6 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 13 May 2004 13:32:12 +0000 Subject: [PATCH] - some code patched - mathql documentation updated --- helm/Makefile | 2 +- helm/gTopLevel/gTopLevel.ml | 2 +- helm/gTopLevel/oldDisambiguate.ml | 4 +-- helm/gTopLevel/oldDisambiguate.mli | 2 +- helm/mathql/doc/mathql.tex | 10 +++++- helm/mathql/doc/mathql_introduction.tex | 2 +- .../doc/mathql_introduction_property.tex | 35 +++++++++++++++++++ .../doc/mathql_introduction_textual.tex | 2 +- helm/mathql/doc/mathql_macros.sty | 7 ++++ helm/mathql/doc/mathql_operational.tex | 2 +- helm/mathql/doc/mathql_operational_core.tex | 6 ++-- helm/mathql/doc/mathql_tests.tex | 2 ++ helm/ocaml/cic_disambiguation/disambiguate.ml | 2 +- .../cic_disambiguation/disambiguateTypes.ml | 2 +- .../cic_disambiguation/disambiguateTypes.mli | 2 +- helm/ocaml/tactics/match_concl.ml | 4 ++- helm/searchEngine/searchEngine.ml | 4 +-- 17 files changed, 72 insertions(+), 18 deletions(-) diff --git a/helm/Makefile b/helm/Makefile index b87be5027..ffab1984d 100644 --- a/helm/Makefile +++ b/helm/Makefile @@ -1,4 +1,4 @@ -DIRS = ocaml hbugs gTopLevel searchEngine mathql_test hxp +DIRS = ocaml gTopLevel searchEngine mathql_test hxp DIRS_BYTE = $(patsubst %,%.byte,$(DIRS)) DIRS_OPT = $(patsubst %,%.opt,$(DIRS)) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 1726725c1..bda4c4b82 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1058,7 +1058,7 @@ module DisambiguateCallbacks = interactive_user_uri_choice ~selection_mode ?ok ?enable_button_for_non_vars ~title ~msg let interactive_interpretation_choice = interactive_interpretation_choice - let input_or_locate_uri ~title ?id = input_or_locate_uri ~title + let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title end ;; diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index a47830a3f..db118b518 100644 --- a/helm/gTopLevel/oldDisambiguate.ml +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -47,7 +47,7 @@ module type Callbacks = title:string -> msg:string -> id:string -> string list -> string list val interactive_interpretation_choice : (string * string) list list -> int list - val input_or_locate_uri : title:string -> ?id:string -> UriManager.uri + val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri end ;; @@ -78,7 +78,7 @@ module Make(C:Callbacks) = [] -> [UriManager.string_of_uri (C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id)] + ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())] | [uri] -> [uri] | _ -> C.interactive_user_uri_choice diff --git a/helm/gTopLevel/oldDisambiguate.mli b/helm/gTopLevel/oldDisambiguate.mli index 8c8bb293f..c9b2775fe 100644 --- a/helm/gTopLevel/oldDisambiguate.mli +++ b/helm/gTopLevel/oldDisambiguate.mli @@ -45,7 +45,7 @@ module type Callbacks = title:string -> msg:string -> id:string -> string list -> string list val interactive_interpretation_choice : (string * string) list list -> int list - val input_or_locate_uri : title:string -> ?id:string -> UriManager.uri + val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri end type domain_and_interpretation = diff --git a/helm/mathql/doc/mathql.tex b/helm/mathql/doc/mathql.tex index ed9a96021..73cd44d2e 100644 --- a/helm/mathql/doc/mathql.tex +++ b/helm/mathql/doc/mathql.tex @@ -1,6 +1,7 @@ \documentclass{llncs} \usepackage{mathql_macros} +\newcommand\xcomment[1]{} \title{MathQL-1 Version 4\\Reference Documentation} \author{Ferruccio Guidi% @@ -21,7 +22,14 @@ Mura Anteo Zamboni 7, 40127 Bologna, ITALY.\\ \begin{abstract} \end{abstract} -\tableofcontents +\addtocounter{tocdepth}{2} + +\section*{\contentsname}{ +\catcode`@=11 +\def\l@title#1#2{} +\def\l@author#1#2{} +\@starttoc{toc} +\catcode`@=12} \input{mathql_overview} \input{mathql_introduction} diff --git a/helm/mathql/doc/mathql_introduction.tex b/helm/mathql/doc/mathql_introduction.tex index 0fad196e0..73086dba7 100644 --- a/helm/mathql/doc/mathql_introduction.tex +++ b/helm/mathql/doc/mathql_introduction.tex @@ -1,4 +1,4 @@ -\section{The language} +\section{Introduction} This paper presents {\MathQL} version 4 which is the latest version of the language, fully developed by the Author. diff --git a/helm/mathql/doc/mathql_introduction_property.tex b/helm/mathql/doc/mathql_introduction_property.tex index 5fffd7276..6bd8561e3 100644 --- a/helm/mathql/doc/mathql_introduction_property.tex +++ b/helm/mathql/doc/mathql_introduction_property.tex @@ -60,6 +60,12 @@ Example 6: imposing constraints on property values: Example 7: inverse traversal of the head path: property inverse /"date" attr /"first" in "" gives "A" attr {/"first" = "2002-01-01"}; "B" attr {/"first" = "2002-02-01"} + +Example 8: some triples of an access relation: +The triples formalizing the property "date" of the resource "A": +("A", /"date", ""); +("A", /"date"/"first", "2002-01-01"); +("A", /"date"/"modified", "2002-03-01") \end{verbatim} \end{footnotesize} \vspace{-1pc} \caption{The ``property'' operator} @@ -163,3 +169,32 @@ and builds the result set composing these {\av}'s with the set-theoretic union. \end{enumerate} See for instance \figref{Property} (example 7). + +Formally \TT{property} accesses the {\RDF} graph through an \emph{access +relation} which is a set of triples $ (r_1, p, r_2) $ where $ r_1 $ and +$ r_2 $ are strings, and $ p $ is a path. +Each triple is a sort of ``extended {\RDF} triple'' in the sense that $ r_1 $ +is a resource for which some metadata is provided, $ p $ is a path in the +{\RDF} graph and $ r_2 $ is the main value of the end-node of the instance of +$ p $ starting from $ r_1 $ (this includes the instances of sub- and +super-arcs of $ p $ if necessary). +See for instance \figref{Property} (example 8). +{\MathQL} does not provide for any built-in access relation so any query +engine can freely define the access relations that are appropriate with +respect to the metadata it can access. + +It is worth remarking, as it was already stressed in \cite{Gui03,GS03}, that +the concept of access relation corresponds to the abstract concept of property +in the basic {\RDF} data model which draws on well established principles from +various data representation communities. +In this sense an {\RDF} property can be thought of either as an attribute of a +resource (traditional attribute-value pairs model), or as a relation between +a resource and a value (entity-relationship model). +This observation leads us to conclude that {\MathQL} is sound and complete +with respect to querying an abstract {\RDF} metadata model. +Finally note that access relations are close to {\RDF} entity-relationship +model, but they do not work if we allow paths with an arbitrary number of +loops ({\ie} with an arbitrary length) because this would lead to creating +infinite sets of triples. +If we want to handle this case, we need to turn these relations into +multivalued functions. diff --git a/helm/mathql/doc/mathql_introduction_textual.tex b/helm/mathql/doc/mathql_introduction_textual.tex index 8e5878bac..2bcb2b4cd 100644 --- a/helm/mathql/doc/mathql_introduction_textual.tex +++ b/helm/mathql/doc/mathql_introduction_textual.tex @@ -1,4 +1,4 @@ -\section{Textual syntax} \label{Textual} +\subsection{Textual syntax} \label{Textual} In this section we present {\MathQL}.4 textual syntax using the same notation that we adopted in \cite{GS03,Gui03}. In particular the grammatical diff --git a/helm/mathql/doc/mathql_macros.sty b/helm/mathql/doc/mathql_macros.sty index de81655d4..8c8a85130 100644 --- a/helm/mathql/doc/mathql_macros.sty +++ b/helm/mathql/doc/mathql_macros.sty @@ -95,3 +95,10 @@ \newcommand\T{\TT{T}} \newcommand\GP[1]{\TT{<#1>}} + +\newcommand\Set{\textsf{Set}} +\newcommand\Prop{\textsf{Prop}} +\newcommand\MainConclusion{\textsf{MainConclusion}} +\newcommand\MainHypothesis{\textsf{MainHypothesis}} +\newcommand\occurrence{\textsf{occurrence}} +\newcommand\refObj{\textsf{refObj}} diff --git a/helm/mathql/doc/mathql_operational.tex b/helm/mathql/doc/mathql_operational.tex index 32be697a5..a7b3a9a49 100644 --- a/helm/mathql/doc/mathql_operational.tex +++ b/helm/mathql/doc/mathql_operational.tex @@ -1,4 +1,4 @@ -\section {Operational semantics} \label {Operational} +\section {Operational Semantics} \label {Operational} This section describes {\MathQL} semantics, that we present in a natural operational style \cite{Lan98,Win93}. diff --git a/helm/mathql/doc/mathql_operational_core.tex b/helm/mathql/doc/mathql_operational_core.tex index ed0391752..e096879bb 100644 --- a/helm/mathql/doc/mathql_operational_core.tex +++ b/helm/mathql/doc/mathql_operational_core.tex @@ -188,8 +188,8 @@ When the \TT{main} clause is not present, we assume $ p_2 = \TT{/} $. Here $ \Property\ h $ gives the appropriate access relation according to the $ h $ flag (this is the primitive function that inspects the {\RDF} -graph, see \subsecref{HighAccess}). - +graph). + $ \Src\ k\ P\ V $ is a helper function giving the source set according to the $ k $ flag. $ \Src $ is based on $ \Match $, the helper function handling {\POSIX} regular expressions. @@ -497,7 +497,7 @@ where $ \Gen \oft \GP{path} \times (\Listof\ \GP{query}) \times K \to \GP{query} $ is the primitive function performing the low level invocation. The core language does not include any external function of this kind and it is a mistake to invoke an undefined function. -The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \{x\}''. +The construction ``\TT{gen} p \TT{in} x'' rewrites to ``\TT{gen} p \verb+{+x\verb+}+''. \end{itemize} diff --git a/helm/mathql/doc/mathql_tests.tex b/helm/mathql/doc/mathql_tests.tex index 1e31b9472..883bf23ab 100644 --- a/helm/mathql/doc/mathql_tests.tex +++ b/helm/mathql/doc/mathql_tests.tex @@ -26,3 +26,5 @@ main /"h:occurrence" istrue /"h:position" in {$IC, $IH} of @uri} in @uri in let $trans = select @uri from $trans1 where ex (not @uri./"extra" and (@uri./"premises" sub {@uri./"rel", @uri./"set"})) in keep $trans \end{verbatim} \end{footnotesize} %$ + +\input{mathql_tests_transitive} diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 92b081c48..f7cfce144 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -407,7 +407,7 @@ module Make (C: Callbacks) = match uris with | [] -> [UriManager.string_of_uri (C.input_or_locate_uri - ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id)] + ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())] | [uri] -> [uri] | _ -> C.interactive_user_uri_choice ~selection_mode:`MULTIPLE diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml index a5e0f96f8..d01f82ee9 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.ml +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.ml @@ -57,7 +57,7 @@ module type Callbacks = title:string -> msg:string -> id:string -> string list -> string list val interactive_interpretation_choice : (string * string) list list -> int list - val input_or_locate_uri : title:string -> ?id:string -> UriManager.uri + val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri end let string_of_domain_item = function diff --git a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli index ccde1a4e8..db9829e03 100644 --- a/helm/ocaml/cic_disambiguation/disambiguateTypes.mli +++ b/helm/ocaml/cic_disambiguation/disambiguateTypes.mli @@ -52,7 +52,7 @@ module type Callbacks = (** @param title gtk window title for user prompting * @param id unbound identifier which originated this callback invocation *) - val input_or_locate_uri : title:string -> ?id:string -> UriManager.uri + val input_or_locate_uri : title:string -> ?id:string -> unit -> UriManager.uri end val string_of_domain_item: domain_item -> string diff --git a/helm/ocaml/tactics/match_concl.ml b/helm/ocaml/tactics/match_concl.ml index 4f36f3ee5..078cb931a 100644 --- a/helm/ocaml/tactics/match_concl.ml +++ b/helm/ocaml/tactics/match_concl.ml @@ -171,8 +171,10 @@ let cmatch (conn:Mysql.dbd) t = let prefixes = NewConstraints.prefixes just_factor t in (match prefixes with Some main, all_concl -> +(* NewConstraints.pp_prefixes all_concl; - (* in some cases, max_prefix_length could be less than n *) +*) + (* in some cases, max_prefix_length could be less than n *) let max_prefix_length = match all_concl with [] -> assert false diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 1762e5fd9..fc0fb9cbe 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -459,8 +459,8 @@ let callback mqi_handle (req: Http_types.request) outchan = interactive_interpretation_choice_TPL; raise Chat_unfinished - let input_or_locate_uri ~title = - UriManager.uri_of_string "cic:/Coq/Init/DataTypes/nat_ind.con" + let input_or_locate_uri ~title ?id () = + assert false end in -- 2.39.2