%%% The CLS machine (a variant of the SECD machine)
%%% Author: Frank Pfenning, based on [Hannan & Pfenning 92]

instruction : type.  %name instruction I.
program     : type.  %name program P.
envstack    : type.  %name envstack Ks.
state       : type.  %name state St.

ev     : exp' -> instruction.
add1   : instruction.
branch : instruction.
mkpair : instruction.
getfst : instruction.
getsnd : instruction.
apply  : instruction.
bind   : instruction.

done : program.
&    : instruction -> program -> program.
%infix right 10 &.

emptys : envstack.
;;     : envstack -> env -> envstack.
%infix left 10 ;;.

st : envstack -> program -> env -> state.