[commit: ghc] master: Add a primitive for coercing values into dictionaries in a special case. (ac330cb)
Iavor Diatchki
diatchki at galois.com
Thu May 30 18:52:36 CEST 2013
Repository : http://darcs.haskell.org/ghc.git/
On branch : master
https://github.com/ghc/ghc/commit/ac330cb607cde34bca6b6c4cf61d5b05000fe7e7
>---------------------------------------------------------------
commit ac330cb607cde34bca6b6c4cf61d5b05000fe7e7
Author: Iavor S. Diatchki <diatchki at Perun.(none)>
Date: Thu May 30 09:20:00 2013 -0700
Add a primitive for coercing values into dictionaries in a special case.
The details of this are described in Note [magicSingIId magic] in basicTypes/MkId.lhs
>---------------------------------------------------------------
compiler/basicTypes/MkId.lhs | 56 ++++++++++++++++++++++++++++++++++++---
compiler/basicTypes/MkId.lhs-boot | 2 ++
compiler/prelude/PrelNames.lhs | 3 +++
compiler/prelude/PrelRules.lhs | 25 ++++++++++++++---
4 files changed, 80 insertions(+), 6 deletions(-)
diff --git a/compiler/basicTypes/MkId.lhs b/compiler/basicTypes/MkId.lhs
index f475ba8..0021b96 100644
--- a/compiler/basicTypes/MkId.lhs
+++ b/compiler/basicTypes/MkId.lhs
@@ -35,7 +35,7 @@ module MkId (
wiredInIds, ghcPrimIds,
unsafeCoerceName, unsafeCoerceId, realWorldPrimId,
voidArgId, nullAddrId, seqId, lazyId, lazyIdKey,
- coercionTokenId,
+ coercionTokenId, magicSingIId,
-- Re-export error Ids
module PrelRules
@@ -136,7 +136,8 @@ ghcPrimIds
realWorldPrimId,
unsafeCoerceId,
nullAddrId,
- seqId
+ seqId,
+ magicSingIId
]
\end{code}
@@ -1022,13 +1023,14 @@ they can unify with both unlifted and lifted types. Hence we provide
another gun with which to shoot yourself in the foot.
\begin{code}
-lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName :: Name
+lazyIdName, unsafeCoerceName, nullAddrName, seqName, realWorldName, coercionTokenName, magicSingIName :: Name
unsafeCoerceName = mkWiredInIdName gHC_PRIM (fsLit "unsafeCoerce#") unsafeCoerceIdKey unsafeCoerceId
nullAddrName = mkWiredInIdName gHC_PRIM (fsLit "nullAddr#") nullAddrIdKey nullAddrId
seqName = mkWiredInIdName gHC_PRIM (fsLit "seq") seqIdKey seqId
realWorldName = mkWiredInIdName gHC_PRIM (fsLit "realWorld#") realWorldPrimIdKey realWorldPrimId
lazyIdName = mkWiredInIdName gHC_MAGIC (fsLit "lazy") lazyIdKey lazyId
coercionTokenName = mkWiredInIdName gHC_PRIM (fsLit "coercionToken#") coercionTokenIdKey coercionTokenId
+magicSingIName = mkWiredInIdName gHC_PRIM (fsLit "magicSingI") magicSingIKey magicSingIId
\end{code}
\begin{code}
@@ -1094,6 +1096,15 @@ lazyId = pcMiscPrelId lazyIdName ty info
where
info = noCafIdInfo
ty = mkForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy)
+
+
+--------------------------------------------------------------------------------
+magicSingIId :: Id -- See Note [magicSingIId magic]
+magicSingIId = pcMiscPrelId magicSingIName ty info
+ where
+ info = noCafIdInfo `setInlinePragInfo` neverInlinePragma
+ ty = mkForAllTys [alphaTyVar] alphaTy
+
\end{code}
Note [Unsafe coerce magic]
@@ -1187,6 +1198,45 @@ See Trac #3259 for a real world example.
lazyId is defined in GHC.Base, so we don't *have* to inline it. If it
appears un-applied, we'll end up just calling it.
+
+Note [magicSingIId magic]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The identifier `magicSIngI` is just a place-holder, which is used to
+implement a primitve that we cannot define in Haskell but we can write
+in Core. It is declared with a place-holder type:
+
+ magicSingI :: forall a. a
+
+The intention is that the identifier will be used in a very specific way,
+namely we add the following to the library:
+
+ withSingI :: Sing n -> (SingI n => a) -> a
+ withSingI x = magicSingI x ((\f -> f) :: () -> ())
+
+The actual primitive is `withSingI`, and it uses its first argument
+(of type `Sing n`) as the evidece/dictionary in the second argument.
+This is done by adding a built-in rule to `prelude/PrelRules.hs`
+(see `match_magicSingI`), which works as follows:
+
+magicSingI @ (Sing n -> (() -> ()) -> (SingI n -> a) -> a)
+ x
+ (\f -> _)
+
+---->
+
+\(f :: (SingI n -> a) -> a) -> f (cast x (newtypeCo n))
+
+The `newtypeCo` coercion is extracted from the `SingI` type constructor,
+which is available in the instantiation. We are casting `Sing n` into `SingI n`,
+which is OK because `SingI` is a class with a single methid,
+and thus it is implemented as newtype.
+
+The `(\f -> f)` parameter is there just so that we can avoid
+having to make up a new name for the lambda, it is completely
+changed by the rewrite.
+
+
-------------------------------------------------------------
@realWorld#@ used to be a magic literal, \tr{void#}. If things get
nasty as-is, change it back to a literal (@Literal@).
diff --git a/compiler/basicTypes/MkId.lhs-boot b/compiler/basicTypes/MkId.lhs-boot
index 201f977..fe66599 100644
--- a/compiler/basicTypes/MkId.lhs-boot
+++ b/compiler/basicTypes/MkId.lhs-boot
@@ -9,6 +9,8 @@ data DataConBoxer
mkDataConWorkId :: Name -> DataCon -> Id
mkPrimOpId :: PrimOp -> Id
+
+magicSingIId :: Id
\end{code}
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index fe1e8b1..2d795ab 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -1686,6 +1686,9 @@ checkDotnetResNameIdKey = mkPreludeMiscIdUnique 154
undefinedKey :: Unique
undefinedKey = mkPreludeMiscIdUnique 155
+
+magicSingIKey :: Unique
+magicSingIKey = mkPreludeMiscIdUnique 156
\end{code}
Certain class operations from Prelude classes. They get their own
diff --git a/compiler/prelude/PrelRules.lhs b/compiler/prelude/PrelRules.lhs
index 05e58e4..50730e2 100644
--- a/compiler/prelude/PrelRules.lhs
+++ b/compiler/prelude/PrelRules.lhs
@@ -20,17 +20,18 @@ module PrelRules ( primOpRules, builtinRules ) where
#include "HsVersions.h"
#include "../includes/MachDeps.h"
-import {-# SOURCE #-} MkId ( mkPrimOpId )
+import {-# SOURCE #-} MkId ( mkPrimOpId, magicSingIId )
import CoreSyn
import MkCore
import Id
+import Var (setVarType)
import Literal
import CoreSubst ( exprIsLiteral_maybe )
import PrimOp ( PrimOp(..), tagToEnumKey )
import TysWiredIn
import TysPrim
-import TyCon ( tyConDataCons_maybe, isEnumerationTyCon, isNewTyCon )
+import TyCon ( tyConDataCons_maybe, isEnumerationTyCon, isNewTyCon, unwrapNewTyCon_maybe )
import DataCon ( dataConTag, dataConTyCon, dataConWorkId )
import CoreUtils ( cheapEqExpr, exprIsHNF )
import CoreUnfold ( exprIsConApp_maybe )
@@ -46,6 +47,7 @@ import BasicTypes
import DynFlags
import Platform
import Util
+import Coercion (mkUnbranchedAxInstCo)
import Control.Monad
import Data.Bits as Bits
@@ -816,7 +818,10 @@ builtinRules
BuiltinRule { ru_name = fsLit "EqString", ru_fn = eqStringName,
ru_nargs = 2, ru_try = \_ _ _ -> match_eq_string },
BuiltinRule { ru_name = fsLit "Inline", ru_fn = inlineIdName,
- ru_nargs = 2, ru_try = \_ _ _ -> match_inline }]
+ ru_nargs = 2, ru_try = \_ _ _ -> match_inline },
+ BuiltinRule { ru_name = fsLit "MagicSingI", ru_fn = idName magicSingIId,
+ ru_nargs = 3, ru_try = \_ _ _ -> match_magicSingI }
+ ]
++ builtinIntegerRules
builtinIntegerRules :: [CoreRule]
@@ -984,6 +989,20 @@ match_inline (Type _ : e : _)
match_inline _ = Nothing
+
+-- See Note [magicSingIId magic] in `basicTypes/MkId.lhs`
+-- for a description of what is going on here.
+match_magicSingI :: [Expr CoreBndr] -> Maybe (Expr CoreBndr)
+match_magicSingI (Type t : e : Lam b _ : _)
+ | ([_,_,fu],_) <- splitFunTys t
+ , (sI_type,_) <- splitFunTy fu
+ , Just (sI_tc,xs) <- splitTyConApp_maybe sI_type
+ , Just (_,_,co) <- unwrapNewTyCon_maybe sI_tc
+ = Just $ let f = setVarType b fu
+ in Lam f $ Var f `App` Cast e (mkUnbranchedAxInstCo co xs)
+
+match_magicSingI _ = Nothing
+
-------------------------------------------------
-- Integer rules
-- smallInteger (79::Int#) = 79::Integer
More information about the ghc-commits
mailing list