Verify handwritten tycon constants against the Prelude (tconcheck); qualification-scoped tycon comparison

src/Libraries/Makefile

@@ -23,14 +23,21 @@ BUILD_ORDER= \
 # Find files to build tags
 SRCS = $(shell find . -name "*.bsv")
 
-.PHONY: all install clean full_clean
+.PHONY: all build tconcheck install clean full_clean
 
 all: install TAGS
 
 build:
 	$(foreach dir, $(BUILD_ORDER), $(MAKE) -C $(dir) $@ &&) true
 
-install: build
+# Check that the compiler's handwritten tycon constants agree with the
+# just-built Prelude (see src/comp/tconcheck.hs); drift fails the build
+TCONCHECK ?= $(BINDIR)/tconcheck
+
+tconcheck: build
+	$(TCONCHECK) $(BUILDDIR)
+
+install: build tconcheck
 	install -d $(INSTALLDIR)
 	install -m644 $(BUILDDIR)/* $(INSTALLDIR)
 

src/comp/.gitignore

@@ -18,6 +18,7 @@ bsc2bsv
 bsv2bsc
 showrules
 vcdcheck
+tconcheck
 
 # Ignore TAGS files
 TAGS

src/comp/CType.hs

@@ -201,12 +201,39 @@ instance Eq Type where
 instance Eq TyVar where
     TyVar i n _ == TyVar i' n' _  =  (n, i) == (n', i')
 
+-- TyCon comparison and the one-tycon-per-qualified-name invariant
+--
+-- BSC's front end enforces one type constructor per qualified name, so a
+-- qualified Id determines its (kind, sort) payload.  The invariant holds
+-- ONLY for qualified names: unqualified TyCons exist during scope
+-- resolution, where the same base name may denote different constructors.
+-- The tconcheck build step (src/comp/tconcheck.hs) verifies the compiler's
+-- handwritten copies of Prelude tycon payloads against the compiled
+-- Prelude, keeping the invariant checkable.
+--
+-- Eq is therefore scoped by qualification:
+--  * both ids qualified: the invariant's regime.  Comparison is by Id;
+--    the payloads are determined by the name (checker-verified), so a
+--    payload comparison would be a dead tail.
+--  * either id unqualified: resolution-era fuzz, where the invariant is
+--    undefined; the kind comparison is kept as a hedge.
+--
+-- Two pre-existing quirks, both deliberate and unchanged:
+--  * Eq is non-transitive: qualEq compares by base name alone when either
+--    side is unqualified, so P.T == T and T == Q.T but P.T /= Q.T.
+--  * Eq and Ord disagree: Ord compares the full qualifier on both sides
+--    (a lawful total order), while Eq admits the qualEq fuzz.  Containers
+--    key on Ord.
 instance Eq TyCon where
-    TyCon i k _ == TyCon i' k' _  =  qualEq i i' && k == k'
+    TyCon i k _ == TyCon i' k' _  =  qualEq i i' && (bothQualified i i' || k == k')
     TyNum i _   == TyNum i' _     =  i == i'
     TyStr s _   == TyStr s' _     =  s == s'
     _           == _              =  False
 
+-- both ids carry a package qualifier (see the invariant note above)
+bothQualified :: Id -> Id -> Bool
+bothQualified i i' = not (isUnqualId i) && not (isUnqualId i')
+
 -- Ord instances
 
 instance Ord Type where
@@ -220,7 +247,15 @@ instance Ord TyVar where
     TyVar i n _ `compare` TyVar i' n' _  =  (n, i) `compare` (n', i')
 
 instance Ord TyCon where
-    TyCon i k _ `compare` TyCon i' k' _   =  (getIdBase i, getIdQual i, k) `compare` (getIdBase i', getIdQual i', k')
+    -- lexicographic on (base, qual); within a (base, qual) bucket either
+    -- both ids are qualified -- unique by the invariant documented at Eq,
+    -- so EQ without consulting the kinds -- or both are unqualified, where
+    -- the kind comparison is kept, as in Eq.  This remains a lawful total
+    -- order.
+    TyCon i k _ `compare` TyCon i' k' _   =
+        case (getIdBase i, getIdQual i) `compare` (getIdBase i', getIdQual i') of
+          EQ -> if bothQualified i i' then EQ else compare k k'
+          o  -> o
     TyCon _ _ _ `compare` TyNum _  _      =  LT
     TyCon _ _ _ `compare` TyStr _  _      =  LT
     TyNum _ _   `compare` TyCon _  _  _   =  GT

src/comp/IConv.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE RankNTypes, ScopedTypeVariables, PatternGuards #-}
 module IConv(
-             iConvPackage, iConvT, iConvExpr, iConvSc, iConvDef,
+             iConvPackage, iConvT, iConvK, iConvExpr, iConvSc, iConvDef,
              lookupSelType
             ) where
 

src/comp/IExpand.hs

@@ -28,7 +28,6 @@ import Control.Monad.Fix(mfix)
 --import Control.Monad.Fix
 import Control.Monad.State(State, evalState, liftIO, get, put)
 import Data.Graph
-import qualified Data.Generics as Generic
 import System.IO(Handle, BufferMode(..), IOMode(..), stdout, stderr,
                  hSetBuffering, hIsOpen, hIsClosed)
 import System.FilePath(isRelative)
@@ -532,14 +531,114 @@ unpack_method_call' _ e =
   -- trace ("unpack_method_call unable to match " ++ show e) $
   --[(mk_homeless_id "NOSTATE", mk_homeless_id "NOMETHOD")]
 
+-- Apply 'removeIdInlinedPositions' to the Id of every ICon reachable
+-- in the IModule.  Heap references are leaves: IRefT payloads and the
+-- cells of ICLazyArray sit behind IORefs and are not traversed.
+-- Clock, reset and inout wires can be cyclic (a state variable's
+-- output clock selects from the state variable itself), so the
+-- rebuilding must stay lazy; consumers only force finite prefixes of
+-- such wires.  Subtrees that cannot contain an ICon are returned
+-- unchanged, rather than reallocated.
 removeInlinedPositions :: Flags -> IModule HeapData -> IModule HeapData
 removeInlinedPositions flags imod0 | (not (methodConditions flags)) = imod0
 removeInlinedPositions flags imod0 =
-    let removeFn :: HExpr -> HExpr
-        removeFn (ICon i ic) = (ICon (removeIdInlinedPositions i) ic)
-        -- XXX do we need a recursive branch for IAps?
-        removeFn e = e
-    in  Generic.everywhere (Generic.mkT removeFn) imod0
+    imod0 { imod_clock_domains =
+                [ (d, map rmClock cs) | (d, cs) <- imod_clock_domains imod0 ],
+            imod_resets = map rmReset (imod_resets imod0),
+            imod_state_insts =
+                [ (i, rmStateVar sv) | (i, sv) <- imod_state_insts imod0 ],
+            imod_local_defs = map rmDef (imod_local_defs imod0),
+            imod_rules = rmRules (imod_rules imod0),
+            imod_interface = map rmIFace (imod_interface imod0)
+          }
+  where
+    rmExpr :: HExpr -> HExpr
+    rmExpr (ILam i t e) = ILam i t (rmExpr e)
+    rmExpr (IAps f ts es) = IAps (rmExpr f) ts (map rmExpr es)
+    rmExpr e@(IVar _) = e
+    rmExpr (ILAM i k e) = ILAM i k (rmExpr e)
+    rmExpr (ICon i ic) = ICon (removeIdInlinedPositions i) (rmConInfo ic)
+    rmExpr e@(IRefT _ _ _ _) = e
+
+    -- only the payloads that can carry an IExpr are rebuilt;
+    -- all other constructors are returned unchanged
+    rmConInfo :: IConInfo HeapData -> IConInfo HeapData
+    rmConInfo (ICDef t d) = ICDef t (rmExpr d)
+    rmConInfo (ICUndet t k mv) = ICUndet t k (fmap rmExpr mv)
+    rmConInfo (ICStateVar t sv) = ICStateVar t (rmStateVar sv)
+    rmConInfo (ICValue t d) = ICValue t (rmExpr d)
+    rmConInfo (ICMethod t ins outs m) = ICMethod t ins outs (rmExpr m)
+    rmConInfo (ICClock t c) = ICClock t (rmClock c)
+    rmConInfo (ICReset t r) = ICReset t (rmReset r)
+    rmConInfo (ICInout t io) = ICInout t (rmInout io)
+    rmConInfo (ICLazyArray t arr mu) =
+        -- the array cells are heap references, thus leaves
+        ICLazyArray t arr (fmap (\ (e1, e2) -> (rmExpr e1, rmExpr e2)) mu)
+    rmConInfo (ICPred t p) = ICPred t (rmPred p)
+    rmConInfo ic@(ICPrim {}) = ic
+    rmConInfo ic@(ICForeign {}) = ic
+    rmConInfo ic@(ICCon {}) = ic
+    rmConInfo ic@(ICIs {}) = ic
+    rmConInfo ic@(ICOut {}) = ic
+    rmConInfo ic@(ICTuple {}) = ic
+    rmConInfo ic@(ICSel {}) = ic
+    rmConInfo ic@(ICVerilog {}) = ic
+    rmConInfo ic@(ICInt {}) = ic
+    rmConInfo ic@(ICReal {}) = ic
+    rmConInfo ic@(ICString {}) = ic
+    rmConInfo ic@(ICChar {}) = ic
+    rmConInfo ic@(ICHandle {}) = ic
+    rmConInfo ic@(ICMethArg {}) = ic
+    rmConInfo ic@(ICModPort {}) = ic
+    rmConInfo ic@(ICModParam {}) = ic
+    rmConInfo ic@(ICIFace {}) = ic
+    rmConInfo ic@(ICRuleAssert {}) = ic
+    rmConInfo ic@(ICSchedPragmas {}) = ic
+    rmConInfo ic@(ICName {}) = ic
+    rmConInfo ic@(ICAttrib {}) = ic
+    rmConInfo ic@(ICPosition {}) = ic
+    rmConInfo ic@(ICType {}) = ic
+
+    rmClock :: HClock -> HClock
+    rmClock c = c { ic_wires = rmExpr (ic_wires c) }
+
+    rmReset :: HReset -> HReset
+    rmReset r = r { ir_clock = rmClock (ir_clock r),
+                    ir_wire = rmExpr (ir_wire r) }
+
+    rmInout :: HInout -> HInout
+    rmInout io = io { io_clock = rmClock (io_clock io),
+                      io_reset = rmReset (io_reset io),
+                      io_wire = rmExpr (io_wire io) }
+
+    rmStateVar :: HStateVar -> HStateVar
+    rmStateVar sv =
+        sv { isv_iargs = map rmExpr (isv_iargs sv),
+             isv_clocks = [ (i, rmClock c) | (i, c) <- isv_clocks sv ],
+             isv_resets = [ (i, rmReset r) | (i, r) <- isv_resets sv ] }
+
+    rmPred :: HPred -> HPred
+    rmPred (PConj ps) = PConj (S.map rmPTerm ps)
+
+    rmPTerm :: PTerm HeapData -> PTerm HeapData
+    rmPTerm (PAtom e) = PAtom (rmExpr e)
+    rmPTerm (PIf c t e) = PIf (rmExpr c) (rmPred t) (rmPred e)
+    rmPTerm (PSel idx sz ps) = PSel (rmExpr idx) sz (map rmPred ps)
+
+    rmDef :: HDef -> HDef
+    rmDef (IDef i t e p) = IDef i t (rmExpr e) p
+
+    rmRules :: HRules -> HRules
+    rmRules (IRules sps rs) = IRules sps (map rmRule rs)
+
+    rmRule :: HRule -> HRule
+    rmRule r = r { irule_pred = rmExpr (irule_pred r),
+                   irule_body = rmExpr (irule_body r) }
+
+    rmIFace :: HEFace -> HEFace
+    rmIFace ief =
+        ief { ief_value = fmap (\ (e, t) -> (rmExpr e, t)) (ief_value ief),
+              ief_body = fmap rmRules (ief_body ief) }
 
 -- -----
 

src/comp/IExpandUtils.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ImplicitParams #-}
 module IExpandUtils(
@@ -77,7 +77,6 @@ import Debug.Trace(traceM)
 import qualified Data.Array as Array
 import qualified Data.Map as M
 import qualified Data.Set as S
-import qualified Data.Generics as Generic
 
 import Eval
 import PPrint
@@ -273,7 +272,7 @@ pTermToIExpr (PSel idx idx_sz es) =
 
 -- An expression with an implicit condition.
 data PExpr = P !HPred HExpr
-        deriving (Eq, Ord, Show, Generic.Data, Generic.Typeable)
+        deriving (Eq, Ord, Show)
 
 instance PPrint PExpr where
     pPrint d prec (P p e) = pPrint d prec (iePrimWhen (iGetType e) (predToIExpr p) e)
@@ -413,7 +412,7 @@ data HeapCell = HUnev { hc_hexpr :: HExpr, hc_name :: NameInfo }
               | HNF { hc_pexpr :: PExpr, hc_wire_set :: HWireSet,
                       hc_name :: NameInfo }
               | HLoop { hc_name :: NameInfo }
-        deriving (Show, Eq, Ord, Generic.Data, Generic.Typeable)
+        deriving (Show, Eq, Ord)
 
 -- should I drop the predicate for better printing of error messages?
 heapCellToHExpr :: HeapCell -> HExpr
@@ -442,7 +441,6 @@ instance PPrint HeapCell where
             text "HLoop" <+> pPrint d 0 name
 
 newtype HeapData = HeapData (IORef (HeapCell))
-  deriving (Generic.Data, Generic.Typeable)
 
 {-
 instance Eq HeapData where