From: Irene Schena <irene.schena@unibo.it>
Date: Fri, 19 Apr 2002 15:38:22 +0000 (+0000)
Subject: Added Files:
X-Git-Tag: V_0_3_0_debian_8~135
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=797425e905a9d26bb21f18d234a34ed211bcf92c;p=helm.git

Added Files:
1) grammar.txt: grammar of the Mathematical Query Language
---

diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt
new file mode 100644
index 000000000..03f6a2c66
--- /dev/null
+++ b/helm/mathql/grammar.txt
@@ -0,0 +1,95 @@
+GRAMMATICA PER QUERY SU DOCUMENTI MATEMATICI- VERSIONE 2002-04-19 #1Irene
+MATHEMATICAL QUERY LANGUAGE (MathQL) 
+
+<query> := <list>                              (* clausola iniziale *)
+
+<list> := ( <list> )                           (* parentesizazione *)
+       |  <list> UNION <list>                  (* unione *)
+       |  <list> INTERSECT <list>              (* intersezione *)
+       |  <list> DIFF <list>                   (* differenza *)
+       |  <list> SORTEDBY <order>
+       |  SELECT <pvar> IN <list> WHERE <bool> (* selezione *)
+       |  EXISTS <pvar> IN <list> WHERE <bool> (* esistenziale *)
+       |  USE <list> POSITION <svar>           (* unione lista backward *)
+       |  USEDBY <list> POSITION <svar>        (* unione lista forward *)
+       |  CONTRUCTORS <list>
+       |  PATTERN <pattern>                    (* espansione del pattern *)
+       |  INTHEORY <list> ITEMTYPE <svar>      (* unione oggetti lista teorie *)
+       |  THEORYREFTO <list>                   (* unione teorie che fanno 
+                                                 riferimento a lista oggetti *)
+
+<bool> := ( <bool> )                           (* parentesizazione *)
+       |  <bool> AND <bool>                    (* congiunzione *)
+       |  <bool> OR <bool>                     (* disgiunzione *)
+       |  NOT <bool>                           (* negazione *)
+       |  TRUE                                 (* vero *)
+       |  FALSE                                (* falso *)
+       |  <string> IS <string>                 (* case sensitive matching *)
+       
+<pattern> := <quoted-constant-string>          (* pattern costante *)
+          
+<string> := <quoted-constant-string>           (* costante letterale *)
+         |  CONCLUSION | HYPOTHESIS | BODY     (* costanti simboliche *)
+         |  MAINCONCLUSION | MAINHYPOTHESIS
+         |  <pvar>                             (* variabile *)
+	 |  <svar>			       (* variabile *)
+	 |  <function> <pvar>                  (* applicazione di funzione *)
+	 
+<function> := NAME			       (* pvar -> nome_oggetto *)
+           |  TITLE			       (* URI -> valore_Prop_DC *)
+           |  CONTRIBUTOR
+           |  CREATOR
+           |  PUBLISHER
+           |  SUBJECT
+           |  DESCRIPTION
+           |  DATE
+           |  TYPE
+           |  FORMAT
+           |  IDENTIFIER
+           |  LANGUAGE
+           |  RELATION
+           |  SOURCE
+           |  COVERAGE
+           |  RIGHTS
+	   |  INSTITUTION
+	   |  CONTACT
+	   |  FIRSTVERSION
+	   |  MODIFIED
+           |  <refineop> <function>
+
+<refineop> := SUB			       (* sub-property of *) 
+           |  SUPER			       (* super-property of *)
+
+<order>    := THEORY                           (* ordinamento alfabetico in 
+                                                  base a teorie e default per
+					          gli oggetti *)
+	   |  ASC			       (* ordinamento crescente *) 
+	   |  DESC                             (* ordinamento decrescente *) 
+	   |  KEY			       (* ordinamento in base a parole
+                                                  chiave o soggetto *)
+
+<pvar> := <not-reserved-identifier>            (* variabile per pattern  *)
+<svar> := $ <not-reserved-identifier>          (* variabile per stringhe *)
+
+- le stringhe sono "case sensitive" 
+- la funzione non definita sull'argomento restituisce la stringa nulla
+- le <pvar> si presuppongono essere istanziate come URI complete o
+  URI#xpointer_expression 
+- ogni binding lega una variabile libera (nuova) 
+- Precedenza operatori:
+  NOT (+)  DIFF
+  AND      INTERSECT
+  OR  (-)  UNION
+- Possibili tipi di RELATION e DEPENDENCE sono rappresentati dalle loro
+  subproperties
+- FUTURO: thesauri di parole e sinonimi per ricerche testuali, ordinamenti sui 
+  risultati, caratteri jolly. Una volta reperito l'oggetto si possono 
+  visualizzare le info associate. 
+- FUTURO: in output numeri ad esempio a fini statistici, aggiungendo anche 
+  operatori aritmetici e di confronto (< = >). Es. Quante proofs di un certo 
+  teorema ci sono? 
+- L'ordinamento di default e' quello alfabetico crescente in base al nome 
+  delle pvar
+ 
+
+