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