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 Variable tyConToCoreTyCon : TyCon -> CoreTyCon. Extract Inlined Constant tyConToCoreTyCon => "(\x -> x)".
16 Variable tyFunToCoreTyCon : TyFun -> CoreTyCon. Extract Inlined Constant tyFunToCoreTyCon => "(\x -> x)".
17 Coercion tyConToCoreTyCon : TyCon >-> CoreTyCon.
18 Coercion tyFunToCoreTyCon : TyFun >-> CoreTyCon.
20 Instance TyConToString : ToString TyCon := { toString := tyConToString }.
21 Instance TyFunToString : ToString TyFun := { toString := tyConToString }.
23 (* a WeakTypeVar merely wraps a CoreVar and includes its Kind *)
24 Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar.
27 * WeakType is much like CoreType, but:
28 * 1. avoids mutually-inductive definitions
29 * 2. gives special cases for the tycons which have their own typing rules so we can pattern-match on them
30 * 3. separates type functions from type constructors, and uses a normal "AppTy" for applying the latter
33 | WTyVarTy : WeakTypeVar -> WeakType
34 | WAppTy : WeakType -> WeakType -> WeakType
35 | WTyFunApp : TyFun -> list WeakType -> WeakType
36 | WTyCon : TyCon -> WeakType
37 | WFunTyCon : WeakType (* never use (WTyCon ArrowCon); always use this! *)
38 | WCodeTy : WeakTypeVar -> WeakType -> WeakType (* never use the raw tycon *)
39 | WCoFunTy : WeakType -> WeakType -> WeakType -> WeakType
40 | WForAllTy : WeakTypeVar -> WeakType -> WeakType
41 | WClassP : Class_ -> list WeakType -> WeakType
42 | WIParam : CoreIPName CoreName -> WeakType -> WeakType.
44 (* EqDecidable instances for WeakType *)
45 Instance WeakTypeVarEqDecidable : EqDecidable WeakTypeVar.
46 apply Build_EqDecidable.
48 destruct v1 as [cv1 k1].
49 destruct v2 as [cv2 k2].
50 destruct (eqd_dec cv1 cv2); subst.
51 destruct (eqd_dec k1 k2); subst.
53 right; intro; apply n; inversion H; subst; auto.
54 right; intro; apply n; inversion H; subst; auto.
57 (* a WeakCoerVar just wraps a CoreVar and tags it with the pair of types amongst which it coerces *)
58 Inductive WeakCoerVar := weakCoerVar : CoreVar -> Kind -> WeakType -> WeakType -> WeakCoerVar.
60 Inductive WeakCoercion : Type :=
61 | WCoVar : WeakCoerVar -> WeakCoercion (* g *)
62 | WCoType : WeakType -> WeakCoercion (* τ *)
63 | WCoApp : WeakCoercion -> WeakCoercion -> WeakCoercion (* γ γ *)
64 | WCoAppT : WeakCoercion -> WeakType -> WeakCoercion (* γ@v *)
65 | WCoAll : Kind -> (WeakTypeVar -> WeakCoercion) -> WeakCoercion (* ∀a:κ.γ *)
66 | WCoSym : WeakCoercion -> WeakCoercion (* sym *)
67 | WCoComp : WeakCoercion -> WeakCoercion -> WeakCoercion (* ◯ *)
68 | WCoLeft : WeakCoercion -> WeakCoercion (* left *)
69 | WCoRight : WeakCoercion -> WeakCoercion (* right *)
70 | WCoUnsafe : WeakType -> WeakType -> WeakCoercion (* unsafe *)
71 (*| WCoCFApp : ∀ n, CoFunConst n -> vec WeakCoercion n -> WeakCoercion (* C γⁿ *)*)
72 (*| WCoTFApp : ∀ n, TyFunConst n -> vec WeakCoercion n -> WeakCoercion (* S_n γⁿ *)*)
75 Variable Prelude_error : forall {A}, string -> A. Extract Inlined Constant Prelude_error => "Prelude.error".
76 Fixpoint weakCoercionTypes (wc:WeakCoercion) : WeakType * WeakType :=
78 | WCoVar (weakCoerVar _ _ t1 t2) => (t1,t2)
79 | WCoType t => Prelude_error "FIXME WCoType"
80 | WCoApp c1 c2 => Prelude_error "FIXME WCoApp"
81 | WCoAppT c t => Prelude_error "FIXME WCoAppT"
82 | WCoAll k f => Prelude_error "FIXME WCoAll"
83 | WCoSym c => let (t2,t1) := weakCoercionTypes c in (t1,t2)
84 | WCoComp c1 c2 => Prelude_error "FIXME WCoComp"
85 | WCoLeft c => Prelude_error "FIXME WCoLeft"
86 | WCoRight c => Prelude_error "FIXME WCoRight"
87 | WCoUnsafe t1 t2 => (t1,t2)
90 Variable ModalBoxTyCon : TyCon. Extract Inlined Constant ModalBoxTyCon => "TysWiredIn.hetMetCodeTypeTyCon".
91 Variable ArrowTyCon : TyCon. Extract Constant ArrowTyCon => "Type.funTyCon".
93 Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
95 | WTyVarTy (weakTypeVar v _) => TyVarTy v
96 | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
97 | WAppTy t1 t2 => match (weakTypeToCoreType t1) with
98 | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
99 | t1' => AppTy t1' (weakTypeToCoreType t2)
101 | WTyCon tc => TyConApp tc nil
102 | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt)
103 | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt))
104 | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty))
105 | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
106 | WFunTyCon => TyConApp ArrowTyCon nil
107 | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
108 | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
109 (weakTypeToCoreType t3)
112 Instance WeakTypeToString : ToString WeakType :=
113 { toString := coreTypeToString ○ weakTypeToCoreType }.