matita/matita/contribs/lambdadelta/bin/roles/rolesParser.mly

   1 /*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ */
  11
  12 %{
  13   module EU = RolesUtils
  14   module ET = RolesTypes
  15 %}
  16
  17 %token EOF SC OP CP VER OLD NEW REL BASE TOP ROLES
  18 %token <string> TEXT
  19
  20 %start status
  21 %type <RolesTypes.status> status
  22
  23 %%
  24
  25 stage:
  26   | TEXT { EU.stage_of_string $1 }
  27 ;
  28
  29 oobj:
  30   | TEXT { EU.oobj_of_string $1 }
  31 ;
  32
  33 nobj:
  34   | TEXT { EU.nobj_of_string $1 }
  35 ;
  36
  37 robj:
  38   | OP REL ver olds news CP {
  39       {ET.rb = false; ET.rx = false; ET.rs = $3; ET.ro = $4; ET.rn = $5}
  40     }
  41 ;
  42
  43 oobjs:
  44   |            { []       }
  45   | oobj oobjs { $1 :: $2 }
  46 ;
  47
  48 nobjs:
  49   |            { []       }
  50   | nobj nobjs { $1 :: $2 }
  51 ;
  52
  53 robjs:
  54   |            { []       }
  55   | robj robjs { $1 :: $2 }
  56 ;
  57
  58 ver:
  59   | OP VER stage CP { $3 }
  60 ;
  61
  62 olds:
  63   | OP OLD oobjs CP { $3 }
  64 ;
  65
  66 news:
  67   | OP NEW nobjs CP { $3 }
  68 ;
  69
  70 base:
  71   | OP BASE robjs CP { $3 }
  72 ;
  73
  74 status:
  75   | ROLES SC OP TOP base ver olds news CP EOF {
  76       {ET.sm = false; ET.sr = $5; ET.ss = $6; ET.so = $7; ET.sn = $8}
  77     }
  78 ;