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.
13 Require Import HaskCoreVars.
14 Require Import HaskWeakTypes.
15 Require Import HaskWeakVars.
16 Require Import HaskCoreToWeak.
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 Γ κ.
179 Definition FreshHaskTyVar {Γ}(κ:Kind) : HaskTyVar (κ::Γ) κ := fun TV env => ilist_head env.
180 Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★) : HaskType Γ ★
181 := fun TV env => TAll κ (σ TV env).
182 Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV ★)
183 (cv:HaskTyVar Γ κ) : HaskType Γ ★
184 := fun TV env => σ TV env (cv TV env).
185 Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
186 fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
187 Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc))
188 := fun TV ite => TCon tc.
189 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
190 fun TV ite => TApp (t1 TV ite) (t2 TV ite).
191 Definition mkHaskCoercionKind {Γ}{κ}(t1:HaskType Γ κ)(t2:HaskType Γ κ) : HaskCoercionKind Γ :=
192 fun TV ite => mkRawCoercionKind _ (t1 TV ite) (t2 TV ite).
194 (* PHOAS substitution on types *)
195 Definition substT {Γ}{κ₁}{κ₂}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ₁ -> RawHaskType TV κ₂)(v:@HaskType Γ κ₁)
198 (fix flattenT {κ} (exp: RawHaskType (fun k => RawHaskType TV k) κ) : RawHaskType TV κ :=
201 | TAll _ y => TAll _ (fun v => flattenT _ (y (TVar v)))
202 | TApp _ _ x y => TApp (flattenT _ x) (flattenT _ y)
204 | TCoerc _ t1 t2 t => TCoerc (flattenT _ t1) (flattenT _ t2) (flattenT _ t)
206 | TCode v e => TCode (flattenT _ v) (flattenT _ e)
207 | TyFunApp tfc lt => TyFunApp tfc (flattenTyFunApp _ lt)
209 with flattenTyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun k => RawHaskType TV k) lk) : @RawHaskTypeList TV lk :=
210 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
211 | TyFunApp_nil => TyFunApp_nil
212 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (flattenT _ t) (flattenTyFunApp _ rest)
214 for flattenT) _ (exp (fun k => RawHaskType TV k) (ilmap (fun κ tv => TVar tv) env) (v TV env)).
216 Notation "t @@ l" := (@mkLeveledHaskType _ _ t l) (at level 20).
217 Notation "t @@@ l" := (mapOptionTree (fun t' => t' @@ l) t) (at level 20).
218 Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t).
220 Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) :=
221 match lht with t@@l => t end.
228 (* yeah, things are kind of messy below this point *)
231 Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Kind->Type}(ite:InstantiatedTypeEnv TV (κ::Γ))
233 Definition addKindToCoercionEnv (Γ:TypeEnv)(Δ:CoercionEnv Γ)(κ:Kind) : CoercionEnv (κ::Γ) :=
234 map (fun f => (fun TV ite => f TV (unAddKindFromInstantiatedTypeEnv ite))) Δ.
235 Definition addKindToInstantiatedTypeEnv {Γ:TypeEnv}{TV:Kind->Type}(env:InstantiatedTypeEnv TV Γ)(κ:Kind)(tv:TV κ)
236 : InstantiatedTypeEnv TV (κ::Γ) := tv::::env.
237 Definition addKindToInstantiatedCoercionEnv {Γ:TypeEnv}{Δ}{TV:Kind->Type}{CV:Type}
238 (env:InstantiatedCoercionEnv TV CV Γ Δ)(κ:Kind)(tv:TV κ)
239 : InstantiatedCoercionEnv TV CV (κ::Γ) (addKindToCoercionEnv Γ Δ κ).
241 unfold InstantiatedCoercionEnv.
242 unfold addKindToCoercionEnv.
244 rewrite <- map_preserves_length.
247 Definition coercionEnvContainsCoercion {Γ}{Δ}{TV:Kind->Type}{CV:Type}(ite:InstantiatedTypeEnv TV Γ)
248 (ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)(ck:RawCoercionKind TV)
249 := @vec_In _ _ (cv,ck) (vec_zip ice (vec_map (fun f => f TV ite) (list2vec Δ))).
250 Definition addCoercionToCoercionEnv {Γ}(Δ:CoercionEnv Γ)(κ:HaskCoercionKind Γ) : CoercionEnv Γ :=
252 Definition addCoercionToInstantiatedCoercionEnv {Γ}{Δ}{κ}{TV CV}(ice:InstantiatedCoercionEnv TV CV Γ Δ)(cv:CV)
253 : InstantiatedCoercionEnv TV CV Γ (addCoercionToCoercionEnv Δ κ).
255 unfold addCoercionToCoercionEnv; simpl.
256 unfold InstantiatedCoercionEnv; simpl.
257 apply vec_cons; auto.
259 (* the various "weak" functions turn a HaskXX-in-Γ into a HaskXX-in-(κ::Γ) *)
260 Definition weakITE {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (κ::Γ)) : InstantiatedTypeEnv TV Γ
262 Definition weakITE' {Γ:TypeEnv}{κ}{TV}(ite:InstantiatedTypeEnv TV (app κ Γ)) : InstantiatedTypeEnv TV Γ.
263 induction κ; auto. apply IHκ. inversion ite; subst. apply X0. Defined.
264 Definition weakCE {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (κ::Γ)
265 := map (fun x => (fun tv ite => x tv (weakITE ite))) Δ.
266 Definition weakV {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (κ::Γ) κv
267 := fun TV ite => (cv' TV (weakITE ite)).
268 Definition weakV' {Γ:TypeEnv}{κ}{κv}(cv':HaskTyVar Γ κv) : HaskTyVar (app κ Γ) κv.
269 induction κ; auto. apply weakV; auto. Defined.
270 Definition weakT {Γ:TypeEnv}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (κ::Γ) κ₂
271 := fun TV ite => lt TV (weakITE ite).
272 Definition weakL {Γ}{κ}(lt:HaskLevel Γ) : HaskLevel (κ::Γ)
274 Definition weakT' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app κ Γ) κ₂.
275 induction κ; auto. apply weakT; auto. Defined.
276 Definition weakT'' {Γ}{κ}{κ₂}(lt:HaskType Γ κ₂) : HaskType (app Γ κ) κ₂.
277 unfold HaskType in *.
278 unfold InstantiatedTypeEnv in *.
280 apply ilist_chop in X.
284 Definition lamer {a}{b}{c}{κ}(lt:HaskType (app (app a b) c) κ) : HaskType (app a (app b c)) κ.
285 rewrite <- ass_app in lt.
288 Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ).
289 induction κ; auto. apply weakL; auto. Defined.
290 Definition weakLT {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (κ::Γ) κ₂
291 := match lt with t @@ l => weakT t @@ weakL l end.
292 Definition weakLT' {Γ}{κ}{κ₂}(lt:LeveledHaskType Γ κ₂) : LeveledHaskType (app κ Γ) κ₂
293 := match lt with t @@ l => weakT' t @@ weakL' l end.
294 Definition weakCE' {Γ:TypeEnv}{κ}(Δ:CoercionEnv Γ) : CoercionEnv (app κ Γ).
295 induction κ; auto. apply weakCE; auto. Defined.
296 Definition weakICE {Γ:TypeEnv}{κ}{Δ:CoercionEnv Γ}{TV}{CV}(ice:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ))
297 : InstantiatedCoercionEnv TV CV Γ Δ.
299 unfold InstantiatedCoercionEnv; intros.
300 unfold InstantiatedCoercionEnv in ice.
301 unfold weakCE in ice.
303 rewrite <- map_preserves_length in ice.
306 Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ).
307 unfold HaskCoercionKind in *.
309 apply hck; clear hck.
310 inversion X; subst; auto.
312 Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ).
318 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
319 match κ as K return list (HaskCoercionKind (app K Γ)) with
321 | _ => map weakCK' hck
324 Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) :=
326 Definition weakCV {Γ}{Δ}{κ}(cv':HaskCoVar Γ Δ) : HaskCoVar (κ::Γ) (weakCE Δ) :=
327 fun TV CV ite ice => (cv' TV CV (weakITE ite) (weakICE ice)).
328 Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ -> RawHaskType TV κ₂) :
329 forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV κ -> RawHaskType TV κ₂
330 := fun TV ite tv => (f TV (weakITE ite) tv).
332 (* I keep mixing up left/right folds *)
333 (* Eval compute in (fold_right (fun x y => "("+++x+++y+++")") "x" ("a"::"b"::"c"::nil)). *)
334 (*Eval compute in (fold_left (fun x y => "("+++x+++y+++")") ("a"::"b"::"c"::nil) "x").*)
336 Fixpoint caseType0 {Γ}(lk:list Kind) :
337 IList _ (HaskType Γ) lk ->
338 HaskType Γ (fold_right KindTypeFunction ★ lk) ->
340 match lk as LK return
341 IList _ (HaskType Γ) LK ->
342 HaskType Γ (fold_right KindTypeFunction ★ LK) ->
345 | nil => fun _ ht => ht
346 | k::lk' => fun tlist ht => caseType0 lk' (ilist_tail tlist) (fun TV env => TApp (ht TV env) (ilist_head tlist TV env))
349 Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc)) : HaskType Γ ★ :=
350 caseType0 (tyConKind tc) atypes (fun TV env => TCon tc).
352 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
353 Record StrongAltCon {tc:TyCon} :=
355 ; sac_altcon : AltCon
356 ; sac_numExTyVars : nat
357 ; sac_numCoerVars : nat
358 ; sac_numExprVars : nat
359 ; sac_ekinds : vec Kind sac_numExTyVars
360 ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds)
361 ; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ
362 ; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars
363 ; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars
364 ; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
366 Coercion sac_tc : StrongAltCon >-> TyCon.
367 Coercion sac_altcon : StrongAltCon >-> AltCon.
370 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
372 Axiom literal_tycons_are_of_ordinary_kind : forall lit, tyConKind (haskLiteralToTyCon lit) = nil.
374 Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★.
375 set (fun TV (ite:InstantiatedTypeEnv TV Γ) => @TCon TV (haskLiteralToTyCon lit)) as z.
376 unfold tyConKind' in z.
377 rewrite literal_tycons_are_of_ordinary_kind in z.
382 Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
385 `{EQD_VV:EqDecidable VV}{Γ}
386 (ξ:VV -> LeveledHaskType Γ ★)
387 (vt:list (VV * LeveledHaskType Γ ★))
388 : VV -> LeveledHaskType Γ ★ :=
391 | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
396 (***************************************************************************************************)
397 (* Well-Formedness of Types and Coercions *)
398 (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *)
399 Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type :=
400 mkTFD : Kind -> TypeFunctionDecl tfc vk.
404 Context {TV:Kind->Type}.
407 (* local notations *)
408 Notation "ienv '⊢ᴛy' σ : κ" := (@WellKinded_RawHaskType TV _ ienv σ κ).
409 Notation "env ∋ cv : t1 ∼ t2 : Γ : t" := (@coercionEnvContainsCoercion Γ _ TV CV t env cv (@mkRawCoercionKind _ t1 t2))
410 (at level 20, t1 at level 99, t2 at level 99, t at level 99).
411 Reserved Notation "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite"
412 (at level 20, γ at level 99, b at level 99, Δ at level 99, ite at level 99, Γ at level 99).
414 (* Figure 8, lower half *)
415 Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ),
416 @InstantiatedTypeEnv TV Γ ->
417 @InstantiatedCoercionEnv TV CV Γ Δ ->
418 @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=
419 | CoTVar':∀ Γ Δ t e c σ τ,
420 (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t
421 | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t
422 | Sym :∀ Γ Δ t e γ σ τ, (e⊢ᴄᴏ γ : σ ∼ τ : Δ : Γ:t) -> e⊢ᴄᴏ CoSym γ : τ ∼ σ : Δ :Γ: t
423 | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t
424 | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t
425 | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t
427 | SComp :∀ Γ Δ t e γ n S σ τ κ,
428 ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TyFunApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TyFunApp S σ∼TyFunApp S τ : Δ : Γ : t
429 | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV),
430 ListWFCo Γ Δ t e γ (map TVar (vec2list σ₁)) (map TVar (vec2list σ₂)) ->
431 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) ->
432 ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) ->
433 e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t
435 | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ ,
436 (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ))
437 -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t
438 | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ,
439 (t ⊢ᴛy TApp σ₁ σ₂:κ)->
440 (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)->
441 (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) ->
442 e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t
443 | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV),
445 (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) ->
446 e⊢ᴄᴏ CoAppT γ (v TV t) : substT σ v TV t ∼substT τ v TV t : Δ : Γ : t
447 with ListWFCo : forall Γ (Δ:CoercionEnv Γ),
448 @InstantiatedTypeEnv TV Γ ->
449 InstantiatedCoercionEnv TV CV Γ Δ ->
450 list (RawHaskCoer TV CV) -> list (RawHaskType TV) -> list (RawHaskType TV) -> Prop :=
451 | LWFCo_nil : ∀ Γ Δ t e , ListWFCo Γ Δ t e nil nil nil
452 | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )->
453 ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc)
454 where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)).
457 Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) :=
458 forall {TV CV:Type}(env:@InstantiatedTypeEnv TV Γ)(cenv:InstantiatedCoercionEnv TV CV Γ Δ),
459 @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)).
460 Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b).
466 (* Decidable equality on PHOAS types *)
467 Fixpoint compareT (n:nat){κ₁}(t1:@RawHaskType (fun _ => nat) κ₁){κ₂}(t2:@RawHaskType (fun _ => nat) κ₂) : bool :=
469 | TVar _ x => match t2 with TVar _ x' => if eqd_dec x x' then true else false | _ => false end
470 | TAll _ y => match t2 with TAll _ y' => compareT (S n) (y n) (y' n) | _ => false end
471 | TApp _ _ x y => match t2 with TApp _ _ x' y' => if compareT n x x' then compareT n y y' else false | _ => false end
472 | TCon tc => match t2 with TCon tc' => if eqd_dec tc tc' then true else false | _ => false end
473 | TArrow => match t2 with TArrow => true | _ => false end
474 | TCode ec t => match t2 with TCode ec' t' => if compareT n ec ec' then compareT n t t' else false | _ => false end
475 | 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
476 | TyFunApp tfc lt => match t2 with TyFunApp tfc' lt' => eqd_dec tfc tfc' && compareTL n lt lt' | _ => false end
478 with compareTL (n:nat){κ₁}(t1:@RawHaskTypeList (fun _ => nat) κ₁){κ₂}(t2:@RawHaskTypeList (fun _ => nat) κ₂) : bool :=
480 | TyFunApp_nil => match t2 with TyFunApp_nil => true | _ => false end
481 | TyFunApp_cons κ kl t r => match t2 with | TyFunApp_cons κ' kl' t' r' => compareT n t t' && compareTL n r r' | _ => false end
484 Fixpoint count' (lk:list Kind)(n:nat) : IList _ (fun _ => nat) lk :=
485 match lk as LK return IList _ _ LK with
487 | h::t => n::::(count' t (S n))
490 Definition compareHT Γ κ (ht1 ht2:HaskType Γ κ) :=
491 compareT (length Γ) (ht1 (fun _ => nat) (count' Γ O)) (ht2 (fun _ => nat) (count' Γ O)).
493 (* This is not provable in Coq's logic because the Coq function space
494 * is "too big" - although its only definable inhabitants are Coq
495 * functions, it is not provable in Coq that all function space
496 * inhabitants are definable (i.e. there are no "exotic" inhabitants).
497 * This is actually an important feature of Coq: it lets us reason
498 * about properties of non-computable (non-recursive) functions since
499 * any property proven to hold for the entire function space will hold
500 * even for those functions. However when representing binding
501 * structure using functions we would actually prefer the smaller
502 * function-space of *definable* functions only. These two axioms
504 Axiom compareHT_decides : forall Γ κ (ht1 ht2:HaskType Γ κ),
505 if compareHT Γ κ ht1 ht2
508 Axiom compareVars : forall Γ κ (htv1 htv2:HaskTyVar Γ κ),
509 if compareHT _ _ (haskTyVarToType htv1) (haskTyVarToType htv2)
513 (* using the axioms, we can now create an EqDecidable instance for HaskType, HaskTyVar, and HaskLevel *)
514 Instance haskTypeEqDecidable Γ κ : EqDecidable (HaskType Γ κ).
515 apply Build_EqDecidable.
517 set (compareHT_decides _ _ v1 v2) as z.
518 set (compareHT Γ κ v1 v2) as q.
519 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
524 Instance haskTyVarEqDecidable Γ κ : EqDecidable (HaskTyVar Γ κ).
525 apply Build_EqDecidable.
527 set (compareVars _ _ v1 v2) as z.
528 set (compareHT Γ κ (haskTyVarToType v1) (haskTyVarToType v2)) as q.
529 destruct q as [ ] _eqn; unfold q in *; rewrite Heqb in *.
534 Instance haskLevelEqDecidable Γ : EqDecidable (HaskLevel Γ).
535 apply Build_EqDecidable.
537 unfold HaskLevel in *.
538 apply (eqd_dec v1 v2).
545 (* ToString instance for PHOAS types *)
546 Fixpoint typeToString' (needparens:bool)(n:nat){κ}(t:RawHaskType (fun _ => nat) κ) {struct t} : string :=
548 | TVar _ v => "tv" +++ v
549 | TCon tc => toString tc
550 | TCoerc _ t1 t2 t => "("+++typeToString' false n t1+++"~"
551 +++typeToString' false n t2+++")=>"
552 +++typeToString' needparens n t
555 | TApp _ _ TArrow t1 =>
557 then "("+++(typeToString' true n t1)+++"->"+++(typeToString' true n t2)+++")"
558 else (typeToString' true n t1)+++"->"+++(typeToString' true n t2)
561 then "("+++(typeToString' true n t1)+++" "+++(typeToString' false n t2)+++")"
562 else (typeToString' true n t1)+++" "+++(typeToString' false n t2)
565 | TAll k f => let alpha := "tv"+++n
566 in "(forall "+++ alpha +++ ":"+++ k +++")"+++
567 typeToString' false (S n) (f n)
568 | TCode ec t => "<["+++(typeToString' true n t)+++"]>@"+++(typeToString' false n ec)
569 | TyFunApp tfc lt => tfc+++"_"+++n+++" ["+++(fold_left (fun x y => " \ "+++x+++y) (typeList2string false n lt) "")+++"]"
571 with typeList2string (needparens:bool)(n:nat){κ}(t:RawHaskTypeList κ) {struct t} : list string :=
573 | TyFunApp_nil => nil
574 | TyFunApp_cons κ kl rhk rhkl => (typeToString' needparens n rhk)::(typeList2string needparens n rhkl)
577 Definition typeToString {Γ}{κ}(ht:HaskType Γ κ) : string :=
578 typeToString' false (length Γ) (ht (fun _ => nat) (count' Γ O)).
580 Instance TypeToStringInstance {Γ} {κ} : ToString (HaskType Γ κ) :=
581 { toString := typeToString }.