From: Irene Schena Date: Tue, 28 May 2002 16:05:50 +0000 (+0000) Subject: Modified Files: X-Git-Tag: V_0_3_0_debian_8~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=b2aca35e823328d93ddc3f76a4c0af60a0c2bde8 Modified Files: 1) grammar.txt: added SUBSET, SETEQUAL, REFERENCE and rvar in --- 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 (* unione costruttori della lista oggetti*) | PATTERN (* espansione del pattern *) + | REFERENCE (* oggetto referenziato *) | INTHEORY ITEMTYPE (* unione oggetti lista teorie *) | THEORYREFTO (* unione teorie che fanno riferimento a lista oggetti *) @@ -23,6 +24,7 @@ MATHEMATICAL QUERY LANGUAGE (MathQL) classi e loro superclassi *) | OFSUBTYPE (* unione oggetti in base a classi e loro sottoclassi *) + | (* valore della var*) := ( ) (* parentesizzazione *) | AND (* congiunzione *) @@ -31,9 +33,11 @@ MATHEMATICAL QUERY LANGUAGE (MathQL) | TRUE (* vero *) | FALSE (* falso *) | IS (* case sensitive matching *) - | EQUAL (* uguaglianza tra liste *) + | SETEQUAL (* uguaglianza tra liste *) + | SUBSET (* operazione di sottoinsieme *) := <"-quoted-constant-string> (* pattern costante *) + := <'-quoted-constant-string> (* riferimento costante *) := <'-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 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