[commit: ghc] type-nats: Remove the unique from CoAxiomRule. (c7ff122)

[Simon Peyton-Jones]

I'm dubious about this, Iavor.  A Name (which is still in your AxiomRule) still contains a Unique; the unique was previously only cached from the name.  If you need infinite families, maybe they should be anonymous.  And if you need an infinite family, why not instead make the lit into an *argument* of the rule axiom?

Simon

| -----Original Message-----
| From: cvs-ghc-bounces at haskell.org [mailto:cvs-ghc-bounces at haskell.org]
| On Behalf Of Iavor Diatchki
| Sent: 02 July 2012 05:26
| To: cvs-ghc at haskell.org
| Subject: [commit: ghc] type-nats: Remove the unique from CoAxiomRule.
| (c7ff122)
| 
| Repository : ssh://darcs.haskell.org//srv/darcs/ghc
| 
| On branch  : type-nats
| 
| http://hackage.haskell.org/trac/ghc/changeset/c7ff12269aa64c38437e10eaa
| 2aeeb888d3d9cf9
| 
| >---------------------------------------------------------------
| 
| commit c7ff12269aa64c38437e10eaa2aeeb888d3d9cf9
| Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
| Date:   Sun Jul 1 21:03:42 2012 -0700
| 
|     Remove the unique from CoAxiomRule.
| 
|     There are two reasons for this:
|       * The unique was not used for anything,
|       * It was incorrect for the infinite families of definitional
| axioms
|         (e.g., 2 + 3 = 5 and 2 + 4 = 6 both got the same unique)
| 
| >---------------------------------------------------------------
| 
|  compiler/typecheck/TcTypeNatsRules.hs |   37 +++++++++++++++----------
| -------
|  compiler/types/Coercion.lhs           |    3 +-
|  2 files changed, 18 insertions(+), 22 deletions(-)
| 
| diff --git a/compiler/typecheck/TcTypeNatsRules.hs
| b/compiler/typecheck/TcTypeNatsRules.hs
| index 0fd2d5c..c99a19c 100644
| --- a/compiler/typecheck/TcTypeNatsRules.hs
| +++ b/compiler/typecheck/TcTypeNatsRules.hs
| @@ -13,7 +13,6 @@ import TysPrim  ( typeNatAddTyCon
|                  )
|  import Name     ( mkSystemName )
|  import OccName  ( mkOccName, tcName )
| -import Unique   ( mkPreludeMiscIdUnique )
| 
| 
| 
| @@ -45,17 +44,15 @@ fRules =
| 
|  ----------------------------------------------------------------------
| ----------
| 
| -mkAx :: Int -> String -> [TyVar] -> [(Type,Type)] -> Type -> Type ->
| CoAxiomRule -mkAx u n vs asmps lhs rhs = CoAxiomRule
| -  { co_axr_unique = mkAxUique u
| -  , co_axr_name   = mkAxName n
| +mkAx :: String -> [TyVar] -> [(Type,Type)] -> Type -> Type ->
| +CoAxiomRule mkAx n vs asmps lhs rhs = CoAxiomRule
| +  { co_axr_name   = mkAxName n
|    , co_axr_tvs    = vs
|    , co_axr_asmps  = asmps
|    , co_axr_lhs    = lhs
|    , co_axr_rhs    = rhs
|    }
|    where
| -  mkAxUique  = mkPreludeMiscIdUnique
|    mkAxName x = mkSystemName unboundKey (mkOccName tcName x)
| 
|  mkAdd :: Type -> Type -> Type
| @@ -77,15 +74,15 @@ axName :: String -> Integer -> Integer -> String
| axName x a b = x ++ "_" ++ show a ++ "_" ++ show b
| 
|  axAddDef :: Integer -> Integer -> CoAxiomRule -axAddDef a b = mkAx 1
| (axName "AddDef" a b) [] []
| +axAddDef a b = mkAx (axName "AddDef" a b) [] []
|               (mkAdd (mkNumLitTy a) (mkNumLitTy b)) (mkNumLitTy (a +
| b))
| 
|  axMulDef :: Integer -> Integer -> CoAxiomRule -axMulDef a b = mkAx 2
| (axName "MulDef" a b) [] []
| +axMulDef a b = mkAx (axName "MulDef" a b) [] []
|               (mkMul (mkNumLitTy a) (mkNumLitTy b)) (mkNumLitTy (a *
| b))
| 
|  axExpDef :: Integer -> Integer -> CoAxiomRule -axExpDef a b = mkAx 3
| (axName "ExpDef" a b) [] []
| +axExpDef a b = mkAx (axName "ExpDef" a b) [] []
|               (mkExp (mkNumLitTy a) (mkNumLitTy b)) (mkNumLitTy (a ^
| b))
| 
| 
| @@ -93,21 +90,21 @@ axExpDef a b = mkAx 3 (axName "ExpDef" a b) [] []
|  -- reasoning too.
|  bRules :: [CoAxiomRule]
|  bRules =
| -  [ bRule 10 "Add0L" (mkAdd n0 a) a
| -  , bRule 11 "Add0R" (mkAdd a n0) a
| +  [ bRule "Add0L" (mkAdd n0 a) a
| +  , bRule "Add0R" (mkAdd a n0) a
| 
| -  , bRule 12 "Mul0L" (mkMul n0 a) n0
| -  , bRule 13 "Mul0R" (mkMul a n0) n0
| -  , bRule 14 "Mul1L" (mkMul n1 a) a
| -  , bRule 15 "Mul1R" (mkMul a n1) a
| +  , bRule "Mul0L" (mkMul n0 a) n0
| +  , bRule "Mul0R" (mkMul a n0) n0
| +  , bRule "Mul1L" (mkMul n1 a) a
| +  , bRule "Mul1R" (mkMul a n1) a
| 
|    -- TnExp0L
| -  , bRule 17 "TnExp0R" (mkExp a n0) n1
| -  , bRule 18 "TnExp1L" (mkExp n1 a) n1
| -  , bRule 19 "TnExp1R" (mkExp a n1) a
| +  , bRule "TnExp0R" (mkExp a n0) n1
| +  , bRule "TnExp1L" (mkExp n1 a) n1
| +  , bRule "TnExp1R" (mkExp a n1) a
|    ]
|    where
| -  bRule x y = mkAx x y (take 1 natVars) []
| +  bRule y   = mkAx y (take 1 natVars) []
|    a : _     = map mkTyVarTy natVars
|    n0        = mkNumLitTy 0
|    n1        = mkNumLitTy 1
| @@ -116,7 +113,7 @@ bRules =
| 
| 
|  axAddComm :: CoAxiomRule
| -axAddComm = mkAx 30 "AddComm" (take 3 natVars) [ (mkAdd a b, c) ]
| (mkAdd b a) c
| +axAddComm = mkAx "AddComm" (take 3 natVars) [ (mkAdd a b, c) ] (mkAdd
| b
| +a) c
|    where a : b : c : _ = map mkTyVarTy natVars
| 
| 
| diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs
| index 7fd8c59..d07bce7 100644
| --- a/compiler/types/Coercion.lhs
| +++ b/compiler/types/Coercion.lhs
| @@ -166,8 +166,7 @@ data Coercion
|  -- In the longer run, it would probably be good to unify this and
| `CoAxiom`,
|  -- as `CoAxiom` is the special case when `co_axr_asmps` is [].
|  data CoAxiomRule = CoAxiomRule
| -  { co_axr_unique   :: Unique
| -  , co_axr_name     :: Name
| +  { co_axr_name     :: Name
|    , co_axr_tvs      :: [TyVar]        -- ^ Quantified variabes
|    , co_axr_asmps    :: [(Type,Type)]  -- ^ Assumptions
|    , co_axr_lhs      :: Type           -- ^ LHS of conclusion
| 
| 
| 
| _______________________________________________
| Cvs-ghc mailing list
| Cvs-ghc at haskell.org
| http://www.haskell.org/mailman/listinfo/cvs-ghc