git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4245 from msmorgan/data-fuel
5218727Ahmad Salim Al-Sibahi
CHANGELOG.md+1
compare with master
unifiedsplit
@@ -52,6 +52,7 @@
52 * Lowered the precedence of `>>=` to be below that of `<|>`.
52 * Lowered the precedence of `>>=` to be below that of `<|>`.
53+ Added some useful string manipulation functions to `Data.String.Extra`.
53+ Added some useful string manipulation functions to `Data.String.Extra`.
54+ Added `Control.Delayed`, a module for conditionally making a type `Inf` or `Lazy`.
54+ 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.
55+ Added `Data.Bool.Extra`, a module with properties of boolean operations.
56+ Added `Data.Bool.Extra`, a module with properties of boolean operations.
56+ Moved core of `Text.Lexer` to `Text.Lexer.Core`. Added several new combinators
57+ Moved core of `Text.Lexer` to `Text.Lexer.Core`. Added several new combinators
57 and lexers to `Text.Lexer`.
58 and lexers to `Text.Lexer`.
libs/contrib/Control/ST.idr+6−11
@@ -1,7 +1,9 @@
1module Control.ST
1module Control.ST
2
2
3−import Language.Reflection.Utils
4import Control.IOExcept
3import Control.IOExcept
4+import Language.Reflection.Utils
5+
6+import public Data.Fuel
5
7
6%default total
8%default total
7
9
@@ -394,13 +396,6 @@ runST env (Call prog res_prf) k
394runST env (Read lbl prf) k = k (lookupEnv prf env) env
396runST env (Read lbl prf) k = k (lookupEnv prf env) env
395runST env (Write lbl prf val) k = k () (updateEnv prf env val)
397runST env (Write lbl prf val) k = k () (updateEnv prf env val)
396
398
397−export
398−data Fuel = Empty | More (Lazy Fuel)
399−
400−export partial
401−forever : Fuel
402−forever = More forever
403−
404runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->
399runSTLoop : Fuel -> Env invars -> STransLoop m a invars outfn ->
405 (k : (x : a) -> Env (outfn x) -> m b) ->
400 (k : (x : a) -> Env (outfn x) -> m b) ->
406 (onDry : m b) -> m b
401 (onDry : m b) -> m b
@@ -589,10 +584,10 @@ run prog = runST [] prog (\res, env' => pure res)
589
584
590export
585export
591runLoop : Applicative m => Fuel -> STLoop m a [] ->
586runLoop : Applicative m => Fuel -> STLoop m a [] ->
592− (onEmpty : m a) ->
587+ (onDry : m a) ->
593 m a
588 m a
594−runLoop fuel prog onEmpty
589+runLoop fuel prog onDry
595− = runSTLoop fuel [] prog (\res, env' => pure res) onEmpty
590+ = runSTLoop fuel [] prog (\res, env' => pure res) onDry
596
591
597||| runWith allows running an STrans program with an initial environment,
592||| runWith allows running an STrans program with an initial environment,
598||| which must be consumed.
593||| 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
28 , Data.Combinators.Applicative
28 , Data.Combinators.Applicative
29 , Data.Combinators.Arrow
29 , Data.Combinators.Arrow
30 , Data.Fin.Extra
30 , Data.Fin.Extra
31+ , Data.Fuel
31 , Data.Fun
32 , Data.Fun
32 , Data.Hash
33 , Data.Hash
33 , Data.Heap
34 , Data.Heap