Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Agda tutorial
module AgdaBasics where
apply : (A : Set)(B : A Set) ((x : A) B x) (a : A) B a
apply A B f a = f a
_∘_ : {A : Set}{B : A Set}{C : (x : A) B x Set}
(f : {x : A}(y : B x) C x y)(g : (x : A) B x)
(x : A) C x (g x)
(f ∘ g) x = f (g x)
module Bool where
data Bool : Set where
true : Bool
false : Bool
not : Bool Bool
not true = false
not false = true
module Nat where
open Bool
data ℕ : Set where
zero :
suc :
_+_ :
zero + m = m
suc n + m = suc (n + m)
_×_ :
zero × _ = zero
suc zero × m = m
suc n × m = n + (n × m)
identity : (A : Set) A A
identity A x = x
zero' :
zero' = identity ℕ zero
plus-two = suc ∘ suc
_<_ : Bool
_ < zero = false
zero < suc n = true
suc m < suc n = m < n
module Fin where
open Nat
data Fin : Set where
fzero : {n : ℕ} Fin (suc n)
fsuc : {n : ℕ} Fin n Fin (suc n)
data Empty : Set where
empty : Fin zero Empty
module Vec where
open Nat
open Fin
data Vec (A : Set) : Set where
[] : Vec A zero
_∷_ : {n : ℕ} A Vec A n Vec A (suc n)
head : {A : Set}{n : ℕ} Vec A (suc n) Vec A n
head (x ∷ xs) = xs
vmap : {A B : Set}{n : ℕ} (A B) Vec A n Vec B n
vmap _ [] = []
vmap f (x ∷ xs) = f x ∷ vmap f xs
_!_ : {n : ℕ}{A : Set} Vec A n Fin n A
[] ! ()
(x ∷ xs) ! fzero = x
(x ∷ xs) ! (fsuc i) = xs ! i
tabulate : {n : ℕ}{A : Set} (Fin n A) Vec A n
tabulate {zero} f = []
tabulate {suc n} f = f fzero ∷ tabulate (f ∘ fsuc)
data Image_∋_ {A B : Set}(f : A B) : B Set where
im : (x : A) Image f ∋ f x
inv : {A B : Set}(f : A B)(y : B) Image f ∋ y A
inv f .(f x) (im x) = x
module BoolTypes where
open Bool
data False : Set where
record True : Set where
trivial : True
trivial = _
isTrue : Bool Set
isTrue true = True
isTrue false = False
module List where
open Nat
open Bool
open BoolTypes
infixr 40 _∷_
data List (A : Set) : Set where
[] : List A
_∷_ : A List A List A
_++_ : {A : Set} List A List A List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
length : {A : Set} List A
length [] = zero
length (x ∷ xs) = suc (length xs)
lookup : {A : Set}(xs : List A)(n : ℕ) isTrue (n < length xs) A
lookup [] n ()
lookup (x ∷ xs) zero _ = x
lookup (x ∷ xs) (suc n) p = lookup xs n p
map : {A B : Set} (A B) List A List B
map f [] = []
map f (x ∷ xs) = f x ∷ map f xs
filter : {A : Set} (A Bool) List A List A
filter _ [] = []
filter p (x ∷ xs) with p x
... | true = x ∷ filter p xs
... | false = filter p xs
infix 20 _⊆_
data _⊆_ {A : Set} : List A List A Set where
stop : [] ⊆ []
drop : {xs y ys} xs ⊆ ys xs ⊆ y ∷ ys
keep : {x xs ys} xs ⊆ ys x ∷ xs ⊆ x ∷ ys
lem-filter : {A : Set}(p : A Bool)(xs : List A) filter p xs ⊆ xs
lem-filter p [] = stop
lem-filter p (x ∷ xs) with p x
... | true = keep (lem-filter p xs)
... | false = drop (lem-filter p xs)
data _≡_ {A : Set} : A A Set where
refl : {x : A} x ≡ x
module EqTypes where
open Nat
open BoolTypes
data _≤_ : Set where
leq-zero : {n : ℕ} zero ≤ n
leq-suc : {m n : ℕ} m ≤ n suc m ≤ suc n
leq-trans : {l m n : ℕ} l ≤ m m ≤ n l ≤ n
leq-trans leq-zero _ = leq-zero
leq-trans (leq-suc p) (leq-suc q) = leq-suc (leq-trans p q)
data _≠_ : Set where
z≠s : {n : ℕ} zero ≠ suc n
s≠z : {n : ℕ} suc n ≠ zero
s≠s : {m n : ℕ} m ≠ n suc m ≠ suc n
data Equal? (n m : ℕ) : Set where
eq : n ≡ m Equal? n m
neq : n ≠ m Equal? n m
equal? : (n m : ℕ) Equal? n m
equal? zero zero = eq refl
equal? zero (suc m) = neq z≠s
equal? (suc m) zero = neq s≠z
equal? (suc n) (suc m) with equal? n m
equal? (suc n) (suc .n) | eq refl = eq refl
equal? (suc n) (suc m) | neq p = neq (s≠s p)
module Maybe where
data Maybe (A : Set) : Set where
nothing : Maybe A
just : A Maybe A
maybe : {A B : Set} B (A B) Maybe A B
maybe z f nothing = z
maybe z f (just x) = f x
module Sort (A : Set)(_<_ : A A Bool.Bool) where
open List
open Bool
insert : A List A List A
insert y [] = y ∷ []
insert y (x ∷ xs) with x < y
... | true = x ∷ insert y xs
... | false = y ∷ x ∷ xs
sort : List A List A
sort [] = []
sort (x ∷ xs) = insert x (sort xs)
module Sortℕ = Sort Nat.ℕ Nat._<_
module Lists (A : Set)(_<_ : A A Bool.Bool) where
open List
open Sort A _<_ public
open Maybe
minimum : List A Maybe A
minimum xs with sort xs
... | [] = nothing
... | y ∷ ys = just y
record Point : Set where
open Nat
field x :
y :
mkPoint : Point
mkPoint a b = record{x = a; y = b}
record Monad (M : Set Set) : Set1 where
open List
field
return : {A : Set} A M A
_>>=_ : {A B : Set} M A (A M B) M B
mapM : {A B : Set} (A M B) List A M (List B)
mapM f [] = return []
mapM f (x ∷ xs) = f x >>= \y
mapM f xs >>= \ys
return (y ∷ ys)
module Exercise2-1 where
open Vec
open Nat
Matrix : Set Set
Matrix A n m = Vec (Vec A n) m
vec : {n : ℕ}{A : Set} A Vec A n
vec {zero} _ = []
vec {suc n} x = x ∷ vec {n} x
infixl 90 _$_
_$_ : {n : ℕ}{A B : Set} Vec (A B) n Vec A n Vec B n
[] $ [] = []
(f ∷ fs) $ (x ∷ xs) = f x ∷ fs $ xs
transpose : {A n m} Matrix A n m Matrix A m n
transpose [] = vec []
transpose (xs ∷ xss) = vmap (\x xs x ∷ xs) xs $ transpose xss
module Exercise2-2 where
open Vec
open Fin
lem-!-tab : {A n} (f : Fin n A)(i : Fin n) (tabulate f ! i) ≡ f i
lem-!-tab f fzero = refl
lem-!-tab f (fsuc i) = lem-!-tab (f ∘ fsuc) i
vec-∷-≡ : {A n} {xs : Vec A n}{ys : Vec A n}{x : A}
xs ≡ ys (x ∷ xs) ≡ (x ∷ ys)
vec-∷-≡ refl = refl
lem-tab-! : {A n} (xs : Vec A n) tabulate (_!_ xs) ≡ xs
lem-tab-! [] = refl
lem-tab-! (x ∷ xs) = vec-∷-≡ (lem-tab-! xs)
module Exercise2-3 where
open List
open Bool
⊆-refl : {A : Set}{xs : List A} xs ⊆ xs
⊆-refl {xs = []} = stop
⊆-refl {xs = x ∷ xs} = keep (⊆-refl {xs = xs})
⊆-trans : {A : Set}{xs ys zs : List A}
xs ⊆ ys ys ⊆ zs xs ⊆ zs
⊆-trans stop stop = stop
⊆-trans p (drop q) = drop (⊆-trans p q)
⊆-trans (drop p) (keep q) = drop (⊆-trans p q)
⊆-trans (keep p) (keep q) = keep (⊆-trans p q)
infixr 30 _∷_
data SubList {A : Set} : List A Set where
[] : SubList []
_∷_ : x {xs} SubList xs SubList (x ∷ xs)
skip : {x xs} SubList xs SubList (x ∷ xs)
forget : {A : Set}{xs : List A} SubList xs List A
forget [] = []
forget (x ∷ xs) = x ∷ forget xs
forget (skip xs) = forget xs
lem-forget : {A : Set}{xs : List A}(zs : SubList xs)
forget zs ⊆ xs
lem-forget [] = stop
lem-forget (x ∷ xs) = keep (lem-forget xs)
lem-forget (skip xs) = drop (lem-forget xs)
filter' : {A : Set} (A Bool) (xs : List A) SubList xs
filter' p [] = []
filter' p (x ∷ xs) with p x
... | true = x ∷ filter' p xs
... | false = skip (filter' p xs)
complement : {A : Set}{xs : List A} SubList xs SubList xs
complement [] = []
complement (x ∷ xs) = skip (complement xs)
complement (skip {x = x} xs) = x ∷ complement xs
sublists : {A : Set}(xs : List A) List (SubList xs)
sublists [] = [] ∷ []
sublists (x ∷ xs) = let s = sublists xs
in map skip s ++ map (_∷_ x) s
module Views where
open import Data.Nat
_×_ :
_×_ = _*_
data Parity : Set where
even : (k : ℕ) Parity (k × 2)
odd : (k : ℕ) Parity (1 + k × 2)
parity : (n : ℕ) Parity n
parity zero = even zero
parity (suc n) with parity n
parity (suc .(k × 2)) | even k = odd k
parity (suc .(1 + k × 2)) | odd k = even (suc k)
half :
half n with parity n
half .(k × 2) | even k = k
half .(1 + k × 2) | odd k = k
open import Data.List
open import Data.Bool renaming (T to isTrue)
isFalse : Bool Set
isFalse b = isTrue (not b)
infixr 30 _:all:_
data All {A : Set}(P : A Set) : List A Set where
all[] : All P []
_:all:_ : {x xs} P x All P xs All P (x ∷ xs)
satisfies : {A : Set} (A Bool) A Set
satisfies p x = isTrue (p x)
data Find {A : Set}(p : A Bool) : List A Set where
found : (xs : List A)(y : A) satisfies p y (ys : List A)
Find p (xs ++ y ∷ ys)
not-found : {xs} All (satisfies (not ∘ p)) xs Find p xs
data Inspect {A : Set}(x : A) : Set where
it : (y : A) x ≡ y Inspect x
inspect : {A : Set}(x : A) Inspect x
inspect x = it x refl
trueIsTrue : {x : Bool} x ≡ true isTrue x
trueIsTrue refl = _
falseIsFalse : {x : Bool} x ≡ false isFalse x
falseIsFalse refl = _
find : {A : Set}(p : A Bool)(xs : List A) Find p xs
find p [] = not-found all[]
find p (x ∷ xs) with inspect (p x)
... | it true prf = found [] x (trueIsTrue prf) xs
... | it false prf with find p xs
find p (x ∷ ._) | it false _ | found xs y py ys =
found (x ∷ xs) y py ys
find p (x ∷ xs) | it false prf | not-found npxs =
not-found (falseIsFalse prf :all: npxs)
data _∈_ {A : Set}(x : A) : List A Set where
hd : {xs} x ∈ (x ∷ xs)
tl : {y xs} x ∈ xs x ∈ (y ∷ xs)
index : {A}{x : A}{xs} x ∈ xs
index hd = zero
index (tl p) = suc (index p)
data Lookup {A : Set}(xs : List A) : Set where
inside : (x : A)(p : x ∈ xs) Lookup xs (index p)
outside : (m : ℕ) Lookup xs (length xs + m)
_!_ : {A : Set}(xs : List A)(n : ℕ) Lookup xs n
[] ! n = outside n
(x ∷ xs) ! zero = inside x hd
(x ∷ xs) ! suc n with xs ! n
(x ∷ xs) ! suc .(index p) | inside y p = inside y (tl p)
(x ∷ xs) ! suc .(length xs + n) | outside n = outside n
module Lambda where
open import Data.Nat
open import Data.List
open Views
infixr 30 _=>_
data Type : Set where
¹ : Type
_=>_ : Type Type Type
data Equal? : Type Type Set where
yes : {τ} Equal? τ τ
no : {σ τ} Equal? σ τ
_=?=_ : (σ τ : Type) Equal? σ τ
¹ =?= ¹ = yes
¹ =?= (_ => _) = no
(_ => _) =?= ¹ = no
(σ₁ => τ₁) =?= (σ₂ => τ₂) with σ₁ =?= σ₂ | τ₁ =?= τ₂
(σ => τ) =?= (.σ => .τ) | yes | yes = yes
(σ₁ => τ₁) =?= (σ₂ => τ₂) | _ | _ = no
infixl 80 _$_
data Raw : Set where
var : Raw
_$_ : Raw Raw Raw
lam : Type Raw Raw
Cxt = List Type
data Term: Cxt) : Type Set where
var : {τ} τ ∈ Γ Term Γ τ
_$_ : {σ τ} Term Γ (σ => τ) Term Γ σ Term Γ τ
lam : σ {τ} Term (σ ∷ Γ) τ Term Γ (σ => τ)
erase : {Γ τ} Term Γ τ Raw
erase (var x) = var (index x)
erase (t $ u) = erase t $ erase u
erase (lam σ t) = lam σ (erase t)
data Infer: Cxt) : Raw Set where
ok :: Type)(t : Term Γ τ) Infer Γ (erase t)
bad : {e : Raw} Infer Γ e
infer :: Cxt)(e : Raw) Infer Γ e
infer Γ (var n) with Γ ! n
infer Γ (var .(length Γ + n)) | outside n = bad
infer Γ (var .(index x)) | inside σ x = ok σ (var x)
infer Γ (t $ u) with infer Γ t
infer Γ (t $ u) | bad = bad
infer Γ (.(erase t₁) $ e₂) | ok ¹ t₁ = bad
infer Γ (.(erase t₁) $ e₂) | ok (σ => τ) t₁ with infer Γ e₂
infer Γ (.(erase t₁) $ e₂) | ok (σ => τ) t₁ | bad = bad
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok σ' t₂ with σ =?= σ'
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok .σ t₂ | yes =
ok τ (t₁ $ t₂)
infer Γ (.(erase t₁) $ .(erase t₂)) | ok (σ => τ) t₁ | ok σ' t₂ | no = bad
infer Γ (lam σ e) with infer (σ ∷ Γ) e
infer Γ (lam σ .(erase t)) | ok τ t = ok (σ => τ) (lam σ t)
infer Γ (lam σ e) | bad = bad
module Exercises3-1 where
open Nat
data Compare : Set where
less : {n} k Compare n (n + suc k)
more : {n} k Compare (n + suc k) n
same : {n} Compare n n
compare : (n m : ℕ) Compare n m
compare zero zero = same
compare zero (suc m) = less m
compare (suc n) zero = more n
compare (suc n) (suc m) with compare n m
compare (suc n) (suc .n) | same = same
compare (suc n) (suc .(n + suc k)) | less k = less k
compare (suc .(m + suc k)) (suc m) | more k = more k
difference :
difference n m with compare n m
difference n .n | same = zero
difference n .(n + suc k) | less k = zero
difference .(m + suc k) m | more k = suc k
module Exercises3-2 where
open import Data.Nat
open import Data.List
open Views
infixr 30 _=>_
data Type : Set where
¹ : Type
_=>_ : Type Type Type
data _≠_ : Type Type Set where
¹≠=> : {σ τ : Type} ¹ ≠ (σ => τ)
=>≠¹ : {σ τ : Type} (σ => τ) ≠ ¹
_≠=> : {σ₁ σ₂ τ : Type} (σ₁ ≠ σ₂) (σ₁ => τ) ≠ (σ₂ => τ)
=>≠_ : {σ τ₁ τ₂ : Type} (τ₁ ≠ τ₂) (σ => τ₁) ≠ (σ => τ₂)
_=>≠=>_ : {σ₁ τ₁ σ₂ τ₂ : Type}
(σ₁ ≠ σ₂) (τ₁ ≠ τ₂) (σ₁ => τ₁) ≠ (σ₂ => τ₂)
data Equal? : Type Type Set where
yes : {τ} Equal? τ τ
no : {σ τ} σ ≠ τ Equal? σ τ
_=?=_ : (σ τ : Type) Equal? σ τ
¹ =?= ¹ = yes
¹ =?= (_ => _) = no ¹≠=>
(_ => _) =?= ¹ = no =>≠¹
(σ₁ => τ₁) =?= (σ₂ => τ₂) with σ₁ =?= σ₂ | τ₁ =?= τ₂
(σ => τ) =?= (.σ => .τ) | yes | yes = yes
(σ => τ₁) =?= (.σ => τ₂) | yes | no p = no (=>≠ p)
(σ₁ => τ) =?= (σ₂ => .τ) | no p | yes = no (p ≠=>)
(σ₁ => τ₁) =?= (σ₂ => τ₂) | no p | no q = no (p =>≠=> q)
infixl 80 _$_
data Raw : Set where
var : Raw
_$_ : Raw Raw Raw
lam : Type Raw Raw
Cxt = List Type
data Term: Cxt) : Type Set where
var : {τ} τ ∈ Γ Term Γ τ
_$_ : {σ τ} Term Γ (σ => τ) Term Γ σ Term Γ τ
lam : σ {τ} Term (σ ∷ Γ) τ Term Γ (σ => τ)
erase : {Γ τ} Term Γ τ Raw
erase (var x) = var (index x)
erase (t $ u) = erase t $ erase u
erase (lam σ t) = lam σ (erase t)
data BadTerm: Cxt) : Set where
var : (n : ℕ) BadTerm Γ
_¹$_ : Term Γ ¹ Raw BadTerm Γ
_≠$_ : {σ₁ σ₂ τ} Term Γ (σ₁ => τ) Term Γ σ₂ (σ₁ ≠ σ₂) BadTerm Γ
_b$_ : BadTerm Γ Raw BadTerm Γ
_$b_ : Raw BadTerm Γ BadTerm Γ
lam : σ BadTerm (σ ∷ Γ) BadTerm Γ
eraseBad :: Cxt} BadTerm Γ Raw
eraseBad {Γ} (var n) = var (length Γ + n)
eraseBad (t ¹$ r) = erase t $ r
eraseBad ((t ≠$ u) p) = erase t $ erase u
eraseBad (b b$ r) = eraseBad b $ r
eraseBad (r $b b) = r $ eraseBad b
eraseBad (lam σ b) = lam σ (eraseBad b)
data Infer: Cxt) : Raw Set where
ok :: Type)(t : Term Γ τ) Infer Γ (erase t)
bad : (b : BadTerm Γ) Infer Γ (eraseBad b)
infer :: Cxt)(e : Raw) Infer Γ e
infer Γ (var n) with Γ ! n
infer Γ (var .(length Γ + n)) | outside n = bad (var n)
infer Γ (var .(index x)) | inside σ x = ok σ (var x)
infer Γ (t $ u) with infer Γ t
infer Γ (.(eraseBad b) $ e₂) | bad b = bad (b b$ e₂)
infer Γ (.(erase t₁) $ e₂) | ok ¹ t₁ = bad (t₁ ¹$ e₂)
infer Γ (.(erase t₁) $ e₂) | ok (σ => τ) t₁ with infer Γ e₂
infer Γ (.(erase t₁) $ .(eraseBad b))
| ok (σ => τ) t₁ | bad b = bad (erase t₁ $b b)
infer Γ (.(erase t₁) $ .(erase t₂))
| ok (σ => τ) t₁ | ok σ' t₂ with σ =?= σ'
infer Γ (.(erase t₁) $ .(erase t₂))
| ok (σ => τ) t₁ | ok .σ t₂ | yes = ok τ (t₁ $ t₂)
infer Γ (.(erase t₁) $ .(erase t₂))
| ok (σ => τ) t₁ | ok σ' t₂ | no p = bad ((t₁ ≠$ t₂) p)
infer Γ (lam σ e) with infer (σ ∷ Γ) e
infer Γ (lam σ .(erase t)) | ok τ t = ok (σ => τ) (lam σ t)
infer Γ (lam σ .(eraseBad b)) | bad b = bad (lam σ b)
module Exercises3-3 where
open Views
open import Data.Bool
open import Data.List
lemma-All-∈ : {A x xs}{P : A Set} All P xs x ∈ xs P x
lemma-All-∈ all[] ()
lemma-All-∈ (p :all: xs) hd = p
lemma-All-∈ (p :all: xs) (tl i) = lemma-All-∈ xs i
lem-filter-sound : {A : Set}(p : A Bool)(xs : List A)
All (satisfies p) (filter p xs)
lem-filter-sound p [] = all[]
lem-filter-sound p (x ∷ xs) with inspect (p x)
lem-filter-sound p (x ∷ xs) | it y prf with p x | prf
lem-filter-sound p (x ∷ xs) | it .true prf | true | refl =
trueIsTrue prf :all: lem-filter-sound p xs
lem-filter-sound p (x ∷ xs) | it .false prf | false | refl =
lem-filter-sound p xs
module Exercises3-4 where
open import Data.List hiding (_++_)
open import Data.Nat
open import Data.String
open import Data.Bool
open Views
True : Set
True = T true
False : Set
False = T false
Tag = String
mutual
data Schema : Set where
tag : Tag List Child Schema
data Child : Set where
text : Child
elem : Schema Child
data BList (A : Set) : Set where
[] : {n} BList A n
_∷_ : {n} A BList A n BList A (suc n)
data Cons (A B : Set) : Set where
_∷_ : A B Cons A B
FList : Set Set
FList A zero m = BList A m
FList A (suc n) zero = False
FList A (suc n) (suc m) = Cons A (FList A n m)
mutual
data XML : Schema Set where
element : {kids}(t : Tag) All Element kids XML (tag t kids)
Element : Child Set
Element text = String
Element (elem n m s) = FList (XML s) n m
mutual
printXML : {s : Schema} XML s String
printXML (element t kids) =
"<" ++ t ++ ">" ++ printChildren kids ++ "</" ++ t ++ ">"
printChildren : {kids : List Child} All Element kids String
printChildren all[] = ""
printChildren {text ∷ _} (s :all: kids) = s
printChildren {elem n m s ∷ _} (fl :all: kids) = printFList n m fl
printFList : {s : Schema}(n m : ℕ) FList (XML s) n m String
printFList {s} (suc n) zero ()
printFList {s} (zero) m bl = printBList bl
printFList {s} (suc n) (suc m) (xml ∷ fl) = printXML xml ++ printFList n m fl
printBList : {s : Schema}{n : ℕ} BList (XML s) n String
printBList [] = ""
printBList (xml ∷ bl) = printXML xml ++ printBList bl
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment