mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-21 03:41:30 +03:00
762f6010dd
Only save the parts of terms and definitions which are needed for typechecking and evaluation (so, for example, we don't need types for machine generated metavariables, don't need types on lambdas, etc).
74 lines
2.3 KiB
Plaintext
74 lines
2.3 KiB
Plaintext
data Nat : Type where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
plus : Nat -> Nat -> Nat
|
|
plus Z $y = y
|
|
plus (S $k) $y = S (plus k y)
|
|
|
|
data Vect : Nat -> Type -> Type where
|
|
Nil : Vect Z $a
|
|
Cons : $a -> Vect $k $a -> Vect (S $k) $a
|
|
|
|
append : Vect $n $a -> Vect $m $a -> Vect (plus $n $m) $a
|
|
append Nil $ys = ys
|
|
append (Cons $x $xs) $ys = Cons x (append xs ys)
|
|
|
|
data Fin : Nat -> Type where
|
|
FZ : Fin (S $k)
|
|
FS : Fin $k -> Fin (S $k)
|
|
|
|
lookup : Fin $k -> Vect $k $ty -> $ty
|
|
lookup FZ (Cons $t $ts) = t;
|
|
lookup (FS $i) (Cons $t $ts) = lookup i ts;
|
|
|
|
-- As a larger example, we'll implement the well-typed interpreter.
|
|
-- So we'll need to represent the types of our expression language:
|
|
|
|
data Ty : Type where
|
|
Base : Type -> Ty
|
|
Arrow : Ty -> Ty -> Ty
|
|
|
|
-- Ty can be translated to a host language type
|
|
|
|
interpTy : Ty -> Type
|
|
interpTy (Base $t) = t
|
|
interpTy (Arrow $s $t) = (argTy : interpTy s) -> interpTy t
|
|
|
|
data HasType : Fin $k -> Ty -> Vect $k Ty -> Type where
|
|
Stop : HasType FZ $t (Cons $t $gam)
|
|
Pop : HasType $i $t $gam -> HasType (FS $i) $t (Cons $u $gam)
|
|
|
|
-- Expressions in our language, indexed by their contexts and types:
|
|
|
|
data Lang : Vect $k Ty -> Ty -> Type where
|
|
Var : HasType $i $t $gam -> Lang $gam $t
|
|
Val : (x : interpTy $a) -> Lang $gam $a
|
|
Lam : (scope : Lang (Cons $s $gam) $t) -> Lang $gam (Arrow $s $t)
|
|
App : Lang $gam (Arrow $s $t) -> Lang $gam $s -> Lang $gam $t;
|
|
Op : (interpTy $a -> interpTy $b -> interpTy $c) ->
|
|
Lang $gam $a -> Lang $gam $b -> Lang $gam $c
|
|
|
|
data Env : Vect $n Ty -> Type where
|
|
ENil : Env Nil
|
|
ECons : (x : interpTy $a) -> Env $xs -> Env (Cons $a $xs)
|
|
|
|
-- Find a value in an environment
|
|
lookupEnv : HasType $i $t $gam -> Env $gam -> interpTy $t
|
|
lookupEnv Stop (ECons $x $xs) = x
|
|
lookupEnv (Pop $var) (ECons $x $env) = lookupEnv var env
|
|
|
|
interp : Env $gam -> Lang $gam $t -> interpTy $t
|
|
interp $env (Var $i) = lookupEnv i env
|
|
interp $env (Val $x) = x
|
|
interp $env (App $f $a) = interp env f (interp env a)
|
|
interp $env (Lam {s = $s} $scope)
|
|
= \var => interp (ECons var env) scope
|
|
interp $env (Op $fn $x $y) = fn (interp env x) (interp env y)
|
|
|
|
testAdd : Lang $gam (Arrow (Base Nat) (Arrow (Base Nat) (Base Nat)))
|
|
testAdd = Lam (Lam (Op plus (Var Stop) (Var (Pop Stop))))
|
|
|
|
main : Nat
|
|
main = interp ENil testAdd (S (S Z)) (S (S Z))
|