]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql/mQueryTParser.mly
textual parser and other utilities for mathql
[helm.git] / helm / ocaml / mathql / mQueryTParser.mly
diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly
new file mode 100644 (file)
index 0000000..dea5f48
--- /dev/null
@@ -0,0 +1,119 @@
+/* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ */
+
+/******************************************************************************/
+/*                                                                            */
+/*                               PROJECT HELM                                 */
+/*                                                                            */
+/*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   */
+/*                                 23/05/2002                                 */
+/*                                                                            */
+/*                                                                            */
+/******************************************************************************/
+
+%{
+   open MathQL
+%}
+   %token    <string> ID STR
+   %token    <MathQL.mqtref> REF
+   %token    LPR RPR DLR SQT DQT EOF PROT SLASH FRAG QUEST STAR SSTAR 
+   %token    NAME
+   %token    MCONCL CONCL
+   %token    TRUE FALSE AND OR NOT IS
+   %token    SELECT IN WHERE USE POS USEDBY PATT UNION INTER
+   %left     OR UNION
+   %left     AND INTER
+   %nonassoc NOT
+   %start    qstr ref query
+   %type     <string>        qstr   
+   %type     <MathQL.mqtref> ref   
+   %type     <MathQL.mquery> query   
+%%
+   prot:
+      | STR  { Some $1 }
+      | STAR { None }
+   ;
+   body:
+      |            { []            }
+      | SLASH body { MQBD :: $2    }
+      | QUEST body { MQBQ :: $2    }
+      | SSTAR body { MQBSS :: $2   }
+      | STAR body  { MQBS :: $2    }
+      | STR body   { MQBC $1 :: $2 } 
+   frag:
+      |                  { []          }
+      | SLASH SSTAR frag { MQFSS :: $3 }
+      | SLASH STAR frag  { MQFS :: $3  }
+      | SLASH STR frag   { try let i = int_of_string $2 in
+                               if i < 1 then raise Parsing.Parse_error;
+                              MQFC i :: $3
+                          with e -> raise Parsing.Parse_error
+                         }
+   ;
+   ref:
+      | prot PROT body DQT           { ($1, $3, []) }
+      | prot PROT body FRAG frag DQT { ($1, $3, $5) }
+   ;   
+   qstr:
+      | STR SQT { $1 }
+   ;
+   rvar:
+      | ID { $1 }
+   ;
+   svar:
+      | DLR ID { $2 }
+   ;
+   func:
+      | NAME { MQName }
+   ;   
+   str:
+      | MCONCL    { MQMConclusion   }
+      | CONCL     { MQConclusion    }
+      | STR       { MQCons $1       } 
+      | rvar      { MQRVar $1       }
+      | svar      { MQSVar $1       }
+      | func rvar { MQFunc ($1, $2) }
+   ;
+   boole:
+      | TRUE            { MQTrue         }
+      | FALSE           { MQFalse        }
+      | str IS str      { MQIs ($1, $3)  }
+      | NOT boole       { MQNot $2       }
+      | boole AND boole { MQAnd ($1, $3) }
+      | boole OR boole  { MQOr ($1, $3)  }
+      | LPR boole RPR   { $2             }
+   ;   
+   rlist:
+      | PATT REF                         { MQPattern $2          } 
+      | rlist UNION rlist                { MQUnion ($1, $3)      }
+      | rlist INTER rlist                { MQIntersect ($1, $3)  }
+      | USE rlist POS svar               { MQUse ($2, $4)        }
+      | USEDBY rlist POS svar            { MQUsedBy ($2, $4)     }
+      | SELECT rvar IN rlist WHERE boole { MQSelect ($2, $4, $6) }
+      | LPR rlist RPR                    { $2                    }
+   ;
+   query:
+      rlist EOF { MQList $1 }
+   ;