mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-18 10:21:39 +03:00
Remove out of date samples
This commit is contained in:
parent
c0ef32d60f
commit
85274107ae
@ -1,15 +0,0 @@
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
AdderTy : Nat -> Type
|
||||
AdderTy Z = Nat
|
||||
AdderTy (S $k) = Nat -> AdderTy k
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z $y = y
|
||||
plus (S $k) $y = S (plus k y)
|
||||
|
||||
adder : (i : Nat) -> (acc : Nat) -> AdderTy i
|
||||
adder Z $acc = acc
|
||||
adder (S $k) $acc = \x => adder k (plus x acc)
|
@ -1,96 +0,0 @@
|
||||
data Bool : Type where
|
||||
False : Bool
|
||||
True : Bool
|
||||
|
||||
{-
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus
|
||||
= \x, y =>
|
||||
case x of
|
||||
Z => y
|
||||
S k => S (plus k y)
|
||||
-}
|
||||
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
S : Nat -> Nat
|
||||
|
||||
data Vect : Nat -> Type -> Type where
|
||||
Nil : {0 a : Type} -> Vect Z a
|
||||
Cons : {0 a : Type} -> {0 k : Nat} -> a -> Vect k a -> Vect (S k) a
|
||||
|
||||
stuff : Vect ? Bool
|
||||
stuff = Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
(Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
Nil)))))))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
|
@ -1,26 +0,0 @@
|
||||
IdType : Type
|
||||
IdType = {0 a : Type} -> a -> a
|
||||
|
||||
id : IdType
|
||||
id = \ x : _ => x
|
||||
|
||||
idid : {0 a : Type} -> a -> a
|
||||
idid = id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
id id id id id id id id id id
|
||||
|
||||
idTy : Type
|
||||
idTy = idid Type
|
@ -1,73 +0,0 @@
|
||||
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))
|
@ -1,10 +0,0 @@
|
||||
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)
|
||||
|
||||
main : Nat
|
||||
main = plus (S (S Z)) (S (S Z))
|
@ -1,36 +0,0 @@
|
||||
data Bool : Type where
|
||||
False : Bool
|
||||
True : Bool
|
||||
|
||||
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 : {0 a : Type} -> Vect Z a
|
||||
Cons : {0 a : Type} -> {0 k : Nat} -> a -> Vect k a -> Vect (S k) a
|
||||
|
||||
data Env : Vect $n Type -> Type where
|
||||
ENil : Env Nil
|
||||
ECons : (x : $a) -> Env $xs -> Env (Cons $a $xs)
|
||||
|
||||
id : $a -> $a
|
||||
apply : ($a -> $b) -> $a -> $b
|
||||
compose : ($b -> $c) -> ($a -> $b) -> $a -> $c
|
||||
|
||||
zipWith : -- {0 a : _} -> {0 b : _} ->{0 c : _} -> {0 n : _} ->
|
||||
($a -> $b -> $c) -> Vect $n $a -> Vect $n $b -> Vect $n $c
|
||||
zipWith $f (Cons $x $xs) (Cons $y $ys) = Cons (f x y) (zipWith f xs ys)
|
||||
zipWith $f Nil Nil = Nil
|
||||
|
||||
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)
|
||||
|
||||
main : Vect (S (S (S (S Z)))) Integer
|
||||
main = append (Cons 1 (Cons 2 Nil)) (Cons 3 (Cons 4 Nil))
|
||||
|
Loading…
Reference in New Issue
Block a user