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 compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
60 exact (if eqd_dec cdc cdc0 then true else false).
63 Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
65 Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
67 apply Build_EqDecidable.
69 set (trust_compare_datacons _ v1 v2) as x.
70 set (compare_datacons tc v1 v2) as y.
71 assert (y=compare_datacons tc v1 v2). reflexivity.
72 destruct y; rewrite <- H in x.
77 Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
79 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
82 (* TV is the PHOAS type which stands for type variables of System FC *)
83 Context {TV:Kind -> Type}.
85 (* Figure 7: ρ, σ, τ, ν *)
86 Inductive RawHaskType : Kind -> Type :=
87 | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
88 | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
89 | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
90 | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
91 | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
92 | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
93 | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
94 | TyFunApp : ∀ tf, RawHaskTypeList (fst (tyFunKind tf)) -> RawHaskType (snd (tyFunKind tf)) (* S_n *)
95 with RawHaskTypeList : list Kind -> Type :=
96 | TyFunApp_nil : RawHaskTypeList nil
97 | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
99 (* the "kind" of a coercion is a pair of types *)
100 Inductive RawCoercionKind : Type :=
101 mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
105 (* the PHOAS type which stands for coercion variables of System FC *)
109 Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
111 | CoVar : CV -> RawHaskCoer (* g *)
112 | CoType : RawHaskType -> RawHaskCoer (* τ *)
113 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
114 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
115 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
116 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
117 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
118 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
119 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
120 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
121 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
126 Implicit Arguments TCon [ [TV] ].
127 Implicit Arguments TyFunApp [ [TV] ].
128 Implicit Arguments RawHaskType [ ].
129 Implicit Arguments RawHaskCoer [ ].
130 Implicit Arguments RawCoercionKind [ ].
131 Implicit Arguments TVar [ [TV] [κ] ].
132 Implicit Arguments TCoerc [ [TV] [κ] ].
133 Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ].
134 Implicit Arguments TAll [ [TV] ].
136 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
137 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
139 (* Kind and Coercion Environments *)
141 * In System FC, the environment consists of three components, each of
142 * whose well-formedness depends on all of those prior to it:
144 * 1. (TypeEnv) The list of free type variables and their kinds
145 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
146 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
149 Definition TypeEnv := list Kind.
150 Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ.
151 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
152 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
153 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
155 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
156 Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
157 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
158 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★).
159 Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
160 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
162 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
163 haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
164 Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
165 Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
167 haskTypeOfSomeKind κ _ => κ
169 Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
170 Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
171 match htosk as H return HaskType Γ H with
172 haskTypeOfSomeKind _ ht => ht
174 Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
176 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
177 @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
178 Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
180 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
181 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
182 := fun TV env => TAll κ (σ TV env).
183 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
184 (cv:HaskTyVar Γ κ) : HaskType Γ ★
185 := fun TV env => σ TV env (cv TV env).
186 Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
187 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
188 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
189 := fun TV ite => TCon tc.
190 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
191 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
192 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
193 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
195 (* PHOAS substitution on types *)
196 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
199 (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
202 | TAll _ y => TAll _ (fun v => flattenT _ (y (TVar v)))
203 | TApp _ _ x y => TApp (flattenT _ x) (flattenT _ y)
205 | TCoerc _ t1 t2 t => TCoerc (flattenT _ t1) (flattenT _ t2) (flattenT _ t)
207 | TCode v e => TCode (flattenT _ v) (flattenT _ e)
208 | TyFunApp tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
210 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
211 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
212 | TyFunApp_nil => TyFunApp_nil
213 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest)
215 for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
217 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
218 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
219 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
221 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
222 match lht with t@@l => t end.
229 (* yeah, things are kind of messy below this point *)
232 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
234 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
235 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
236 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
237 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
238 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
239 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
240 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
242 unfold InstantiatedCoercionEnv.
243 unfold addKindToCoercionEnv.
245 rewrite <- map_preserves_length.
248 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
249 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
250 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
251 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
253 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
254 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
256 unfold addCoercionToCoercionEnv; simpl.
257 unfold InstantiatedCoercionEnv; simpl.
258 apply vec_cons; auto.
260 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
261 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
263 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
264 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
265 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
266 := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
267 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
268 := fun TV ite => (cv' TV (weakITE ite)).
269 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
270 induction κ; auto. apply weakV; auto. Defined.
271 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
272 := fun TV ite => lt TV (weakITE ite).
273 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
275 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
276 induction κ; auto. apply weakT; auto. Defined.
277 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
278 unfold HaskType in *.
279 unfold InstantiatedTypeEnv in *.
281 apply ilist_chop in X.
285 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
286 rewrite <- ass_app in lt.
289 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
290 induction κ; auto. apply weakL; auto. Defined.
291 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
292 := match lt with t @@ l => weakT t @@ weakL l end.
293 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
294 := match lt with t @@ l => weakT' t @@ weakL' l end.
295 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
296 induction κ; auto. apply weakCE; auto. Defined.
297 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
298 : InstantiatedCoercionEnv TV CV Γ Δ.
300 unfold InstantiatedCoercionEnv; intros.
301 unfold InstantiatedCoercionEnv in ice.
302 unfold weakCE in ice.
304 rewrite <- map_preserves_length in ice.
307 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
308 unfold HaskCoercionKind in *.
310 apply hck; clear hck.
311 inversion X; subst; auto.
313 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
319 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
320 match κ as K return list (HaskCoercionKind (app K Γ)) with
322 | _ => map weakCK' hck
325 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
327 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
328 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
329 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
330 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
331 := fun TV ite tv => (f TV (weakITE ite) tv).
333 (* I keep mixing up left/right folds *)
334 (* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
335 (*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
337 Fixpoint caseType0 {Γ}(lk:list Kind) :
338 IList _ (HaskType Γ) lk ->
339 HaskType Γ (fold_right KindArrow ★ lk) ->
341 match lk as LK return
342 IList _ (HaskType Γ) LK ->
343 HaskType Γ (fold_right KindArrow ★ LK) ->
346 | nil => fun _ ht => ht
347 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
350 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
351 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
353 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
354 Record StrongAltCon {tc:TyCon} :=
356 ; sac_altcon : WeakAltCon
357 ; sac_numExTyVars : nat
358 ; sac_numCoerVars : nat
359 ; sac_numExprVars : nat
360 ; sac_ekinds : vec Kind sac_numExTyVars
361 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
362 ; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
363 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
364 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
365 ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
367 Coercion sac_tc : StrongAltCon >-> TyCon.
368 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
371 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
373 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
375 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
376 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
377 unfold tyConKind' in z.
378 rewrite literal_tycons_are_of_ordinary_kind in z.
383 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
386 `{EQD_VV:EqDecidable VV}{Γ}
387 (ξ:VV -> LeveledHaskType Γ ★)
388 (vt:list (VV * LeveledHaskType Γ ★))
389 : VV -> LeveledHaskType Γ ★ :=
392 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
397 (***************************************************************************************************)
398 (* Well-Formedness of Types and Coercions *)
399 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
400 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
401 mkTFD : Kind -> TypeFunctionDecl tfc vk.
405 Context {TV:Kind->Type}.
408 (* local notations *)
409 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
410 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
411 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
412 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
413 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
415 (* Figure 8, lower half *)
416 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
417 @InstantiatedTypeEnv TV Γ ->
418 @InstantiatedCoercionEnv TV CV Γ Δ ->
419 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
420 | CoTVar':∀ Γ Δ t e c σ τ,
421 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
422 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
423 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
424 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
425 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
426 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
428 | SComp :∀ Γ Δ t e γ n S σ τ κ,
429 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
430 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
431 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
432 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
433 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
434 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
436 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
437 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
438 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
439 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
440 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
441 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
442 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
443 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
444 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
446 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
447 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
448 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
449 @InstantiatedTypeEnv TV Γ ->
450 InstantiatedCoercionEnv TV CV Γ Δ ->
451 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
452 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
453 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
454 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
455 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
458 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
459 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
460 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
461 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
467 (* Decidable equality on PHOAS types *)
468 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
470 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
471 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
472 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
473 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
474 | TArrow => match t2 with TArrow => true | _ => false end
475 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
476 | 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
477 | TyFunApp tfc lt => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
479 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
481 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
482 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
485 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
486 match lk as LK return IList _ _ LK with
488 | h::t => n::::(count' t (S n))
491 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
492 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" +++ 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"+++n
567 in "(forall "+++ alpha +++ ":"+++ k +++")"+++
568 typeToString' false (S n) (f n)
569 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
570 | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
572 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
574 | TyFunApp_nil => nil
575 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
578 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
579 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
581 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
582 { toString := typeToString }.