Initialise

Author: edwinb

.gitignore

@@ -0,0 +1,17 @@
+*~
+*.ttc
+*.ttm
+*.o
+*.d
+*.a
+*.dll
+
+# Editor/IDE Related
+.\#* # Emacs swap file
+*~   # Vim swap file
+*.swo
+*.swp
+# VS Code
+.vscode/*
+
+/build

Code/Lecture1/WarmupExercise/Ex1.idr

@@ -0,0 +1,21 @@
+import Decidable.Equality
+
+-- This is the (simplified) definition of names in Core.TT
+data Name : Type where
+     UN : String -> Name -- user written name
+     MN : String -> Int -> Name -- machine generated name
+
+-- 1. Write an Eq instance for Name
+-- (sorry, it's not derivable yet!)
+Eq Name where
+  -- ...
+
+-- 2. Sometimes, we need to compare names for equality and use a proof that
+-- they're equal. So, implement the following 
+nameEq : (x : Name) -> (y : Name) -> Maybe (x = y)
+
+-- 3. (Optional, since we don't need this in Idris 2, but it's a good
+-- exercise to see if you can do it!) Implement decidable equality, so you
+-- also have a proof if names are *not* equal.
+DecEq Name where
+  decEq x y = ?decEq_rhs

Code/Lecture1/WarmupExercise/Ex2.idr

@@ -0,0 +1,26 @@
+
+data Name : Type where
+     UN : String -> Name -- user written name
+     MN : String -> Int -> Name -- machine generated name
+
+-- In the term representation, we represent local variables as an index into
+-- a list of bound names:
+data IsVar : Name -> Nat -> List Name -> Type where
+     First : IsVar n Z (n :: ns)
+     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)
+
+-- And, sometimes, it's convenient to manipulate variables separately.
+-- Note the erasure properties of the following definition (it is just a Nat
+-- at run time)
+data Var : List Name -> Type where
+     MkVar : {i : Nat} -> (0 p : IsVar n i vars) -> Var vars
+
+-- 1. Remove all references to the most recently bound variable
+dropFirst : List (Var (v :: vs)) -> List (Var vs)
+
+-- 2. Add a reference to a variable in the middle of a scope - we'll need 
+-- something like this later.
+-- Note: The type here isn't quite right, you'll need to modify it slightly.
+insertName : Var (outer ++ inner) -> Var (outer ++ n :: inner)
+
+

Code/Lecture1/WarmupExercise/Ex3.idr

@@ -0,0 +1,24 @@
+
+-- 1. Prove that appending Nil is the identity
+-- (Note: this is defined in Data.List, but have a go yourself!)
+appendNilNeutral : (xs : List a) -> xs ++ [] = xs
+
+-- 2. Prove that appending lists is associative.
+-- (Note: also defined in Data.List)
+appendAssoc : (xs : List a) -> (ys : List a) -> (zs : List a) ->
+              xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
+
+-- A tree indexed by the (inorder) flattening of its contents
+data Tree : List a -> Type where
+     Leaf : Tree []
+     Node : Tree xs -> (x : a) -> Tree ys -> Tree (xs ++ x :: ys)
+
+-- 3. Fill in rotateLemma. You'll need appendAssoc.
+rotateL : Tree xs -> Tree xs
+rotateL Leaf = Leaf
+rotateL (Node left n Leaf) = Node left n Leaf
+rotateL (Node left n (Node rightl n' rightr))
+    =  ?rotateLemma $ Node (Node left n rightl) n' rightr
+
+-- 4. Complete the definition of rotateR
+rotateR : Tree xs -> Tree xs

TinyIdris-v1/Test/Nat.tidr

@@ -0,0 +1,9 @@
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+pat y : Nat =>
+   plus Z y = y
+pat k : Nat, y : Nat =>
+   plus (S k) y = S (plus k y)

TinyIdris-v1/Test/Vect.tidr

@@ -0,0 +1,22 @@
+data Nat : Type where
+     Z : Nat
+     S : Nat -> Nat
+
+plus : Nat -> Nat -> Nat
+pat y : Nat =>
+   plus Z y = y
+pat k : Nat, y : Nat =>
+   plus (S k) y = S (plus k y)
+
+data Vect : Nat -> Type -> Type where
+     Nil : (a : Type) -> Vect Z a
+     Cons : (a : Type) -> (k : Nat) ->
+            a -> Vect k a -> Vect (S k) a
+
+append : (a : Type) -> (n : Nat) -> (m : Nat) ->
+         Vect n a -> Vect m a -> Vect (plus n m) a
+pat a : Type, k : Nat, ys : Vect k a =>
+    append a Z k (Nil a) ys = ys
+pat a : Type, n : Nat, x : a, xs : Vect n a, k : Nat, ys : Vect k a =>
+    append a (S n) k (Cons a n x xs) ys
+        = Cons a (plus n k) x (append a n k xs ys)