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 HaskCoreLiterals.
12 Require Import HaskCoreTypes. (* FIXME *)
13 Require Import HaskCoreVars. (* FIXME *)
14 Require Import HaskWeakTypes.
15 Require Import HaskWeakVars. (* FIXME *)
16 Require Import HaskCoreToWeak. (* FIXME *)
18 Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon".
19 Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars".
20 Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta".
21 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
23 (* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
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 compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool.
59 exact (if eqd_dec cdc cdc0 then true else false).
62 Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2).
64 Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
66 apply Build_EqDecidable.
68 set (trust_compare_datacons _ v1 v2) as x.
69 set (compare_datacons tc v1 v2) as y.
70 assert (y=compare_datacons tc v1 v2). reflexivity.
71 destruct y; rewrite <- H in x.
76 Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc).
78 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
81 (* TV is the PHOAS type which stands for type variables of System FC *)
82 Context {TV:Kind -> Type}.
84 (* Figure 7: ρ, σ, τ, ν *)
85 Inductive RawHaskType : Kind -> Type :=
86 | TVar : ∀ κ, TV κ -> RawHaskType κ (* a *)
87 | TCon : ∀ tc, RawHaskType (tyConKind' tc) (* T *)
88 | TArrow : RawHaskType (★ ⇛★ ⇛★ ) (* (->) *)
89 | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *)
90 | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *)
91 | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *)
92 | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *)
93 | TyFunApp : ∀ tf, RawHaskTypeList (fst (tyFunKind tf)) -> RawHaskType (snd (tyFunKind tf)) (* S_n *)
94 with RawHaskTypeList : list Kind -> Type :=
95 | TyFunApp_nil : RawHaskTypeList nil
96 | TyFunApp_cons : ∀ κ kl, RawHaskType κ -> RawHaskTypeList kl -> RawHaskTypeList (κ::kl).
98 (* the "kind" of a coercion is a pair of types *)
99 Inductive RawCoercionKind : Type :=
100 mkRawCoercionKind : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawCoercionKind.
104 (* the PHOAS type which stands for coercion variables of System FC *)
108 Inductive RawHaskCoer {CV:Type} : RawCoercionKind -> Prop := (* FIXME *).
110 | CoVar : CV -> RawHaskCoer (* g *)
111 | CoType : RawHaskType -> RawHaskCoer (* τ *)
112 | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *)
113 | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *)
114 | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *)
115 | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *)
116 | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *)
117 | CoSym : RawHaskCoer -> RawHaskCoer (* sym *)
118 | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *)
119 | CoLeft : RawHaskCoer -> RawHaskCoer (* left *)
120 | CoRight : RawHaskCoer -> RawHaskCoer (* right *).
125 Implicit Arguments TCon [ [TV] ].
126 Implicit Arguments TyFunApp [ [TV] ].
127 Implicit Arguments RawHaskType [ ].
128 Implicit Arguments RawHaskCoer [ ].
129 Implicit Arguments RawCoercionKind [ ].
130 Implicit Arguments TVar [ [TV] [κ] ].
131 Implicit Arguments TCoerc [ [TV] [κ] ].
132 Implicit Arguments TApp [ [TV] [κ₁] [κ₂] ].
133 Implicit Arguments TAll [ [TV] ].
135 Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))).
136 Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)).
138 (* Kind and Coercion Environments *)
140 * In System FC, the environment consists of three components, each of
141 * whose well-formedness depends on all of those prior to it:
143 * 1. (TypeEnv) The list of free type variables and their kinds
144 * 2. (CoercionEnv) The list of free coercion variables and the pair of types between which it witnesses coercibility
145 * 3. (Tree ??CoreVar) The list of free value variables and the type of each one
148 Definition TypeEnv := list Kind.
149 Definition InstantiatedTypeEnv (TV:Kind->Type) (Γ:TypeEnv) := IList _ TV Γ.
150 Definition HaskCoercionKind (Γ:TypeEnv) := ∀ TV, InstantiatedTypeEnv TV Γ -> @RawCoercionKind TV.
151 Definition CoercionEnv (Γ:TypeEnv) := list (HaskCoercionKind Γ).
152 Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:CoercionEnv Γ):= vec CV (length Δ).
154 (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *)
155 Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ.
156 Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV.
157 Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★).
158 Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ.
159 Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite).
161 Inductive HaskTypeOfSomeKind (Γ:TypeEnv) :=
162 haskTypeOfSomeKind : ∀ κ, HaskType Γ κ -> HaskTypeOfSomeKind Γ.
163 Implicit Arguments haskTypeOfSomeKind [ [Γ] [κ] ].
164 Definition kindOfHaskTypeOfSomeKind {Γ}(htosk:HaskTypeOfSomeKind Γ) :=
166 haskTypeOfSomeKind κ _ => κ
168 Coercion kindOfHaskTypeOfSomeKind : HaskTypeOfSomeKind >-> Kind.
169 Definition haskTypeOfSomeKindToHaskType {Γ}(htosk:HaskTypeOfSomeKind Γ) : HaskType Γ htosk :=
170 match htosk as H return HaskType Γ H with
171 haskTypeOfSomeKind _ ht => ht
173 Coercion haskTypeOfSomeKindToHaskType : HaskTypeOfSomeKind >-> HaskType.
175 Definition HaskCoercion Γ Δ (hk:HaskCoercionKind Γ) := forall TV CV (ite:@InstantiatedTypeEnv TV Γ),
176 @InstantiatedCoercionEnv TV CV Γ Δ -> @RawHaskCoer TV CV (hk TV ite).
177 Inductive LeveledHaskType (Γ:TypeEnv) κ := mkLeveledHaskType : HaskType Γ κ -> HaskLevel Γ -> LeveledHaskType Γ κ.
178 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
179 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
180 := fun TV env => TAll κ (σ TV env).
181 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
182 (cv:HaskTyVar Γ κ) : HaskType Γ ★
183 := fun TV env => σ TV env (cv TV env).
184 Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
185 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
186 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc))
187 := fun TV ite => TCon tc.
188 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
189 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
190 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
191 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
193 (* PHOAS substitution on types *)
194 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
197 (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
200 | TAll _ y => TAll _ (fun v => flattenT _ (y (TVar v)))
201 | TApp _ _ x y => TApp (flattenT _ x) (flattenT _ y)
203 | TCoerc _ t1 t2 t => TCoerc (flattenT _ t1) (flattenT _ t2) (flattenT _ t)
205 | TCode v e => TCode (flattenT _ v) (flattenT _ e)
206 | TyFunApp tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
208 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
209 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
210 | TyFunApp_nil => TyFunApp_nil
211 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest)
213 for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
215 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
216 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
217 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
225 (* yeah, things are kind of messy below this point *)
228 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
230 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
231 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
232 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
233 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
234 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
235 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
236 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
238 unfold InstantiatedCoercionEnv.
239 unfold addKindToCoercionEnv.
241 rewrite <- map_preserves_length.
244 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
245 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
246 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
247 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
249 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
250 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
252 unfold addCoercionToCoercionEnv; simpl.
253 unfold InstantiatedCoercionEnv; simpl.
254 apply vec_cons; auto.
256 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
257 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
259 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
260 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
261 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
262 := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
263 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
264 := fun TV ite => (cv' TV (weakITE ite)).
265 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
266 induction κ; auto. apply weakV; auto. Defined.
267 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
268 := fun TV ite => lt TV (weakITE ite).
269 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
271 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
272 induction κ; auto. apply weakT; auto. Defined.
273 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
274 unfold HaskType in *.
275 unfold InstantiatedTypeEnv in *.
277 apply ilist_chop in X.
281 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
282 rewrite <- ass_app in lt.
285 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
286 induction κ; auto. apply weakL; auto. Defined.
287 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
288 := match lt with t @@ l => weakT t @@ weakL l end.
289 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
290 := match lt with t @@ l => weakT' t @@ weakL' l end.
291 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
292 induction κ; auto. apply weakCE; auto. Defined.
293 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
294 : InstantiatedCoercionEnv TV CV Γ Δ.
296 unfold InstantiatedCoercionEnv; intros.
297 unfold InstantiatedCoercionEnv in ice.
298 unfold weakCE in ice.
300 rewrite <- map_preserves_length in ice.
303 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
304 unfold HaskCoercionKind in *.
306 apply hck; clear hck.
307 inversion X; subst; auto.
309 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
314 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
315 match κ as K return list (HaskCoercionKind (app K Γ)) with
317 | _ => map weakCK' hck
319 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
320 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
321 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
322 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
323 := fun TV ite tv => (f TV (weakITE ite) tv).
325 (* I keep mixing up left/right folds *)
326 (* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
327 (*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
329 Fixpoint caseType0 {Γ}(lk:list Kind) :
330 IList _ (HaskType Γ) lk ->
331 HaskType Γ (fold_right KindTypeFunction ★ lk) ->
333 match lk as LK return
334 IList _ (HaskType Γ) LK ->
335 HaskType Γ (fold_right KindTypeFunction ★ LK) ->
338 | nil => fun _ ht => ht
339 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
342 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
343 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
345 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
346 Record StrongAltCon {tc:TyCon} :=
348 ; sac_altcon : AltCon
349 ; sac_numExTyVars : nat
350 ; sac_numCoerVars : nat
351 ; sac_numExprVars : nat
352 ; sac_ekinds : vec Kind sac_numExTyVars
353 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
354 ; sac_Γ := fun Γ => app (tyConKind tc) Γ
355 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
356 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
357 ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
359 Coercion sac_tc : StrongAltCon >-> TyCon.
360 Coercion sac_altcon : StrongAltCon >-> AltCon.
363 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
365 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
367 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
368 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
369 unfold tyConKind' in z.
370 rewrite literal_tycons_are_of_ordinary_kind in z.
375 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
378 `{EQD_VV:EqDecidable VV}{Γ}
379 (ξ:VV -> LeveledHaskType Γ ★)
380 (vt:list (VV * LeveledHaskType Γ ★))
381 : VV -> LeveledHaskType Γ ★ :=
384 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
389 (***************************************************************************************************)
390 (* Well-Formedness of Types and Coercions *)
391 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
392 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
393 mkTFD : Kind -> TypeFunctionDecl tfc vk.
397 Context {TV:Kind->Type}.
400 (* local notations *)
401 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
402 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
403 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
404 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
405 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
407 (* Figure 8, lower half *)
408 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
409 @InstantiatedTypeEnv TV Γ ->
410 @InstantiatedCoercionEnv TV CV Γ Δ ->
411 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
412 | CoTVar':∀ Γ Δ t e c σ τ,
413 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
414 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
415 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
416 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
417 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
418 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
420 | SComp :∀ Γ Δ t e γ n S σ τ κ,
421 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
422 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
423 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
424 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
425 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
426 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
428 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
429 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
430 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
431 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
432 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
433 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
434 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
435 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
436 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
438 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
439 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
440 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
441 @InstantiatedTypeEnv TV Γ ->
442 InstantiatedCoercionEnv TV CV Γ Δ ->
443 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
444 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
445 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
446 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
447 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
450 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
451 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
452 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
453 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
459 (* Decidable equality on PHOAS types *)
460 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
462 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
463 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
464 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
465 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
466 | TArrow => match t2 with TArrow => true | _ => false end
467 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
468 | 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
469 | TyFunApp tfc lt => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
471 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
473 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
474 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
477 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
478 match lk as LK return IList _ _ LK with
480 | h::t => n::::(count' t (S n))
483 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
484 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
486 (* This is not provable in Coq's logic because the Coq function space
487 * is "too big" - although its only definable inhabitants are Coq
488 * functions, it is not provable in Coq that all function space
489 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
490 * This is actually an important feature of Coq: it lets us reason
491 * about properties of non-computable (non-recursive) functions since
492 * any property proven to hold for the entire function space will hold
493 * even for those functions. However when representing binding
494 * structure using functions we would actually prefer the smaller
495 * function-space of *definable* functions only. These two axioms
497 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
498 if compareHT Γ κ ht1 ht2
501 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
502 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
506 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
507 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
508 apply Build_EqDecidable.
510 set (compareHT_decides _ _ v1 v2) as z.
511 set (compareHT Γ κ v1 v2) as q.
512 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
517 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
518 apply Build_EqDecidable.
520 set (compareVars _ _ v1 v2) as z.
521 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
522 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
527 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
528 apply Build_EqDecidable.
530 unfold HaskLevel in *.
531 apply (eqd_dec v1 v2).
538 (* ToString instance for PHOAS types *)
539 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
541 | TVar _ v => "tv" +++ v
542 | TCon tc => toString tc
543 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
544 +++typeToString' false n t2+++")=>"
545 +++typeToString' needparens n t
548 | TApp _ _ TArrow t1 =>
550 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
551 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
554 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
555 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
558 | TAll k f => let alpha := "tv"+++n
559 in "(forall "+++ alpha +++ "{:}"+++ k +++")"+++
560 typeToString' false (S n) (f n)
561 | TCode ec t => "<["+++(typeToString' true n ec)+++"]>@"+++(typeToString' false n t)
562 | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
564 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
566 | TyFunApp_nil => nil
567 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
570 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
571 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
573 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
574 { toString := typeToString }.