fix

Author: GulinSS

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

@@ -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

src/Compiler/ES/TailRec.idr

@@ -118,6 +118,7 @@ module Compiler.ES.TailRec
 
 import Data.List
 import Data.List1
+import Data.SnocList
 import Libraries.Data.Graph
 import Libraries.Data.SortedSet
 import Libraries.Data.List.Extra as L
@@ -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

src/Compiler/Opts/CSE.idr

@@ -127,8 +127,8 @@ dropVar : SizeOf inner
         -> (0 p : IsVar x n (Scope.addInner outer inner))
         -> Maybe (Erased (IsVar x n inner))
 dropVar inn p = case locateIsVar inn p of
-  Left p => Just p
-  Right p => Nothing
+  Right p => Just p
+  Left p => Nothing
 
 
 -- Tries to 'strengthen' an expression by removing an `outer` context.
@@ -174,15 +174,9 @@ mutual
   dropConAlt : Drop CConAlt
   dropConAlt inn (MkConAlt x y tag args z) =
     MkConAlt x y tag args <$>
-        rewrite fishAsSnocAppend inner args in
         dropCExp
-          (inn + mkSizeOf (cast args))
-          (replace {p = CExp} rule z)
-    where
-      rule : (outer ++ inner) <>< args = outer ++ (inner ++ (cast args))
-      rule = do rewrite appendAssociative outer inner (cast args)
-                rewrite fishAsSnocAppend (outer ++ inner) args
-                Builtin.Refl
+          (inn + mkSizeOf args)
+          (replace {p = CExp} (sym $ appendAssociative outer inner args) z)
 
   dropConstAlt : Drop CConstAlt
   dropConstAlt inn (MkConstAlt x y) = MkConstAlt x <$> dropCExp inn y

src/Compiler/Opts/ConstantFold.idr

@@ -57,12 +57,6 @@ 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}
@@ -72,7 +66,7 @@ record WkCExp (vars : Scope) where
 
 Weaken WkCExp where
   weakenNs s' (MkWkCExp {supp, outer} s Refl e)
-    = MkWkCExp (s + s') (sym $ appendAssociative supp outer ns) e
+    = MkWkCExp (s + s') (sym $ appendAssociative supp outer inner) e
 
 lookup : FC -> Var ds -> Subst ds vars -> CExp vars
 lookup fc (MkVar p) rho = case go p rho of
@@ -178,7 +172,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 (wksN rho (mkSizeOf xs)) e
+      = MkConAlt n ci t xs $ constFold (wk (mkSizeOf xs) rho) e
 
 constFold rho (CConstCase fc sc xs x) =
     let sc' = constFold rho sc

src/Compiler/Opts/Identity.idr

@@ -17,11 +17,6 @@ makeArgs args = makeArgs' args id
     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 $ Var.allVars ([<] <>< args)
-
 parameters (fn1 : Name) (idIdx : Nat)
   mutual
     -- special case for matching on 'Nat'-shaped things
@@ -94,8 +89,8 @@ parameters (fn1 : Name) (idIdx : Nat)
         altEq : CConAlt vars -> Bool
         altEq (MkConAlt y _ _ args exp) =
             cexpIdentity
-                (weakensN (mkSizeOf args) var)
-                (Just (y, makeArgz args))
+                (weakenNs (mkSizeOf args) var)
+                (Just (y, makeArgs args))
                 const
                 exp
     cexpIdentity var con const (CConstCase fc sc xs x) =

src/Compiler/Scheme/Common.idr

@@ -14,6 +14,7 @@ import Core.TT
 
 import Libraries.Data.SortedSet
 import Libraries.Data.String.Builder
+import Data.SnocList
 
 import Data.Vect
 
@@ -358,11 +359,11 @@ parameters (constants : SortedSet Name)
     schConAlt : Nat -> Builder -> NamedConAlt -> Core Builder
     schConAlt i target (MkNConAlt n ci tag args sc)
         = pure $ "((" ++ showTag n tag ++ ") "
-                      ++ bindArgs target sc 1 args !(schExp i sc) ++ ")"
+                      ++ bindArgs target sc 1 (toList args) !(schExp i sc) ++ ")"
 
     schConUncheckedAlt : Nat -> Builder -> NamedConAlt -> Core Builder
     schConUncheckedAlt i target (MkNConAlt n ci tag args sc)
-        = pure $ bindArgs target sc 1 args !(schExp i sc)
+        = pure $ bindArgs target sc 1 (toList args) !(schExp i sc)
 
     schConstAlt : Nat -> Builder -> NamedConstAlt -> Core Builder
     schConstAlt i target (MkNConstAlt c exp)
@@ -435,7 +436,7 @@ parameters (constants : SortedSet Name)
       where
         getAltCode : Builder -> NamedConAlt -> Core Builder
         getAltCode n (MkNConAlt _ _ _ args sc)
-            = pure $ bindArgs n sc 0 args !(schExp i sc)
+            = pure $ bindArgs n sc 0 (toList args) !(schExp i sc)
     schRecordCase _ _ _ _ = throw $ InternalError "Case of a record has multiple alternatives"
 
     schListCase : Nat -> NamedCExp -> List NamedConAlt -> Maybe NamedCExp ->
@@ -475,7 +476,7 @@ parameters (constants : SortedSet Name)
 
         getConsCode : Builder -> List NamedConAlt -> Core (Maybe Builder)
         getConsCode n [] = pure Nothing
-        getConsCode n (MkNConAlt _ CONS _ [x,xs] sc :: _)
+        getConsCode n (MkNConAlt _ CONS _ [<x,xs] sc :: _)
             = do sc' <- schExp (i + 1) sc
                  pure $ Just $ bindArgs [(x, "car"), (xs, "cdr")] sc'
           where
@@ -525,7 +526,7 @@ parameters (constants : SortedSet Name)
 
         getJustCode : Builder -> List NamedConAlt -> Core (Maybe Builder)
         getJustCode n [] = pure Nothing
-        getJustCode n (MkNConAlt _ JUST _ [x] sc :: _)
+        getJustCode n (MkNConAlt _ JUST _ [<x] sc :: _)
             = do sc' <- schExp (i + 1) sc
                  pure $ Just $ bindArg x sc'
           where

src/Core/Case/CaseBuilder.idr

@@ -1201,7 +1201,7 @@ mkPatClause fc fn args s ty pid (ps, rhs)
                := case as of
                       [] => (Unknown, [])
                       (a :: as) => (embed a, as)
-           let info = MkInfo {name=r} p (fishyIsVar {outer=[<]} h) ty
+           let info = MkInfo {name=r} p (isVarFishily {outer=[<]} h) ty
            rest <- mkNames args ps eq h as
            pure (info :: rewrite fishAsSnocAppend [<r] args in embed rest)