0 | module Derive.Pretty
  1 |
  2 | import public Text.PrettyPrint.Bernardy
  3 | import Language.Reflection.Util
  4 | import public Derive.Show
  5 |
  6 | %default total
  7 |
  8 | public export
  9 | data PlaceHolder = US
 10 |
 11 | public export
 12 | Pretty PlaceHolder where
 13 |   prettyPrec _ _ = symbol '_'
 14 |
 15 | --------------------------------------------------------------------------------
 16 | --          Claims
 17 | --------------------------------------------------------------------------------
 18 |
 19 | ||| General type of a `prettyPrec` function with the given list
 20 | ||| of implicit and auto-implicit arguments, plus the given argument type
 21 | ||| to be displayed.
 22 | export
 23 | generalPrettyType : (implicits : List Arg) -> (arg : TTImp) -> TTImp
 24 | generalPrettyType is arg =
 25 |   piAll `({opts : LayoutOpts} -> Prec -> ~(arg) -> Doc opts) is
 26 |
 27 | ||| Top-level function declaration implementing the `prettyPrec` function for
 28 | ||| the given data type.
 29 | export
 30 | prettyClaim : Visibility -> (fun : Name) -> (p : ParamTypeInfo) -> Decl
 31 | prettyClaim vis fun p =
 32 |   simpleClaim vis fun (generalPrettyType (allImplicits p "Pretty") p.applied)
 33 |
 34 | ||| Top-level declaration of the `Pretty` implementation for the given data type.
 35 | export
 36 | prettyImplClaim : Visibility -> (impl : Name) -> (p : ParamTypeInfo) -> Decl
 37 | prettyImplClaim v impl p = implClaimVis v impl (implType "Pretty" p)
 38 |
 39 | --------------------------------------------------------------------------------
 40 | --          Definitions
 41 | --------------------------------------------------------------------------------
 42 |
 43 | ||| Top-level definition of the `Pretty` implementation for the given data type.
 44 | export
 45 | prettyImplDef : (fun, impl : Name) -> Decl
 46 | prettyImplDef f i = def i [patClause (var i) (var "MkPretty" `app` var f)]
 47 |
 48 | pvar : TTImp
 49 | pvar = var "p"
 50 |
 51 | parameters (nms : List Name)
 52 |   -- pretty printing a single, explicit, unnamed constructor argument
 53 |   arg : BoundArg 1 Explicit -> TTImp
 54 |   arg (BA (MkArg M0 _ _ _) _   _) = `(pretty US)
 55 |   arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(prettyArg ~(var x))
 56 |
 57 |   -- prettying a constructor plus its arguments
 58 |   rhs : Name -> SnocList TTImp -> TTImp
 59 |   rhs n st  = `(prettyCon p ~(n.namePrim) ~(listOf st))
 60 |
 61 |   -- prettying a single, explicit, named constructor argument
 62 |   narg : BoundArg 1 NamedExplicit -> TTImp
 63 |   narg (BA a [x]   _) =
 64 |     let nm := (argName a).namePrim
 65 |      in case a.count of
 66 |        M0 => `(prettyField ~(nm) US)
 67 |        _  => assertIfRec nms a.type `(prettyField ~(nm) ~(var x))
 68 |
 69 |   -- prettying a constructor plus its named arguments
 70 |   nrhs : Name -> SnocList TTImp -> TTImp
 71 |   nrhs n st  = `(prettyRecord p ~(n.namePrim) ~(listOf st))
 72 |
 73 |   export
 74 |   prettyClauses : (fun : Maybe Name) -> TypeInfo -> List Clause
 75 |   prettyClauses fun ti = map clause ti.cons
 76 |
 77 |     where
 78 |       lhs : TTImp -> TTImp
 79 |       lhs bc = maybe bc (\x => `(~(var x) ~(pvar) ~(bc))) fun
 80 |
 81 |       clause : Con ti.arty ti.args -> Clause
 82 |       clause c = case all namedArg c.args of
 83 |         True  => accumArgs namedExplicit lhs (nrhs c.name) narg c
 84 |         False => accumArgs explicit lhs (rhs c.name) arg c
 85 |
 86 |   export
 87 |   prettyDef : Name -> TypeInfo -> Decl
 88 |   prettyDef fun ti = def fun (prettyClauses (Just fun) ti)
 89 |
 90 | --------------------------------------------------------------------------------
 91 | --          Deriving
 92 | --------------------------------------------------------------------------------
 93 |
 94 | ||| Derive an implementation of `Pretty a` for a custom data type `a`.
 95 | |||
 96 | ||| Note: This is mainly to be used for indexed data types. Consider using
 97 | |||       `derive` together with `Derive.Pretty.Pretty` for parameterized data types.
 98 | export %macro
 99 | derivePretty : Elab (Pretty f)
100 | derivePretty = do
101 |   Just tpe <- goal
102 |     | Nothing => fail "Can't infer goal"
103 |   let Just (resTpe, nm) := extractResult tpe
104 |     | Nothing => fail "Invalid goal type: \{show tpe}"
105 |   ti <- getInfo' nm
106 |
107 |   let impl :=
108 |         lam (lambdaArg {a = Name} "p") $
109 |         lam (lambdaArg {a = Name} "x") $
110 |         iCase `(x) implicitFalse (prettyClauses [ti.name] Nothing ti)
111 |
112 |   logTerm "derive.definitions" 1 "pretty implementation" impl
113 |   check $ var "MkPretty" `app` impl
114 |
115 | ||| Generate declarations and implementations for `Pretty` for a given data type.
116 | export
117 | PrettyVis : Visibility -> List Name -> ParamTypeInfo -> Res (List TopLevel)
118 | PrettyVis vis nms p =
119 |   let fun  := funName p "prettyPrec"
120 |       impl := implName p "Pretty"
121 |    in Right
122 |         [ TL (prettyClaim vis fun p) (prettyDef nms fun p.info)
123 |         , TL (prettyImplClaim vis impl p) (prettyImplDef fun impl)
124 |         ]
125 |
126 | ||| Alias for `PrettyVis Public`
127 | export %inline
128 | Pretty : List Name -> ParamTypeInfo -> Res (List TopLevel)
129 | Pretty = PrettyVis Public
130 |