X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongTypes.v;h=916afe14ac601e8fd68f551e432ef95ef61e9590;hp=614a09c190760551550d432a69fa8ee0196d8f21;hb=bcb16a7fa1ff772f12807c4587609fd756b7762e;hpb=8282f5a7639dbe862bba29d3170d58b81bbb1446 diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 614a09c..916afe1 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -4,11 +4,82 @@ Generalizable All Variables. Require Import Preamble. -Require Import General. Require Import Coq.Strings.String. Require Import Coq.Lists.List. -Require Import HaskGeneral. -Require Import HaskLiterals. +Require Import General. +Require Import HaskKinds. +Require Import HaskCoreLiterals. +Require Import HaskCoreTypes. (* FIXME *) +Require Import HaskCoreVars. (* FIXME *) +Require Import HaskWeakTypes. +Require Import HaskWeakVars. (* FIXME *) +Require Import HaskCoreToWeak. (* FIXME *) + +Variable CoFunConst : nat -> Type. (* FIXME *) +Variable TyFunConst : nat -> Type. (* FIXME *) + +Variable dataConTyCon : CoreDataCon -> TyCon. Extract Inlined Constant dataConTyCon => "DataCon.dataConTyCon". + +Variable dataConExVars_ : CoreDataCon -> list CoreVar. Extract Inlined Constant dataConExVars_ => "DataCon.dataConExTyVars". +Variable dataConEqTheta_ : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_ => "DataCon.dataConEqTheta". +Variable dataConOrigArgTys_:CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_ =>"DataCon.dataConOrigArgTys". +Variable getTyConTyVars_ : TyCon -> list CoreVar. Extract Inlined Constant getTyConTyVars_ => "TyCon.tyConTyVars". + +(* FIXME: might be a better idea to panic here than simply drop things that look wrong *) +Definition tyConTyVars (tc:TyCon) := + filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (getTyConTyVars_ tc)). + Opaque tyConTyVars. +Definition dataConExTyVars cdc := + filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)). + Opaque dataConExTyVars. +Definition dataConCoerKinds cdc := + filter (map (fun x => match x with EqPred t1 t2 => + match ( + coreTypeToWeakType t1 >>= fun t1' => + coreTypeToWeakType t2 >>= fun t2' => + OK (t1',t2')) + with OK z => Some z + | _ => None + end + | _ => None + end) (dataConEqTheta_ cdc)). + Opaque dataConCoerKinds. +Definition dataConFieldTypes cdc := + filter (map (fun x => match coreTypeToWeakType x with + | OK z => Some z + | _ => None + end) (dataConOrigArgTys_ cdc)). + +Definition tyConNumKinds (tc:TyCon) := length (tyConTyVars tc). + Coercion tyConNumKinds : TyCon >-> nat. + +Inductive DataCon : TyCon -> Type := + mkDataCon : forall cdc:CoreDataCon, DataCon (dataConTyCon cdc). + Definition dataConToCoreDataCon `(dc:DataCon tc) : CoreDataCon := match dc with mkDataCon cdc => cdc end. + Coercion mkDataCon : CoreDataCon >-> DataCon. + Coercion dataConToCoreDataCon : DataCon >-> CoreDataCon. + (*Opaque DataCon.*) + +Definition compare_datacons : forall tc, forall dc1 dc2:DataCon tc, bool. + intros. + destruct dc1. + destruct dc2. + exact (if eqd_dec cdc cdc0 then true else false). + Defined. + +Axiom trust_compare_datacons : forall tc dc1 dc2, if compare_datacons tc dc1 dc2 then dc1=dc2 else not (dc1=dc2). + +Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc). + intros. + apply Build_EqDecidable. + intros. + set (trust_compare_datacons _ v1 v2) as x. + set (compare_datacons tc v1 v2) as y. + assert (y=compare_datacons tc v1 v2). reflexivity. + destruct y; rewrite <- H in x. + left; auto. + right; auto. + Defined. (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *) Section Raw. @@ -19,13 +90,14 @@ Section Raw. (* Figure 7: ρ, σ, τ, ν *) Inductive RawHaskType : Type := | TVar : TV -> RawHaskType (* a *) - | TCon : ∀n, TyCon n -> RawHaskType (* T *) - | TCoerc : Kind -> RawHaskType (* (+>) *) + | TCon : TyCon -> RawHaskType (* T *) + | TArrow : RawHaskType (* (->) *) + | TCoerc : RawHaskType -> RawHaskType -> RawHaskType -> RawHaskType (* (+>) *) | TApp : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) - | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) + | TFCApp : forall tc:TyCon, vec RawHaskType tc -> RawHaskType (* S_n *) | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). - + (* the "kind" of a coercion is a pair of types *) Inductive RawCoercionKind : Type := mkRawCoercionKind : RawHaskType -> RawHaskType -> RawCoercionKind. @@ -40,8 +112,8 @@ Section Raw. | CoType : RawHaskType -> RawHaskCoer (* τ *) | CoApp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* γ γ *) | CoAppT : RawHaskCoer -> RawHaskType -> RawHaskCoer (* γ@v *) - | CoCFApp : ∀n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) - | CoTFApp : ∀n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) + | CoCFApp : ∀ n, CoFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* C γⁿ *) + | CoTFApp : ∀ n, TyFunConst n -> vec RawHaskCoer n -> RawHaskCoer (* S_n γⁿ *) | CoAll : Kind -> (TV -> RawHaskCoer) -> RawHaskCoer (* ∀a:κ.γ *) | CoSym : RawHaskCoer -> RawHaskCoer (* sym *) | CoComp : RawHaskCoer -> RawHaskCoer -> RawHaskCoer (* ◯ *) @@ -51,15 +123,14 @@ Section Raw. End CV. End Raw. -Implicit Arguments TCon [ [TV] [n]]. -Implicit Arguments TFCApp [ [TV] [n]]. +Implicit Arguments TCon [ [TV] ]. +Implicit Arguments TFCApp [ [TV] ]. Implicit Arguments RawHaskType [ ]. Implicit Arguments RawHaskCoer [ ]. Implicit Arguments RawCoercionKind [ ]. -Notation "t1 ---> t2" := (fun TV env => (@TApp _ (@TApp _ (@TCon TV _ ArrowTyCon) (t1 TV env)) (t2 TV env))). -Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃" := - (fun TV env => @TApp _ (@TApp _ (@TCon _ _ ArrowTyCon) (@TApp _ (@TApp _ (@TCoerc _ κ) (φ₁ TV env)) (φ₂ TV env))) (φ₃ TV env)). +Notation "t1 ---> t2" := (fun TV env => (TApp (TApp TArrow (t1 TV env)) (t2 TV env))). +Notation "φ₁ ∼∼ φ₂ ⇒ φ₃" := (fun TV env => TCoerc (φ₁ TV env) (φ₂ TV env) (φ₃ TV env)). @@ -94,10 +165,13 @@ Definition HaskTAll {Γ}(κ:Kind)(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), Definition HaskTApp {Γ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> RawHaskType TV)(cv:HaskTyVar Γ) : HaskType Γ := fun TV env => σ TV env (cv TV env). Definition HaskBrak {Γ}(v:HaskTyVar Γ)(t:HaskType Γ) : HaskType Γ := fun TV env => @TCode TV (TVar (v TV env)) (t TV env). -Definition HaskTCon {Γ}{n}(tc:TyCon n) : HaskType Γ := fun TV ite => TCon tc. +Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ := fun TV ite => TCon tc. Definition HaskAppT {Γ}(t1 t2:HaskType Γ) : HaskType Γ := fun TV ite => TApp (t1 TV ite) (t2 TV ite). Definition mkHaskCoercionKind {Γ}(t1 t2:HaskType Γ) : HaskCoercionKind Γ := fun TV ite => mkRawCoercionKind (t1 TV ite) (t2 TV ite). +Definition unMkHaskCoercionKind {Γ}(hck:HaskCoercionKind Γ) : (HaskType Γ * HaskType Γ) := + ((fun TV ite => match (hck TV ite) with mkRawCoercionKind t1 _ => t1 end), + (fun TV ite => match (hck TV ite) with mkRawCoercionKind _ t2 => t2 end)). (* PHOAS substitution on types *) @@ -108,15 +182,16 @@ Definition substT {Γ}(exp:forall TV (env:@InstantiatedTypeEnv TV Γ), TV -> Raw | TVar x => x | TAll k y => TAll k (fun v => flattenT (y (TVar v))) | TApp x y => TApp (flattenT x) (flattenT y) - | TCon n tc => TCon tc - | TCoerc k => TCoerc k + | TCon tc => TCon tc + | TCoerc t1 t2 t => TCoerc (flattenT t1) (flattenT t2) (flattenT t) + | TArrow => TArrow | TCode v e => TCode (flattenT v) (flattenT e) - | TFCApp n tfc lt => TFCApp tfc + | TFCApp tfc lt => TFCApp tfc ((fix flatten_vec n (expv:vec (RawHaskType (RawHaskType TV)) n) : vec (RawHaskType TV) n := match expv in vec _ N return vec (RawHaskType TV) N with | vec_nil => vec_nil | x:::y => (flattenT x):::(flatten_vec _ y) - end) n lt) + end) _ lt) end) (exp (RawHaskType TV) (vec_map (fun tv => TVar tv) env) (v TV env)). Notation "t @@ l" := (@mkLeveledHaskType _ t l) (at level 20). @@ -125,21 +200,6 @@ Notation "'<[' a '|-' t ']>'" := (@HaskBrak _ a t). -(* like a GHC DataCon, but using PHOAS representation for types and coercions *) -Record StrongAltConInfo {n}{tc:TyCon n} := -{ saci_numExTyVars : nat -; saci_numCoerVars : nat -; saci_numExprVars : nat -; saci_akinds : vec Kind n -; saci_ekinds : vec Kind saci_numExTyVars -; saci_kinds := app (vec2list saci_akinds) (vec2list saci_ekinds) -; saci_coercions : vec (HaskType saci_kinds * HaskType saci_kinds) saci_numCoerVars -; saci_types : vec (HaskType saci_kinds) saci_numExprVars -}. -Implicit Arguments StrongAltConInfo [[n]]. - -Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) := - fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). @@ -151,7 +211,7 @@ Definition caseType {Γ:TypeEnv}{n}(tc:TyCon n)(atypes:vec (HaskType Γ) n) := -(* FIXME: it's a mess below this point *) +(* yeah, things are kind of messy below this point *) Definition unAddKindFromInstantiatedTypeEnv {Γ:TypeEnv}{κ:Kind}{TV:Type}(ite:InstantiatedTypeEnv TV (κ::Γ)) := vec_tail ite. @@ -209,6 +269,15 @@ Definition lamer {a}{b}{c}(lt:HaskType (app (app a b) c)) : HaskType (app a (a rewrite <- ass_app in lt. exact lt. Defined. +Definition weakCK {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (κ::Γ) := + let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT t1) (weakT t2). +Definition weakCK' {Γ}{κ}(hck:HaskCoercionKind Γ) : HaskCoercionKind (app κ Γ) := + let (t1,t2) := unMkHaskCoercionKind hck in mkHaskCoercionKind (weakT' t1) (weakT' t2). +Definition weakCK'' {Γ}{κ}(hck:list (HaskCoercionKind Γ)) : list (HaskCoercionKind (app κ Γ)) := +match κ as K return list (HaskCoercionKind (app K Γ)) with + | nil => hck + | _ => map weakCK' hck +end. Definition weakL' {Γ}{κ}(lev:HaskLevel Γ) : HaskLevel (app κ Γ). induction κ; auto. apply weakL; auto. Defined. Definition weakLT {Γ}{κ}(lt:LeveledHaskType Γ) : LeveledHaskType (κ::Γ) := match lt with t @@ l => weakT t @@ weakL l end. @@ -237,11 +306,31 @@ Definition weakF {Γ:TypeEnv}{κ:Kind}(f:forall TV (env:@InstantiatedTypeEnv TV forall TV (env:@InstantiatedTypeEnv TV (κ::Γ)), TV -> RawHaskType TV := fun TV ite tv => (f TV (weakITE ite) tv). +(* like a GHC DataCon, but using PHOAS representation for types and coercions *) +Record StrongAltCon {tc:TyCon} := +{ sac_altcon : AltCon +; sac_numExTyVars : nat +; sac_numCoerVars : nat +; sac_numExprVars : nat +; sac_akinds : vec Kind tc +; sac_ekinds : vec Kind sac_numExTyVars +; sac_kinds := app (vec2list sac_akinds) (vec2list sac_ekinds) +; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ +; sac_coercions : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars +; sac_types : forall Γ (atypes:vec (HaskType Γ) tc), vec (HaskType (sac_Γ Γ)) sac_numExprVars +; sac_Δ := fun Γ (atypes:vec (HaskType Γ) tc) Δ => app (vec2list (sac_coercions Γ atypes)) Δ +}. +Coercion sac_altcon : StrongAltCon >-> AltCon. + +Definition caseType {Γ:TypeEnv}(tc:TyCon)(atypes:vec (HaskType Γ) tc) := + fold_left HaskAppT (vec2list atypes) (HaskTCon(Γ:=Γ) tc). + + (***************************************************************************************************) (* Well-Formedness of Types and Coercions *) (* also represents production "S_n:κ" of Γ because these can only wind up in Γ via rule (Type) *) -Inductive TypeFunctionDecl (n:nat)(tfc:TyFunConst n)(vk:vec Kind n) : Type := - mkTFD : Kind -> TypeFunctionDecl n tfc vk. +Inductive TypeFunctionDecl (tfc:TyCon)(vk:vec Kind tfc) : Type := + mkTFD : Kind -> TypeFunctionDecl tfc vk. (* Figure 8, upper half *) @@ -257,8 +346,8 @@ Inductive WellKinded_RawHaskType (TV:Type) | WFTyAll : forall Γ (env:InstantiatedTypeEnv TV Γ) κ σ , (∀ a, WellKinded_RawHaskType TV _ (@addKindToInstantiatedTypeEnv _ TV env a κ) (σ a) ★ ) -> WellKinded_RawHaskType TV _ env (TAll κ σ) ★ - | TySCon : forall Γ env n tfc lt vk ι , - @TypeFunctionDecl n tfc vk -> + | TySCon : forall Γ env tfc lt vk ι , + @TypeFunctionDecl tfc vk -> ListWellKinded_RawHaskType TV Γ _ env lt vk -> WellKinded_RawHaskType TV Γ env (TFCApp tfc lt) ι with ListWellKinded_RawHaskType (TV:Type) @@ -270,32 +359,42 @@ with ListWellKinded_RawHaskType (TV:Type) ListWellKinded_RawHaskType TV Γ n env lt lk -> ListWellKinded_RawHaskType TV Γ (S n) env (t:::lt) (k:::lk). -(* -Fixpoint kindOfRawHaskType {TV}(rht:RawHaskType Kind) : Kind := +Variable kindOfTyCon : forall (tc:TyCon), Kind. + Extract Inlined Constant kindOfTyCon => "(\x -> Prelude.error ""not implemented yet"")". + +Fixpoint kindOfRawHaskType (rht:RawHaskType Kind) : ???Kind := match rht with - | TVar k => k - | TCon n tc => ̱★ (* FIXME: use the StrongAltConInfo *) - | TCoerc k => k ⇛ (k ⇛ (★ ⇛ ★ )) - | TApp ht1 ht2 : RawHaskType -> RawHaskType -> RawHaskType (* φ φ *) - | TFCApp : ∀n, TyFunConst n -> vec RawHaskType n -> RawHaskType (* S_n *) - | TAll : Kind -> (TV -> RawHaskType) -> RawHaskType (* ∀a:κ.φ *) - | TCode : RawHaskType -> RawHaskType -> RawHaskType (* from λ^α *). -*) + | TVar k => OK k + | TCon tc => OK (kindOfTyCon tc) + | TCoerc t1 t2 t => OK (★ ⇛ ★ ) + | TArrow => OK (★ ⇛ ★ ⇛ ★ ) + | TApp ht1 ht2 => kindOfRawHaskType ht1 >>= fun k1 => + kindOfRawHaskType ht2 >>= fun k2 => + match k1 with + | k1' ⇛ k2' => if eqd_dec k1' k1 then OK k2' else Error "kind mismatch" + | _ => Error "attempt to apply a non-functional kind" + end + | TFCApp tc rht' => Error "calculating kind of TFCApp is not yet implemented" + | TAll k t' => kindOfRawHaskType (t' k) >>= fun k' => OK (k ⇛ k') + | TCode t1 t2 => OK ★ +end. + +Definition kindITE (Γ:TypeEnv) : InstantiatedTypeEnv Kind Γ := + list2vec Γ. + +Definition kindOfType {Γ}(ht:HaskType Γ) : ???Kind := + kindOfRawHaskType (ht Kind (kindITE Γ)). + Definition WellKindedHaskType Γ (ht:HaskType Γ) κ := forall TV env, WellKinded_RawHaskType TV Γ env (ht TV env) κ. Notation "Γ '⊢ᴛy' σ : κ" := (WellKindedHaskType Γ σ κ). - - (* "decl", production for "axiom" *) Structure AxiomDecl (n:nat)(ccon:CoFunConst n)(vk:vec Kind n){TV:Type} : Type := { axd_τ : vec TV n -> RawHaskType TV ; axd_σ : vec TV n -> RawHaskType TV }. - - - Section WFCo. Context {TV:Type}. Context {CV:Type}. @@ -311,8 +410,7 @@ Section WFCo. Inductive WFCoercion:forall Γ (Δ:CoercionEnv Γ), @InstantiatedTypeEnv TV Γ -> @InstantiatedCoercionEnv TV CV Γ Δ -> - @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop :=. -(* + @RawHaskCoer TV CV -> @RawCoercionKind TV -> Prop := | CoTVar':∀ Γ Δ t e c σ τ, (@coercionEnvContainsCoercion Γ _ TV CV t e c (@mkRawCoercionKind _ σ τ)) -> e⊢ᴄᴏ CoVar c : σ ∼ τ : Δ : Γ : t | CoRefl :∀ Γ Δ t e τ κ, t ⊢ᴛy τ :κ -> e⊢ᴄᴏ CoType τ : τ ∼ τ : Δ :Γ: t @@ -320,6 +418,7 @@ Section WFCo. | Trans :∀ Γ Δ t e γ₁ γ₂ σ₁ σ₂ σ₃,(e⊢ᴄᴏ γ₁:σ₁∼σ₂:Δ:Γ:t) -> (e⊢ᴄᴏ γ₂:σ₂∼σ₃:Δ:Γ:t) -> e⊢ᴄᴏ CoComp γ₁ γ₂: σ₁ ∼ σ₃ : Δ :Γ: t | Left :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoLeft γ : σ₁ ∼ τ₁ : Δ :Γ: t | Right :∀ Γ Δ t e γ σ₁ σ₂ τ₁ τ₂,(e⊢ᴄᴏ γ : TApp σ₁ σ₂ ∼ TApp τ₁ τ₂ :Δ:Γ:t ) -> e⊢ᴄᴏ CoRight γ : σ₂ ∼ τ₂ : Δ :Γ: t + (* | SComp :∀ Γ Δ t e γ n S σ τ κ, ListWFCo Γ Δ t e γ σ τ -> t ⊢ᴛy TFCApp(n:=n) S σ : κ -> e⊢ᴄᴏ CoTFApp S γ : TFCApp S σ∼TFCApp S τ : Δ : Γ : t | CoAx :∀ Γ Δ t e n C κ γ, forall (σ₁:vec TV n) (σ₂:vec TV n), forall (ax:@AxiomDecl n C κ TV), @@ -327,17 +426,15 @@ Section WFCo. ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₁)) (vec2list κ) -> ListWellKinded_RawHaskType TV Γ t (map TVar (vec2list σ₂)) (vec2list κ) -> e⊢ᴄᴏ CoCFApp C γ : axd_σ _ _ _ ax σ₁ ∼ axd_τ _ _ _ ax σ₂ : Δ : Γ : t - + *) | WFCoAll : forall Γ Δ κ (t:InstantiatedTypeEnv TV Γ) (e:InstantiatedCoercionEnv TV CV (κ::Γ) (weakCE Δ)) γ σ τ , (∀ a, e ⊢ᴄᴏ ( γ a) : ( σ a) ∼ ( τ a) : _ : _ : (t + a : κ)) -> weakICE e ⊢ᴄᴏ (CoAll κ γ ) : (TAll κ σ ) ∼ (TAll κ τ ) : Δ : Γ : t - | Comp :forall Γ Δ t e γ₁ γ₂ σ₁ σ₂ τ₁ τ₂ κ, (t ⊢ᴛy TApp σ₁ σ₂:κ)-> (e⊢ᴄᴏ γ₁:σ₁∼τ₁:Δ:Γ:t)-> (e⊢ᴄᴏ γ₂:σ₂∼τ₂:Δ:Γ:t) -> e⊢ᴄᴏ (CoApp γ₁ γ₂) : (TApp σ₁ σ₂) ∼ (TApp τ₁ τ₂) : Δ:Γ:t - | CoInst :forall Γ Δ t e σ τ κ γ (v:∀ TV, InstantiatedTypeEnv TV Γ -> RawHaskType TV), t ⊢ᴛy v TV t : κ -> (e⊢ᴄᴏ γ:HaskTAll κ σ _ t ∼ HaskTAll κ τ _ t:Δ:Γ:t) -> @@ -350,7 +447,6 @@ Section WFCo. | LWFCo_cons : ∀ Γ Δ t e a b c la lb lc, (e⊢ᴄᴏ a : b∼c : Δ : Γ : t )-> ListWFCo Γ Δ t e la lb lc -> ListWFCo Γ Δ t e (a::la) (b::lb) (c::lc) where "ice '⊢ᴄᴏ' γ : a '∼' b : Δ : Γ : ite" := (@WFCoercion Γ Δ ite ice γ (@mkRawCoercionKind _ a b)). -*) End WFCo. Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:HaskType Γ) := @@ -358,9 +454,9 @@ Definition WFCCo (Γ:TypeEnv)(Δ:CoercionEnv Γ)(γ:HaskCoercion Γ Δ)(a b:Hask @WFCoercion _ _ Γ Δ env cenv (γ TV CV env cenv) (@mkRawCoercionKind _ (a TV env) (b TV env)). Notation "Δ '⊢ᴄᴏ' γ : a '∼' b" := (@WFCCo _ Δ γ a b). - Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)). - Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18). +Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ := fun TV ite => (TCon (haskLiteralToTyCon lit)). +Notation "a ∼∼∼ b" := (mkHaskCoercionKind a b) (at level 18). Fixpoint update_ξ `{EQD_VV:EqDecidable VV}{Γ}(ξ:VV -> LeveledHaskType Γ)(vt:list (VV * LeveledHaskType Γ)) : VV -> LeveledHaskType Γ := @@ -368,29 +464,3 @@ Fixpoint update_ξ | nil => ξ | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v' end. - - - - - - - - - - - - - - - - -(* just like GHC's AltCon, but using PHOAS types and coercions *) -Record StrongCaseBranch {n}{tc:TyCon n}{Γ}{atypes:vec (HaskType Γ) n} := -{ scb_saci : @StrongAltConInfo _ tc -; scb_Γ : TypeEnv := app (vec2list (saci_ekinds scb_saci)) Γ -; scb_Δ : CoercionEnv scb_Γ -; scb_types : vec (LeveledHaskType (app (vec2list (saci_ekinds scb_saci)) Γ)) (saci_numExprVars scb_saci) -}. -Coercion scb_saci : StrongCaseBranch >-> StrongAltConInfo. -Implicit Arguments StrongCaseBranch [[n][Γ]]. -