]> matita.cs.unibo.it Git - helm.git/commitdiff
- some code patched
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 13 May 2004 13:32:12 +0000 (13:32 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Thu, 13 May 2004 13:32:12 +0000 (13:32 +0000)
- mathql documentation updated

17 files changed:
helm/Makefile
helm/gTopLevel/gTopLevel.ml
helm/gTopLevel/oldDisambiguate.ml
helm/gTopLevel/oldDisambiguate.mli
helm/mathql/doc/mathql.tex
helm/mathql/doc/mathql_introduction.tex
helm/mathql/doc/mathql_introduction_property.tex
helm/mathql/doc/mathql_introduction_textual.tex
helm/mathql/doc/mathql_macros.sty
helm/mathql/doc/mathql_operational.tex
helm/mathql/doc/mathql_operational_core.tex
helm/mathql/doc/mathql_tests.tex
helm/ocaml/cic_disambiguation/disambiguate.ml
helm/ocaml/cic_disambiguation/disambiguateTypes.ml
helm/ocaml/cic_disambiguation/disambiguateTypes.mli
helm/ocaml/tactics/match_concl.ml
helm/searchEngine/searchEngine.ml

index b87be5027dfaee912ace426b570fec59eeb3d8e7..ffab1984d244a6642fe7f82fe0f48bdb089b4592 100644 (file)
@@ -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))
index 1726725c15370b146e42439def72b6b34c23c655..bda4c4b826126a2caf354bfdd5e7838227e6f8d6 100644 (file)
@@ -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
 ;;
 
index a47830a3ffc60bca7049332ad53a66a8b2ae30cc..db118b5187516a129ed59278a3e2cd059f9a2953 100644 (file)
@@ -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
index 8c8bb293fbc27b017d5f0c881d7e977e403f72b9..c9b2775fe0f5e9d5a2eaaab0554531608a3f18b5 100644 (file)
@@ -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 =
index ed9a96021736fa05b3ea5c2426e8f9ece81ea998..73cd44d2e2404c8040f3e44fc4d9d9e703896446 100644 (file)
@@ -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}
index 0fad196e03dc62ffd389824f17c0fb102e715422..73086dba7600f8c749678a020c27a7736ce6cf0a 100644 (file)
@@ -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.
index 5fffd727642dd6316edee64254e3957a4d74c69b..6bd8561e37b2376937efe608d5850933a382bdda 100644 (file)
@@ -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.
index 8e5878bac08f3faefef2f051619a369fa69dcb20..2bcb2b4cd0a7592add7d94fccc0e5591ffa5331a 100644 (file)
@@ -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
index de81655d4be40bec1eb133a188ab025466283000..8c8a851302800c5a060f211acc91fa9443b0706b 100644 (file)
 \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}}
index 32be697a50486a2ac4b99142a91c26613e9ccba4..a7b3a9a49dcfcef733349d20dac34d854253ea74 100644 (file)
@@ -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}. 
index ed03917528c3890363feafa39197255bb6d7de2d..e096879bba42f55f705be95811949e3a056a271e 100644 (file)
@@ -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}
 
index 1e31b947242714b0ae69c9f4474e9685ec6d257e..883bf23abe2947986711038794ff79d5dc610d29 100644 (file)
@@ -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}
index 92b081c4841b00833727309e69b9787bbc41ed3e..f7cfce144d7b6daacbceaafdc16ef71cdbc4286d 100644 (file)
@@ -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
index a5e0f96f838b48b1e04cacc3aa2cae96ad11d8f8..d01f82ee9e25f24a5656dfdb1696c8c9b8332fb9 100644 (file)
@@ -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
index ccde1a4e85690dc66374e93a67deffc9558f8fc7..db9829e03d1a0fc6c23734b6257d54d93e1e7755 100644 (file)
@@ -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
index 4f36f3ee55695705a025ee6927f2a49219834d73..078cb931a903b26ac2281d6dd8fa7b4a0236fc78 100644 (file)
@@ -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 
index 1762e5fd9f161f4da5409a3526abbdcfd953da66..fc0fb9cbee4ec2af67bb77d7f2b12ccfc1f269c2 100644 (file)
@@ -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