1 (*********************************************************************************************************************************)
2 (* HaskWeakTypes: types HaskWeak *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import Coq.Strings.String.
9 Require Import Coq.Lists.List.
10 Require Import HaskKinds.
11 Require Import HaskCoreLiterals.
12 Require Import HaskCoreVars.
13 Require Import HaskCoreTypes.
15 (* TO DO: mark the TyCon used for hetmet as a "type family" so GHC keeps it fully-applied-at-all-times *)
16 Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)".
17 Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)".
18 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
19 Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.
21 Instance TyConToString : ToString TyCon := { toString := tyConToString }.
22 Instance TyFunToString : ToString TyFun := { toString := tyConToString }.
24 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
25 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
28 * WeakType is much like CoreType, but:
29 * 1. avoids mutually-inductive definitions
30 * 2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them
31 * 3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter
34 | WTyVarTy : WeakTypeVar -> WeakType
35 | WAppTy : WeakType -> WeakType -> WeakType
36 | WTyFunApp : TyFun -> list WeakType -> WeakType
37 | WTyCon : TyCon -> WeakType
38 | WFunTyCon : WeakType (* never use (WTyCon ArrowCon); always use this! *)
39 | WCodeTy : WeakTypeVar -> WeakType -> WeakType (* never use the raw tycon *)
40 | WCoFunTy : WeakType -> WeakType -> WeakType -> WeakType
41 | WForAllTy : WeakTypeVar -> WeakType -> WeakType
42 | WClassP : Class_ -> list WeakType -> WeakType
43 | WIParam : CoreIPName CoreName -> WeakType -> WeakType.
45 (* EqDecidable instances for WeakType *)
46 Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
47 apply Build_EqDecidable.
49 destruct v1 as [cv1 k1].
50 destruct v2 as [cv2 k2].
51 destruct (eqd_dec cv1 cv2); subst.
52 destruct (eqd_dec k1 k2); subst.
54 right; intro; apply n; inversion H; subst; auto.
55 right; intro; apply n; inversion H; subst; auto.
58 (* TO DO: write a proper EqDecidable instance for WeakType and then move the rest of this into HaskWeakToCore *)
59 Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
60 Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
62 (* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
63 Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) :=
65 | WTyCon tc => Some (tc,acc)
66 | WAppTy t1 t2 => isTyConApp t1 (t2::acc)
70 (* messy first-order NON-CAPTURE-AVOIDING substitution on WeakType's *)
71 Fixpoint replaceWeakTypeVar (te:WeakType)(tv:WeakTypeVar)(tsubst:WeakType) : WeakType :=
73 | WTyVarTy tv' => if eqd_dec tv tv' then tsubst else te
74 | WAppTy t1 t2 => WAppTy (replaceWeakTypeVar t1 tv tsubst) (replaceWeakTypeVar t2 tv tsubst)
75 | WForAllTy tv' t => if eqd_dec tv tv' then te else WForAllTy tv' (replaceWeakTypeVar t tv tsubst)
76 | WCoFunTy t1 t2 t => WCoFunTy (replaceWeakTypeVar t1 tv tsubst)
77 (replaceWeakTypeVar t2 tv tsubst) (replaceWeakTypeVar t tv tsubst)
78 | WIParam ip ty => WIParam ip (replaceWeakTypeVar ty tv tsubst)
79 | WClassP c lt => WClassP c ((fix replaceCoreDistinctList (lt:list WeakType) :=
82 | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t)
84 | WTyFunApp tc lt => WTyFunApp tc ((fix replaceCoreDistinctList (lt:list WeakType) :=
87 | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t)
89 | WTyCon tc => WTyCon tc
90 | WFunTyCon => WFunTyCon
91 | WModalBoxTyCon => WModalBoxTyCon
94 (* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *)
95 Definition normalizeWeakType (wt:WeakType) : WeakType := wt.
97 Fixpoint weakTypeToCoreType' (wt:WeakType) : CoreType :=
99 | WTyVarTy (weakTypeVar v _) => TyVarTy v
100 | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)
101 | WAppTy t1 t2 => match (weakTypeToCoreType' t1) with
102 | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType' t2)::nil))
103 | t1' => AppTy t1' (weakTypeToCoreType' t2)
105 | WTyCon tc => TyConApp tc nil
106 | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType' lt)
107 | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType' lt))
108 | WIParam n ty => PredTy (IParam n (weakTypeToCoreType' ty))
109 | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType' t)
110 | WFunTyCon => TyConApp ArrowTyCon nil
111 | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType' t)::nil)
112 | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType' t1) (weakTypeToCoreType' t2)))
113 (weakTypeToCoreType' t3)
116 Definition weakTypeToCoreType (wt:WeakType) :=
117 weakTypeToCoreType' (normalizeWeakType wt).
119 Definition compare_weakTypes (w1 w2:WeakType) :=
120 if coretype_eq_dec (weakTypeToCoreType w1) (weakTypeToCoreType w2)
125 Instance EqDecidableWeakType : EqDecidable WeakType.
126 apply Build_EqDecidable.
128 set (compare_weakTypes_axiom v1 v2) as x.
129 set (compare_weakTypes v1 v2) as y.
130 assert (y=compare_weakTypes v1 v2). reflexivity.
131 destruct y; rewrite <- H in x.
137 Instance WeakTypeToString : ToString WeakType :=
138 { toString := coreTypeToString ○ weakTypeToCoreType }.