Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
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.
-Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.
-
-Instance TyConToString : ToString TyCon := { toString := tyConToString }.
-Instance TyFunToString : ToString TyFun := { toString := tyConToString }.
(* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> 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 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)
- 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 }.
-
+(* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
+Inductive WeakCoerVar := weakCoerVar : CoreVar -> 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) => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
+| 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.
projects / coq-hetmet.git / blobdiff