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