
   0 | module TyRE.Core
   1 | 
   2 | import public Data.List
   3 | import public Data.Either
   4 | import public Data.SortedSet
   5 | import public Data.List1
   6 | import Data.SnocList
   7 | 
   8 | infixr 6 <*>, <*, *>
   9 | 
  10 | public export 
  11 | data CharCond =
  12 |       OneOf (SortedSet Char)
  13 |     | Range (Char, Char)
  14 |     | Pred (Char -> Bool)
  15 | 
  16 | public export
  17 | Eq CharCond where
  18 |   (==) (OneOf x) (OneOf y) = x == y
  19 |   (==) (OneOf x) _ = False
  20 |   (==) (Range x) (Range y) = x == y
  21 |   (==) (Range x) _ = False
  22 |   (==) (Pred _) _ = False
  23 | 
  24 | public export
  25 | satisfies : CharCond -> Char -> Bool
  26 | satisfies (OneOf xs) c = contains c xs
  27 | satisfies (Range (x, y)) c = x <= c && c <= y
  28 | satisfies (Pred f) c = f c
  29 | 
  30 | public export
  31 | data TyRE : Type -> Type where
  32 |   Empty     : TyRE ()
  33 |   MatchChar : CharCond -> TyRE Char
  34 |   Group     : TyRE a -> TyRE String
  35 |   (<*>)     : {0 a,b : Type} -> TyRE a -> TyRE b -> TyRE (a, b)
  36 |   Conv      : {0 a,b : Type} -> TyRE a -> (a -> b) -> TyRE b
  37 |   (<|>)     : {0 a,b : Type} -> TyRE a -> TyRE b -> TyRE (Either a b)
  38 |   Rep       : {0 a   : Type} -> TyRE a -> TyRE (SnocList a)
  39 | 
  40 | public export
  41 | Functor TyRE where
  42 |   map f tyre = Conv tyre f
  43 | 
  44 | public export
  45 | predicate : (Char -> Bool) -> TyRE Char
  46 | predicate f = MatchChar (Pred f)
  47 | 
  48 | public export
  49 | empty : TyRE ()
  50 | empty = Empty
  51 | 
  52 | public export
  53 | any : TyRE Char
  54 | any = predicate (\_ => True)
  55 | 
  56 | public export
  57 | group : TyRE a -> TyRE String
  58 | group tyre = Group tyre
  59 | 
  60 | public export
  61 | ignore : TyRE a -> TyRE ()
  62 | ignore tyre = (\_ => ()) `map` (group tyre)
  63 | 
  64 | public export
  65 | range : Char -> Char -> TyRE Char
  66 | range x y = MatchChar (Range (x,y))
  67 | 
  68 | public export
  69 | digit : TyRE Integer
  70 | digit = (\c => cast c - cast '0') `map` range '0' '9'
  71 | 
  72 | public export
  73 | digitChar : TyRE Char
  74 | digitChar = range '0' '9'
  75 | 
  76 | public export
  77 | oneOfCharsList : List Char -> TyRE Char
  78 | oneOfCharsList xs = MatchChar (OneOf (fromList xs))
  79 | 
  80 | public export
  81 | oneOfChars : String -> TyRE Char
  82 | oneOfChars xs = oneOfCharsList (unpack xs)
  83 | 
  84 | public export
  85 | match : Char -> TyRE ()
  86 | match c = ignore $ oneOfCharsList [c]
  87 | 
  88 | public export
  89 | rep0 : TyRE a -> TyRE (List a)
  90 | rep0 tyre = cast `map` Rep tyre
  91 | 
  92 | public export
  93 | rep1 : TyRE a -> TyRE (List a)
  94 | rep1 tyre = (\(e,l) => e::l) `map` (tyre <*> rep0 tyre)
  95 | 
  96 | public export
  97 | rep1l1 : TyRE a -> TyRE (List1 a)
  98 | rep1l1 tyre = (\(e,l) => e:::l) `map` (tyre <*> rep0 tyre)
  99 | 
 100 | public export
 101 | option : TyRE a -> TyRE (Maybe a)
 102 | option tyre = (\e => case e of {(Left x) => Just x ; (Right _) => Nothing}) `map` tyre <|> empty
 103 | 
 104 | public export
 105 | (*>) : TyRE a -> TyRE b -> TyRE b
 106 | (*>) t1 t2 = snd `map` (ignore t1 <*> t2)
 107 | 
 108 | public export
 109 | (<*) : TyRE a -> TyRE b -> TyRE a
 110 | (<*) t1 t2 = fst `map` (t1 <*> ignore t2)
 111 | 
 112 | public export
 113 | or : TyRE a -> TyRE a -> TyRE a
 114 | or t1 t2 = fromEither `map` (t1 <|> t2)
 115 | 
 116 | public export
 117 | oneOf : List1 (TyRE a) -> TyRE a
 118 | oneOf (head ::: []) = head
 119 | oneOf (head ::: (x :: xs)) = oneOf $ (head `or` x) ::: xs
 120 | 
 121 | public export
 122 | letter : TyRE Char
 123 | letter = range 'a' 'z' `or` range 'A' 'Z'
 124 | 
 125 | public export
 126 | repFrom : Nat -> TyRE a -> TyRE (List a)
 127 | repFrom 0 re = rep0 re
 128 | repFrom (S k) re = (\(e,l) => e::l) `map` (re <*> repFrom k re)
 129 | 
 130 | public export
 131 | repTo : Nat -> TyRE a -> TyRE (List a)
 132 | repTo 0 re = const [] `map` empty
 133 | repTo (S k) re = 
 134 |   optionalAdd `map` (option re <*> repTo k re) where
 135 |     optionalAdd : (Maybe a, List a) -> List a
 136 |     optionalAdd (Nothing, xs) = xs
 137 |     optionalAdd ((Just x), xs) = x::xs
 138 | 
 139 | public export
 140 | repFromTo : (from : Nat) -> (to : Nat) -> {auto prf : from <= to = True} -> TyRE a -> TyRE (List a)
 141 | repFromTo 0 0 _ = const [] `map` empty
 142 | repFromTo 0 (S from) re = repTo (S from) re
 143 | repFromTo (S from) 0 re {prf} = absurd prf
 144 | repFromTo (S from) (S to) re = (\(e,l) => e::l) `map` (re <*> repFromTo from to re)
 145 | 
 146 | public export
 147 | repTimesType : (n : Nat) -> (reType : Type) -> Type
 148 | repTimesType 0 reType = Unit
 149 | repTimesType 1 reType = reType
 150 | repTimesType (S (S k)) reType = (reType, (repTimesType (S k) reType))
 151 | 
 152 | public export
 153 | repTimes : (n : Nat)-> (re : TyRE a) -> TyRE (repTimesType n a)
 154 | repTimes 0 re = empty
 155 | repTimes 1 re = re
 156 | repTimes (S (S k)) re = re <*> repTimes (S k) re
 157 | 
 158 | public export
 159 | isConsuming : (re : TyRE a) -> Bool
 160 | isConsuming (r1 <*> r2) = isConsuming r1 || isConsuming r2
 161 | isConsuming (Conv r f) = isConsuming r
 162 | isConsuming (r1 <|> r2) = isConsuming r1 && isConsuming r2
 163 | isConsuming (Rep r1) = False
 164 | isConsuming Empty = False
 165 | isConsuming (MatchChar _) = True
 166 | isConsuming (Group r) = isConsuming r
 167 | 
 168 | public export
 169 | data IsConsuming : TyRE a -> Type where
 170 |   ItIsConsuming : {re : TyRE a} -> {auto 0 prf : isConsuming re = True}
 171 |                 -> IsConsuming re
 172 | 
 173 | leftBranchTrue : (a = True) -> (a || b = True)
 174 | leftBranchTrue Refl = Refl
 175 | 
 176 | rightBranchTrue : {a : Bool} -> (b = True) -> (a || b = True)
 177 | rightBranchTrue {a = False} Refl = Refl
 178 | rightBranchTrue {a = True} Refl = Refl
 179 |