0 | module Text.Show.PrettyVal.Derive
  1 |
  2 | import System.Clock
  3 | import System.File
  4 | import Text.Lex
  5 | import Text.Parse
  6 | import Text.Show.PrettyVal
  7 | import Text.Show.Value
  8 | import public Derive.Show
  9 | import Derive.Prelude
 10 |
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Utilities
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| Displays an applied constructer in record syntax.
 18 | ||| This is called, if all arguments have user-defined names.
 19 | ||| Note: If the list of arguments is empty, this uses the
 20 | |||       `Con` data constructor in agreement with `parseValue`.
 21 | public export
 22 | rec : String -> List (Value,String) -> Value
 23 | rec con [] = Con (MkName con) []
 24 | rec con ps = Rec (MkName con) $ map (\(v,n) => (MkName n, v)) ps
 25 |
 26 |   where
 27 |     named : Value -> String -> (VName,Value)
 28 |     named v name = (MkName name, v)
 29 |
 30 | -- Displays an applied constructer with unnamed arguments.
 31 | public export
 32 | other : String -> List Value -> Value
 33 | other con = Con (MkName con)
 34 |
 35 | --------------------------------------------------------------------------------
 36 | --          Claims
 37 | --------------------------------------------------------------------------------
 38 |
 39 | ||| General type of a `prettyVal` function with the given list
 40 | ||| of implicit and auto-implicit arguments, plus the given argument type
 41 | ||| to be displayed.
 42 | export
 43 | generalPrettyValType : (implicits : List Arg) -> (arg : TTImp) -> TTImp
 44 | generalPrettyValType is arg = piAll `(~(arg) -> Value) is
 45 |
 46 | ||| Top-level function declaration implementing the `prettyVal` function for
 47 | ||| the given data type.
 48 | export
 49 | prettyValClaim : (fun : Name) -> (p : ParamTypeInfo) -> Decl
 50 | prettyValClaim fun p =
 51 |   let tpe := generalPrettyValType (allImplicits p "PrettyVal") p.applied
 52 |    in public' fun tpe
 53 |
 54 | ||| Top-level declaration of the `PrettyVal` implementation for the given data type.
 55 | export
 56 | prettyValImplClaim : (impl : Name) -> (p : ParamTypeInfo) -> Decl
 57 | prettyValImplClaim impl p = implClaim impl (implType "PrettyVal" p)
 58 |
 59 | --------------------------------------------------------------------------------
 60 | --          Definitions
 61 | --------------------------------------------------------------------------------
 62 |
 63 | ||| Top-level definition of the `PrettyVal` implementation for the given data type.
 64 | export
 65 | prettyValImplDef : (fun, impl : Name) -> Decl
 66 | prettyValImplDef f i = def i [patClause (var i) (var "MkPrettyVal" `app` var f)]
 67 |
 68 | parameters (nms : List Name)
 69 |   arg : BoundArg 1 Explicit -> TTImp
 70 |   arg (BA (MkArg M0 _ _ _) _   _) = `(Chr "_")
 71 |   arg (BA (MkArg _  _ _ t) [x] _) = assertIfRec nms t `(prettyVal ~(var x))
 72 |
 73 |   rhs : Name -> SnocList TTImp -> TTImp
 74 |   rhs n st = `(other ~(n.namePrim) ~(listOf st))
 75 |
 76 |   narg : BoundArg 1 NamedExplicit -> TTImp
 77 |   narg (BA a [x]   _) =
 78 |     let nm := (argName a).namePrim
 79 |      in case a.count of
 80 |        M0 => `(MkPair ~(nm) (Chr "_"))
 81 |        _  =>
 82 |          let pv := assertIfRec nms a.type `(prettyVal ~(var x))
 83 |           in `(MkPair ~(pv) ~(nm))
 84 |
 85 |   nrhs : Name -> SnocList TTImp -> TTImp
 86 |   nrhs n st  = `(rec ~(n.namePrim) ~(listOf st))
 87 |
 88 |   export
 89 |   pvClauses : (fun : Maybe Name) -> TypeInfo -> List Clause
 90 |   pvClauses fun ti = map clause ti.cons
 91 |
 92 |     where
 93 |       lhs : TTImp -> TTImp
 94 |       lhs bc = maybe bc ((`app` bc) . var) fun
 95 |
 96 |       clause : Con ti.arty ti.args -> Clause
 97 |       clause c = case all namedArg c.args of
 98 |         True  => accumArgs namedExplicit lhs (nrhs c.name) narg c
 99 |         False => accumArgs explicit lhs (rhs c.name) arg c
100 |
101 |   export
102 |   prettyValDef : Name -> TypeInfo -> Decl
103 |   prettyValDef fun ti = def fun (pvClauses (Just fun) ti)
104 |
105 | --------------------------------------------------------------------------------
106 | --          Deriving
107 | --------------------------------------------------------------------------------
108 |
109 | ||| Derive an implementation of `PrettyVal a` for a custom data type `a`.
110 | |||
111 | ||| Note: This is mainly to be used for indexed data types. Consider using
112 | |||       `derive` together with `Derive.PrettyVal.PrettyVal` for parameterized data types.
113 | export %macro
114 | derivePrettyVal : Elab (PrettyVal f)
115 | derivePrettyVal = do
116 |   Just tpe <- goal
117 |     | Nothing => fail "Can't infer goal"
118 |   let Just (resTpe, nm) := extractResult tpe
119 |     | Nothing => fail "Invalid goal type: \{show tpe}"
120 |   ti <- getInfo' nm
121 |
122 |   let impl := lam (lambdaArg {a = Name} "x") $
123 |               iCase `(x) implicitFalse (pvClauses [ti.name] Nothing ti)
124 |
125 |   logMsg "derive.definitions" 1 $ show impl
126 |   check $ var "MkPrettyVal" `app` impl
127 |
128 | ||| Generate declarations and implementations for `PrettyVal` for a given data type.
129 | export
130 | PrettyVal : List Name -> ParamTypeInfo -> Res (List TopLevel)
131 | PrettyVal nms p =
132 |   let fun  := funName p "prettyVal"
133 |       impl := implName p "PrettyVal"
134 |    in Right [ TL (prettyValClaim fun p) (prettyValDef nms fun p.info)
135 |             , TL (prettyValImplClaim impl p) (prettyValImplDef fun impl)
136 |             ]
137 |
138 | %runElab derive "Bool" [PrettyVal]
139 |
140 | %runElab derive "Ordering" [PrettyVal]
141 |
142 | %runElab derive "Maybe" [PrettyVal]
143 |
144 | %runElab derive "Either" [PrettyVal]
145 |
146 | %runElab derive "List1" [PrettyVal]
147 |
148 | %runElab derive "Prec" [PrettyVal]
149 |
150 | -- Pretty
151 |
152 | %runElab derive "VName" [PrettyVal]
153 |
154 | %runElab derive "Value" [PrettyVal]
155 |
156 | %runElab derive "Text.Show.Value.Token" [PrettyVal]
157 |
158 | %runElab derive "Text.Show.Value.Err" [PrettyVal]
159 |
160 | %runElab derive "Text.Bounds.Position" [PrettyVal]
161 |
162 | %runElab derive "Text.Bounds.Bounds" [PrettyVal]
163 |
164 | %runElab derive "Text.Bounds.Bounded" [PrettyVal]
165 |
166 | %runElab derive "Text.ParseError.DigitType" [PrettyVal]
167 |
168 | %runElab derive "Text.ParseError.CharClass" [PrettyVal]
169 |
170 | %runElab derive "Text.FC.Origin" [PrettyVal]
171 |
172 | %runElab derive "Text.FC.FileContext" [PrettyVal]
173 |
174 | %runElab derive "Text.ParseError.InnerError" [PrettyVal]
175 |
176 | %runElab derive "Text.ParseError.ParseError" [PrettyVal]
177 |
178 | -- System
179 |
180 | %runElab derive "System.File.Mode.Mode" [PrettyVal]
181 |
182 | %runElab derive "FileError" [PrettyVal]
183 |
184 | %runElab derive "FileMode" [PrettyVal]
185 |
186 | %runElab derive "Permissions" [PrettyVal]
187 |
188 | %runElab derive "ClockType" [PrettyVal]
189 |
190 | -- Reflection
191 |
192 | %runElab derive "ModuleIdent" [PrettyVal]
193 |
194 | %runElab derive "VirtualIdent" [PrettyVal]
195 |
196 | %runElab derive "OriginDesc" [PrettyVal]
197 |
198 | %runElab derive "Language.Reflection.TT.FC" [PrettyVal]
199 |
200 | %runElab derive "WithFC" [PrettyVal]
201 |
202 | %runElab derive "NameType" [PrettyVal]
203 |
204 | %runElab derive "PrimType" [PrettyVal]
205 |
206 | %runElab derive "Constant" [PrettyVal]
207 |
208 | %runElab derive "Namespace" [PrettyVal]
209 |
210 | %runElab derive "UserName" [PrettyVal]
211 |
212 | %runElab derive "Language.Reflection.TT.Name" [PrettyVal]
213 |
214 | %runElab derive "Count" [PrettyVal]
215 |
216 | %runElab derive "PiInfo" [PrettyVal]
217 |
218 | %runElab derive "LazyReason" [PrettyVal]
219 |
220 | %runElab derive "TotalReq" [PrettyVal]
221 |
222 | %runElab derive "Visibility" [PrettyVal]
223 |
224 | %runElab derive "WithDefault" [PrettyVal]
225 |
226 | %runElab derive "BindMode" [PrettyVal]
227 |
228 | %runElab derive "UseSide" [PrettyVal]
229 |
230 | %runElab derive "DotReason" [PrettyVal]
231 |
232 | %runElab derive "DataOpt" [PrettyVal]
233 |
234 | %runElab derive "WithFlag" [PrettyVal]
235 |
236 | %runElab derive "BuiltinType" [PrettyVal]
237 |
238 | %runElab deriveMutual
239 |   [ "TTImp"
240 |   , "IField"
241 |   , "IFieldUpdate"
242 |   , "AltType"
243 |   , "FnOpt"
244 |   , "ITy"
245 |   , "Data"
246 |   , "Record"
247 |   , "Clause"
248 |   , "Decl"
249 |   , "IClaimData"
250 |   ] [PrettyVal]
251 |