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