From 635ee434c9edbad1bc6c9bf5ba2b91cb8c51be8e Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 16:37:12 -0700 Subject: [PATCH] minor cleanups, deleted dead code, eliminated use of (==) on CoreType --- src/Extraction-prefix.hs | 56 ++++++++++++++++++++++---------------------- src/HaskCoreToWeak.v | 12 ++++++++-- src/HaskCoreTypes.v | 6 ++--- src/HaskWeakTypes.v | 58 ++++++++++------------------------------------ 4 files changed, 52 insertions(+), 80 deletions(-) diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 558d0ab..5a657bc 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -35,18 +35,14 @@ bin2ascii = (\ b0 b1 b2 b3 b4 b5 b6 b7 -> let f b i = if b then 1 `shiftL` i else 0 in Data.Char.chr (f b0 0 .|. f b1 1 .|. f b2 2 .|. f b3 3 .|. f b4 4 .|. f b5 5 .|. f b6 6 .|. f b7 7)) ---bin2ascii' = --- (\ f c -> let n = Char.code c in let h i = (n .&. (1 `shiftL` i)) /= 0 in f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7)) ---shiftAscii = --- \ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&. 255 .|. if b then 1 else 0) - --- crude way of casting Coq "error monad" into Haskell exceptions -errOrFail :: OrError a -> a -errOrFail (OK x) = x -errOrFail (Error s) = Prelude.error s getTyConTyVars :: TyCon.TyCon -> [Var.TyVar] -getTyConTyVars tc = if TyCon.isFunTyCon tc then [] else if TyCon.isPrimTyCon tc then [] else TyCon.tyConTyVars tc +getTyConTyVars tc = + if TyCon.isFunTyCon tc + then [] + else if TyCon.isPrimTyCon tc + then [] + else TyCon.tyConTyVars tc sortAlts :: [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] -> [(CoreSyn.AltCon,[Var.Var],CoreSyn.Expr Var.Var)] sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) x @@ -54,6 +50,9 @@ sortAlts x = Data.List.sortBy (\(a1,_,_) -> \(a2,_,_) -> Data.Ord.compare a1 a2) -- to do: this could be moved into Coq coreVarToWeakVar :: Var.Var -> WeakVar coreVarToWeakVar v | Id.isId v = WExprVar (WeakExprVar v (errOrFail (coreTypeToWeakType (Var.varType v)))) + where + errOrFail (OK x) = x + errOrFail (Error s) = Prelude.error s coreVarToWeakVar v | Var.isTyVar v = WTypeVar (WeakTypeVar v (coreKindToKind (Var.varType v))) coreVarToWeakVar v | Var.isCoVar v = WCoerVar (WeakCoerVar v (Prelude.error "FIXME") (Prelude.error "FIXME") (Prelude.error "FIXME")) @@ -61,12 +60,12 @@ coreVarToWeakVar _ = Prelude.error "Var.Var that is neither an expression variable, type variable, nor coercion variable!" tyConOrTyFun :: TyCon.TyCon -> Prelude.Either TyCon.TyCon TyCon.TyCon ---FIXME: go back to this ---tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Right n -tyConOrTyFun n = if TyCon.isFamInstTyCon n then Prelude.Left n else Prelude.Left n - -tyFunResultKind :: TyCon.TyCon -> Kind -tyFunResultKind tc = coreKindToKind (TyCon.tyConKind tc) +tyConOrTyFun n = + if n == TysPrim.statePrimTyCon -- special-purpose hack treat State# as a type family since it has kind *->* but no tyvars + then Prelude.Right n + else if TyCon.isFamInstTyCon n + then Prelude.Right n + else Prelude.Left n nat2int :: Nat -> Prelude.Int nat2int O = 0 @@ -77,11 +76,11 @@ natToString n = show (nat2int n) -- only needs to sanitize characters which might appear in Haskell identifiers sanitizeForLatex :: Prelude.String -> Prelude.String -sanitizeForLatex [] = [] +sanitizeForLatex [] = [] sanitizeForLatex ('_':x) = "\\_"++(sanitizeForLatex x) sanitizeForLatex ('$':x) = "\\$"++(sanitizeForLatex x) sanitizeForLatex ('#':x) = "\\#"++(sanitizeForLatex x) -sanitizeForLatex (c:x) = c:(sanitizeForLatex x) +sanitizeForLatex (c:x) = c:(sanitizeForLatex x) coreKindToKind :: TypeRep.Kind -> Kind coreKindToKind k = @@ -89,10 +88,14 @@ coreKindToKind k = Prelude.Just (k1,k2) -> KindTypeFunction (coreKindToKind k1) (coreKindToKind k2) Prelude.Nothing -> if (Coercion.isLiftedTypeKind k) then KindType - else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType - else if (Coercion.isOpenTypeKind k) then KindOpenType - else if (Coercion.isArgTypeKind k) then KindArgType - else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple + else if (Coercion.isUnliftedTypeKind k) then KindType + else if (Coercion.isArgTypeKind k) then KindType + else if (Coercion.isUbxTupleKind k) then KindType + else if (Coercion.isOpenTypeKind k) then KindType +-- else if (Coercion.isUnliftedTypeKind k) then KindUnliftedType +-- else if (Coercion.isOpenTypeKind k) then KindOpenType +-- else if (Coercion.isArgTypeKind k) then KindArgType +-- else if (Coercion.isUbxTupleKind k) then KindUnboxedTuple else if (Coercion.isTySuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-types" else if (Coercion.isCoSuperKind k) then Prelude.error "coreKindToKind got the kind-of-the-kind-of-coercions" else Prelude.error ((Prelude.++) "coreKindToKind got an unknown kind: " @@ -100,12 +103,9 @@ coreKindToKind k = outputableToString :: Outputable.Outputable a => a -> Prelude.String outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x)) --- TO DO: I think we can remove this now -checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool -checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) - ---showType t = outputableToString (Type.expandTypeSynonyms t) -showType t = outputableToString (coreViewDeep t) +-- I'm leaving this here (commented out) in case I ever need it again) +--checkTypeEquality :: Type.Type -> Type.Type -> Prelude.Bool +--checkTypeEquality t1 t2 = Type.tcEqType (Type.expandTypeSynonyms t1) (Type.expandTypeSynonyms t2) coreViewDeep :: Type.Type -> Type.Type coreViewDeep t = diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 1cbaf22..63c7e95 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -107,6 +107,15 @@ Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion. OK (WCoUnsafe t1' t2'). *) +(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *) +Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) := + match wt with + | WTyCon tc => OK (tc,acc) + | WAppTy t1 t2 => expectTyConApp t1 (t2::acc) + | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt) + | _ => Error ("expectTyConApp encountered " +++ wt) + end. + Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match ce with | CoreELit lit => OK (WELit lit) @@ -178,8 +187,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := | WExprVar ev => coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' => coreExprToWeakExpr e >>= fun e' => - (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end) - >>= fun tca => + expectTyConApp te' nil >>= fun tca => let (tc,lt) := tca in ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar))) : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index ea4a02a..5c4ce6e 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -40,11 +40,11 @@ Extract Inductive CoreType => Extract Inductive PredType => "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. -Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "showType". Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". -Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". +Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "(outputableToString . coreViewDeep)". (* once again, we pull the trick of having multiple Coq types map to a single Haskell type to provide stronger typing *) Variable TyCon : Type. Extract Inlined Constant TyCon => "TyCon.TyCon". @@ -56,8 +56,6 @@ Variable tyCon_eq : EqDecider TyCon. Extract Inlined Consta Variable tyFun_eq : EqDecider TyFun. Extract Inlined Constant tyFun_eq => "(==)". Variable dataCon_eq : EqDecider CoreDataCon. Extract Inlined Constant dataCon_eq => "(==)". Variable coreName_eq : EqDecider CoreName. Extract Inlined Constant coreName_eq => "(==)". -Variable coretype_eq_dec : EqDecider CoreType. Extract Inlined Constant coretype_eq_dec => "checkTypeEquality". -Instance CoreTypeEqDecidable : EqDecidable CoreType := { eqd_dec := coretype_eq_dec }. Instance CoreTyConEqDecidable: EqDecidable CoreTyCon := { eqd_dec := coreTyCon_eq }. Instance TyConEqDecidable : EqDecidable TyCon := { eqd_dec := tyCon_eq }. Instance TyFunEqDecidable : EqDecidable TyFun := { eqd_dec := tyFun_eq }. diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index cdbc9e7..8f55346 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -12,7 +12,6 @@ Require Import HaskCoreLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. -(* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *) Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)". Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)". Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon. @@ -88,61 +87,28 @@ match wc with | WCoUnsafe t1 t2 => (t1,t2) end. -(* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *) Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon". Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon". -(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *) -Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) := - match wt with - | WTyCon tc => Some (tc,acc) - | WAppTy t1 t2 => isTyConApp t1 (t2::acc) - | _ => None - end. - -(* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *) -Definition normalizeWeakType (wt:WeakType) : WeakType := wt. - -Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType := +Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType := match wt with | WTyVarTy (weakTypeVar v _) => TyVarTy v - | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2) - | WAppTy t1 t2 => match (weakTypeToCoreType' t1) with - | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil)) - | t1' => AppTy t1' (weakTypeToCoreType' t2) + | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2) + | WAppTy t1 t2 => match (weakTypeToCoreType t1) with + | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil)) + | t1' => AppTy t1' (weakTypeToCoreType t2) end | WTyCon tc => TyConApp tc nil - | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType' lt) - | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType' lt)) - | WIParam n ty => PredTy (IParam n (weakTypeToCoreType' ty)) - | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t) + | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt) + | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt)) + | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty)) + | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t) | WFunTyCon => TyConApp ArrowTyCon nil - | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType' t)::nil) - | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType' t1) (weakTypeToCoreType' t2))) - (weakTypeToCoreType' t3) + | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil) + | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2))) + (weakTypeToCoreType t3) end. -Definition weakTypeToCoreType (wt:WeakType) := - weakTypeToCoreType' (normalizeWeakType wt). - -Definition compare_weakTypes (w1 w2:WeakType) := - if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2) - then true - else false. - -(* -Instance EqDecidableWeakType : EqDecidable WeakType. - apply Build_EqDecidable. - intros. - set (compare_weakTypes_axiom v1 v2) as x. - set (compare_weakTypes v1 v2) as y. - assert (y=compare_weakTypes v1 v2). reflexivity. - destruct y; rewrite <- H in x. - left; auto. - right; auto. - Defined. -*) - Instance WeakTypeToString : ToString WeakType := { toString := coreTypeToString ○ weakTypeToCoreType }. -- 1.7.10.4