[ refactor ] change constructor argument representation from Scope to List Name

This refactor changes the representation of constructor arguments throughout the compiler from `Scope` to `List Name`. This simplifies the API and reduces complexity in handling variable indices.

Key changes:
- Updated `MkConAlt` and related types to use `List Name` instead of `Scope` for constructor arguments
- Modified variable binding and weakening operations to work with list-based arguments
- Adjusted pattern matching and case analysis code throughout the compiler
- Added new helper functions for list-based variable operations

The change affects multiple compiler modules including ANF, LambdaLift, CaseOpts, and optimization passes, ensuring consistent handling of constructor arguments across the compilation pipeline.

Author: GulinSS

src/Compiler/ANF.idr

@@ -194,12 +194,12 @@ mlet fc val sc
 
 bindAsFresh :
   {auto v : Ref Next Int} ->
-  (args : Scope) -> AVars vars' ->
-  Core (List Int, AVars (vars' ++ args))
-bindAsFresh [<] vs = pure ([], vs)
-bindAsFresh (ns :< n) vs
+  (args : List Name) -> AVars vars' ->
+  Core (List Int, AVars (Scope.ext vars' args))
+bindAsFresh [] vs = pure ([], vs)
+bindAsFresh (n :: ns) vs
     = do i <- nextVar
-         bimap (i ::) (:< i) <$> bindAsFresh ns vs
+         mapFst (i ::) <$> bindAsFresh ns (vs :< i)
 
 mutual
   anfArgs : {auto v : Ref Next Int} ->
@@ -265,11 +265,11 @@ toANF : LiftedDef -> Core ANFDef
 toANF (MkLFun args scope sc)
     = do v <- newRef Next (the Int 0)
          (iargs, vsNil) <- bindAsFresh args AVars.empty
-         let vs : AVars args
-           := rewrite sym $ appendLinLeftNeutral args in
-              vsNil
-         (iargs', vs) <- bindAsFresh scope vs
-         sc' <- anf vs sc
+         (iargs', vs) <- bindAsFresh (toList scope) vsNil
+         sc' <- anf vs $
+            do rewrite fishAsSnocAppend (cast args) (toList scope)
+               rewrite castToList scope
+               sc
          pure $ MkAFun (iargs ++ iargs') sc'
 toANF (MkLCon t a ns) = pure $ MkACon t a ns
 toANF (MkLForeign ccs fargs t) = pure $ MkAForeign ccs fargs t

src/Compiler/CaseOpts.idr

@@ -42,26 +42,26 @@ shiftUnder : {args : _} ->
 shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
 shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
 
-shiftVar : {inner : Scope} -> {args : Scope} ->
-           NVar n ((vars ++ args :< x) ++ inner) ->
-           NVar n ((vars :< x ++ args) ++ inner)
+shiftVar : {inner : Scope} -> {args : List Name} ->
+           NVar n ((vars <>< args :< x) ++ inner) ->
+           NVar n ((vars :< x <>< args) ++ inner)
 shiftVar nvar
   = let inn = mkSizeOf inner in
     case locateNVar inn nvar of
-      Left (MkNVar p) => weakenNs inn (shiftUnderNs (mkSizeOf args) p)
+      Left (MkNVar p) => weakenNs inn (shiftUndersN (mkSizeOf _) p)
       Right nvar => embed nvar
 
 mutual
   shiftBinder : {inner, args : _} ->
                 (new : Name) ->
-                CExp (((vars ++ args) :< old) ++ inner) ->
-                CExp ((vars :< new ++ args) ++ inner)
+                CExp (((vars <>< args) :< old) ++ inner) ->
+                CExp ((vars :< new <>< args) ++ inner)
   shiftBinder new (CLocal fc p)
       = case shiftVar (MkNVar p) of
              MkNVar p' => CLocal fc (renameVar p')
     where
-      renameVar : IsVar x i ((vars :< old ++ args) ++ local) ->
-                  IsVar x i ((vars :< new ++ args) ++ local)
+      renameVar : IsVar x i ((vars :< old <>< args) ++ local) ->
+                  IsVar x i ((vars :< new <>< args) ++ local)
       renameVar = believe_me -- it's the same index, so just the identity at run time
   shiftBinder new (CRef fc n) = CRef fc n
   shiftBinder {inner} new (CLam fc n sc)
@@ -92,27 +92,27 @@ mutual
 
   shiftBinderConAlt : {inner, args : _} ->
                 (new : Name) ->
-                CConAlt (((vars ++ args) :< old) ++ inner) ->
-                CConAlt ((vars :< new ++ args) ++ inner)
+                CConAlt (((vars <>< args) :< old) ++ inner) ->
+                CConAlt ((vars :< new <>< args) ++ inner)
   shiftBinderConAlt new (MkConAlt n ci t args' sc)
-      = let sc' : CExp (((vars ++ args) :< old) ++ (inner ++ args'))
-                = (rewrite appendAssociative ((vars ++ args) :< old) inner args' in sc) in
+      = let sc' : CExp (((vars <>< args) :< old) ++ (inner <>< args'))
+                = rewrite sym $ snocAppendFishAssociative (vars <>< args :< old) inner args' in sc in
         MkConAlt n ci t args' $
-               rewrite sym $ appendAssociative (vars :< new ++ args) inner args' in
+               rewrite snocAppendFishAssociative (vars :< new <>< args) inner args' in
                shiftBinder new sc'
 
   shiftBinderConstAlt : {inner, args : _} ->
                 (new : Name) ->
-                CConstAlt (((vars ++ args) :< old) ++ inner) ->
-                CConstAlt ((vars :< new ++ args) ++ inner)
+                CConstAlt (((vars <>< args) :< old) ++ inner) ->
+                CConstAlt ((vars :< new <>< args) ++ inner)
   shiftBinderConstAlt new (MkConstAlt c sc) = MkConstAlt c $ shiftBinder new sc
 
 -- If there's a lambda inside a case, move the variable so that it's bound
 -- outside the case block so that we can bind it just once outside the block
 liftOutLambda : {args : _} ->
                 (new : Name) ->
-                CExp (Scope.bind (Scope.addInner vars args) old) ->
-                CExp (Scope.addInner (Scope.bind vars new) args)
+                CExp (Scope.bind (Scope.ext vars args) old) ->
+                CExp (Scope.ext (Scope.bind vars new) args)
 liftOutLambda = shiftBinder {inner = Scope.empty}
 
 -- If all the alternatives start with a lambda, we can have a single lambda
@@ -133,7 +133,7 @@ tryLiftOutConst : (new : Name) ->
 tryLiftOutConst new [] = Just []
 tryLiftOutConst new (MkConstAlt c (CLam fc x sc) :: as)
     = do as' <- tryLiftOutConst new as
-         let sc' = liftOutLambda {args = [<]} new sc
+         let sc' = liftOutLambda {args = []} new sc
          pure (MkConstAlt c sc' :: as')
 tryLiftOutConst _ _ = Nothing
 
@@ -142,7 +142,7 @@ tryLiftDef : (new : Name) ->
              Maybe (Maybe (CExp (Scope.bind vars new)))
 tryLiftDef new Nothing = Just Nothing
 tryLiftDef new (Just (CLam fc x sc))
-   = let sc' = liftOutLambda {args = [<]} new sc in
+   = let sc' = liftOutLambda {args = []} new sc in
          pure (Just sc')
 tryLiftDef _ _ = Nothing
 
@@ -318,8 +318,8 @@ doCaseOfCase fc x xalts xdef alts def
     updateAlt (MkConAlt n ci t args sc)
         = MkConAlt n ci t args $
               CConCase fc sc
-                       (map (weakenNs (mkSizeOf args)) alts)
-                       (map (weakenNs (mkSizeOf args)) def)
+                       (map (weakensN (mkSizeOf args)) alts)
+                       (map (weakensN (mkSizeOf args)) def)
 
     updateDef : CExp vars -> CExp vars
     updateDef sc = CConCase fc sc alts def

src/Compiler/Common.idr

@@ -356,7 +356,7 @@ getCompileDataWith exports doLazyAnnots phase_in tm_in
                               traverse (lambdaLift doLazyAnnots) cseDefs
                          else pure []
 
-         let lifted = (mainname, MkLFun Scope.empty Scope.empty liftedtm) ::
+         let lifted = (mainname, MkLFun [] Scope.empty liftedtm) ::
                       (ldefs ++ concat lifted_in)
 
          anf <- if phase >= ANF

src/Compiler/CompileExpr.idr

@@ -229,7 +229,7 @@ mutual
            Just gdef <- lookupCtxtExact x (gamma defs)
                 | Nothing => -- primitive type match
                      do xn <- getFullName x
-                        pure $ MkConAlt xn TYCON Nothing (cast args) !(toCExpTree n (rewrite sym $ fishAsSnocAppend vars args in sc))
+                        pure $ MkConAlt xn TYCON Nothing (cast args) !(toCExpTree n sc)
                                   :: !(conCases n ns)
            case (definition gdef) of
                 DCon _ arity (Just pos) => conCases n ns -- skip it
@@ -240,8 +240,8 @@ mutual
                         sc' <- toCExpTree n sc
                         ns' <- conCases n ns
                         if dcon (definition gdef)
-                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) args' (shrinkCExp subList sc') :: ns'
-                           else pure $ MkConAlt xn !(dconFlag xn) Nothing args' (shrinkCExp subList sc') :: ns'
+                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) (cast args') (rewrite sym $ snocAppendAsFish vars args' in shrinkCExp subList sc') :: ns'
+                           else pure $ MkConAlt xn !(dconFlag xn) Nothing (cast args') (rewrite sym $ snocAppendAsFish vars args' in shrinkCExp subList sc') :: ns'
     where
       dcon : Def -> Bool
       dcon (DCon {}) = True

src/Compiler/Inline.idr

@@ -130,7 +130,7 @@ mutual
   usedCon : {free : _} ->
             {idx : Nat} -> (0 p : IsVar n idx free) -> CConAlt free -> Int
   usedCon n (MkConAlt _ _ _ args sc)
-      = let MkVar n' = weakenNs (mkSizeOf args) (MkVar n) in
+      = let MkVar n' = weakensN (mkSizeOf args) (MkVar n) in
             used n' sc
 
   usedConst : {free : _} ->
@@ -306,9 +306,13 @@ mutual
             FC -> List Name -> EEnv free vars -> Stack free -> CConAlt (Scope.addInner free vars) ->
             Core (CConAlt free)
   evalAlt {free} {vars} fc rec env stk (MkConAlt n ci t args sc)
-      = do (bs, env') <- extendLoc fc env args
-           scEval <- eval rec env' stk (rewrite appendAssociative free vars args in sc)
-           pure $ MkConAlt n ci t args (refsToLocals bs scEval)
+      = do (bs, env') <- extendLoc fc env (cast args)
+           scEval <- eval rec env' stk $
+                do rewrite appendAssociative free vars (cast args)
+                   rewrite sym $ fishAsSnocAppend (free ++ vars) (args)
+                   sc
+           let sc'' = rewrite snocAppendFishAssociative free Scope.empty args in refsToLocals bs scEval
+           pure $ MkConAlt n ci t args sc''
 
   evalConstAlt : {vars, free : _} ->
                  {auto c : Ref Ctxt Defs} ->
@@ -335,10 +339,7 @@ mutual
                      Just m =>
                          do let env' = extend env (toList args') args m
                             pure $ Just !(eval rec env' stk
-                                    (do rewrite sym $ snocAppendFishAssociative free vars (toList args')
-                                        rewrite sym $ snocAppendAsFish (free ++ vars) args'
-                                        sc
-                                    ))
+                                    (rewrite sym $ snocAppendFishAssociative free vars args' in sc))
            else pickAlt rec env stk con alts def
     where
       matches : Name -> Maybe Int -> Name -> Maybe Int -> Bool

src/Compiler/LambdaLift.idr

@@ -194,8 +194,7 @@ mutual
        ||| @ body is the expression that is evaluated as the consequence of
        |||   this branch matching.
        MkLConAlt : (n : Name) -> (info : ConInfo) -> (tag : Maybe Int) ->
-                   -- TODO should args be a List?
-                   (args : Scope) -> (body : Lifted (Scope.addInner vars args)) ->
+                   (args : List Name) -> (body : Lifted (Scope.ext vars args)) ->
                    LiftedConAlt vars
 
   ||| A branch of an "LConst" (constant expression) case statement.
@@ -232,8 +231,8 @@ data LiftedDef : Type where
      -- (Sorry for the awkward API - it's to do with how the indices are
      -- arranged for the variables, and it could be expensive to reshuffle them!
      -- See Compiler.ANF for an example of how they get resolved to names)
-     MkLFun : (args : Scope) -> (scope : Scope) ->
-              (body : Lifted (Scope.addInner args scope)) -> LiftedDef
+     MkLFun : (args : List Name) -> (scope : Scope) ->
+              (body : Lifted (Scope.addInner (cast args) scope)) -> LiftedDef
 
      ||| Constructs a definition of a constructor for a compound data type.
      |||
@@ -454,7 +453,7 @@ usedVars used (LConCase fc sc alts def) =
     usedConAlt : {default Nothing lazy : Maybe LazyReason} ->
                   Used vars -> LiftedConAlt vars -> Used vars
     usedConAlt used (MkLConAlt n ci tag args sc) =
-      contractUsedMany {remove=args} (usedVars (weakenUsed used) sc)
+      contractUsedManyFish {remove=args} (usedVars (weakenUsedFish used) sc)
 
 usedVars used (LConstCase fc sc alts def) =
     let defUsed = maybe used (usedVars used {vars}) def
@@ -553,7 +552,7 @@ dropUnused inn unused (LConstCase fc sc alts def) =
       LConstCase fc (dropUnused inn unused sc) alts' (map (dropUnused inn unused) def)
 
 dropConCase inn unused (MkLConAlt n ci t args sc) =
-  MkLConAlt n ci t args (underBinders Lifted (\inn => dropUnused inn unused) inn (mkSizeOf args) sc)
+  MkLConAlt n ci t args (underBinderz Lifted (\inn => dropUnused inn unused) inn (mkSizeOf args) sc)
 
 dropConstCase inn unused (MkLConstAlt c val) = MkLConstAlt c (dropUnused inn unused val)
 
@@ -575,8 +574,10 @@ mutual
                unused = getUnused unusedContracted
                scl' = dropUnused (mkSizeOf bound) unused scl
            n <- genName
-           update Lifts { defs $= ((n, MkLFun (dropped vars unused) bound scl') ::) }
-           pure $ LUnderApp fc n (length bound) (allVars fc vars unused)
+           let scl'' : Lifted ((cast (toList $ dropped vars unused)) ++ bound)
+                     := rewrite castToList (dropped vars unused) in scl'
+           update Lifts { defs $= ((n, MkLFun (toList $ dropped vars unused) bound scl'') ::) }
+           pure $  LUnderApp fc n (length bound) (reverse $ allVars fc vars unused)
     where
 
         allPrfs : (vs : Scope) -> SizeOf inner -> (unused : Vect (length vs) Bool) -> List (Var (vs <>< inner))
@@ -650,7 +651,7 @@ export
 lambdaLiftDef : (doLazyAnnots : Bool) -> Name -> CDef -> Core (List (Name, LiftedDef))
 lambdaLiftDef doLazyAnnots n (MkFun args exp)
     = do (expl, defs) <- liftBody {doLazyAnnots} n exp
-         pure ((n, MkLFun args Scope.empty expl) :: defs)
+         pure ((n, MkLFun (toList args) Scope.empty (rewrite castToList args in expl)) :: defs)
 lambdaLiftDef _ n (MkCon t a nt) = pure [(n, MkLCon t a nt)]
 lambdaLiftDef _ n (MkForeign ccs fargs ty) = pure [(n, MkLForeign ccs fargs ty)]
 lambdaLiftDef doLazyAnnots n (MkError exp)

src/Compiler/Opts/CSE.idr

@@ -174,9 +174,9 @@ mutual
   dropConAlt : Drop CConAlt
   dropConAlt inn (MkConAlt x y tag args z) =
     MkConAlt x y tag args <$>
-        dropCExp
-          (inn + mkSizeOf args)
-          (replace {p = CExp} (sym $ appendAssociative outer inner args) z)
+        dropCExp {outer=outer}
+          (rewrite fishAsSnocAppend inner args in inn + mkSizeOf (cast args))
+          (rewrite sym $ snocAppendFishAssociative outer inner args in z)
 
   dropConstAlt : Drop CConstAlt
   dropConstAlt inn (MkConstAlt x y) = MkConstAlt x <$> dropCExp inn y

src/Compiler/Opts/ConstantFold.idr

@@ -57,6 +57,12 @@ wk sout (Wk {ws, ds, vars} rho sws)
     Wk rho (sws + sout)
 wk ws rho = Wk rho ws
 
+wksN : Subst ds vars -> SizeOf out -> Subst (Scope.ext ds out) (Scope.ext vars out)
+wksN s s'
+  = rewrite fishAsSnocAppend ds out in
+    rewrite fishAsSnocAppend vars out in
+    wk (zero <>< s') s
+
 record WkCExp (vars : Scope) where
   constructor MkWkCExp
   {0 outer, supp : Scope}
@@ -172,7 +178,7 @@ constFold rho (CConCase fc sc xs x)
   where
     foldAlt : CConAlt vars -> CConAlt vars'
     foldAlt (MkConAlt n ci t xs e)
-      = MkConAlt n ci t xs $ constFold (wk (mkSizeOf xs) rho) e
+      = MkConAlt n ci t xs $ constFold (wksN rho (mkSizeOf xs)) e
 
 constFold rho (CConstCase fc sc xs x) =
     let sc' = constFold rho sc

src/Compiler/Opts/Constructor.idr

@@ -105,12 +105,12 @@ natBranch (MkConAlt n SUCC _ _ _) = True
 natBranch _ = False
 
 trySBranch : CExp vars -> CConAlt vars -> Maybe (CExp vars)
-trySBranch n (MkConAlt nm SUCC _ [<arg] sc)
+trySBranch n (MkConAlt nm SUCC _ [arg] sc)
     = Just (CLet (getFC n) arg YesInline (magic__natUnsuc (getFC n) (getFC n) [n]) sc)
 trySBranch _ _ = Nothing
 
 tryZBranch : CConAlt vars -> Maybe (CExp vars)
-tryZBranch (MkConAlt n ZERO _ [<] sc) = Just sc
+tryZBranch (MkConAlt n ZERO _ [] sc) = Just sc
 tryZBranch _ = Nothing
 
 getSBranch : CExp vars -> List (CConAlt vars) -> Maybe (CExp vars)
@@ -159,7 +159,7 @@ enum (CConCase fc sc alts def) = do
     Just $ CConstCase fc sc alts' def
   where
     toEnum : CConAlt vars -> Maybe (CConstAlt vars)
-    toEnum (MkConAlt nm (ENUM n) (Just tag) [<] sc)
+    toEnum (MkConAlt nm (ENUM n) (Just tag) [] sc)
         = pure $ MkConstAlt (enumTag n tag) sc
     toEnum _ = Nothing
 enum t = Nothing
@@ -172,7 +172,7 @@ enum t = Nothing
 
 unitTree : Ref NextMN Int => CExp vars -> Core (Maybe (CExp vars))
 unitTree exp@(CConCase fc sc alts def) =
-    let [MkConAlt _ UNIT _ [<] e] = alts
+    let [MkConAlt _ UNIT _ [] e] = alts
             | _ => pure Nothing
     in case sc of -- TODO: Check scrutinee has no effect, and skip let binding
         CLocal {} => pure $ Just e

src/Compiler/Opts/Identity.idr

@@ -10,13 +10,19 @@ import Data.Vect
 import Libraries.Data.List.SizeOf
 import Libraries.Data.SnocList.SizeOf
 
+-- TODO reduce quadratic weakening
 makeArgs : (args : Scope) -> List (Var (Scope.addInner vars args))
 makeArgs args = makeArgs' args id
   where
     makeArgs' : (args : Scope) -> (Var (Scope.addInner vars args) -> a) -> List a
     makeArgs' [<] f = []
     makeArgs' (xs :< x) f = f first :: makeArgs' xs (f . weaken)
 
+makeArgz : (args : List Name) -> List (Var (Scope.ext vars args))
+makeArgz args
+  = embedFishily @{ListFreelyEmbeddable}
+  $ reverse $ allVars ([<] <>< args)
+
 parameters (fn1 : Name) (idIdx : Nat)
   mutual
     -- special case for matching on 'Nat'-shaped things
@@ -89,8 +95,8 @@ parameters (fn1 : Name) (idIdx : Nat)
         altEq : CConAlt vars -> Bool
         altEq (MkConAlt y _ _ args exp) =
             cexpIdentity
-                (weakenNs (mkSizeOf args) var)
-                (Just (y, makeArgs args))
+                (weakensN (mkSizeOf args) var)
+                (Just (y, makeArgz args))
                 const
                 exp
     cexpIdentity var con const (CConstCase fc sc xs x) =