[ refactor ] Refactor and optimize CaseBuilder (#16)

* [ refactor ] Replace `rev` with `reverse` and make `LengthMatch` arguments erased

* [ refactor ] Move `embed'` definition into `FreelyEmbeddable` implementation

* [ refactor ] Optimize `mkPatClause.mkNames` in `CaseBuilder`

* [ refactor ] Swap parameters of `NamedPats`

* [ refactor ] Remove `snoc` for `NamedPats`

* [ refactor ] Use `List` for forward order in `CaseBuilder.idr`

* [ refactor ] Swap the arguments of `PatClause`, `Group` and `ScoredPats` like `NamedPats`

* [ refactor ] Merge simillar cases in `nextNames'` and `mkNames`

* [ cleanup ] Remove redudant functions

Cherry-picked from GulinSS#16
Fully authored by Viktor Yudov <[email protected]>

Co-authored-by: Viktor Yudov <[email protected]>

Author: GulinSS

src/Core/Case/CaseBuilder.idr

@@ -188,8 +188,16 @@ interface GenWeaken (0 tm : Scoped) where
 
 export
 genWeaken : GenWeaken tm =>
-  SizeOf outer -> tm (Scope.addInner local outer) -> tm (Scope.addInner local (Scope.addInner [<n] outer))
-genWeaken l = genWeakenNs l (suc zero)
+  SizeOf outer -> tm (Scope.addInner local outer) -> tm (Scope.addInner (Scope.bind local n) outer)
+genWeaken l = rewrite sym $ appendAssociative local [<n] outer in genWeakenNs l (suc zero)
+
+export
+genWeakenFishily : GenWeaken tm =>
+  SizeOf outer -> tm (Scope.ext local outer) -> tm (Scope.ext (Scope.bind local n) outer)
+genWeakenFishily
+    = rewrite fishAsSnocAppend local outer in
+      rewrite fishAsSnocAppend (local :<n) outer in
+      genWeaken . cast
 
 export
 weakensN : Weaken tm =>

src/Core/Name/Scoped.idr

@@ -328,8 +328,8 @@ normalisePrims : {auto c : Ref Ctxt Defs} -> {vs : _} ->
                  -- list of primitives
                  List Name ->
                  -- view of the potential redex
-                 (n : Name) ->          -- function name
-                 (args : List arg) ->   -- arguments from inside out (arg1, ..., argk)
+                 (n : Name) ->               -- function name
+                 (args : SnocList arg) ->   -- arguments in reversed order [<arg1, ..., argk]
                  -- actual term to evaluate if needed
                  (tm : Term vs) ->      -- original term (n arg1 ... argk)
                  Env Term vs ->         -- evaluation environment
@@ -338,7 +338,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 :: _) = 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.idr

@@ -38,6 +38,18 @@ data IsVar : a -> Nat -> SnocList a -> Type where
 
 %name IsVar idx
 
+namespace List
+  ||| IsVar n k ns is a proof that
+  ||| the name n
+  ||| is a position k
+  ||| in the list ns
+  public export
+  data IsVarL : a -> Nat -> List a -> Type where
+      First : IsVarL n Z (n :: ns)
+      Later : IsVarL n i ns -> IsVarL n (S i) (m :: ns)
+
+  %name IsVarL idx
+
 export
 finIdx : {idx : _} -> (0 prf : IsVar x idx vars) ->
          Fin (length vars)
@@ -83,12 +95,19 @@ dropIsVar :
 dropIsVar (xs :< _) First = xs
 dropIsVar (xs :< n) (Later p) = dropIsVar xs p :< n
 
+||| Compute the remaining scope once the target variable has been removed
+public export
+dropIsVarL : (ns : List a) -> {idx : Nat} -> (0 _ : IsVarL nm idx ns) -> List a
+dropIsVarL (_ :: xs) First = xs
+dropIsVarL (n :: xs) (Later p) = n :: dropIsVarL xs p
+
 ||| Throw in extra variables on the outer side of the context
 ||| This is essentially the identity function
 ||| This is slow so we ensure it's only used in a runtime irrelevant manner
 export
 0 embedIsVar : IsVar x idx vars -> IsVar x idx (more ++ vars)
-embedIsVar tm = believe_me tm
+embedIsVar First = First
+embedIsVar (Later p) = Later (embedIsVar p)
 
 ||| Throw in extra variables on the local end of the context.
 ||| This is slow so we ensure it's only used in a runtime irrelevant manner
@@ -97,6 +116,13 @@ export
 weakenIsVar (MkSizeOf Z Z) p =  p
 weakenIsVar (MkSizeOf (S k) (S l)) p =  Later (weakenIsVar (MkSizeOf k l) p)
 
+||| Throw in extra variables on the local end of the context.
+||| This is slow so we ensure it's only used in a runtime irrelevant manner
+export
+0 weakenIsVarL : (s : SizeOf ns) -> IsVarL x idx xs -> IsVarL x (size s + idx) (ns ++ xs)
+weakenIsVarL (MkSizeOf Z Z) p =  p
+weakenIsVarL (MkSizeOf (S k) (S l)) p =  Later (weakenIsVarL (MkSizeOf k l) p)
+
 0 locateIsVarLT :
   (s : SizeOf local) ->
   So (idx < size s) ->
@@ -203,6 +229,13 @@ record NVar {0 a : Type} (nm : a) (vars : SnocList a) where
   {nvarIdx : Nat}
   0 nvarPrf : IsVar nm nvarIdx vars
 
+namespace List
+  public export
+  record NVarL {0 a : Type} (nm : a) (vars : List a) where
+    constructor MkNVarL
+    {nvarIdx : Nat}
+    0 nvarPrf : IsVarL nm nvarIdx vars
+
 namespace NVar
   export
   later : NVar nm ns -> NVar nm (ns :< n)
@@ -268,8 +301,11 @@ locateVar s v  = bimap forgetName forgetName
 
 export
 weakenNVar : SizeOf ns -> NVar name inner -> NVar name (inner ++ ns)
-weakenNVar s (MkNVar {nvarIdx} p)
-  = MkNVar {nvarIdx = plus (size s) nvarIdx} (weakenIsVar s p)
+weakenNVar s (MkNVar p) = MkNVar (weakenIsVar s p)
+
+export
+weakenNVarL : SizeOf ns -> NVarL nm inner -> NVarL nm (ns ++ inner)
+weakenNVarL s (MkNVarL p) = MkNVarL (weakenIsVarL s p)
 
 export
 embedNVar : NVar name vars -> NVar name (more ++ vars)

src/Core/TT/Var.idr

@@ -33,18 +33,6 @@ revOnto xs (vs :< v)
         rewrite Extra.revOnto [<v] vs in
           rewrite appendAssociative xs [<v] (reverse vs) in Refl
 
-export
-lookup : Eq a => a -> SnocList (a, b) -> Maybe b
-lookup n [<] = Nothing
-lookup n (ns :< (x, n')) = if x == n then Just n' else lookup n ns
-
-lengthDistributesOverAppend
-  : (xs, ys : SnocList a)
-  -> length (ys ++ xs) = length xs + length ys
-lengthDistributesOverAppend [<] ys = Refl
-lengthDistributesOverAppend (xs :< x) ys =
-  cong S $ lengthDistributesOverAppend xs ys
-
 export
 lengthDistributesOverFish : (sx : SnocList a) -> (ys : List a) ->
                             length (sx <>< ys) === length sx + length ys

src/Libraries/Data/SnocList/Extra.idr

@@ -855,7 +855,7 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp
         = do tm <- Normalise.normalisePrims (`boundSafe` elabMode elabinfo)
                                             isIPrimVal
                                             (onLHS (elabMode elabinfo))
-                                            prims n expargs (fst res) env
+                                            prims n (cast {to=SnocList RawImp} expargs) (fst res) env
              pure (fromMaybe (fst res) tm, snd res)
 
       where

src/TTImp/Elab/App.idr

@@ -194,7 +194,7 @@ Value *Main_main_10
 ,   Value * var_1
 )
 {
-    Value * var_2 = idris2_getPredefinedInteger(0);          // Main:10:30--10:36
+    Value * var_2 = idris2_getPredefinedInteger(0);          // Main:14:25--14:31
     Value * var_3 = idris2_trampoline(Main_last(var_0, var_2));
                                                              // Prelude.Show:110:1--112:50
     Value * var_4 = idris2_trampoline(Prelude_Show_show_Show_Integer(var_3));
@@ -205,9 +205,9 @@ Value *Main_main_10
     Value * var_6 = primVar_50;                              // Prelude.IO:98:22--98:34
     Value *closure_51 = (Value *)idris2_mkClosure((Value *(*)())Prelude_IO_prim__putStr, 2, 2);
                                                              // Prelude.IO:98:22--98:34
-    ((Value_Closure*)closure_48)->args[0] = var_6;
-    ((Value_Closure*)closure_48)->args[1] = var_1;
-    return closure_48;
+    ((Value_Closure*)closure_51)->args[0] = var_6;
+    ((Value_Closure*)closure_51)->args[1] = var_1;
+    return closure_51;
 }
 Value *Main_main_9
 (
@@ -243,20 +243,20 @@ Value *Main_main_9
      // constructor Prelude.Interfaces.MkFoldable            // Prelude.Types:656:1--669:59
     Value_Constructor* constructor_62 = idris2_newConstructor(6, 0);
                                                              // Prelude.Types:656:1--669:59
-    constructor_59->args[0] = var_5;
-    constructor_59->args[1] = var_6;
-    constructor_59->args[2] = var_7;
-    constructor_59->args[3] = var_8;
-    constructor_59->args[4] = var_9;
-    constructor_59->args[5] = var_10;
-    Value * var_12 = (Value*)constructor_59;                 // Main:10:13--10:17
-    Value *closure_60 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Interfaces_for_, 4, 4);
-                                                             // Main:10:13--10:17
-    ((Value_Closure*)closure_60)->args[0] = var_11;
-    ((Value_Closure*)closure_60)->args[1] = var_12;
-    ((Value_Closure*)closure_60)->args[2] = var_0;
-    ((Value_Closure*)closure_60)->args[3] = var_1;
-    return closure_60;
+    constructor_62->args[0] = var_5;
+    constructor_62->args[1] = var_6;
+    constructor_62->args[2] = var_7;
+    constructor_62->args[3] = var_8;
+    constructor_62->args[4] = var_9;
+    constructor_62->args[5] = var_10;
+    Value * var_12 = (Value*)constructor_62;                 // Main:14:8--14:12
+    Value *closure_63 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Interfaces_for_, 4, 4);
+                                                             // Main:14:8--14:12
+    ((Value_Closure*)closure_63)->args[0] = var_11;
+    ((Value_Closure*)closure_63)->args[1] = var_12;
+    ((Value_Closure*)closure_63)->args[2] = var_0;
+    ((Value_Closure*)closure_63)->args[3] = var_1;
+    return closure_63;
 }
 Value *Main_main_8
 (
@@ -269,12 +269,12 @@ Value *Main_main_8
 {
     idris2_removeReference(var_0);
     idris2_removeReference(var_1);
-    Value *closure_61 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldMap_Foldable_List, 3, 3);
+    Value *closure_64 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldMap_Foldable_List, 3, 3);
                                                              // Prelude.Types:656:1--669:59
-    ((Value_Closure*)closure_61)->args[0] = var_2;
-    ((Value_Closure*)closure_61)->args[1] = var_3;
-    ((Value_Closure*)closure_61)->args[2] = var_4;
-    return closure_61;
+    ((Value_Closure*)closure_64)->args[0] = var_2;
+    ((Value_Closure*)closure_64)->args[1] = var_3;
+    ((Value_Closure*)closure_64)->args[2] = var_4;
+    return closure_64;
 }
 Value *Main_main_7
 (
@@ -299,13 +299,13 @@ Value *Main_main_6
     idris2_removeReference(var_0);
     idris2_removeReference(var_1);
     idris2_removeReference(var_2);
-    Value *closure_62 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldlM_Foldable_List, 4, 4);
+    Value *closure_65 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldlM_Foldable_List, 4, 4);
                                                              // Prelude.Types:656:1--669:59
-    ((Value_Closure*)closure_62)->args[0] = var_3;
-    ((Value_Closure*)closure_62)->args[1] = var_4;
-    ((Value_Closure*)closure_62)->args[2] = var_5;
-    ((Value_Closure*)closure_62)->args[3] = var_6;
-    return closure_62;
+    ((Value_Closure*)closure_65)->args[0] = var_3;
+    ((Value_Closure*)closure_65)->args[1] = var_4;
+    ((Value_Closure*)closure_65)->args[2] = var_5;
+    ((Value_Closure*)closure_65)->args[3] = var_6;
+    return closure_65;
 }
 Value *Main_main_5
 (
@@ -314,10 +314,10 @@ Value *Main_main_5
 )
 {
     idris2_removeReference(var_0);
-    Value *closure_63 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_null_Foldable_List, 1, 1);
+    Value *closure_66 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_null_Foldable_List, 1, 1);
                                                              // Prelude.Types:656:1--669:59
-    ((Value_Closure*)closure_63)->args[0] = var_1;
-    return closure_63;
+    ((Value_Closure*)closure_66)->args[0] = var_1;
+    return closure_66;
 }
 Value *Main_main_4
 (
@@ -330,12 +330,12 @@ Value *Main_main_4
 {
     idris2_removeReference(var_0);
     idris2_removeReference(var_1);
-    Value *closure_64 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldl_Foldable_List, 3, 3);
+    Value *closure_67 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldl_Foldable_List, 3, 3);
                                                              // Prelude.Types:656:1--669:59
-    ((Value_Closure*)closure_64)->args[0] = var_2;
-    ((Value_Closure*)closure_64)->args[1] = var_3;
-    ((Value_Closure*)closure_64)->args[2] = var_4;
-    return closure_64;
+    ((Value_Closure*)closure_67)->args[0] = var_2;
+    ((Value_Closure*)closure_67)->args[1] = var_3;
+    ((Value_Closure*)closure_67)->args[2] = var_4;
+    return closure_67;
 }
 Value *Main_main_3
 (
@@ -348,12 +348,12 @@ Value *Main_main_3
 {
     idris2_removeReference(var_0);
     idris2_removeReference(var_1);
-    Value *closure_65 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldr_Foldable_List, 3, 3);
+    Value *closure_68 = (Value *)idris2_mkClosure((Value *(*)())Prelude_Types_foldr_Foldable_List, 3, 3);
                                                              // Prelude.Types:656:1--669:59
-    ((Value_Closure*)closure_65)->args[0] = var_2;
-    ((Value_Closure*)closure_65)->args[1] = var_3;
-    ((Value_Closure*)closure_65)->args[2] = var_4;
-    return closure_65;
+    ((Value_Closure*)closure_68)->args[0] = var_2;
+    ((Value_Closure*)closure_68)->args[1] = var_3;
+    ((Value_Closure*)closure_68)->args[2] = var_4;
+    return closure_68;
 }
 Value *Main_main_2
 (
@@ -393,10 +393,10 @@ Value *Main_main_0
 {
     idris2_removeReference(var_0);
     idris2_removeReference(var_1);
-    Value *closure_66 = (Value *)idris2_mkClosure((Value *(*)())Prelude_IO_map_Functor_IO, 3, 3);
+    Value *closure_69 = (Value *)idris2_mkClosure((Value *(*)())Prelude_IO_map_Functor_IO, 3, 3);
                                                              // Prelude.IO:15:1--17:38
-    ((Value_Closure*)closure_66)->args[0] = var_2;
-    ((Value_Closure*)closure_66)->args[1] = var_3;
-    ((Value_Closure*)closure_66)->args[2] = var_4;
-    return closure_66;
+    ((Value_Closure*)closure_69)->args[0] = var_2;
+    ((Value_Closure*)closure_69)->args[1] = var_3;
+    ((Value_Closure*)closure_69)->args[2] = var_4;
+    return closure_69;
 }