[ refactor ] Use ConTag for represetaion constructor in case tree

Author: spcfox

src/Compiler/CompileExpr.idr

@@ -209,27 +209,22 @@ mutual
              Name -> List (CaseAlt vars) ->
              Core (List (CConAlt vars))
   conCases n [] = pure []
-  conCases {vars} n (ConCase x tag args sc :: ns)
-      = do defs <- get Ctxt
-           Just gdef <- lookupCtxtExact x (gamma defs)
+  conCases {vars} n (ConCase tag args sc :: ns)
+      = do let n = conName tag
+           defs <- get Ctxt
+           Just gdef <- lookupCtxtExact n (gamma defs)
                 | Nothing => -- primitive type match
-                     do xn <- getFullName x
+                     do xn <- getFullName n
                         pure $ MkConAlt xn TYCON Nothing args !(toCExpTree n sc)
                                   :: !(conCases n ns)
            case (definition gdef) of
                 DCon _ arity (Just pos) => conCases n ns -- skip it
-                _ => do xn <- getFullName x
+                _ => do xn <- getFullName n
                         let (args' ** sub)
                             = mkDropSubst 0 (eraseArgs gdef) vars args
                         sc' <- toCExpTree n sc
                         ns' <- conCases n ns
-                        if dcon (definition gdef)
-                           then pure $ MkConAlt xn !(dconFlag xn) (Just tag) args' (shrinkCExp sub sc') :: ns'
-                           else pure $ MkConAlt xn !(dconFlag xn) Nothing args' (shrinkCExp sub sc') :: ns'
-    where
-      dcon : Def -> Bool
-      dcon (DCon {}) = True
-      dcon _ = False
+                        pure $ MkConAlt xn !(dconFlag xn) (tagOrder tag) args' (shrinkCExp sub sc') :: ns'
   conCases n (_ :: ns) = conCases n ns
 
   constCases : {vars : _} ->
@@ -257,9 +252,9 @@ mutual
   getNewType fc scr n [] = pure Nothing
   getNewType fc scr n (DefaultCase sc :: ns)
       = pure $ Nothing
-  getNewType {vars} fc scr n (ConCase x tag args sc :: ns)
+  getNewType {vars} fc scr n (ConCase tag args sc :: ns)
       = do defs <- get Ctxt
-           case !(lookupDefExact x (gamma defs)) of
+           case !(lookupDefExact (conName tag) (gamma defs)) of
                 -- If the flag is False, we still take the
                 -- default, but need to evaluate the scrutinee of the
                 -- case anyway - if the data structure contains a %World,
@@ -332,7 +327,7 @@ mutual
                 {auto c : Ref Ctxt Defs} ->
                 Name -> CaseTree vars ->
                 Core (CExp vars)
-  toCExpTree' n (Case _ x scTy alts@(ConCase _ _ _ _ :: _))
+  toCExpTree' n (Case _ x scTy alts@(ConCase {} :: _))
       = let fc = getLoc scTy in
             do Nothing <- getNewType fc (CLocal fc x) n alts
                    | Just def => pure def

src/Core/Binary.idr

@@ -25,7 +25,7 @@ import public Libraries.Utils.Binary
 ||| version number if you're changing the version more than once in the same day.
 export
 ttcVersion : Int
-ttcVersion = 2025_12_06_00
+ttcVersion = 2025_12_08_00
 
 export
 checkTTCVersion : String -> Int -> Int -> Core ()

src/Core/Case/CaseBuilder.idr

@@ -21,8 +21,6 @@ import Libraries.Data.List.LengthMatch
 import Libraries.Data.List01
 import Libraries.Data.List01.Quantifiers
 
-import Decidable.Equality
-
 import Libraries.Text.PrettyPrint.Prettyprinter
 
 %default covering
@@ -364,24 +362,14 @@ partition phase (x :: xs) with (partition phase xs)
                VarClause => VarClauses [x] NoClauses
 
 data ConType : Type where
-     CName : Name -> (tag : Int) -> ConType
+     CName : ConTag -> ConType
      CDelay : ConType
      CConst : Constant -> ConType
 
-conTypeEq : (x, y : ConType) -> Maybe (x = y)
-conTypeEq (CName x tag) (CName x' tag')
-   = do Refl <- nameEq x x'
-        case decEq tag tag' of
-             Yes Refl => Just Refl
-             No contra => Nothing
-conTypeEq CDelay CDelay = Just Refl
-conTypeEq (CConst x) (CConst y) = (\xy => cong CConst xy) <$> constantEq x y
-conTypeEq _ _ = Nothing
-
 data Group : List Name -> -- pattern variables still to process
              Scoped where
      ConGroup : {newargs : _} ->
-                Name -> (tag : Int) ->
+                ConTag ->
                 List01 True (PatClause (newargs ++ todo) (newargs ++ vars)) ->
                 Group todo vars
      DelayGroup : {tyarg, valarg : _} ->
@@ -393,14 +381,14 @@ data Group : List Name -> -- pattern variables still to process
 
 covering
 {vars : _} -> {todo : _} -> Show (Group todo vars) where
-  show (ConGroup c t cs) = "Con " ++ show c ++ ": " ++ show cs
+  show (ConGroup tag cs) = "Con " ++ show (conName tag) ++ ": " ++ show cs
   show (DelayGroup cs) = "Delay: " ++ show cs
   show (ConstGroup c cs) = "Const " ++ show c ++ ": " ++ show cs
 
 data GroupMatch : ConType -> List Pat -> Group todo vars -> Type where
-     ConMatch : {tag : Int} -> LengthMatch ps newargs ->
-                GroupMatch (CName n tag) ps
-                  (ConGroup {newargs} n tag (MkPatClause pvs pats pid rhs :: rest))
+     ConMatch : {tag : ConTag} -> LengthMatch ps newargs ->
+                GroupMatch (CName tag) ps
+                  (ConGroup {newargs} tag (MkPatClause pvs pats pid rhs :: rest))
      DelayMatch : GroupMatch CDelay []
                     (DelayGroup {tyarg} {valarg} (MkPatClause pvs pats pid rhs :: rest))
      ConstMatch : GroupMatch (CConst c) []
@@ -409,13 +397,13 @@ data GroupMatch : ConType -> List Pat -> Group todo vars -> Type where
 
 checkGroupMatch : (c : ConType) -> (ps : List Pat) -> (g : Group todo vars) ->
                   GroupMatch c ps g
-checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats pid rhs :: rest))
+checkGroupMatch (CName tag) ps (ConGroup {newargs} tag' (MkPatClause pvs pats pid rhs :: rest))
     = case checkLengthMatch ps newargs of
            Nothing => NoMatch
-           Just prf => case (nameEq x x', decEq tag tag') of
-                            (Just Refl, Yes Refl) => ConMatch prf
+           Just prf => case conTagEq tag tag' of
+                            Just Refl => ConMatch prf
                             _ => NoMatch
-checkGroupMatch (CName x tag) ps _ = NoMatch
+checkGroupMatch (CName tag) ps _ = NoMatch
 checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats pid rhs :: rest))
     = DelayMatch
 checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats pid rhs :: rest))
@@ -511,7 +499,7 @@ groupCons fc fn pvars (x :: xs) {isCons = p :: ps}
     = foldlC (uncurry . gc) !(gc [] x p) $ pushIn xs ps
   where
     addConG : {vars', todo' : _} ->
-              Name -> (tag : Int) ->
+              ConTag ->
               List Pat -> NamedPats todo' vars' ->
               Int -> (rhs : Term vars') ->
               (acc : List01 ne (Group todo' vars')) ->
@@ -520,13 +508,13 @@ groupCons fc fn pvars (x :: xs) {isCons = p :: ps}
     -- add new pattern arguments for each of that constructor's arguments.
     -- The type of 'ConGroup' ensures that we refer to the arguments by
     -- the same name in each of the clauses
-    addConG n tag pargs pats pid rhs []
-        = do cty <- if n == UN (Basic "->")
+    addConG tag pargs pats pid rhs []
+        = do cty <- if tag == TConTag (UN $ Basic "->")
                       then pure $ NBind fc (MN "_" 0) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NType fc (MN "top" 0)))) $
                               (\d, a => pure $ NBind fc (MN "_" 1) (Pi fc top Explicit (MkNFClosure defaultOpts (mkEnv fc vars') (NErased fc Placeholder)))
                                 (\d, a => pure $ NType fc (MN "top" 0)))
                       else do defs <- get Ctxt
-                              Just t <- lookupTyExact n (gamma defs)
+                              Just t <- lookupTyExact (conName tag) (gamma defs)
                                    | Nothing => pure (NErased fc Placeholder)
                               nf defs (mkEnv fc vars') (embed t)
              (patnames ** (l, newargs)) <- nextNames fc "e" pargs (Just cty)
@@ -535,20 +523,20 @@ groupCons fc fn pvars (x :: xs) {isCons = p :: ps}
              let pats' = updatePatNames (updateNames (zip patnames pargs))
                                         (weakenNs l pats)
              let clause = MkPatClause pvars (newargs ++ pats') pid (weakenNs l rhs)
-             pure [ConGroup n tag [clause]]
-    addConG n tag pargs pats pid rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g)
-      addConG n tag pargs pats pid rhs
-              (ConGroup n tag (MkPatClause pvars ps tid tm :: rest) :: gs) | ConMatch {newargs} lprf
+             pure [ConGroup tag [clause]]
+    addConG tag pargs pats pid rhs (g :: gs) with (checkGroupMatch (CName tag) pargs g)
+      addConG tag pargs pats pid rhs
+              (ConGroup tag (MkPatClause pvars ps tid tm :: rest) :: gs) | ConMatch {newargs} lprf
         = do let newps = newPats pargs lprf ps
              let l = mkSizeOf newargs
              let pats' = updatePatNames (updateNames (zip newargs pargs))
                                         (weakenNs l pats)
              let newclause = MkPatClause pvars (newps ++ pats') pid (weakenNs l rhs)
              -- put the new clause at the end of the group, since we
              -- match the clauses top to bottom.
-             pure $ ConGroup n tag (MkPatClause pvars ps tid tm :: rest ++ [newclause]) :: gs
-      addConG n tag pargs pats pid rhs (g :: gs) | NoMatch
-        = (g ::) <$> addConG n tag pargs pats pid rhs gs
+             pure $ ConGroup tag (MkPatClause pvars ps tid tm :: rest ++ [newclause]) :: gs
+      addConG tag pargs pats pid rhs (g :: gs) | NoMatch
+        = (g ::) <$> addConG tag pargs pats pid rhs gs
 
     -- This rather ugly special case is to deal with laziness, where Delay
     -- is like a constructor, but with a special meaning that it forces
@@ -613,14 +601,14 @@ groupCons fc fn pvars (x :: xs) {isCons = p :: ps}
          = addGroup p pprf pats pid (substName n (Local fc (Just True) idx pprf) rhs) acc
     addGroup (PCon cfc n t a pargs) pprf pats pid rhs acc
          = if a == length pargs
-              then addConG n t pargs pats pid rhs acc
+              then addConG (DConTag n t) pargs pats pid rhs acc
               else throw (CaseCompile cfc fn (NotFullyApplied n))
     addGroup (PTyCon cfc n a pargs) pprf pats pid rhs acc
          = if a == length pargs
-           then addConG n 0 pargs pats pid rhs acc
+           then addConG (TConTag n) pargs pats pid rhs acc
            else throw (CaseCompile cfc fn (NotFullyApplied n))
     addGroup (PArrow _ _ s t) pprf pats pid rhs acc
-         = addConG (UN $ Basic "->") 0 [s, t] pats pid rhs acc
+         = addConG (TConTag $ UN $ Basic "->") [s, t] pats pid rhs acc
     -- Go inside the delay; we'll flag the case as needing to force its
     -- scrutinee (need to check in 'caseGroups below)
     addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc
@@ -919,10 +907,10 @@ mutual
     where
       altGroups : forall ne. List01 ne (Group todo vars) -> Core (List (CaseAlt vars))
       altGroups [] = pure $ toList $ DefaultCase <$> errorCase
-      altGroups (ConGroup {newargs} cn tag rest :: cs)
+      altGroups (ConGroup {newargs} tag rest :: cs)
           = do crest <- match fc fn phase rest (map (weakenNs (mkSizeOf newargs)) errorCase)
                cs' <- altGroups cs
-               pure (ConCase cn tag newargs crest :: cs')
+               pure (ConCase tag newargs crest :: cs')
       altGroups (DelayGroup {tyarg} {valarg} rest :: cs)
           = do crest <- match fc fn phase rest (map (weakenNs (mkSizeOf [tyarg, valarg])) errorCase)
                cs' <- altGroups cs
@@ -1150,7 +1138,7 @@ simpleCase fc phase fn ty clauses
 
 mutual
   findReachedAlts : CaseAlt ns' -> List Int
-  findReachedAlts (ConCase _ _ _ t) = findReached t
+  findReachedAlts (ConCase _ _ t) = findReached t
   findReachedAlts (DelayCase _ _ t) = findReached t
   findReachedAlts (ConstCase _ t) = findReached t
   findReachedAlts (DefaultCase t) = findReached t
@@ -1195,7 +1183,7 @@ identifyUnreachableDefaults fc defs nfty cs
 
     dropRep : List (CaseAlt vars) -> SortedSet Int -> (List (CaseAlt vars), SortedSet Int)
     dropRep [] extra = ([], extra)
-    dropRep (c@(ConCase n t args sc) :: rest) extra
+    dropRep (c@(ConCase t args sc) :: rest) extra
           -- assumption is that there's no defaultcase in 'rest' because
           -- we've just removed it
         = let (filteredClauses, extraCases) = partition (not . tagIs t) rest
@@ -1225,11 +1213,11 @@ findExtraDefaults fc defs (Case idx el ty altsIn)
        pure (Prelude.toList extraCases ++ extraCases')
   where
     findExtraAlts : CaseAlt vars -> Core (List Int)
-    findExtraAlts (ConCase x tag args ctree) = findExtraDefaults fc defs ctree
-    findExtraAlts (DelayCase x arg ctree) = findExtraDefaults fc defs ctree
-    findExtraAlts (ConstCase x ctree) = findExtraDefaults fc defs ctree
+    findExtraAlts (ConCase _ _ ctree) = findExtraDefaults fc defs ctree
+    findExtraAlts (DelayCase _ _ ctree) = findExtraDefaults fc defs ctree
+    findExtraAlts (ConstCase _ ctree) = findExtraDefaults fc defs ctree
     -- already handled defaults by elaborating them to all possible cons
-    findExtraAlts (DefaultCase ctree) = pure []
+    findExtraAlts (DefaultCase _) = pure []
 
 findExtraDefaults fc defs ctree = pure []
 

src/Core/Case/CaseTree.idr

@@ -11,8 +11,40 @@ import Libraries.Data.NameMap
 import Libraries.Text.PrettyPrint.Prettyprinter
 import Libraries.Data.List.SizeOf
 
+import Decidable.Equality
+
 %default covering
 
+public export
+data ConTag = DConTag Name Int
+            | TConTag Name
+
+export
+conName : ConTag -> Name
+conName (DConTag n _) = n
+conName (TConTag n) = n
+
+export
+tagOrder : ConTag -> Maybe Int
+tagOrder (DConTag _ i) = Just i
+tagOrder (TConTag {}) = Nothing
+
+export
+conTagEq : (x, y : ConTag) -> Maybe (x = y)
+conTagEq (DConTag n i) (DConTag n' i')
+    = do Refl <- nameEq n n'
+         case decEq i i' of
+              Yes Refl => Just Refl
+              No contra => Nothing
+conTagEq (TConTag n) (TConTag n') = (\xy => cong TConTag xy) <$> nameEq n n'
+conTagEq _ _ = Nothing
+
+export
+Eq ConTag where
+  DConTag _ i == DConTag _ i' = i == i'
+  TConTag n == TConTag n' = n == n'
+  _ == _ = False
+
 mutual
   ||| Case trees in A-normal forms
   ||| i.e. we may only dispatch on variables, not expressions
@@ -37,7 +69,7 @@ mutual
   public export
   data CaseAlt : Scoped where
        ||| Constructor for a data type; bind the arguments and subterms.
-       ConCase : Name -> (tag : Int) -> (args : List Name) ->
+       ConCase : ConTag -> (args : List Name) ->
                  CaseTree (Scope.addInner vars args) -> CaseAlt vars
        ||| Lazy match for the Delay type use for codata types
        DelayCase : (ty : Name) -> (arg : Name) ->
@@ -60,7 +92,7 @@ mutual
   measure Impossible = 0
 
   measureAlts : CaseAlt vars -> Nat
-  measureAlts (ConCase x tag args y) = 1 + (measure y)
+  measureAlts (ConCase tag args y) = 1 + (measure y)
   measureAlts (DelayCase ty arg x) = 1 + (measure x)
   measureAlts (ConstCase x y) = 1 + (measure y)
   measureAlts (DefaultCase x) = 1 + (measure x)
@@ -85,12 +117,12 @@ mutual
 
   export
   StripNamespace (CaseAlt vars) where
-    trimNS ns (ConCase x tag args t) = ConCase x tag args (trimNS ns t)
+    trimNS ns (ConCase tag args t) = ConCase tag args (trimNS ns t)
     trimNS ns (DelayCase ty arg t) = DelayCase ty arg (trimNS ns t)
     trimNS ns (ConstCase x t) = ConstCase x (trimNS ns t)
     trimNS ns (DefaultCase t) = DefaultCase (trimNS ns t)
 
-    restoreNS ns (ConCase x tag args t) = ConCase x tag args (restoreNS ns t)
+    restoreNS ns (ConCase tag args t) = ConCase tag args (restoreNS ns t)
     restoreNS ns (DelayCase ty arg t) = DelayCase ty arg (restoreNS ns t)
     restoreNS ns (ConstCase x t) = ConstCase x (restoreNS ns t)
     restoreNS ns (DefaultCase t) = DefaultCase (restoreNS ns t)
@@ -141,8 +173,8 @@ showCT indent (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
 showCT indent (Unmatched msg) = "Error: " ++ show msg
 showCT indent Impossible = "Impossible"
 
-showCA indent (ConCase n tag args sc)
-        = showSep " " (map show (n :: args)) ++ " => " ++
+showCA indent (ConCase tag args sc)
+        = showSep " " (map show (conName tag :: args)) ++ " => " ++
           showCT indent sc
 showCA indent (DelayCase _ arg sc)
         = "Delay " ++ show arg ++ " => " ++ showCT indent sc
@@ -174,8 +206,8 @@ mutual
   eqTree _ _ = False
 
   eqAlt : CaseAlt vs -> CaseAlt vs' -> Bool
-  eqAlt (ConCase n t args tree) (ConCase n' t' args' tree')
-      = n == n' && eqTree tree tree' -- assume arities match, since name does
+  eqAlt (ConCase t args tree) (ConCase t' args' tree')
+      = t == t' && eqTree tree tree' -- assume arities match, since name does
   eqAlt (DelayCase _ _ tree) (DelayCase _ _ tree')
       = eqTree tree tree'
   eqAlt (ConstCase c tree) (ConstCase c' tree')
@@ -227,8 +259,8 @@ mutual
                        SizeOf ns ->
                        CaseAlt (outer ++ inner) ->
                        CaseAlt (outer ++ (ns ++ inner))
-  insertCaseAltNames p q (ConCase x tag args ct)
-      = ConCase x tag args
+  insertCaseAltNames p q (ConCase tag args ct)
+      = ConCase tag args
            (rewrite appendAssociative args outer (ns ++ inner) in
                     insertCaseNames (mkSizeOf args + p) q {inner}
                         (rewrite sym (appendAssociative args outer inner) in
@@ -252,7 +284,7 @@ getNames add ns sc = getSet ns sc
   where
     mutual
       getAltSet : NameMap Bool -> CaseAlt vs -> NameMap Bool
-      getAltSet ns (ConCase n t args sc) = getSet ns sc
+      getAltSet ns (ConCase t args sc) = getSet ns sc
       getAltSet ns (DelayCase t a sc) = getSet ns sc
       getAltSet ns (ConstCase i sc) = getSet ns sc
       getAltSet ns (DefaultCase sc) = getSet ns sc

src/Core/Case/CaseTree/Pretty.idr

@@ -26,8 +26,9 @@ namespace Raw
   prettyTree (Unmatched msg) = "Error:" <++> pretty0 msg
   prettyTree Impossible = "Impossible"
 
-  prettyAlt (ConCase n tag args sc)
-      = hsep (annotate (DCon (Just n)) (pretty0 n) ::  map pretty0 args)
+  prettyAlt (ConCase tag args sc)
+      = let n = conName tag in
+        hsep (annotate (DCon (Just n)) (pretty0 n) ::  map pretty0 args)
         <++> fatArrow
         <+> let sc = prettyTree sc in
             Union (spaces 1 <+> sc) (nest 2 (hardline <+> sc))
@@ -78,7 +79,8 @@ namespace Resugared
   prettyTree env (Unmatched msg) = pure ("Error:" <++> pretty0 msg)
   prettyTree env Impossible = pure "Impossible"
 
-  prettyAlt env (ConCase n tag args sc) = do
+  prettyAlt env (ConCase tag args sc) = do
+    let n = conName tag
     con <- prettyName n
     sc <- prettyTree (mkEnvOnto emptyFC args env) sc
     pure $ hsep (annotate (DCon (Just n)) con ::  map pretty0 args)