POPL Tutorial/Session 2 Starter

Starter code for Session 2

Arithmetic primitives

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add z N N %.
%term add/s %pi (add (s M) N (s P)) %<- (add M N P) %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.

Expressions

%sort val %.
%term num %pi nat %-> val %.
%sort exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.
%sort eval {_ exp} {_ val} %.
%mode eval %in %out %.
%term eval/val eval (ret V) V %.
%term eval/plus
  %pi (eval (plus E1 E2) (num N))
  %<- (eval E1 (num N1))
  %<- (eval E2 (num N2))
  %<- (add N1 N2 N) %.
%term eval/let %pi (eval (let E1 ([x] E2 x)) A) %<- (eval E1 V) %<- (eval (E2 V) A) %.
%worlds () (eval _ _) %.
%total E (eval E _) %.