[ refactor ] Use list of vars instead of names

Author: spcfox

src/Core/Case/CaseBuilder.idr

@@ -1232,55 +1232,66 @@ findExtraDefaults fc defs (Case idx el ty altsIn)
 
 findExtraDefaults fc defs ctree = pure []
 
-mkSubst : {vars : _} -> (args : List Name) ->
+mkSubst : {vars : _} -> (args : List (Var vars)) ->
           (0 _ : LengthMatch args dropped) -> Subst Var dropped vars
 mkSubst [] NilMatch = []
-mkSubst (x :: xs) (ConsMatch m)
-  = case isVar x vars of
-      Just prf => prf :: mkSubst xs m
-      Nothing => ?todo
+mkSubst (x :: xs) (ConsMatch m) = x :: mkSubst xs m
 
-data MatchResult : Type where
-    ConPat   : Name -> (tag : Int) -> List Name -> MatchResult
-    DelayPat : (ty, arg : Name) -> MatchResult
-    ConstPat : Constant -> MatchResult
+data MatchResult : Scoped where
+    ConPat   : Name -> (tag : Int) -> List (Var vars) -> MatchResult vars
+    DelayPat : (ty, arg : Var vars) -> MatchResult vars
+    ConstPat : Constant -> MatchResult vars
 
-Show MatchResult where
+Show (MatchResult vars) where
   show (ConPat n tag args) = "ConPat \{show n} \{show tag} \{show args}"
   show (DelayPat ty arg) = "DelayPat \{show ty} \{show arg}"
   show (ConstPat c) = "ConstPat \{show c}"
 
-optimiseTree : {vars : _} -> List (Name, MatchResult) -> CaseTree vars -> CaseTree vars
-
-optimiseAlt : {vars : _} -> List (Name, MatchResult) -> Name -> CaseAlt vars -> CaseAlt vars
-optimiseAlt ps nm (ConCase n tag args sc)
-    = ConCase n tag args (optimiseTree ((nm, ConPat n tag args) :: ps) sc)
-optimiseAlt ps nm (DelayCase ty arg sc)
-    = DelayCase ty arg (optimiseTree ((nm, DelayPat ty arg) :: ps) sc)
-optimiseAlt ps nm (ConstCase c sc)
-    = ConstCase c (optimiseTree ((nm, ConstPat c) :: ps) sc)
-optimiseAlt ps nm (DefaultCase sc) = DefaultCase (optimiseTree ps sc)
-
-pickAlt : {vars : _} -> List (Name, MatchResult) -> MatchResult -> List (CaseAlt vars) -> Maybe (CaseTree vars)
+Weaken MatchResult where
+  weakenNs s (ConPat n tag args) = ConPat n tag (weakenNs s <$> args)
+  weakenNs s (DelayPat ty arg) = DelayPat (weakenNs s ty) (weakenNs s arg)
+  weakenNs s (ConstPat c) = ConstPat c
+
+optimiseTree : {vars : _} -> List (Var vars, MatchResult vars) -> CaseTree vars -> CaseTree vars
+
+optimiseAlt : {vars : _} -> List (Var vars, MatchResult vars) -> Var vars -> CaseAlt vars -> CaseAlt vars
+optimiseAlt ps v (ConCase n tag args sc)
+    = do let sz = mkSizeOf args
+         let v' = weakenNs sz v
+         let ps' = map (bimap (weakenNs sz) (weakenNs sz)) ps
+         let args' = allVarsPrefix sz
+         ConCase n tag args (optimiseTree ((v', ConPat n tag args') :: ps') sc)
+optimiseAlt ps v (DelayCase ty arg sc)
+    = do let sz = mkSizeOf [_, _]
+         let v' = weakenNs sz v
+         let ps' = map (bimap (weakenNs sz) (weakenNs sz)) ps
+         DelayCase ty arg (optimiseTree ((v', DelayPat first (later first)) :: ps') sc)
+optimiseAlt ps v (ConstCase c sc)
+    = ConstCase c (optimiseTree ((v, ConstPat c) :: ps) sc)
+optimiseAlt ps v (DefaultCase sc) = DefaultCase (optimiseTree ps sc)
+
+pickAlt : {vars : _} -> List (Var vars, MatchResult vars) ->
+          MatchResult vars -> List (CaseAlt vars) -> Maybe (CaseTree vars)
 pickAlt _ _ [] = Nothing
 pickAlt ps p@(ConPat n t args) (ConCase n' t' args' sc :: alts)
     = if t == t' && n == n'
          then checkLengthMatch args args' <&> \match => -- lengths should always match
                 optimiseTree ps $ substCaseTree zero (mkSizeOf _) (mkSubst args match) sc
          else pickAlt ps p alts
 pickAlt ps (DelayPat ty arg) (DelayCase ty' arg' sc :: alts)
-    = Just $ optimiseTree ps $ substCaseTree zero (mkSizeOf _) (mkSubst {dropped=[_, _]} [ty, arg] %search) sc
+    = do let subst : Subst Var [ty', arg'] vars = mkSubst [ty, arg] %search
+         Just (optimiseTree ps $ substCaseTree zero (mkSizeOf _) subst sc)
 pickAlt ps p@(ConstPat c) (ConstCase c' sc :: alts)
     = if c == c'
-         then Just $ optimiseTree ps sc
+         then Just (optimiseTree ps sc)
          else pickAlt ps p alts
-pickAlt ps _ (DefaultCase sc :: alts) = Just $ optimiseTree ps sc
+pickAlt ps _ (DefaultCase sc :: alts) = Just (optimiseTree ps sc)
 pickAlt ps p (_ :: alts) = pickAlt ps p alts
 
 optimiseTree ps (Case idx el ty alts)
-    = do let name = nameAt el
-         fromMaybe (Case idx el ty (map (optimiseAlt ps name) alts)) $ do
-           p <- lookup name ps
+    = do let var = MkVar el
+         fromMaybe (Case idx el ty (map (optimiseAlt ps var) alts)) $ do
+           p <- lookup var ps
            pickAlt ps p alts
 optimiseTree _ tm = tm
 

src/Core/TT/Var.idr

@@ -166,14 +166,18 @@ export
 mkVarChiply : SizeOf inner -> Var (inner <>> nm :: outer)
 mkVarChiply (MkSizeOf s p) = MkVar (mkIsVarChiply p)
 
+export
+allVarsPrefix : SizeOf vars -> List (Var (vars ++ outer))
+allVarsPrefix = go [<] where
+  go : SizeOf local -> SizeOf vs -> List (Var (local <>> vs ++ outer))
+  go s (MkSizeOf Z Z) = []
+  go s (MkSizeOf (S k) (S l)) = mkVarChiply s :: go (suc s) (MkSizeOf k l)
+
 ||| Generate all variables
 export
 allVars : (vars : Scope) -> List (Var vars)
-allVars = go [<] where
-
-  go : SizeOf local -> (vs : Scope) -> List (Var (local <>> vs))
-  go s [] = []
-  go s (v :: vs) = mkVarChiply s :: go (s :< v) vs
+allVars vars = rewrite sym (appendNilRightNeutral vars)
+               in allVarsPrefix (mkSizeOf vars)
 
 export
 Eq (Var xs) where