1 (*********************************************************************************************************************************)
2 (* HaskStrongTypes: representation of types and coercions for HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import Coq.Strings.String.
8 Require Import Coq.Lists.List.
9 Require Import General.
10 Require Import HaskKinds.
11 Require Import HaskLiteralsAndTyCons.
12 Require Import HaskCoreTypes.
13 Require Import HaskCoreVars.
14 Require Import HaskWeakTypes.
15 Require Import HaskWeakVars.
16 Require Import HaskWeak.
17 Require Import HaskCoreToWeak.
19 Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
20 Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
21 Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
22 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
24 Definition dataConExTyVars cdc :=
25 filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
26 Opaque dataConExTyVars.
27 Definition dataConCoerKinds cdc :=
28 filter (map (fun x => match x with EqPred t1 t2 =>
30 coreTypeToWeakType t1 >>= fun t1' =>
31 coreTypeToWeakType t2 >>= fun t2' =>
37 end) (dataConEqTheta_ cdc)).
38 Opaque dataConCoerKinds.
39 Definition dataConFieldTypes cdc :=
40 filter (map (fun x => match coreTypeToWeakType x with
43 end) (dataConOrigArgTys_ cdc)).
45 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
46 Coercion tyConNumKinds : TyCon >-> nat.
48 Inductive DataCon : TyCon -> Type :=
49 mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
50 Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
51 Coercion mkDataCon : CoreDataCon >-> DataCon.
52 Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
55 Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
57 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
60 (* TV is the PHOAS type which stands for type variables of System FC *)
61 Context {TV:Kind -> Type}.
63 (* Figure 7: ρ, σ, τ, ν *)
64 Inductive RawHaskType : Kind -> Type :=
65 | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
66 | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
67 | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
68 | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
69 | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
70 | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
71 | TCode : RawHaskType ECKind -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
72 | TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *)
73 with RawHaskTypeList : list Kind -> Type :=
74 | TyFunApp_nil : RawHaskTypeList nil
75 | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
77 (* the "kind" of a coercion is a pair of types *)
78 Inductive RawCoercionKind : Type :=
79 mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
81 (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
82 Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
84 * This has been disabled until we manage to reconcile SystemFC's
85 * coercions with what GHC actually implements (they are not the
88 | CoVar : CV -> RawHaskCoer (* g *)
89 | CoType : RawHaskType -> RawHaskCoer (* τ *)
90 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
91 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
92 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
93 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
94 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
95 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
96 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
97 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
98 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
102 Implicit Arguments TCon [ [TV] ].
103 Implicit Arguments TyFunApp [ [TV] ].
104 Implicit Arguments RawHaskType [ ].
105 Implicit Arguments RawHaskCoer [ ].
106 Implicit Arguments RawCoercionKind [ ].
107 Implicit Arguments TVar [ [TV] [κ] ].
108 Implicit Arguments TCoerc [ [TV] [κ] ].
109 Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ].
110 Implicit Arguments TAll [ [TV] ].
112 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
113 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
115 (* Kind and Coercion Environments *)
117 * In System FC, the environment consists of three components, each of
118 * whose well-formedness depends on all of those prior to it:
120 * 1. (TypeEnv) The list of free type variables and their kinds
121 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
122 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
125 Definition TypeEnv := list Kind.
126 Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ.
127 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
128 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
129 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
131 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
132 Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
133 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
134 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ECKind).
135 Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
136 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
138 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
139 haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
140 Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
141 Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
143 haskTypeOfSomeKind κ _ => κ
145 Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
146 Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
147 match htosk as H return HaskType Γ H with
148 haskTypeOfSomeKind _ ht => ht
150 Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
152 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
153 @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
154 Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
156 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
157 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
158 := fun TV env => TAll κ (σ TV env).
159 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
160 (cv:HaskTyVar Γ κ) : HaskType Γ ★
161 := fun TV env => σ TV env (cv TV env).
162 Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
163 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
164 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
165 := fun TV ite => TCon tc.
166 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
167 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
168 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
169 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
172 Context {TV:Kind -> Type }.
173 Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
176 | TAll _ y => TAll _ (fun v => flattenT (y (TVar v)))
177 | TApp _ _ x y => TApp (flattenT x) (flattenT y)
179 | TCoerc _ t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t)
181 | TCode v e => TCode (flattenT v) (flattenT e)
182 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
184 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
185 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
186 | TyFunApp_nil => TyFunApp_nil
187 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT t) (flattenTyFunApp _ rest)
191 (* PHOAS substitution on types *)
192 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
195 flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
197 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
198 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
199 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
201 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
202 match lht with t@@l => t end.
204 Structure Global Γ :=
205 { glob_wv : WeakExprVar
206 ; glob_kinds : list Kind
207 ; glob_tf : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
209 Coercion glob_tf : Global >-> Funclass.
210 Coercion glob_wv : Global >-> WeakExprVar.
216 (* yeah, things are kind of messy below this point *)
219 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
221 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
222 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
223 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
224 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
225 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
226 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
227 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
229 unfold InstantiatedCoercionEnv.
230 unfold addKindToCoercionEnv.
232 rewrite <- map_preserves_length.
235 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
236 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
237 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
238 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
240 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
241 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
243 unfold addCoercionToCoercionEnv; simpl.
244 unfold InstantiatedCoercionEnv; simpl.
245 apply vec_cons; auto.
247 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
248 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
250 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
251 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
252 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
253 := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
254 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
255 := fun TV ite => (cv' TV (weakITE ite)).
256 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
257 induction κ; auto. apply weakV; auto. Defined.
258 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
259 := fun TV ite => lt TV (weakITE ite).
260 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
262 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
263 induction κ; auto. apply weakT; auto. Defined.
264 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
265 unfold HaskType in *.
266 unfold InstantiatedTypeEnv in *.
268 apply ilist_chop in X.
272 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
273 rewrite <- ass_app in lt.
276 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
277 induction κ; auto. apply weakL; auto. Defined.
278 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
279 := match lt with t @@ l => weakT t @@ weakL l end.
280 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
281 := match lt with t @@ l => weakT' t @@ weakL' l end.
282 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
283 induction κ; auto. apply weakCE; auto. Defined.
284 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
285 : InstantiatedCoercionEnv TV CV Γ Δ.
287 unfold InstantiatedCoercionEnv; intros.
288 unfold InstantiatedCoercionEnv in ice.
289 unfold weakCE in ice.
291 rewrite <- map_preserves_length in ice.
294 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
295 unfold HaskCoercionKind in *.
297 apply hck; clear hck.
298 inversion X; subst; auto.
300 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
305 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
307 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
308 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
309 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
310 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
311 := fun TV ite tv => (f TV (weakITE ite) tv).
313 Fixpoint caseType0 {Γ}(lk:list Kind) :
314 IList _ (HaskType Γ) lk ->
315 HaskType Γ (fold_right KindArrow ★ lk) ->
317 match lk as LK return
318 IList _ (HaskType Γ) LK ->
319 HaskType Γ (fold_right KindArrow ★ LK) ->
322 | nil => fun _ ht => ht
323 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
326 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
327 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
329 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
330 Record StrongAltCon {tc:TyCon} :=
332 ; sac_altcon : WeakAltCon
333 ; sac_numExTyVars : nat
334 ; sac_numCoerVars : nat
335 ; sac_numExprVars : nat
336 ; sac_ekinds : vec Kind sac_numExTyVars
337 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
338 ; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
339 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
340 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
341 ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
343 Coercion sac_tc : StrongAltCon >-> TyCon.
344 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
347 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
349 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
351 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
352 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
353 unfold tyConKind' in z.
354 rewrite literal_tycons_are_of_ordinary_kind in z.
359 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
362 `{EQD_VV:EqDecidable VV}{Γ}
363 (ξ:VV -> LeveledHaskType Γ ★)
365 (vt:list (VV * HaskType Γ ★))
366 : VV -> LeveledHaskType Γ ★ :=
369 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
372 Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
373 not (In v (map (@fst _ _) varstypes)) ->
374 (update_ξ ξ lev varstypes) v = ξ v.
380 destruct (eqd_dec v0 v).
395 (***************************************************************************************************)
396 (* Well-Formedness of Types and Coercions *)
397 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
398 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
399 mkTFD : Kind -> TypeFunctionDecl tfc vk.
403 Context {TV:Kind->Type}.
406 (* local notations *)
407 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
408 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
409 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
410 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
411 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
413 (* Figure 8, lower half *)
414 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
415 @InstantiatedTypeEnv TV Γ ->
416 @InstantiatedCoercionEnv TV CV Γ Δ ->
417 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
418 | CoTVar':∀ Γ Δ t e c σ τ,
419 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
420 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
421 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
422 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
423 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
424 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
426 | SComp :∀ Γ Δ t e γ n S σ τ κ,
427 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
428 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
429 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
430 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
431 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
432 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
434 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
435 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
436 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
437 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
438 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
439 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
440 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
441 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
442 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
444 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
445 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
446 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
447 @InstantiatedTypeEnv TV Γ ->
448 InstantiatedCoercionEnv TV CV Γ Δ ->
449 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
450 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
451 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
452 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
453 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
456 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
457 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
458 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
459 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
465 (* Decidable equality on PHOAS types *)
466 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
468 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
469 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
470 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
471 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
472 | TArrow => match t2 with TArrow => true | _ => false end
473 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
474 | TCoerc _ t1 t2 t => match t2 with TCoerc _ t1' t2' t' => compareT n t1 t1' && compareT n t2 t2' && compareT n t t' | _ =>false end
475 | TyFunApp tfc kl k lt => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
477 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
479 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
480 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
483 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
484 match lk as LK return IList _ _ LK with
486 | h::t => n::::(count' t (S n))
489 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
490 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
494 * This is not provable in Coq's logic because the Coq function space
495 * is "too big" - although its only definable inhabitants are Coq
496 * functions, it is not provable in Coq that all function space
497 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
498 * This is actually an important feature of Coq: it lets us reason
499 * about properties of non-computable (non-recursive) functions since
500 * any property proven to hold for the entire function space will hold
501 * even for those functions. However when representing binding
502 * structure using functions we would actually prefer the smaller
503 * function-space of *definable* functions only. These two axioms
505 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
506 if compareHT Γ κ ht1 ht2
509 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
510 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
514 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
515 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
516 apply Build_EqDecidable.
518 set (compareHT_decides _ _ v1 v2) as z.
519 set (compareHT Γ κ v1 v2) as q.
520 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
525 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
526 apply Build_EqDecidable.
528 set (compareVars _ _ v1 v2) as z.
529 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
530 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
535 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
536 apply Build_EqDecidable.
538 unfold HaskLevel in *.
539 apply (eqd_dec v1 v2).
546 (* ToString instance for PHOAS types *)
547 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
549 | TVar _ v => "tv" +++ toString v
550 | TCon tc => toString tc
551 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
552 +++typeToString' false n t2+++")=>"
553 +++typeToString' needparens n t
556 | TApp _ _ TArrow t1 =>
558 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
559 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
562 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
563 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
566 | TAll k f => let alpha := "tv"+++ toString n
567 in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
568 typeToString' false (S n) (f n)
569 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
570 | TyFunApp tfc kl k lt => toString tfc+++ "_" +++ toString n+++" ["+++
571 (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
573 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
575 | TyFunApp_nil => nil
576 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
579 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
580 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
582 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
583 { toString := typeToString }.