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 877bd075fddc85f7955296612a7f388eacb2e53b..a9fbcf214f1279e9ea368a9ee92301a0cdaaadb0 100644 (file)
--- 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 68fb9992e42064a9de3f9489a9efc7c97bb34c6d..8e8f3792a0a13d2b5384e27462d0d89d86905bc2 100644 (file)
--- 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 57b663f73c0264518b2a04eed766f9c8db4136b3..f875f1022bc820351c64b8a72e7f83c606f833f9 100644 (file)
--- 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