update PCF.v for new ECKind

[coq-hetmet.git] / src / HaskStrongTypes.v

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index 7ce04fb..dab8cde 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -8,7 +8,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
@@ -68,7 +69,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 +132,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 +160,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.
@@ -209,6 +210,51 @@ Structure Global Γ :=
 Coercion glob_tf : Global >-> Funclass.
 Coercion glob_wv : Global >-> WeakExprVar.
 
+(* From (t1->(t2->(t3-> ... t))), return t1::t2::t3::...nil *)
+(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
+Definition take_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), list (RawHaskType TV κ).
+refine (fix take_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : list (RawHaskType TV κ) :=
+  match exp as E in RawHaskType _ K return κ=K -> list (RawHaskType _ K) with
+  | TApp   κ₁ κ₂ x y      =>
+    fun eqpf =>
+      ((fun q:list (RawHaskType TV κ₂) =>
+        match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> list (RawHaskType _ _) with
+          | TApp   κ₁' κ₂' x' y'      =>
+            fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
+                           | TArrow => fun eqpf'' => _
+                           | _      => fun _      => nil
+                         end (refl_equal _)
+          | _                         => fun _ => nil
+        end (refl_equal _))
+      (take_arg_types TV _ y))
+    | _                     => fun _ => nil
+  end (refl_equal _)).
+  subst; inversion eqpf''; subst.
+  apply (y'::q).
+  Defined.
+
+(* From (t1->(t2->(t3-> ... t))), return t *)
+(* this is a billion times uglier than it needs to be as a result of how primitive Coq's termiation checker is *)
+Definition drop_arg_types : forall {TV}{κ}(exp: RawHaskType TV κ), RawHaskType TV κ.
+refine (fix drop_arg_types {TV}{κ}(exp: RawHaskType TV κ) {struct exp} : RawHaskType TV κ :=
+  match exp as E in RawHaskType _ K return κ=K -> RawHaskType _ K with
+  | TApp   κ₁ κ₂ x y      =>
+    fun eqpf =>
+      ((fun q:RawHaskType TV κ₂ =>
+        match x as X in RawHaskType _ KX return κ₂ ⇛ κ₁ = KX -> RawHaskType _ _ with
+          | TApp   κ₁' κ₂' x' y'      =>
+            fun eqpf' => match x' in RawHaskType _ KX' return (κ₂' ⇛ κ₁') = KX' -> _ with
+                           | TArrow => fun eqpf'' => _
+                           | z      => fun _      => TApp x y
+                         end (refl_equal _)
+          | z                         => fun _ => TApp x y
+        end (refl_equal _))
+      (drop_arg_types TV _ y))
+    | z                     => fun _ => z
+  end (refl_equal _)).
+  subst; inversion eqpf''; subst.
+  apply q.
+  Defined.