From b8f115f6fcbf58e512830f3980d696ce25148a03 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Tue, 16 Jan 2024 18:11:10 +0300 Subject: [PATCH 1/4] [ refactor ] Make `hasNamesInsideDeep` pure, precompute needed info --- src/Deriving/DepTyCheck/Gen/Checked.idr | 4 +- src/Deriving/DepTyCheck/Gen/Core.idr | 3 +- .../DepTyCheck/Gen/Core/ConsDerive.idr | 4 +- src/Deriving/DepTyCheck/Gen/Derive.idr | 2 +- src/Deriving/DepTyCheck/Gen/Entry.idr | 1 + src/Deriving/DepTyCheck/Util/Reflection.idr | 119 +++++------------- 6 files changed, 42 insertions(+), 91 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Checked.idr b/src/Deriving/DepTyCheck/Gen/Checked.idr index 63f17c0f..b9dbf2c1 100644 --- a/src/Deriving/DepTyCheck/Gen/Checked.idr +++ b/src/Deriving/DepTyCheck/Gen/Checked.idr @@ -110,7 +110,7 @@ namespace ClojuringCanonicImpl Yes prf => Just $ Element extSig prf No _ => Nothing - DerivatorCore => ClojuringContext m => Elaboration m => CanonicGen m where + DerivatorCore => ClojuringContext m => Elaboration m => NamesInfoInTypes => CanonicGen m where callGen sig fuel values = do -- check if we are the first, then we need to start the loop @@ -172,7 +172,7 @@ namespace ClojuringCanonicImpl --- Canonic-dischagring function --- export - runCanonic : DerivatorCore => SortedMap ExternalGenSignature Name -> (forall m. CanonicGen m => m a) -> Elab (a, List Decl) + runCanonic : DerivatorCore => NamesInfoInTypes => SortedMap ExternalGenSignature Name -> (forall m. CanonicGen m => m a) -> Elab (a, List Decl) runCanonic exts calc = do let exts = SortedMap.fromList $ exts.asList <&> \namedSig => (fst $ internalise $ fst namedSig, namedSig) (x, defs, bodies) <- evalRWST exts (empty, empty, True) calc {s=(SortedMap GenSignature Name, List (GenSignature, Name), _)} {w=(_, _)} diff --git a/src/Deriving/DepTyCheck/Gen/Core.idr b/src/Deriving/DepTyCheck/Gen/Core.idr index 77a526fb..ed4e50d4 100644 --- a/src/Deriving/DepTyCheck/Gen/Core.idr +++ b/src/Deriving/DepTyCheck/Gen/Core.idr @@ -47,8 +47,9 @@ ConstructorDerivator => DerivatorCore where -- calculate which constructors are recursive and which are not consRecs <- for sig.targetType.cons $ \con => logBounds "consRec" [sig, con] $ do let conExprs = map type con.args ++ (getExpr <$> snd (unAppAny con.type)) - r <- any (hasNameInsideDeep sig.targetType.name) conExprs + let r = any (hasNameInsideDeep sig.targetType.name) conExprs pure (con, toRec r) + -- TODO to get rid of `for`, move `logBounds` somewhere else -- decide how to name a fuel argument on the LHS let fuelArg = "^fuel_arg^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 04706254..935e156a 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -37,6 +37,8 @@ namespace NonObligatoryExts [LeastEffort] {default False simplificationHack : Bool} -> ConstructorDerivator where consGenExpr sig con givs fuel = do + let niit : NamesInfoInTypes = %search -- I don't why it won't be found without this + ------------------------------------------------------------- -- Prepare intermediate data and functions using this data -- ------------------------------------------------------------- @@ -114,7 +116,7 @@ namespace NonObligatoryExts | No _ => fail "INTERNAL ERROR: error in given params set length computation" -- Check if called subgenerator can call the current one - mutRec <- hasNameInsideDeep sig.targetType.name $ var subsig.targetType.name + let mutRec = hasNameInsideDeep sig.targetType.name $ var subsig.targetType.name -- Decide whether to use local (decreasing) or outmost fuel, depending on whether we are in mutual recursion with subgen let subfuel = if mutRec then fuel else var outmostFuelArg diff --git a/src/Deriving/DepTyCheck/Gen/Derive.idr b/src/Deriving/DepTyCheck/Gen/Derive.idr index ef3139a9..78ae7989 100644 --- a/src/Deriving/DepTyCheck/Gen/Derive.idr +++ b/src/Deriving/DepTyCheck/Gen/Derive.idr @@ -44,7 +44,7 @@ Ord GenSignature where ---------------------- public export -interface Elaboration m => CanonicGen m where +interface Elaboration m => NamesInfoInTypes => CanonicGen m where callGen : (sig : GenSignature) -> (fuel : TTImp) -> Vect sig.givenParams.size TTImp -> m TTImp export diff --git a/src/Deriving/DepTyCheck/Gen/Entry.idr b/src/Deriving/DepTyCheck/Gen/Entry.idr index b5844445..2a47053e 100644 --- a/src/Deriving/DepTyCheck/Gen/Entry.idr +++ b/src/Deriving/DepTyCheck/Gen/Entry.idr @@ -296,6 +296,7 @@ deriveGenExpr signature = do checkResult@(signature ** externals ** _) <- checkTypeIsGen DerivationTask signature let externalsSigToName = fromList $ externals.externals <&> \(sig, _) => (sig, nameForGen sig) let fuelArg = outmostFuelArg + niit <- logBounds "namesInfo" [] $ getNamesInfoInTypes signature.targetType (callExpr, locals) <- runCanonic externalsSigToName $ callMainDerivedGen signature fuelArg wrapFuel fuelArg <$> internalGenCallingLambda checkResult (local locals callExpr) diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr index 36effced..f1463309 100644 --- a/src/Deriving/DepTyCheck/Util/Reflection.idr +++ b/src/Deriving/DepTyCheck/Util/Reflection.idr @@ -473,92 +473,39 @@ allVarNames expr = ttimp expr where piInfo (DefImplicit x) = ttimp x export -hasNameInsideDeep : Elaboration m => Name -> TTImp -> m Bool -hasNameInsideDeep nm expr = evalStateT .| the (SortedSet Name) empty .| hasInside where - - hasInside : forall mm. Elaboration mm => MonadState (SortedSet Name) mm => mm Bool - hasInside = ttimp expr where - mutual - - ttimp : TTImp -> mm Bool - ttimp $ IVar _ n = if n == nm then pure True else - if contains n !get then pure False else do - modify $ insert n - Just ty <- catch (getInfo' n) - | Nothing => pure False - let subexprs = (map type ty.args) ++ (ty.cons >>= \con => con.type :: map type con.args) - assert_total $ any ttimp subexprs - ttimp $ IPi _ _ z _ argTy retTy = ttimp argTy || ttimp retTy || piInfo z - ttimp $ ILam _ _ z _ argTy lamTy = ttimp argTy || ttimp lamTy || piInfo z - ttimp $ ILet _ _ _ _ nTy nVal sc = ttimp nTy || ttimp nVal || ttimp sc -- should we check `nTy` here? - ttimp $ ICase _ _ _ ty xs = ttimp ty || assert_total (any clause xs) - ttimp $ ILocal _ xs y = assert_total (any decl xs) || ttimp y - ttimp $ IUpdate _ xs y = assert_total (any fieldUpdate xs) || ttimp y - ttimp $ IApp _ y z = ttimp y || ttimp z - ttimp $ INamedApp _ y _ w = ttimp y || ttimp w - ttimp $ IAutoApp _ y z = ttimp y || ttimp z - ttimp $ IWithApp _ y z = ttimp y || ttimp z - ttimp $ ISearch _ _ = pure False - ttimp $ IAlternative _ y xs = altType y || assert_total (any ttimp xs) - ttimp $ IRewrite _ y z = ttimp y || ttimp z - ttimp $ IBindHere _ _ z = ttimp z - ttimp $ IBindVar _ _ = pure False - ttimp $ IAs _ _ _ _ w = ttimp w - ttimp $ IMustUnify _ _ z = ttimp z - ttimp $ IDelayed _ _ z = ttimp z - ttimp $ IDelay _ y = ttimp y - ttimp $ IForce _ y = ttimp y - ttimp $ IQuote _ y = ttimp y - ttimp $ IQuoteName _ _ = pure False - ttimp $ IQuoteDecl _ xs = assert_total $ any decl xs - ttimp $ IUnquote _ y = ttimp y - ttimp $ IPrimVal _ _ = pure False - ttimp $ IType _ = pure False - ttimp $ IHole _ _ = pure False - ttimp $ Implicit _ _ = pure False - ttimp $ IWithUnambigNames _ _ y = ttimp y - - altType : AltType -> mm Bool - altType FirstSuccess = pure False - altType Unique = pure False - altType (UniqueDefault x) = ttimp x - - lncpt : List (Name, Count, PiInfo TTImp, TTImp) -> mm Bool - lncpt = any (\(_, _, pii, tt) => piInfo pii || ttimp tt) - - ity : ITy -> mm Bool - ity $ MkTy _ _ _ ty = ttimp ty - - decl : Decl -> mm Bool - decl $ IClaim _ _ _ _ t = ity t - decl $ IData _ _ _ z = data_ z - decl $ IDef _ _ xs = any clause xs - decl $ IParameters _ xs ys = lncpt xs || assert_total (any decl ys) - decl $ IRecord _ _ _ _ $ MkRecord _ _ ps _ _ fs = lncpt ps || any (\(MkIField _ _ pii _ tt) => piInfo pii || ttimp tt) fs - decl $ INamespace _ _ xs = assert_total $ any decl xs - decl $ ITransform _ _ z w = ttimp z || ttimp w - decl $ IRunElabDecl _ y = ttimp y - decl $ ILog _ = pure False - decl $ IBuiltin _ _ _ = pure False - - data_ : Data -> mm Bool - data_ $ MkData x n tycon _ datacons = maybe (pure False) ttimp tycon || any ity datacons - data_ $ MkLater x n tycon = ttimp tycon - - fieldUpdate : IFieldUpdate -> mm Bool - fieldUpdate $ ISetField _ x = ttimp x - fieldUpdate $ ISetFieldApp _ x = ttimp x - - clause : Clause -> mm Bool - clause $ PatClause _ lhs rhs = ttimp lhs || ttimp rhs - clause $ WithClause _ lhs _ wval _ _ xs = ttimp lhs || ttimp wval || assert_total (any clause xs) - clause $ ImpossibleClause _ lhs = ttimp lhs - - piInfo : PiInfo TTImp -> mm Bool - piInfo ImplicitArg = pure False - piInfo ExplicitArg = pure False - piInfo AutoImplicit = pure False - piInfo (DefImplicit x) = ttimp x +record NamesInfoInTypes where + constructor Names + names : SortedMap Name $ List TTImp + +export +hasNameInsideDeep : NamesInfoInTypes => Name -> TTImp -> Bool +hasNameInsideDeep @{tyi} nm expr = hasInside empty [expr] where + + hasInside : (visited : SortedSet Name) -> (toLook : List TTImp) -> Bool + hasInside visited [] = False + hasInside visited (curr::rest) = do + let vs = toList $ allVarNames curr + let False = any (== nm) vs + | True => True + let nonVisited = filter (not . flip contains visited) vs + let new = nonVisited >>= \n => fromMaybe [] $ lookup n tyi.names + -- visited is limited and either growing or `new` is empty, thus `toLook` is strictly less + assert_total $ hasInside (visited `union` fromList nonVisited) (new ++ rest) + +export +getNamesInfoInTypes : Elaboration m => TypeInfo -> m NamesInfoInTypes +getNamesInfoInTypes ty = Names <$> go empty [ty] + where + + subexprs : TypeInfo -> List TTImp + subexprs ty = map type ty.args ++ (ty.cons >>= \con => con.type :: map type con.args) + + go : SortedMap Name (List TTImp) -> List TypeInfo -> m $ SortedMap Name (List TTImp) + go tyi [] = pure tyi + go tyi (ti::rest) = do + let subes = subexprs ti + new <- map join $ for subes $ map (mapMaybe id) . traverse (catch . getInfo') . filter (isNothing . flip lookup tyi) . allVarNames + assert_total $ go (insert ti.name subes tyi) (new ++ rest) public export isVar : TTImp -> Bool From f6b6e57e4d44a56fc7a39d78aa040218d84b0dea Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Thu, 28 Mar 2024 15:35:09 +0300 Subject: [PATCH 2/4] [ refactor ] Reimplement `allVarNames` through a obeserving traversal --- .../DepTyCheck/Gen/Core/ConsDerive.idr | 2 +- src/Deriving/DepTyCheck/Util/Reflection.idr | 89 +++---------------- 2 files changed, 13 insertions(+), 78 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 935e156a..5cb8193d 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -161,7 +161,7 @@ namespace NonObligatoryExts -------------------------------------------------------------------------------- -- Acquire those variables that appear in non-trivial type expressions, i.e. those which needs to be generated before the left-to-right phase - let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ as) => rights (toList as) >>= toList . allVarNames + let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ as) => rights (toList as) >>= allVarNames let preLTR = SortedSet.fromList $ mapMaybe (flip lookup conArgIdxs) preLTR -- Find rightmost arguments among `preLTR` diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr index f1463309..1863c218 100644 --- a/src/Deriving/DepTyCheck/Util/Reflection.idr +++ b/src/Deriving/DepTyCheck/Util/Reflection.idr @@ -1,6 +1,8 @@ ||| `Language.Reflection`-related utilities module Deriving.DepTyCheck.Util.Reflection +import public Control.Applicative.Const + import public Data.Fin import public Data.Fuel import public Data.Nat.Pos @@ -394,83 +396,16 @@ nameConformsTo cand origin = do -- simple syntactic search of a `IVar`, disregarding shadowing or whatever export -allVarNames : TTImp -> LazyList Name -allVarNames expr = ttimp expr where - mutual +allVarNames' : TTImp -> SortedSet Name +allVarNames' = runConst . mapATTImp' f where + f : TTImp -> Const (SortedSet Name) TTImp -> Const (SortedSet Name) TTImp + f (IVar _ n) = const $ MkConst $ singleton n + f _ = id - ttimp : TTImp -> LazyList Name - ttimp $ IVar _ n = [n] - ttimp $ IPi _ _ z _ argTy retTy = ttimp argTy ++ ttimp retTy ++ piInfo z - ttimp $ ILam _ _ z _ argTy lamTy = ttimp argTy ++ ttimp lamTy ++ piInfo z - ttimp $ ILet _ _ _ _ nTy nVal sc = ttimp nTy ++ ttimp nVal ++ ttimp sc -- should we check `nTy` here? - ttimp $ ICase _ _ _ ty xs = ttimp ty ++ assert_total (foldMap clause xs) - ttimp $ ILocal _ xs y = assert_total (foldMap decl xs) ++ ttimp y - ttimp $ IUpdate _ xs y = assert_total (foldMap fieldUpdate xs) ++ ttimp y - ttimp $ IApp _ y z = ttimp y ++ ttimp z - ttimp $ INamedApp _ y _ w = ttimp y ++ ttimp w - ttimp $ IAutoApp _ y z = ttimp y ++ ttimp z - ttimp $ IWithApp _ y z = ttimp y ++ ttimp z - ttimp $ ISearch _ _ = [] - ttimp $ IAlternative _ y xs = altType y ++ assert_total (foldMap ttimp xs) - ttimp $ IRewrite _ y z = ttimp y ++ ttimp z - ttimp $ IBindHere _ _ z = ttimp z - ttimp $ IBindVar _ _ = [] - ttimp $ IAs _ _ _ _ w = ttimp w - ttimp $ IMustUnify _ _ z = ttimp z - ttimp $ IDelayed _ _ z = ttimp z - ttimp $ IDelay _ y = ttimp y - ttimp $ IForce _ y = ttimp y - ttimp $ IQuote _ y = ttimp y - ttimp $ IQuoteName _ _ = [] - ttimp $ IQuoteDecl _ xs = assert_total $ foldMap decl xs - ttimp $ IUnquote _ y = ttimp y - ttimp $ IPrimVal _ _ = [] - ttimp $ IType _ = [] - ttimp $ IHole _ _ = [] - ttimp $ Implicit _ _ = [] - ttimp $ IWithUnambigNames _ _ y = ttimp y - - altType : AltType -> LazyList Name - altType FirstSuccess = [] - altType Unique = [] - altType (UniqueDefault x) = ttimp x - - lncpt : List (Name, Count, PiInfo TTImp, TTImp) -> LazyList Name - lncpt = foldMap (\(_, _, pii, tt) => piInfo pii ++ ttimp tt) - - ity : ITy -> LazyList Name - ity $ MkTy _ _ _ ty = ttimp ty - - decl : Decl -> LazyList Name - decl $ IClaim _ _ _ _ t = ity t - decl $ IData _ _ _ z = data_ z - decl $ IDef _ _ xs = foldMap clause xs - decl $ IParameters _ xs ys = lncpt xs ++ assert_total (foldMap decl ys) - decl $ IRecord _ _ _ _ $ MkRecord _ _ ps _ _ fs = lncpt ps ++ foldMap (\(MkIField _ _ pii _ tt) => piInfo pii ++ ttimp tt) fs - decl $ INamespace _ _ xs = assert_total $ foldMap decl xs - decl $ ITransform _ _ z w = ttimp z ++ ttimp w - decl $ IRunElabDecl _ y = ttimp y - decl $ ILog _ = [] - decl $ IBuiltin _ _ _ = [] - - data_ : Data -> LazyList Name - data_ $ MkData x n tycon _ datacons = maybe [] ttimp tycon ++ foldMap ity datacons - data_ $ MkLater x n tycon = ttimp tycon - - fieldUpdate : IFieldUpdate -> LazyList Name - fieldUpdate $ ISetField _ x = ttimp x - fieldUpdate $ ISetFieldApp _ x = ttimp x - - clause : Clause -> LazyList Name - clause $ PatClause _ lhs rhs = ttimp lhs ++ ttimp rhs - clause $ WithClause _ lhs _ wval _ _ xs = ttimp lhs ++ ttimp wval ++ assert_total (foldMap clause xs) - clause $ ImpossibleClause _ lhs = ttimp lhs - - piInfo : PiInfo TTImp -> LazyList Name - piInfo ImplicitArg = [] - piInfo ExplicitArg = [] - piInfo AutoImplicit = [] - piInfo (DefImplicit x) = ttimp x +-- Same as `allVarNames'`, but returning `List` +export +allVarNames : TTImp -> List Name +allVarNames = SortedSet.toList . allVarNames' export record NamesInfoInTypes where @@ -484,7 +419,7 @@ hasNameInsideDeep @{tyi} nm expr = hasInside empty [expr] where hasInside : (visited : SortedSet Name) -> (toLook : List TTImp) -> Bool hasInside visited [] = False hasInside visited (curr::rest) = do - let vs = toList $ allVarNames curr + let vs = allVarNames curr let False = any (== nm) vs | True => True let nonVisited = filter (not . flip contains visited) vs From 4061894f30314da4d53acd8400d038a9581a82ff Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Thu, 8 Feb 2024 20:38:21 +0300 Subject: [PATCH 3/4] [ refactor ] Get rid of useless traversal, lose precise `consRec` logs --- src/Deriving/DepTyCheck/Gen/Core.idr | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Core.idr b/src/Deriving/DepTyCheck/Gen/Core.idr index ed4e50d4..f114ac11 100644 --- a/src/Deriving/DepTyCheck/Gen/Core.idr +++ b/src/Deriving/DepTyCheck/Gen/Core.idr @@ -45,11 +45,10 @@ ConstructorDerivator => DerivatorCore where canonicConsBody sig (consGenName con) con <&> def (consGenName con) -- calculate which constructors are recursive and which are not - consRecs <- for sig.targetType.cons $ \con => logBounds "consRec" [sig, con] $ do + consRecs <- logBounds "consRec" [sig] $ pure $ sig.targetType.cons <&> \con => do let conExprs = map type con.args ++ (getExpr <$> snd (unAppAny con.type)) let r = any (hasNameInsideDeep sig.targetType.name) conExprs - pure (con, toRec r) - -- TODO to get rid of `for`, move `logBounds` somewhere else + (con, toRec r) -- decide how to name a fuel argument on the LHS let fuelArg = "^fuel_arg^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend From 309d67fd3829df0f4f5be4ff957998349a384a5d Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Thu, 28 Mar 2024 17:18:13 +0300 Subject: [PATCH 4/4] [ fixup ] More optmimal storage of names info --- src/Deriving/DepTyCheck/Util/Reflection.idr | 25 ++++++++++----------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr index 1863c218..fdee6c88 100644 --- a/src/Deriving/DepTyCheck/Util/Reflection.idr +++ b/src/Deriving/DepTyCheck/Util/Reflection.idr @@ -410,22 +410,18 @@ allVarNames = SortedSet.toList . allVarNames' export record NamesInfoInTypes where constructor Names - names : SortedMap Name $ List TTImp + names : SortedMap Name $ SortedSet Name export hasNameInsideDeep : NamesInfoInTypes => Name -> TTImp -> Bool -hasNameInsideDeep @{tyi} nm expr = hasInside empty [expr] where +hasNameInsideDeep @{tyi} nm = hasInside empty . allVarNames where - hasInside : (visited : SortedSet Name) -> (toLook : List TTImp) -> Bool + hasInside : (visited : SortedSet Name) -> (toLook : List Name) -> Bool hasInside visited [] = False - hasInside visited (curr::rest) = do - let vs = allVarNames curr - let False = any (== nm) vs - | True => True - let nonVisited = filter (not . flip contains visited) vs - let new = nonVisited >>= \n => fromMaybe [] $ lookup n tyi.names + hasInside visited (curr::rest) = if curr == nm then True else do + let new = if contains curr visited then [] else maybe [] SortedSet.toList $ lookup curr tyi.names -- visited is limited and either growing or `new` is empty, thus `toLook` is strictly less - assert_total $ hasInside (visited `union` fromList nonVisited) (new ++ rest) + assert_total $ hasInside (insert curr visited) (new ++ rest) export getNamesInfoInTypes : Elaboration m => TypeInfo -> m NamesInfoInTypes @@ -435,11 +431,14 @@ getNamesInfoInTypes ty = Names <$> go empty [ty] subexprs : TypeInfo -> List TTImp subexprs ty = map type ty.args ++ (ty.cons >>= \con => con.type :: map type con.args) - go : SortedMap Name (List TTImp) -> List TypeInfo -> m $ SortedMap Name (List TTImp) + go : SortedMap Name (SortedSet Name) -> List TypeInfo -> m $ SortedMap Name $ SortedSet Name go tyi [] = pure tyi go tyi (ti::rest) = do - let subes = subexprs ti - new <- map join $ for subes $ map (mapMaybe id) . traverse (catch . getInfo') . filter (isNothing . flip lookup tyi) . allVarNames + let subes = concatMap allVarNames' $ subexprs ti + new <- map join $ for (SortedSet.toList subes) $ \n => + if isNothing $ lookup n tyi + then map toList $ catch $ getInfo' n + else pure [] assert_total $ go (insert ti.name subes tyi) (new ++ rest) public export