From: Irene Schena <irene.schena@unibo.it>
Date: Fri, 20 Sep 2002 14:14:25 +0000 (+0000)
Subject: Modified Files:
X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~67
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4f195220f9e7ee0fcb0de4d78a3e5817b70ea803;p=helm.git

Modified Files:
1)grammar.txt xmathql.dtd: updated versions
Removed Files:
1)core_grammar.txt: now all the grammar is implemented
---

diff --git a/helm/mathql/core_grammar.txt b/helm/mathql/core_grammar.txt
deleted file mode 100644
index 2ef292c99..000000000
--- a/helm/mathql/core_grammar.txt
+++ /dev/null
@@ -1,113 +0,0 @@
-GRAMMATICA PER QUERY SU DOCUMENTI MATEMATICI
-	VERSIONE IMPLEMENTATA
-MATHEMATICAL QUERY LANGUAGE (MathQL) 
-
-<query> := <set>                               (* clausola iniziale *)
-
-<set> :=  ( <set> )                            (* parentesizzazione *)
-       |  <rvar>			       (* var per insieme singoletto 
-						  di una risorsa *)
-       |  <svar>			       (* var per insieme di risorse
-						  (insieme di valori) *)
-       |  REF <string-set>                     (* oggetto/i referenziato/i da 
-						  URI esplicita/e *)
-       |  PATTERN <string-set>                 (* oggetto/i referenziato/i da 
-						  URI ottenute da espansione 
-						  del pattern *)
-       |  SELECT <rvar> IN <set> WHERE <bool>  (* selezione *)
-       |  LET <svar> BE <set> IN <set>         (* assegnazione a set-var in 
-                                                  contesto *)
-       |  <relation> <quoted-constant-string> <set> ATTR <vvar-list>           
-                                               (* unione insieme risorse in
-						  relazione specificata con le
-						  risorse in set, ognuna con 
-						  attributi (ATTR) *)
-       |  <set> UNION <set>                    (* unione *)
-       |  <set> INTERSECT <set>                (* intersezione *)
-
-<relation> := RELATION			       (* relazione (proprieta') *)
-	   |  SUBRELATION		       (* proprieta' e 
-						  sotto-proprieta' *)
-	   |  SUPERRELATION		       (* proprieta' e 
-						  super-proprieta' *)
-
-<vvar-list> := <vvar>
-            |  <vvar> , <vvar-list>
-
-<bool> := ( <bool> )                           (* parentesizzazione *)
-       |  TRUE                                 (* vero *)
-       |  FALSE                                (* falso *)
-       |  NOT <bool>                           (* negazione *)
-       |  <bool> AND <bool>                    (* congiunzione *)
-       |  <bool> OR <bool>                     (* disgiunzione *)
-       |  <string-set> EQ <string-set>         (* uguaglianza tra insiemi 
-						  stringhe (case sensitive) *)
-       |  <string-set> SUB <string-set>        (* operazione di sottoinsieme 
-						  tra insiemi stringhe *)
-       |  <string-set> MEET <string-set>       (* operazione di meet tra 
-						  insiemi stringhe *)
-       |  EX <bool>			       (* existential on attributes
-						  of references *)
-
-<string-set> := {}				   (* insieme vuoto*)
-	     |  <quoted-constant-string-set>       (* stringa singoletto *)
-             |  {<quoted-constant-string-set>}	   (* insieme stringhe *)
-             |  REFOF <set>			   (* insieme riferimenti *)
-             |  <rvar>.<vvar>                      (* variabile per insieme
-						      stringhe, relativa a 
-						      riferimento *)
-   	     |  <function> <quoted-constant-string> <string-set> 
-						   (* applicazione di funzione
-						      specificata a riferimento
-						      o insiemi di rif. o var*)
-
-<quoted-constant-string-set> := <quoted-constant-string>
-			     |  <quoted-constant-string> , <quoted-constant-string-set>				                  
-						   (* lista di stringhe *)
-
-<function> := FUN			           (* funzione generale *)
-
-<rvar> := @ <not-reserved-identifier>          (* variabile per riferimento *)
-<vvar> := $ <not-reserved-identifier>          (* variabile per insiemi 
-						  stringhe *)
-<svar> := % <not-reserved-identifier>          (* variabile per insiemi 
-						  riferimenti *)
-
-
-- MEET e' definito come "esiste almeno un elemento che appartiene 
-  all'interserzione tra due insiemi"
-- Le stringhe sono "case sensitive" 
-- La funzione non definita sull'argomento restituisce la stringa nulla
-- Le <rvar> si presuppongono essere istanziate come URI references costituite
-  da un URI e da un fragment identifier opzionale complete; i riferimenti 
-  identificano risorse 
-- Precedenza operatori:
-  NOT (+)  DIFF
-  AND      INTERSECT
-  OR  (-)  UNION
-- L'ordinamento di default e' quello alfabetico crescente in base al nome 
-  delle rvar
-- REF aumenta performance perche' NON accede al data base (costoso).
-- L'argomento di PATTERN ha sintassi di una espressione regolare 
-  POSIX 1003.2-1992
-- Possibili FUN (<quoted-constant-string>):
-  NAME (* URIREF -> nome_oggetto *)
-- MEET aumenta performance nel caso si verifichi (a in S) oppure 
-  (b in S) = ({a,b} meet S) perche' valuta S una volta sola
-- Record <rvar>.<svar> serve per disambiguare nomi uguali di variabili
-- Operatori (come EQ) hanno nomi abbreviati rispetto ai costrutti del 
-  linguaggio
-- EX verfica che la sua condizione sia vera per almeno un insieme di attributi
-  associato all'URI in rvar
-- Possibili RELATION sono:
-  USE con attributo POSITION (riferimenti backward) e valori MAINHYPOTHESIS, 
-		    HYPOTHESIS, MAINCONCLUSION, CONCLUSION, BODY
-  USEBY con attributo POSITION (riferimenti forward) e valori MAINHYPOTHESIS, 
-		    HYPOTHESIS, MAINCONCLUSION, CONCLUSION, BODY
-  CONSTRUCTORS
-  INTHEORY con attributo ITEMTYPE (riferimenti oggetti contenuti in teorie)
-  THEORYREFTO con attributo ITEMTYPE (riferimenti teorie referenti a oggetti)
-- <string-set> invece di <set> come argomento di <function> poiche' la REF non
-  e' piu' restrittiva su argomento/i e quindi e' inutile imporne l'uso quando
-  si passano i riferimenti alle funzioni. Con <string-set> l'utente e' libero
-  di passare direttamente le stringhe dei riferimenti.
\ No newline at end of file
diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt
index 979b4c549..0416f0187 100644
--- a/helm/mathql/grammar.txt
+++ b/helm/mathql/grammar.txt
@@ -16,8 +16,10 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
        |  SELECT <rvar> IN <set> WHERE <bool>  (* selezione *)
        |  LET <svar> BE <set> IN <set>         (* assegnazione a set-var in 
                                                   contesto *)
-       |  <relation> <quoted-constant-string> <set> ATTR <vvar-list>           
-                                               (* unione insieme risorse in
+       |  LET <vvar> BE <string-set> IN <set>  (* assegnamento a value-var
+						  in contesto*)
+       |  RELATION <refine_op> <quoted-constant-string> <set> ATTR <vvar-list>
+       		                               (* unione insieme risorse in
 						  relazione specificata con le
 						  risorse in set, ognuna con 
 						  attributi (ATTR) *)
@@ -25,12 +27,18 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
        |  <set> INTERSECT <set>                (* intersezione *)
        |  <set> DIFF <set>                     (* differenza *)
 
-<relation> := RELATION			       (* relazione (proprieta') *)
-	   |  SUBRELATION		       (* proprieta' e 
+<refine_op> := <quoted-constant-string-set>    (* relazione (proprieta') 
+					          strutturata *)
+      	    |  SUB			       (* proprieta' e 
 						  sotto-proprieta' *)
-	   |  SUPERRELATION		       (* proprieta' e 
+	    |  SUPER			       (* proprieta' e 
 						  super-proprieta' *)
 
+<quoted-constant-string-set> := ""
+			     |  <quoted-constant-string>
+			     |  <quoted-constant-string> <quoted-constant-string-set>
+						(* insieme di stringhe *)
+
 <vvar-list> := <vvar>
             |  <vvar> , <vvar-list>
 
@@ -50,16 +58,17 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
        |  EX <bool>			       (* existential on attributes
 						  of references *)
 <string-set> := {}				   (* insieme vuoto*)
-	     |  <quoted-constant-string-set>       (* stringa singoletto *)
-             |  {<quoted-constant-string-set>}	   (* insieme stringhe *)
-             |  REFOF <set>			   (* insieme riferimenti *)
-             |  <rvar>.<vvar>                      (* variabile per insieme
-						      stringhe, relativa a 
-						      riferimento *)
+	     |  <quoted-constant-string>       (* stringa singoletto *)
+             |  {<quoted-constant-string-list>}(* insieme stringhe *)
+             |  REFOF <set>		       (* insieme riferimenti *)
+             |  <rvar>.<vvar>                  (* variabile per insieme
+				                  stringhe, relativa a 
+					          riferimento *)
    	     |  <function> <quoted-constant-string> <string-set> 
-						   (* applicazione di funzione
-						      specificata a riferimento
-						      o insiemi di rif. o var*)
+					       (* applicazione di funzione
+						  specificata a riferimento
+						  o insiemi di rif. o var*)
+             |  <vvar>			       (* vvar introduced by LET *)
 
 <quoted-constant-string-list> := <quoted-constant-string>
 			      |  <quoted-constant-string> , <quoted-constant-string-list>				                  
@@ -68,12 +77,11 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
 <function> := FUN			   (* funzione generale *)
 	   |  <property>	
 
-<property> := ATTRIBUTE		           (* funzione proprieta': restituisce
-					      suoi  valori*)
-           |  SUBATTR			   (* restituisce valori proprieta' e 
-					      sotto-proprieta' di *) 
-           |  SUPERATTR			   (* restituisce valori proprieta' e 
-					      super-proprieta' di *)
+<property> := ATTRIBUTE	<refine-op>	   (* funzione proprieta': restituisce
+					      suoi valori (anche strutturati)
+					      (e delle sotto-proprieta' o 
+				              super-proprieta' *)
+
 
 <rvar> := @ <not-reserved-identifier>          (* variabile per riferimento *)
 <vvar> := $ <not-reserved-identifier>          (* variabile per insiemi 
@@ -99,7 +107,7 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
 - REF aumenta performance perche' NON accede al data base (costoso).
 - l'argomento di PATTERN ha sintassi di una espressione regolare 
   POSIX 1003.2-1992
-- Possibile <function> (<quoted-constant-string>):
+- Possibile FUN (<quoted-constant-string>):
   NAME (* URIREF -> nome_oggetto *)
 - MEET aumenta performance nel caso si verifichi (a in S) oppure 
   (b in S) = ({a,b} meet S) perche' valuta S una volta sola
diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index 63c014565..3cf73eba6 100644
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -52,7 +52,7 @@
 
 <!-- MathQL query expression declaration -->
 
-<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetIn|Relation|
+<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetSIn|LetVIn|Relation|
                      Union|Intersect|Diff)'>
 
 <!-- MathQL boolean expression declaration -->
@@ -63,8 +63,7 @@
 
 <!ENTITY % functexpr '(FUN|PROPERTY)'>
 
-<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|%functexpr;)'>
-
+<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|VVAR|%functexpr;)'>
 
 <!-- MathQL query top-element -->
 
@@ -86,12 +85,13 @@
 
 <!ELEMENT Select (In, Where)>
 
-<!ELEMENT LetIn (%setexpr;, Target)>
+<!ELEMENT LetSIn (%setexpr;, Starget)>
+
+<!ELEMENT LetVIn (%stringsetexpr;, Vtarget)>
 
 <!ELEMENT Relation (Refine?,%setexpr;, Attr+)>
 <!ATTLIST Relation
-          name CDATA #REQUIRED
-          refine (sub|super) #IMPLIED>
+          name CDATA #REQUIRED>
 
 <!ELEMENT Union (%setexpr;, %setexpr;)>
 
@@ -107,14 +107,20 @@
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
-<!ELEMENT Target %setexpr;>
-<!ATTLIST Target
+<!ELEMENT Starget %setexpr;>
+<!ATTLIST Starget
           svar CDATA #REQUIRED>
 
+<!ELEMENT Vtarget %setexpr;>
+<!ATTLIST Vtarget
+          vvar CDATA #REQUIRED>
+
 <!ELEMENT Attr EMPTY>
 <!ATTLIST Attr 
           binder CDATA #REQUIRED>
 
+<!ELEMENT Refine (SUB|SUPER|CONST+)>
+
 <!-- MathQL boolean expressions -->
 
 <!ELEMENT BOOL EMPTY>
@@ -143,6 +149,8 @@
 
 <!ELEMENT REFOF %setexpr;>
 
+<!ELEMENT VVAR %stringsetexpr;>
+
 <!ELEMENT BINDER (Rvar)>
 <!ATTLIST BINDER
           name CDATA #REQUIRED>
@@ -151,7 +159,6 @@
 <!ATTLIST FUN
           name CDATA #REQUIRED>
 
-<!ELEMENT PROPERTY %stringsetexpr;>
+<!ELEMENT PROPERTY (Refine?,%stringsetexpr;)>
 <!ATTLIST PROPERTY
-          name CDATA #REQUIRED
-          refine (sub|super) #IMPLIED>
\ No newline at end of file
+          name CDATA #REQUIRED>