cime-theory.opp.exp 1.28 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
%{
  
  open User_signatures
  open Term_algebra

%}
%start theory
%token SEMICOLON
%token OPENPAR
%token KW_BR
%token KW_AG
%token KW_ACUN
%token KW_ACU
%token KW_ACI
%token <int> INT
%token <User_signatures.symbol_id> IDENT
%token EOF
%token COMMA
%token CLOSEPAR

%type <User_signatures.symbol_id Theory.elem_theory list> theory
%%

theory:
25 26 27 28 29 30 31 32 33 34
| _1 = EOF
    {      ( [] )}
| _1 = decl
    {      ( 
        [_1]
      )}
| _1 = decl _2 = SEMICOLON _3 = theory
    {      ( 
	_1 :: _3 
      )}
35 36

decl:
37 38 39 40 41 42 43 44 45 46
| _1 = acu
    {      ( _1 )}
| _1 = aci
    {      ( _1 )}
| _1 = ag
    {     ( _1 )}
| _1 = acun
    {       ( _1 )}
| _1 = br
    {     ( _1 )}
47 48

acu:
49 50 51 52
| _1 = KW_ACU _2 = OPENPAR _3 = IDENT _4 = COMMA _5 = IDENT _6 = CLOSEPAR
    {  ( 
    Theory.ACU(_3,_5)
  )}
53 54

aci:
55 56 57 58
| _1 = KW_ACI _2 = OPENPAR _3 = IDENT _4 = CLOSEPAR
    {  ( 
    Theory.ACI(_3)
  )}
59 60

ag:
61 62 63 64
| _1 = KW_AG _2 = OPENPAR _3 = IDENT _4 = COMMA _5 = IDENT _6 = COMMA _7 = IDENT _8 = CLOSEPAR
    {  ( 
    Theory.AG(_3,_5,_7)
  )}
65 66

acun:
67 68 69 70
| _1 = KW_ACUN _2 = OPENPAR _3 = IDENT _4 = COMMA _5 = IDENT _6 = COMMA _7 = INT _8 = CLOSEPAR
    {  ( 
    Theory.ACUN(_3,_5,_7)
  )}
71 72

br:
73 74 75 76
| _1 = KW_BR _2 = OPENPAR _3 = IDENT _4 = COMMA _5 = IDENT _6 = COMMA _7 = IDENT _8 = COMMA _9 = IDENT _10 = CLOSEPAR
    {  ( 
    Theory.BR(_3,_5,_7,_9)
  )}
77 78 79 80 81

%%