0 | ||| Utilities for Language.Reflection.Refined
 1 | module Language.Reflection.Refined.Util
 2 |
 3 | import public Data.Maybe
 4 | import public Data.So
 5 |
 6 | %default total
 7 |
 8 | --------------------------------------------------------------------------------
 9 | --          Utilities
10 | --------------------------------------------------------------------------------
11 |
12 | ||| Try and convert a boolean to `So`, that is, a proof that the
13 | ||| boolean in question equals `True`.
14 | public export
15 | maybeSo : (b : Bool) -> Maybe (So b)
16 | maybeSo True  = Just Oh
17 | maybeSo False = Nothing
18 |
19 | ||| Try to create a refined value that requires an erased proof of `So (f v)`.
20 | public export
21 | refineSo :
22 |      {f : a -> Bool}
23 |   -> (make : (v : a) -> (0 prf : So $ f v) -> b)
24 |   -> (val : a)
25 |   -> Maybe b
26 | refineSo make val = case maybeSo (f val) of
27 |   Just oh => Just $ make val oh
28 |   Nothing => Nothing
29 |