Deriving.Show


   0 | ||| Deriving show instances using reflection
   1 | ||| You can for instance define:
   2 | ||| ```
   3 | ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
   4 | ||| treeShow : Show a => Show (Tree a)
   5 | ||| treeShow = %runElab derive
   6 | ||| ```
   7 | 
   8 | module Deriving.Show
   9 | 
  10 | import public Control.Monad.Either
  11 | import public Control.Monad.State
  12 | import public Data.Maybe
  13 | import public Decidable.Equality
  14 | import public Language.Reflection
  15 | 
  16 | import public Deriving.Common
  17 | 
  18 | %language ElabReflection
  19 | %default total
  20 | 
  21 | public export
  22 | fromShowPrec :
  23 |   (Prec -> ty -> String) ->
  24 |   Show ty
  25 | fromShowPrec sp = MkShow (sp Open) sp
  26 | 
  27 | ------------------------------------------------------------------------------
  28 | -- Errors
  29 | 
  30 | ||| Possible errors for the functor-deriving machinery.
  31 | public export
  32 | data Error : Type where
  33 |   NotAShowable : Name -> Error
  34 |   UnsupportedType : TTImp -> Error
  35 |   NotAFiniteStructure : Error
  36 |   NotAnUnconstrainedValue : Count -> Error
  37 |   InvalidGoal : Error
  38 |   ConfusingReturnType : Error
  39 |   -- Contextual information
  40 |   WhenCheckingConstructor : Name -> Error -> Error
  41 |   WhenCheckingArg : TTImp -> Error -> Error
  42 | 
  43 | export
  44 | Show Error where
  45 |   show = joinBy "\n" . go [<] where
  46 | 
  47 |     go : SnocList String -> Error -> List String
  48 |     go acc (NotAShowable nm) = acc <>> ["Couldn't find a `Show' instance for the type \{show nm}"]
  49 |     go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
  50 |     go acc NotAFiniteStructure = acc <>> ["Cannot show an infinite structure"]
  51 |     go acc (NotAnUnconstrainedValue rig) = acc <>> ["Cannot show a \{enunciate rig} value"]
  52 |     go acc InvalidGoal = acc <>> ["Expected a goal of the form `Show t`"]
  53 |     go acc ConfusingReturnType = acc <>> ["Confusing telescope"]
  54 |     go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
  55 |     go acc (WhenCheckingArg s err) = go (acc :< "When checking argument of type \{show s}") err
  56 | 
  57 | record Parameters where
  58 |   constructor MkParameters
  59 |   asShowables : List Nat
  60 | 
  61 | initParameters : Parameters
  62 | initParameters = MkParameters []
  63 | 
  64 | paramConstraints : Parameters -> Nat -> Maybe TTImp
  65 | paramConstraints params pos
  66 |     = IVar emptyFC `{Prelude.Show.Show} <$ guard (pos `elem` params.asShowables)
  67 | 
  68 | ------------------------------------------------------------------------------
  69 | -- Core machinery: being showable
  70 | 
  71 | ShowN : TTImp -> Name -> TTImp
  72 | ShowN ty nm = go (IVar emptyFC nm) ty Z where
  73 | 
  74 |   go : TTImp -> TTImp -> Nat -> TTImp
  75 |   go acc (IPi _ _ pinfo mn (IType _) ty) n
  76 |     = let var = MN "__param" (cast n) in
  77 |       IPi emptyFC M0 ImplicitArg (Just var) (Implicit emptyFC False)
  78 |     $ IPi emptyFC MW AutoImplicit Nothing (IApp emptyFC `(Show) (IVar emptyFC var))
  79 |     $ go (TTImp.apply acc (toList (fromPiInfo emptyFC pinfo mn (IVar emptyFC var)))) ty (S n)
  80 |   go acc (IPi _ _ pinfo mn _ ty) n
  81 |     = let var = MN "__param" (cast n) in
  82 |       IPi emptyFC M0 ImplicitArg (Just var) (Implicit emptyFC False)
  83 |     $ go (TTImp.apply acc (toList (fromPiInfo emptyFC pinfo mn (IVar emptyFC var)))) ty (S n)
  84 |   go acc _ _ = IApp emptyFC `(Show) acc
  85 | 
  86 | ||| IsShowable is parametrised by
  87 | ||| @ t  the name of the data type whose constructors are being analysed
  88 | ||| @ ty the type being analysed
  89 | ||| The inductive type delivers a proof that ty can be shown,
  90 | ||| assuming that t also is showable.
  91 | public export
  92 | data IsShowable : (t : Name) -> (ty : TTImp) -> Type
  93 | data IsShowableArgs : (t : Name) -> (tconty : TTImp) -> (ty : List (Argument TTImp)) -> Type
  94 | 
  95 | data IsShowable : (t : Name) -> (ty : TTImp) -> Type where
  96 |   ||| The subterm is delayed (Lazy only, we can't traverse infinite structures)
  97 |   ISDelayed : IsShowable t ty -> IsShowable t (IDelayed fc LLazy ty)
  98 |   ||| There is a recursive subtree of type (t a1 ... an)
  99 |   ISRec : (0 _ : IsAppView (_, t) _ ty) -> IsShowable t ty
 100 |   ||| There are nested subtrees somewhere inside a 3rd party type constructor
 101 |   ||| which satisfies the Show interface
 102 |   ISShowN : (0 _ : IsAppView (_, tcon) args ty) ->
 103 |             HasType tcon tconty ->
 104 |             IsProvable (ShowN tconty tcon) ->
 105 |             IsShowableArgs t tconty (args <>> []) -> IsShowable t ty
 106 |   ||| Or we could be referring to one of the parameters
 107 |   ISParam : IsShowable t ty
 108 |   ||| A primitive type is trivially Showable
 109 |   ISPrim : (ty : PrimType) -> IsShowable t (IPrimVal fc (PrT ty))
 110 | 
 111 | data IsShowableArgs : (t : Name) -> (tconty : TTImp) -> (ty : List (Argument TTImp)) -> Type where
 112 |   Done : IsShowableArgs t tconty []
 113 |   Step :  IsShowable t (unArg arg) -> IsShowableArgs t ty args ->
 114 |          IsShowableArgs t (IPi fc1 r ExplicitArg mn (IType fc2) ty) (arg :: args)
 115 |   Drop : (forall fc. Not (dom === IType fc)) -> IsShowableArgs t ty args ->
 116 |          IsShowableArgs t (IPi fc1 r ExplicitArg mn dom ty) (arg :: args)
 117 |   Skip : Not (pinfo === ExplicitArg) -> IsShowableArgs t ty args ->
 118 |          IsShowableArgs t (IPi fc1 r pinfo mn dom ty) args -- TODO: constrain more?
 119 | 
 120 | parameters (fc : FC) (mutualWith : List Name)
 121 | 
 122 |   isRecs : IsShowableArgs t ty ts -> Bool
 123 |   isRec : IsShowable t ts -> Bool
 124 | 
 125 |   isRecs Done = False
 126 |   isRecs (Step x xs) = isRec x || isRecs xs
 127 |   isRecs (Drop f xs) = isRecs xs
 128 |   isRecs (Skip f xs) = isRecs xs
 129 | 
 130 |   isRec (ISDelayed x) = isRec x
 131 |   isRec (ISRec _) = True
 132 |   isRec (ISShowN _ _ _ xs) = isRecs xs
 133 |   isRec ISParam = False
 134 |   isRec (ISPrim _) = False
 135 | 
 136 |   showPrecFun : {ty : _} -> IsShowable t ty -> TTImp -> TTImp
 137 |   showPrecFun (ISDelayed p) t = showPrecFun p (IForce (getFC t) t)
 138 |   showPrecFun (ISRec _) t = IApp emptyFC `(assert_total) (IApp emptyFC `(showArg) t)
 139 |   showPrecFun {ty} (ISShowN _ _ _ as) t
 140 |     = let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
 141 |       ifThenElse (isMutual || isRecs as) (IApp emptyFC `(assert_total)) id
 142 |     $ IApp emptyFC `(showArg) t
 143 |   showPrecFun ISParam t = IApp emptyFC  `(showArg) t
 144 |   showPrecFun (ISPrim pty) t = IApp emptyFC  `(showArg) t
 145 | 
 146 | parameters
 147 |   {0 m : Type -> Type}
 148 |   {auto elab : Elaboration m}
 149 |   {auto error : MonadError Error m}
 150 |   {auto cs : MonadState Parameters m}
 151 |   (t : Name)
 152 |   (ps : List (Name, Nat))
 153 | 
 154 |   ||| Hoping to observe that ty can be shown
 155 |   export
 156 |   typeView : (ty : TTImp) -> m (IsShowable t ty)
 157 |   typeViews : (tconty : TTImp) -> (tys : List (Argument TTImp)) ->
 158 |               m (IsShowableArgs t tconty tys)
 159 | 
 160 |   typeView (IDelayed _ lz ty) = case lz of
 161 |     LLazy => ISDelayed <$> typeView ty
 162 |     _ => throwError NotAFiniteStructure
 163 |   typeView (IPrimVal _ (PrT ty)) = pure (ISPrim ty)
 164 |   typeView ty = do
 165 |     let Just (MkAppView (_, hd) ts prf) = appView ty
 166 |       | _ => throwError (UnsupportedType ty)
 167 |     let No _ = decEq hd t
 168 |       | Yes Refl => pure (ISRec prf)
 169 |     Just (hdty ** hT) <- hasType hd
 170 |       | _ => case lookup hd ps <* guard (null ts) of
 171 |                Just n => do
 172 |                  -- record that the nth parameter should be showable
 173 |                  ns <- gets asShowables
 174 |                  let ns = ifThenElse (n `elem` ns) ns (n :: ns)
 175 |                  modify { asShowables := ns }
 176 |                  -- and happily succeed
 177 |                  logMsg "derive.show.assumption" 10 $
 178 |                    "I am assuming that the parameter \{show hd} can be shown"
 179 |                  pure ISParam
 180 |                _ => throwError (UnsupportedType ty)
 181 |     Just iP <- isProvable (ShowN hdty hd)
 182 |       | _ => throwError (NotAShowable hd)
 183 |     ISShowN prf hT iP <$> typeViews hdty (ts <>> [])
 184 | 
 185 |   typeViews _ [] = pure Done
 186 |   typeViews (IPi _ _ ExplicitArg _ (IType fc) ty) (t :: ts)
 187 |     = Step <$> assert_total (typeView (unArg t)) <*> typeViews ty ts
 188 |   typeViews (IPi _ _ ExplicitArg _ dom ty) (t :: ts)
 189 |     = Drop (\ x => believe_me x) <$> typeViews ty ts
 190 |   typeViews (IPi _ _ _ _ _ ty) ts
 191 |     = Skip (\ x => believe_me x) <$> typeViews ty ts
 192 |   typeViews ty ts = throwError (UnsupportedType ty)
 193 | 
 194 | namespace Show
 195 | 
 196 |   derive' : (Elaboration m, MonadError Error m) =>
 197 |             {default Private vis : Visibility} ->
 198 |             {default Total treq : TotalReq} ->
 199 |             {default [] mutualWith : List Name} ->
 200 |             m (Show f)
 201 |   derive' = do
 202 | 
 203 |     -- expand the mutualwith names to have the internal, fully qualified, names
 204 |     mutualWith <- map concat $ for mutualWith $ \ nm => do
 205 |                     ntys <- getType nm
 206 |                     pure (fst <$> ntys)
 207 | 
 208 |     -- The goal should have the shape (Show t)
 209 |     Just (IApp _ (IVar _ showable) t) <- goal
 210 |       | _ => throwError InvalidGoal
 211 |     when (`{Prelude.Show.Show} /= showable) $
 212 |       logMsg "derive.show" 1 "Expected to derive Show but got \{show showable}"
 213 | 
 214 |     -- t should be a type constructor
 215 |     logMsg "derive.show" 1 "Deriving Show for \{showPrec App $ mapTTImp cleanup t}"
 216 |     MkIsType f params cs <- isType t
 217 |     logMsg "derive.show.constructors" 1 $
 218 |       joinBy "\n" $ "" :: map (\ (n, ty) => "  \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
 219 | 
 220 |     -- Generate a clause for each data constructor
 221 |     let fc = emptyFC
 222 |     let un = UN . Basic
 223 |     let showName = un ("showPrec" ++ show (dropNS f))
 224 |     let precName = un "d"
 225 |     let prec = IVar fc precName
 226 |     (ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
 227 |       withError (WhenCheckingConstructor cName) $ do
 228 |         -- Grab the types of the constructor's explicit arguments
 229 |         let Just (MkConstructorView paraz args) = constructorView ty
 230 |               | _ => throwError ConfusingReturnType
 231 |         logMsg "derive.show.clauses" 10 $
 232 |           "\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
 233 |         -- Only keep the visible arguments
 234 |         let args = mapMaybe (bitraverse pure (map snd . isExplicit)) args
 235 |         -- Special case for constructors with no argument
 236 |         let (_ :: _) = args
 237 |           | [] => pure $ PatClause fc
 238 |                     (apply fc (IVar fc showName) [ prec, IVar fc cName])
 239 |                     (IPrimVal fc (Str (showPrefix True (dropNS cName))))
 240 | 
 241 |         let vars = zipWith (const . IVar fc . un . ("x" ++) . show . (`minus` 1)) [1..length args] args
 242 |         recs <- for (zip vars args) $ \ (v, (rig, ty)) => do
 243 | 
 244 |                   let MW = rig
 245 |                     | _ => throwError (NotAnUnconstrainedValue rig)
 246 | 
 247 |                   -- try to reduce the type before analysis
 248 |                   ty <- try (check {expected=Type} ty >>= \x => quote x) (pure ty)
 249 |                   res <- withError (WhenCheckingArg (mapTTImp cleanup ty)) $ do
 250 |                            typeView f (paraz <>> []) ty
 251 |                   pure $ Just (showPrecFun fc mutualWith res v)
 252 | 
 253 |         let args = catMaybes recs
 254 |         let asList = foldr (\ a, as => apply fc (IVar fc `{Prelude.(::)}) [a,as]) `(Prelude.Nil)
 255 |         pure $ PatClause fc
 256 |           (apply fc (IVar fc showName) [ prec, apply fc (IVar fc cName) vars])
 257 |           (apply fc (IVar fc (un "showCon"))
 258 |             [ prec
 259 |             , IPrimVal fc (Str (showPrefix True (dropNS cName)))
 260 |             , case args of
 261 |                 [a] => a
 262 |                 _ => IApp fc (IVar fc (un "concat")) (asList args)
 263 |             ])
 264 | 
 265 |     -- Generate the type of the show function
 266 |     let ty = MkTy fc (NoFC showName) $ withParams fc (paramConstraints ns) params
 267 |            $ `(Prec -> ~(t) -> String)
 268 |     logMsg "derive.show.clauses" 1 $
 269 |       joinBy "\n" ("" :: ("  " ++ show (mapITy cleanup ty))
 270 |                       :: map (("  " ++) . showClause InDecl . mapClause cleanup) cls)
 271 | 
 272 |     -- Define the instance
 273 |     check $ ILocal fc
 274 |       [ IClaim (MkFCVal fc (MkIClaimData MW vis [Totality treq] ty))
 275 |       , IDef fc showName cls
 276 |       ] `(fromShowPrec ~(IVar fc showName))
 277 | 
 278 |   ||| Derive an implementation of Show for a type constructor.
 279 |   ||| This can be used like so:
 280 |   ||| ```
 281 |   ||| data Tree a = Leaf a | Node (Tree a) (Tree a)
 282 |   ||| treeShow : Show a => Show (Tree a)
 283 |   ||| treeShow = %runElab derive
 284 |   ||| ```
 285 |   export
 286 |   derive : {default Private vis : Visibility} ->
 287 |            {default Total treq : TotalReq} ->
 288 |            {default [] mutualWith : List Name} ->
 289 |            Elab (Show f)
 290 |   derive = do
 291 |     res <- runEitherT {e = Error, m = Elab} (derive' {vis, treq, mutualWith})
 292 |     case res of
 293 |       Left err => fail (show err)
 294 |       Right prf => pure prf
 295 |