Summer school 2008:Typed arithmetic expressions with pairs

From The Twelf Project

Summer school 2008

Previous: Exercises 1

Arithmetic expressions with pairs.

Numbers and strings are unchanged.

Typed expressions

Add a type for products:

tp : type.				%name tp T.
number : tp.
string : tp.
prod   : tp -> tp -> tp.

Add pairs as a value, projections as expressions:

val : tp -> type.			%name val V.  %postfix 1 val.
num : nat -> number val.
lit : str -> string val.
pair : T val -> U val -> (prod T U) val.

exp : tp -> type.			%name exp E.  %postfix 1 exp.
ret : T val -> T exp.
plus : number exp -> number exp -> number exp.
append : string exp -> string exp -> string exp.
let : T exp -> (T val -> U exp) -> U exp.
fst : (prod T U) exp -> T exp.
snd : (prod T U) exp -> U exp.

For simplicity, take answers to be values.

And we add cases to eval:

eval : T exp -> T val -> type.
%mode eval +E1 -E2.

eval/val
   : eval (ret V) V.

eval/plus
   : eval (plus E1 E2) (num N)
      <- eval E1 (num N1)
      <- eval E2 (num N2)
      <- add N1 N2 N.

eval/append
   : eval (append E1 E2) (lit S)
      <- eval E1 (lit S1)
      <- eval E2 (lit S2)
      <- cat S1 S2 S.

eval/let
   : eval (let E1 ([x] E2 x)) A
      <- eval E1 V
      <- eval (E2 V) A.

eval/fst
   : eval (fst E) A
      <- eval E (pair A _).

eval/snd
   : eval (snd E) B
      <- eval E (pair _ B).

%worlds () (eval _ _).
%total E (eval E _).

Summer school 2008

Previous: Exercises 1