link.opp.exp 1.35 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 25
%{
  open Structures
%}
%start main
%token VDASH
%token <string> VAR
%token RIMP
%token OP
%token LIMP
%token IMP
%token END
%token DIRECTIVE
%token CP
%token SEQ
%token PAR
%token TIMES
%token NEXT
%token NEG
%left SEQ PAR 
%left TIMES NEXT 
%nonassoc NEG 
%type <[`Directive of string | `Sequent of Structures.sequent]> main
%%

main:
26 27 28 29
| _1 = sequent _2 = END
    {              (`Sequent _1)}
| _1 = DIRECTIVE _2 = VAR
    {                (`Directive _2)}
30 31

formimp:
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
| _1 = VAR
    {       (`Var _1)}
| _1 = formimp _2 = PAR _3 = formimp
    {                      (`Par(_1,_3))}
| _1 = formimp _2 = TIMES _3 = formimp
    {                        (`Times(_1,_3))}
| _1 = formimp _2 = NEXT _3 = formimp
    {                       (`Next(_1,_3))}
| _1 = formimp _2 = SEQ _3 = formimp
    {                      (`Seq(_1,_3))}
| _1 = formimp _2 = IMP _3 = formimp
    {                      (`Imp(_1,_3))}
| _1 = formimp _2 = RIMP _3 = formimp
    {                       (`RImp(_1,_3))}
| _1 = formimp _2 = LIMP _3 = formimp
    {                       (`LImp(_1,_3))}
| _1 = OP _2 = formimp _3 = CP
    {                (_2)}
| _1 = formimp _2 = NEG
    {              (`Not(_1))}
52 53

sequent:
54 55 56 57 58 59
| _1 = formimp _2 = VDASH _3 = formimp
    {                      (Sequent(_1, _3))}
| _1 = VDASH _2 = formimp
    {                (Form(_2))}
| _1 = formimp
    {          (Form(_1))}
60 61 62 63 64

%%