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.
159 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
160 := fun TV env => TAll κ (σ TV env).
161 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
162 (cv:HaskTyVar Γ κ) : HaskType Γ ★
163 := fun TV env => σ TV env (cv TV env).
164 Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:=
165 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
166 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
167 := fun TV ite => TCon tc.
168 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
169 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
170 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
171 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
174 Context {TV:Kind -> Type }.
175 Fixpoint flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
178 | TAll _ y => TAll _ (fun v => flattenT (y (TVar v)))
179 | TApp _ _ x y => TApp (flattenT x) (flattenT y)
181 | TCoerc _ t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t)
183 | TCode v e => TCode (flattenT v) (flattenT e)
184 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (flattenTyFunApp _ lt)
186 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
187 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
188 | TyFunApp_nil => TyFunApp_nil
189 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT t) (flattenTyFunApp _ rest)
193 (* PHOAS substitution on types *)
194 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
197 flattenT (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
199 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
200 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
201 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
203 Definition getlev {Γ}(lt:LeveledHaskType Γ ★) := match lt with _ @@ l => l end.
205 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
206 match lht with t@@l => t end.
208 Structure Global Γ :=
209 { glob_wv : WeakExprVar
210 ; glob_kinds : list Kind
211 ; glob_tf : IList _ (fun κ => HaskType Γ κ) glob_kinds -> HaskType Γ ★
213 Coercion glob_tf : Global >-> Funclass.
214 Coercion glob_wv : Global >-> WeakExprVar.
216 (* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
217 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
218 Fixpoint take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
219 match exp as E in RawHaskType _ K return list (RawHaskType _ K) with
221 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> list (RawHaskType TV κ₂) -> list (RawHaskType _ K1) with
223 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> list (RawHaskType TV K2) -> list (RawHaskType _ KindStar) with
224 | KindStar => fun x' =>
225 match x' return list (RawHaskType TV KindStar) -> list (RawHaskType _ KindStar) with
226 | TApp κ₁'' κ₂'' w'' x'' =>
227 match κ₂'' as K2'' return RawHaskType TV K2'' -> list (RawHaskType TV KindStar) ->
228 list (RawHaskType _ KindStar) with
231 | TArrow => fun a b => a::b
232 | _ => fun _ _ => nil
234 | _ => fun _ _ => nil
238 | _ => fun _ _ => nil
240 | _ => fun _ _ => nil
241 end) x (take_arg_types y)
245 Fixpoint count_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : nat :=
246 match exp as E in RawHaskType _ K return nat with
248 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> nat -> nat with
250 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> nat -> nat with
251 | KindStar => fun x' =>
252 match x' return nat -> nat with
253 | TApp κ₁'' κ₂'' w'' x'' =>
254 match κ₂'' as K2'' return RawHaskType TV K2'' -> nat -> nat with
257 | TArrow => fun a b => S b
267 end) x (count_arg_types y)
271 Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
279 Definition take_arg_type {Γ}{κ}(ht:HaskType Γ κ) : (gt (count_arg_types (ht _ (ite_unit _))) 0) -> HaskType Γ κ :=
282 match take_arg_types (ht TV ite) with
283 | nil => Prelude_error "impossible"
287 (* From (t1->(t2->(t3-> ... t))), return t *)
288 (* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
289 Fixpoint drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ :=
290 match exp as E in RawHaskType _ K return RawHaskType _ K with
293 (match κ₁ as K1 return RawHaskType TV (κ₂ ⇛ K1) -> (RawHaskType TV κ₂) -> ??(RawHaskType _ K1) with
295 match κ₂ as K2 return RawHaskType TV (K2 ⇛ KindStar) -> (RawHaskType TV K2) -> ??(RawHaskType _ KindStar) with
296 | KindStar => fun x' =>
297 match x' return (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
298 | TApp κ₁'' κ₂'' w'' x'' =>
299 match κ₂'' as K2'' return RawHaskType TV K2'' -> (RawHaskType TV KindStar) -> ??(RawHaskType _ KindStar) with
302 | TArrow => fun _ b => Some b
303 | _ => fun _ b => None
305 | _ => fun _ b => None
309 | _ => fun _ _ => None
311 | _ => fun _ _ => None
312 end) x (drop_arg_types y)
323 (* yeah, things are kind of messy below this point *)
326 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
328 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
329 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
330 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
331 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
332 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
333 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
334 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
336 unfold InstantiatedCoercionEnv.
337 unfold addKindToCoercionEnv.
339 rewrite <- map_preserves_length.
342 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
343 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
344 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
345 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
347 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
348 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
350 unfold addCoercionToCoercionEnv; simpl.
351 unfold InstantiatedCoercionEnv; simpl.
352 apply vec_cons; auto.
355 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
356 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ := ilist_tail ite.
357 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ) := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
358 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv := fun TV ite => (cv' TV (weakITE ite)).
359 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂ := fun TV ite => lt TV (weakITE ite).
360 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ) := map weakV lt.
361 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂ := match lt with t @@ l => weakT t @@ weakL l end.
362 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
363 : InstantiatedCoercionEnv TV CV Γ Δ.
365 unfold InstantiatedCoercionEnv; intros.
366 unfold InstantiatedCoercionEnv in ice.
367 unfold weakCE in ice.
369 rewrite <- map_preserves_length in ice.
372 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
373 unfold HaskCoercionKind in *.
375 apply hck; clear hck.
376 inversion X; subst; auto.
378 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
379 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
380 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
381 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
382 := fun TV ite tv => (f TV (weakITE ite) tv).
385 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
386 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
387 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
388 induction κ; auto. apply weakV; auto. Defined.
389 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
390 induction κ; auto. apply weakT; auto. Defined.
391 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
392 unfold HaskType in *.
393 unfold InstantiatedTypeEnv in *.
395 apply ilist_chop in X.
399 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
400 induction κ; auto. apply weakL; auto. Defined.
401 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
402 := match lt with t @@ l => weakT' t @@ weakL' l end.
403 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
404 induction κ; auto. apply weakCE; auto. Defined.
405 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
410 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
413 Definition weakITE_ {Γ:TypeEnv}{κ}{n}{TV}(ite:InstantiatedTypeEnv TV (list_ins n κ Γ)) : InstantiatedTypeEnv TV Γ.
414 rewrite list_ins_app in ite.
415 set (weakITE' ite) as ite'.
416 set (ilist_chop ite) as a.
417 rewrite <- (list_take_drop _ Γ n).
418 apply ilist_app; auto.
419 inversion ite'; auto.
422 Definition weakV_ {Γ:TypeEnv}{κ}{n}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (list_ins n κ Γ) κv.
423 unfold HaskTyVar; intros.
424 unfold HaskTyVar in cv'.
426 apply weakITE_ in env.
430 Definition weakT_ {Γ}{κ}{n}{κ₂}(lt:HaskType Γ κ₂) : HaskType (list_ins n κ Γ) κ₂.
431 unfold HaskType; intros.
436 Definition weakL_ {Γ}{κ}{n}(lev:HaskLevel Γ) : HaskLevel (list_ins n κ Γ).
437 unfold HaskLevel; intros.
438 unfold HaskLevel in lev.
443 Definition weakLT_ {Γ}{κ}{n}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (list_ins n κ Γ) κ₂ :=
444 match lt with t@@l => weakT_ t @@ weakL_ l end.
445 Definition weakCK_ {Γ}{κ}{n}(hck:HaskCoercionKind Γ) : HaskCoercionKind (list_ins n κ Γ).
446 unfold HaskCoercionKind; intros.
447 unfold HaskCoercionKind in hck.
452 Definition weakCE_ {Γ:TypeEnv}{κ}{n}(Δ:CoercionEnv Γ) : CoercionEnv (list_ins n κ Γ) := map weakCK_ Δ.
453 Definition weakF_ {Γ:TypeEnv}{n}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
454 forall TV (env:@InstantiatedTypeEnv TV (list_ins n κ Γ)), TV κ -> RawHaskType TV κ₂.
457 apply weakITE_ in env.
461 Definition weakCV_ {Γ}{Δ}{κ}{n}(cv':HaskCoVar Γ Δ) : HaskCoVar (list_ins n κ Γ) (weakCE_ Δ).
462 unfold HaskCoVar; intros.
463 unfold HaskCoVar in cv'.
465 apply weakITE_ in env.
467 unfold InstantiatedCoercionEnv.
468 unfold InstantiatedCoercionEnv in cenv.
469 replace (length (@weakCE_ _ κ n Δ)) with (length Δ) in cenv.
472 rewrite <- map_preserves_length.
476 Definition FreshHaskTyVar_ {Γ}(κ:Kind) : forall {n}, HaskTyVar (list_ins n κ Γ) κ.
480 rewrite list_ins_app in env.
481 apply weakITE' in env.
482 inversion env; subst; auto.
487 Fixpoint caseType0 {Γ}(lk:list Kind) :
488 IList _ (HaskType Γ) lk ->
489 HaskType Γ (fold_right KindArrow ★ lk) ->
491 match lk as LK return
492 IList _ (HaskType Γ) LK ->
493 HaskType Γ (fold_right KindArrow ★ LK) ->
496 | nil => fun _ ht => ht
497 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
500 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
501 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
503 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
504 Record StrongAltCon {tc:TyCon} :=
506 ; sac_altcon : WeakAltCon
507 ; sac_numExTyVars : nat
508 ; sac_numCoerVars : nat
509 ; sac_numExprVars : nat
510 ; sac_ekinds : vec Kind sac_numExTyVars
511 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
512 ; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ
513 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars
514 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars
515 ; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
517 Coercion sac_tc : StrongAltCon >-> TyCon.
518 Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
521 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
523 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
525 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
526 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
527 unfold tyConKind' in z.
528 rewrite literal_tycons_are_of_ordinary_kind in z.
533 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
536 `{EQD_VV:EqDecidable VV}{Γ}
537 (ξ:VV -> LeveledHaskType Γ ★)
539 (vt:list (VV * HaskType Γ ★))
540 : VV -> LeveledHaskType Γ ★ :=
543 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v'
546 Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
547 not (In v (map (@fst _ _) varstypes)) ->
548 (update_xi ξ lev varstypes) v = ξ v.
554 destruct (eqd_dec v0 v).
569 (***************************************************************************************************)
570 (* Well-Formedness of Types and Coercions *)
571 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
572 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
573 mkTFD : Kind -> TypeFunctionDecl tfc vk.
577 Context {TV:Kind->Type}.
580 (* local notations *)
581 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
582 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
583 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
584 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
585 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
587 (* Figure 8, lower half *)
588 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
589 @InstantiatedTypeEnv TV Γ ->
590 @InstantiatedCoercionEnv TV CV Γ Δ ->
591 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
592 | CoTVar':∀ Γ Δ t e c σ τ,
593 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
594 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
595 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
596 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
597 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
598 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
600 | SComp :∀ Γ Δ t e γ n S σ τ κ,
601 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
602 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
603 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
604 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
605 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
606 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
608 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
609 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
610 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
611 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
612 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
613 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
614 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
615 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
616 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
618 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
619 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
620 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
621 @InstantiatedTypeEnv TV Γ ->
622 InstantiatedCoercionEnv TV CV Γ Δ ->
623 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
624 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
625 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
626 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
627 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
630 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
631 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
632 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
633 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
639 (* Decidable equality on PHOAS types *)
640 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
642 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
643 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
644 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
645 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
646 | TArrow => match t2 with TArrow => true | _ => false end
647 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
648 | 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
649 | TyFunApp tfc kl k lt => match t2 with TyFunApp tfc' kl' k' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
651 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
653 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
654 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
657 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
658 match lk as LK return IList _ _ LK with
660 | h::t => n::::(count' t (S n))
663 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
664 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
668 * This is not provable in Coq's logic because the Coq function space
669 * is "too big" - although its only definable inhabitants are Coq
670 * functions, it is not provable in Coq that all function space
671 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
672 * This is actually an important feature of Coq: it lets us reason
673 * about properties of non-computable (non-recursive) functions since
674 * any property proven to hold for the entire function space will hold
675 * even for those functions. However when representing binding
676 * structure using functions we would actually prefer the smaller
677 * function-space of *definable* functions only. These two axioms
679 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
680 if compareHT Γ κ ht1 ht2
683 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
684 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
688 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
689 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
690 apply Build_EqDecidable.
692 set (compareHT_decides _ _ v1 v2) as z.
693 set (compareHT Γ κ v1 v2) as q.
694 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
699 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
700 apply Build_EqDecidable.
702 set (compareVars _ _ v1 v2) as z.
703 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
704 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
709 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
710 apply Build_EqDecidable.
712 unfold HaskLevel in *.
713 apply (eqd_dec v1 v2).
720 (* ToString instance for PHOAS types *)
721 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
723 | TVar _ v => "tv" +++ toString v
724 | TCon tc => toString tc
725 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
726 +++typeToString' false n t2+++")=>"
727 +++typeToString' needparens n t
730 | TApp _ _ TArrow t1 =>
732 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
733 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
736 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
737 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
740 | TAll k f => let alpha := "tv"+++ toString n
741 in "(forall "+++ alpha +++ ":"+++ toString k +++")"+++
742 typeToString' false (S n) (f n)
743 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
744 | TyFunApp tfc kl k lt => toString tfc+++ "_" +++ toString n+++" ["+++
745 (fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
747 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
749 | TyFunApp_nil => nil
750 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
753 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
754 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
756 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
757 { toString := typeToString }.
759 Definition TBool {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp BoolTyCon _ _ TyFunApp_nil.
760 Definition TInt {Γ} : HaskType Γ ★ := fun TV ite => TyFunApp IntTyCon _ _ TyFunApp_nil.