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

diff --git a/helm/mathql/grammar.txt b/helm/mathql/grammar.txt
deleted file mode 100644
index 7bdd67c3a..000000000
--- a/helm/mathql/grammar.txt
+++ /dev/null
@@ -1,135 +0,0 @@
-GRAMMATICA PER QUERY SU DOCUMENTI MATEMATICI
-MATHEMATICAL QUERY LANGUAGE (MathQL) 
-
-<query> := <list>                              (* clausola iniziale *)
-
-<list> := ( <list> )                           (* parentesizazione *)
-       |  <list> UNION <list>                  (* unione *)
-       |  <list> INTERSECT <list>              (* intersezione *)
-       |  <list> DIFF <list>                   (* differenza *)
-       |  SELECT <rvar> IN <list> WHERE <bool> (* selezione *)
-       |  EXISTS <rvar> IN <list> WHERE <bool> (* esistenziale *)
-       |  USE <list> POSITION <svar>           (* unione lista backward *)
-       |  USEDBY <list> POSITION <svar>        (* unione lista forward *)
-       |  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 *)
-       |  <list> OFTYPE <svar>		       (* unione oggetti in base a 
-                                                  classi *)
-       |  <list> OFSUPERTYPE <svar>	       (* unione oggetti in base a 
-                                                  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 *)
-       |  <bool> OR <bool>                     (* disgiunzione *)
-       |  NOT <bool>                           (* negazione *)
-       |  TRUE                                 (* vero *)
-       |  FALSE                                (* falso *)
-       |  <string> IS <string>                 (* case sensitive matching *)
-       |  <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 *)
-         |  MAINCONCLUSION | MAINHYPOTHESIS
-         |  <rvar>                             (* variabile *)
-	 |  <svar>			       (* variabile *)
-	 |  <function> <rvar>                  (* applicazione di funzione *)
-	 
-<function> := NAME			       (* URIREF -> nome_oggetto *)
-	   |  <property>
-
-<property> := THEORY                           (* URIREF -> valore_Proprieta' *)
-           |  TITLE			       (* URIREF -> valore_Prop_DC *)
-           |  CONTRIBUTOR
-           |  CREATOR
-           |  PUBLISHER
-           |  SUBJECT
-           |  DESCRIPTION
-           |  DATE
-           |  TYPE
-           |  FORMAT
-           |  IDENTIFIER
-           |  LANGUAGE
-           |  RELATION
-           |  SOURCE
-           |  COVERAGE
-           |  RIGHTS
-	   |  INSTITUTION
-	   |  CONTACT
-	   |  FIRSTVERSION
-	   |  MODIFIED
-           |  <refineprop> <property>
-
-<refineprop> := SUB			       (* proprieta' e sotto-proprieta'
-                                                  di *) 
-             |  SUPER			       (* proprieta' e super-proprieta'
-                                                  di *)
-
-<rvar> := <not-reserved-identifier>            (* variabile per risorse *)
-<svar> := $ <not-reserved-identifier>          (* variabile per stringhe *)
-
-- () = lista vuota (?)
-- 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 
-- 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 rvar
-- Note su <pattern>
-  Contiene un'espressione regolare per selezionare delle "reference" 
-  (cioe` delle uri eventualmente seguite da un fragment identifier)
-  L'espressione regolare contiene i seguenti costrutti:
-
-  costrutto        semanticamente fa match con                       
-  ?                un singolo carattere diverso da / # :             
-  *                la piu' lunga sottostringa che non contiene / # : 
-  **               la piu' lunga sottostringa che non contiene # :
-  altro carattere  solo se' stesso
-
-  costrutto        puo' appareire in
-  ?                "body"
-  *                dovunque
-  **               "body" e "fragment"
-  altro carattere  dovunque
-
-  "body"     parte compresa fra le occorrenze di ":/" e "#1" escluse
-  "fragment" parte successiva all'occorrenza "#1"
-- FUTURO: operatore di ordinamento sul risultato finale della query.
-  <query> SORTEDBY <order> <function>   (* unione lista ordinata secondo
-                                           ordine e valore funzione *)
-  <order>    := DESC                           (* ordinamento decrescente *)
-	     |  ASC			       (* ordinamento crescente *)     
-  DTD:
-  <!ENTITY % order '(ascendant|descendant)'>
-  <!ELEMENT Query %queryexpr;>
-  <!ELEMENT SortBy (Query, SortField)>
-  <!ELEMENT SortField %functexpr;>
-  <!ATTLIST SortField 
-            order %order; #IMPLIED>
-- RILASSAMENTO degli operatori UNION e INTERSECT. Operatori fuzzy con 
-  introduzione di pesi associati ai risultati.
\ No newline at end of file