mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
c88bf7af8d
This was taking too long, and adding too many things, because it was going too deep in the name of having everything accessible at the REPL and for the compiler. So, it's done a bit differently now, only chasing everything on a "full" load (i.e., final load at the REPL) This has some effects: + As systems get bigger, load time gets better (on my machine, checking Idris.Main now takes 52s from scratch, down from 76s) + You might find import errors that you didn't previously get, because things were being imported that shouldn't have been. The new way is correct! An unfortunate effect is that sometimes you end up getting "undefined name" errors even if you didn't explicitly use the name, because sometimes a module uses a name from another module in a type, which then gets exported, and eventually needs to be reduced. This mostly happens because there is a compile time check that should be done which I haven't implemented yet. That is, public export definitions should only be allowed to use names that are also public export. I'll get to this soon.
97 lines
3.3 KiB
Idris
97 lines
3.3 KiB
Idris
module Data.List.Views
|
|
|
|
import Control.WellFounded
|
|
import Data.List
|
|
import Data.Nat
|
|
import Data.Nat.Views
|
|
|
|
lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) ->
|
|
length (xs ++ (y :: ys)) = S (length (xs ++ ys))
|
|
lengthSuc [] _ _ = Refl
|
|
lengthSuc (x :: xs) y ys = cong S (lengthSuc xs y ys)
|
|
|
|
lengthLT : (xs : List a) -> (ys : List a) ->
|
|
LTE (length xs) (length (ys ++ xs))
|
|
lengthLT xs [] = lteRefl
|
|
lengthLT xs (x :: ys) = lteSuccRight (lengthLT _ _)
|
|
|
|
smallerLeft : (ys : List a) -> (y : a) -> (zs : List a) ->
|
|
LTE (S (S (length ys))) (S (length (ys ++ (y :: zs))))
|
|
smallerLeft [] y zs = LTESucc (LTESucc LTEZero)
|
|
smallerLeft (z :: ys) y zs = LTESucc (smallerLeft ys _ _)
|
|
|
|
smallerRight : (ys : List a) -> (zs : List a) ->
|
|
LTE (S (S (length zs))) (S (length (ys ++ (y :: zs))))
|
|
smallerRight {y} ys zs = rewrite lengthSuc ys y zs in
|
|
(LTESucc (LTESucc (lengthLT _ _)))
|
|
|
|
||| View for splitting a list in half, non-recursively
|
|
public export
|
|
data Split : List a -> Type where
|
|
SplitNil : Split []
|
|
SplitOne : (x : a) -> Split [x]
|
|
SplitPair : (x : a) -> (xs : List a) ->
|
|
(y : a) -> (ys : List a) ->
|
|
Split (x :: xs ++ y :: ys)
|
|
|
|
splitHelp : (head : a) ->
|
|
(xs : List a) ->
|
|
(counter : List a) -> Split (head :: xs)
|
|
splitHelp head [] counter = SplitOne _
|
|
splitHelp head (x :: xs) [] = SplitPair head [] x xs
|
|
splitHelp head (x :: xs) [y] = SplitPair head [] x xs
|
|
splitHelp head (x :: xs) (_ :: _ :: ys)
|
|
= case splitHelp head xs ys of
|
|
SplitOne x => SplitPair x [] _ []
|
|
SplitPair x' xs y' ys => SplitPair x' (x :: xs) y' ys
|
|
|
|
||| Covering function for the `Split` view
|
|
||| Constructs the view in linear time
|
|
export
|
|
split : (xs : List a) -> Split xs
|
|
split [] = SplitNil
|
|
split (x :: xs) = splitHelp x xs xs
|
|
|
|
public export
|
|
data SplitRec : List a -> Type where
|
|
SplitRecNil : SplitRec []
|
|
SplitRecOne : (x : a) -> SplitRec [x]
|
|
SplitRecPair : (lefts, rights : List a) -> -- Explicit, don't erase
|
|
(lrec : Lazy (SplitRec lefts)) ->
|
|
(rrec : Lazy (SplitRec rights)) -> SplitRec (lefts ++ rights)
|
|
|
|
||| Covering function for the `SplitRec` view
|
|
||| Constructs the view in O(n lg n)
|
|
public export total
|
|
splitRec : (xs : List a) -> SplitRec xs
|
|
splitRec xs with (sizeAccessible xs)
|
|
splitRec xs | acc with (split xs)
|
|
splitRec [] | acc | SplitNil = SplitRecNil
|
|
splitRec [x] | acc | SplitOne x = SplitRecOne x
|
|
splitRec (y :: ys ++ z :: zs) | Access acc | SplitPair y ys z zs
|
|
= SplitRecPair _ _
|
|
(splitRec (y :: ys) | acc _ (smallerLeft ys z zs))
|
|
(splitRec (z :: zs) | acc _ (smallerRight ys zs))
|
|
|
|
||| View for traversing a list backwards
|
|
public export
|
|
data SnocList : List a -> Type where
|
|
Empty : SnocList []
|
|
Snoc : (x : a) -> (xs : List a) ->
|
|
(rec : SnocList xs) -> SnocList (xs ++ [x])
|
|
|
|
snocListHelp : {input : _} ->
|
|
SnocList input -> (rest : List a) -> SnocList (input ++ rest)
|
|
snocListHelp snoc [] = rewrite appendNilRightNeutral input in snoc
|
|
snocListHelp snoc (x :: xs)
|
|
= rewrite appendAssociative input [x] xs in
|
|
snocListHelp (Snoc x input snoc) xs
|
|
|
|
||| Covering function for the `SnocList` view
|
|
||| Constructs the view in linear time
|
|
export
|
|
snocList : (xs : List a) -> SnocList xs
|
|
snocList xs = snocListHelp Empty xs
|
|
|
|
|