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 (* TODO: might be a better idea to panic here than simply drop things that look wrong *)
25 Definition dataConExTyVars cdc :=
26 filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
27 Opaque dataConExTyVars.
28 Definition dataConCoerKinds cdc :=
29 filter (map (fun x => match x with EqPred t1 t2 =>
31 coreTypeToWeakType t1 >>= fun t1' =>
32 coreTypeToWeakType t2 >>= fun t2' =>
38 end) (dataConEqTheta_ cdc)).
39 Opaque dataConCoerKinds.
40 Definition dataConFieldTypes cdc :=
41 filter (map (fun x => match coreTypeToWeakType x with
44 end) (dataConOrigArgTys_ cdc)).
46 Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc).
47 Coercion tyConNumKinds : TyCon >-> nat.
49 Inductive DataCon : TyCon -> Type :=
50 mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc).
51 Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end.
52 Coercion mkDataCon : CoreDataCon >-> DataCon.
53 Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon.
56 Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
58 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
61 (* TV is the PHOAS type which stands for type variables of System FC *)
62 Context {TV:Kind -> Type}.
64 (* Figure 7: ρ, σ, τ, ν *)
65 Inductive RawHaskType : Kind -> Type :=
66 | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
67 | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
68 | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
69 | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
70 | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
71 | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
72 | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
73 | TyFunApp : ∀ tf, RawHaskTypeList (fst (tyFunKind tf)) -> RawHaskType (snd (tyFunKind tf)) (* S_n *)
74 with RawHaskTypeList : list Kind -> Type :=
75 | TyFunApp_nil : RawHaskTypeList nil
76 | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
78 (* the "kind" of a coercion is a pair of types *)
79 Inductive RawCoercionKind : Type :=
80 mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
84 (* the PHOAS type which stands for coercion variables of System FC *)
88 Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
90 | CoVar : CV -> RawHaskCoer (* g *)
91 | CoType : RawHaskType -> RawHaskCoer (* τ *)
92 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
93 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
94 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
95 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
96 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
97 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
98 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
99 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
100 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
105 Implicit Arguments TCon [ [TV] ].
106 Implicit Arguments TyFunApp [ [TV] ].
107 Implicit Arguments RawHaskType [ ].
108 Implicit Arguments RawHaskCoer [ ].
109 Implicit Arguments RawCoercionKind [ ].
110 Implicit Arguments TVar [ [TV] [κ] ].
111 Implicit Arguments TCoerc [ [TV] [κ] ].
112 Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ].
113 Implicit Arguments TAll [ [TV] ].
115 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
116 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
118 (* Kind and Coercion Environments *)
120 * In System FC, the environment consists of three components, each of
121 * whose well-formedness depends on all of those prior to it:
123 * 1. (TypeEnv) The list of free type variables and their kinds
124 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
125 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
128 Definition TypeEnv := list Kind.
129 Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ.
130 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
131 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
132 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
134 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
135 Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
136 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
137 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★).
138 Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
139 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
141 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
142 haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
143 Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
144 Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
146 haskTypeOfSomeKind κ _ => κ
148 Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
149 Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
150 match htosk as H return HaskType Γ H with
151 haskTypeOfSomeKind _ ht => ht
153 Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
155 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
156 @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
157 Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
159 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
160 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
161 := fun TV env => TAll κ (σ TV env).
162 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
163 (cv:HaskTyVar Γ κ) : HaskType Γ ★
164 := fun TV env => σ TV env (cv TV env).
165 Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
166 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
167 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
168 := fun TV ite => TCon tc.
169 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
170 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
171 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
172 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
174 (* PHOAS substitution on types *)
175 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
178 (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
181 | TAll _ y => TAll _ (fun v => flattenT _ (y (TVar v)))
182 | TApp _ _ x y => TApp (flattenT _ x) (flattenT _ y)
184 | TCoerc _ t1 t2 t => TCoerc (flattenT _ t1) (flattenT _ t2) (flattenT _ t)
186 | TCode v e => TCode (flattenT _ v) (flattenT _ e)
187 | TyFunApp tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
189 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
190 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
191 | TyFunApp_nil => TyFunApp_nil
192 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest)
194 for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
196 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
197 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
198 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
200 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
201 match lht with t@@l => t end.
208 (* yeah, things are kind of messy below this point *)
211 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
213 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
214 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
215 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
216 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
217 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
218 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
219 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
221 unfold InstantiatedCoercionEnv.
222 unfold addKindToCoercionEnv.
224 rewrite <- map_preserves_length.
227 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
228 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
229 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
230 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
232 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
233 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
235 unfold addCoercionToCoercionEnv; simpl.
236 unfold InstantiatedCoercionEnv; simpl.
237 apply vec_cons; auto.
239 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
240 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
242 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
243 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
244 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
245 := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
246 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
247 := fun TV ite => (cv' TV (weakITE ite)).
248 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
249 induction κ; auto. apply weakV; auto. Defined.
250 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
251 := fun TV ite => lt TV (weakITE ite).
252 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
254 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
255 induction κ; auto. apply weakT; auto. Defined.
256 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
257 unfold HaskType in *.
258 unfold InstantiatedTypeEnv in *.
260 apply ilist_chop in X.
264 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
265 rewrite <- ass_app in lt.
268 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
269 induction κ; auto. apply weakL; auto. Defined.
270 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
271 := match lt with t @@ l => weakT t @@ weakL l end.
272 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
273 := match lt with t @@ l => weakT' t @@ weakL' l end.
274 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
275 induction κ; auto. apply weakCE; auto. Defined.
276 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
277 : InstantiatedCoercionEnv TV CV Γ Δ.
279 unfold InstantiatedCoercionEnv; intros.
280 unfold InstantiatedCoercionEnv in ice.
281 unfold weakCE in ice.
283 rewrite <- map_preserves_length in ice.
286 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
287 unfold HaskCoercionKind in *.
289 apply hck; clear hck.
290 inversion X; subst; auto.
292 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
298 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
299 match κ as K return list (HaskCoercionKind (app K Γ)) with
301 | _ => map weakCK' hck
304 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
306 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
307 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
308 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
309 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
310 := fun TV ite tv => (f TV (weakITE ite) tv).
312 (* I keep mixing up left/right folds *)
313 (* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
314 (*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
316 Fixpoint caseType0 {Γ}(lk:list Kind) :
317 IList _ (HaskType Γ) lk ->
318 HaskType Γ (fold_right KindArrow ★ lk) ->
320 match lk as LK return
321 IList _ (HaskType Γ) LK ->
322 HaskType Γ (fold_right KindArrow ★ LK) ->
325 | nil => fun _ ht => ht
326 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
329 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
330 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
332 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
333 Record StrongAltCon {tc:TyCon} :=
335 ; sac_altcon : WeakAltCon
336 ; sac_numExTyVars : nat
337 ; sac_numCoerVars : nat
338 ; sac_numExprVars : nat
339 ; sac_ekinds : vec Kind sac_numExTyVars
340 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
341 ; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
342 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
343 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
344 ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
346 Coercion sac_tc : StrongAltCon >-> TyCon.
347 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
350 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
352 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
354 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
355 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
356 unfold tyConKind' in z.
357 rewrite literal_tycons_are_of_ordinary_kind in z.
362 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
365 `{EQD_VV:EqDecidable VV}{Γ}
366 (ξ:VV -> LeveledHaskType Γ ★)
368 (vt:list (VV * HaskType Γ ★))
369 : VV -> LeveledHaskType Γ ★ :=
372 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
375 Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
376 not (In v (map (@fst _ _) varstypes)) ->
377 (update_ξ ξ lev varstypes) v = ξ v.
383 destruct (eqd_dec v0 v).
398 (***************************************************************************************************)
399 (* Well-Formedness of Types and Coercions *)
400 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
401 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
402 mkTFD : Kind -> TypeFunctionDecl tfc vk.
406 Context {TV:Kind->Type}.
409 (* local notations *)
410 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
411 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
412 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
413 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
414 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
416 (* Figure 8, lower half *)
417 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
418 @InstantiatedTypeEnv TV Γ ->
419 @InstantiatedCoercionEnv TV CV Γ Δ ->
420 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
421 | CoTVar':∀ Γ Δ t e c σ τ,
422 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
423 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
424 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
425 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
426 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
427 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
429 | SComp :∀ Γ Δ t e γ n S σ τ κ,
430 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
431 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
432 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
433 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
434 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
435 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
437 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
438 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
439 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
440 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
441 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
442 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
443 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
444 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
445 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
447 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
448 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
449 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
450 @InstantiatedTypeEnv TV Γ ->
451 InstantiatedCoercionEnv TV CV Γ Δ ->
452 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
453 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
454 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
455 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
456 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
459 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
460 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
461 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
462 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
468 (* Decidable equality on PHOAS types *)
469 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
471 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
472 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
473 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
474 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
475 | TArrow => match t2 with TArrow => true | _ => false end
476 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
477 | 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
478 | TyFunApp tfc lt => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
480 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
482 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
483 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
486 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
487 match lk as LK return IList _ _ LK with
489 | h::t => n::::(count' t (S n))
492 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
493 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
495 (* This is not provable in Coq's logic because the Coq function space
496 * is "too big" - although its only definable inhabitants are Coq
497 * functions, it is not provable in Coq that all function space
498 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
499 * This is actually an important feature of Coq: it lets us reason
500 * about properties of non-computable (non-recursive) functions since
501 * any property proven to hold for the entire function space will hold
502 * even for those functions. However when representing binding
503 * structure using functions we would actually prefer the smaller
504 * function-space of *definable* functions only. These two axioms
506 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
507 if compareHT Γ κ ht1 ht2
510 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
511 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
515 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
516 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
517 apply Build_EqDecidable.
519 set (compareHT_decides _ _ v1 v2) as z.
520 set (compareHT Γ κ v1 v2) as q.
521 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
526 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
527 apply Build_EqDecidable.
529 set (compareVars _ _ v1 v2) as z.
530 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
531 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
536 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
537 apply Build_EqDecidable.
539 unfold HaskLevel in *.
540 apply (eqd_dec v1 v2).
547 (* ToString instance for PHOAS types *)
548 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
550 | TVar _ v => "tv" +++ toString v
551 | TCon tc => toString tc
552 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
553 +++typeToString' false n t2+++")=>"
554 +++typeToString' needparens n t
557 | TApp _ _ TArrow t1 =>
559 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
560 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
563 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
564 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
567 | TAll k f => let alpha := "tv"+++ toString n
568 in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
569 typeToString' false (S n) (f n)
570 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
571 | TyFunApp tfc lt => toString tfc+++ "_" +++ toString n+++" ["+++
572 (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
574 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
576 | TyFunApp_nil => nil
577 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
580 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
581 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
583 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
584 { toString := typeToString }.