diff --git a/src/Core/Case/CaseBuilder.idr b/src/Core/Case/CaseBuilder.idr index fc4b42ee3a..5b6e5424f2 100644 --- a/src/Core/Case/CaseBuilder.idr +++ b/src/Core/Case/CaseBuilder.idr @@ -19,6 +19,7 @@ import Data.String import Data.Vect import Libraries.Data.List.LengthMatch import Libraries.Data.SortedSet +import Libraries.Data.SnocList.SizeOf import Decidable.Equality diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index 398db4571a..aaca20c392 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -15,6 +15,7 @@ import Data.String import Libraries.Data.NameMap import Libraries.Data.String.Extra +import Libraries.Data.SnocList.SizeOf import Libraries.Text.PrettyPrint.Prettyprinter %default covering @@ -77,7 +78,7 @@ conflict defs env nfty n | Nothing => pure False case (definition gdef, type gdef) of (DCon t arity _, dty) - => do Nothing <- conflictNF 0 nfty !(nf defs [] dty) + => do Nothing <- conflictNF 0 nfty !(nf defs [<] dty) | Just ms => pure $ conflictMatch ms pure True _ => pure False @@ -110,7 +111,7 @@ conflict defs env nfty n -- put posslbe = let x' = MN (show x) i in conflictNF (i + 1) t - !(sc defs (toClosure defaultOpts [] (Ref fc Bound x'))) + !(sc defs (toClosure defaultOpts [<] (Ref fc Bound x'))) conflictNF i nf (NApp _ (NRef Bound n) [<]) = do empty <- clearDefs defs pure (Just [(n, !(quote empty env nf))]) @@ -455,7 +456,7 @@ checkMatched cs ulhs where tryClauses : List Clause -> ClosedTerm -> Core (Maybe ClosedTerm) tryClauses [] ulhs - = do logTermNF "coverage" 10 "Nothing matches" [] ulhs + = do logTermNF "coverage" 10 "Nothing matches" [<] ulhs pure $ Just ulhs tryClauses (MkClause env lhs _ :: cs) ulhs = if !(clauseMatches env lhs ulhs) 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/LinearCheck.idr b/src/Core/LinearCheck.idr index 93fc2a82ce..8710ccc4e7 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -12,6 +12,7 @@ import Core.Value import Core.TT import Data.List +import Data.SnocList import Libraries.Data.SnocList.SizeOf @@ -20,29 +21,29 @@ import Libraries.Data.SnocList.SizeOf -- List of variable usages - we'll count the contents of specific variables -- when discharging binders, to ensure that linear names are only used once data Usage : SnocList Name -> Type where - Nil : Usage vars - (::) : Var vars -> Usage vars -> Usage vars + Lin : Usage vars + (:<) : Usage vars -> Var vars -> Usage vars Show (Usage vars) where show xs = "[" ++ showAll xs ++ "]" where showAll : Usage vs -> String - showAll [] = "" - showAll [el] = show el - showAll (x :: xs) = show x ++ ", " ++ show xs + showAll [<] = "" + showAll [ Usage vars -doneScope [] = [] -doneScope (MkVar First :: xs) = doneScope xs -doneScope (MkVar (Later p) :: xs) = MkVar p :: doneScope xs +doneScope [<] = [<] +doneScope (xs :< MkVar First) = doneScope xs +doneScope (xs :< MkVar (Later p)) = doneScope xs :< MkVar p (++) : Usage ns -> Usage ns -> Usage ns -(++) [] ys = ys -(++) (x :: xs) ys = x :: xs ++ ys +(++) sx Lin = sx +(++) sx (sy :< y) = (sx ++ sy) :< y count : Nat -> Usage ns -> Nat -count p [] = 0 -count p (v :: xs) +count p [<] = 0 +count p (xs :< v) = if p == varIdx v then 1 + count p xs else count p xs mutual @@ -196,12 +197,12 @@ mutual -- count the usage if we're in a linear context. If not, the usage doesn't -- matter used : RigCount -> Usage vars - used r = if isLinear r then [MkVar prf] else [] + used r = if isLinear r then [ eraseLinear env _ => env else env - (sc', sct, usedsc) <- lcheck rig erase (b' :: env') sc + (sc', sct, usedsc) <- lcheck rig erase (env' :< b') sc let used_in = count 0 usedsc holeFound <- if not erase && isLinear (multiplicity b) @@ -295,18 +296,18 @@ mutual else linear getZeroes : {vs : _} -> Env Term vs -> List (Var vs) - getZeroes [] = [] - getZeroes (b :: bs) + getZeroes [<] = [] + getZeroes (bs :< b) = if isErased (multiplicity b) then MkVar First :: map weaken (getZeroes bs) else map weaken (getZeroes bs) eraseLinear : Env Term vs -> Env Term vs - eraseLinear [] = [] - eraseLinear (b :: bs) + eraseLinear [<] = [<] + eraseLinear (bs :< b) = if isLinear (multiplicity b) - then setMultiplicity b erased :: eraseLinear bs - else b :: eraseLinear bs + then eraseLinear bs :< setMultiplicity b erased + else eraseLinear bs :< b checkUsageOK : Nat -> RigCount -> Core () checkUsageOK used r = when (isLinear r && used /= 1) @@ -351,7 +352,7 @@ mutual do when (not erase) $ needFunctionType f' gfty -- we don't do any linearity checking when `erase` is set -- so returning an empty usage is fine - pure (App fc f a, gErased fc, []) + pure (App fc f a, gErased fc, [<]) _ => needFunctionType f' gfty where @@ -386,14 +387,14 @@ mutual _ => throw (GenericMsg fc "Not a delayed type") lcheck rig erase env (PrimVal fc c) = do log "quantity" 15 "lcheck PrimVal" - pure (PrimVal fc c, gErased fc, []) + pure (PrimVal fc c, gErased fc, [<]) lcheck rig erase env (Erased fc i) = do log "quantity" 15 "lcheck Erased" - pure (Erased fc i, gErased fc, []) + pure (Erased fc i, gErased fc, [<]) lcheck rig erase env (TType fc u) -- Not universe checking here, just use the top of the hierarchy = do log "quantity" 15 "lcheck TType" - pure (TType fc u, gType fc (MN "top" 0), []) + pure (TType fc u, gType fc (MN "top" 0), [<]) lcheckBinder : {vars : _} -> {auto c : Ref Ctxt Defs} -> @@ -403,24 +404,24 @@ mutual Core (Binder (Term vars), Glued vars, Usage vars) lcheckBinder rig erase env (Lam fc c x ty) = do (tyv, tyt, _) <- lcheck erased erase env ty - pure (Lam fc c x tyv, tyt, []) + pure (Lam fc c x tyv, tyt, [<]) lcheckBinder rig erase env (Let fc rigc val ty) = do (tyv, tyt, _) <- lcheck erased erase env ty (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val pure (Let fc rigc valv tyv, tyt, vs) lcheckBinder rig erase env (Pi fc c x ty) = do (tyv, tyt, _) <- lcheck (rig |*| c) erase env ty - pure (Pi fc c x tyv, tyt, []) + pure (Pi fc c x tyv, tyt, [<]) lcheckBinder rig erase env (PVar fc c p ty) = do (tyv, tyt, _) <- lcheck erased erase env ty - pure (PVar fc c p tyv, tyt, []) + pure (PVar fc c p tyv, tyt, [<]) lcheckBinder rig erase env (PLet fc rigc val ty) = do (tyv, tyt, _) <- lcheck erased erase env ty (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val pure (PLet fc rigc valv tyv, tyt, vs) lcheckBinder rig erase env (PVTy fc c ty) = do (tyv, tyt, _) <- lcheck erased erase env ty - pure (PVTy fc c tyv, tyt, []) + pure (PVTy fc c tyv, tyt, [<]) discharge : {vars : _} -> Defs -> Env Term vars -> @@ -525,12 +526,12 @@ mutual checkEnvUsage : {vars : _} -> SizeOf done -> RigCount -> - Env Term vars -> Usage (done <>> vars) -> - List (Term (done <>> vars)) -> - Term (done <>> vars) -> Core () - checkEnvUsage s rig [] usage args tm = pure () - checkEnvUsage s rig {done} {vars = xs :< nm} (b :: env) usage args tm - = do let pos = mkVarChiply s + Env Term vars -> Usage (vars ++ done) -> + List (Term (vars ++ done)) -> + Term (vars ++ done) -> Core () + checkEnvUsage s rig [<] usage args tm = pure () + checkEnvUsage s rig {done} {vars = xs :< nm} (env :< b) usage args tm + = do let pos = mkVar s let used_in = count (varIdx pos) usage holeFound <- if isLinear (multiplicity b) @@ -543,7 +544,10 @@ mutual checkUsageOK (getLoc (binderType b)) used nm (isLocArg pos args) ((multiplicity b) |*| rig) - checkEnvUsage (s :< nm) rig env usage args tm + checkEnvUsage ([ (vs ** (Env Term vs, Term vs, Term vs)) -> Core (List (Name, ArgUsage)) @@ -646,7 +650,7 @@ mutual Name -> Int -> Def -> List (Term vars) -> Core (Term vars, Glued vars, Usage vars) expandMeta rig erase env n idx (PMDef _ [<] (STerm _ fn) _ _) args - = do tm <- substMeta (embed fn) args zero [] + = do tm <- substMeta (embed fn) args zero [<] lcheck rig erase env tm where substMeta : {drop, vs : _} -> @@ -654,7 +658,7 @@ mutual SizeOf drop -> SubstEnv drop vs -> Core (Term vs) substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) drop env - = substMeta sc as (suc drop) (a :: env) + = substMeta sc as (suc drop) (env :< a) substMeta (Bind bfc n (Let _ c val ty) sc) as drop env = substMeta (subst val sc) as drop env substMeta rhs [] drop env = pure (substs drop env rhs) @@ -691,19 +695,19 @@ mutual ++ " not a function type)")) lcheckMeta rig erase env fc n idx [] chk nty = do defs <- get Ctxt - pure (Meta fc n idx (reverse chk), glueBack defs env nty, []) + pure (Meta fc n idx (reverse chk), glueBack defs env nty, [<]) checkEnvUsage : {vars : _} -> {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> FC -> SizeOf done -> RigCount -> - Env Term vars -> Usage (done <>> vars) -> - Term (done <>> vars) -> + Env Term vars -> Usage (vars ++ done) -> + Term (vars ++ done) -> Core () -checkEnvUsage fc s rig [] usage tm = pure () -checkEnvUsage fc s rig {vars = xs :< nm} (b :: env) usage tm - = do let pos = mkVarChiply s +checkEnvUsage fc s rig [<] usage tm = pure () +checkEnvUsage fc s rig {vars = xs :< nm} (env :< b) usage tm + = do let pos = mkVar s let used_in = count (varIdx pos) usage holeFound <- if isLinear (multiplicity b) @@ -714,7 +718,10 @@ checkEnvUsage fc s rig {vars = xs :< nm} (b :: env) usage tm then 1 else used_in checkUsageOK used ((multiplicity b) |*| rig) - checkEnvUsage fc (s :< nm) rig env usage tm + checkEnvUsage fc ([ RigCount -> Core () checkUsageOK used r = when (isLinear r && used /= 1) 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.idr b/src/TTImp/Elab.idr index 87094e66b1..6ef47d708f 100644 --- a/src/TTImp/Elab.idr +++ b/src/TTImp/Elab.idr @@ -69,8 +69,8 @@ normaliseHoleTypes where updateType : Defs -> Int -> GlobalDef -> Core () updateType defs i def - = do ty' <- catch (tryNormaliseSizeLimit defs 10 [] (type def)) - (\err => normaliseHoles defs [] (type def)) + = do ty' <- catch (tryNormaliseSizeLimit defs 10 [<] (type def)) + (\err => normaliseHoles defs [<] (type def)) ignore $ addDef (Resolved i) ({ type := ty' } def) normaliseH : Defs -> Int -> Core () diff --git a/src/TTImp/Elab/Ambiguity.idr b/src/TTImp/Elab/Ambiguity.idr index 5798502d26..e4d066a763 100644 --- a/src/TTImp/Elab/Ambiguity.idr +++ b/src/TTImp/Elab/Ambiguity.idr @@ -221,7 +221,7 @@ mutual {vars : _} -> Defs -> NF vars -> NF [<] -> Core TypeMatch mightMatch defs target (NBind fc n (Pi _ _ _ _) sc) - = mightMatchD defs target !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + = mightMatchD defs target !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder))) mightMatch defs (NBind _ _ _ _) (NBind _ _ _ _) = pure Poly -- lambdas might match mightMatch defs (NTCon _ n t a args) (NTCon _ n' t' a' args') = if n == n' @@ -249,7 +249,7 @@ couldBeName : {auto c : Ref Ctxt Defs} -> couldBeName defs target n = case !(lookupTyExact n (gamma defs)) of Nothing => pure Poly -- could be a local name, don't rule it out - Just ty => mightMatchD defs target !(nf defs [] ty) + Just ty => mightMatchD defs target !(nf defs [<] ty) couldBeFn : {auto c : Ref Ctxt Defs} -> {vars : _} -> diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 88da7b3e9f..5cb28ab34e 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -18,6 +18,7 @@ import TTImp.Elab.Dot import TTImp.TTImp import Data.List +import Data.SnocList import Data.Maybe import Libraries.Data.WithDefault @@ -854,7 +855,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp = do tm <- Normalise.normalisePrims (`boundSafe` elabMode elabinfo) isIPrimVal (onLHS (elabMode elabinfo)) - prims n (fromList expargs) (fst res) env + prims n (cast {to=SnocList RawImp} expargs) (fst res) env pure (fromMaybe (fst res) tm, snd res) where diff --git a/src/TTImp/Elab/Binders.idr b/src/TTImp/Elab/Binders.idr index 372a1d7550..1e611fa315 100644 --- a/src/TTImp/Elab/Binders.idr +++ b/src/TTImp/Elab/Binders.idr @@ -70,7 +70,7 @@ checkPi rig elabinfo nest env fc rigf info n argTy retTy expTy (tyv, tyt) <- check pirig elabinfo nest env argTy (Just (gType fc tyu)) info' <- checkPiInfo rigf elabinfo nest env info (Just (gnf env tyv)) - let env' : Env Term (_ :< n) = Pi fc rigf info' tyv :: env + let env' : Env Term (_ :< n) = env :< Pi fc rigf info' tyv let nest' = weaken (dropName n nest) scu <- uniVar fc (scopev, scopet) <- @@ -115,7 +115,7 @@ inferLambda rig elabinfo nest env fc rigl info n argTy scope expTy u <- uniVar fc (tyv, tyt) <- check erased elabinfo nest env argTy (Just (gType fc u)) info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv)) - let env' : Env Term (_ :< n) = Lam fc rigb info' tyv :: env + let env' : Env Term (_ :< n) = env :< Lam fc rigb info' tyv let nest' = weaken (dropName n nest) (scopev, scopet) <- inScope fc env' (\e' => check {e=e'} rig elabinfo @@ -172,7 +172,7 @@ checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in) argTy (Just (gType fc u)) info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv)) let rigb = rigl `glb` c - let env' : Env Term (_ :< n) = Lam fc rigb info' tyv :: env + let env' : Env Term (_ :< n) = env :< Lam fc rigb info' tyv ignore $ convert fc elabinfo env (gnf env tyv) (gnf env pty) let nest' = weaken (dropName n nest) (scopev, scopet) <- @@ -248,7 +248,7 @@ checkLet rigc_in elabinfo nest env fc lhsFC rigl n nTy nVal scope expty {vars} elabinfo -- without preciseInf nest env nVal (Just (gnf env tyv)) pure (fst c, snd c, rigl |*| rigc)) - let env' : Env Term (_ :< n) = Lam fc rigb Explicit tyv :: env + let env' : Env Term (_ :< n) = env :< Lam fc rigb Explicit tyv let nest' = weaken (dropName n nest) expScope <- weakenExp env' expty (scopev, gscopet) <- diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 6005fc8b56..9a266ae11c 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -60,21 +60,21 @@ findLater {older} x (xs :< _) MkVar (Later p) toRig1 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs -toRig1 First (b :: bs) +toRig1 First (bs :< b) = if isErased (multiplicity b) - then setMultiplicity b linear :: bs - else b :: bs -toRig1 (Later p) (b :: bs) = b :: toRig1 p bs + then bs :< setMultiplicity b linear + else bs :< b +toRig1 (Later p) (bs :< b) = toRig1 p bs :< b toRig0 : {idx : Nat} -> (0 p : IsVar nm idx vs) -> Env Term vs -> Env Term vs -toRig0 First (b :: bs) = setMultiplicity b erased :: bs -toRig0 (Later p) (b :: bs) = b :: toRig0 p bs +toRig0 First (bs :< b) = bs :< setMultiplicity b erased +toRig0 (Later p) (bs :< b) = toRig0 p bs :< b -- When we abstract over the evironment, pi needs to be explicit explicitPi : Env Term vs -> Env Term vs -explicitPi (Pi fc c _ ty :: env) = Pi fc c Explicit ty :: explicitPi env -explicitPi (b :: env) = b :: explicitPi env -explicitPi [] = [] +explicitPi (env :< Pi fc c _ ty) = explicitPi env :< Pi fc c Explicit ty +explicitPi (env :< b) = explicitPi env :< b +explicitPi [<] = [<] allow : Maybe (Var vs) -> Env Term vs -> Env Term vs allow Nothing env = env @@ -90,11 +90,11 @@ findImpsIn : {vars : _} -> FC -> Env Term vars -> List (Name, Term vars) -> Term vars -> Core () findImpsIn fc env ns (Bind _ n b@(Pi _ _ Implicit ty) sc) - = findImpsIn fc (b :: env) + = findImpsIn fc (env :< b) ((n, weaken ty) :: map (\x => (fst x, weaken (snd x))) ns) sc findImpsIn fc env ns (Bind _ n b sc) - = findImpsIn fc (b :: env) + = findImpsIn fc (env :< b) (map (\x => (fst x, weaken (snd x))) ns) sc findImpsIn fc env ns ty @@ -121,7 +121,7 @@ extendNeeded b env needed findScrutinee : {vs : _} -> Env Term vs -> RawImp -> Maybe (Var vs) -findScrutinee {vs = _ :< n'} (b :: bs) (IVar loc' n) +findScrutinee {vs = _ :< n'} (bs :< b) (IVar loc' n) = if n' == n && not (isLet b) then Just (MkVar First) else do MkVar p <- findScrutinee bs (IVar loc' n) @@ -218,11 +218,11 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp -- If we can normalise the type without the result being excessively -- big do it. It's the depth of stuck applications - 10 is already -- pretty much unreadable! - casefnty <- normaliseSizeLimit defs 10 [] casefnty + casefnty <- normaliseSizeLimit defs 10 [<] casefnty (erasedargs, _) <- findErased casefnty logEnv "elab.case" 10 "Case env" env - logTermNF "elab.case" 2 ("Case function type: " ++ show casen) [] casefnty + logTermNF "elab.case" 2 ("Case function type: " ++ show casen) [<] casefnty traverse_ addToSave (keys (getMetas casefnty)) -- If we've had to add implicits to the case type (because there @@ -230,7 +230,7 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp -- way out is to throw an error and try again with the implicits -- actually bound! This is rather hacky, but a lot less fiddly than -- the alternative of fixing up the environment - when (not (isNil fullImps)) $ findImpsIn fc [] [] casefnty + when (not (isNil fullImps)) $ findImpsIn fc [<] [] casefnty cidx <- addDef casen ({ eraseArgs := erasedargs } (newDef fc casen (if isErased rigc then erased else top) [<] casefnty vis None)) @@ -266,7 +266,7 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp -- we come out again, so save them let olddelayed = delayedElab ust put UST ({ delayedElab := [] } ust) - processDecl [InCase] nest' [] (IDef fc casen alts') + processDecl [InCase] nest' [<] (IDef fc casen alts') -- If there's no duplication of the scrutinee in the block, -- flag it as inlinable. @@ -284,12 +284,12 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp pure (appTm, gnf env caseretty) where mkLocalEnv : Env Term vs -> Env Term vs - mkLocalEnv [] = [] - mkLocalEnv (b :: bs) + mkLocalEnv [<] = [<] + mkLocalEnv (bs :< b) = let b' = if isLinear (multiplicity b) then setMultiplicity b erased else b in - b' :: mkLocalEnv bs + mkLocalEnv bs :< b' -- Return the original name in the environment, and what it needs to be -- called in the case block. We need to mapping to build the ICaseLocal @@ -305,8 +305,8 @@ caseBlock {vars} rigc elabinfo fc nest env opts scr scrtm scrty caseRig alts exp -- the LHS of the case to be applied to. addEnv : {vs : _} -> Int -> Env Term vs -> List Name -> (List (Name, Name), List RawImp) - addEnv idx [] used = ([], []) - addEnv idx {vs = vs :< v} (b :: bs) used + addEnv idx [<] used = ([], []) + addEnv idx {vs = vs :< v} (bs :< b) used = let n = getBindName idx v used (ns, rest) = addEnv (idx + 1) bs (snd n :: used) ns' = n :: ns in @@ -434,20 +434,20 @@ checkCase rig elabinfo nest env fc opts scr scrty_in alts exp applyTo : Defs -> RawImp -> NF [<] -> Core RawImp applyTo defs ty (NBind fc _ (Pi _ _ Explicit _) sc) = applyTo defs (IApp fc ty (Implicit fc False)) - !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder))) applyTo defs ty (NBind _ x (Pi _ _ _ _) sc) = applyTo defs (INamedApp fc ty x (Implicit fc False)) - !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder))) applyTo defs ty _ = pure ty -- Get the name and type of the family the scrutinee is in getRetTy : Defs -> NF [<] -> Core (Maybe (Name, NF [<])) getRetTy defs (NBind fc _ (Pi _ _ _ _) sc) - = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + = getRetTy defs !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder))) getRetTy defs (NTCon _ n _ arity _) = do Just ty <- lookupTyExact n (gamma defs) | Nothing => pure Nothing - pure (Just (n, !(nf defs [] ty))) + pure (Just (n, !(nf defs [<] ty))) getRetTy _ _ = pure Nothing -- Guess a scrutinee type by looking at the alternatives, so that we @@ -460,7 +460,7 @@ checkCase rig elabinfo nest env fc opts scr scrty_in alts exp do defs <- get Ctxt [(_, (_, ty))] <- lookupTyName (mapNestedName nest n) (gamma defs) | _ => guessScrType xs - Just (tyn, tyty) <- getRetTy defs !(nf defs [] ty) + Just (tyn, tyty) <- getRetTy defs !(nf defs [<] ty) | _ => guessScrType xs applyTo defs (IVar fc tyn) tyty _ => guessScrType xs 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/Delayed.idr b/src/TTImp/Elab/Delayed.idr index 81e3d9d514..570c753629 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -15,7 +15,9 @@ import TTImp.Elab.Check import Libraries.Data.IntMap import Libraries.Data.NameMap + import Data.List +import Data.SnocList %default covering @@ -25,10 +27,10 @@ mkClosedElab : {vars : _} -> FC -> Env Term vars -> (Core (Term vars, Glued vars)) -> Core ClosedTerm -mkClosedElab fc [] elab +mkClosedElab fc [<] elab = do (tm, _) <- elab pure tm -mkClosedElab {vars = vars :< x} fc (b :: env) elab +mkClosedElab {vars = vars :< x} fc (env :< b) elab = mkClosedElab fc env (do (sc', _) <- elab let b' = newBinder b @@ -260,7 +262,7 @@ retryDelayed' errmode p acc (d@(_, i, hints, elab) :: ds) (PMDef (MkPMDefInfo NotHole True False) [<] (STerm 0 tm) (STerm 0 tm) []))) logTerm "elab.update" 5 ("Resolved delayed hole " ++ show i) tm - logTermNF "elab.update" 5 ("Resolved delayed hole NF " ++ show i) [] tm + logTermNF "elab.update" 5 ("Resolved delayed hole NF " ++ show i) [<] tm removeHole i retryDelayed' errmode True acc ds') (\err => do logC "elab" 5 $ do pure $ show errmode ++ ":Error in " ++ show !(getFullName (Resolved i)) diff --git a/src/TTImp/Elab/ImplicitBind.idr b/src/TTImp/Elab/ImplicitBind.idr index a8d3d9d28e..50df4ad67f 100644 --- a/src/TTImp/Elab/ImplicitBind.idr +++ b/src/TTImp/Elab/ImplicitBind.idr @@ -100,7 +100,7 @@ mkPatternHole {vars'} loc rig n topenv imode (Just expty_in) Env Term vs -> Term vs -> Thin newvars vs -> Maybe (Term newvars) bindInner env ty Refl = Just ty - bindInner {vs = _ :< x} (b :: env) ty (Drop p) + bindInner {vs = _ :< x} (env :< b) ty (Drop p) = bindInner env (Bind loc x b ty) p bindInner _ _ _ = Nothing @@ -285,7 +285,7 @@ normaliseHolesScope defs env (Bind fc n b sc) = pure $ Bind fc n b !(normaliseHolesScope defs -- use Lam because we don't want it reducing in the scope - (Lam fc (multiplicity b) Explicit (binderType b) :: env) sc) + (env :< Lam fc (multiplicity b) Explicit (binderType b)) sc) normaliseHolesScope defs env tm = normaliseHoles defs env tm export diff --git a/src/TTImp/Elab/Local.idr b/src/TTImp/Elab/Local.idr index 6887727332..8c7d5cc02b 100644 --- a/src/TTImp/Elab/Local.idr +++ b/src/TTImp/Elab/Local.idr @@ -83,11 +83,11 @@ localHelper {vars} nest env nestdecls_in func -- This is because, at the moment, we don't have any mechanism of -- ensuring the nested definition is used exactly once dropLinear : Env Term vs -> Env Term vs - dropLinear [] = [] - dropLinear (b :: bs) + dropLinear [<] = [<] + dropLinear (bs :< b) = if isLinear (multiplicity b) - then setMultiplicity b erased :: dropLinear bs - else b :: dropLinear bs + then dropLinear bs :< setMultiplicity b erased + else dropLinear bs :< b applyEnv : Int -> Name -> Core (Name, (Maybe Name, List (Var vars), FC -> NameType -> Term vars)) diff --git a/src/TTImp/Elab/Record.idr b/src/TTImp/Elab/Record.idr index b4a6fbd1b5..623eaa84e6 100644 --- a/src/TTImp/Elab/Record.idr +++ b/src/TTImp/Elab/Record.idr @@ -18,6 +18,7 @@ import TTImp.Elab.Delayed import TTImp.TTImp import Data.List +import Data.SnocList import Libraries.Data.SortedSet %default covering @@ -87,7 +88,7 @@ findFieldsAndTypeArgs : {auto c : Ref Ctxt Defs} -> Core $ Maybe (List (String, Maybe Name, Maybe Name), SortedSet Name) findFieldsAndTypeArgs defs con = case !(lookupTyExact con (gamma defs)) of - Just t => pure (Just !(getExpNames empty [] !(nf defs [] t))) + Just t => pure (Just !(getExpNames empty [] !(nf defs [<] t))) _ => pure Nothing where getExpNames : SortedSet Name -> @@ -100,8 +101,8 @@ findFieldsAndTypeArgs defs con _ => Just x nfty <- evalClosure defs ty let names = !(getNames defs nfty) `union` names - let expNames = (nameRoot x, imp, getRecordType [] nfty) :: expNames - getExpNames names expNames !(sc defs (toClosure defaultOpts [] (Ref fc Bound x))) + let expNames = (nameRoot x, imp, getRecordType [<] nfty) :: expNames + getExpNames names expNames !(sc defs (toClosure defaultOpts [<] (Ref fc Bound x))) getExpNames names expNames nfty = pure (reverse expNames, (!(getNames defs nfty) `union` names)) genFieldName : {auto u : Ref UST UState} -> diff --git a/src/TTImp/Elab/Rewrite.idr b/src/TTImp/Elab/Rewrite.idr index 97b71e9139..67d06cd5b0 100644 --- a/src/TTImp/Elab/Rewrite.idr +++ b/src/TTImp/Elab/Rewrite.idr @@ -18,6 +18,9 @@ import TTImp.Elab.Check import TTImp.Elab.Delayed import TTImp.TTImp +import Data.SnocList +import Libraries.Data.SnocList.SizeOf + %default covering -- TODO: Later, we'll get the name of the lemma from the type, if it's one @@ -135,7 +138,7 @@ checkRewrite {vars} rigc elabinfo nest env ifc rule tm (Just expected) let pbind = Let vfc erased lemma.pred lemma.predTy let rbind = Let vfc erased (weaken rulev) (weaken rulet) - let env' = rbind :: pbind :: env + let env' = env :< pbind :< rbind -- Nothing we do in this last part will affect the EState, -- we're only doing the application this way to make sure the @@ -143,7 +146,7 @@ checkRewrite {vars} rigc elabinfo nest env ifc rule tm (Just expected) -- we still need the right type for the EState, so weaken it once -- for each of the let bindings above. (rwtm, grwty) <- - inScope vfc (pbind :: env) $ \e' => + inScope vfc (env :< pbind) $ \e' => inScope {e=e'} vfc env' $ \e'' => let offset = mkSizeOf [ Core (Name, RawImp) unelabType (n, _, ty) - = pure (n, map rawName !(unelabUniqueBinders [] ty)) + = pure (n, map rawName !(unelabUniqueBinders [<] ty)) elabCon defs "GetInfo" [ @@ -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/ProcessData.idr b/src/TTImp/ProcessData.idr index a93ef5fa12..5b4a6f7aad 100644 --- a/src/TTImp/ProcessData.idr +++ b/src/TTImp/ProcessData.idr @@ -23,6 +23,7 @@ import TTImp.TTImp import Data.DPair import Data.List +import Data.SnocList import Libraries.Data.NameMap import Libraries.Data.WithDefault @@ -112,7 +113,7 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc _ cn_in ty_raw) -- Check 'ty' returns something in the right family checkFamily fc cn tn env !(nf defs env ty) let fullty = abstractEnvType fc env ty - logTermNF "declare.data.constructor" 5 ("Constructor " ++ show cn) [] fullty + logTermNF "declare.data.constructor" 5 ("Constructor " ++ show cn) [<] fullty traverse_ addToSave (keys (getMetas ty)) addToSave cn @@ -123,26 +124,27 @@ checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc _ cn_in ty_raw) addHashWithNames fullty log "module.hash" 15 "Adding hash for data constructor: \{show cn}" _ => pure () - pure (MkCon fc cn !(getArity defs [] fullty) fullty) + pure (MkCon fc cn !(getArity defs [<] fullty) fullty) -- Get the indices of the constructor type (with non-constructor parts erased) getIndexPats : {auto c : Ref Ctxt Defs} -> ClosedTerm -> Core (List (NF [<])) getIndexPats tm = do defs <- get Ctxt - tmnf <- nf defs [] tm + tmnf <- nf defs [<] tm ret <- getRetType defs tmnf getPats defs ret where getRetType : Defs -> NF [<] -> Core (NF [<]) getRetType defs (NBind fc _ (Pi _ _ _ _) sc) - = do sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + = do sc' <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) getRetType defs sc' getRetType defs t = pure t getPats : Defs -> NF [<] -> Core (List (NF [<])) getPats defs (NTCon fc _ _ _ args) - = traverse (evalClosure defs . snd) (toList args) + = do args' <- traverse (evalClosure defs . snd) args + pure (cast args') getPats defs _ = pure [] -- Can't happen if we defined the type successfully! getDetags : {auto c : Ref Ctxt Defs} -> @@ -156,10 +158,10 @@ getDetags fc tys xs => pure $ Just xs where mutual - disjointArgs : List (NF [<]) -> List (NF [<]) -> Core Bool - disjointArgs [] _ = pure False - disjointArgs _ [] = pure False - disjointArgs (a :: args) (a' :: args') + disjointArgs : SnocList (NF [<]) -> SnocList (NF [<]) -> Core Bool + disjointArgs [<] _ = pure False + disjointArgs _ [<] = pure False + disjointArgs (args :< a) (args' :< a') = if !(disjoint a a') then pure True else disjointArgs args args' @@ -169,15 +171,15 @@ getDetags fc tys = if t /= t' then pure True else do defs <- get Ctxt - argsnf <- traverse (evalClosure defs . snd) (toList args) - args'nf <- traverse (evalClosure defs . snd) (toList args') + argsnf <- traverse (evalClosure defs . snd) args + args'nf <- traverse (evalClosure defs . snd) args' disjointArgs argsnf args'nf disjoint (NTCon _ n _ _ args) (NDCon _ n' _ _ args') = if n /= n' then pure True else do defs <- get Ctxt - argsnf <- traverse (evalClosure defs . snd) (toList args) - args'nf <- traverse (evalClosure defs . snd) (toList args') + argsnf <- traverse (evalClosure defs . snd) args + args'nf <- traverse (evalClosure defs . snd) args' disjointArgs argsnf args'nf disjoint (NPrimVal _ c) (NPrimVal _ c') = pure (c /= c') disjoint _ _ = pure False @@ -213,19 +215,19 @@ getRelevantArg : {auto c : Ref Ctxt Defs} -> Core (Maybe (Bool, Nat)) getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc) = branchZero (getRelevantArg defs (1 + i) rel world - !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder)))) + !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)))) (case !(evalClosure defs val) of -- %World is never inspected, so might as well be deleted from data types, -- although it needs care when compiling to ensure that the function that -- returns the IO/%World type isn't erased (NPrimVal _ $ PrT WorldType) => getRelevantArg defs (1 + i) rel False - !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder))) _ => -- if we haven't found a relevant argument yet, make -- a note of this one and keep going. Otherwise, we -- have more than one, so give up. - maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + maybe (do sc' <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) getRelevantArg defs (1 + i) (Just i) False sc') (const (pure Nothing)) rel) @@ -240,7 +242,7 @@ findNewtype : {auto c : Ref Ctxt Defs} -> List Constructor -> Core () findNewtype [con] = do defs <- get Ctxt - Just arg <- getRelevantArg defs 0 Nothing True !(nf defs [] (type con)) + Just arg <- getRelevantArg defs 0 Nothing True !(nf defs [<] (type con)) | Nothing => pure () updateDef (name con) $ \case @@ -279,7 +281,7 @@ shaped : {auto c : Ref Ctxt Defs} -> shaped as [] = pure Nothing shaped as (c :: cs) = do defs <- get Ctxt - if as !(normalise defs [] (type c)) + if as !(normalise defs [<] (type c)) then pure (Just (name c)) else shaped as cs @@ -332,7 +334,7 @@ calcEnum fc cs isNullary : Constructor -> Core Bool isNullary c = do defs <- get Ctxt - pure $ hasArgs 0 !(normalise defs [] (type c)) + pure $ hasArgs 0 !(normalise defs [<] (type c)) calcRecord : {auto c : Ref Ctxt Defs} -> FC -> List Constructor -> Core Bool @@ -405,7 +407,7 @@ processData : {vars : _} -> ImpData -> Core () processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw) = do n <- inCurrentNS n_in - ty_raw <- bindTypeNames fc [] (toList vars) ty_raw + ty_raw <- bindTypeNames fc [] (cast {to=List _} vars) ty_raw defs <- get Ctxt -- Check 'n' is undefined @@ -419,10 +421,10 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpLater dfc n_in ty_raw) (IBindHere fc (PI erased) ty_raw) (Just (gType dfc u)) let fullty = abstractEnvType dfc env ty - logTermNF "declare.data" 5 ("data " ++ show n) [] fullty + logTermNF "declare.data" 5 ("data " ++ show n) [<] fullty checkIsType fc n env !(nf defs env ty) - arity <- getArity defs [] fullty + arity <- getArity defs [<] fullty -- Add the type constructor as a placeholder tidx <- addDef n (newDef fc n linear vars fullty def_vis @@ -448,7 +450,7 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o defs <- get Ctxt mmetasfullty <- flip traverseOpt mty_raw $ \ ty_raw => do - ty_raw <- bindTypeNames fc [] (toList vars) ty_raw + ty_raw <- bindTypeNames fc [] (cast {to=List _} vars) ty_raw u <- uniVar fc (ty, _) <- @@ -484,16 +486,16 @@ processData {vars} eopts nest env fc def_vis mbtot (MkImpData dfc n_in mty_raw o TCon _ _ _ _ _ mw [] _ => case mfullty of Nothing => pure (mw, vis, type ndef) Just fullty => - do ok <- convert defs [] fullty (type ndef) + do ok <- convert defs [<] fullty (type ndef) if ok then pure (mw, vis, fullty) - else do logTermNF "declare.data" 1 "Previous" [] (type ndef) - logTermNF "declare.data" 1 "Now" [] fullty + else do logTermNF "declare.data" 1 "Previous" [<] (type ndef) + logTermNF "declare.data" 1 "Now" [<] fullty throw (AlreadyDefined fc n) _ => throw (AlreadyDefined fc n) - logTermNF "declare.data" 5 ("data " ++ show n) [] fullty + logTermNF "declare.data" 5 ("data " ++ show n) [<] fullty - arity <- getArity defs [] fullty + arity <- getArity defs [<] fullty -- Add the type constructor as a placeholder while checking -- data constructors diff --git a/src/TTImp/ProcessFnOpt.idr b/src/TTImp/ProcessFnOpt.idr index 384293091b..0cfcf4e02c 100644 --- a/src/TTImp/ProcessFnOpt.idr +++ b/src/TTImp/ProcessFnOpt.idr @@ -10,9 +10,11 @@ import TTImp.TTImp import Libraries.Data.NameMap +import Data.SnocList + getRetTy : Defs -> NF [<] -> Core Name getRetTy defs (NBind fc _ (Pi _ _ _ _) sc) - = getRetTy defs !(sc defs (toClosure defaultOpts [] (Erased fc Placeholder))) + = getRetTy defs !(sc defs (toClosure defaultOpts [<] (Erased fc Placeholder))) getRetTy defs (NTCon _ n _ _ _) = pure n getRetTy defs ty = throw (GenericMsg (getLoc ty) @@ -42,7 +44,7 @@ processFnOpt fc True ndef (Hint d) = do defs <- get Ctxt Just ty <- lookupTyExact ndef (gamma defs) | Nothing => undefinedName fc ndef - target <- getRetTy defs !(nf defs [] ty) + target <- getRetTy defs !(nf defs [<] ty) addHintFor fc target ndef d False processFnOpt fc _ ndef (Hint d) = do logC "elab" 5 $ do pure $ "Adding local hint " ++ show !(toFullNames ndef) @@ -69,7 +71,7 @@ processFnOpt fc _ ndef (SpecArgs ns) = do defs <- get Ctxt Just gdef <- lookupCtxtExact ndef (gamma defs) | Nothing => undefinedName fc ndef - nty <- nf defs [] (type gdef) + nty <- nf defs [<] (type gdef) ps <- getNamePos 0 nty ddeps <- collectDDeps nty specs <- collectSpec [] ddeps ps nty @@ -89,10 +91,10 @@ processFnOpt fc _ ndef (SpecArgs ns) collectDDeps (NBind tfc x (Pi _ _ _ nty) sc) = do defs <- get Ctxt empty <- clearDefs defs - sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x)) + sc' <- sc defs (toClosure defaultOpts [<] (Ref tfc Bound x)) if x `elem` ns then collectDDeps sc' - else do aty <- quote empty [] nty + else do aty <- quote empty [<] nty -- Get names depended on by nty let deps = keys (getRefs (UN Underscore) aty) rest <- collectDDeps sc' @@ -113,12 +115,12 @@ processFnOpt fc _ ndef (SpecArgs ns) getDeps inparam (NBind _ x (Pi _ _ _ pty) sc) ns = do defs <- get Ctxt ns' <- getDeps inparam !(evalClosure defs pty) ns - sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + sc' <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) getDeps inparam sc' ns' getDeps inparam (NBind _ x b sc) ns = do defs <- get Ctxt ns' <- getDeps False !(evalClosure defs (binderType b)) ns - sc' <- sc defs (toClosure defaultOpts [] (Erased fc Placeholder)) + sc' <- sc defs (toClosure defaultOpts [<] (Erased fc Placeholder)) getDeps False sc' ns getDeps inparam (NApp _ (NRef Bound n) args) ns = do defs <- get Ctxt @@ -159,7 +161,7 @@ processFnOpt fc _ ndef (SpecArgs ns) collectSpec acc ddeps ps (NBind tfc x (Pi _ _ _ nty) sc) = do defs <- get Ctxt empty <- clearDefs defs - sc' <- sc defs (toClosure defaultOpts [] (Ref tfc Bound x)) + sc' <- sc defs (toClosure defaultOpts [<] (Ref tfc Bound x)) if x `elem` ns then do deps <- getDeps True !(evalClosure defs nty) NameMap.empty -- Get names depended on by nty @@ -177,6 +179,6 @@ processFnOpt fc _ ndef (SpecArgs ns) getNamePos : Nat -> NF [<] -> Core (List (Name, Nat)) getNamePos i (NBind tfc x (Pi _ _ _ _) sc) = do defs <- get Ctxt - ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [] (Erased tfc Placeholder))) + ns' <- getNamePos (1 + i) !(sc defs (toClosure defaultOpts [<] (Erased tfc Placeholder))) pure ((x, i) :: ns') getNamePos _ _ = pure [] diff --git a/src/TTImp/Reflect.idr b/src/TTImp/Reflect.idr index cf9affbc31..aba6c79171 100644 --- a/src/TTImp/Reflect.idr +++ b/src/TTImp/Reflect.idr @@ -10,6 +10,8 @@ import Core.Value import TTImp.TTImp import Libraries.Data.WithDefault +import Data.SnocList + %default covering export 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