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