%
% operator precedence parsing
%

int : sort.
% z : trm int.
% s : trm int -> trm int. %prefix 10 s.
1 : trm int.
2 : trm int.
3 : trm int.

con : trm int -> atm.

op = arrow int (arrow int int).
+ : trm op.  
* : trm op.  
end : trm op.

fun : trm op -> atm.

gt : trm op -> trm op -> atm.
lt : trm op -> trm op -> atm.

evc : trm op -> trm int -> atm.
evo : trm op -> trm int -> atm.
red : trm int -> atm.


gt_1 : prog ( ^ gt * _ ).
lt_0 : prog ( ^ lt end * ).
lt_2 : prog ( ^ lt end + ).
lt_1 : prog ( ^ lt + * ).

ev_0 : prog (
^ evc end A <<= ^ con A <<= ^ fun end
).

ev_1 : prog (
^ evc Op A <<= ^ con C <<= ( ^ con C >=> ^ evo Op A)
).

ev_2 : prog (
^ evo Op (app (app Op X) Y) <<= ^ fun end 
                            <<= ^ con X <<= ^ fun Op <<= ^ con Y
).

ev_3 : prog (
^ evo Op A <<= ^ fun Op' <= ^ gt Op Op' <<= ( ^ fun Op' =>> ^ red A)
).

ev_4 : prog (
^ evo Op A <<= ^ fun Op' <= ^ lt Op Op' <<= ( ^ fun Op' >=> ^ evc Op' A )
).

ev_5 : prog (
^ red A <=< ^ con X <=< ^ fun F <=< ^ con Y <=< ^ fun Op
        <=< ( ^ fun Op >=> ^ con (app (app F X) Y) >=> ^ evo Op A)
).