# Summer school 2008:Typed arithmetic expressions (extrinsic encoding)

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

Here we take a more traditional approach to representing syntax, by first giving a definition of raw syntax, with a separate judgement defining the well-typed expressions. This is called an extrinsic encoding.

Numbers and strings are as before.

## Raw syntax

```tp : type.				%name tp T.
number : tp.
string : tp.

val : type.				%name val V.
num : nat -> val.
lit : str -> val.

exp : type.				%name exp E.
ret : val -> exp.
plus : exp -> exp -> exp.
append : exp -> exp -> exp.
let : exp -> (val -> exp) -> exp.```

## Typing judgement on raw syntax

```ofv : val -> tp -> type.		%name ofv Dofv.
%mode ofv +V -T.

- : ofv (num _) number.
- : ofv (lit _) string.

of : exp -> tp -> type.			%name of Dof.
%mode of +E -T.

- : of (ret V) T <- ofv V T.
- : of (plus E1 E2) number <- of E1 number <- of E2 number.
- : of (append E1 E2) string <- of E1 string <- of E2 string.
- : of (let E1 ([x] E2 x)) T' <- of E1 T <- ({x:val} ofv x T -> of (E2 x) T').```

## Evaluation

```ans : type.				%name ans A.
anum : nat -> ans.
astr : str -> ans.

ofa : ans -> tp -> type.		%name ofa Dofa.
%mode ofa +A -T.

- : ofa (anum _) number.
- : ofa (astr _) string.```

### Evaluation judgement on raw syntax

```eval : exp -> ans -> type.
%mode eval +E1 -E2.

eval/val/num
: eval (ret (num N)) (anum N).

eval/val/lit
: eval (ret (lit S)) (astr S).

eval/plus
: eval (plus E1 E2) (anum N)
<- eval E1 (anum N1)
<- eval E2 (anum N2)

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

eval/let
: eval (let E1 ([x] E2 x)) A
<- eval E1 (anum N)
<- eval (E2 (num N)) A.```

Evaluation is not total because of run-time type errors! (e.g., try appending two numbers).

`%worlds () (eval _ _).`

Twelf gives this error, refering to the first recursive call of eval/plus.

`%total E (eval E _).`
```Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)
Error:
Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{E1:exp} {S1:str} |- eval E1 (astr S1).

%% ABORT %%```
 Summer school 2008 Previous: Typed arithmetic expressions Next: Exercises 1