X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakTypes.v;h=5b73a41ae629278e8ae8912eaa93d1428354af2c;hp=b295cf1d9ac8e42ed114116cd15bcf3624268939;hb=786b693ac8d5f2081db75b49bba838a6cff7e2f6;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index b295cf1..5b73a41 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -8,11 +8,8 @@ Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. -Require Import HaskCoreLiterals. +Require Import HaskLiteralsAndTyCons. 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 *) (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *) Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. @@ -26,7 +23,7 @@ Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. Inductive WeakType := | WTyVarTy : WeakTypeVar -> WeakType | WAppTy : WeakType -> WeakType -> WeakType -| WTyFunApp : TyCon -> list WeakType -> WeakType +| WTyFunApp : TyFun -> list WeakType -> WeakType | WTyCon : TyCon -> WeakType | WFunTyCon : WeakType (* never use (WTyCon ArrowCon); always use this! *) | WCodeTy : WeakTypeVar -> WeakType -> WeakType (* never use the raw tycon *) @@ -48,85 +45,45 @@ Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar. right; intro; apply n; inversion H; subst; auto. Defined. -(* 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. - -(* messy first-order NON-CAPTURE-AVOIDING substitution on WeakType's *) -Fixpoint replaceWeakTypeVar (te:WeakType)(tv:WeakTypeVar)(tsubst:WeakType) : WeakType := - match te with - | WTyVarTy tv' => if eqd_dec tv tv' then tsubst else te - | WAppTy t1 t2 => WAppTy (replaceWeakTypeVar t1 tv tsubst) (replaceWeakTypeVar t2 tv tsubst) - | WForAllTy tv' t => if eqd_dec tv tv' then te else WForAllTy tv' (replaceWeakTypeVar t tv tsubst) - | WCoFunTy t1 t2 t => WCoFunTy (replaceWeakTypeVar t1 tv tsubst) - (replaceWeakTypeVar t2 tv tsubst) (replaceWeakTypeVar t tv tsubst) - | WIParam ip ty => WIParam ip (replaceWeakTypeVar ty tv tsubst) - | WClassP c lt => WClassP c ((fix replaceCoreDistinctList (lt:list WeakType) := - match lt with - | nil => nil - | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t) - end) lt) - | WTyFunApp tc lt => WTyFunApp tc ((fix replaceCoreDistinctList (lt:list WeakType) := - match lt with - | nil => nil - | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t) - end) lt) - | WTyCon tc => WTyCon tc - | WFunTyCon => WFunTyCon - | WModalBoxTyCon => WModalBoxTyCon - 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 := - match wt with - | WTyVarTy (weakTypeVar v _) => TyVarTy v - | 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 tc lt => TyConApp tc (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) - 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. - -(* Coq's "decide equality" can't cope here; we have to cheat for now *) -Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2). - -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. - -Definition weakTypeToString : WeakType -> string := - coreTypeToString ○ weakTypeToCoreType. - +(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *) +Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar. + +Inductive WeakCoercion : Type := +| WCoVar : WeakCoerVar -> WeakCoercion (* g *) +| WCoType : WeakType -> WeakCoercion (* τ *) +| WCoApp : WeakCoercion -> WeakCoercion -> WeakCoercion (* γ γ *) +| WCoAppT : WeakCoercion -> WeakType -> WeakCoercion (* γ@v *) +| WCoAll : Kind -> (WeakTypeVar -> WeakCoercion) -> WeakCoercion (* ∀a:κ.γ *) +| WCoSym : WeakCoercion -> WeakCoercion (* sym *) +| WCoComp : WeakCoercion -> WeakCoercion -> WeakCoercion (* ◯ *) +| WCoLeft : WeakCoercion -> WeakCoercion (* left *) +| WCoRight : WeakCoercion -> WeakCoercion (* right *) +| WCoUnsafe : WeakType -> WeakType -> WeakCoercion (* unsafe *) +(*| WCoCFApp : ∀ n, CoFunConst n -> vec WeakCoercion n -> WeakCoercion (* C γⁿ *)*) +(*| WCoTFApp : ∀ n, TyFunConst n -> vec WeakCoercion n -> WeakCoercion (* S_n γⁿ *)*) +. + +Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType := +match wc with +| WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2) +| WCoType t => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoApp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoAppT c t => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoAll k f => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2) +| WCoComp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoLeft c => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoRight c => (WFunTyCon,WFunTyCon) (* FIXME!!! *) +| WCoUnsafe t1 t2 => (t1,t2) +end. + + +(* this is a trick to allow circular definitions, post-extraction *) +Variable weakTypeToString : WeakType -> string. + Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)". +Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }. + +Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)". +Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)". +Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon. +Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.