erase arts in lifted where functions

src/Lib/LiftWhere.newt

@@ -8,22 +8,23 @@ import Lib.Ref2
 import Data.SortedMap
 import Data.IORef
 
--- track depth and whether we need to replace Bnd with a top level call
+-- track quantity, depth, and whether we need to replace Bnd with a top level call.
+-- We _could_ keep track of the support and elide that as well.
 LiftEnv : U
-LiftEnv = List (Maybe (QName × Nat))
+LiftEnv = List (Quant × Maybe (QName × List Quant))
 
 liftWhereTm : {{Ref2 Defs St}} → QName → LiftEnv → Tm → M Tm
 liftWhereTm name env (Lam fc nm icit quant t) =
-  Lam fc nm icit quant <$> liftWhereTm name (Nothing :: env) t
+  Lam fc nm icit quant <$> liftWhereTm name ((quant, Nothing) :: env) t
 liftWhereTm name env (App fc t u) =
   App fc <$> liftWhereTm name env t <*> liftWhereTm name env u
 liftWhereTm name env (Pi fc nm icit quant t u) = do
   t <- liftWhereTm name env t
-  u <- liftWhereTm name (Nothing :: env) u
+  u <- liftWhereTm name ((quant, Nothing) :: env) u
   pure $ Pi fc nm icit quant t u
 liftWhereTm name env (Let fc nm v sc) = do
   v <- liftWhereTm name env v
-  sc <- liftWhereTm name (Nothing :: env) sc
+  sc <- liftWhereTm name ((Many, Nothing) :: env) sc
   pure $ Let fc nm v sc
 liftWhereTm name env tm@(Case fc t alts) = do
   t <- liftWhereTm name env t
@@ -35,16 +36,20 @@ liftWhereTm name env tm@(Case fc t alts) = do
     liftWhereAlt (CaseDefault tm) = CaseDefault <$> liftWhereTm name env tm
     liftWhereAlt (CaseLit l tm) = CaseLit l <$> liftWhereTm name env tm
     liftWhereAlt (CaseCons qn args tm) =
-      CaseCons qn args <$> liftWhereTm name (map (const Nothing) args ++ env) tm
+      -- TODO - can we pull quantities off of these arguments?
+      -- We should switch to SnocList first, the args are backwards here
+      CaseCons qn args <$> liftWhereTm name ((map (const (Many, Nothing)) args) ++ env) tm
 -- This is where the magic happens
 liftWhereTm name env (LetRec fc nm ty t u) = do
-  let l = length env
+  -- let l = length env
   qn <- getName name nm
-  let env' = (Just (qn, S l) :: env)
+  -- I'll erase this one, since we're replacing all of the usages
+  let qs = Zero :: map fst env
+  let env' = ((Zero, Just (qn, qs)) :: env)
   -- environment should subst this function (see next case)
   t' <- liftWhereTm qn env' t
   -- TODO we could have subst in this var and dropped the extra argument
-  modifyRef Defs (updateMap qn (Fn $ wrapLam (S l) t'))
+  modifyRef Defs (updateMap qn (Fn $ wrapLam qs t'))
 
   -- The rest
   u' <- liftWhereTm qn env' u
@@ -58,19 +63,18 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
       let (Just _) = lookupMap qn' top | _ => pure qn'
       getName qn (ext ++ "'")
 
-    wrapLam : Nat → Tm → Tm
-    wrapLam Z tm = tm
-    -- REVIEW We've already erased, hopefully we don't need quantity
-    wrapLam (S k) tm = Lam fc "_" Explicit Many $ wrapLam k tm
+    wrapLam : List Quant → Tm → Tm
+    wrapLam Nil tm = tm
+    wrapLam (q :: qs) tm = wrapLam qs $ Lam fc "_" Explicit q tm
 
 -- And where it lands
 liftWhereTm name env tm@(Bnd fc k) = case getAt (cast k) env of
-  Just (Just (qn, v)) => pure $ apply (length' env) (cast v) (Ref fc qn)
+  Just (_, Just (qn, v)) => pure $ apply (length' env) (length' v) (Ref fc qn)
   _ => pure tm
   where
     apply : Int → Int → Tm → Tm
     apply l 0 tm = tm
-    -- (l - k) is like lvl2ix, but witih k one bigger
+    -- (l - k) is like lvl2ix, but with k one bigger
     apply l k tm = App fc (apply l (k - 1) tm) (Bnd fc (l - k))
 liftWhereTm name env tm = pure tm
 
@@ -78,7 +82,6 @@ liftWhereFn : {{Ref2 Defs St}} → QName × Def → M Unit
 liftWhereFn (name, Fn tm) = do
   tm' <- liftWhereTm name Nil tm
   modifyRef Defs $ updateMap name (Fn tm')
-  -- updateDef name fc type (Fn tm')
 liftWhereFn _ = pure MkUnit
 
 liftWhere : {{Ref2 Defs St}} → M Unit