0 | module Derive.Show
  1 |
  2 | import Language.Reflection.Util
  3 |
  4 | %default total
  5 |
  6 | --------------------------------------------------------------------------------
  7 | --          Utilities
  8 | --------------------------------------------------------------------------------
  9 |
 10 | public export
 11 | conWithArgs : Prec -> String -> List String -> String
 12 | conWithArgs p str [] = str
 13 | conWithArgs p str ss = showCon p str $ concat ss
 14 |
 15 | public export
 16 | recordWithArgs : Prec -> String -> List (String,String) -> String
 17 | recordWithArgs p str [] = str
 18 | recordWithArgs p str ss =
 19 |   let args := concat $ intersperse ", " $ map (\(n,v) => "\{n} = \{v}") ss
 20 |    in showCon p str $ " {\{args}}"
 21 |
 22 | --------------------------------------------------------------------------------
 23 | --          Named Constructors
 24 | --------------------------------------------------------------------------------
 25 |
 26 | ||| Checks, if the given argument is properly named.
 27 | public export
 28 | namedArg : (a : Arg) -> Bool
 29 | namedArg (MkArg _ ExplicitArg (Just $ UN _) _) = True
 30 | namedArg (MkArg _ ExplicitArg _ _)             = False
 31 | namedArg (MkArg _ ImplicitArg _ _)             = True
 32 | namedArg (MkArg _ AutoImplicit _ _)            = True
 33 | namedArg (MkArg _ (DefImplicit _) _ _)         = True
 34 |
 35 | --------------------------------------------------------------------------------
 36 | --          Claims
 37 | --------------------------------------------------------------------------------
 38 |
 39 | ||| General type of a `showPrec` function with the given list
 40 | ||| of implicit and auto-implicit arguments, plus the given argument type
 41 | ||| to be displayed.
 42 | export
 43 | generalShowType : (implicits : List Arg) -> (arg : TTImp) -> TTImp
 44 | generalShowType is arg = piAll `(Prec -> ~(arg) -> String) is
 45 |
 46 | ||| Top-level function declaration implementing the `showPrec` function for
 47 | ||| the given data type.
 48 | export
 49 | showClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
 50 | showClaim vis fun p =
 51 |   simpleClaim vis fun (generalShowType (allImplicits p "Show") p.applied)
 52 |
 53 | ||| Top-level declaration of the `Show` implementation for the given data type.
 54 | export
 55 | showImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
 56 | showImplClaim v impl p = implClaimVis v impl (implType "Show" p)
 57 |
 58 | --------------------------------------------------------------------------------
 59 | --          Definitions
 60 | --------------------------------------------------------------------------------
 61 |
 62 | ||| Top-level definition of the `Show` implementation for the given data type.
 63 | export
 64 | showImplDef : (fun, impl : Name) -> Decl
 65 | showImplDef f i = def i [patClause (var i) (var "mkShowPrec" `app` var f)]
 66 |
 67 | pvar : TTImp
 68 | pvar = var "p"
 69 |
 70 | parameters (nms : List Name)
 71 |   -- showing a single, explicit, unnamed constructor argument
 72 |   arg : BoundArg 1 Explicit -> TTImp
 73 |   arg (BA (MkArg M0 _ _ _) _   _) = primVal (Str " _")
 74 |   arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(showArg ~(var x))
 75 |
 76 |   -- showing a constructor plus its arguments
 77 |   rhs : Name -> SnocList TTImp -> TTImp
 78 |   rhs n [<] = n.namePrim
 79 |   rhs n st  = `(conWithArgs p ~(n.namePrim) ~(listOf st))
 80 |
 81 |   -- showing a single, explicit, named constructor argument
 82 |   narg : BoundArg 1 NamedExplicit -> TTImp
 83 |   narg (BA a [x]   _) =
 84 |     let nm := (argName a).namePrim
 85 |      in case a.count of
 86 |        M0 => `(MkPair ~(nm) "_")
 87 |        _  =>
 88 |          let shown := assertIfRec nms a.type `(show ~(var x))
 89 |           in `(MkPair ~(nm) ~(shown))
 90 |
 91 |   -- showing a constructor plus its named arguments
 92 |   nrhs : Name -> SnocList TTImp -> TTImp
 93 |   nrhs n [<] = n.namePrim
 94 |   nrhs n st  = `(recordWithArgs p ~(n.namePrim) ~(listOf st))
 95 |
 96 |   export
 97 |   showClauses : (fun : Maybe Name) -> TypeInfo -> List Clause
 98 |   showClauses fun ti = map clause ti.cons
 99 |
100 |     where
101 |       lhs : TTImp -> TTImp
102 |       lhs bc = maybe bc (\x => `(~(var x) ~(pvar) ~(bc))) fun
103 |
104 |       clause : Con ti.arty ti.args -> Clause
105 |       clause c = case all namedArg c.args of
106 |         True  => accumArgs namedExplicit lhs (nrhs c.name) narg c
107 |         False => accumArgs explicit lhs (rhs c.name) arg c
108 |
109 |   export
110 |   showDef : Name -> TypeInfo -> Decl
111 |   showDef fun ti = def fun (showClauses (Just fun) ti)
112 |
113 | --------------------------------------------------------------------------------
114 | --          Deriving
115 | --------------------------------------------------------------------------------
116 |
117 | ||| Derive an implementation of `Show a` for a custom data type `a`.
118 | |||
119 | ||| Note: This is mainly to be used for indexed data types. Consider using
120 | |||       `derive` together with `Derive.Show.Show` for parameterized data types.
121 | export %macro
122 | deriveShow : Elab (Show f)
123 | deriveShow = do
124 |   Just tpe <- goal
125 |     | Nothing => fail "Can't infer goal"
126 |   let Just (resTpe, nm) := extractResult tpe
127 |     | Nothing => fail "Invalid goal type: \{show tpe}"
128 |   ti <- getInfo' nm
129 |
130 |   let impl :=
131 |            lam (lambdaArg {a = Name} "p") $
132 |            lam (lambdaArg {a = Name} "x") $
133 |            iCase `(x) implicitFalse (showClauses [ti.name] Nothing ti)
134 |
135 |   logMsg "derive.definitions" 1 $ show impl
136 |   check $ var "mkShowPrec" `app` impl
137 |
138 | ||| Generate declarations and implementations for `Show` for a given data type.
139 | export
140 | ShowVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
141 | ShowVis vis nms p =
142 |   let fun  := funName p "showPrec"
143 |       impl := implName p "Show"
144 |    in Right
145 |         [ TL (showClaim vis fun p) (showDef nms fun p.info)
146 |         , TL (showImplClaim vis impl p) (showImplDef fun impl)
147 |         ]
148 |
149 | ||| Alias for `ShowVis Public`
150 | export %inline
151 | Show : List Name -> ParamTypeInfo -> Res (List TopLevel)
152 | Show = ShowVis Public
153 |