0 | module Derive.Abs
 1 |
 2 | import Language.Reflection.Util
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Claims
 8 | --------------------------------------------------------------------------------
 9 |
10 | export
11 | absClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
12 | absClaim vis fun p =
13 |   let arg := p.applied
14 |       tpe := piAll `(~(arg) -> ~(arg)) (allImplicits p "Abs")
15 |    in simpleClaim vis fun tpe
16 |
17 | export
18 | absImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
19 | absImplClaim vis impl p = implClaimVis vis impl (implType "Abs" p)
20 |
21 | --------------------------------------------------------------------------------
22 | --          Definitions
23 | --------------------------------------------------------------------------------
24 |
25 | absImplDef : (abs, impl : Name) -> Decl
26 | absImplDef abs impl = def impl [patClause (var impl) (appNames "MkAbs" [abs])]
27 |
28 | parameters (nms : List Name)
29 |   abs : BoundArg 1 Explicit -> TTImp
30 |   abs (BA _ [x] _)  = `(abs ~(var x))
31 |
32 |   export
33 |   absDef : Name -> Con n vs -> Decl
34 |   absDef fun c = def fun [mapArgs explicit (var fun `app`) abs c]
35 |
36 | --------------------------------------------------------------------------------
37 | --          Deriving
38 | --------------------------------------------------------------------------------
39 |
40 | ||| Generate declarations and implementations for `Abs` for a
41 | ||| single-constructor data type with the given visibility.
42 | export
43 | AbsVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
44 | AbsVis vis nms p = case p.info.cons of
45 |   [c] =>
46 |     let abs  := funName p "abs"
47 |         impl := implName p "Abs"
48 |      in Right
49 |           [ TL (absClaim vis abs p) (absDef nms abs c)
50 |           , TL (absImplClaim vis impl p) (absImplDef abs impl)
51 |           ]
52 |   _   => failRecord "Abs"
53 |
54 | ||| Generate declarations and implementations for `Abs` for a
55 | ||| single-constructor data type with `public export` visibility.
56 | export %inline
57 | Abs : List Name -> ParamTypeInfo -> Res (List TopLevel)
58 | Abs = AbsVis Public
59 |