ScopedSnocList: Cleanup and refactor

Author: spcfox

libs/base/Data/SnocList/Operations.idr

@@ -96,6 +96,17 @@ lengthHomomorphism sx (sy :< x) = Calc $
   ~~ 1 + (length sx + length sy) ...(cong (1+) $ lengthHomomorphism _ _)
   ~~ length sx + (1 + length sy) ...(plusSuccRightSucc _ _)
 
+export
+lengthDistributesOverFish : (sx : SnocList a) -> (ys : List a) ->
+                            length (sx <>< ys) === length sx + length ys
+lengthDistributesOverFish sx [] = sym $ plusZeroRightNeutral _
+lengthDistributesOverFish sx (y :: ys) = Calc $
+  |~ length ((sx :< y) <>< ys)
+  ~~ length (sx :< y) + length ys ...( lengthDistributesOverFish (sx :< y) ys)
+  ~~ S (length sx) + length ys    ...( Refl )
+  ~~ length sx + S (length ys)    ...( plusSuccRightSucc _ _ )
+  ~~ length sx + length (y :: ys) ...( Refl )
+
 -- cons-list operations on snoc-lists
 
 ||| Take `n` first elements from `sx`, returning the whole list if

src/Compiler/CompileExpr.idr

@@ -23,12 +23,6 @@ import Libraries.Data.SnocList.Extra
 
 %default covering
 
--- For ease of type level reasoning!
-public export
-rev : SnocList a -> SnocList a
-rev [<] = [<]
-rev (xs :< x) = [<x] ++ rev xs
-
 data Args
     = NewTypeBy Nat Nat
     | EraseArgs Nat (List Nat)

src/Compiler/Inline.idr

@@ -18,14 +18,11 @@ import Data.Maybe
 import Data.List
 import Data.SnocList
 import Data.Vect
-import Libraries.Data.List.LengthMatch
+
 import Libraries.Data.NameMap
 import Libraries.Data.WithDefault
-
 import Libraries.Data.List.SizeOf
-import Libraries.Data.SnocList.LengthMatch
 import Libraries.Data.SnocList.SizeOf
-import Libraries.Data.SnocList.HasLength
 import Libraries.Data.SnocList.Extra
 
 %default covering

src/Compiler/LambdaLift.idr

@@ -18,6 +18,7 @@ import Core.TT
 
 import Data.List
 import Data.SnocList
+import Data.SnocList.Operations
 import Data.Vect
 
 import Libraries.Data.SnocList.Extra
@@ -360,31 +361,19 @@ record Used (vars : SnocList Name) where
 initUsed : {vars : _} -> Used vars
 initUsed {vars} = MkUsed (replicate (length vars) False)
 
-lengthDistributesOverAppend
-  : (xs, ys : SnocList a)
-  -> length (ys ++ xs) = length xs + length ys
-lengthDistributesOverAppend [<] ys = Refl
-lengthDistributesOverAppend (xs :< x) ys =
-  cong S $ lengthDistributesOverAppend xs ys
-
 weakenUsed : {outer : _} -> Used vars -> Used (vars ++ outer)
 weakenUsed {outer} (MkUsed xs) =
-  MkUsed (rewrite lengthDistributesOverAppend outer vars in
-         (replicate (length outer) False ++ xs))
-
--- TODO
--- lengthDistributesOverAppendFish
---   : (xs : List a)
---   -> (ys : SnocList a)
---   -> length (ys <>< xs) = length xs + length ys
+  MkUsed (rewrite lengthHomomorphism vars outer in
+          rewrite plusCommutative (length vars) (length outer) in
+          replicate (length outer) False ++ xs)
 
 weakenUsedFish : {outer : _} -> Used vars -> Used (vars <>< outer)
 weakenUsedFish {outer} (MkUsed xs) =
     do rewrite fishAsSnocAppend vars outer
-       MkUsed $ do
-                  rewrite lengthDistributesOverAppend (cast outer) vars
-                  -- See lengthDistributesOverAppendFish
-                  (believe_me $ replicate (length outer) False ++ xs)
+       MkUsed $ do rewrite lengthHomomorphism vars (cast outer)
+                   rewrite Extra.lengthDistributesOverFish [<] outer
+                   rewrite plusCommutative (length vars) (length outer)
+                   replicate (length outer) False ++ xs
 
 contractUsed : (Used (vars :< x)) -> Used vars
 contractUsed (MkUsed xs) = MkUsed (tail xs)

src/Core/Case/CaseBuilder.idr

@@ -222,9 +222,9 @@ covering
     where
       showAll : {vs, ts : _} -> NamedPats vs ts -> String
       showAll [] = ""
-      showAll {ts = _ :< t } [x]
+      showAll {ts = _ :< t} [x]
           = show t ++ " " ++ show (pat x) ++ " [" ++ show (argType x) ++ "]"
-      showAll {ts = _ :< t } (x :: xs)
+      showAll {ts = _ :< t} (x :: xs)
           = show t ++ " " ++ show (pat x) ++ " [" ++ show (argType x) ++ "]"
                      ++ ", " ++ showAll xs
 
@@ -233,7 +233,7 @@ covering
     where
       prettyAll : {vs, ts : _} -> NamedPats vs ts -> List (Doc IdrisSyntax)
       prettyAll [] = []
-      prettyAll {ts = _ :< t } (x :: xs)
+      prettyAll {ts = _ :< t} (x :: xs)
           = parens (pretty0 t <++> equals <++> pretty (pat x))
           :: prettyAll xs
 
@@ -597,10 +597,6 @@ updatePatNames _ [] = []
 updatePatNames ns (pi :: ps)
     = { pat $= update } pi :: updatePatNames ns ps
   where
-    lookup : Name -> SnocList (Name, Name) -> Maybe Name
-    lookup n [<] = Nothing
-    lookup n (ns :< (x, n')) = if x == n then Just n' else lookup n ns
-
     update : Pat -> Pat
     update (PAs fc n p)
         = case lookup n ns of
@@ -1226,7 +1222,7 @@ mkPat args orig (Ref fc (DataCon t a) n) = pure $ PCon fc n t a (rev args)
 mkPat args orig (Ref fc (TyCon t a) n) = pure $ PTyCon fc n a (rev args)
 mkPat args orig (Ref fc Func n)
   = do prims <- getPrimitiveNames
-       mtm <- normalisePrims (const True) isPConst True prims n args orig [<]
+       mtm <- normalisePrims (const True) isPConst True prims n (cast args) orig [<]
        case mtm of
          Just tm => if tm /= orig -- check we made progress; if there's an
                                   -- unresolved interface, we might be stuck

src/Core/Context/Context.idr

@@ -195,7 +195,7 @@ export
 covering
 Show Clause where
   show (MkClause {vars} env lhs rhs)
-      = show (toList $ reverse vars) ++ ": " ++ show lhs ++ " = " ++ show rhs
+      = show (asList vars) ++ ": " ++ show lhs ++ " = " ++ show rhs
 
 public export
 data DefFlag

src/Core/Env.idr

@@ -78,15 +78,6 @@ bindEnv loc (env :< b) tm
                                         Explicit
                                         (binderType b)) tm)
 
-public export
-revNs : (vs, ns : SnocList a) -> reverse vs ++ reverse ns = reverse (ns ++ vs)
-revNs [<] ns = rewrite appendLinLeftNeutral (reverse ns) in Refl
-revNs (vs :< v) ns
-    = rewrite Extra.revOnto [<v] vs in
-        rewrite Extra.revOnto [<v] (ns ++ vs) in
-          rewrite sym $ revNs vs ns in
-            rewrite appendAssociative [<v] (reverse vs) (reverse ns) in Refl
-
 -- Weaken by all the names at once at the end, to save multiple traversals
 -- in big environments
 -- Also reversing the names at the end saves significant time over concatenating

src/Core/Normalise.idr

@@ -362,7 +362,7 @@ normalisePrims : {auto c : Ref Ctxt Defs} -> {vs : _} ->
                  List Name ->
                  -- view of the potential redex
                  (n : Name) ->          -- function name
-                 (args : SnocList arg) ->   -- arguments from inside out (arg1, ..., argk)
+                 (args : List arg) ->   -- arguments from inside out (arg1, ..., argk)
                  -- actual term to evaluate if needed
                  (tm : Term vs) ->      -- original term (n arg1 ... argk)
                  Env Term vs ->         -- evaluation environment
@@ -371,7 +371,7 @@ normalisePrims : {auto c : Ref Ctxt Defs} -> {vs : _} ->
 normalisePrims boundSafe viewConstant all prims n args tm env
    = do let True = isPrimName prims !(getFullName n) -- is a primitive
               | _ => pure Nothing
-        let (_ :< mc) = reverse args -- with at least one argument
+        let (mc :: _) = args -- with at least one argument
               | _ => pure Nothing
         let (Just c) = viewConstant mc -- that is a constant
               | _ => pure Nothing

src/Core/Normalise/Convert.idr

@@ -14,6 +14,8 @@ import Data.List
 import Data.SnocList
 
 import Libraries.Data.List.SizeOf
+import Libraries.Data.SnocList.HasLength
+import Libraries.Data.SnocList.SizeOf
 
 %default covering
 
@@ -369,10 +371,12 @@ mutual
 
     convGen q inf defs env (NApp fc val args) (NApp _ val' args')
         = if !(chkConvHead q inf defs env val val')
-             then do i <- getInfPos val
-                     allConv q inf defs env
-                        (cast {from = List (FC, Closure vars)} $ dropInf 0 i $ cast args) -- TODO: UGH!
-                        (cast {from = List (FC, Closure vars)} $ dropInf 0 i $ cast args')
+             then case !(getInfPos val) of
+                    [] => allConv q inf defs env args args'
+                    i  => allConv q inf defs env
+                                  (dropInf i args  $ mkSizeOf args)
+                                  (dropInf i args' $ mkSizeOf args')
+
              else chkConvCaseBlock fc q inf defs env val args1 val' args2
         where
           getInfPos : NHead vars -> Core (List Nat)
@@ -384,13 +388,12 @@ mutual
                    else pure []
           getInfPos _ = pure []
 
-          dropInf : Nat -> List Nat -> List a -> List a
-          dropInf _ [] xs = xs
-          dropInf _ _ [] = []
-          dropInf i ds (x :: xs)
+          dropInf : List Nat -> (sx : SnocList a) -> SizeOf sx -> SnocList a
+          dropInf _ [<] _ = [<]
+          dropInf ds (sx :< x) (MkSizeOf (S i) (S p))
               = if i `elem` ds
-                   then dropInf (S i) ds xs
-                   else x :: dropInf (S i) ds xs
+                   then dropInf ds sx (MkSizeOf i p)
+                   else dropInf ds sx (MkSizeOf i p) :< x
 
           -- Discard file context information irrelevant for conversion checking
           args1 : SnocList (Closure vars)

src/Core/SchemeEval/Compile.idr

@@ -97,7 +97,7 @@ reverseOnto acc [<]       = acc
 reverseOnto acc (sx :< x) = reverseOnto (acc :< x) sx
 
 reverse : SchVars vars -> SchVars (reverse vars)
-reverse sx = reverseOnto [<] sx
+reverse = reverseOnto [<]
 
 getSchVar : {idx : _} -> (0 _ : IsVar n idx vars) -> SchVars vars -> String
 getSchVar First (xs :< Bound x) = x

src/Core/Unify.idr

@@ -273,10 +273,10 @@ unifyArgs : (Unify tm, Quote tm) =>
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             UnifyInfo -> FC -> Env Term vars ->
-            SnocList (tm vars) -> SnocList (tm vars) ->
+            List (tm vars) -> List (tm vars) ->
             Core UnifyResult
-unifyArgs mode loc env [<] [<] = pure success
-unifyArgs mode loc env (cxs :< cx) (cys :< cy)
+unifyArgs mode loc env [] [] = pure success
+unifyArgs mode loc env (cx :: cxs) (cy :: cys)
     = do -- Do later arguments first, since they may depend on earlier
          -- arguments and use their solutions.
          cs <- unifyArgs mode loc env cxs cys
@@ -286,6 +286,24 @@ unifyArgs mode loc env (cxs :< cx) (cys :< cy)
          pure (union res cs)
 unifyArgs mode loc env _ _ = ufail loc ""
 
+unifySpine : (Unify tm, Quote tm) =>
+             {vars : _} ->
+             {auto c : Ref Ctxt Defs} ->
+             {auto u : Ref UST UState} ->
+             UnifyInfo -> FC -> Env Term vars ->
+             SnocList (tm vars) -> SnocList (tm vars) ->
+             Core UnifyResult
+unifySpine mode loc env [<] [<] = pure success
+unifySpine mode loc env (cxs :< cx) (cys :< cy)
+    = do -- Do later arguments first, since they may depend on earlier
+         -- arguments and use their solutions.
+         res <- unify (lower mode) loc env cx cy
+         logC "unify" 20 $ pure $ "unify done: " ++ show res
+         cs <- unifySpine mode loc env cxs cys
+         logC "unify" 20 $ pure $ "unifySpine done: " ++ show cs
+         pure (union cs res)
+unifySpine mode loc env _ _ = ufail loc ""
+
 -- Get the variables in an application argument list; fail if any arguments
 -- are not variables, fail if there's any repetition of variables
 -- We use this to check that the pattern unification rule is applicable
@@ -460,7 +478,7 @@ tryInstantiate : {auto c : Ref Ctxt Defs} ->
               Term newvars -> -- shrunk environment
               Core Bool -- postpone if the type is yet unknown
 tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
-    = do logTerm "unify.instantiate" 5 ("Instantiating in " ++ show !(traverse toFullNames (reverse $ toList newvars))) !(toFullNames tm)
+    = do logTerm "unify.instantiate" 5 ("Instantiating in " ++ show !(traverse toFullNames (asList newvars))) !(toFullNames tm)
 --          let Hole _ _ = definition mdef
 --              | def => ufail {a=()} loc (show mname ++ " already resolved as " ++ show def)
          case fullname mdef of
@@ -473,7 +491,7 @@ tryInstantiate {newvars} loc mode env mname mref num mdef locs otm tm
          logTerm "unify.instantiate" 5 ("Type: " ++ show !(toFullNames mname)) (type mdef)
          logTerm "unify.instantiate" 5 ("Type: " ++ show mname) ty
          log "unify.instantiate" 5 ("With locs: " ++ show locs)
-         log "unify.instantiate" 5 ("From vars: " ++ show (reverse $ toList newvars))
+         log "unify.instantiate" 5 ("From vars: " ++ show (asList newvars))
 
          defs <- get Ctxt
          -- Try to instantiate the hole
@@ -1001,7 +1019,7 @@ mutual
   -- for *all* possible values, we can safely unify the arguments.
   unifyBothApps mode@(MkUnifyInfo p InTerm) loc env xfc (NLocal xr x xp) xargs yfc (NLocal yr y yp) yargs
       = if x == y
-           then unifyArgs mode loc env (reverse $ map snd xargs) (reverse $ map snd yargs)
+           then unifySpine mode loc env (map snd xargs) (map snd yargs)
            else postpone loc mode "Postponing local app"
                          env (NApp xfc (NLocal xr x xp) xargs)
                              (NApp yfc (NLocal yr y yp) yargs)
@@ -1015,8 +1033,8 @@ mutual
            if xi == yi && (invx || umode mode == InSearch)
                                -- Invertible, (from auto implicit search)
                                -- so we can also unify the arguments.
-              then unifyArgs mode loc env (reverse $ map snd $ xargs' ++ xargs)
-                                          (reverse $ map snd $ yargs' ++ yargs)
+              then unifySpine mode loc env (map snd $ xargs' ++ xargs)
+                                           (map snd $ yargs' ++ yargs)
               else do xlocs <- localsIn xargs
                       ylocs <- localsIn yargs
                       -- Solve the one with the bigger context, and if they're
@@ -1054,7 +1072,7 @@ mutual
                                         (NApp yfc (NMeta yn yi yargs) yargs')
   unifyBothApps mode@(MkUnifyInfo p InSearch) loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
       = if hdx == hdy
-           then unifyArgs mode loc env (reverse $ map snd xargs) (reverse $ map snd yargs)
+           then unifySpine mode loc env (map snd xargs) (map snd yargs)
            else unifyApp False mode loc env xfc fx xargs (NApp yfc fy yargs)
   unifyBothApps mode@(MkUnifyInfo p InMatch) loc env xfc fx@(NRef xt hdx) xargs yfc fy@(NRef yt hdy) yargs
       = if hdx == hdy
@@ -1063,7 +1081,7 @@ mutual
                               xs <- traverse (quote defs env) (map snd xargs)
                               ys <- traverse (quote defs env) (map snd yargs)
                               pure ("Matching args " ++ show xs ++ " " ++ show ys))
-                   unifyArgs mode loc env (reverse $ map snd xargs) (reverse $ map snd yargs)
+                   unifySpine mode loc env (map snd xargs) (map snd yargs)
            else unifyApp False mode loc env xfc fx xargs (NApp yfc fy yargs)
   unifyBothApps mode loc env xfc fx ax yfc fy ay
       = unifyApp False mode loc env xfc fx ax (NApp yfc fy ay)
@@ -1183,7 +1201,7 @@ mutual
                            log "unify" 20 "WITH:"
                            traverse_ (dumpArg env) ys
                      -}
-                     unifyArgs mode loc env (reverse $ map snd xs) (reverse $ map snd ys)
+                     unifySpine mode loc env (map snd xs) (map snd ys)
              else convertError loc env
                        (NDCon xfc x tagx ax xs)
                        (NDCon yfc y tagy ay ys)
@@ -1194,14 +1212,11 @@ mutual
           pure $ "Comparing type constructors " ++ show x ++ " and " ++ show y
         if x == y
            then do -- [Note] Restore logging sequence
-                   let xs = reverse $ map snd xs
-                   let ys = reverse $ map snd ys
-
                    logC "unify" 20 $
                      pure $ "Constructor " ++ show x
-                   logC "unify" 20 $ map (const "xs ↑") $ traverse_ (dumpArg env) $ xs
-                   logC "unify" 20 $ map (const "ys ↑") $ traverse_ (dumpArg env) $ ys
-                   unifyArgs mode loc env xs ys
+                   logC "unify" 20 $ map (const "xs ↑") $ traverse_ (dumpArg env) $ reverse $ map snd xs
+                   logC "unify" 20 $ map (const "ys ↑") $ traverse_ (dumpArg env) $ reverse $ map snd ys
+                   unifySpine mode loc env (map snd xs) (map snd ys)
              -- TODO: Type constructors are not necessarily injective.
              -- If we don't know it's injective, need to postpone the
              -- constraint. But before then, we need some way to decide
@@ -1215,10 +1230,10 @@ mutual
   unifyNoEta mode loc env (NDelayed xfc _ x) (NDelayed yfc _ y)
       = unify (lower mode) loc env x y
   unifyNoEta mode loc env (NDelay xfc _ xty x) (NDelay yfc _ yty y)
-      = unifyArgs mode loc env [<xty, x] [<yty, y]
+      = unifyArgs mode loc env [xty, x] [yty, y]
   unifyNoEta mode loc env (NForce xfc _ x axs) (NForce yfc _ y ays)
       = do cs <- unify (lower mode) loc env x y
-           cs' <- unifyArgs mode loc env (reverse $ map snd axs) (reverse $ map snd ays)
+           cs' <- unifySpine mode loc env (map snd axs) (map snd ays)
            pure (union cs cs')
   unifyNoEta mode loc env x@(NApp xfc fx@(NMeta _ _ _) axs)
                           y@(NApp yfc fy@(NMeta _ _ _) ays)

src/Core/Value.idr

@@ -129,16 +129,6 @@ export
 (++) sx Lin = sx
 (++) sx (sy :< y) = (sx ++ sy) :< y
 
-export
-reverseOnto : LocalEnv free varsl -> LocalEnv free varsr -> LocalEnv free (varsl ++ reverse varsr)
-reverseOnto acc Lin       = acc
-reverseOnto {varsr=[<] :< r} acc ([<] :< x) = reverseOnto {varsl=varsl :< r} (acc :< x) [<]
-reverseOnto {varsr=[<] :< vars :< r} acc (sx :< x) = reverseOnto {varsl=varsl :< r} (acc :< x) sx
-
-export
-reverse : LocalEnv free vars -> LocalEnv free (reverse vars)
-reverse {vars} = rewrite sym $ appendLinLeftNeutral (reverse vars) in reverseOnto Lin
-
 export
 cons : LocalEnv free vars -> Closure free -> LocalEnv free (v `cons` vars)
 cons [<] p = Lin :< p