Summer school 2008:Typed arithmetic expressions with pairs

Arithmetic expressions with pairs.

Numbers and strings are unchanged.

%sort nat %.
%name 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 _ _) %.
%sort char %.
%name char %.
%term a char %.
%term b char %.
%sort str %.
%name str %.
%term emp str %.
%term cons %pi char %-> str %-> str %.
%sort cat {_ str} {_ str} {_ str} %.
%mode cat %in %in %out %.
%term cat/e cat emp S S %.
%term cat/c %pi (cat (cons X S1) S2 (cons X S3)) %<- (cat S1 S2 S3) %.
%worlds () (cat _ _ _) %.
%total S (cat S _ _) %.

Typed expressions

Add a type for products:

%sort tp %.
%name tp %.
%term number tp %.
%term string tp %.
%term prod %pi tp %-> tp %-> tp %.

Add pairs as a value, projections as expressions:

%sort val {_ tp} %.
%name val %.
%prec %postfix 1 val %.
%term num %pi nat %-> (number val) %.
%term lit %pi str %-> (string val) %.
%term pair %pi (T val) %-> (U val) %-> (prod T U val) %.
%sort exp {_ tp} %.
%name exp %.
%prec %postfix 1 exp %.
%term ret %pi (T val) %-> (T exp) %.
%term plus %pi (number exp) %-> (number exp) %-> (number exp) %.
%term append %pi (string exp) %-> (string exp) %-> (string exp) %.
%term let %pi (T exp) %-> (%pi (T val) %-> (U exp)) %-> (U exp) %.
%term fst %pi (prod T U exp) %-> (T exp) %.
%term snd %pi (prod T U exp) %-> (U exp) %.

For simplicity, take answers to be values.

And we add cases to eval:

%sort eval {_ T exp} {_ T 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/append
  %pi (eval (append E1 E2) (lit S))
  %<- (eval E1 (lit S1))
  %<- (eval E2 (lit S2))
  %<- (cat S1 S2 S) %.
%term eval/let %pi (eval (let E1 ([x] E2 x)) A) %<- (eval E1 V) %<- (eval (E2 V) A) %.
%term eval/fst %pi (eval (fst E) A) %<- (eval E (pair A _)) %.
%term eval/snd %pi (eval (snd E) B) %<- (eval E (pair _ B)) %.
%worlds () (eval _ _) %.
%total E (eval E _) %.