{- 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)