Skip to content

Commit 1122268

Browse files
nanavaticlaude
andcommitted
Fix drifted handwritten tycon constants found by tconcheck
Bring all nine drifted constants in line with the Prelude-derived truth (the checker's DRIFT output was used as the spec), and empty the tconcheck knownDrift waiver list; the waiver mechanism remains for future incidents but ships empty. * Type.hs tInt/tUInt: TIabstract -> TIdata (Prelude declares 'data Int n = Int (Bit n)' and likewise UInt) * Type.hs tPrimPair (and StdPrel tiPair, used by itPrimPair): SStruct -> SInterface [] (PrimPair is declared as an interface) * Type.hs tActionValue: old struct sort -> TIdata [ActionValue] ('data ActionValue a = ActionValue ...') * Type.hs tActionValue_: field names __value/__action -> avValue_/avAction_ (new PreIds position variants added) * Type.hs tFile: TIabstract -> TIdata [InvalidFile, MCD, FD] (new PreStrings/PreIds constructor ids added) * ISyntaxUtil itInout: kind # -> * (apparently copied from itInout_) corrected to * -> * * ISyntaxUtil itPrimPair: kind was left-nested, (* -> *) -> *, because IKFun had no fixity declaration and defaulted to infixl 9; IType.hs now declares infixr 8 `IKFun` (matching Kind's right-nested Kfun and IConv.iConvK). Census of every backticked IKFun chain in the tree: itPrimPair was the only unparenthesized multi-arrow chain; all others are single-arrow or already explicitly parenthesized, so the fixity change reparses nothing else. * StdPrel tiBufferMode (used by itBufferMode): tiEnum -> tiData (BlockBuffering carries a Maybe Integer argument, so BufferMode is not an enum) The corresponding position-parameterized variants (tIntAt, tActionValueAt, tActionValue_At) are fixed to the same payloads. A consumer audit found no reader of these payloads out of the constants themselves: comparison sites use Eq/Ord (which compare by qualified Id) or wildcard the payload fields in patterns; the payloads only travel into generated ISyntax via iConvT, where they now agree with what symtab-derived types already carried. tconcheck now reports all 94 entries OK with zero waived. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01LVL9ornS6uf9hVxAuL7GhK
1 parent c10da80 commit 1122268

7 files changed

Lines changed: 47 additions & 43 deletions

File tree

src/comp/ISyntaxUtil.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ itReal = ITCon idReal IKStar tiReal
6161
itClock, itReset, itInout, itInout_ :: IType
6262
itClock = ITCon idClock IKStar tiClock
6363
itReset = ITCon idReset IKStar tiReset
64-
itInout = ITCon idInout (IKNum `IKFun` IKStar) tiInout
64+
itInout = ITCon idInout (IKStar `IKFun` IKStar) tiInout
6565
itInout_ = ITCon idInout_ (IKNum `IKFun` IKStar) tiInout
6666

6767
itInoutT :: IType -> IType

src/comp/IType.hs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,12 @@ import qualified Data.Generics as Generic
3131
-- ==============================
3232
-- IKind, IType
3333

34+
-- Arrow kinds nest to the right (matching Kind's Kfun and IConv.iConvK),
35+
-- so backticked IKFun chains must associate to the right. Without this
36+
-- declaration the default infixl 9 silently built left-nested (wrong)
37+
-- kinds; tconcheck caught exactly that in itPrimPair.
38+
infixr 8 `IKFun`
39+
3440
data IKind
3541
= IKStar
3642
| IKNum

src/comp/PreIds.hs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,11 @@ idInvalid = prelude_id_no fsInvalid
120120
idValid = prelude_id_no fsValid
121121
idEmpty = prelude_id_no fsEmptyIfc
122122
idFile = prelude_id_no fsFile
123+
-- constructors of the File type
124+
idInvalidFile, idMCD, idFD :: Id
125+
idInvalidFile = prelude_id_no fsInvalidFile
126+
idMCD = prelude_id_no fsMCD
127+
idFD = prelude_id_no fsFD
123128
idEither, idLeft, idRight :: Id
124129
idEither = prelude_id_no fsEither
125130
idLeft = prelude_id_no fsLeft
@@ -138,6 +143,9 @@ idActionValue_ = prelude_id_no fsActionValue_
138143
idAVValue_, idAVAction_ :: Id
139144
idAVValue_ = prelude_id_no fsAVValue_
140145
idAVAction_ = prelude_id_no fsAVAction_
146+
idAVValue_at, idAVAction_at :: Position -> Id
147+
idAVValue_at pos = prelude_id pos fsAVValue_
148+
idAVAction_at pos = prelude_id pos fsAVAction_
141149

142150
-- names of the special selector functions in the Prelude
143151
id__value, id__action :: Id

src/comp/PreStrings.hs

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -502,6 +502,12 @@ fsBitsToReal = mkFString "$bitstoreal"
502502

503503
fsFile = mkFString "File"
504504

505+
-- | Constructors of the File type in the Prelude
506+
fsInvalidFile, fsMCD, fsFD :: FString
507+
fsInvalidFile = mkFString "InvalidFile"
508+
fsMCD = mkFString "MCD"
509+
fsFD = mkFString "FD"
510+
505511

506512
-- | Classes hardcoded in the Prelude which were added for ContextErrors
507513
fsBitwise, fsBitReduce, fsBitExtend, fsArith, fsOrd :: FString

src/comp/StdPrel.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1053,7 +1053,7 @@ tiInout = TIabstract
10531053
tiPrimArray = TIabstract
10541054

10551055
tiPair, tiBool, tiAction, tiRules, tiString, tiChar :: TISort
1056-
tiPair = TIstruct SStruct [idPrimFst, idPrimSnd]
1056+
tiPair = TIstruct (SInterface []) [idPrimFst, idPrimSnd]
10571057
tiBool = tiEnum [idFalse, idTrue]
10581058
tiAction = TIabstract
10591059
tiRules = TIabstract
@@ -1062,7 +1062,7 @@ tiChar = TIabstract
10621062

10631063
tiHandle, tiBufferMode, tiMaybe, tiList, tiFmt :: TISort
10641064
tiHandle = TIabstract
1065-
tiBufferMode = tiEnum [idNoBuffering, idLineBuffering, idBlockBuffering]
1065+
tiBufferMode = tiData [idNoBuffering, idLineBuffering, idBlockBuffering]
10661066
tiMaybe = tiData [idInvalid, idValid]
10671067
tiList = tiData [idNil noPosition, idCons noPosition]
10681068
tiFmt = TIabstract

src/comp/Type.hs

Lines changed: 13 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -10,20 +10,20 @@ infixr 4 `fn`
1010

1111
-- XXX these definitions should be synced with StdPrel.hs where applicable
1212

13+
tiData, tiEnum :: [Id] -> TISort
14+
tiEnum cons = TIdata { tidata_cons = cons, tidata_enum = True }
15+
tiData cons = TIdata { tidata_cons = cons, tidata_enum = False }
16+
1317
tArrow, tBit, tInt :: Type
1418
tArrow = TCon (TyCon (idArrow noPosition) (Just (Kfun KStar (Kfun KStar KStar))) TIabstract)
1519
tBit = TCon (TyCon idBit (Just (Kfun KNum KStar)) TIabstract)
16-
tInt = TCon (TyCon idInt (Just (Kfun KNum KStar)) TIabstract)
20+
tInt = TCon (TyCon idInt (Just (Kfun KNum KStar)) (tiData [idInt]))
1721

1822
tIntAt :: Position -> Type
19-
tIntAt pos = TCon (TyCon (idIntAt pos) (Just (Kfun KNum KStar)) TIabstract)
20-
21-
tiData, tiEnum :: [Id] -> TISort
22-
tiEnum cons = TIdata { tidata_cons = cons, tidata_enum = True }
23-
tiData cons = TIdata { tidata_cons = cons, tidata_enum = False }
23+
tIntAt pos = TCon (TyCon (idIntAt pos) (Just (Kfun KNum KStar)) (tiData [idIntAt pos]))
2424

2525
tUInt, tBool, tPrimUnit :: Type
26-
tUInt = TCon (TyCon idUInt (Just (Kfun KNum KStar)) TIabstract)
26+
tUInt = TCon (TyCon idUInt (Just (Kfun KNum KStar)) (tiData [idUInt]))
2727
tBool = TCon (TyCon idBool (Just KStar) (tiEnum [idFalse, idTrue]))
2828
--tArray = TCon (TyCon idArray (Just (Kfun KNum (Kfun KNum KStar))) (TIstruct SInterface [id_sub, id_upd]))
2929
tPrimUnit = TCon (TyCon idPrimUnit (Just KStar) (TIstruct SStruct []))
@@ -55,18 +55,18 @@ tType = TCon (TyCon idType (Just KStar) TIabstract)
5555
tPred, tAttributes, tPrimPair :: Type
5656
tPred = TCon (TyCon idPred (Just KStar) TIabstract)
5757
tAttributes = TCon (TyCon idAttributes (Just KStar) TIabstract)
58-
tPrimPair = TCon (TyCon idPrimPair (Just (Kfun KStar (Kfun KStar KStar))) (TIstruct SStruct [idPrimFst, idPrimSnd]))
58+
tPrimPair = TCon (TyCon idPrimPair (Just (Kfun KStar (Kfun KStar KStar))) (TIstruct (SInterface []) [idPrimFst, idPrimSnd]))
5959

6060
tAction, tActionValue, tActionValue_, tAction_:: Type
6161
tAction = TCon (TyCon idAction (Just KStar) (TItype 0 (TAp tActionValue tPrimUnit)))
62-
tActionValue = TCon (TyCon idActionValue (Just (Kfun KStar KStar)) (TIstruct SStruct [id__value, id__action]))
63-
tActionValue_ = TCon (TyCon idActionValue_ (Just (Kfun KStar KStar)) (TIstruct SStruct [id__value, id__action]))
62+
tActionValue = TCon (TyCon idActionValue (Just (Kfun KStar KStar)) (tiData [idActionValue]))
63+
tActionValue_ = TCon (TyCon idActionValue_ (Just (Kfun KStar KStar)) (TIstruct SStruct [idAVValue_, idAVAction_]))
6464
tAction_ = TAp tActionValue_ tPrimUnit
6565

6666
tActionAt, tActionValueAt, tActionValue_At :: Position -> Type
6767
tActionAt pos = TCon (TyCon (idActionAt pos) (Just KStar) (TItype 0 (TAp (tActionValueAt pos) (tPrimUnitAt pos))))
68-
tActionValueAt pos = TCon (TyCon (idActionValueAt pos) (Just (Kfun KStar KStar)) (TIstruct SStruct [id__value_at pos, id__action_at pos]))
69-
tActionValue_At pos = TCon (TyCon (idActionValue_At pos) (Just (Kfun KStar KStar)) (TIstruct SStruct [id__value_at pos, id__action_at pos]))
68+
tActionValueAt pos = TCon (TyCon (idActionValueAt pos) (Just (Kfun KStar KStar)) (tiData [idActionValueAt pos]))
69+
tActionValue_At pos = TCon (TyCon (idActionValue_At pos) (Just (Kfun KStar KStar)) (TIstruct SStruct [idAVValue_at pos, idAVAction_at pos]))
7070

7171
tPrimAction, tRules :: Type
7272
tPrimAction = TCon (TyCon idPrimAction (Just KStar) TIabstract)
@@ -98,7 +98,7 @@ tNat :: Position -> Type
9898
tNat pos = tBitN 32 pos
9999

100100
tFile, tSvaParam :: Type
101-
tFile = TCon (TyCon idFile (Just KStar) TIabstract)
101+
tFile = TCon (TyCon idFile (Just KStar) (tiData [idInvalidFile, idMCD, idFD]))
102102
tSvaParam = TCon (TyCon idSvaParam (Just KStar) (tiData [idSvaBool, idSvaNumber]))
103103

104104
fn :: Type -> Type -> Type

src/comp/tconcheck.hs

Lines changed: 11 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -63,35 +63,19 @@ exemptMissing :: [(Id, String)]
6363
exemptMissing = []
6464

6565
-- Entries confirmed to drift from the Prelude truth, pending direction on
66-
-- the fix. These are reported loudly (as DRIFT-WAIVED) but do not fail
67-
-- the check, so that the build stays green while the fix is decided.
68-
-- This list should shrink to empty over time; do NOT add new entries to
69-
-- paper over a check failure.
66+
-- the fix. Waived entries are reported loudly (as DRIFT-WAIVED) but do
67+
-- not fail the check, so that the build can stay green while a fix is
68+
-- decided. Keep this list EMPTY; do NOT add entries to paper over a
69+
-- check failure.
7070
--
71-
-- All of the entries below are pre-existing: they have been masked for
72-
-- years by the fact that TyCon Eq/Ord ignore the sort and ITCon
73-
-- comparisons ignore both kind and sort (see CType.hs and IType.hs).
71+
-- (The nine pre-existing drifts this checker originally found -- masked
72+
-- for years by the payload-ignoring TyCon/ITCon comparisons -- were
73+
-- fixed in the commit that emptied this list: Int/UInt/File/ActionValue
74+
-- sorts, ActionValue_ field names, PrimPair's SInterface sort, itInout's
75+
-- kind, itPrimPair's kind via the IKFun fixity declaration, and
76+
-- BufferMode's enum flag.)
7477
knownDrift :: [(String, String)] -- (section ++ " " ++ name, reason)
75-
knownDrift =
76-
[ ("Type Prelude.Int",
77-
"Prelude.bs declares 'data Int n = Int (Bit n)'; handwritten sort predates it (TIabstract)")
78-
, ("Type Prelude.UInt",
79-
"Prelude.bs declares 'data UInt n = UInt (Bit n)'; handwritten sort predates it (TIabstract)")
80-
, ("Type Prelude.PrimPair",
81-
"Prelude.bs declares PrimPair as an interface (TIstruct (SInterface []) ...); handwritten sort says SStruct")
82-
, ("Type Prelude.ActionValue",
83-
"Prelude.bs declares 'data ActionValue a = ActionValue ...'; handwritten sort is the old struct representation")
84-
, ("Type Prelude.ActionValue_",
85-
"ActionValue_ field names are avValue_/avAction_ in Prelude.bs; handwritten sort has the old __value/__action")
86-
, ("Type Prelude.File",
87-
"Prelude.bs declares 'data File = InvalidFile | MCD .. | FD ..'; handwritten sort predates it (TIabstract)")
88-
, ("ISyntaxUtil Prelude.Inout",
89-
"itInout has kind # -> * (apparently copied from itInout_); Inout's kind is * -> *")
90-
, ("ISyntaxUtil Prelude.PrimPair",
91-
"itPrimPair's kind is left-nested, (* -> *) -> *, because IKFun has no fixity declaration (defaults to infixl 9); also the SStruct-vs-SInterface sort, as in Type.hs")
92-
, ("ISyntaxUtil Prelude.BufferMode",
93-
"BlockBuffering carries a Maybe Integer argument, so BufferMode is not an enum; tiBufferMode says tiEnum")
94-
]
78+
knownDrift = []
9579

9680
-- -------------------------
9781
-- Verdicts

0 commit comments

Comments
 (0)