ScopedSnocList: WIP: trivial constructor substitutions

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

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

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

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,15 +55,15 @@ 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
 
 -- 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
 

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)

src/Idris/Doc/Display.idr

@@ -24,21 +24,21 @@ 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} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Defs -> ClosedTerm ->
               Core (Doc IdrisSyntax)
 displayTerm defs tm
-  = do ptm <- resugar [] !(normaliseHoles defs [] tm)
+  = do ptm <- resugar [<] !(normaliseHoles defs [<] tm)
        pure (pretty ptm)
 
 export

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)

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)

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

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