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 | ||| Derives an implementation of `HasBytes` for a record type with the
105 | ||| following fields:
106 | |||
107 | ||| ```idris
108 | ||| prev_      : Ref q ByteString
109 | ||| cur_       : Ref q ByteString
110 | ||| offset_    : Ref q Nat
111 | ||| relpos_    : Ref q Integer
112 | ||| len_       : Ref q Nat
113 | ||| positions_ : Ref q (SnocList BytePos)
114 | ||| ```
115 | export
116 | HasBytes : List Name -> ParamTypeInfo -> Res (List TopLevel)
117 | HasBytes nms p =
118 |  let impl := implName p "HasBytes"
119 |   in Right [ TL (clm impl) (dfn impl) ]
120 |   where
121 |     clm : (impl : Name) -> Decl
122 |     clm impl =
123 |      let arg := unapply1 p.applied
124 |       in implClaimVis Export impl (ifaceType p $ var "HasBytes" `app` arg)
125 |
126 |     dfn : (impl : Name) -> Decl
127 |     dfn impl = def impl [patClause (var impl) `(MkHB prev_ cur_ offset_ relpos_ len_ positions_)]
128 |
129 | ||| Derives an implementation of `HasStringLits` for a record type with the
130 | ||| following field:
131 | |||
132 | ||| ```idris
133 | ||| strings_     : Ref q (SnocList String)
134 | ||| ```
135 | export
136 | HasStringLits : List Name -> ParamTypeInfo -> Res (List TopLevel)
137 | HasStringLits nms p =
138 |  let impl := implName p "HasStringLits"
139 |   in Right [ TL (clm impl) (dfn impl) ]
140 |   where
141 |     clm : (impl : Name) -> Decl
142 |     clm impl =
143 |      let arg := unapply1 p.applied
144 |       in implClaimVis Export impl (ifaceType p $ var "HasStringLits" `app` arg)
145 |
146 |     dfn : (impl : Name) -> Decl
147 |     dfn impl = def impl [patClause (var impl) `(MkHSL strings_)]
148 |
149 | errErr : Res a
150 | errErr = Left "HasError can only be derived for a record type with a field name `error_`"
151 |
152 | errType : ParamTypeInfo -> Res TTImp
153 | errType p =
154 |   case p.cons of
155 |     [c] => go (toList c.args)
156 |     _   => errErr
157 |   where
158 |     go : List (ConArg p.numParams) -> Res TTImp
159 |     go []      = errErr
160 |     go (ParamArg {}::as) = go as
161 |     go (CArg mnm rig pinfo x::as) =
162 |       case mnm == Just "error_" of
163 |         False => go as
164 |         True  => case x of
165 |           -- `Ref q (Maybe (BoundedErr e))`
166 |           (PApp refq (PApp m (PApp b z))) => Right (ttimp p.paramNames z)
167 |           _                               => errErr
168 |
169 | ||| Derives an implementation of `HasError` for a record type with the
170 | ||| following field:
171 | |||
172 | ||| ```idris
173 | ||| error_     : Ref q (Maybe $ BoundedErr e)
174 | ||| ```
175 | |||
176 | ||| The error type `e` can be freely chosen (it can also be a parameter) and
177 | ||| will be determined when deriving the implementation.
178 | export
179 | HasError : List Name -> ParamTypeInfo -> Res (List TopLevel)
180 | HasError nms p =
181 |  let impl := implName p "HasError"
182 |      Right c := clm impl | Left x => Left x
183 |   in Right [TL c (dfn impl)]
184 |   where
185 |     clm : (impl : Name) -> Res Decl
186 |     clm impl =
187 |      let arg      := unapply1 p.applied
188 |          Right te := errType p | Left x => Left x
189 |       in Right $ implClaimVis Export impl (ifaceType p $ appAll "HasError" [arg,te])
190 |
191 |     dfn : (impl : Name) -> Decl
192 |     dfn impl = def impl [patClause (var impl) `(MkHE error_)]
193 |
194 | ||| Derives an implementation of `HasBBEr` for a record type with the
195 | ||| following field:
196 | |||
197 | ||| ```idris
198 | ||| error_     : Ref q (Maybe $ BBErr e)
199 | ||| ```
200 | |||
201 | ||| The error type `e` can be freely chosen (it can also be a parameter) and
202 | ||| will be determined when deriving the implementation.
203 | export
204 | HasBBErr : List Name -> ParamTypeInfo -> Res (List TopLevel)
205 | HasBBErr nms p =
206 |  let impl := implName p "HasBBErr"
207 |      Right c := clm impl | Left x => Left x
208 |   in Right [TL c (dfn impl)]
209 |   where
210 |     clm : (impl : Name) -> Res Decl
211 |     clm impl =
212 |      let arg      := unapply1 p.applied
213 |          Right te := errType p | Left x => Left x
214 |       in Right $ implClaimVis Export impl (ifaceType p $ appAll "HasBBErr" [arg,te])
215 |
216 |     dfn : (impl : Name) -> Decl
217 |     dfn impl = def impl [patClause (var impl) `(MkBE error_)]
218 |
219 | stackErr : Res a
220 | stackErr = Left "HasStack can only be derived for a record type with a field name `stack_`"
221 |
222 | stackType : ParamTypeInfo -> Res TTImp
223 | stackType p =
224 |   case p.cons of
225 |     [c] => go (toList c.args)
226 |     _   => stackErr
227 |   where
228 |     go : List (ConArg p.numParams) -> Res TTImp
229 |     go []      = stackErr
230 |     go (ParamArg {}::as) = go as
231 |     go (CArg mnm rig pinfo x::as) =
232 |       case mnm == Just "stack_" of
233 |         False => go as
234 |         True  => case x of
235 |           -- `Ref q a`
236 |           (PApp refq z) => Right (ttimp p.paramNames z)
237 |           _             => stackErr
238 |
239 | ||| Derives an implementation of `HasStack` for a record type with the
240 | ||| following field:
241 | |||
242 | ||| ```idris
243 | ||| stack_     : Ref q a
244 | ||| ```
245 | |||
246 | ||| The stack type `a` can be freely chosen (it can also be a parameter) and
247 | ||| will be determined when deriving the implementation.
248 | export
249 | HasStack : List Name -> ParamTypeInfo -> Res (List TopLevel)
250 | HasStack nms p =
251 |  let impl := implName p "HasStack"
252 |      Right c := clm impl | Left x => Left x
253 |   in Right [TL c (dfn impl)]
254 |   where
255 |     clm : (impl : Name) -> Res Decl
256 |     clm impl =
257 |      let arg      := unapply1 p.applied
258 |          Right ts := stackType p | Left x => Left x
259 |       in Right $ implClaimVis Export impl (ifaceType p $ appAll "HasStack" [arg,ts])
260 |
261 |     dfn : (impl : Name) -> Decl
262 |     dfn impl = def impl [patClause (var impl) `(MkHS stack_)]
263 |
264 | ||| Derives implementations of the following interfaces for a suitable
265 | ||| record type: `HasBytePos`, `HasStringLits`, `HasBBErr`, and
266 | ||| `HasStack`.
267 | export
268 | FullStack : List Name -> ParamTypeInfo -> Res (List TopLevel)
269 | FullStack nms p =
270 |   sequenceJoin
271 |     [ HasBytes nms p
272 |     , HasStringLits nms p
273 |     , HasBBErr nms p
274 |     , HasStack nms p
275 |     ]
276 |