[Git][ghc/ghc][wip/T24978] Add axiomrules to the list

[Simon Peyton Jones (@simonpj)]

Simon Peyton Jones pushed to branch wip/T24978 at Glasgow Haskell Compiler / GHC


Commits:
71054963 by Simon Peyton Jones at 2024-06-24T11:59:43+01:00
Add axiomrules to the list

- - - - -


1 changed file:

- compiler/GHC/Builtin/Types/Literals.hs


Changes:

=====================================
compiler/GHC/Builtin/Types/Literals.hs
=====================================
@@ -32,7 +32,7 @@ import GHC.Prelude
 import GHC.Core.Type
 import GHC.Data.Pair
 import GHC.Core.TyCon    ( TyCon, FamTyConFlav(..), mkFamilyTyCon
-                         , Injectivity(..) )
+                         , Injectivity(..), isBuiltInSynFamTyCon_maybe )
 import GHC.Core.Coercion.Axiom
 import GHC.Core.TyCo.Compare   ( tcEqType )
 import GHC.Types.Name          ( Name, BuiltInSyntax(..) )
@@ -193,6 +193,57 @@ typeNatTyCons =
   , typeNatToCharTyCon
   ]
 
+
+tyConAxiomRules :: TyCon -> [CoAxiomRule]
+tyConAxiomRules tc
+  | Just ops <- isBuiltInSynFamTyCon_maybe tc
+  = sfInteractTop ops ++ sfInteractInert ops
+  | otherwise
+  = []
+
+-- The list of built-in type family axioms that GHC uses.
+-- If you define new axioms, make sure to include them in this list.
+-- See Note [Adding built-in type families]
+typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
+typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x)) $
+  concatMap tyConAxiomRules typeNatTyCons
+     -- ToDO: tyConAxiomRules should get the sfMatchFam rules too
+  ++
+  [ axAddDef
+  , axMulDef
+  , axExpDef
+  , axCmpNatDef
+  , axCmpSymbolDef
+  , axCmpCharDef
+  , axAppendSymbolDef
+  , axConsSymbolDef
+  , axUnconsSymbolDef
+  , axCharToNatDef
+  , axNatToCharDef
+  , axAdd0L
+  , axAdd0R
+  , axMul0L
+  , axMul0R
+  , axMul1L
+  , axMul1R
+  , axExp1L
+  , axExp0R
+  , axExp1R
+  , axCmpNatRefl
+  , axCmpSymbolRefl
+--  , axCmpCharRefl
+  , axSubDef
+  , axSub0R
+  , axAppendSymbol0R
+  , axAppendSymbol0L
+  , axDivDef
+  , axDiv1
+  , axModDef
+  , axMod1
+  , axLogDef
+  ]
+
+
 -------------------------------------------------------------------------------
 --                   Addition (+)
 -------------------------------------------------------------------------------
@@ -897,46 +948,6 @@ axAppendSymbol0R  = mkAxiom1 "Concat0R"
 axAppendSymbol0L  = mkAxiom1 "Concat0L"
                     $ \(Pair s t) -> (s `appendSymbol` mkStrLitTy nilFS) === t
 
--- The list of built-in type family axioms that GHC uses.
--- If you define new axioms, make sure to include them in this list.
--- See Note [Adding built-in type families]
-typeNatCoAxiomRules :: UniqFM FastString CoAxiomRule
-typeNatCoAxiomRules = listToUFM $ map (\x -> (coaxrName x, x))
-  [ axAddDef
-  , axMulDef
-  , axExpDef
-  , axCmpNatDef
-  , axCmpSymbolDef
-  , axCmpCharDef
-  , axAppendSymbolDef
-  , axConsSymbolDef
-  , axUnconsSymbolDef
-  , axCharToNatDef
-  , axNatToCharDef
-  , axAdd0L
-  , axAdd0R
-  , axMul0L
-  , axMul0R
-  , axMul1L
-  , axMul1R
-  , axExp1L
-  , axExp0R
-  , axExp1R
-  , axCmpNatRefl
-  , axCmpSymbolRefl
---  , axCmpCharRefl
-  , axSubDef
-  , axSub0R
-  , axAppendSymbol0R
-  , axAppendSymbol0L
-  , axDivDef
-  , axDiv1
-  , axModDef
-  , axMod1
-  , axLogDef
-  ]
-
-
 
 {-------------------------------------------------------------------------------
 Various utilities for making axioms and types



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/710549634b170fe97f030c21fa97640de88e226d

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/710549634b170fe97f030c21fa97640de88e226d
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20240624/2094015c/attachment-0001.html>