diff options
Diffstat (limited to 'compiler/coreSyn')
| -rw-r--r-- | compiler/coreSyn/CoreLint.lhs | 123 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreSubst.lhs | 8 | ||||
| -rw-r--r-- | compiler/coreSyn/CoreUtils.lhs | 16 | ||||
| -rw-r--r-- | compiler/coreSyn/ExternalCore.lhs | 29 | ||||
| -rw-r--r-- | compiler/coreSyn/MkExternalCore.lhs | 24 | ||||
| -rw-r--r-- | compiler/coreSyn/PprExternalCore.lhs | 60 | ||||
| -rw-r--r-- | compiler/coreSyn/TrieMap.lhs | 82 |
7 files changed, 224 insertions, 118 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index f9256e18ad..5befacdd45 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -24,7 +24,6 @@ import Demand import CoreSyn import CoreFVs import CoreUtils -import Pair import Bag import Literal import DataCon @@ -306,7 +305,8 @@ lintCoreExpr (Lit lit) lintCoreExpr (Cast expr co) = do { expr_ty <- lintCoreExpr expr ; co' <- applySubstCo co - ; (_, from_ty, to_ty) <- lintCoercion co' + ; (_, from_ty, to_ty, r) <- lintCoercion co' + ; checkRole co' Representational r ; checkTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty) ; return to_ty } @@ -400,9 +400,9 @@ lintCoreExpr (Type ty) = pprPanic "lintCoreExpr" (ppr ty) lintCoreExpr (Coercion co) - = do { co' <- lintInCo co - ; let Pair ty1 ty2 = coercionKind co' - ; return (mkCoercionType ty1 ty2) } + = do { (_kind, ty1, ty2, role) <- lintInCo co + ; checkRole co Nominal role + ; return (mkCoercionType role ty1 ty2) } \end{code} @@ -804,49 +804,56 @@ lint_app doc kfn kas %************************************************************************ \begin{code} -lintInCo :: InCoercion -> LintM OutCoercion +lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role) -- Check the coercion, and apply the substitution to it -- See Note [Linting type lets] lintInCo co = addLoc (InCo co) $ do { co' <- applySubstCo co - ; _ <- lintCoercion co' - ; return co' } + ; lintCoercion co' } -lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType) +lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role) -- Check the kind of a coercion term, returning the kind -- Post-condition: the returned OutTypes are lint-free -- and have the same kind as each other -- If you edit this function, you may need to update the GHC formalism -- See Note [GHC Formalism] -lintCoercion (Refl ty) +lintCoercion (Refl r ty) = do { k <- lintType ty - ; return (k, ty, ty) } + ; return (k, ty, ty, r) } -lintCoercion co@(TyConAppCo tc cos) +lintCoercion co@(TyConAppCo r tc cos) | tc `hasKey` funTyConKey , [co1,co2] <- cos - = do { (k1,s1,t1) <- lintCoercion co1 - ; (k2,s2,t2) <- lintCoercion co2 + = do { (k1,s1,t1,r1) <- lintCoercion co1 + ; (k2,s2,t2,r2) <- lintCoercion co2 ; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2 - ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2) } + ; checkRole co1 r r1 + ; checkRole co2 r r2 + ; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) } | otherwise - = do { (ks,ss,ts) <- mapAndUnzip3M lintCoercion cos + = do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos ; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks) - ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts) } + ; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs + ; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) } lintCoercion co@(AppCo co1 co2) - = do { (k1,s1,t1) <- lintCoercion co1 - ; (k2,s2,t2) <- lintCoercion co2 + = do { (k1,s1,t1,r1) <- lintCoercion co1 + ; (k2,s2,t2,r2) <- lintCoercion co2 ; rk <- lint_co_app co k1 [(s2,k2)] - ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2) } + ; if r1 == Phantom + then checkL (r2 == Phantom || r2 == Nominal) + (ptext (sLit "Second argument in AppCo cannot be R:") $$ + ppr co) + else checkRole co Nominal r2 + ; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) } lintCoercion (ForAllCo tv co) = do { lintTyBndrKind tv - ; (k, s, t) <- addInScopeVar tv (lintCoercion co) - ; return (k, mkForAllTy tv s, mkForAllTy tv t) } + ; (k, s, t, r) <- addInScopeVar tv (lintCoercion co) + ; return (k, mkForAllTy tv s, mkForAllTy tv t, r) } lintCoercion (CoVarCo cv) | not (isCoVar cv) @@ -857,52 +864,58 @@ lintCoercion (CoVarCo cv) ; cv' <- lookupIdInScope cv ; let (s,t) = coVarKind cv' k = typeKind s + r = coVarRole cv' ; when (isSuperKind k) $ - checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality")) - 2 (ppr cv)) - ; return (k, s, t) } + do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality")) + 2 (ppr cv)) + ; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality")) + 2 (ppr cv)) } + ; return (k, s, t, r) } -lintCoercion (UnsafeCo ty1 ty2) +lintCoercion (UnivCo r ty1 ty2) = do { k1 <- lintType ty1 ; _k2 <- lintType ty2 -- ; unless (k1 `eqKind` k2) $ -- failWithL (hang (ptext (sLit "Unsafe coercion changes kind")) -- 2 (ppr co)) - ; return (k1, ty1, ty2) } + ; return (k1, ty1, ty2, r) } lintCoercion (SymCo co) - = do { (k, ty1, ty2) <- lintCoercion co - ; return (k, ty2, ty1) } + = do { (k, ty1, ty2, r) <- lintCoercion co + ; return (k, ty2, ty1, r) } lintCoercion co@(TransCo co1 co2) - = do { (k1, ty1a, ty1b) <- lintCoercion co1 - ; (_, ty2a, ty2b) <- lintCoercion co2 + = do { (k1, ty1a, ty1b, r1) <- lintCoercion co1 + ; (_, ty2a, ty2b, r2) <- lintCoercion co2 ; checkL (ty1b `eqType` ty2a) (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co) 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b])) - ; return (k1, ty1a, ty2b) } + ; checkRole co r1 r2 + ; return (k1, ty1a, ty2b, r1) } lintCoercion the_co@(NthCo n co) - = do { (_,s,t) <- lintCoercion co + = do { (_,s,t,r) <- lintCoercion co ; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of (Just (tc_s, tys_s), Just (tc_t, tys_t)) | tc_s == tc_t , tys_s `equalLength` tys_t , n < length tys_s - -> return (ks, ts, tt) + -> return (ks, ts, tt, tr) where ts = getNth tys_s n tt = getNth tys_t n + tr = nthRole r tc_s n ks = typeKind ts _ -> failWithL (hang (ptext (sLit "Bad getNth:")) 2 (ppr the_co $$ ppr s $$ ppr t)) } lintCoercion the_co@(LRCo lr co) - = do { (_,s,t) <- lintCoercion co + = do { (_,s,t,r) <- lintCoercion co + ; checkRole co Nominal r ; case (splitAppTy_maybe s, splitAppTy_maybe t) of (Just s_pr, Just t_pr) - -> return (k, s_pick, t_pick) + -> return (k, s_pick, t_pick, Nominal) where s_pick = pickLR lr s_pr t_pick = pickLR lr t_pr @@ -912,13 +925,13 @@ lintCoercion the_co@(LRCo lr co) 2 (ppr the_co $$ ppr s $$ ppr t)) } lintCoercion (InstCo co arg_ty) - = do { (k,s,t) <- lintCoercion co - ; arg_kind <- lintType arg_ty + = do { (k,s,t,r) <- lintCoercion co + ; arg_kind <- lintType arg_ty ; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of (Just (tv1,ty1), Just (tv2,ty2)) | arg_kind `isSubKind` tyVarKind tv1 -> return (k, substTyWith [tv1] [arg_ty] ty1, - substTyWith [tv2] [arg_ty] ty2) + substTyWith [tv2] [arg_ty] ty2, r) | otherwise -> failWithL (ptext (sLit "Kind mis-match in inst coercion")) _ -> failWithL (ptext (sLit "Bad argument of inst")) } @@ -927,27 +940,29 @@ lintCoercion co@(AxiomInstCo con ind cos) = do { unless (0 <= ind && ind < brListLength (coAxiomBranches con)) (bad_ax (ptext (sLit "index out of range"))) -- See Note [Kind instantiation in coercions] - ; let CoAxBranch { cab_tvs = ktvs - , cab_lhs = lhs - , cab_rhs = rhs } = coAxiomNthBranch con ind + ; let CoAxBranch { cab_tvs = ktvs + , cab_roles = roles + , cab_lhs = lhs + , cab_rhs = rhs } = coAxiomNthBranch con ind ; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths"))) ; in_scope <- getInScope ; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv ; (subst_l, subst_r) <- foldlM check_ki (empty_subst, empty_subst) - (ktvs `zip` cos) + (zip3 ktvs roles cos) ; let lhs' = Type.substTys subst_l lhs rhs' = Type.substTy subst_r rhs ; case checkAxInstCo co of Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch) Nothing -> return () - ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs') } + ; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) } where bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what) 2 (ppr co)) - check_ki (subst_l, subst_r) (ktv, co) - = do { (k, t1, t2) <- lintCoercion co + check_ki (subst_l, subst_r) (ktv, role, co) + = do { (k, t1, t2, r) <- lintCoercion co + ; checkRole co role r ; let ktv_kind = Type.substTy subst_l (tyVarKind ktv) -- Using subst_l is ok, because subst_l and subst_r -- must agree on kind equalities @@ -955,6 +970,11 @@ lintCoercion co@(AxiomInstCo con ind cos) (bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] )) ; return (Type.extendTvSubst subst_l ktv t1, Type.extendTvSubst subst_r ktv t2) } + +lintCoercion co@(SubCo co') + = do { (k,s,t,r) <- lintCoercion co' + ; checkRole co Nominal r + ; return (k,s,t,Representational) } \end{code} %************************************************************************ @@ -1131,6 +1151,17 @@ checkTys :: OutType -> OutType -> MsgDoc -> LintM () -- annotations need only be consistent, not equal) -- Assumes ty1,ty2 are have alrady had the substitution applied checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg + +checkRole :: Coercion + -> Role -- expected + -> Role -- actual + -> LintM () +checkRole co r1 r2 + = checkL (r1 == r2) + (ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+> + ptext (sLit "got") <+> ppr r2 $$ + ptext (sLit "in") <+> ppr co) + \end{code} %************************************************************************ diff --git a/compiler/coreSyn/CoreSubst.lhs b/compiler/coreSyn/CoreSubst.lhs index bc9c767d29..25a751b423 100644 --- a/compiler/coreSyn/CoreSubst.lhs +++ b/compiler/coreSyn/CoreSubst.lhs @@ -1163,7 +1163,7 @@ data ConCont = CC [CoreExpr] Coercion -- where t1..tk are the *universally-qantified* type args of 'dc' exprIsConApp_maybe :: InScopeEnv -> CoreExpr -> Maybe (DataCon, [Type], [CoreExpr]) exprIsConApp_maybe (in_scope, id_unf) expr - = go (Left in_scope) expr (CC [] (mkReflCo (exprType expr))) + = go (Left in_scope) expr (CC [] (mkReflCo Representational (exprType expr))) where go :: Either InScopeSet Subst -> CoreExpr -> ConCont @@ -1252,9 +1252,11 @@ dealWithCoercion co dc dc_args -- Make the "theta" from Fig 3 of the paper gammas = decomposeCo tc_arity co - theta_subst = liftCoSubstWith + theta_subst = liftCoSubstWith Representational (dc_univ_tyvars ++ dc_ex_tyvars) - (gammas ++ map mkReflCo (stripTypeArgs ex_args)) + -- existentials are at role N + (gammas ++ map (mkReflCo Nominal) + (stripTypeArgs ex_args)) -- Cast the value arguments (which include dictionaries) new_val_args = zipWith cast_arg arg_tys val_args diff --git a/compiler/coreSyn/CoreUtils.lhs b/compiler/coreSyn/CoreUtils.lhs index 00f704f7c8..c872ac311e 100644 --- a/compiler/coreSyn/CoreUtils.lhs +++ b/compiler/coreSyn/CoreUtils.lhs @@ -187,9 +187,12 @@ mkCast (Coercion e_co) co = Coercion (mkCoCast e_co co) mkCast (Cast expr co2) co - = ASSERT(let { Pair from_ty _to_ty = coercionKind co; - Pair _from_ty2 to_ty2 = coercionKind co2} in - from_ty `eqType` to_ty2 ) + = WARN(let { Pair from_ty _to_ty = coercionKind co; + Pair _from_ty2 to_ty2 = coercionKind co2} in + not (from_ty `eqType` to_ty2), + vcat ([ ptext (sLit "expr:") <+> ppr expr + , ptext (sLit "co2:") <+> ppr co2 + , ptext (sLit "co:") <+> ppr co ]) ) mkCast expr (mkTransCo co2 co) mkCast expr co @@ -1602,7 +1605,7 @@ need to address that here. \begin{code} tryEtaReduce :: [Var] -> CoreExpr -> Maybe CoreExpr tryEtaReduce bndrs body - = go (reverse bndrs) body (mkReflCo (exprType body)) + = go (reverse bndrs) body (mkReflCo Representational (exprType body)) where incoming_arity = count isId bndrs @@ -1659,9 +1662,10 @@ tryEtaReduce bndrs body | Just tv <- getTyVar_maybe ty , bndr == tv = Just (mkForAllCo tv co) ok_arg bndr (Var v) co - | bndr == v = Just (mkFunCo (mkReflCo (idType bndr)) co) + | bndr == v = Just (mkFunCo Representational + (mkReflCo Representational (idType bndr)) co) ok_arg bndr (Cast (Var v) co_arg) co - | bndr == v = Just (mkFunCo (mkSymCo co_arg) co) + | bndr == v = Just (mkFunCo Representational (mkSymCo co_arg) co) -- The simplifier combines multiple casts into one, -- so we can have a simple-minded pattern match here ok_arg _ _ _ = Nothing diff --git a/compiler/coreSyn/ExternalCore.lhs b/compiler/coreSyn/ExternalCore.lhs index f002c3a3e5..ecc24b1155 100644 --- a/compiler/coreSyn/ExternalCore.lhs +++ b/compiler/coreSyn/ExternalCore.lhs @@ -34,7 +34,7 @@ data Exp | Lam Bind Exp | Let Vdefg Exp | Case Exp Vbind Ty [Alt] {- non-empty list -} - | Cast Exp Ty + | Cast Exp Coercion | Tick String Exp {- XXX probably wrong -} | External String String Ty {- target name, convention, and type -} | DynExternal String Ty {- convention and type (incl. Addr# of target as first arg) -} @@ -52,23 +52,30 @@ data Alt type Vbind = (Var,Ty) type Tbind = (Tvar,Kind) --- Internally, we represent types and coercions separately; but for --- the purposes of external core (at least for now) it's still --- convenient to collapse them into a single type. data Ty = Tvar Tvar | Tcon (Qual Tcon) | Tapp Ty Ty | Tforall Tbind Ty + +data Coercion -- We distinguish primitive coercions because External Core treats -- them specially, so we have to print them out with special syntax. - | TransCoercion Ty Ty - | SymCoercion Ty - | UnsafeCoercion Ty Ty - | InstCoercion Ty Ty - | NthCoercion Int Ty - | AxiomCoercion (Qual Tcon) Int [Ty] - | LRCoercion LeftOrRight Ty + = ReflCoercion Role Ty + | SymCoercion Coercion + | TransCoercion Coercion Coercion + | TyConAppCoercion Role (Qual Tcon) [Coercion] + | AppCoercion Coercion Coercion + | ForAllCoercion Tbind Coercion + | CoVarCoercion Var + | UnivCoercion Role Ty Ty + | InstCoercion Coercion Ty + | NthCoercion Int Coercion + | AxiomCoercion (Qual Tcon) Int [Coercion] + | LRCoercion LeftOrRight Coercion + | SubCoercion Coercion + +data Role = Nominal | Representational | Phantom data LeftOrRight = CLeft | CRight diff --git a/compiler/coreSyn/MkExternalCore.lhs b/compiler/coreSyn/MkExternalCore.lhs index e84dff900d..a0776af218 100644 --- a/compiler/coreSyn/MkExternalCore.lhs +++ b/compiler/coreSyn/MkExternalCore.lhs @@ -309,29 +309,29 @@ make_var_qid dflags force_unqual = make_qid dflags force_unqual True make_con_qid :: DynFlags -> Name -> C.Qual C.Id make_con_qid dflags = make_qid dflags False False -make_co :: DynFlags -> Coercion -> C.Ty -make_co dflags (Refl ty) = make_ty dflags ty -make_co dflags (TyConAppCo tc cos) = make_conAppCo dflags (qtc dflags tc) cos -make_co dflags (AppCo c1 c2) = C.Tapp (make_co dflags c1) (make_co dflags c2) -make_co dflags (ForAllCo tv co) = C.Tforall (make_tbind tv) (make_co dflags co) -make_co _ (CoVarCo cv) = C.Tvar (make_var_id (coVarName cv)) +make_co :: DynFlags -> Coercion -> C.Coercion +make_co dflags (Refl r ty) = C.ReflCoercion (make_role r) $ make_ty dflags ty +make_co dflags (TyConAppCo r tc cos) = C.TyConAppCoercion (make_role r) (qtc dflags tc) (map (make_co dflags) cos) +make_co dflags (AppCo c1 c2) = C.AppCoercion (make_co dflags c1) (make_co dflags c2) +make_co dflags (ForAllCo tv co) = C.ForAllCoercion (make_tbind tv) (make_co dflags co) +make_co _ (CoVarCo cv) = C.CoVarCoercion (make_var_id (coVarName cv)) make_co dflags (AxiomInstCo cc ind cos) = C.AxiomCoercion (qcc dflags cc) ind (map (make_co dflags) cos) -make_co dflags (UnsafeCo t1 t2) = C.UnsafeCoercion (make_ty dflags t1) (make_ty dflags t2) +make_co dflags (UnivCo r t1 t2) = C.UnivCoercion (make_role r) (make_ty dflags t1) (make_ty dflags t2) make_co dflags (SymCo co) = C.SymCoercion (make_co dflags co) make_co dflags (TransCo c1 c2) = C.TransCoercion (make_co dflags c1) (make_co dflags c2) make_co dflags (NthCo d co) = C.NthCoercion d (make_co dflags co) make_co dflags (LRCo lr co) = C.LRCoercion (make_lr lr) (make_co dflags co) make_co dflags (InstCo co ty) = C.InstCoercion (make_co dflags co) (make_ty dflags ty) +make_co dflags (SubCo co) = C.SubCoercion (make_co dflags co) make_lr :: LeftOrRight -> C.LeftOrRight make_lr CLeft = C.CLeft make_lr CRight = C.CRight --- Used for both tycon app coercions and axiom instantiations. -make_conAppCo :: DynFlags -> C.Qual C.Tcon -> [Coercion] -> C.Ty -make_conAppCo dflags con cos = - foldl C.Tapp (C.Tcon con) - (map (make_co dflags) cos) +make_role :: Role -> C.Role +make_role Nominal = C.Nominal +make_role Representational = C.Representational +make_role Phantom = C.Phantom ------- isALocal :: Name -> CoreM Bool diff --git a/compiler/coreSyn/PprExternalCore.lhs b/compiler/coreSyn/PprExternalCore.lhs index 24ee560cb1..7fd3ac1d65 100644 --- a/compiler/coreSyn/PprExternalCore.lhs +++ b/compiler/coreSyn/PprExternalCore.lhs @@ -102,22 +102,6 @@ pbty t = paty t pty (Tapp(Tapp(Tcon tc) t1) t2) | tc == tcArrow = fsep [pbty t1, text "->",pty t2] pty (Tforall tb t) = text "%forall" <+> pforall [tb] t -pty (TransCoercion t1 t2) = - sep [text "%trans", paty t1, paty t2] -pty (SymCoercion t) = - sep [text "%sym", paty t] -pty (UnsafeCoercion t1 t2) = - sep [text "%unsafe", paty t1, paty t2] -pty (NthCoercion n t) = - sep [text "%nth", int n, paty t] -pty (LRCoercion CLeft t) = - sep [text "%left", paty t] -pty (LRCoercion CRight t) = - sep [text "%right", paty t] -pty (InstCoercion t1 t2) = - sep [text "%inst", paty t1, paty t2] -pty (AxiomCoercion tc i cos) = - pqname tc <+> int i <+> sep (map paty cos) pty ty@(Tapp {}) = pappty ty [] pty ty@(Tvar {}) = paty ty pty ty@(Tcon {}) = paty ty @@ -130,6 +114,48 @@ pforall :: [Tbind] -> Ty -> Doc pforall tbs (Tforall tb t) = pforall (tbs ++ [tb]) t pforall tbs t = hsep (map ptbind tbs) <+> char '.' <+> pty t +paco, pbco, pco :: Coercion -> Doc +paco (ReflCoercion r ty) = char '<' <> pty ty <> text ">_" <> prole r +paco (TyConAppCoercion r qtc []) = pqname qtc <> char '_' <> prole r +paco (AxiomCoercion qtc i []) = pqname qtc <> char '[' <> int i <> char ']' +paco (CoVarCoercion cv) = pname cv +paco c = parens (pco c) + +pbco (TyConAppCoercion _ arr [co1, co2]) + | arr == tcArrow + = parens (fsep [pbco co1, text "->", pco co2]) +pbco co = paco co + +pco c@(ReflCoercion {}) = paco c +pco (SymCoercion co) = sep [text "%sub", paco co] +pco (TransCoercion co1 co2) = sep [text "%trans", paco co1, paco co2] +pco (TyConAppCoercion _ arr [co1, co2]) + | arr == tcArrow = fsep [pbco co1, text "->", pco co2] +pco (TyConAppCoercion r qtc cos) = parens (pqname qtc <+> sep (map paco cos)) <> char '_' <> prole r +pco co@(AppCoercion {}) = pappco co [] +pco (ForAllCoercion tb co) = text "%forall" <+> pforallco [tb] co +pco co@(CoVarCoercion {}) = paco co +pco (UnivCoercion r ty1 ty2) = sep [text "%univ", prole r, paty ty1, paty ty2] +pco (InstCoercion co ty) = sep [text "%inst", paco co, paty ty] +pco (NthCoercion i co) = sep [text "%nth", int i, paco co] +pco (AxiomCoercion qtc i cos) = pqname qtc <> char '[' <> int i <> char ']' <+> sep (map paco cos) +pco (LRCoercion CLeft co) = sep [text "%left", paco co] +pco (LRCoercion CRight co) = sep [text "%right", paco co] +pco (SubCoercion co) = sep [text "%sub", paco co] + +pappco :: Coercion -> [Coercion ] -> Doc +pappco (AppCoercion co1 co2) cos = pappco co1 (co2:cos) +pappco co cos = sep (map paco (co:cos)) + +pforallco :: [Tbind] -> Coercion -> Doc +pforallco tbs (ForAllCoercion tb co) = pforallco (tbs ++ [tb]) co +pforallco tbs co = hsep (map ptbind tbs) <+> char '.' <+> pco co + +prole :: Role -> Doc +prole Nominal = char 'N' +prole Representational = char 'R' +prole Phantom = char 'P' + pvdefg :: Vdefg -> Doc pvdefg (Rec vdefs) = text "%rec" $$ braces (indent (vcat (punctuate (char ';') (map pvdef vdefs)))) pvdefg (Nonrec vdef) = pvdef vdef @@ -172,7 +198,7 @@ pexp (Let vd e) = (text "%let" <+> pvdefg vd) $$ (text "%in" <+> pexp e) pexp (Case e vb ty alts) = sep [text "%case" <+> paty ty <+> paexp e, text "%of" <+> pvbind vb] $$ (indent (braces (vcat (punctuate (char ';') (map palt alts))))) -pexp (Cast e co) = (text "%cast" <+> parens (pexp e)) $$ paty co +pexp (Cast e co) = (text "%cast" <+> parens (pexp e)) $$ paco co pexp (Tick s e) = (text "%source" <+> pstring s) $$ pexp e pexp (External n cc t) = (text "%external" <+> text cc <+> pstring n) $$ paty t pexp (DynExternal cc t) = (text "%dynexternal" <+> text cc) $$ paty t diff --git a/compiler/coreSyn/TrieMap.lhs b/compiler/coreSyn/TrieMap.lhs index c5cd9902bc..f8ad8da5f4 100644 --- a/compiler/coreSyn/TrieMap.lhs +++ b/compiler/coreSyn/TrieMap.lhs @@ -458,27 +458,28 @@ fdA k m = foldTM k (am_deflt m) \begin{code} data CoercionMap a = EmptyKM - | KM { km_refl :: TypeMap a - , km_tc_app :: NameEnv (ListMap CoercionMap a) + | KM { km_refl :: RoleMap (TypeMap a) + , km_tc_app :: RoleMap (NameEnv (ListMap CoercionMap a)) , km_app :: CoercionMap (CoercionMap a) , km_forall :: CoercionMap (TypeMap a) , km_var :: VarMap a , km_axiom :: NameEnv (IntMap.IntMap (ListMap CoercionMap a)) - , km_unsafe :: TypeMap (TypeMap a) + , km_univ :: RoleMap (TypeMap (TypeMap a)) , km_sym :: CoercionMap a , km_trans :: CoercionMap (CoercionMap a) , km_nth :: IntMap.IntMap (CoercionMap a) , km_left :: CoercionMap a , km_right :: CoercionMap a - , km_inst :: CoercionMap (TypeMap a) } + , km_inst :: CoercionMap (TypeMap a) + , km_sub :: CoercionMap a } wrapEmptyKM :: CoercionMap a -wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyNameEnv +wrapEmptyKM = KM { km_refl = emptyTM, km_tc_app = emptyTM , km_app = emptyTM, km_forall = emptyTM , km_var = emptyTM, km_axiom = emptyNameEnv - , km_unsafe = emptyTM, km_sym = emptyTM, km_trans = emptyTM + , km_univ = emptyTM, km_sym = emptyTM, km_trans = emptyTM , km_nth = emptyTM, km_left = emptyTM, km_right = emptyTM - , km_inst = emptyTM } + , km_inst = emptyTM, km_sub = emptyTM } instance TrieMap CoercionMap where type Key CoercionMap = Coercion @@ -493,34 +494,35 @@ mapC _ EmptyKM = EmptyKM mapC f (KM { km_refl = krefl, km_tc_app = ktc , km_app = kapp, km_forall = kforall , km_var = kvar, km_axiom = kax - , km_unsafe = kunsafe, km_sym = ksym, km_trans = ktrans + , km_univ = kuniv , km_sym = ksym, km_trans = ktrans , km_nth = knth, km_left = kml, km_right = kmr - , km_inst = kinst }) - = KM { km_refl = mapTM f krefl - , km_tc_app = mapNameEnv (mapTM f) ktc + , km_inst = kinst, km_sub = ksub }) + = KM { km_refl = mapTM (mapTM f) krefl + , km_tc_app = mapTM (mapNameEnv (mapTM f)) ktc , km_app = mapTM (mapTM f) kapp , km_forall = mapTM (mapTM f) kforall , km_var = mapTM f kvar , km_axiom = mapNameEnv (IntMap.map (mapTM f)) kax - , km_unsafe = mapTM (mapTM f) kunsafe + , km_univ = mapTM (mapTM (mapTM f)) kuniv , km_sym = mapTM f ksym , km_trans = mapTM (mapTM f) ktrans , km_nth = IntMap.map (mapTM f) knth , km_left = mapTM f kml , km_right = mapTM f kmr - , km_inst = mapTM (mapTM f) kinst } + , km_inst = mapTM (mapTM f) kinst + , km_sub = mapTM f ksub } lkC :: CmEnv -> Coercion -> CoercionMap a -> Maybe a lkC env co m | EmptyKM <- m = Nothing | otherwise = go co m where - go (Refl ty) = km_refl >.> lkT env ty - go (TyConAppCo tc cs) = km_tc_app >.> lkNamed tc >=> lkList (lkC env) cs + go (Refl r ty) = km_refl >.> lookupTM r >=> lkT env ty + go (TyConAppCo r tc cs) = km_tc_app >.> lookupTM r >=> lkNamed tc >=> lkList (lkC env) cs go (AxiomInstCo ax ind cs) = km_axiom >.> lkNamed ax >=> lookupTM ind >=> lkList (lkC env) cs go (AppCo c1 c2) = km_app >.> lkC env c1 >=> lkC env c2 go (TransCo c1 c2) = km_trans >.> lkC env c1 >=> lkC env c2 - go (UnsafeCo t1 t2) = km_unsafe >.> lkT env t1 >=> lkT env t2 + go (UnivCo r t1 t2) = km_univ >.> lookupTM r >=> lkT env t1 >=> lkT env t2 go (InstCo c t) = km_inst >.> lkC env c >=> lkT env t go (ForAllCo v c) = km_forall >.> lkC (extendCME env v) c >=> lkBndr env v go (CoVarCo v) = km_var >.> lkVar env v @@ -528,15 +530,16 @@ lkC env co m go (NthCo n c) = km_nth >.> lookupTM n >=> lkC env c go (LRCo CLeft c) = km_left >.> lkC env c go (LRCo CRight c) = km_right >.> lkC env c + go (SubCo c) = km_sub >.> lkC env c xtC :: CmEnv -> Coercion -> XT a -> CoercionMap a -> CoercionMap a xtC env co f EmptyKM = xtC env co f wrapEmptyKM -xtC env (Refl ty) f m = m { km_refl = km_refl m |> xtT env ty f } -xtC env (TyConAppCo tc cs) f m = m { km_tc_app = km_tc_app m |> xtNamed tc |>> xtList (xtC env) cs f } +xtC env (Refl r ty) f m = m { km_refl = km_refl m |> xtR r |>> xtT env ty f } +xtC env (TyConAppCo r tc cs) f m = m { km_tc_app = km_tc_app m |> xtR r |>> xtNamed tc |>> xtList (xtC env) cs f } xtC env (AxiomInstCo ax ind cs) f m = m { km_axiom = km_axiom m |> xtNamed ax |>> xtInt ind |>> xtList (xtC env) cs f } xtC env (AppCo c1 c2) f m = m { km_app = km_app m |> xtC env c1 |>> xtC env c2 f } xtC env (TransCo c1 c2) f m = m { km_trans = km_trans m |> xtC env c1 |>> xtC env c2 f } -xtC env (UnsafeCo t1 t2) f m = m { km_unsafe = km_unsafe m |> xtT env t1 |>> xtT env t2 f } +xtC env (UnivCo r t1 t2) f m = m { km_univ = km_univ m |> xtR r |>> xtT env t1 |>> xtT env t2 f } xtC env (InstCo c t) f m = m { km_inst = km_inst m |> xtC env c |>> xtT env t f } xtC env (ForAllCo v c) f m = m { km_forall = km_forall m |> xtC (extendCME env v) c |>> xtBndr env v f } @@ -544,23 +547,56 @@ xtC env (CoVarCo v) f m = m { km_var = km_var m |> xtVar env v f xtC env (SymCo c) f m = m { km_sym = km_sym m |> xtC env c f } xtC env (NthCo n c) f m = m { km_nth = km_nth m |> xtInt n |>> xtC env c f } xtC env (LRCo CLeft c) f m = m { km_left = km_left m |> xtC env c f } -xtC env (LRCo CRight c) f m = m { km_right = km_right m |> xtC env c f } +xtC env (LRCo CRight c) f m = m { km_right = km_right m |> xtC env c f } +xtC env (SubCo c) f m = m { km_sub = km_sub m |> xtC env c f } fdC :: (a -> b -> b) -> CoercionMap a -> b -> b fdC _ EmptyKM = \z -> z -fdC k m = foldTM k (km_refl m) - . foldTM (foldTM k) (km_tc_app m) +fdC k m = foldTM (foldTM k) (km_refl m) + . foldTM (foldTM (foldTM k)) (km_tc_app m) . foldTM (foldTM k) (km_app m) . foldTM (foldTM k) (km_forall m) . foldTM k (km_var m) . foldTM (foldTM (foldTM k)) (km_axiom m) - . foldTM (foldTM k) (km_unsafe m) + . foldTM (foldTM (foldTM k)) (km_univ m) . foldTM k (km_sym m) . foldTM (foldTM k) (km_trans m) . foldTM (foldTM k) (km_nth m) . foldTM k (km_left m) . foldTM k (km_right m) . foldTM (foldTM k) (km_inst m) + . foldTM k (km_sub m) + +\end{code} + +\begin{code} + +newtype RoleMap a = RM { unRM :: (IntMap.IntMap a) } + +instance TrieMap RoleMap where + type Key RoleMap = Role + emptyTM = RM emptyTM + lookupTM = lkR + alterTM = xtR + foldTM = fdR + mapTM = mapR + +lkR :: Role -> RoleMap a -> Maybe a +lkR Nominal = lookupTM 1 . unRM +lkR Representational = lookupTM 2 . unRM +lkR Phantom = lookupTM 3 . unRM + +xtR :: Role -> XT a -> RoleMap a -> RoleMap a +xtR Nominal f = RM . alterTM 1 f . unRM +xtR Representational f = RM . alterTM 2 f . unRM +xtR Phantom f = RM . alterTM 3 f . unRM + +fdR :: (a -> b -> b) -> RoleMap a -> b -> b +fdR f (RM m) = foldTM f m + +mapR :: (a -> b) -> RoleMap a -> RoleMap b +mapR f = RM . mapTM f . unRM + \end{code} |