git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4245 from msmorgan/data-fuel

Data.Fuel: move `Fuel` data type from Control.ST to its own module

commit5218727b2f6cc14d7992cc3409a1f4d7dfef35c1 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateWed 6 Dec 2017, 09:33 (9 years ago) parentd773edd99f0d60
4 files changed+26−11
compare with master
unifiedsplit
CHANGELOG.md+1 libs/contrib/Control/ST.idr+6−11 libs/contrib/Data/Fuel.idr+18 libs/contrib/contrib.ipkg+1
CHANGELOG.md+1
@@ -52,6 +52,7 @@
5252 * Lowered the precedence of `>>=` to be below that of `<|>`.
5353+ Added some useful string manipulation functions to `Data.String.Extra`.
5454+ Added `Control.Delayed`, a module for conditionally making a type `Inf` or `Lazy`.
55++ Added `Data.Fuel`, which implements the `Fuel` data type and the partial `forever` function.
5556+ Added `Data.Bool.Extra`, a module with properties of boolean operations.
5657+ Moved core of `Text.Lexer` to `Text.Lexer.Core`. Added several new combinators
5758 and lexers to `Text.Lexer`.
libs/contrib/Control/ST.idr+6−11
@@ -1,7 +1,9 @@
11module Control.ST
22
3−import Language.Reflection.Utils
43import Control.IOExcept
4+import Language.Reflection.Utils
5+
6+import public Data.Fuel
57
68%default total
79
@@ -394,13 +396,6 @@ runST env (Call prog res_prf) k
394396runST env (Read lbl prf) k = k (lookupEnv prf env) env
395397runST env (Write lbl prf val) k = k () (updateEnv prf env val)
396398
397−export
398−data Fuel = Empty | More (Lazy Fuel)
399−
400−export partial
401−forever : Fuel
402−forever = More forever
403−
404399runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->
405400 (k : (x : a) -> Env (outfn x) -> m b) ->
406401 (onDry : m b) -> m b
@@ -589,10 +584,10 @@ run prog = runST [] prog (\res, env' => pure res)
589584
590585export
591586runLoop : Applicative m => Fuel -> STLoop m a [] ->
592− (onEmpty : m a) ->
587+ (onDry : m a) ->
593588 m a
594−runLoop fuel prog onEmpty
595− = runSTLoop fuel [] prog (\res, env' => pure res) onEmpty
589+runLoop fuel prog onDry
590+ = runSTLoop fuel [] prog (\res, env' => pure res) onDry
596591
597592||| runWith allows running an STrans program with an initial environment,
598593||| which must be consumed.
libs/contrib/Data/Fuel.idrnew file+18
@@ -0,0 +1,18 @@
1+module Data.Fuel
2+
3+%access public export
4+%default total
5+
6+||| Fuel for running total operations potentially indefinitely.
7+data Fuel = Dry | More (Lazy Fuel)
8+
9+||| Provide `n` units of fuel.
10+limit : Nat -> Fuel
11+limit Z = Dry
12+limit (S n) = More (limit n)
13+
14+||| Provide fuel indefinitely.
15+||| This function is fundamentally partial.
16+partial
17+forever : Fuel
18+forever = More forever
libs/contrib/contrib.ipkg+1
@@ -28,6 +28,7 @@ modules = CFFI
2828 , Data.Combinators.Applicative
2929 , Data.Combinators.Arrow
3030 , Data.Fin.Extra
31+ , Data.Fuel
3132 , Data.Fun
3233 , Data.Hash
3334 , Data.Heap