From: Irene Schena <irene.schena@unibo.it>
Date: Mon, 29 Apr 2002 14:27:49 +0000 (+0000)
Subject: Modified Files:
X-Git-Tag: V_0_3_0_debian_8~116
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=7b7d26322d3bd9be8d6cdde79c74ff38e921290b

Modified Files:
1) grammar.txt query.xml xmathql.dtd: Pattern structure added in the dtd
and some other changes
---

diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt
index 877bd075f..a9fbcf214 100644
--- a/helm/mathql/grammar.txt
+++ b/helm/mathql/grammar.txt
@@ -43,11 +43,11 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
 	 |  <svar>			       (* variabile *)
 	 |  <function> <rvar>                  (* applicazione di funzione *)
 	 
-<function> := NAME			       (* rvar -> nome_oggetto *)
+<function> := NAME			       (* URIREF -> nome_oggetto *)
 	   |  <property>
 
-<property> := THEORY                           (* URI -> valore_Proprieta' *)
-           |  TITLE			       (* URI -> valore_Prop_DC *)
+<property> := THEORY                           (* URIREF -> valore_Proprieta' *)
+           |  TITLE			       (* URIREF -> valore_Prop_DC *)
            |  CONTRIBUTOR
            |  CREATOR
            |  PUBLISHER
@@ -81,8 +81,9 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
 
 - le stringhe sono "case sensitive" 
 - la funzione non definita sull'argomento restituisce la stringa nulla
-- le <rvar> si presuppongono essere istanziate come URI complete o
-  URI#xpointer_expression e identificano risorse 
+- le <rvar> si presuppongono essere istanziate come URI references costituite
+  da un URI e da un fragment identifier opzionalecomplete; esse identificano 
+  risorse 
 - ogni binding lega una variabile libera (nuova) 
 - Precedenza operatori:
   NOT (+)  DIFF
diff --git a/helm/mathql/query.xml b/helm/mathql/query.xml
index 68fb9992e..8e8f3792a 100644
--- a/helm/mathql/query.xml
+++ b/helm/mathql/query.xml
@@ -2,13 +2,28 @@
 
 <!DOCTYPE MathQL SYSTEM "xmathql.dtd">
 
-<!-- To validate: xmllint -valid -loaddtd -noout proquery.xml -->
+<!-- To validate: xmllint -valid -loaddtd -noout query.xml -->
 
 <MathQL>
  <Select>
   <In>
    <Use>
-    <Pattern arg="cic:/Coq/Init/Logic/Equality/eq.ind"/>
+    <Pattern>
+     <Prefix>cic</Prefix>
+     <TokenList>
+      <SLASH/>
+      <CONST>Coq</CONST>
+      <SLASH/>
+      <CONST>Init</CONST>
+      <SLASH/>
+      <CONST>Logic</CONST>
+      <SLASH/>
+      <CONST>Equality</CONST>
+      <SLASH/>
+      <CONST>eq</CONST>
+     </TokenList>
+     <Extension>ind</Extension>
+    </Pattern>
     <Position binder="$1"/>
    </Use>
   </In>
diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index 57b663f73..f875f1022 100644
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -43,6 +43,8 @@
 <!-- Operators are unambiguous (binary or unary), so there isn't any -->
 <!-- grouping operator.                                              -->
 <!-- CONST is the constant string.                                   -->
+<!-- The attributes binder and rvar declare variables which are      -->
+<!-- referred to and used by means of respectively BINDER and RVAR   -->
 <!--*****************************************************************-->
 
 <!ENTITY % position '(Conclusion|Hypothesis|Body|MainConclusion|
@@ -97,9 +99,7 @@
 
 <!ELEMENT ConstructorsOf %queryexpr;>
 
-<!ELEMENT Pattern EMPTY>
-<!ATTLIST Pattern
-          arg CDATA #REQUIRED>
+<!ELEMENT Pattern (Prefix, (TokenList, (Extension, FragmentID?)?)?)>
 
 <!ELEMENT InTheory (%queryexpr;, ItemType)>
 
@@ -133,6 +133,22 @@
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
+<!ELEMENT STAR EMPTY>
+
+<!ELEMENT TWOSTARS EMPTY>
+
+<!ELEMENT SLASH EMPTY>
+
+<!ELEMENT QUESTIONMARK EMPTY>
+
+<!ELEMENT TokenList (CONST|STAR|TWOSTARS|SLASH|QUESTIONMARK)+>
+
+<!ELEMENT Prefix (#PCDATA)>
+
+<!ELEMENT Extension (#PCDATA)>
+
+<!ELEMENT FragmentID (#PCDATA)>
+
 <!-- MathQL boolean expressions -->
 
 <!ELEMENT AND (%boolexpr;, %boolexpr;)>
@@ -148,6 +164,7 @@
           value %bool; #REQUIRED>
 
 <!-- MathQL string expressions -->
+
 <!ELEMENT CONST (#PCDATA)>
 
 <!ELEMENT RVAR EMPTY>
@@ -164,14 +181,14 @@
 
 <!ELEMENT NAME (RVAR)>
 
-<!ELEMENT PROPERTY (RVAR|CONST)>
+<!ELEMENT PROPERTY (RVAR)>
 <!ATTLIST PROPERTY
           name CDATA #REQUIRED>
 
-<!ELEMENT SUPERPROPERTY  (RVAR|CONST)>
+<!ELEMENT SUPERPROPERTY (RVAR)>
 <!ATTLIST SUPERPROPERTY
           name CDATA #REQUIRED>
 
-<!ELEMENT SUBPROPERTY (RVAR|CONST)>
+<!ELEMENT SUBPROPERTY (RVAR)>
 <!ATTLIST SUBPROPERTY
           name CDATA #REQUIRED>
\ No newline at end of file