0 | module Idrall.Parser.Rule

  2 | import Data.List

  3 | import Data.List1

  4 | import Data.String

  6 | import Text.Parser

  7 | import Text.Quantity

  8 | import Text.Token

  9 | import Text.Lexer

 10 | import Text.Bounded

 12 | import Idrall.Parser.Lexer

 13 | import Idrall.Expr

 14 | import Idrall.Path

 16 | public export

 17 | Rule : {state : Type} -> Type -> Type

 18 | Rule ty = Grammar state RawToken True ty

 20 | public export

 21 | EmptyRule : {state : Type} -> Type -> Type

 22 | EmptyRule ty = Grammar state RawToken False ty

 25 | whitespace : Rule ()

 26 | whitespace =

 27 |   terminal ("Expected whitespace") $

 28 |     \case

 29 |       White => Just ()

 30 |       _ => Nothing

 33 | tokenW : Grammar state (TokenRawToken) True a -> Grammar state (TokenRawToken) True a

 34 | tokenW p = do

 35 |   x <- p

 36 |   _ <- optional whitespace

 37 |   pure x

 40 | keyword : String -> Rule ()

 41 | keyword req =

 42 |   terminal ("Expected '" ++ req ++ "'") $

 43 |     \case

 44 |       Keyword s => if s == req then Just () else Nothing

 45 |       _ => Nothing

 48 | symbol : String -> Rule ()

 49 | symbol req =

 50 |   terminal ("Expected '" ++ req ++ "'") $

 51 |     \case

 52 |       Symbol s => if s == req then Just () else Nothing

 53 |       _ => Nothing

 56 | textBegin : Rule IsMultiline

 57 | textBegin =

 58 |   terminal "expected \" or ''" $

 59 |     \case

 60 |       StringBegin x => Just x

 61 |       _ => Nothing

 64 | textBoundary : Rule ()

 65 | textBoundary =

 66 |   terminal "expected \" or ''" $

 67 |     \case

 68 |       StringBegin _ => Just ()

 69 |       StringEnd => Just ()

 70 |       _ => Nothing

 72 | escapeSingle : List Char -> List Char -> Maybe (List Char)

 73 | escapeSingle escapeChars [] = pure []

 74 | escapeSingle escapeChars (x :: xs) =

 75 |   if isPrefixOf escapeChars (x :: xs)

 76 |   then case drop (length escapeChars) (x::xs) of

 77 |        ('b' :: xs) => pure $ '\b' :: !(escapeSingle escapeChars xs)

 78 |        ('f' :: xs) => escapeSingle escapeChars ('\f' :: xs)

 79 |        ('n' :: xs) => escapeSingle escapeChars ('\n' :: xs)

 80 |        ('r' :: xs) => escapeSingle escapeChars ('\r' :: xs)

 81 |        ('t' :: xs) => escapeSingle escapeChars ('\t' :: xs)

 82 |        ('"' :: xs) => escapeSingle escapeChars ('"' :: xs)

 83 |        ('$' :: xs) => escapeSingle escapeChars ('$' :: xs)

 84 |        ('\\' :: xs) => pure $ '\\' :: !(escapeSingle escapeChars xs)

 85 |        ('/' :: xs) => escapeSingle escapeChars ('/' :: xs)

 86 |        -- TODO unicode

 87 |        _ => pure $ x :: !(escapeSingle escapeChars xs)

 88 |   else Just $ x :: !(escapeSingle escapeChars xs)

 90 | escape : IsMultiline -> String -> Maybe String

 91 | escape Single str = Just $ pack $ !(escapeSingle ['\\'] $ unpack str)

 92 | escape Multi str = Just $ str

 95 | textLit : IsMultiline -> Rule String

 96 | textLit x =

 97 |   terminal "expected valid Text" $

 98 |     \case

 99 |       StringLit str => escape x str

100 |       _ => Nothing

103 | interpBegin : Rule ()

104 | interpBegin =

105 |   terminal "expected ${" $

106 |     \case

107 |       InterpBegin => Just ()

108 |       _ => Nothing

111 | interpEnd : Rule ()

112 | interpEnd =

113 |   terminal "expected }" $

114 |     \case

115 |       InterpEnd => Just ()

116 |       _ => Nothing

119 | identPart : Rule String

120 | identPart =

121 |   terminal "expected name" $

122 |     \case

123 |       Ident x => Just x

124 |       _ => Nothing

127 | fieldName : Rule String

128 | fieldName =

129 |   terminal "expected fieldName" $

130 |     \case

131 |       Ident x => Just x

132 |       Builtin x => Just x

133 |       _ => Nothing

136 | missingImport : Rule ()

137 | missingImport =

138 |   terminal "expected missing" $

139 |     \case

140 |       MissingImport => Just ()

141 |       _ => Nothing

144 | httpImport : Rule String

145 | httpImport =

146 |   terminal "expected http import" $

147 |     \case

148 |       HttpImport x => Just x

149 |       _ => Nothing

152 | envImport : Rule String

153 | envImport =

154 |   terminal "expected env import" $

155 |     \case

156 |       EnvImport x => Just x

157 |       _ => Nothing

160 | arrow : Rule ()

161 | arrow = tokenW $ symbol "->" <|> symbol "→"

164 | shaImport : Rule String

165 | shaImport =

166 |   terminal "expected sha import" $

167 |     \case

168 |       Sha x => Just x -- TODO remove `sha:` prefix

169 |       _ => Nothing

172 | filePath : Rule Path

173 | filePath =

174 |   terminal "expected import path" $

175 |     \case

176 |       RelImport x => Just $ Relative $ forget $ split (== '/') x

177 |       AbsImport x => Just $ Absolute $ forget $ split (== '/') x

178 |       HomeDirImport x => Just $ Home $ forget $ split (== '/') x

179 |       _ => Nothing

182 | naturalLit : Rule Nat

183 | naturalLit =

184 |   terminal "expected natural" $

185 |     \case

186 |       TNatural x => Just x

187 |       _ => Nothing

190 | integerLit : Rule Integer

191 | integerLit =

192 |   terminal "expected integer" $

193 |     \case

194 |       TInteger x => Just x

195 |       _ => Nothing

198 | doubleLit : Rule Double

199 | doubleLit =

200 |   terminal "expected double" $

201 |     \case

202 |       TDouble x => Just x

203 |       _ => Nothing

206 | dottedList : Rule (List1 FieldName)

207 | dottedList = do

208 |   _ <- optional whitespace

209 |   x <- sepBy1 (tokenW $ symbol ".") (identPart)

210 |   pure $ map MkFieldName x

213 | dottedListRec : Rule (List1 FieldName)

214 | dottedListRec = do

215 |   _ <- optional whitespace

216 |   x <- sepBy1 (tokenW $ symbol ".") (fieldName)

217 |   pure $ map MkFieldName x

221 | builtin : Rule String

222 | builtin =

223 |   terminal "expected builtin" $

224 |     \case

225 |       Builtin x => Just x

226 |       _ => Nothing

229 | someBuiltin : Rule ()

230 | someBuiltin =

231 |   terminal "expected builtin" $

232 |     \case

233 |       Builtin "Some" => Just ()

234 |       _ => Nothing

237 | endOfInput : Rule ()

238 | endOfInput =

239 |   terminal "expected builtin" $

240 |     \case

241 |       EndInput => Just ()

242 |       _ => Nothing