Merge pull request #3370 from rtfeldman/list-unreachable

List unreachable
This commit is contained in:
Richard Feldman 2022-07-06 10:45:50 -04:00 committed by GitHub
commit 7365da6f69
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 41 additions and 10 deletions

View file

@ -373,17 +373,11 @@ contains = \list, needle ->
## `fold`, `foldLeft`, or `foldl`.
walk : List elem, state, (state, elem -> state) -> state
walk = \list, state, func ->
walkHelp list state func 0 (len list)
walkHelp = \currentState, element -> Continue (func currentState element)
## internal helper
walkHelp : List elem, state, (state, elem -> state), Nat, Nat -> state
walkHelp = \list, state, f, index, length ->
if index < length then
nextState = f state (getUnsafe list index)
walkHelp list nextState f (index + 1) length
else
state
when List.iterate list state walkHelp is
Continue newState -> newState
Break void -> List.unreachable void
## Note that in other languages, `walkBackwards` is sometimes called `reduceRight`,
## `fold`, `foldRight`, or `foldr`.
@ -841,3 +835,6 @@ iterHelp = \list, state, f, index, length ->
Break b
else
Continue state
## useful for typechecking guaranteed-unreachable cases
unreachable : [] -> a