X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fgrammar.txt;fp=helm%2Fmathql%2Fgrammar.txt;h=7bdd67c3aeec2efab71c1cde13d1859ad6fab4e5;hb=b2aca35e823328d93ddc3f76a4c0af60a0c2bde8;hp=2c53c2a1d07d4118ba6498a5aed968810afce66c;hpb=1bcce271566f8b2c2efdeb2283ebf210f6fcc6f1;p=helm.git

diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt
index 2c53c2a1d..7bdd67c3a 100644
--- a/helm/mathql/grammar.txt
+++ b/helm/mathql/grammar.txt
@@ -14,6 +14,7 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
        |  CONTRUCTORS <list>                   (* unione costruttori della 
 						  lista oggetti*)
        |  PATTERN <pattern>                    (* espansione del pattern *)
+       |  REFERENCE <reference>                (* oggetto referenziato *)
        |  INTHEORY <list> ITEMTYPE <svar>      (* unione oggetti lista teorie *)
        |  THEORYREFTO <list>                   (* unione teorie che fanno 
                                                  riferimento a lista oggetti *)
@@ -23,6 +24,7 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
                                                   classi e loro superclassi *)
        |  <list> OFSUBTYPE <svar>	       (* unione oggetti in base a 
                                                   classi e loro sottoclassi *)
+       |  <rvar>			       (* valore della var*)
 
 <bool> := ( <bool> )                           (* parentesizzazione *)
        |  <bool> AND <bool>                    (* congiunzione *)
@@ -31,9 +33,11 @@ MATHEMATICAL QUERY LANGUAGE (MathQL)
        |  TRUE                                 (* vero *)
        |  FALSE                                (* falso *)
        |  <string> IS <string>                 (* case sensitive matching *)
-       |  <list> EQUAL <list>                  (* uguaglianza tra liste *)
+       |  <list> SETEQUAL <list>               (* uguaglianza tra liste *)
+       |  <list> SUBSET <list>		       (* operazione di sottoinsieme *)  
        
 <pattern> := <"-quoted-constant-string>        (* pattern costante *)
+<reference> := <'-quoted-constant-string>      (* riferimento costante *)
           
 <string> := <'-quoted-constant-string>         (* costante letterale *)
          |  CONCLUSION | HYPOTHESIS | BODY     (* costanti simboliche *)
@@ -79,8 +83,8 @@ 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 references costituite
-  da un URI e da un fragment identifier opzionalecomplete; esse identificano 
-  risorse 
+  da un URI e da un fragment identifier opzionale complete; i riferimenti 
+  identificano risorse 
 - ogni binding lega una variabile libera (nuova) 
 - Precedenza operatori:
   NOT (+)  DIFF