# Summer school 2008:Typed arithmetic expressions with sums 2

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.
 Summer school 2008 Previous: Typed arithmetic expressions

Arithmetic expressions with pairs and sums. (This solution involves output factoring, but no identity types. Dan posted a solution involving identity types, and Chris posted a solution that avoids output factoring.)

Numbers and strings are unchanged.

## Typed expressions

Add a type for disjoint sums:

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

Add injections as values, and case as an expression.

```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.
inl : T val -> (sum T U) val.
inr : U val -> (sum 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 technical reasons, we bundle the branches of the case into a separate term with type cases; this makes the termination order more evident to Twelf. An element of "cases T U V" is the branches for a "sum T U" whose result has tp "V".

```cases : tp -> tp -> tp -> type.
cases/i : (T val -> V exp) -> (U val -> V exp) -> cases T U V.
case : (sum T U) exp -> cases T U V -> V exp.```

```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)

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).```

For "case" evaluation, we need an auxiliary relation "evalcase" to branch on inl vs. inr (output factoring).

```evalcase : (sum T U) val -> cases T U S -> S val -> type.
%mode evalcase +V +Cases -A.

eval/case
: eval (case E Cases) A
<- eval E V
<- evalcase V Cases A.

evalcase/inl
: evalcase (inl V1) (cases/i ([x] F1 x) ([y] F2 y)) A
<- eval (F1 V1) A.

evalcase/inr
: evalcase (inr V2) (cases/i ([x] F1 x) ([y] F2 y)) A
<- eval (F2 V2) A.```

Then we use mutual induction to show evaluation total.

```%worlds () (eval _ _) (evalcase _ _ _).
%total (E Cases) (eval E _) (evalcase _ Cases _).```
 Summer school 2008 Previous: Exercises 1