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 HaskLiterals.
12 Require Import HaskTyCons.
13 Require Import HaskCoreVars.
15 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
16 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
19 * WeakType is much like CoreType, but:
20 * 1. avoids mutually-inductive definitions
21 * 2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them
22 * 3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter
25 | WTyVarTy : WeakTypeVar -> WeakType
26 | WAppTy : WeakType -> WeakType -> WeakType
27 | WTyFunApp : TyFun -> list WeakType -> WeakType
28 | WTyCon : TyCon -> WeakType
29 | WFunTyCon : WeakType (* never use (WTyCon ArrowCon); always use this! *)
30 | WCodeTy : WeakTypeVar -> WeakType -> WeakType (* never use the raw tycon *)
31 | WCoFunTy : WeakType -> WeakType -> WeakType -> WeakType
32 | WForAllTy : WeakTypeVar -> WeakType -> WeakType
33 | WClassP : Class_ -> list WeakType -> WeakType
34 | WIParam : CoreIPName CoreName -> WeakType -> WeakType.
36 (* EqDecidable instances for WeakType *)
37 Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
38 apply Build_EqDecidable.
40 destruct v1 as [cv1 k1].
41 destruct v2 as [cv2 k2].
42 destruct (eqd_dec cv1 cv2); subst.
43 destruct (eqd_dec k1 k2); subst.
45 right; intro; apply n; inversion H; subst; auto.
46 right; intro; apply n; inversion H; subst; auto.
49 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
50 Inductive WeakCoerVar := weakCoerVar : CoreVar -> WeakType -> WeakType -> WeakCoerVar.
52 Inductive WeakCoercion : Type :=
53 | WCoVar : WeakCoerVar -> WeakCoercion (* g *)
54 | WCoType : WeakType -> WeakCoercion (* τ *)
55 | WCoApp : WeakCoercion -> WeakCoercion -> WeakCoercion (* γ γ *)
56 | WCoAppT : WeakCoercion -> WeakType -> WeakCoercion (* γ@v *)
57 | WCoAll : Kind -> (WeakTypeVar -> WeakCoercion) -> WeakCoercion (* ∀a:κ.γ *)
58 | WCoSym : WeakCoercion -> WeakCoercion (* sym *)
59 | WCoComp : WeakCoercion -> WeakCoercion -> WeakCoercion (* ◯ *)
60 | WCoLeft : WeakCoercion -> WeakCoercion (* left *)
61 | WCoRight : WeakCoercion -> WeakCoercion (* right *)
62 | WCoUnsafe : WeakType -> WeakType -> WeakCoercion (* unsafe *)
63 (*| WCoCFApp : ∀ n, CoFunConst n -> vec WeakCoercion n -> WeakCoercion (* C γⁿ *)*)
64 (*| WCoTFApp : ∀ n, TyFunConst n -> vec WeakCoercion n -> WeakCoercion (* S_n γⁿ *)*)
67 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
69 | WCoVar (weakCoerVar _ t1 t2) => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
70 | WCoType t => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
71 | WCoApp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
72 | WCoAppT c t => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
73 | WCoAll k f => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
74 | WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
75 | WCoComp c1 c2 => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
76 | WCoLeft c => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
77 | WCoRight c => (WFunTyCon,WFunTyCon) (* FIXME!!! *)
78 | WCoUnsafe t1 t2 => (t1,t2)
82 (* this is a trick to allow circular definitions, post-extraction *)
83 Variable weakTypeToString : WeakType -> string.
84 Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)".
85 Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }.
87 Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)".
88 Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)".
89 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
90 Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.