0 | module Text.ILex.Derive
  1 |
  2 | import public Language.Reflection.Util
  3 |
  4 | %default total
  5 |
  6 | --------------------------------------------------------------------------------
  7 | -- Deriving Parser States
  8 | --------------------------------------------------------------------------------
  9 |
 10 | ||| Given names for the number of states (`size`), the
 11 | ||| parser state (`state`), and the distinct parser states,
 12 | ||| this will compute the actual number of states and define
 13 | ||| a constant for each state.
 14 | |||
 15 | ||| For instance, `deriveParserState "SZ" "ST" ["SIni", "Str", "Err", "Done"]`
 16 | ||| will generate the following definitions:
 17 | |||
 18 | ||| ```idris
 19 | ||| public export
 20 | ||| SZ : Bits32
 21 | ||| SZ = 4
 22 | |||
 23 | ||| public export
 24 | ||| 0 ST : Type
 25 | ||| ST = Index SZ
 26 | |||
 27 | ||| export
 28 | ||| SIni : ST
 29 | ||| SIni = I 0
 30 | |||
 31 | ||| export
 32 | ||| Str : ST
 33 | ||| Str = I 1
 34 | |||
 35 | ||| export
 36 | ||| Err : ST
 37 | ||| Err = I 2
 38 | |||
 39 | ||| export
 40 | ||| Done : ST
 41 | ||| Done = I 3
 42 | |||
 43 | ||| export
 44 | ||| showST : ST -> String
 45 | ||| showST (I 0) = "SIni"
 46 | ||| showST (I 1) = "Str"
 47 | ||| showST (I 2) = "Err"
 48 | ||| showST (I 3) = "Done"
 49 | ||| showST _     = "impossible"
 50 | ||| ```
 51 | export
 52 | deriveParserState :
 53 |      {auto elb : Elaboration m}
 54 |   -> (size, state : Name)
 55 |   -> (states : List Name)
 56 |   -> m ()
 57 | deriveParserState sz st ss =
 58 |  let count      := primVal $ B32 $ cast (length ss)
 59 |      decls      := defs [<] count ss 0
 60 |      sizeClaim  := public' sz `(Bits32)
 61 |      sizeDefn   := def sz [patClause (var sz) count]
 62 |      stateClaim := claim M0 Public [] st type
 63 |      stateDefn  := def st [patClause (var st) `(Index ~(var sz))]
 64 |      showName   := fromString "show\{st}"
 65 |      showVar    := var showName
 66 |      showClaim  := export' showName `(~(var st) -> String)
 67 |      showDecl   := def showName (shows [<] showVar ss 0)
 68 |
 69 |   in declare $
 70 |        [sizeClaim, sizeDefn, stateClaim, stateDefn] ++ decls ++ [showClaim, showDecl]
 71 |
 72 |   where
 73 |     defs : SnocList Decl -> TTImp -> List Name -> Bits32 -> List Decl
 74 |     defs sd c []      _ = sd <>> []
 75 |     defs sd c (n::ns) x =
 76 |      let claim := export' n (var st)
 77 |          defn  := def n [patClause (var n) `(I ~(primVal $ B32 x))]
 78 |       in defs (sd :< claim :< defn) c ns (x+1)
 79 |
 80 |     shows : SnocList Clause -> TTImp -> List Name -> Bits32 -> List Clause
 81 |     shows sc v []      _ = sc <>> [patClause `(~(v) _) `("impossible")]
 82 |     shows sc v (n::ns) x =
 83 |      let c := patClause `(~(v) (I ~(primVal $ B32 x))) n.namePrim
 84 |       in shows (sc :< c) v ns (x+1)
 85 |
 86 | --------------------------------------------------------------------------------
 87 | -- Deriving Interfaces
 88 | --------------------------------------------------------------------------------
 89 |
 90 | dropLastArg : List Arg -> List Arg
 91 | dropLastArg args =
 92 |   case [<] <>< args of
 93 |     sa :< _ => sa <>> []
 94 |     [<]     => []
 95 |
 96 | unapply1 : TTImp -> TTImp
 97 | unapply1 (IApp      fc f _)   = f
 98 | unapply1 (INamedApp fc f _ _) = f
 99 | unapply1 t                    = t
100 |
101 | ifaceType : ParamTypeInfo -> TTImp -> TTImp
102 | ifaceType p t = piAll t (dropLastArg p.implicits)
103 |
104 | copyImpl : TTImp
105 | copyImpl =
106 |   `(\s,o,bs,buf,rf,rt,sk =>
107 |       { bufSize_    := s
108 |       , cur_        := buf
109 |       , prev_       := bs
110 |       , prevOffset_ := o
111 |       , curOffset_  := o + bs.size
112 |       , from_       := rf
113 |       , till_       := rt
114 |       } sk
115 |    )
116 |
117 | ||| Derives an implementation of `HasBytes` for a record type with the
118 | ||| following fields:
119 | |||
120 | ||| ```idris
121 | |||   bufSize_    : Nat
122 | |||   prev_       : ByteString
123 | |||   cur_        : IBuffer bufSize_
124 | |||   prevOffset_ : Nat
125 | |||   curOffset_  : Nat
126 | |||   from_       : Ref q (LTENat bufSize_)
127 | |||   till_       : Ref q (LTENat bufSize_)
128 | |||   positions_  : Ref q (SnocList BytePos)
129 | ||| ```
130 | export
131 | HasBytes : List Name -> ParamTypeInfo -> Res (List TopLevel)
132 | HasBytes nms p =
133 |  let impl := implName p "HasBytes"
134 |   in Right [ TL (clm impl) (dfn impl) ]
135 |   where
136 |     clm : (impl : Name) -> Decl
137 |     clm impl =
138 |      let arg := unapply1 p.applied
139 |       in implClaimVis Export impl (ifaceType p $ var "HasBytes" `app` arg)
140 |
141 |     dfn : (impl : Name) -> Decl
142 |     dfn impl =
143 |       def impl
144 |         [patClause (var impl)
145 |           `( MkHB
146 |                ~(copyImpl)
147 |                bufSize_ prev_ cur_ prevOffset_ curOffset_ from_ till_ positions_
148 |            )]
149 |
150 | ||| Derives an implementation of `HasStringLits` for a record type with the
151 | ||| following field:
152 | |||
153 | ||| ```idris
154 | ||| strings_     : Ref q (SnocList String)
155 | ||| ```
156 | export
157 | HasStringLits : List Name -> ParamTypeInfo -> Res (List TopLevel)
158 | HasStringLits nms p =
159 |  let impl := implName p "HasStringLits"
160 |   in Right [ TL (clm impl) (dfn impl) ]
161 |   where
162 |     clm : (impl : Name) -> Decl
163 |     clm impl =
164 |      let arg := unapply1 p.applied
165 |       in implClaimVis Export impl (ifaceType p $ var "HasStringLits" `app` arg)
166 |
167 |     dfn : (impl : Name) -> Decl
168 |     dfn impl = def impl [patClause (var impl) `(MkHSL strings_)]
169 |
170 | errErr : Res a
171 | errErr = Left "HasError can only be derived for a record type with a field name `error_`"
172 |
173 | errType : ParamTypeInfo -> Res TTImp
174 | errType p =
175 |   case p.cons of
176 |     [c] => go (toList c.args)
177 |     _   => errErr
178 |   where
179 |     go : List (ConArg p.numParams) -> Res TTImp
180 |     go []      = errErr
181 |     go (ParamArg {}::as) = go as
182 |     go (CArg mnm rig pinfo x::as) =
183 |       case mnm == Just "error_" of
184 |         False => go as
185 |         True  => case x of
186 |           -- `Ref q (Maybe (BoundedErr e))`
187 |           (PApp refq (PApp m (PApp b z))) => Right (ttimp p.paramNames z)
188 |           _                               => errErr
189 |
190 | ||| Derives an implementation of `HasError` for a record type with the
191 | ||| following field:
192 | |||
193 | ||| ```idris
194 | ||| error_     : Ref q (Maybe $ BoundedErr e)
195 | ||| ```
196 | |||
197 | ||| The error type `e` can be freely chosen (it can also be a parameter) and
198 | ||| will be determined when deriving the implementation.
199 | export
200 | HasError : List Name -> ParamTypeInfo -> Res (List TopLevel)
201 | HasError nms p =
202 |  let impl := implName p "HasError"
203 |      Right c := clm impl | Left x => Left x
204 |   in Right [TL c (dfn impl)]
205 |   where
206 |     clm : (impl : Name) -> Res Decl
207 |     clm impl =
208 |      let arg      := unapply1 p.applied
209 |          Right te := errType p | Left x => Left x
210 |       in Right $ implClaimVis Export impl (ifaceType p $ appAll "HasError" [arg,te])
211 |
212 |     dfn : (impl : Name) -> Decl
213 |     dfn impl = def impl [patClause (var impl) `(MkHE error_)]
214 |
215 | ||| Derives an implementation of `HasBBEr` for a record type with the
216 | ||| following field:
217 | |||
218 | ||| ```idris
219 | ||| error_     : Ref q (Maybe $ BBErr e)
220 | ||| ```
221 | |||
222 | ||| The error type `e` can be freely chosen (it can also be a parameter) and
223 | ||| will be determined when deriving the implementation.
224 | export
225 | HasBBErr : List Name -> ParamTypeInfo -> Res (List TopLevel)
226 | HasBBErr nms p =
227 |  let impl := implName p "HasBBErr"
228 |      Right c := clm impl | Left x => Left x
229 |   in Right [TL c (dfn impl)]
230 |   where
231 |     clm : (impl : Name) -> Res Decl
232 |     clm impl =
233 |      let arg      := unapply1 p.applied
234 |          Right te := errType p | Left x => Left x
235 |       in Right $ implClaimVis Export impl (ifaceType p $ appAll "HasBBErr" [arg,te])
236 |
237 |     dfn : (impl : Name) -> Decl
238 |     dfn impl = def impl [patClause (var impl) `(MkBE error_)]
239 |
240 | stackErr : Res a
241 | stackErr = Left "HasStack can only be derived for a record type with a field name `stack_`"
242 |
243 | stackType : ParamTypeInfo -> Res TTImp
244 | stackType p =
245 |   case p.cons of
246 |     [c] => go (toList c.args)
247 |     _   => stackErr
248 |   where
249 |     go : List (ConArg p.numParams) -> Res TTImp
250 |     go []      = stackErr
251 |     go (ParamArg {}::as) = go as
252 |     go (CArg mnm rig pinfo x::as) =
253 |       case mnm == Just "stack_" of
254 |         False => go as
255 |         True  => case x of
256 |           -- `Ref q a`
257 |           (PApp refq z) => Right (ttimp p.paramNames z)
258 |           _             => stackErr
259 |
260 | ||| Derives an implementation of `HasStack` for a record type with the
261 | ||| following field:
262 | |||
263 | ||| ```idris
264 | ||| stack_     : Ref q a
265 | ||| ```
266 | |||
267 | ||| The stack type `a` can be freely chosen (it can also be a parameter) and
268 | ||| will be determined when deriving the implementation.
269 | export
270 | HasStack : List Name -> ParamTypeInfo -> Res (List TopLevel)
271 | HasStack nms p =
272 |  let impl := implName p "HasStack"
273 |      Right c := clm impl | Left x => Left x
274 |   in Right [TL c (dfn impl)]
275 |   where
276 |     clm : (impl : Name) -> Res Decl
277 |     clm impl =
278 |      let arg      := unapply1 p.applied
279 |          Right ts := stackType p | Left x => Left x
280 |       in Right $ implClaimVis Export impl (ifaceType p $ appAll "HasStack" [arg,ts])
281 |
282 |     dfn : (impl : Name) -> Decl
283 |     dfn impl = def impl [patClause (var impl) `(MkHS stack_)]
284 |
285 | ||| Derives implementations of the following interfaces for a suitable
286 | ||| record type: `HasBytePos`, `HasStringLits`, `HasBBErr`, and
287 | ||| `HasStack`.
288 | export
289 | FullStack : List Name -> ParamTypeInfo -> Res (List TopLevel)
290 | FullStack nms p =
291 |   sequenceJoin
292 |     [ HasBytes nms p
293 |     , HasStringLits nms p
294 |     , HasBBErr nms p
295 |     , HasStack nms p
296 |     ]
297 |