b7cf1ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix delab of scoped implicits

We shouldn't display implicit arguments as explicit arguments, so we need to keep track of the current environment to know what the implicit arguments are to locally defined names.

commitb7cf1ec0f4a2ca455c8cc32769c3607641be88fd authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 13 Mar 2017, 22:49 (10 years ago) parent3dc90d3

8 files changed+126−93

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+5 src/Idris/Core/Elaborate.hs+1−3 src/Idris/Delaborate.hs+101−76 src/Idris/Elab/Clause.hs−3 src/Idris/Elab/Interface.hs+1−1 src/Idris/Elab/Term.hs+3−1 src/Idris/Elab/Utils.hs+5−2 src/Idris/REPL.hs+10−7

src/Idris/AbsSyntaxTree.hs+5

@@ -1871,12 +1871,17 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18711871 depth d . bracket p startPrec $

18721872 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>

18731873 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1874+ | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc

18741875 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc

18751876 where

18761877 showRig Rig0 n = text "0" <+> prettyBindingOf n True

18771878 showRig Rig1 n = text "1" <+> prettyBindingOf n True

18781879 showRig _ n = prettyBindingOf n True

18791880

1881+ isPi (PPi (Exp{}) _ _ _ _) = True

1882+ isPi (PPi _ _ _ _ sc) = isPi sc

1883+ isPi _ = False

1884+

18801885 st =

18811886 case s of

18821887 Static -> text "%static" <> space

src/Idris/Core/Elaborate.hs+1−3

@@ -611,9 +611,7 @@ prepare_apply fn imps =

611611 mkClaims _ _ _ _

612612 | Var n <- fn

613613 = do ctxt <- get_context

614− case lookupTy n ctxt of

615− [] -> lift $ tfail $ NoSuchVariable n

616− _ -> lift $ tfail $ TooManyArguments n

614+ lift $ tfail $ TooManyArguments n

617615 | otherwise = fail $ "Too many arguments for " ++ show fn

618616

619617 doClaim ((i, _), n, t) = do claim n t

src/Idris/Delaborate.hs+101−76

@@ -8,7 +8,7 @@ Maintainer : The Idris Community.

88{-# LANGUAGE PatternGuards #-}

99{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

1010module Idris.Delaborate (

11− annName, bugaddr, delab, delabDirect, delab', delabMV, delabSugared

11+ annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared

1212 , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab

1313 , pprintDelabTy, pprintErr, resugar

1414 ) where

@@ -82,6 +82,9 @@ delabSugared ist tm = resugar ist $ delab ist tm

8282delab :: IState -> Term -> PTerm

8383delab i tm = delab' i tm False False

8484

85+delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm

86+delabWithEnv i tys tm = delabWithEnv' i tys tm False False

87+

8588delabMV :: IState -> Term -> PTerm

8689delabMV i tm = delab' i tm False True

8790

@@ -89,26 +92,31 @@ delabMV i tm = delab' i tm False True

8992-- We need this for interactive case splitting, where we need access to the

9093-- underlying function in a delaborated form, to generate the right patterns

9194delabDirect :: IState -> Term -> PTerm

92−delabDirect i tm = delabTy' i [] tm False False False

95+delabDirect i tm = delabTy' i [] [] tm False False False

9396

9497delabTy :: IState -> Name -> PTerm

9598delabTy i n

9699 = case lookupTy n (tt_ctxt i) of

97100 (ty:_) -> case lookupCtxt n (idris_implicits i) of

98− (imps:_) -> delabTy' i imps ty False False True

99− _ -> delabTy' i [] ty False False True

101+ (imps:_) -> delabTy' i imps [] ty False False True

102+ _ -> delabTy' i [] [] ty False False True

100103 [] -> error "delabTy: got non-existing name"

101104

102105delab' :: IState -> Term -> Bool -> Bool -> PTerm

103−delab' i t f mvs = delabTy' i [] t f mvs True

106+delab' i t f mvs = delabTy' i [] [] t f mvs True

107+

108+delabWithEnv' :: IState -> [(Name, Type)] -> Term -> Bool -> Bool -> PTerm

109+delabWithEnv' i tys t f mvs = delabTy' i [] tys t f mvs True

104110

105111delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

112+ -> [(Name, Type)] -- ^ Names and types in environment

113+ -- (for properly hiding scoped implicits)

106114 -> Term

107115 -> Bool -- ^ use full names

108116 -> Bool -- ^ Don't treat metavariables specially

109117 -> Bool -- ^ resugar cases

110118 -> PTerm

111−delabTy' ist imps tm fullname mvs docases = de [] imps tm

119+delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

112120 where

113121 un = fileFC "(val)"

114122

@@ -118,64 +126,71 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

118126 -- the last argument,

119127 -- although that's not always the thing that gets pattern matched

120128 -- in the elaborated block)

121− de env imps sc

129+ de tys env imps sc

122130 | docases

123131 , isCaseApp sc

124132 , (P _ cOp _, args@(_:_)) <- unApply sc

125− , Just caseblock <- delabCase env imps (last args) cOp args

133+ , Just caseblock <- delabCase tys env imps (last args) cOp args

126134 = caseblock

127135

128− de env _ (App _ f a) = deFn env f [a]

129− de env _ (V i) | i < length env = PRef un [] (snd (env!!i))

136+ de tys env _ (App _ f a) = deFn tys env f [a]

137+ de tys env _ (V i) | i < length env = PRef un [] (snd (env!!i))

130138 | otherwise = PRef un [] (sUN ("v" ++ show i ++ ""))

131− de env _ (P _ n _) | n == unitTy = PTrue un IsType

132− | n == unitCon = PTrue un IsTerm

133− | Just n' <- lookup n env = PRef un [] n'

134− | otherwise

135− = case lookup n (idris_metavars ist) of

136− Just (Just _, mi, _, _, _) -> mkMVApp n []

137− _ -> PRef un [] n

138− de env _ (Bind n (Lam _ ty) sc)

139− = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

140− de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

139+ de tys env _ (P _ n _) | n == unitTy = PTrue un IsType

140+ | n == unitCon = PTrue un IsTerm

141+ | Just n' <- lookup n env = PRef un [] n'

142+ | otherwise

143+ = case lookup n (idris_metavars ist) of

144+ Just (Just _, mi, _, _, _) -> mkMVApp n []

145+ _ -> PRef un [] n

146+ de tys env _ (Bind n (Lam _ ty) sc)

147+ = PLam un n NoFC (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) [] sc)

148+ de tys env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

141149 | toplevel_imp impl -- information in 'imps' repeated

142− = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

143− de env is (Bind n (Pi rig (Just impl) ty _) sc)

150+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC

151+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

152+ de tys env is (Bind n (Pi rig (Just impl) ty _) sc)

144153 | tcimplementation impl

145− = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

154+ = PPi constraint n NoFC (de tys env [] ty)

155+ (de ((n, ty) : tys) ((n,n):env) is sc)

146156 | otherwise

147− = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

148− de env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)

149− = PPi (Imp opts Dynamic False Nothing False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

150− de env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)

151− = PPi (constraint { pcount = rig}) n NoFC (de env [] ty) (de ((n,n):env) is sc)

152− de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)

153− = PPi ((tacimpl tac) { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) is sc)

154− de env (plic:is) (Bind n (Pi rig _ ty _) sc)

157+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de tys env [] ty) (de tys ((n,n):env) is sc)

158+ de tys env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)

159+ = PPi (Imp opts Dynamic False Nothing False rig) n NoFC

160+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

161+ de tys env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)

162+ = PPi (constraint { pcount = rig}) n NoFC

163+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

164+ de tys env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)

165+ = PPi ((tacimpl tac) { pcount = rig }) n NoFC

166+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

167+ de tys env (plic:is) (Bind n (Pi rig _ ty _) sc)

155168 = PPi (Exp (argopts plic) Dynamic False rig)

156169 n NoFC

157− (de env [] ty)

158− (de ((n,n):env) is sc)

159− de env [] (Bind n (Pi rig _ ty _) sc)

160− = PPi (expl { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) [] sc)

170+ (de tys env [] ty)

171+ (de ((n, ty) : tys) ((n,n):env) is sc)

172+ de tys env [] (Bind n (Pi rig _ ty _) sc)

173+ = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)

174+ (de ((n, ty) : tys) ((n,n):env) [] sc)

161175

162− de env imps (Bind n (Let ty val) sc)

176+ de tys env imps (Bind n (Let ty val) sc)

163177 | docases

164178 , isCaseApp sc

165179 , (P _ cOp _, args) <- unApply sc

166− , Just caseblock <- delabCase env imps val cOp args = caseblock

180+ , Just caseblock <- delabCase tys env imps val cOp args = caseblock

167181 | otherwise =

168− PLet un n NoFC (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

169− de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

170− de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

171− de env plic (Bind n bb sc) = de ((n,n):env) [] sc

172− de env _ (Constant i) = PConstant NoFC i

173− de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

174− de env _ Erased = Placeholder

175− de env _ Impossible = Placeholder

176− de env _ (Inferred t) = Placeholder

177− de env _ (TType i) = PType un

178− de env _ (UType u) = PUniverse un u

182+ PLet un n NoFC (de tys env [] ty)

183+ (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)

184+ de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

185+ de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

186+ de tys env plic (Bind n bb sc) = de ((n, binderTy bb) : tys) ((n,n):env) [] sc

187+ de tys env _ (Constant i) = PConstant NoFC i

188+ de tys env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

189+ de tys env _ Erased = Placeholder

190+ de tys env _ Impossible = Placeholder

191+ de tys env _ (Inferred t) = Placeholder

192+ de tys env _ (TType i) = PType un

193+ de tys env _ (UType u) = PUniverse un u

179194

180195 dens x | fullname = x

181196 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

@@ -184,38 +199,48 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

184199 _ -> ns

185200 dens n = n

186201

187− deFn env (App _ f a) args = deFn env f (a:args)

188− deFn env (P _ n _) [l,r]

189− | n == pairTy = PPair un [] IsType (de env [] l) (de env [] r)

190− | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

191− deFn env (P _ n _) [ty, Bind x (Lam _ _) r]

202+ deFn tys env (App _ f a) args = deFn tys env f (a:args)

203+ deFn tys env (P _ n _) [l,r]

204+ | n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)

205+ deFn tys env (P _ n _) [ty, Bind x (Lam _ _) r]

192206 | n == sigmaTy

193− = PDPair un [] IsType (PRef un [] x) (de env [] ty)

194− (de ((x,x):env) [] (instantiate (P Bound x ty) r))

195− deFn env (P _ n _) [lt,rt,l,r]

196− | n == pairCon = PPair un [] IsTerm (de env [] l) (de env [] r)

197− | n == sigmaCon = PDPair un [] IsTerm (de env [] l) Placeholder

198− (de env [] r)

199− deFn env f@(P _ n _) args

200− | n `elem` map snd env

201− = PApp un (de env [] f) (map pexp (map (de env []) args))

202− deFn env (P _ n _) args

207+ = PDPair un [] IsType (PRef un [] x) (de tys env [] ty)

208+ (de tys ((x,x):env) [] (instantiate (P Bound x ty) r))

209+ deFn tys env (P _ n _) [lt,rt,l,r]

210+ | n == pairCon = PPair un [] IsTerm (de tys env [] l) (de tys env [] r)

211+ | n == sigmaCon = PDPair un [] IsTerm (de tys env [] l) Placeholder

212+ (de tys env [] r)

213+-- deFn tys env f@(P _ n _) args

214+-- | n `elem` map snd env

215+-- = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))

216+ deFn tys env (P _ n _) args

203217 | not mvs = case lookup n (idris_metavars ist) of

204218 Just (Just _, mi, _, _, _) ->

205− mkMVApp n (drop mi (map (de env []) args))

206− _ -> mkPApp n (map (de env []) args)

207− | otherwise = mkPApp n (map (de env []) args)

208− deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

219+ mkMVApp n (drop mi (map (de tys env []) args))

220+ _ -> mkPApp tys n (map (de tys env []) args)

221+ | otherwise = mkPApp tys n (map (de tys env []) args)

222+ deFn tys env (V i) args

223+ | i < length env = mkPApp tys (fst (env!!i)) (map (de tys env []) args)

224+ deFn tys env f args = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))

209225

210226 mkMVApp n []

211227 = PMetavar NoFC n

212228 mkMVApp n args

213229 = PApp un (PMetavar NoFC n) (map pexp args)

214− mkPApp n args

230+

231+ mkPApp tys n args

232+ | Just ty <- lookup n tys

233+ = let imps = findImp ty in

234+ PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

215235 | Just imps <- lookupCtxtExact n (idris_implicits ist)

216236 = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

217237 | otherwise = PApp un (PRef un [] n) (map pexp args)

218−

238+ where

239+ findImp (Bind n (Pi _ im@(Just i) _ _) sc)

240+ = pimp n Placeholder True : findImp sc

241+ findImp (Bind n (Pi _ _ _ _) sc)

242+ = pexp Placeholder : findImp sc

243+ findImp _ = []

219244 imp (PImp p m l n _) arg = PImp p m l n arg

220245 imp (PExp p l n _) arg = PExp p l n arg

221246 imp (PConstraint p l n _) arg = PConstraint p l n arg

@@ -227,14 +252,14 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

227252 isCN (SN (CaseN _ _)) = True

228253 isCN _ = False

229254

230− delabCase :: [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm

231− delabCase env imps scrutinee caseName caseArgs =

255+ delabCase :: [(Name, Type)] -> [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm

256+ delabCase tys env imps scrutinee caseName caseArgs =

232257 do cases <- case lookupCtxt caseName (idris_patdefs ist) of

233258 [(cases, _)] -> return cases

234259 _ -> Nothing

235− return $ PCase un (de env imps scrutinee)

236− [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),

237− de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)

260+ return $ PCase un (de tys env imps scrutinee)

261+ [ (de tys (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),

262+ de tys (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)

238263 | (vars, lhs, rhs) <- cases

239264 ]

240265 where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)

@@ -268,8 +293,8 @@ pprintDelabTy i n

268293 = case lookupTy n (tt_ctxt i) of

269294 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $

270295 case lookupCtxt n (idris_implicits i) of

271− (imps:_) -> resugar i $ delabTy' i imps ty False False True

272− _ -> resugar i $ delabTy' i [] ty False False True

296+ (imps:_) -> resugar i $ delabTy' i imps [] ty False False True

297+ _ -> resugar i $ delabTy' i [] [] ty False False True

273298 [] -> error "pprintDelabTy got a name that doesn't exist"

274299

275300pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

src/Idris/Elab/Clause.hs−3

@@ -753,9 +753,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

753753

754754 -- These are the names we're not allowed to use on the RHS, because

755755 -- they're UniqueTypes and borrowed from another function.

756− -- FIXME: There is surely a nicer way than this...

757− -- Issue #1615 on the Issue Tracker.

758− -- https://github.com/idris-lang/Idris-dev/issues/1615

759756 when (not (null borrowed)) $

760757 logElab 5 ("Borrowed names on LHS: " ++ show borrowed)

761758

src/Idris/Elab/Interface.hs+1−1

@@ -212,7 +212,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

212212 Just i -> i

213213 Nothing -> []

214214 case lookupTyExact n (tt_ctxt ist) of

215− Just ty -> return (delabTy' ist impls ty False False False)

215+ Just ty -> return (delabTy' ist impls [] ty False False False)

216216 Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))

217217

218218 -- Find the argument position of the current interface in a method type

src/Idris/Elab/Term.hs+3−1

@@ -2659,8 +2659,10 @@ runTac autoSolve ist perhapsFC fn tac

26592659 letbind scriptvar scriptTy (Var script)

26602660 focus script

26612661 ptm <- get_term

2662+ env <- get_env

2663+ let denv = map (\(n, _, b) -> (n, binderTy b)) env

26622664 elab ist toplevel ERHS [] (sMN 0 "tac")

2663− (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True True)])

2665+ (PApp emptyFC tm [pexp (delabTy' ist [] denv tgoal True True True)])

26642666 (script', _) <- get_type_val (Var scriptvar)

26652667 -- now that we have the script apply

26662668 -- it to the reflected goal

src/Idris/Elab/Utils.hs+5−2

@@ -209,8 +209,11 @@ getPBtys _ = []

209209psolve (Bind n (PVar _ t) sc) = do solve; psolve sc

210210psolve tm = return ()

211211

212−pvars ist (Bind n (PVar _ t) sc) = (n, delab ist t) : pvars ist sc

213−pvars ist _ = []

212+pvars ist tm = pv' [] tm

213+ where

214+ pv' env (Bind n (PVar _ t) sc)

215+ = (n, delabWithEnv ist env t) : pv' ((n, t) : env) sc

216+ pv' env _ = []

214217

215218getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ _ t _) sc)

216219 = nub $ getFixedInType i env [] t ++

src/Idris/REPL.hs+10−7

@@ -93,6 +93,8 @@ import Util.Pretty hiding ((</>))

9393import Util.System

9494import Version_idris (gitHash)

9595

96+import Debug.Trace

97+

9698-- | Run the REPL

9799repl :: IState -- ^ The initial state

98100 -> [FilePath] -- ^ The loaded modules

@@ -422,9 +424,9 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

422424 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

423425 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

424426 let (hs, c, pc) = splitPi ist (i - 1) rest in

425− ((n, t, delabTy' ist [] t False False True):hs,

426− c, delabTy' ist [] c False False True)

427− splitPi ist i tm = ([], tm, delabTy' ist [] tm False False True)

427+ ((n, t, delabTy' ist [] [] t False False True):hs,

428+ c, delabTy' ist [] [] c False False True)

429+ splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

428430

429431 -- | Get the types of a list of metavariable names

430432 mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]

@@ -1511,15 +1513,16 @@ pprintDef asCore n =

15111513 ppDef amb ist (n, (clauses, missing)) =

15121514 prettyName True amb [] n <+> colon <+>

15131515 align (pprintDelabTy ist n) <$>

1514− ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing

1516+ ppClauses ist clauses <> ppMissing missing

15151517 ppClauses ist [] = text "No clauses."

15161518 ppClauses ist cs = vsep (map pp cs)

1517− where pp (vars, lhs, rhs) =

1518− let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .

1519+ where pp (varTys, lhs, rhs) =

1520+ let vars = map fst varTys

1521+ ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .

15191522 pprintPTerm (ppOptionIst ist)

15201523 (zip vars (repeat False))

15211524 [] (idris_infixes ist) .

1522− delab ist $

1525+ delabWithEnv ist varTys $

15231526 t

15241527 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)

15251528 ppMissing _ = empty