From 85274107aeba5b3b4f67719b9e1ca71aa5284b98 Mon Sep 17 00:00:00 2001
From: Edwin Brady <ecb10@st-andrews.ac.uk>
Date: Tue, 9 Jul 2019 13:31:25 +0200
Subject: [PATCH] Remove out of date samples

---
 sample/Adder.yaff   | 15 -------
 sample/BigVect.yaff | 96 ---------------------------------------------
 sample/Id.yaff      | 26 ------------
 sample/Interp.yaff  | 73 ----------------------------------
 sample/Nat.yaff     | 10 -----
 sample/Vect.yaff    | 36 -----------------
 6 files changed, 256 deletions(-)
 delete mode 100644 sample/Adder.yaff
 delete mode 100644 sample/BigVect.yaff
 delete mode 100644 sample/Id.yaff
 delete mode 100644 sample/Interp.yaff
 delete mode 100644 sample/Nat.yaff
 delete mode 100644 sample/Vect.yaff

diff --git a/sample/Adder.yaff b/sample/Adder.yaff
deleted file mode 100644
index 58552dc..0000000
--- a/sample/Adder.yaff
+++ /dev/null
@@ -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)
diff --git a/sample/BigVect.yaff b/sample/BigVect.yaff
deleted file mode 100644
index c82aeea..0000000
--- a/sample/BigVect.yaff
+++ /dev/null
@@ -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)))))))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-        ))))))))))))))))))))))))))))))))))))))))))))))))
-
diff --git a/sample/Id.yaff b/sample/Id.yaff
deleted file mode 100644
index dfc3208..0000000
--- a/sample/Id.yaff
+++ /dev/null
@@ -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
diff --git a/sample/Interp.yaff b/sample/Interp.yaff
deleted file mode 100644
index 6c87d87..0000000
--- a/sample/Interp.yaff
+++ /dev/null
@@ -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))
diff --git a/sample/Nat.yaff b/sample/Nat.yaff
deleted file mode 100644
index 94f0f36..0000000
--- a/sample/Nat.yaff
+++ /dev/null
@@ -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))
diff --git a/sample/Vect.yaff b/sample/Vect.yaff
deleted file mode 100644
index 170f1be..0000000
--- a/sample/Vect.yaff
+++ /dev/null
@@ -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))
-