0 | module Derive.FunctorB
 1 |
 2 | import Language.Reflection.Util
 3 | import Derive.BarbieInfo
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------------------------------------
 8 | --          Claims
 9 | --------------------------------------------------------------------------------
10 |
11 | bmapTpe : (k : TTImp) -> TTImp -> TTImp
12 | bmapTpe k arg =
13 |   `(
14 |        {0 f,g : ~(k) -> Type}
15 |     -> ((0 a : ~(k)) -> f a -> g a)
16 |     -> ~(arg) f
17 |     -> ~(arg) g
18 |   )
19 |
20 | export
21 | bmapClaim : Visibility -> (fun : Name) -> (p : BarbieInfo) -> Decl
22 | bmapClaim vis fun p =
23 |   simpleClaim vis fun $ piAll (bmapTpe p.kind p.applied) p.implicits
24 |
25 | ||| Top-level declaration implementing the `Eq` interface for
26 | ||| the given data type.
27 | export
28 | functorImplClaim : Visibility -> (impl : Name) -> (p : BarbieInfo) -> Decl
29 | functorImplClaim vis impl p =
30 |   let tpe := piAll `(FunctorB ~(p.kind) ~(p.applied)) p.implicits
31 |    in implClaimVis vis impl tpe
32 |
33 | --------------------------------------------------------------------------------
34 | --          Definitions
35 | --------------------------------------------------------------------------------
36 |
37 | export
38 | functorImplDef : (fun, impl : Name) -> Decl
39 | functorImplDef fun impl =
40 |   def impl [patClause (var impl) (var "MkFunctorB" `app` var fun)]
41 |
42 | parameters (farg : Name)
43 |
44 |   arg : BoundArg 1 Regular -> TTImp
45 |   arg (BA g [x] _) =
46 |     if hasFArg farg g.type then `(fun _ ~(var x)) else var x
47 |
48 |   export
49 |   functorClauses : (fun : Name) -> TypeInfo -> List Clause
50 |   functorClauses fun ti = map clause ti.cons
51 |    where
52 |      clause : Con ti.arty ti.args -> Clause
53 |      clause = mapArgs regular (\x => `(~(var fun) fun ~(x))) arg
54 |
55 |   export
56 |   functorDef : Name -> TypeInfo -> Decl
57 |   functorDef fun ti = def fun (functorClauses fun ti)
58 |
59 | --------------------------------------------------------------------------------
60 | --          Deriving
61 | --------------------------------------------------------------------------------
62 |
63 | ||| Generate declarations and implementations for `FunctorB`
64 | ||| for a given data type.
65 | export
66 | FunctorBVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
67 | FunctorBVis vis nms p = case barbieArgs p.info.args of
68 |   Just prf =>
69 |     let fun  := funName p "bmap"
70 |         impl := implName p "FunctorB"
71 |         farg := barbieArg prf
72 |         bti  := BI p prf
73 |      in Right
74 |           [ TL (bmapClaim vis fun bti) (functorDef (barbieArg prf) fun p.info)
75 |           , TL (functorImplClaim vis impl bti) (functorImplDef fun impl)
76 |           ]
77 |   Nothing => Left $ "Not a barbie type"
78 |
79 | ||| Alias for `FunctorBVis Public`
80 | export %inline
81 | FunctorB : List Name -> ParamTypeInfo -> Res (List TopLevel)
82 | FunctorB = FunctorBVis Public
83 |