X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql%2FmQueryTParser.mly;fp=helm%2Focaml%2Fmathql%2FmQueryTParser.mly;h=0000000000000000000000000000000000000000;hb=869549224eef6278a48c16ae27dd786376082b38;hp=1ebadd29a53ea356fe8f283a4a3d26c18e35b208;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8;p=helm.git diff --git a/helm/ocaml/mathql/mQueryTParser.mly b/helm/ocaml/mathql/mQueryTParser.mly deleted file mode 100644 index 1ebadd29a..000000000 --- a/helm/ocaml/mathql/mQueryTParser.mly +++ /dev/null @@ -1,202 +0,0 @@ -/* 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 */ -/* 23/05/2002 */ -/* */ -/* */ -/******************************************************************************/ - -%{ - let analyze x = - let module M = MathQL in - let rec join l1 l2 = match l1, l2 with - | [], _ -> l2 - | _, [] -> l1 - | s1 :: tl1, s2 :: _ when s1 < s2 -> s1 :: join tl1 l2 - | s1 :: _, s2 :: tl2 when s2 < s1 -> s2 :: join l1 tl2 - | s1 :: tl1, s2 :: tl2 -> s1 :: join tl1 tl2 - in - let rec an_val = function - | M.Const _ -> [] - | M.VVar _ -> [] - | M.Record (rv, _) -> [rv] - | M.Fun (_, x) -> an_val x - | M.Property (_, _, _, x) -> an_val x - | M.RefOf x -> an_set x - and an_boole = function - | M.False -> [] - | M.True -> [] - | M.Ex _ -> [] - | M.Not x -> an_boole x - | M.And (x, y) -> join (an_boole x) (an_boole y) - | M.Or (x, y) -> join (an_boole x) (an_boole y) - | M.Sub (x, y) -> join (an_val x) (an_val y) - | M.Meet (x, y) -> join (an_val x) (an_val y) - | M.Eq (x, y) -> join (an_val x) (an_val y) - and an_set = function - | M.SVar _ -> [] - | M.RVar _ -> [] - | M.Relation (_, _, _, x, _) -> an_set x - | M.Pattern x -> an_val x - | M.Ref x -> an_val x - | M.Union (x, y) -> join (an_set x) (an_set y) - | M.Intersect (x, y) -> join (an_set x) (an_set y) - | M.Diff (x, y) -> join (an_set x) (an_set y) - | M.LetSVar (_, x, y) -> join (an_set x) (an_set y) - | M.LetVVar (_, x, y) -> join (an_val x) (an_set y) - | M.Select (_, x, y) -> join (an_set x) (an_boole y) - in - an_boole x - - let path_of_vvar v = (v, []) -%} - %token ID STR - %token SL IS LC RC CM SC LP RP AT PC DL FS DQ GETS EOF - %token AND ATTR BE DIFF EQ EX FALSE FUN IN INTER INV LET MEET NOT OR PAT - %token PROP REF REFOF REL SELECT SUB SUPER TRUE UNION WHERE - %left DIFF WHERE REFOF - %left OR UNION - %left AND INTER - %nonassoc REL - %nonassoc NOT EX IN ATTR - - %start qstr query result - %type qstr - %type query - %type result -%% - qstr: - | DQ { "" } - | STR qstr { $1 ^ $2 } - ; - svar: - | PC ID { $2 } - ; - rvar: - | AT ID { $2 } - ; - vvar: - | DL ID { $2 } - ; - strs: - | STR CM strs { $1 :: $3 } - | STR { [$1] } - ; - subpath: - | STR SL subpath { $1 :: $3 } - | STR { [$1] } - ; - path: - | STR SL subpath { ($1, $3) } - | STR { ($1, []) } - ; - inv: - | INV { true } - | { false } - ; - ref: - | SUB { MathQL.RefineSub } - | SUPER { MathQL.RefineSuper } - | { MathQL.RefineExact } - ; - assign: - | vvar GETS path { (path_of_vvar $1, $3) } - ; - assigns: - | assign CM assigns { $1 :: $3 } - | assign { [$1] } - ; - val_exp: - | STR { MathQL.Const [$1] } - | FUN STR val_exp { MathQL.Fun ($2, $3) } - | PROP inv ref path val_exp { MathQL.Property ($2, $3, $4, $5) } - | rvar FS vvar { MathQL.Record ($1, path_of_vvar $3) } - | vvar { MathQL.VVar $1 } - | LC strs RC { MathQL.Const $2 } - | LC RC { MathQL.Const [] } - | REFOF set_exp { MathQL.RefOf $2 } - | LP val_exp RP { $2 } - ; - boole_exp: - | TRUE { MathQL.True } - | FALSE { MathQL.False } - | LP boole_exp RP { $2 } - | NOT boole_exp { MathQL.Not $2 } - | EX boole_exp { MathQL.Ex (analyze $2) $2 } - | val_exp SUB val_exp { MathQL.Sub ($1, $3) } - | val_exp MEET val_exp { MathQL.Meet ($1, $3) } - | val_exp EQ val_exp { MathQL.Eq ($1, $3) } - | boole_exp AND boole_exp { MathQL.And ($1, $3) } - | boole_exp OR boole_exp { MathQL.Or ($1, $3) } - ; - set_exp: - | REF val_exp { MathQL.Ref $2 } - | PAT val_exp { MathQL.Pattern $2 } - | LP set_exp RP { $2 } - | SELECT rvar IN set_exp WHERE boole_exp { MathQL.Select ($2, $4, $6) } - | REL inv ref path val_exp ATTR assigns { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, $7) } - | REL inv ref path val_exp { MathQL.Relation ($2, $3, $4, MathQL.Ref $5, []) } - | svar { MathQL.SVar $1 } - | rvar { MathQL.RVar $1 } - | set_exp UNION set_exp { MathQL.Union ($1, $3) } - | set_exp INTER set_exp { MathQL.Intersect ($1, $3) } - | set_exp DIFF set_exp { MathQL.Diff ($1, $3) } - | LET svar BE set_exp IN set_exp { MathQL.LetSVar ($2, $4, $6) } - | LET vvar BE val_exp IN set_exp { MathQL.LetVVar ($2, $4, $6) } - ; - query: - | set_exp EOF { $1 } - ; - attr: - | vvar IS strs { (path_of_vvar $1, $3) } - | vvar { (path_of_vvar $1, []) } - ; - attrs: - | attr SC attrs { $1 :: $3 } - | attr { [$1] } - ; - group: - LC attrs RC { $2 } - ; - groups: - | group CM groups { $1 :: $3 } - | group { [$1] } - ; - resource: - | STR ATTR groups { ($1, $3) } - | STR { ($1, []) } - ; - resources: - | resource SC resources { $1 :: $3 } - | resource { [$1] } - | { [] } - ; - result: - | resources EOF { $1 }