abstract out the kind of environment classifiers (ECKind)

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 58bc13e..e628f26 100644 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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 (file)
--- 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' =>