0 | module Derive.DistributiveB
 1 |
 2 | import Language.Reflection.Util
 3 | import Derive.BarbieInfo
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------------------------------------
 8 | --          Claims
 9 | --------------------------------------------------------------------------------
10 |
11 | bdistTpe : (k : TTImp) -> TTImp -> TTImp
12 | bdistTpe k arg =
13 |   `(
14 |        {0 f : Type -> Type}
15 |     -> {0 g : ~(k) -> Type}
16 |     -> Functor f
17 |     => f (~(arg) g)
18 |     -> ~(arg) (f . g)
19 |   )
20 |
21 | export
22 | bdistClaim : Visibility -> (fun : Name) -> (p : BarbieInfo) -> Decl
23 | bdistClaim vis fun p =
24 |   simpleClaim vis fun $ piAll (bdistTpe p.kind p.applied) p.implicits
25 |
26 | ||| Top-level declaration implementing the `Eq` interface for
27 | ||| the given data type.
28 | export
29 | distImplClaim : Visibility -> (impl : Name) -> (p : BarbieInfo) -> Decl
30 | distImplClaim vis impl p =
31 |   let tpe := piAll `(DistributiveB ~(p.kind) ~(p.applied)) p.implicits
32 |    in implClaimVis vis impl tpe
33 |
34 | --------------------------------------------------------------------------------
35 | --          Definitions
36 | --------------------------------------------------------------------------------
37 |
38 | export
39 | distImplDef : (fun, impl : Name) -> Decl
40 | distImplDef fun impl =
41 |   def impl [patClause (var impl) `(MkDistributiveB ~(var fun))]
42 |
43 | rhs : Name -> SnocList TTImp -> TTImp
44 | rhs nm [<]       = var nm
45 | rhs nm (sx :< x) = rhs nm sx `app` x
46 |
47 | arg : BoundArg 0 RegularNamed -> TTImp
48 | arg (BA g [] _) = `(Prelude.map ~(var $ argName g) x_)
49 |
50 | export
51 | distClause : (fun : Name) -> Con n vs -> Clause
52 | distClause fun c = patClause `(~(var fun) x_) (injArgs regularNamed arg c)
53 |
54 | export
55 | distDef : Name -> Con n vs -> Decl
56 | distDef fun c = def fun [distClause fun c]
57 |
58 | --------------------------------------------------------------------------------
59 | --          Deriving
60 | --------------------------------------------------------------------------------
61 |
62 | ||| Generate declarations and implementations for `DistributiveB`
63 | ||| for a given data type.
64 | export
65 | DistributiveBVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
66 | DistributiveBVis vis nms p = case barbieArgs p.info.args of
67 |   Just prf => case p.info.cons of
68 |     [c] =>
69 |       let ndist := funName p "bdist"
70 |           impl  := implName p "DistributiveB"
71 |           bti   := BI p prf
72 |        in Right
73 |             [ TL (bdistClaim vis ndist bti) (distDef ndist c)
74 |             , TL (distImplClaim vis impl bti) (distImplDef ndist impl)
75 |             ]
76 |     _ => failRecord "DistributiveB"
77 |   Nothing => Left $ "Not a barbie type"
78 |
79 | ||| Alias for `DistributiveBVis Public`
80 | export %inline
81 | DistributiveB : List Name -> ParamTypeInfo -> Res (List TopLevel)
82 | DistributiveB = DistributiveBVis Public
83 |