// -*- sugar -*-

p:                                      // program
= De: d* e
| Dm: d* m
;
        
dt: d* t;                               // top-level type
d: 'def' ao ++ ',' '.';                 // top-level definition

e:                                      // expression
> Run: 'run' xm ++ ',' 'in' e
= Ret: 'return' m
;
        
m:                                      // term
> Case: 'case' m 'of' '|'? m ++ '|'
| If: 'if' m 'then' m 'else' m
| Ifsub: 'if' m '<:' m 'then' m 'else' m
| Ifcert: 'if' m '=>' m '#>' m 'then' m 'else' m
| Fun: 'fun' xt ++ ',' '.' m
| Poly: 'poly' ab ++ ',' '.' m
| Pack: 'pack' m 'with' t ++ ',' 'as' t
| Open: 'open' x '=' m 'with' a ++ ',' 'in' m
| Let: 'let' xm ++ ',' 'in' m
| Match: 'let' '<' x ++ ',' '>' '=' m 'in' m
| Del: 'delegate' m '<:' m 'in' m
| Effect: '{' t ++ ',' '}' e
| Bind: 'bind' xm ++ ',' 'in' m
| Rep: '\'' t	
| Acq: 'acquire' m '#>' m
| Dcls: 'declassify' m 'as' t
| Cert: 'Cert' '(' t ',' t ')'
| Seq: m ';' m
< Inj: m '@' i 'as' t 
< Eq: m '=' m
< Add: m '+' m
| Sub: m '-' m
< App: m m
> Esc: '\\' m
< Inst: m '[' t ++ ',' ']'
< Prj: m '.' i
< Label: m '{' t ++ ',' '}'
=  Atom: '(' m ')'
| True: 'true'
| False: 'false'
| Int: i
| Str: str
| Prod: '<' m ** ',' '>'
| Id: x
| Error: 'error' str
;


t:                                      // type
> Tall: 'all' ab ++ ',' '.' t
| Tsome: 'some' ab ++ ',' '.' t
| Teffect: '{' t ++ ',' '}' t
| Trep: '\'' t
| Tread: 'R' t+
| Ttrust: 'T' t+
| Tdel: 'delegate' t
| Tdcls: 'declassify' t?
> Tfun: t '->' t 
> Tmeet: t '&' t
> Tjoin: t '#' t
> Tsum: t '+' t
< Tlabel: t '{' t ++ ',' '}'
= Tatom: '(' t ')'
| Ttop: 'top'
| Tbot: 'bot'
| Tbool: 'bool'
| Tint: 'int'
| Tstr: 'string'
| Tcert: 'cert'
| Tprod: '<' t ** ',' '>'
| Tid: a
;

xt: x ':' t;                            // variable binding
xm: x '=' m;                            // let binding of term
xe: x '=' e;                            // let binding of exp
x: id;                                  // term variable 
a: id;                                  // type variable
i: num;                                 // integer
ab: a b;                                // type bound
ao: a o;                                // type order
       
b:                                      // bound
= Btop:
| Bsub: '<:' t
;

o:                                      // order
= Otop:
| Osub: '<:' t
| Oeq: '=' t
;