git.iko.soy/Idris-dev
on master help sign in
Control.Delayed: utilities for conditional `Lazy` or `Inf`

this abstracts a pattern common to Text.Lexer and Text.Parser Due to a bug in Idris, this module must be imported with `import public` when a module exports functions whose types use these functions.

commitfd9a45a905ff0d91b57b14d00b490bf523e173e1 authorMichael Morgan <morgan.michael@me.com> dateThu 26 Oct 2017, 18:06 (9 years ago) parentb6d3c48
4 files changed+31−10
compare with master
unifiedsplit
libs/contrib/Control/Delayed.idr+26 libs/contrib/Text/Lexer.idr+2−5 libs/contrib/Text/Parser.idr+2−5 libs/contrib/contrib.ipkg+1
libs/contrib/Control/Delayed.idrnew file+26
@@ -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 @@
11module Text.Lexer
22
3+import public Control.Delayed
4+
35%default total
46
57||| A language of token recognisers.
@@ -20,11 +22,6 @@ public export
2022Lexer : Type
2123Lexer = Recognise True
2224
23−public export
24−inf : Bool -> Type -> Type
25−inf True t = Inf t
26−inf False t = t
27−
2825||| Sequence two recognisers. If either consumes a character, the sequence
2926||| is guaranteed to consume a character.
3027export %inline
libs/contrib/Text/Parser.idr+2−5
@@ -1,5 +1,7 @@
11module Text.Parser
22
3+import public Control.Delayed
4+
35%default total
46
57-- TODO: Add some primitives for helping with error messages.
@@ -29,11 +31,6 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
2931 Grammar tok c1 ty -> Grammar tok c2 ty ->
3032 Grammar tok (c1 && c2) ty
3133
32−public export
33−inf : Bool -> Type -> Type
34−inf True t = Inf t
35−inf False t = t
36−
3734||| Sequence two grammars. If either consumes some input, the sequence is
3835||| guaranteed to consume some input. If the first one consumes input, the
3936||| second is allowed to be recursive (because it means some input has been
libs/contrib/contrib.ipkg+1
@@ -9,6 +9,7 @@ modules = CFFI
99 , Control.Algebra.Lattice
1010 , Control.Algebra.NumericImplementations
1111 , Control.Algebra.VectorSpace
12+ , Control.Delayed
1213 , Control.Isomorphism.Primitives
1314 , Control.Partial
1415 , Control.Pipeline