[ refactor ] complete refactors regarding swapping inner/outer

Author: mjustus

src/Compiler/ANF.idr

@@ -194,12 +194,12 @@ mlet fc val sc
 
 bindAsFresh :
   {auto v : Ref Next Int} ->
-  (args : List Name) -> AVars vars' ->
-  Core (List Int, AVars (Scope.ext vars' args))
-bindAsFresh [] vs = pure ([], vs)
-bindAsFresh (n :: ns) vs
+  (args : Scope) -> AVars vars' ->
+  Core (List Int, AVars (vars' ++ args))
+bindAsFresh [<] vs = pure ([], vs)
+bindAsFresh (ns :< n) vs
     = do i <- nextVar
-         mapFst (i ::) <$> bindAsFresh ns (vs :< i)
+         bimap (i ::) (:< i) <$> bindAsFresh ns vs
 
 mutual
   anfArgs : {auto v : Ref Next Int} ->
@@ -211,7 +211,7 @@ mutual
 
   anf : {auto v : Ref Next Int} ->
         AVars vars -> Lifted vars -> Core ANF
-  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup p vs))
+  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup vs p))
   anf vs (LAppName fc lazy n args)
       = anfArgs fc vs args (AAppName fc lazy n)
   anf vs (LUnderApp fc n m args)
@@ -264,12 +264,12 @@ export
 toANF : LiftedDef -> Core ANFDef
 toANF (MkLFun args scope sc)
     = do v <- newRef Next (the Int 0)
-         (iargs, vsNil) <- bindAsFresh (cast args) AVars.empty
+         (iargs, vsNil) <- bindAsFresh args AVars.empty
          let vs : AVars args
            := rewrite sym $ appendLinLeftNeutral args in
-              rewrite snocAppendAsFish Scope.empty args in vsNil
-         (iargs', vs) <- bindAsFresh (cast scope) vs
-         sc' <- anf (rewrite snocAppendAsFish args scope in vs) sc
+              vsNil
+         (iargs', vs) <- bindAsFresh scope vs
+         sc' <- anf vs 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,33 +42,33 @@ shiftUnder : {args : _} ->
 shiftUnder First = weakenNVar (mkSizeOf args) (MkNVar First)
 shiftUnder (Later p) = insertNVar (mkSizeOf args) (MkNVar p)
 
-shiftVar : {outer : Scope} -> {args : List Name} ->
-           NVar n ((vars <>< args :< x) ++ outer) ->
-           NVar n ((vars :< x <>< args) ++ outer)
+shiftVar : {inner : Scope} -> {args : Scope} ->
+           NVar n ((vars ++ args :< x) ++ inner) ->
+           NVar n ((vars :< x ++ args) ++ inner)
 shiftVar nvar
-  = let out = mkSizeOf outer in
-    case locateNVar out nvar of
-      Left nvar => embed nvar
-      Right (MkNVar p) => weakenNs out (shiftUndersN (mkSizeOf _) p)
+  = let inn = mkSizeOf inner in
+    case locateNVar inn nvar of
+      Left (MkNVar p) => weakenNs inn (shiftUnderNs (mkSizeOf args) p)
+      Right nvar => embed nvar
 
 mutual
-  shiftBinder : {outer, args : _} ->
+  shiftBinder : {inner, args : _} ->
                 (new : Name) ->
-                CExp (((vars <>< args) :< old) ++ outer) ->
-                CExp ((vars :< new <>< args) ++ outer)
+                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 {outer} new (CLam fc n sc)
-      = CLam fc n $ shiftBinder {outer = outer :< n} new sc
+  shiftBinder {inner} new (CLam fc n sc)
+      = CLam fc n $ shiftBinder {inner = inner :< n} new sc
   shiftBinder new (CLet fc n inlineOK val sc)
       = CLet fc n inlineOK (shiftBinder new val)
-                           $ shiftBinder {outer = outer :< n} new sc
+                           $ shiftBinder {inner = inner :< n} new sc
   shiftBinder new (CApp fc f args)
       = CApp fc (shiftBinder new f) $ map (shiftBinder new) args
   shiftBinder new (CCon fc ci c tag args)
@@ -90,30 +90,30 @@ mutual
   shiftBinder new (CErased fc) = CErased fc
   shiftBinder new (CCrash fc msg) = CCrash fc msg
 
-  shiftBinderConAlt : {outer, args : _} ->
+  shiftBinderConAlt : {inner, args : _} ->
                 (new : Name) ->
-                CConAlt (((vars <>< args) :< old) ++ outer) ->
-                CConAlt ((vars :< new <>< args) ++ outer)
+                CConAlt (((vars ++ args) :< old) ++ inner) ->
+                CConAlt ((vars :< new ++ args) ++ inner)
   shiftBinderConAlt new (MkConAlt n ci t args' sc)
-      = let sc' : CExp (((vars <>< args) :< old) ++ (outer <>< args'))
-                = rewrite sym $ snocAppendFishAssociative (vars <>< args :< old) outer args' in sc in
+      = let sc' : CExp (((vars ++ args) :< old) ++ (inner ++ args'))
+                = (rewrite appendAssociative ((vars ++ args) :< old) inner args' in sc) in
         MkConAlt n ci t args' $
-           rewrite snocAppendFishAssociative (vars :< new <>< args) outer args'
-             in shiftBinder new {outer = outer <>< args'} sc'
+               rewrite sym $ appendAssociative (vars :< new ++ args) inner args' in
+               shiftBinder new sc'
 
-  shiftBinderConstAlt : {outer, args : _} ->
+  shiftBinderConstAlt : {inner, args : _} ->
                 (new : Name) ->
-                CConstAlt (((vars <>< args) :< old) ++ outer) ->
-                CConstAlt ((vars :< new <>< args) ++ outer)
+                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.ext vars args) old) ->
-                CExp (Scope.ext (Scope.bind vars new) args)
-liftOutLambda = shiftBinder {outer = Scope.empty}
+                CExp (Scope.bind (Scope.addInner vars args) old) ->
+                CExp (Scope.addInner (Scope.bind vars new) args)
+liftOutLambda = shiftBinder {inner = Scope.empty}
 
 -- If all the alternatives start with a lambda, we can have a single lambda
 -- binding outside
@@ -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 (weakensN (mkSizeOf args)) alts)
-                       (map (weakensN (mkSizeOf args)) def)
+                       (map (weakenNs (mkSizeOf args)) alts)
+                       (map (weakenNs (mkSizeOf args)) def)
 
     updateDef : CExp vars -> CExp vars
     updateDef sc = CConCase fc sc alts def

src/Compiler/CompileExpr.idr

@@ -66,7 +66,7 @@ etaExpand i Z exp args = mkApp exp (map (mkLocal (getFC exp)) (reverse args))
 etaExpand i (S k) exp args
     = CLam (getFC exp) (MN "eta" i)
              (etaExpand (i + 1) k (weaken exp)
-                  (first :: map weakenVar args))
+                  (first :: map later args))
 
 export
 expandToArity : Nat -> CExp vars -> List (CExp vars) -> CExp vars
@@ -229,7 +229,7 @@ mutual
            Just gdef <- lookupCtxtExact x (gamma defs)
                 | Nothing => -- primitive type match
                      do xn <- getFullName x
-                        pure $ MkConAlt xn TYCON Nothing args !(toCExpTree n sc)
+                        pure $ MkConAlt xn TYCON Nothing (cast args) !(toCExpTree n (rewrite sym $ fishAsSnocAppend vars args in sc))
                                   :: !(conCases n ns)
            case (definition gdef) of
                 DCon _ arity (Just pos) => conCases n ns -- skip it
@@ -240,16 +240,16 @@ mutual
                         sc' <- toCExpTree n sc
                         ns' <- conCases n ns
                         if dcon (definition gdef)
-                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) (toList args') (shrinkCExp subList sc') :: ns'
-                           else pure $ MkConAlt xn !(dconFlag xn) Nothing (toList args') (shrinkCExp subList sc') :: ns'
+                           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'
     where
       dcon : Def -> Bool
       dcon (DCon {}) = True
       dcon _ = False
 
-      subThinList : Thin (vars ++ args') (vars ++ ([<] <>< args)) -> Thin (vars <>< (args' <>> [])) (vars <>< args)
-      subThinList t = do rewrite fishAsSnocAppend vars (toList args')
-                         rewrite castToList args'
+      subThinList : Thin (vars ++ args') (vars ++ ([<] <>< args)) -> Thin (vars ++ args') (vars <>< args)
+      subThinList t = do -- rewrite fishAsSnocAppend vars (toList args')
+                         -- rewrite castToList args'
                          rewrite fishAsSnocAppend vars args
                          t
 
@@ -315,10 +315,9 @@ mutual
                                     := rewrite sym $ fishAsSnocAppend vars args in sc'
 
                                 let scope : CExp ((vars ++ [<MN "eff" 0]) ++ cast args)
-                                    scope = rewrite sym $ appendAssociative vars [<MN "eff" 0] (cast args) in
-                                            insertNames {outer=cast args}
-                                                        {inner=vars}
-                                                        {ns = [<MN "eff" 0]}
+                                    scope = insertNames {inner=cast args}
+                                                        {outer=vars}
+                                                        {middle = [<MN "eff" 0]}
                                                         (mkSizeOf _) (mkSizeOf _) sc''
                                 let tm = CLet fc (MN "eff" 0) NotInline scr (substs (cast s) env scope)
                                 log "compiler.newtype.world" 50 "Kept the scrutinee \{show tm}, scope: \{show scope}"
@@ -554,7 +553,7 @@ lamRHS ns tm
           tmExp = substs s env (rewrite appendLinLeftNeutral ns in tm)
           newArgs = getNewArgs env
           bounds = mkBounds newArgs
-          expLocs = mkLocals zero {vars = Scope.empty} bounds tmExp in
+          expLocs = mkLocals bounds zero {inner = Scope.empty} tmExp in
           lamBind (getFC tm) _ expLocs
   where
     lamBind : FC -> (ns : Scope) -> CExp ns -> ClosedCExp
@@ -586,7 +585,7 @@ toCDef n ty _ (ExternDef arity)
         -- TODO has quadratic runtime
         getVars : ArgList k ns -> List (Var ns)
         getVars Z = []
-        getVars (S rest) = first :: map weakenVar (getVars rest)
+        getVars (S rest) = first :: map later (getVars rest)
 
 toCDef n ty _ (ForeignDef arity cs)
     = do defs <- get Ctxt
@@ -599,7 +598,7 @@ toCDef n ty _ (Builtin {arity} op)
         -- TODO has quadratic runtime
         getVars : ArgList k ns -> Vect k (Var ns)
         getVars Z = []
-        getVars (S rest) = first :: map weakenVar (getVars rest)
+        getVars (S rest) = first :: map later (getVars rest)
 
 toCDef n _ _ (DCon tag arity pos)
     = do let nt = snd <$> pos

src/Compiler/ES/TailRec.idr

@@ -118,6 +118,7 @@ module Compiler.ES.TailRec
 
 import Data.List
 import Data.List1
+import Data.SnocList
 import Data.SortedSet
 import Data.SortedMap as M
 import Libraries.Data.Graph
@@ -249,7 +250,7 @@ tcDoneName gi = MN "TcDone" gi
 conAlt : TcGroup -> TcFunction -> NamedConAlt
 conAlt (MkTcGroup tcIx funs) (MkTcFunction n ix args exp) =
   let name = tcContinueName tcIx ix
-   in MkNConAlt name DATACON (Just ix) args (toTc exp)
+   in MkNConAlt name DATACON (Just ix) (cast args) (toTc exp)
 
    where
      mutual

src/Compiler/ES/ToAst.idr

@@ -3,6 +3,7 @@
 module Compiler.ES.ToAst
 
 import Data.Vect
+import Data.SnocList
 import Core.CompileExpr
 import Core.Context
 import Compiler.ES.Ast
@@ -223,7 +224,7 @@ mutual
     -- We map the list of args to the corresponding
     -- data projections (field accessors). They'll
     -- be then properly inlined when converting `x`.
-    projections sc args
+    projections sc (toList args)
     MkEConAlt (tag n tg) ci <$> stmt e x
 
   -- a single branch in a pattern match on a constant

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' = weakensN (mkSizeOf args) (MkVar n) in
+      = let MkVar n' = weakenNs (mkSizeOf args) (MkVar n) in
             used n' sc
 
   usedConst : {free : _} ->
@@ -292,20 +292,13 @@ mutual
 
   extendLoc : {vars, free : _} ->
               {auto l : Ref LVar Int} ->
-              FC -> EEnv free vars -> (args' : List Name) ->
-              Core (Bounds (cast args'), EEnv free (Scope.ext vars args'))
-  extendLoc fc env [] = pure (None, env)
-  extendLoc fc env (n :: ns)
+              FC -> EEnv free vars -> (args' : Scope) ->
+              Core (Bounds args', EEnv free (Scope.addInner vars args'))
+  extendLoc fc env [<] = pure (None, env)
+  extendLoc fc env (ns :< n)
       = do xn <- genName "cv"
-           let env' = env :< CRef fc xn
-           (bs', env'') <- extendLoc fc env' ns
-
-           let
-                bs'' : Bounds ([<n] <>< ns)
-                bs'' = do
-                    rewrite snocAppendFishAssociative [<n] [<] ns
-                    cons n xn bs'
-           pure (bs'', env'')
+           (bs', env') <- extendLoc fc env ns
+           pure (Add n xn bs', env' :< CRef fc xn)
 
   evalAlt : {vars, free : _} ->
             {auto c : Ref Ctxt Defs} ->
@@ -314,9 +307,8 @@ mutual
             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 sym $ snocAppendFishAssociative free vars args in sc)
-           pure $ MkConAlt n ci t args (rewrite snocAppendFishAssociative free Scope.empty args in refsToLocals bs scEval)
+           scEval <- eval rec env' stk (rewrite appendAssociative free vars args in sc)
+           pure $ MkConAlt n ci t args (refsToLocals bs scEval)
 
   evalConstAlt : {vars, free : _} ->
                  {auto c : Ref Ctxt Defs} ->
@@ -336,14 +328,17 @@ mutual
   pickAlt rec env stk (CCon fc n ci t args) [] def
       = traverseOpt (eval rec env stk) def
   pickAlt {vars} {free} rec env stk con@(CCon fc n ci t args) (MkConAlt n' _ t' args' sc :: alts) def
-      =
+      = let args'' = toList args' in
         if matches n t n' t'
-           then case checkLengthMatch args' args of
+           then case checkLengthMatch (toList args') args of
                      Nothing => pure Nothing
                      Just m =>
-                         do let env' = extend env args' args m
+                         do let env' = extend env (toList args') args m
                             pure $ Just !(eval rec env' stk
-                                    (rewrite sym $ snocAppendFishAssociative free vars args' in sc))
+                                    (do rewrite sym $ snocAppendFishAssociative free vars (toList args')
+                                        rewrite sym $ snocAppendAsFish (free ++ vars) args'
+                                        sc
+                                    ))
            else pickAlt rec env stk con alts def
     where
       matches : Name -> Maybe Int -> Name -> Maybe Int -> Bool