From c6bf7b3b6e607945332e554a8e5c22529b44b138 Mon Sep 17 00:00:00 2001 From: "Serge S. Gulin" Date: Thu, 3 Oct 2024 12:22:25 +0400 Subject: [PATCH] ScopedSnocList: WIP: trivial constructor substitutions --- src/Core/GetType.idr | 2 +- src/Core/Metadata.idr | 12 ++++++------ src/Core/Termination/CallGraph.idr | 3 ++- src/Core/Termination/Positivity.idr | 24 ++++++++++++------------ src/Core/Unify.idr | 26 ++++++++++++++------------ src/Idris/Doc/Display.idr | 6 +++--- src/Idris/Doc/String.idr | 14 +++++++------- src/Idris/Error.idr | 6 +++--- src/Idris/IDEMode/Holes.idr | 4 ++-- src/TTImp/Elab/Check.idr | 4 +++- src/TTImp/Elab/Utils.idr | 20 +++++++++++--------- src/TTImp/TTImp.idr | 11 ++++++----- src/TTImp/Unelab.idr | 4 +++- 13 files changed, 73 insertions(+), 63 deletions(-) diff --git a/src/Core/GetType.idr b/src/Core/GetType.idr index 0e82282684..3cd9d3967c 100644 --- a/src/Core/GetType.idr +++ b/src/Core/GetType.idr @@ -33,7 +33,7 @@ mutual chkMeta fc env !(nf defs env (embed mty)) args chk env (Bind fc nm b sc) = do bt <- chkBinder env b - sct <- chk {vars = _ :< nm} (b :: env) sc + sct <- chk {vars = _ :< nm} (env :< b) sc pure $ gnf env (discharge fc nm b !(getTerm bt) !(getTerm sct)) chk env (App fc f a) = do fty <- chk env f diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 2743e7313d..c91d86845d 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -205,9 +205,9 @@ addLHS loc outerenvlen env tm where toPat : Env Term vs -> Env Term vs - toPat (Lam fc c p ty :: bs) = PVar fc c p ty :: toPat bs - toPat (b :: bs) = b :: toPat bs - toPat [] = [] + toPat (bs :< Lam fc c p ty) = toPat bs :< PVar fc c p ty + toPat (bs :< b) = toPat bs :< b + toPat [<] = [<] -- For giving local variable names types, just substitute the name -- rather than storing the whole environment, otherwise we'll repeatedly @@ -219,8 +219,8 @@ addLHS loc outerenvlen env tm -- types directly! substEnv : {vars : _} -> FC -> Env Term vars -> (tm : Term vars) -> ClosedTerm -substEnv loc [] tm = tm -substEnv {vars = _ :< x} loc (b :: env) tm +substEnv loc [<] tm = tm +substEnv {vars = _ :< x} loc (env :< b) tm = substEnv loc env (subst (Ref loc Bound x) tm) export @@ -357,7 +357,7 @@ normaliseTypes nfType : Defs -> (NonEmptyFC, (Name, Nat, ClosedTerm)) -> Core (NonEmptyFC, (Name, Nat, ClosedTerm)) nfType defs (loc, (n, len, ty)) - = pure (loc, (n, len, !(normaliseArgHoles defs [] ty))) + = pure (loc, (n, len, !(normaliseArgHoles defs [<] ty))) record TTMFile where constructor MkTTMFile diff --git a/src/Core/Termination/CallGraph.idr b/src/Core/Termination/CallGraph.idr index 9b318ad3d1..e4a81a974c 100644 --- a/src/Core/Termination/CallGraph.idr +++ b/src/Core/Termination/CallGraph.idr @@ -5,6 +5,7 @@ import Core.Context.Log import Core.Env import Core.Normalise import Core.Value +import Core.Name.CompatibleVars import Libraries.Data.SparseMatrix @@ -76,7 +77,7 @@ mutual findSC {vars} defs env g pats (Bind fc n b sc) = pure $ !(findSCbinder b) ++ - !(findSC defs (b :: env) g (map weaken pats) sc) + !(findSC defs (env :< b) g (map weaken pats) sc) where findSCbinder : Binder (Term vars) -> Core (List SCCall) findSCbinder (Let _ c val ty) = findSC defs env g pats val diff --git a/src/Core/Termination/Positivity.idr b/src/Core/Termination/Positivity.idr index 6498797dbf..b4020842c0 100644 --- a/src/Core/Termination/Positivity.idr +++ b/src/Core/Termination/Positivity.idr @@ -26,7 +26,7 @@ nameIn defs tyns (NBind fc x b sc) = if !(nameIn defs tyns !(evalClosure defs (binderType b))) then pure True else do let nm = Ref fc Bound (MN ("NAMEIN_" ++ show x) 0) - let arg = toClosure defaultOpts [] nm + let arg = toClosure defaultOpts [<] nm sc' <- sc defs arg nameIn defs tyns sc' nameIn defs tyns (NApp _ nh args) @@ -55,7 +55,7 @@ posArgs : {auto c : Ref Ctxt Defs} -> posArgs defs tyn [] = pure IsTerminating posArgs defs tyn (x :: xs) = do xNF <- evalClosure defs x - logNF "totality.positivity" 50 "Checking parameter for positivity" [] xNF + logNF "totality.positivity" 50 "Checking parameter for positivity" [<] xNF IsTerminating <- posArg defs tyn xNF | err => pure err posArgs defs tyn xs @@ -63,7 +63,7 @@ posArgs defs tyn (x :: xs) -- a tyn can only appear in the parameter positions of -- tc; report positivity failure if it appears anywhere else posArg defs tyns nf@(NTCon loc tc _ _ args) = - do logNF "totality.positivity" 50 "Found a type constructor" [] nf + do logNF "totality.positivity" 50 "Found a type constructor" [<] nf testargs <- case !(lookupDefExact tc (gamma defs)) of Just (TCon _ _ params _ _ _ _ _) => do logC "totality.positivity" 50 $ @@ -86,25 +86,25 @@ posArg defs tyns nf@(NTCon loc tc _ _ args) = else mapSnd (x ::) (splitParams (S i) ps xs) -- a tyn can not appear as part of ty posArg defs tyns nf@(NBind fc x (Pi _ _ e ty) sc) - = do logNF "totality.positivity" 50 "Found a Pi-type" [] nf + = do logNF "totality.positivity" 50 "Found a Pi-type" [<] nf if !(nameIn defs tyns !(evalClosure defs ty)) then pure (NotTerminating NotStrictlyPositive) else do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 1) - let arg = toClosure defaultOpts [] nm + let arg = toClosure defaultOpts [<] nm sc' <- sc defs arg posArg defs tyns sc' posArg defs tyns nf@(NApp fc nh args) = do False <- isAssertTotal nh - | True => do logNF "totality.positivity" 50 "Trusting an assertion" [] nf + | True => do logNF "totality.positivity" 50 "Trusting an assertion" [<] nf pure IsTerminating - logNF "totality.positivity" 50 "Found an application" [] nf + logNF "totality.positivity" 50 "Found an application" [<] nf args <- traverse (evalClosure defs . snd) (toList args) pure $ if !(anyM (nameIn defs tyns) args) then NotTerminating NotStrictlyPositive else IsTerminating posArg defs tyn (NDelayed fc lr ty) = posArg defs tyn ty posArg defs tyn nf - = do logNF "totality.positivity" 50 "Reached the catchall" [] nf + = do logNF "totality.positivity" 50 "Reached the catchall" [<] nf pure IsTerminating checkPosArgs : {auto c : Ref Ctxt Defs} -> @@ -113,11 +113,11 @@ checkPosArgs defs tyns (NBind fc x (Pi _ _ e ty) sc) = case !(posArg defs tyns !(evalClosure defs ty)) of IsTerminating => do let nm = Ref fc Bound (MN ("POSCHECK_" ++ show x) 0) - let arg = toClosure defaultOpts [] nm + let arg = toClosure defaultOpts [<] nm checkPosArgs defs tyns !(sc defs arg) bad => pure bad checkPosArgs defs tyns nf - = do logNF "totality.positivity" 50 "Giving up on non-Pi type" [] nf + = do logNF "totality.positivity" 50 "Giving up on non-Pi type" [<] nf pure IsTerminating checkCon : {auto c : Ref Ctxt Defs} -> @@ -130,8 +130,8 @@ checkCon defs tyns cn Just ty => case !(totRefsIn defs ty) of IsTerminating => - do tyNF <- nf defs [] ty - logNF "totality.positivity" 20 "Checking the type " [] tyNF + do tyNF <- nf defs [<] ty + logNF "totality.positivity" 20 "Checking the type " [<] tyNF checkPosArgs defs tyns tyNF bad => pure bad diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 63830ce873..159663d19c 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -13,10 +13,12 @@ import public Core.UnifyState import Core.Value import Data.List +import Data.SnocList import Data.Maybe import Libraries.Data.IntMap import Libraries.Data.NameMap +import Libraries.Data.SnocList.SizeOf %default covering @@ -452,7 +454,7 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm PV pv pi => throw (PatternVariableUnifies loc (getLoc otm) env (PV pv pi) otm) _ => pure () defs <- get Ctxt - ty <- normalisePis defs [] $ type mdef + ty <- normalisePis defs [<] $ type mdef -- make sure we have all the pi binders we need in the -- type to make the metavariable definition logTerm "unify.instantiate" 5 ("Type: " ++ show mname) (type mdef) @@ -1071,7 +1073,7 @@ mutual ct <- unify (lower mode) loc env tx ty xn <- genVarName "x" let env' : Env Term (_ :< x) - = Pi fcy cy Explicit tx' :: env + = env :< Pi fcy cy Explicit tx' case constraints ct of [] => -- No constraints, check the scope do tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn)) @@ -1108,7 +1110,7 @@ mutual xn <- genVarName "x" txtm <- quote empty env tx let env' : Env Term (_ :< x) - = Lam fcx cx Explicit txtm :: env + = env :< Lam fcx cx Explicit txtm tscx <- scx defs (toClosure defaultOpts env (Ref loc Bound xn)) tscy <- scy defs (toClosure defaultOpts env (Ref loc Bound xn)) @@ -1438,9 +1440,9 @@ retryGuess mode smode (hid, (loc, hname)) BySearch rig depth defining => handleUnify (do tm <- search loc rig (smode == Defaults) depth defining - (type def) [] + (type def) [<] let gdef = { definition := PMDef defaultPI [<] (STerm 0 tm) (STerm 0 tm) [] } def - logTermNF "unify.retry" 5 ("Solved " ++ show hname) [] tm + logTermNF "unify.retry" 5 ("Solved " ++ show hname) [<] tm ignore $ addDef (Resolved hid) gdef removeGuess hid pure True) @@ -1454,13 +1456,13 @@ retryGuess mode smode (hid, (loc, hname)) err => do logTermNF "unify.retry" 5 ("Search failed at " ++ show rig ++ " for " ++ show hname) - [] (type def) + [<] (type def) case smode of LastChance => throw err _ => if recoverable err then pure False -- Postpone again else throw (CantSolveGoal loc (gamma defs) - [] (type def) (Just err)) + [<] (type def) (Just err)) Guess tm envb [constr] => do let umode = case smode of MatchArgs => inMatch @@ -1471,7 +1473,7 @@ retryGuess mode smode (hid, (loc, hname)) NoLazy => pure tm AddForce r => pure $ forceMeta r envb tm AddDelay r => - do ty <- getType [] tm + do ty <- getType [<] tm logTerm "unify.retry" 5 "Retry Delay" tm pure $ delayMeta r envb !(getTerm ty) tm let gdef = { definition := PMDef (MkPMDefInfo NotHole True False) @@ -1484,7 +1486,7 @@ retryGuess mode smode (hid, (loc, hname)) NoLazy => pure tm AddForce r => pure $ forceMeta r envb tm AddDelay r => - do ty <- getType [] tm + do ty <- getType [<] tm logTerm "unify.retry" 5 "Retry Delay (constrained)" tm pure $ delayMeta r envb !(getTerm ty) tm let gdef = { definition := Guess tm' envb newcs } def @@ -1579,7 +1581,7 @@ checkArgsSame (x :: xs) Just (PMDef _ [<] (STerm 0 def) _ _) <- lookupDefExact (Resolved t) (gamma defs) | _ => anySame tm ts - if !(convert defs [] tm def) + if !(convert defs [<] tm def) then pure True else anySame tm ts @@ -1597,7 +1599,7 @@ checkDots getHoleName : Term [<] -> Core (Maybe Name) getHoleName tm = do defs <- get Ctxt - NApp _ (NMeta n' i args) _ <- nf defs [] tm + NApp _ (NMeta n' i args) _ <- nf defs [<] tm | _ => pure Nothing pure (Just n') @@ -1651,7 +1653,7 @@ checkDots do defs <- get Ctxt Just dty <- lookupTyExact n (gamma defs) | Nothing => undefinedName fc n - logTermNF "unify.constraint" 5 "Dot type" [] dty + logTermNF "unify.constraint" 5 "Dot type" [<] dty -- Clear constraints so we don't report again -- later put UST ({ dotConstraints := [] } ust) diff --git a/src/Idris/Doc/Display.idr b/src/Idris/Doc/Display.idr index aaeafd73af..972c66d9d9 100644 --- a/src/Idris/Doc/Display.idr +++ b/src/Idris/Doc/Display.idr @@ -24,13 +24,13 @@ displayType : {auto c : Ref Ctxt Defs} -> (shortName : Bool) -> Defs -> (Name, Int, GlobalDef) -> Core (Doc IdrisSyntax) displayType shortName defs (n, i, gdef) - = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef)) + = maybe (do tm <- resugar [<] !(normaliseHoles defs [<] (type gdef)) nm <- aliasName (fullname gdef) let nm = ifThenElse shortName (dropNS nm) nm let prig = prettyRig gdef.multiplicity let ann = showCategory id gdef pure (prig <+> ann (cast $ prettyOp True nm) <++> colon <++> pretty tm)) - (\num => prettyHole defs [] n num (type gdef)) + (\num => prettyHole defs [<] n num (type gdef)) (isHole gdef) export displayTerm : {auto c : Ref Ctxt Defs} -> @@ -38,7 +38,7 @@ displayTerm : {auto c : Ref Ctxt Defs} -> Defs -> ClosedTerm -> Core (Doc IdrisSyntax) displayTerm defs tm - = do ptm <- resugar [] !(normaliseHoles defs [] tm) + = do ptm <- resugar [<] !(normaliseHoles defs [<] tm) pure (pretty ptm) export diff --git a/src/Idris/Doc/String.idr b/src/Idris/Doc/String.idr index 45c15ab92d..51e6d3f48d 100644 --- a/src/Idris/Doc/String.idr +++ b/src/Idris/Doc/String.idr @@ -88,9 +88,9 @@ prettyType : {auto c : Ref Ctxt Defs} -> (IdrisSyntax -> ann) -> ClosedTerm -> Core (Doc ann) prettyType syn ty = do defs <- get Ctxt - ty <- normaliseHoles defs [] ty + ty <- normaliseHoles defs [<] ty ty <- toFullNames ty - ty <- resugar [] ty + ty <- resugar [<] ty pure (prettyBy syn ty) ||| Look up implementations @@ -108,10 +108,10 @@ getImplDocs keep let Just Func = defNameType (definition def) | _ => pure [] -- Check that the type mentions the name of interest - ty <- toFullNames !(normaliseHoles defs [] (type def)) + ty <- toFullNames !(normaliseHoles defs [<] (type def)) True <- keep ty | False => pure [] - ty <- resugar [] ty + ty <- resugar [<] ty pure [annotate (Decl impl) $ prettyBy Syntax ty] pure $ case concat docss of [] => [] @@ -156,7 +156,7 @@ getDocsForPrimitive constant = do let (_, type) = checkPrim EmptyFC constant let typeString = prettyBy Syntax constant <++> colon - <++> prettyBy Syntax !(resugar [] type) + <++> prettyBy Syntax !(resugar [<] type) hintsDoc <- getHintsForPrimitive constant pure $ vcat $ typeString :: indent 2 (primDoc constant) @@ -451,7 +451,7 @@ getDocsForName fc n config (pure (Nothing, [])) -- Then form the type declaration - ty <- resugar [] =<< normaliseHoles defs [] (type def) + ty <- resugar [<] =<< normaliseHoles defs [<] (type def) -- when printing e.g. interface methods there is no point in -- repeating the interface's name let ty = ifThenElse (not dropFirst) ty $ case ty of @@ -504,7 +504,7 @@ getDocsForImplementation t = do -- get the return type of all the candidate hints Just (ix, def) <- lookupCtxtExactI hint (gamma defs) | Nothing => pure Nothing - ty <- resugar [] =<< normaliseHoles defs [] (type def) + ty <- resugar [<] =<< normaliseHoles defs [<] (type def) let (_, retTy) = underPis ty -- try to see whether it approximates what we are looking for -- we throw the head away because it'll be the interface name (I) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index be8b1c2476..20bfbfbdeb 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -392,7 +392,7 @@ perrorRaw (NotCovering fc n (MissingCases cs)) = pure $ errorDesc (code (pretty0 !(prettyName n)) <++> reflow "is not covering.") <+> line <+> !(ploc fc) <+> line <+> reflow "Missing cases" <+> colon <+> line - <+> indent 4 (vsep !(traverse (pshow []) (toList cs))) <+> line + <+> indent 4 (vsep !(traverse (pshow [<]) (toList cs))) <+> line perrorRaw (NotCovering fc n (NonCoveringCall ns)) = pure $ errorDesc (pretty0 !(prettyName n) <++> reflow "is not covering.") <+> line <+> !(ploc fc) <+> line @@ -533,8 +533,8 @@ perrorRaw (CantSolveGoal fc gam env g reason) dropEnv : {vars : _} -> Env Term vars -> Term vars -> (ns ** (Env Term ns, Term ns)) - dropEnv env (Bind _ n b@(Pi _ _ _ _) sc) = dropEnv (b :: env) sc - dropEnv env (Bind _ n b@(Let _ _ _ _) sc) = dropEnv (b :: env) sc + dropEnv env (Bind _ n b@(Pi _ _ _ _) sc) = dropEnv (env :< b) sc + dropEnv env (Bind _ n b@(Let _ _ _ _) sc) = dropEnv (env :< b) sc dropEnv env tm = (_ ** (env, tm)) perrorRaw (DeterminingArg fc n i env g) diff --git a/src/Idris/IDEMode/Holes.idr b/src/Idris/IDEMode/Holes.idr index a32a3889e1..982ef3e727 100644 --- a/src/Idris/IDEMode/Holes.idr +++ b/src/Idris/IDEMode/Holes.idr @@ -100,7 +100,7 @@ extractHoleData : {vars : _} -> extractHoleData defs env fn (S args) (Bind fc x (Let _ c val ty) sc) = extractHoleData defs env fn args (subst val sc) extractHoleData defs env fn (S args) (Bind fc x b sc) - = do rest <- extractHoleData defs (b :: env) fn args sc + = do rest <- extractHoleData defs (env :< b) fn args sc let True = showName x | False => do log "ide-mode.hole" 10 $ "Not showing name: " ++ show x pure rest @@ -155,7 +155,7 @@ getUserHolesData traverse (\n_gdef_args => -- Inference can't deal with this for now :/ let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in - holeData defs [] n args (type gdef)) + holeData defs [<] n args (type gdef)) holesWithArgs export diff --git a/src/TTImp/Elab/Check.idr b/src/TTImp/Elab/Check.idr index bd4c819f8a..9c7a166996 100644 --- a/src/TTImp/Elab/Check.idr +++ b/src/TTImp/Elab/Check.idr @@ -27,6 +27,8 @@ import Libraries.Data.NameMap import Libraries.Data.UserNameMap import Libraries.Data.WithDefault +import Libraries.Data.SnocList.SizeOf + %default covering public export @@ -470,7 +472,7 @@ searchVar fc rig depth def env nest n ty varn <- toFullNames n' pure ((vs :< varn) ** (\t => f (Bind fc varn binder t), - binder :: env')) + env' :< binder)) -- Elaboration info (passed to recursive calls) public export diff --git a/src/TTImp/Elab/Utils.idr b/src/TTImp/Elab/Utils.idr index c0ecbc65b0..00e45f97bf 100644 --- a/src/TTImp/Elab/Utils.idr +++ b/src/TTImp/Elab/Utils.idr @@ -11,6 +11,8 @@ import Core.Value import TTImp.Elab.Check import TTImp.TTImp +import Data.SnocList + %default covering detagSafe : {auto c : Ref Ctxt Defs} -> @@ -38,7 +40,7 @@ findErasedFrom defs pos (NBind fc x (Pi _ c _ aty) scf) = do -- In the scope, use 'Erased fc Impossible' to mean 'argument is erased'. -- It's handy here, because we can use it to tell if a detaggable -- argument position is available - sc <- scf defs (toClosure defaultOpts [] (Erased fc (ifThenElse (isErased c) Impossible Placeholder))) + sc <- scf defs (toClosure defaultOpts [<] (Erased fc (ifThenElse (isErased c) Impossible Placeholder))) (erest, dtrest) <- findErasedFrom defs (1 + pos) sc let dt' = if !(detagSafe defs !(evalClosure defs aty)) then (pos :: dtrest) else dtrest @@ -54,7 +56,7 @@ findErased : {auto c : Ref Ctxt Defs} -> ClosedTerm -> Core (List Nat, List Nat) findErased tm = do defs <- get Ctxt - tmnf <- nf defs [] tm + tmnf <- nf defs [<] tm findErasedFrom defs 0 tmnf export @@ -86,16 +88,16 @@ bindNotReq : {vs : _} -> FC -> Int -> Env Term vs -> (sub : Thin pre vs) -> List (PiInfo RawImp, Name) -> Term vs -> (List (PiInfo RawImp, Name), Term pre) -bindNotReq fc i [] Refl ns tm = (ns, embed tm) -bindNotReq fc i (b :: env) Refl ns tm +bindNotReq fc i [<] Refl ns tm = (ns, embed tm) +bindNotReq fc i (env :< b) Refl ns tm = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm (ns', btm) = bindNotReq fc (1 + i) env Refl ns tmptm in (ns', refToLocal (MN "arg" i) _ btm) -bindNotReq fc i (b :: env) (Keep p) ns tm +bindNotReq fc i (env :< b) (Keep p) ns tm = let tmptm = subst (Ref fc Bound (MN "arg" i)) tm (ns', btm) = bindNotReq fc (1 + i) env p ns tmptm in (ns', refToLocal (MN "arg" i) _ btm) -bindNotReq {vs = _ :< n} fc i (b :: env) (Drop p) ns tm +bindNotReq {vs = _ :< n} fc i (env :< b) (Drop p) ns tm = bindNotReq fc i env p ((plicit b, n) :: ns) (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b)) tm) @@ -109,13 +111,13 @@ bindReq {vs} fc env Refl ns tm where notLets : List Name -> (vars : SnocList Name) -> Env Term vars -> List Name notLets acc [<] _ = acc - notLets acc (vs :< v) (b :: env) = if isLet b then notLets acc vs env + notLets acc (vs :< v) (env :< b) = if isLet b then notLets acc vs env else notLets (v :: acc) vs env -bindReq {vs = _ :< n} fc (b :: env) (Keep p) ns tm +bindReq {vs = _ :< n} fc (env :< b) (Keep p) ns tm = do b' <- shrinkBinder b p bindReq fc env p ((plicit b, n) :: ns) (Bind fc _ (Pi (binderLoc b) (multiplicity b) Explicit (binderType b')) tm) -bindReq fc (b :: env) (Drop p) ns tm +bindReq fc (env :< b) (Drop p) ns tm = bindReq fc env p ns tm -- This machinery is to calculate whether any top level argument is used diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 0c80fd78ab..812fed6cdb 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -15,6 +15,7 @@ import Data.Maybe import Libraries.Data.SortedSet import Libraries.Data.WithDefault +import Libraries.Data.SnocList.SizeOf %default covering @@ -693,7 +694,7 @@ implicitsAs n defs ns tm "Could not find variable " ++ show n pure $ IVar loc nm Just ty => - do ty' <- nf defs [] ty + do ty' <- nf defs [<] ty implicits <- findImps is es ns ty' log "declare.def.lhs.implicits" 30 $ "\n In the type of " ++ show n ++ ": " ++ show ty ++ @@ -730,12 +731,12 @@ implicitsAs n defs ns tm -- and explicit variables. So we first peel off all of the quantifiers -- corresponding to these variables. findImps ns es (_ :: locals) (NBind fc x (Pi _ _ _ _) sc) - = do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + = do body <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) findImps ns es locals body -- ^ TODO? check that name of the pi matches name of local? -- don't add implicits coming after explicits that aren't given findImps ns es [] (NBind fc x (Pi _ _ Explicit _) sc) - = do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + = do body <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) case es of -- Explicits were skipped, therefore all explicits are given anyway Just (UN Underscore) :: _ => findImps ns es [] body @@ -745,13 +746,13 @@ implicitsAs n defs ns tm Just es' => findImps ns es' [] body -- if the implicit was given, skip it findImps ns es [] (NBind fc x (Pi _ _ AutoImplicit _) sc) - = do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + = do body <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) case updateNs x ns of Nothing => -- didn't find explicit call pure $ (x, AutoImplicit) :: !(findImps ns es [] body) Just ns' => findImps ns' es [] body findImps ns es [] (NBind fc x (Pi _ _ p _) sc) - = do body <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + = do body <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) if Just x `elem` ns then findImps ns es [] body else pure $ (x, forgetDef p) :: !(findImps ns es [] body) diff --git a/src/TTImp/Unelab.idr b/src/TTImp/Unelab.idr index bf89fabb6e..66690cb84b 100644 --- a/src/TTImp/Unelab.idr +++ b/src/TTImp/Unelab.idr @@ -13,6 +13,8 @@ import TTImp.TTImp import Data.List import Data.String +import Libraries.Data.SnocList.SizeOf + %default covering used : (idx : Nat) -> Term vars -> Bool @@ -237,7 +239,7 @@ mutual _ => pure (term, gErased fc) pure (term, gnf env (embed ty)) unelabTy' umode nest env (Bind fc x b sc) - = do (sc', scty) <- unelabTy umode nest (b :: env) sc + = do (sc', scty) <- unelabTy umode nest (env :< b) sc case umode of NoSugar True => let x' = uniqueLocal vars x in