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 HaskLiterals.
12 Require Import HaskTyCons.
13 Require Import HaskCoreTypes.
14 Require Import HaskCoreVars.
15 Require Import HaskWeakTypes.
16 Require Import HaskWeakVars.
17 Require Import HaskWeak.
18 Require Import HaskCoreToWeak.
20 Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
21 Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
22 Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConTheta".
23 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
25 Definition dataConExTyVars cdc :=
26 filter (map (fun x => match coreVarToWeakVar' x with OK (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 ECKind -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
73 | TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* 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.
82 (* Figure 7: γ, δ; CV is the PHOAS type which stands for coercion variables of System FC *)
83 Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := .
85 * This has been disabled until we manage to reconcile SystemFC's
86 * coercions with what GHC actually implements (they are not the
89 | CoVar : CV -> RawHaskCoer (* g *)
90 | CoType : RawHaskType -> RawHaskCoer (* τ *)
91 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
92 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
93 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
94 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
95 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
96 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
97 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
98 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
99 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
103 Implicit Arguments TCon [ [TV] ].
104 Implicit Arguments TyFunApp [ [TV] ].
105 Implicit Arguments RawHaskType [ ].
106 Implicit Arguments RawHaskCoer [ ].
107 Implicit Arguments RawCoercionKind [ ].
108 Implicit Arguments TVar [ [TV] [κ] ].
109 Implicit Arguments TCoerc [ [TV] [κ] ].
110 Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ].
111 Implicit Arguments TAll [ [TV] ].
113 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
114 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
116 (* Kind and Coercion Environments *)
118 * In System FC, the environment consists of three components, each of
119 * whose well-formedness depends on all of those prior to it:
121 * 1. (TypeEnv) The list of free type variables and their kinds
122 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
123 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
126 Definition TypeEnv := list Kind.
127 Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ.
128 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
129 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
130 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
132 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
133 Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
134 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
135 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ECKind).
136 Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
137 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
139 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
140 haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
141 Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
142 Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
144 haskTypeOfSomeKind κ _ => κ
146 Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
147 Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
148 match htosk as H return HaskType Γ H with
149 haskTypeOfSomeKind _ ht => ht
151 Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
153 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
154 @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
155 Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
157 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
158 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
159 := fun TV env => TAll κ (σ TV env).
160 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
161 (cv:HaskTyVar Γ κ) : HaskType Γ ★
162 := fun TV env => σ TV env (cv TV env).
163 Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
164 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
165 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
166 := fun TV ite => TCon tc.
167 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
168 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
169 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
170 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
173 Context {TV:Kind -> Type }.
174 Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
177 | TAll _ y => TAll _ (fun v => flattenT (y (TVar v)))
178 | TApp _ _ x y => TApp (flattenT x) (flattenT y)
180 | TCoerc _ t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t)
182 | TCode v e => TCode (flattenT v) (flattenT e)
183 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
185 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
186 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
187 | TyFunApp_nil => TyFunApp_nil
188 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT t) (flattenTyFunApp _ rest)
192 (* PHOAS substitution on types *)
193 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
196 flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
198 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
199 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
200 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
202 Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
204 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
205 match lht with t@@l => t end.
207 Structure Global Γ :=
208 { glob_wv : WeakExprVar
209 ; glob_kinds : list Kind
210 ; glob_tf : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
212 Coercion glob_tf : Global >-> Funclass.
213 Coercion glob_wv : Global >-> WeakExprVar.
215 (* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
216 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
217 Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
218 match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
220 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
222 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
223 | KindStar => fun x' =>
224 match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
225 | TApp κ₁'' κ₂'' w'' x'' =>
226 match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
227 list (RawHaskType _ KindStar) with
230 | TArrow => fun a b => a::b
231 | _ => fun _ _ => nil
233 | _ => fun _ _ => nil
237 | _ => fun _ _ => nil
239 | _ => fun _ _ => nil
240 end) x (take_arg_types y)
244 Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
245 match exp as E in RawHaskType _ K return nat with
247 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
249 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
250 | KindStar => fun x' =>
251 match x' return nat -> nat with
252 | TApp κ₁'' κ₂'' w'' x'' =>
253 match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
256 | TArrow => fun a b => S b
266 end) x (count_arg_types y)
270 Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
278 Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
281 match take_arg_types (ht TV ite) with
282 | nil => Prelude_error "impossible"
286 (* From (t1->(t2->(t3-> ... t))), return t *)
287 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
288 Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
289 match exp as E in RawHaskType _ K return RawHaskType _ K with
292 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
294 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
295 | KindStar => fun x' =>
296 match x' return (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
297 | TApp κ₁'' κ₂'' w'' x'' =>
298 match κ₂'' as K2'' return RawHaskType TV K2'' -> (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
301 | TArrow => fun _ b => Some b
302 | _ => fun _ b => None
304 | _ => fun _ b => None
308 | _ => fun _ _ => None
310 | _ => fun _ _ => None
311 end) x (drop_arg_types y)
322 (* yeah, things are kind of messy below this point *)
325 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
327 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
328 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
329 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
330 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
331 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
332 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
333 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
335 unfold InstantiatedCoercionEnv.
336 unfold addKindToCoercionEnv.
338 rewrite <- map_preserves_length.
341 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
342 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
343 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
344 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
346 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
347 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
349 unfold addCoercionToCoercionEnv; simpl.
350 unfold InstantiatedCoercionEnv; simpl.
351 apply vec_cons; auto.
353 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
354 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
356 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
357 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
358 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
359 := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
360 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
361 := fun TV ite => (cv' TV (weakITE ite)).
362 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
363 induction κ; auto. apply weakV; auto. Defined.
364 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
365 := fun TV ite => lt TV (weakITE ite).
366 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
368 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
369 induction κ; auto. apply weakT; auto. Defined.
370 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
371 unfold HaskType in *.
372 unfold InstantiatedTypeEnv in *.
374 apply ilist_chop in X.
378 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
379 rewrite <- ass_app in lt.
382 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
383 induction κ; auto. apply weakL; auto. Defined.
384 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
385 := match lt with t @@ l => weakT t @@ weakL l end.
386 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
387 := match lt with t @@ l => weakT' t @@ weakL' l end.
388 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
389 induction κ; auto. apply weakCE; auto. Defined.
390 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
391 : InstantiatedCoercionEnv TV CV Γ Δ.
393 unfold InstantiatedCoercionEnv; intros.
394 unfold InstantiatedCoercionEnv in ice.
395 unfold weakCE in ice.
397 rewrite <- map_preserves_length in ice.
400 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
401 unfold HaskCoercionKind in *.
403 apply hck; clear hck.
404 inversion X; subst; auto.
406 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
411 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
413 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
414 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
415 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
416 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
417 := fun TV ite tv => (f TV (weakITE ite) tv).
419 Fixpoint caseType0 {Γ}(lk:list Kind) :
420 IList _ (HaskType Γ) lk ->
421 HaskType Γ (fold_right KindArrow ★ lk) ->
423 match lk as LK return
424 IList _ (HaskType Γ) LK ->
425 HaskType Γ (fold_right KindArrow ★ LK) ->
428 | nil => fun _ ht => ht
429 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
432 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
433 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
435 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
436 Record StrongAltCon {tc:TyCon} :=
438 ; sac_altcon : WeakAltCon
439 ; sac_numExTyVars : nat
440 ; sac_numCoerVars : nat
441 ; sac_numExprVars : nat
442 ; sac_ekinds : vec Kind sac_numExTyVars
443 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
444 ; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ
445 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
446 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
447 ; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
449 Coercion sac_tc : StrongAltCon >-> TyCon.
450 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
453 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
455 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
457 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
458 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
459 unfold tyConKind' in z.
460 rewrite literal_tycons_are_of_ordinary_kind in z.
465 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
468 `{EQD_VV:EqDecidable VV}{Γ}
469 (ξ:VV -> LeveledHaskType Γ ★)
471 (vt:list (VV * HaskType Γ ★))
472 : VV -> LeveledHaskType Γ ★ :=
475 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
478 Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
479 not (In v (map (@fst _ _) varstypes)) ->
480 (update_xi ξ lev varstypes) v = ξ v.
486 destruct (eqd_dec v0 v).
501 (***************************************************************************************************)
502 (* Well-Formedness of Types and Coercions *)
503 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
504 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
505 mkTFD : Kind -> TypeFunctionDecl tfc vk.
509 Context {TV:Kind->Type}.
512 (* local notations *)
513 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
514 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
515 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
516 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
517 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
519 (* Figure 8, lower half *)
520 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
521 @InstantiatedTypeEnv TV Γ ->
522 @InstantiatedCoercionEnv TV CV Γ Δ ->
523 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
524 | CoTVar':∀ Γ Δ t e c σ τ,
525 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
526 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
527 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
528 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
529 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
530 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
532 | SComp :∀ Γ Δ t e γ n S σ τ κ,
533 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
534 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
535 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
536 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
537 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
538 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
540 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
541 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
542 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
543 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
544 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
545 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
546 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
547 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
548 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
550 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
551 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
552 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
553 @InstantiatedTypeEnv TV Γ ->
554 InstantiatedCoercionEnv TV CV Γ Δ ->
555 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
556 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
557 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
558 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
559 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
562 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
563 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
564 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
565 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
571 (* Decidable equality on PHOAS types *)
572 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
574 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
575 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
576 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
577 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
578 | TArrow => match t2 with TArrow => true | _ => false end
579 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
580 | 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
581 | TyFunApp tfc kl k lt => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
583 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
585 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
586 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
589 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
590 match lk as LK return IList _ _ LK with
592 | h::t => n::::(count' t (S n))
595 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
596 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
600 * This is not provable in Coq's logic because the Coq function space
601 * is "too big" - although its only definable inhabitants are Coq
602 * functions, it is not provable in Coq that all function space
603 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
604 * This is actually an important feature of Coq: it lets us reason
605 * about properties of non-computable (non-recursive) functions since
606 * any property proven to hold for the entire function space will hold
607 * even for those functions. However when representing binding
608 * structure using functions we would actually prefer the smaller
609 * function-space of *definable* functions only. These two axioms
611 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
612 if compareHT Γ κ ht1 ht2
615 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
616 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
620 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
621 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
622 apply Build_EqDecidable.
624 set (compareHT_decides _ _ v1 v2) as z.
625 set (compareHT Γ κ v1 v2) as q.
626 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
631 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
632 apply Build_EqDecidable.
634 set (compareVars _ _ v1 v2) as z.
635 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
636 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
641 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
642 apply Build_EqDecidable.
644 unfold HaskLevel in *.
645 apply (eqd_dec v1 v2).
652 (* ToString instance for PHOAS types *)
653 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
655 | TVar _ v => "tv" +++ toString v
656 | TCon tc => toString tc
657 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
658 +++typeToString' false n t2+++")=>"
659 +++typeToString' needparens n t
662 | TApp _ _ TArrow t1 =>
664 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
665 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
668 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
669 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
672 | TAll k f => let alpha := "tv"+++ toString n
673 in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
674 typeToString' false (S n) (f n)
675 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
676 | TyFunApp tfc kl k lt => toString tfc+++ "_" +++ toString n+++" ["+++
677 (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
679 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
681 | TyFunApp_nil => nil
682 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
685 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
686 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
688 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
689 { toString := typeToString }.