git.iko.soy/Idris-dev
on master help sign in
Control.Delayed: utilities for conditional `Lazy` or `Inf`
fd9a45aMichael Morgan
libs/contrib/Control/Delayed.idrnew file+26
compare with master
unifiedsplit
@@ -0,0 +1,26 @@
1+||| Utilities functions for contitionally delaying values.
2+module Control.Delayed
3+
4+%default total
5+
6+||| Type-level function for a conditionally delayed type (`Lazy` or `Inf`).
7+public export
8+delayed : DelayReason -> Bool -> Type -> Type
9+delayed r False a = a
10+delayed r True a = Delayed r a
11+
12+||| Type-level function for a conditionally infinite type.
13+public export
14+inf : Bool -> Type -> Type
15+inf = delayed Infinite
16+
17+||| Type-level function for a conditionally lazy type.
18+public export
19+lazy : Bool -> Type -> Type
20+lazy = delayed LazyValue
21+
22+||| Conditionally delay a value.
23+export
24+delay : (d : Bool) -> a -> delayed r d a
25+delay False x = x
26+delay True x = Delay x
libs/contrib/Text/Lexer.idr+2−5
@@ -1,5 +1,7 @@
1module Text.Lexer
1module Text.Lexer
2
2
3+import public Control.Delayed
4+
3%default total
5%default total
4
6
5||| A language of token recognisers.
7||| A language of token recognisers.
@@ -20,11 +22,6 @@ public export
20Lexer : Type
22Lexer : Type
21Lexer = Recognise True
23Lexer = Recognise True
22
24
23−public export
24−inf : Bool -> Type -> Type
25−inf True t = Inf t
26−inf False t = t
27−
28||| Sequence two recognisers. If either consumes a character, the sequence
25||| Sequence two recognisers. If either consumes a character, the sequence
29||| is guaranteed to consume a character.
26||| is guaranteed to consume a character.
30export %inline
27export %inline
libs/contrib/Text/Parser.idr+2−5
@@ -1,5 +1,7 @@
1module Text.Parser
1module Text.Parser
2
2
3+import public Control.Delayed
4+
3%default total
5%default total
4
6
5-- TODO: Add some primitives for helping with error messages.
7-- TODO: Add some primitives for helping with error messages.
@@ -29,11 +31,6 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
29 Grammar tok c1 ty -> Grammar tok c2 ty ->
31 Grammar tok c1 ty -> Grammar tok c2 ty ->
30 Grammar tok (c1 && c2) ty
32 Grammar tok (c1 && c2) ty
31
33
32−public export
33−inf : Bool -> Type -> Type
34−inf True t = Inf t
35−inf False t = t
36−
37||| Sequence two grammars. If either consumes some input, the sequence is
34||| Sequence two grammars. If either consumes some input, the sequence is
38||| guaranteed to consume some input. If the first one consumes input, the
35||| guaranteed to consume some input. If the first one consumes input, the
39||| second is allowed to be recursive (because it means some input has been
36||| second is allowed to be recursive (because it means some input has been
libs/contrib/contrib.ipkg+1
@@ -9,6 +9,7 @@ modules = CFFI
9 , Control.Algebra.Lattice
9 , Control.Algebra.Lattice
10 , Control.Algebra.NumericImplementations
10 , Control.Algebra.NumericImplementations
11 , Control.Algebra.VectorSpace
11 , Control.Algebra.VectorSpace
12+ , Control.Delayed
12 , Control.Isomorphism.Primitives
13 , Control.Isomorphism.Primitives
13 , Control.Partial
14 , Control.Partial
14 , Control.Pipeline
15 , Control.Pipeline