git.iko.soy/Idris-dev
on master help sign in
Text.Lexer: add `concat`
a792d6bMichael Morgan
libs/contrib/Data/Bool/Extra.idr+4
compare with master
unifiedsplit
@@ -26,3 +26,7 @@ orFalseNeutral True = Refl
26orTrueTrue : (x : Bool) -> x || True = True
26orTrueTrue : (x : Bool) -> x || True = True
27orTrueTrue False = Refl
27orTrueTrue False = Refl
28orTrueTrue True = Refl
28orTrueTrue True = Refl
29+
30+orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
31+orSameAndRightNeutral False _ = Refl
32+orSameAndRightNeutral True _ = Refl
libs/contrib/Text/Lexer.idr+10
@@ -1,5 +1,7 @@
1module Text.Lexer
1module Text.Lexer
2
2
3+import Data.Bool.Extra
4+
3import public Control.Delayed
5import public Control.Delayed
4
6
5%default total
7%default total
@@ -61,6 +63,14 @@ export
61reject : Recognise c -> Recognise False
63reject : Recognise c -> Recognise False
62reject = Lookahead False
64reject = Lookahead False
63
65
66+||| Sequence a list of recognisers.
67+export
68+concat : {c : Bool} -> (xs : List (Recognise c)) -> Recognise (c && isCons xs)
69+concat {c} [] = rewrite andFalseFalse c in Empty
70+concat {c} (x :: xs) = rewrite andTrueNeutral c in
71+ rewrite sym (orSameAndRightNeutral c (isCons xs)) in
72+ SeqEmpty x (concat xs)
73+
64data StrLen : Type where
74data StrLen : Type where
65 MkStrLen : String -> Nat -> StrLen
75 MkStrLen : String -> Nat -> StrLen
66
76