From: Adam Megacz Date: Mon, 9 May 2011 04:35:56 +0000 (-0700) Subject: abstract out the kind of environment classifiers (ECKind) X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=b4857a6f575dffd5c9c9d5decbc21ff63a338270;hp=cb424978e057bc2b4868517302738d52246fba04 abstract out the kind of environment classifiers (ECKind) --- diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 58bc13e..e628f26 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -335,13 +335,13 @@ Section core2proof. Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil. Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ := TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b. - Definition ga_type {TV}(a b c:RawHaskType TV ★) : RawHaskType TV ★ := + Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ := TApp (TApp (TApp (@TyFunApp TV hetmet_PGArrowTyCon nil _ TyFunApp_nil) a) b) c. Definition ga := @ga_mk ga_unit ga_prod (@ga_type). - Definition ga_type' {Γ}(a b c:HaskType Γ ★) : HaskType Γ ★ := + Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ := fun TV ite => TApp (TApp (TApp (@TyFunApp TV hetmet_PGArrowTyCon nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite). diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 6d9d7a6..60a205f 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -196,12 +196,12 @@ Section HaskFlattener. Context {unitTy : forall TV, RawHaskType TV ★ }. Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. - Context {gaTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. + Context {gaTy : forall TV, RawHaskType TV ECKind -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr). - Definition ga_mk {Γ}(ec:HaskType Γ ★ )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := + Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite). Class garrow := @@ -257,7 +257,7 @@ Section HaskFlattener. fun TV ite => garrowfy_raw_codetypes (ht TV ite). - Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite). + Definition v2t {Γ}(ec:HaskTyVar Γ ECKind) := fun TV ite => TVar (ec TV ite). Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ := match lev with @@ -509,7 +509,7 @@ Section HaskFlattener. *) Definition garrowfy_arrangement' : forall Γ (Δ:CoercionEnv Γ) - (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), + (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ]. intros Γ Δ ec lev. @@ -554,7 +554,7 @@ Section HaskFlattener. Definition garrowfy_arrangement : forall Γ (Δ:CoercionEnv Γ) n - (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ, + (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ, ND Rule [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1) |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]] diff --git a/src/HaskKinds.v b/src/HaskKinds.v index 3539e95..2200f51 100644 --- a/src/HaskKinds.v +++ b/src/HaskKinds.v @@ -37,6 +37,10 @@ Instance KindToString : ToString Kind := { toString := kindToString }. Notation "'★'" := KindStar. Notation "a ⇛ b" := (KindArrow a b). +(* the kind of environment classifiers *) +Definition ECKind := ★ . +Opaque ECKind. + Fixpoint kindToLatexMath (k:Kind) : LatexMath := match k with | ★ => rawLatexMath "\star" diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index edac1aa..0d33b0a 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -126,7 +126,7 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS | nil => t'' | lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++ (fold_left (fun x y => x+++(rawLatexMath ":")+++y) - (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath "")) + (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath "")) end end); try apply ConcatenableLatexMath. try apply VarNameMonad. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 7ce04fb..aafbe9b 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -68,7 +68,7 @@ Section Raw. | TCoerc : ∀ κ, RawHaskType κ -> RawHaskType κ -> RawHaskType ★ -> RawHaskType ★ (* (+>) *) | TApp : ∀ κ₁ κ₂, RawHaskType (κ₂⇛κ₁) -> RawHaskType κ₂ -> RawHaskType κ₁ (* φ φ *) | TAll : ∀ κ, (TV κ -> RawHaskType ★) -> RawHaskType ★ (* ∀a:κ.φ *) - | TCode : RawHaskType ★ -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *) + | TCode : RawHaskType ECKind -> RawHaskType ★ -> RawHaskType ★ (* from λ^α *) | TyFunApp : forall (tf:TyFun) kl k, RawHaskTypeList kl -> RawHaskType k (* S_n *) with RawHaskTypeList : list Kind -> Type := | TyFunApp_nil : RawHaskTypeList nil @@ -131,7 +131,7 @@ Definition InstantiatedCoercionEnv (TV:Kind->Type) CV (Γ:TypeEnv)(Δ:Coer (* A (HaskXX Γ) is an XX which is valid in environments of shape Γ; they are always PHOAS-uninstantiated *) Definition HaskTyVar (Γ:TypeEnv) κ := forall TV (env:@InstantiatedTypeEnv TV Γ), TV κ. Definition HaskCoVar Γ Δ := forall TV CV (env:@InstantiatedTypeEnv TV Γ)(cenv:@InstantiatedCoercionEnv TV CV Γ Δ), CV. -Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ★). +Definition HaskLevel (Γ:TypeEnv) := list (HaskTyVar Γ ECKind). Definition HaskType (Γ:TypeEnv) κ := ∀ TV, @InstantiatedTypeEnv TV Γ -> RawHaskType TV κ. Definition haskTyVarToType {Γ}{κ}(htv:HaskTyVar Γ κ) : HaskType Γ κ := fun TV ite => TVar (htv TV ite). @@ -159,7 +159,7 @@ 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 Γ ★:= +Definition HaskBrak {Γ}(v:HaskTyVar Γ ECKind)(t:HaskType Γ ★) : HaskType Γ ★:= fun TV env => @TCode TV (TVar (v TV env)) (t TV env). Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc)) := fun TV ite => TCon tc. diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index b9ac068..122db2a 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -124,7 +124,8 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _ | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _ | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _ - | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ★ ec) >>= fun ec' => _ + | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody + >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _ | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' =>