[ refactor ] Make name in Case erased

Author: spcfox

src/Core/Case/CaseTree.idr

@@ -19,8 +19,7 @@ mutual
   public export
   data CaseTree : Scoped where
        ||| case x return scTy of { p1 => e1 ; ... }
-       Case : {name : _} ->
-              (idx : Nat) ->
+       Case : (idx : Nat) ->
               (0 p : IsVar name idx vars) ->
               (scTy : Term vars) -> List (CaseAlt vars) ->
               CaseTree vars
@@ -132,8 +131,8 @@ IsConPat = So . isConPat
 showCT : {vars : _} -> (indent : String) -> CaseTree vars -> String
 showCA : {vars : _} -> (indent : String) -> CaseAlt vars  -> String
 
-showCT indent (Case {name} idx prf ty alts)
-  = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of"
+showCT indent (Case idx prf ty alts)
+  = "case " ++ show (nameAt prf) ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of"
   ++ "\n" ++ indent ++ " { "
   ++ showSep ("\n" ++ indent ++ " | ")
              (assert_total (map (showCA ("  " ++ indent)) alts))

src/Core/Case/CaseTree/Pretty.idr

@@ -15,11 +15,11 @@ namespace Raw
   prettyTree : {vars : _} -> CaseTree vars -> Doc IdrisSyntax
   prettyAlt : {vars : _} -> CaseAlt vars -> Doc IdrisSyntax
 
-  prettyTree (Case {name} idx prf ty alts)
+  prettyTree (Case idx prf ty alts)
       = let ann = case ty of
                     Erased {} => ""
                     _ => space <+> keyword ":" <++> byShow ty
-        in case_ <++> annotate Bound (pretty0 name) <+> ann <++> of_
+        in case_ <++> annotate Bound (pretty0 $ nameAt prf) <+> ann <++> of_
          <+> nest 2 (hardline
          <+> vsep (assert_total (map prettyAlt alts)))
   prettyTree (STerm i tm) = byShow tm
@@ -66,13 +66,13 @@ namespace Resugared
     {auto s : Ref Syn SyntaxInfo} ->
     Env Term vars -> CaseAlt vars -> Core (Doc IdrisSyntax)
 
-  prettyTree env (Case {name} idx prf ty alts) = do
+  prettyTree env (Case idx prf ty alts) = do
     ann <- case ty of
              Erased {} => pure ""
              _ => do ty <- resugar env ty
                      pure (space <+> keyword ":" <++> pretty ty)
     alts <- assert_total (traverse (prettyAlt env) alts)
-    pure $ case_ <++> pretty0 name <+> ann <++> of_
+    pure $ case_ <++> pretty0 (nameAt prf) <+> ann <++> of_
        <+> nest 2 (hardline <+> vsep alts)
   prettyTree env (STerm i tm) = pretty <$> resugar env tm
   prettyTree env (Unmatched msg) = pure ("Error:" <++> pretty0 msg)

src/Core/Coverage.idr

@@ -273,7 +273,7 @@ buildArgs : {auto c : Ref Ctxt Defs} ->
                                     -- (because a previous case matches)
             List ClosedTerm -> -- ^ arguments, with explicit names
             CaseTree vars -> Core (List (List ClosedTerm))
-buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
+buildArgs fc defs known not ps cs@(Case idx el ty altsIn)
   -- If we've already matched on 'el' in this branch, restrict the alternatives
   -- to the tag we already know. Otherwise, add missing cases and filter out
   -- the ones it can't possibly be (the 'not') because a previous case
@@ -293,20 +293,21 @@ buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn)
     buildArgAlt not' (ConCase n t args sc)
         = do let l = mkSizeOf args
              let con = Ref fc (DataCon t (size l)) n
-             let ps' = map (substName var
+             let ps' = map (substName (nameAt el)
                              (apply fc
                                     con (map (Ref fc Bound) args))) ps
              buildArgs fc defs (weakenNs l ((MkVar el, t) :: known))
                                (weakenNs l not') ps' sc
     buildArgAlt not' (DelayCase t a sc)
         = let l = mkSizeOf [t, a]
-              ps' = map (substName var (TDelay fc LUnknown
+              ps' = map (substName (nameAt el)
+                                   (TDelay fc LUnknown
                                              (Ref fc Bound t)
                                              (Ref fc Bound a))) ps in
               buildArgs fc defs (weakenNs l known) (weakenNs l not')
                                 ps' sc
     buildArgAlt not' (ConstCase c sc)
-        = do let ps' = map (substName var (PrimVal fc c)) ps
+        = do let ps' = map (substName (nameAt el) (PrimVal fc c)) ps
              buildArgs fc defs known not' ps' sc
     buildArgAlt not' (DefaultCase sc)
         = buildArgs fc defs known not' ps sc

src/Core/Normalise/Eval.idr

@@ -422,13 +422,13 @@ parameters (defs : Defs) (topopts : EvalOpts)
                EvalOpts -> FC ->
                Stack free -> CaseTree args ->
                Core (CaseResult (TermWithEnv free))
-    evalTree env loc opts fc stk (Case {name} idx x _ alts)
+    evalTree env loc opts fc stk (Case idx x _ alts)
       = do xval <- evalLocal env fc Nothing idx (embedIsVar x) [] loc
            -- we have not defined quote yet (it depends on eval itself) so we show the NF
            -- i.e. only the top-level constructor.
            logC "eval.casetree" 5 $ do
              xval <- toFullNames xval
-             pure "Evaluated \{show name} to \{show xval}"
+             pure "Evaluated \{show (nameAt x)} to \{show xval}"
            let loc' = updateLocal opts env idx (embedIsVar x) loc xval
            findAlt env loc' opts fc stk xval alts
     evalTree env loc opts fc stk (STerm _ tm)

src/Core/TTC.idr

@@ -468,8 +468,8 @@ TTC Pat where
 mutual
   export
   {vars : _} -> TTC (CaseTree vars) where
-    toBuf (Case {name} idx x scTy xs)
-        = do tag 0; toBuf name; toBuf idx; toBuf xs
+    toBuf (Case idx x scTy xs)
+        = do tag 0; toBuf idx; toBuf xs
     toBuf (STerm _ x)
         = do tag 1; toBuf x
     toBuf (Unmatched msg)
@@ -478,8 +478,10 @@ mutual
 
     fromBuf
         = case !getTag of
-               0 => do name <- fromBuf; idx <- fromBuf
+               0 => do idx <- fromBuf
                        xs <- fromBuf
+                       name <- maybe (corrupt "Term") pure
+                                     (getAt idx vars)
                        pure (Case {name} idx (mkPrf idx) (Erased emptyFC Placeholder) xs)
                1 => do x <- fromBuf
                        pure (STerm 0 x)