0 | module Derive.ApplicativeB
  1 |
  2 | import Language.Reflection.Util
  3 | import Derive.BarbieInfo
  4 |
  5 | %default total
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --          Claims
  9 | --------------------------------------------------------------------------------
 10 |
 11 | bpureTpe : (k : TTImp) -> TTImp -> TTImp
 12 | bpureTpe k arg =
 13 |   `(
 14 |        {0 f : ~(k) -> Type}
 15 |     -> ((0 a : ~(k)) -> f a)
 16 |     -> ~(arg) f
 17 |   )
 18 |
 19 | bprodTpe : (k : TTImp) -> TTImp -> TTImp
 20 | bprodTpe k arg =
 21 |   `(
 22 |        {0 f,g : ~(k) -> Type}
 23 |     -> ~(arg) f
 24 |     -> ~(arg) g
 25 |     -> ~(arg) (\x => Pair (f x) (g x))
 26 |   )
 27 |
 28 | export
 29 | bpureClaim : Visibility -> (fun : Name) -> (p : BarbieInfo) -> Decl
 30 | bpureClaim vis fun p =
 31 |   simpleClaim vis fun $ piAll (bpureTpe p.kind p.applied) p.implicits
 32 |
 33 | export
 34 | bprodClaim : Visibility -> (fun : Name) -> (p : BarbieInfo) -> Decl
 35 | bprodClaim vis fun p =
 36 |   simpleClaim vis fun $ piAll (bprodTpe p.kind p.applied) p.implicits
 37 |
 38 | ||| Top-level declaration implementing the `Eq` interface for
 39 | ||| the given data type.
 40 | export
 41 | applicativeImplClaim : Visibility -> (impl : Name) -> (p : BarbieInfo) -> Decl
 42 | applicativeImplClaim vis impl p =
 43 |   let tpe := piAll `(ApplicativeB ~(p.kind) ~(p.applied)) p.implicits
 44 |    in implClaimVis vis impl tpe
 45 |
 46 | --------------------------------------------------------------------------------
 47 | --          Definitions
 48 | --------------------------------------------------------------------------------
 49 |
 50 | export
 51 | applicativeImplDef : (bpure, bprod, impl : Name) -> Decl
 52 | applicativeImplDef bpure bprod impl =
 53 |   def impl [patClause (var impl) `(MkApplicativeB ~(var bpure) ~(var bprod))]
 54 |
 55 | prodArg : BoundArg 2 Regular -> TTImp
 56 | prodArg (BA g [x,y] _) = `(MkPair ~(var x) ~(var y))
 57 |
 58 | export
 59 | prodClause : (fun : Name) -> Con n vs -> Clause
 60 | prodClause f =
 61 |   mapArgs2 regular (\x,y => `(~(var f) ~(x) ~(y))) prodArg
 62 |
 63 | export
 64 | prodDef : Name -> Con n vs -> Decl
 65 | prodDef fun c = def fun [prodClause fun c]
 66 |
 67 | export
 68 | pureDef : Name -> Con n vs -> Decl
 69 | pureDef f c =
 70 |   let rhs := injArgs explicit (const `(fun _)) c
 71 |    in def f [patClause `(~(var f) fun) rhs]
 72 |
 73 | --------------------------------------------------------------------------------
 74 | --          Deriving
 75 | --------------------------------------------------------------------------------
 76 |
 77 | ||| Generate declarations and implementations for `ApplicativeB`
 78 | ||| for a given data type.
 79 | export
 80 | ApplicativeBVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
 81 | ApplicativeBVis vis nms p = case barbieArgs p.info.args of
 82 |   Just prf => case p.info.cons of
 83 |     [c] =>
 84 |       let npure := funName p "bpure"
 85 |           nprod := funName p "bprod"
 86 |           impl  := implName p "ApplicativeB"
 87 |           bti   := BI p prf
 88 |        in Right
 89 |             [ TL (bpureClaim vis npure bti) (pureDef npure c)
 90 |             , TL (bprodClaim vis nprod bti) (prodDef nprod c)
 91 |             , TL (applicativeImplClaim vis impl bti)
 92 |                  (applicativeImplDef npure nprod impl)
 93 |             ]
 94 |     _ => failRecord "ApplicativeB"
 95 |   Nothing => Left $ "Not a barbie type"
 96 |
 97 | ||| Alias for `ApplicativeBVis Public`
 98 | export %inline
 99 | ApplicativeB : List Name -> ParamTypeInfo -> Res (List TopLevel)
100 | ApplicativeB = ApplicativeBVis Public
101 |