X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fmathql_test%2FmQGTopParser.mly;fp=helm%2Fmathql_test%2FmQGTopParser.mly;h=0000000000000000000000000000000000000000;hp=3e260d88f03cb7a1eed2d0a8cc80a3f3bda2ff5e;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/mathql_test/mQGTopParser.mly b/helm/mathql_test/mQGTopParser.mly deleted file mode 100644 index 3e260d88f..000000000 --- a/helm/mathql_test/mQGTopParser.mly +++ /dev/null @@ -1,107 +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/. - */ - -/* AUTOR: Ferruccio Guidi - */ - -%{ - let f (x, y, z) = x - let s (x, y, z) = y - let t (x, y, z) = z - - module T = MQGTypes - module U = MQGUtil -%} - %token ID - %token CONURI - %token VARURI - %token INDTYURI - %token INDCONURI - %token ALIAS EOF - - %start interp - %type CicTextualParser0.interpretation_codomain_item option> interp - - %token STR - %token DL DQ LC RC CM - %token MOBJ MSORT MREL OOBJ OSORT OREL UNIV - - %start qstr specs - %type qstr - %type specs -%% - uri: - | CONURI { CicTextualParser0.ConUri $1 } - | VARURI { CicTextualParser0.VarUri $1 } - | INDTYURI { CicTextualParser0.IndTyUri ((fst $1), (snd $1)) } - | INDCONURI { CicTextualParser0.IndConUri ((f $1), (s $1), (t $1)) } - ; - alias: - | ALIAS ID uri { ($2, CicTextualParser0.Uri $3) } - ; - aliases: - | alias aliases { $1 :: $2 } - | EOF { [] } - ; - interp: - | aliases { function CicTextualParser0.Id s -> (try Some (List.assoc s $1) - with Not_found -> None) - | _ -> None } - ; - - qstr: - | DQ { "" } - | STR qstr { $1 ^ $2 } - ; - strs: - | STR CM strs { $1 :: $3 } - | STR { [$1] } - | { [] } - ; - uri_list: - | LC strs RC { List.map U.uri_of_mathql $2 } - ; - sort_list: - | LC strs RC { List.map U.sort_of_mathql $2 } - ; - pos_list: - | LC strs RC { List.map U.position_of_mathql $2 } - ; - depth_list: - | LC strs RC { List.map U.depth_of_mathql $2 } - ; - spec: - | MOBJ uri_list pos_list depth_list { T.MustObj ($2, $3, $4) } - | MSORT sort_list pos_list depth_list { T.MustSort ($2, $3, $4) } - | MREL pos_list depth_list { T.MustRel ($2, $3) } - | OOBJ uri_list pos_list depth_list { T.OnlyObj ($2, $3, $4) } - | OSORT sort_list pos_list depth_list { T.OnlySort ($2, $3, $4) } - | OREL pos_list depth_list { T.OnlyRel ($2, $3) } - | UNIV pos_list { T.Universe $2 } - ; - specs: - | spec specs { $1 :: $2 } - | EOF { [] } - ;