0 | ||| This module derives functionality for refinement type. In general,
  1 | ||| a refinement type is of the following shape:
  2 | |||
  3 | ||| ```idris
  4 | ||| record Percent where
  5 | |||   constructor MkPercent
  6 | |||   value : Double
  7 | |||   0 prf : IsPercent value
  8 | ||| ```
  9 | |||
 10 | ||| That is, a value paired with a predicate on that value. The
 11 | ||| predicate can be an explicit or implicit argument of any
 12 | ||| quantity.
 13 | module Derive.Refined
 14 |
 15 | import public Data.Refined
 16 | import Language.Reflection.Util
 17 |
 18 | %default total
 19 |
 20 | --------------------------------------------------------------------------------
 21 | --          View
 22 | --------------------------------------------------------------------------------
 23 |
 24 | ||| Proof that a constructor argument `arg` is a dependent type
 25 | ||| on a second argument of name `name`, that is, `arg` is
 26 | ||| of type `p nm` for some predicate `p`.
 27 | public export
 28 | data AppVar : (arg : PArg n) -> (nm : Name) -> Type where
 29 |   HereApp :
 30 |        {0 n1, n2   : Name}
 31 |     -> {0 p        : PArg n}
 32 |     -> (0 prf : (n1 == n2) === True)
 33 |     -> AppVar (PApp p (PVar n2)) n1
 34 |
 35 |   HereNamedApp :
 36 |        {0 n1, n2, n3 : Name}
 37 |     -> {0 p          : PArg n}
 38 |     -> (0 prf : (n1 == n2) === True)
 39 |     -> AppVar (PNamedApp p n3 (PVar n2)) n1
 40 |
 41 |   ThereApp :
 42 |        {0 n1    : Name}
 43 |     -> {0 p, p2 : PArg n}
 44 |     -> AppVar p n1
 45 |     -> AppVar (PApp p p2) n1
 46 |
 47 |   ThereNamedApp :
 48 |        {0 n1,n2 : Name}
 49 |     -> {0 p, p2 : PArg n}
 50 |     -> AppVar p n1
 51 |     -> AppVar (PNamedApp p n2 p2) n1
 52 |
 53 | ||| Tests if `arg` is a dependent type on a value with name `nm`.
 54 | public export
 55 | appVar : (nm : Name) -> (arg : PArg n) -> Maybe (AppVar arg nm)
 56 | appVar nm (PApp p (PVar n2)) with (nm == n2) proof eq
 57 |   _ | True  = Just (HereApp eq)
 58 |   _ | False = case appVar nm p of
 59 |     Just prf => Just (ThereApp prf)
 60 |     Nothing  => Nothing
 61 | appVar nm (PApp p q) = case appVar nm p of
 62 |     Just prf => Just (ThereApp prf)
 63 |     Nothing  => Nothing
 64 | appVar nm (PNamedApp p _ (PVar n2)) with (nm == n2) proof eq
 65 |   _ | True  = Just (HereNamedApp eq)
 66 |   _ | False = case appVar nm p of
 67 |     Just prf => Just (ThereNamedApp prf)
 68 |     Nothing  => Nothing
 69 | appVar nm (PNamedApp p _ q) = case appVar nm p of
 70 |     Just prf => Just (ThereNamedApp prf)
 71 |     Nothing  => Nothing
 72 | appVar n1 _                          = Nothing
 73 |
 74 | ||| A proof (value of a predicate) in a refined type must be
 75 | ||| an explicit or auto-implicit argument of that type.
 76 | public export
 77 | data ProofInfo : PiInfo TTImp -> Type where
 78 |   PIAuto     : ProofInfo AutoImplicit
 79 |   PIExplicit : ProofInfo ExplicitArg
 80 |
 81 | ||| Tests if `pi` is explicit or auto-implicit
 82 | public export
 83 | proofInfo : (pi : PiInfo TTImp) -> Maybe (ProofInfo pi)
 84 | proofInfo ExplicitArg  = Just PIExplicit
 85 | proofInfo AutoImplicit = Just PIAuto
 86 | proofInfo _            = Nothing
 87 |
 88 | ||| Proof that the argument list of a data constructor
 89 | ||| consists of erased implicits followed by a single
 90 | ||| explicit value, followed by an explicit or auto-implicit
 91 | ||| predicate on the value.
 92 | public export
 93 | data RefinedArgs : (args : Vect m (ConArg n)) -> Type where
 94 |   RArgs :
 95 |        {0 nm    : Name}
 96 |     -> {0 t1,t2 : PArg n}
 97 |     -> {0 mn    : Maybe Name}
 98 |     -> {0 c     : Count}
 99 |     -> {0 pi    : PiInfo TTImp}
100 |     -> ProofInfo pi
101 |     -> AppVar t2 nm
102 |     -> RefinedArgs [CArg (Just nm) MW ExplicitArg t1 , CArg mn c pi t2]
103 |
104 |   RImplicit :
105 |        {0 as : _}
106 |     -> {0 t  : TTImp}
107 |     -> {0 ix : Fin n}
108 |     -> RefinedArgs as
109 |     -> RefinedArgs (ParamArg ix t :: as)
110 |
111 | ||| Tests if the arguments of a data constructor are valid
112 | ||| arguments of a refined type.
113 | public export
114 | refinedArgs : (as : Vect m (ConArg n)) -> Maybe (RefinedArgs as)
115 | refinedArgs [CArg (Just n1) MW ExplicitArg _, CArg _ M0 pi t] =
116 |   [| RArgs (proofInfo pi) (appVar n1 t) |]
117 | refinedArgs (ParamArg ix t :: as) = RImplicit <$> refinedArgs as
118 | refinedArgs _ = Nothing
119 |
120 | --------------------------------------------------------------------------------
121 | --          fromInteger
122 | --------------------------------------------------------------------------------
123 |
124 | ||| Extracts the predicate from the constructor of a refined type.
125 | export
126 | proofType :
127 |      Vect n Name
128 |   -> (as : Vect m (ConArg n))
129 |   -> RefinedArgs as
130 |   -> TTImp
131 | proofType ns (_ :: as) (RImplicit x)        = proofType ns as x
132 | proofType ns [_, CArg _ _ _ t2] (RArgs x y) = `(\x => ~(fromApp t2 y))
133 |
134 |   where
135 |     fromApp : (t : PArg n) -> AppVar t nm -> TTImp
136 |     fromApp (PApp p _)         (HereApp _)       = `(~(ttimp ns p) x)
137 |     fromApp (PApp p t)         (ThereApp q)      = app (fromApp p q) (ttimp ns t)
138 |     fromApp (PNamedApp p nm _) (HereNamedApp _)  = namedApp (ttimp ns p) nm (varStr "x")
139 |     fromApp (PNamedApp p nm t) (ThereNamedApp q) = namedApp (fromApp p q) nm (ttimp ns t)
140 |
141 | ||| Extracts the predicate from the constructor of a refined type.
142 | export
143 | isErased :
144 |      (as : Vect m (ConArg n))
145 |   -> RefinedArgs as
146 |   -> Bool
147 | isErased (_ :: as) (RImplicit x)        = isErased as x
148 | isErased [_, CArg _ M0 _ _] (RArgs x y) = True
149 | isErased [_, CArg _ _ _ _]  (RArgs x y) = False
150 |
151 | ||| Extracts the value type from the constructor of a refined type.
152 | export
153 | valType :
154 |      Vect n Name
155 |   -> (as : Vect m (ConArg n))
156 |   -> RefinedArgs as
157 |   -> TTImp
158 | valType ns [CArg _ _ _ t, _] (RArgs x y)   = ttimp ns t
159 | valType ns (_ :: as)         (RImplicit x) = valType ns as x
160 |
161 | ||| Extracts the field name from the constructor of a refined type
162 | export
163 | valName : (as : Vect m (ConArg n)) -> RefinedArgs as -> Name
164 | valName [CArg (Just nm) _ _ t, _] (RArgs x y)   = nm
165 | valName (_ :: as)                 (RImplicit x) = valName as x
166 |
167 | ||| Applies the data constructor of a refinement type to a
168 | ||| refined value. We assume that a proof of validity of
169 | ||| the correct count is already in scope.
170 | |||
171 | ||| In case of an explicit proof argument, we pass the argument
172 | ||| by invoking `%search`, in case of an auto-implicit proof argument,
173 | ||| proof search will do this for us automatically.
174 | export
175 | appCon : TTImp -> (c : ParamCon n) -> RefinedArgs c.args -> TTImp
176 | appCon t (MkParamCon cn _ as) x = fromArgs (var cn `app` t) as x
177 |
178 |   where
179 |     fromArgs : TTImp -> (as : Vect k (ConArg n)) -> RefinedArgs as -> TTImp
180 |     fromArgs s [_, CArg mn c ExplicitArg _]  (RArgs x y)  = `(~(s) prf)
181 |     fromArgs s [_, CArg mn c _ _]            (RArgs x y)  = `(~(s) @{prf})
182 |     fromArgs s (ParamArg _ _ :: as)          (RImplicit x) = fromArgs s as x
183 |
184 | ||| Proof that a data type is a refinement type: A data type with a single
185 | ||| data constructor taking an arbitrary number or erased implicit arguments,
186 | ||| a single explicit value argument of quantity "any" and an explict or
187 | ||| auto-implicit predicate on the value.
188 | public export
189 | data RefinedInfo : ParamTypeInfo -> Type where
190 |   RI :
191 |        {0 c : ParamCon n}
192 |     -> RefinedArgs c.args
193 |     -> RefinedInfo (MkParamTypeInfo ti p ns [c] s)
194 |
195 | export
196 | refinedInfo : (p : ParamTypeInfo) -> Res (RefinedInfo p)
197 | refinedInfo (MkParamTypeInfo t _ _ [c] _) = case refinedArgs c.args of
198 |   Just x  => Right (RI x)
199 |   Nothing => Left "\{t.name} is not a refinement type with an explicit or auto-implicit proof"
200 | refinedInfo p = Left "\{p.getName} is not a single-constructor data type"
201 |
202 | ||| Function for refining a value at runtime. This returns a `Maybe` of
203 | ||| the refinement type.
204 | export
205 | refineClaim : (fun : Name) -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl
206 | refineClaim fun (MkParamTypeInfo ti p ns [c] s) (RI x) =
207 |   let res  := `(Maybe ~(ti.applied))
208 |       vtpe := valType ns c.args x
209 |       tpe  := piAll `(~(vtpe) -> ~(res)) ti.implicits
210 |    in public' fun tpe
211 |
212 | export
213 | refineDef : (fun : Name) -> (p : ParamTypeInfo) -> RefinedInfo p -> Decl
214 | refineDef fun (MkParamTypeInfo ti p ns [c] s) (RI x) =
215 |   let prf  := proofType ns c.args x
216 |       v    := varStr "v"
217 |       lhs  := var fun `app` v
218 |       rhs0 := `(case hdec0 {p = ~(proofType ns c.args x)} ~(v) of
219 |                      Just0 prf => Just $ ~(appCon v c x)
220 |                      Nothing0  => Nothing)
221 |       rhs  := `(case hdec {p = ~(proofType ns c.args x)} ~(v) of
222 |                      Just prf  => Just $ ~(appCon v c x)
223 |                      Nothing  => Nothing)
224 |    in def fun [patClause lhs (if isErased c.args x then rhs0 else rhs)]
225 |
226 | export
227 | refineTL : (fun : Name) -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel
228 | refineTL fun p x = TL (refineClaim fun p x) (refineDef fun p x)
229 |
230 | litTL :
231 |      Visibility
232 |   -> (fun,constraint : Name)
233 |   -> (tpe : TTImp)
234 |   -> (p : ParamTypeInfo)
235 |   -> RefinedInfo p
236 |   -> TopLevel
237 | litTL vis fun con tpe (MkParamTypeInfo ti q ns [c] s) (RI x) =
238 |   let p    := MkParamTypeInfo ti q ns [c] s
239 |       arg  := p.applied
240 |       vfun := var fun
241 |       res  := appCon (var fun `app` varStr "n") c x
242 |    in case isErased c.args x of
243 |         False =>
244 |           let test := `(hdec {p = ~(proofType ns c.args x)} (~(vfun) n))
245 |               pi   := `((n : ~(tpe)) -> {auto 0 _ : IsJust ~(test)} -> ~(arg))
246 |               tpe  := piAll pi (allImplicits p con)
247 |               rhs  := `(let prf := fromJust ~(test) in ~(res))
248 |               df   := def fun [ patClause `(~(var fun) n) rhs ]
249 |            in TL (simpleClaim vis fun tpe) df
250 |         True =>
251 |           let test := `(hdec0 {p = ~(proofType ns c.args x)} (~(vfun) n))
252 |               pi   := `((n : ~(tpe)) -> {auto 0 _ : IsJust0 ~(test)} -> ~(arg))
253 |               tpe  := piAll pi (allImplicits p con)
254 |               rhs  := `(let 0 prf := fromJust0 ~(test) in ~(res))
255 |               df   := def fun [ patClause `(~(var fun) n) rhs ]
256 |            in TL (simpleClaim vis fun tpe) df
257 |
258 | export
259 | fromIntTL : Visibility -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel
260 | fromIntTL vis = litTL vis "fromInteger" "Num" `(Integer)
261 |
262 | export
263 | fromDblTL : Visibility -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel
264 | fromDblTL vis = litTL vis "fromDouble" "FromDouble" `(Double)
265 |
266 | export
267 | fromStrTL : Visibility -> (p : ParamTypeInfo) -> RefinedInfo p -> TopLevel
268 | fromStrTL vis = litTL vis "fromString" "FromString" `(String)
269 |
270 | --------------------------------------------------------------------------------
271 | --          Derive
272 | --------------------------------------------------------------------------------
273 |
274 | export %inline
275 | refineName : Named a => a -> Name
276 | refineName v = funName v "refine"
277 |
278 | export %inline
279 | Refined : List Name -> ParamTypeInfo -> Res (List TopLevel)
280 | Refined nms p = map (pure . refineTL (refineName p) p) $ refinedInfo p
281 |
282 | export
283 | RefinedIntegerVis :
284 |      Visibility
285 |   -> List Name
286 |   -> ParamTypeInfo
287 |   -> Res (List TopLevel)
288 | RefinedIntegerVis vis nms p = map decls $ refinedInfo p
289 |   where
290 |     decls : RefinedInfo p -> List TopLevel
291 |     decls x =
292 |       let fun := refineName p.getName
293 |        in [ refineTL fun p x, fromIntTL vis p x ]
294 |
295 | export %inline
296 | RefinedInteger : List Name -> ParamTypeInfo -> Res (List TopLevel)
297 | RefinedInteger = RefinedIntegerVis Export
298 |
299 | export
300 | RefinedDoubleVis :
301 |      Visibility
302 |   -> List Name
303 |   -> ParamTypeInfo
304 |   -> Res (List TopLevel)
305 | RefinedDoubleVis vis nms p = map decls $ refinedInfo p
306 |   where
307 |     decls : RefinedInfo p -> List TopLevel
308 |     decls x =
309 |       let fun := refineName p
310 |        in [ refineTL fun p x, fromIntTL vis p x, fromDblTL vis p x ]
311 |
312 | export %inline
313 | RefinedDouble : List Name -> ParamTypeInfo -> Res (List TopLevel)
314 | RefinedDouble = RefinedDoubleVis Export
315 |
316 | export
317 | RefinedStringVis :
318 |      Visibility
319 |   -> List Name
320 |   -> ParamTypeInfo
321 |   -> Res (List TopLevel)
322 | RefinedStringVis vis nms p = map decls $ refinedInfo p
323 |   where
324 |     decls : RefinedInfo p -> List TopLevel
325 |     decls x =
326 |       let fun := refineName p
327 |        in [ refineTL fun p x, fromStrTL vis p x ]
328 |
329 | export %inline
330 | RefinedString : List Name -> ParamTypeInfo -> Res (List TopLevel)
331 | RefinedString = RefinedStringVis Export
332 |