git.iko.soy/Idris-dev
on 019faba help sign in
Idris-dev/interp.mi
61 lines 1.7 kB history raw
1data Nat = O | S Nat;
3plus : Nat -> Nat -> Nat;
4plus O y = y;
5plus (S k) y = S (plus k y);
7data Ty = TyNat | TyFun Ty Ty;
9interpTy : Ty -> Set;
10interpTy TyNat = Nat;
11interpTy (TyFun s t) = interpTy s -> interpTy t;
13data Fin : Nat -> Set where
14 fO : Fin (S k)
15 | fS : Fin k -> Fin (S k);
17infixr 7 :: ;
19data Vect : Set -> Nat -> Set where
20 VNil : Vect a O
21 | (::) : a -> Vect a k -> Vect a (S k);
23data Env : Vect Ty n -> Set where
24 Empty : Env VNil
25 | Extend : {xs : Vect Ty n} -> interpTy a -> Env xs -> Env (a :: xs);
27lookup : (i : Fin n) -> Vect a n -> a;
28lookup fO (x :: xs) = x;
29lookup (fS i) (x :: xs) = lookup i xs;
31envLookup : {xs : Vect Ty n} ->
32 (i : Fin n) -> Env xs -> interpTy (lookup i xs);
33envLookup fO (Extend x xs) = x;
34envLookup (fS i) (Extend x xs) = envLookup i xs;
36data Expr : Vect Ty n -> Ty -> Set where
37 Var : {G : Vect Ty n} ->
38 (i : Fin n) -> Expr G (lookup i G)
39 | Val : {G : Vect Ty n} ->
40 Nat -> Expr G TyNat
41 | Lam : {G : Vect Ty n} ->
42 Expr (a :: G) t -> Expr G (TyFun a t)
43 | App : {G : Vect Ty n} ->
44 Expr G (TyFun a t) -> Expr G a -> Expr G t
45 | Add : {G : Vect Ty n} ->
46 Expr G TyNat -> Expr G TyNat -> Expr G TyNat;
48interp : {G : Vect Ty n} ->
49 Env G -> Expr G t -> interpTy t;
50interp env (Var i) = envLookup i env;
51interp env (Val x) = x;
52interp env (Lam sc) = \x => interp (Extend x env) sc;
53interp env (App f s) = (interp env f) (interp env s);
54interp env (Add x y) = plus (interp env x) (interp env y);
56eAdd : {G : Vect Ty n} ->
57 Expr G (TyFun TyNat (TyFun TyNat TyNat));
58eAdd = Lam (Lam (Add (Var fO) (Var (fS fO))));
60test : Nat;
61test = interp Empty eAdd (S (S O)) (S (S O));