{- Run-Time List Type:
- List;
- Polymorphic funtions.
Copyright (c) Groupoid Infinity, 2014-2018. -}
module list where
import eq
import nat
import maybe
import proto
data list (A: U) = nil | cons (a: A) (as: list A)
listCase (A C:U) (a b: C): list A -> C
= split { nil -> a ; cons x xs -> b }
listRec (A C:U) (z: C) (s: A->list A->C->C): (n:list A) -> C
= split { nil -> z ; cons x xs -> s x xs (listRec A C z s xs) }
listElim (A: U) (C:list A->U) (z: C nil) (s: (x:A)(xs:list A)->C(cons x xs)): (n:list A) -> C(n)
= split { nil -> z ; cons x xs -> s x xs }
listInd (A: U) (C:list A->U) (z: C nil) (s: (x:A)(xs:list A)->C(xs)->C(cons x xs)): (n:list A) -> C(n)
= split { nil -> z ; cons x xs -> s x xs (listInd A C z s xs) }
null (A: U): list A -> bool = split
nil -> true
cons x xs -> false
head (A: U): list A -> maybe A = split
nil -> nothing
cons x xs -> just x
tail (A: U): list A -> maybe (list A) = split
nil -> nothing
cons x xs -> just xs
nth (A: U): nat -> list A -> maybe A = split
zero -> split@(list A -> maybe A) with
nil -> nothing
cons x xs -> just x
succ i -> split@(list A -> maybe A) with
nil -> nothing
cons x xs -> nth A (pred i) xs
append (A: U): list A -> list A -> list A = split
nil -> idfun (list A)
cons x xs -> \(ys: list A) -> cons x (append A xs ys)
reverse (A: U): list A -> list A = rev nil where
rev (acc: list A): list A -> list A = split
nil -> acc
cons x xs -> rev (cons x acc) xs
map (A B: U) (f: A -> B) : list A -> list B = split
nil -> nil
cons x xs -> cons (f x) (map A B f xs)
zipWith (A B C: U) (f: A -> B -> C): list A -> list B -> list C = go where
go: list A -> list B -> list C = split
nil -> split@(list B->list C) with { nil -> nil ; cons y ys -> nil }
cons x xs -> split@(list B->list C) with { nil->nil ; cons y ys -> cons (f x y) (go xs ys) }
zip (A B: U): list A -> list B -> list (tuple A B)
= zipWith A B (tuple A B) (\(x:A)(y:B) -> pair x y)
foldr (A B: U) (f: A -> B -> B) (Z: B): list A -> B = split
nil -> Z
cons x xs -> f x (foldr A B f Z xs)
foldl (A B: U) (f: B -> A -> B) (Z: B): list A -> B = split
nil -> Z
cons x xs -> foldl A B f (f Z x) xs
switch (A: U) (a b: unit -> list A) : bool -> list A = split
false -> b tt
true -> a tt
filter (A: U) (p: A -> bool) : list A -> list A = split
nil -> nil
cons x xs -> switch A (\(_:unit) -> cons x (filter A p xs))
(\(_:unit) -> filter A p xs) (p x)
uncons (A: U): list A -> maybe ((a: A) * (list A)) = split
nil -> nothing
cons x xs -> just (x,xs)
length (A: U): list A -> nat = split
nil -> zero
cons x xs -> add one (length A xs)
list_eq (A: eq_): list A.1 -> list A.1 -> bool = split
nil -> split@(list A.1 -> bool) with
nil -> true
cons b bs -> false
cons x xs -> split@(list A.1 -> bool) with
nil -> false
cons a as -> or (A.2 a x) (list_eq A xs as)