require all branches of LetRec be at the same level in HaskProof

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

diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v
index e79927a..f8493b4 100644 (file)
--- a/src/HaskStrongTypes.v
+++ b/src/HaskStrongTypes.v
@@ -8,7 +8,7 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import General.
 Require Import HaskKinds.
-Require Import HaskCoreLiterals.
+Require Import HaskLiteralsAndTyCons.
 Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
@@ -21,7 +21,7 @@ Variable dataConExVars_    : CoreDataCon -> list CoreVar.  Extract Inlined Const
 Variable dataConEqTheta_   : CoreDataCon -> list PredType. Extract Inlined Constant dataConEqTheta_   => "DataCon.dataConEqTheta".
 Variable dataConOrigArgTys_: CoreDataCon -> list CoreType. Extract Inlined Constant dataConOrigArgTys_=>"DataCon.dataConOrigArgTys".
 
-(* FIXME: might be a better idea to panic here than simply drop things that look wrong *)
+(* TODO: might be a better idea to panic here than simply drop things that look wrong *)
 Definition dataConExTyVars cdc :=
   filter (map (fun x => match coreVarToWeakVar x with WTypeVar v => Some v | _ => None end) (dataConExVars_ cdc)).
   Opaque dataConExTyVars.
@@ -74,7 +74,7 @@ Instance DataConEqDecidable : forall tc, EqDecidable (@DataCon tc).
   right; auto.
   Defined.
 
-Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc).
+Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
 
 (* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
 Section Raw.
@@ -185,7 +185,7 @@ Definition HaskTApp {Γ}{κ}(σ:forall TV (env:@InstantiatedTypeEnv TV Γ), TV 
   := 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 {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc))
+Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
   := fun TV ite => TCon tc.
 Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
   fun TV ite => TApp (t1 TV ite) (t2 TV ite).
@@ -336,11 +336,11 @@ Definition weakF {Γ:TypeEnv}{κ}{κ₂}(f:forall TV (env:@InstantiatedTypeEnv T
 
 Fixpoint caseType0 {Γ}(lk:list Kind) :
   IList _ (HaskType Γ) lk ->
-  HaskType Γ (fold_right KindTypeFunction ★ lk) ->
+  HaskType Γ (fold_right KindArrow ★ lk) ->
   HaskType Γ ★ :=
   match lk as LK return
     IList _ (HaskType Γ) LK ->
-    HaskType Γ (fold_right KindTypeFunction ★ LK) ->
+    HaskType Γ (fold_right KindArrow ★ LK) ->
     HaskType Γ ★ 
   with
   | nil    => fun _     ht => ht
@@ -353,7 +353,7 @@ Definition caseType {Γ}(tc:TyCon)(atypes:IList _ (HaskType Γ) (tyConKind tc))
 (* like a GHC DataCon, but using PHOAS representation for types and coercions *)
 Record StrongAltCon {tc:TyCon} :=
 { sac_tc          := tc
-; sac_altcon      :  AltCon
+; sac_altcon      :  WeakAltCon
 ; sac_numExTyVars :  nat
 ; sac_numCoerVars :  nat
 ; sac_numExprVars :  nat
@@ -365,7 +365,7 @@ Record StrongAltCon {tc:TyCon} :=
 ; sac_Δ           := fun    Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ
 }.
 Coercion sac_tc     : StrongAltCon >-> TyCon.
-Coercion sac_altcon : StrongAltCon >-> AltCon.
+Coercion sac_altcon : StrongAltCon >-> WeakAltCon.
   
 
 Definition kindOfType {Γ}{κ}(ht:@HaskType Γ κ) : ???Kind := OK κ.
@@ -385,13 +385,35 @@ Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18).
 Fixpoint update_ξ
   `{EQD_VV:EqDecidable VV}{Γ}
    (ξ:VV -> LeveledHaskType Γ ★)
-   (vt:list (VV * LeveledHaskType Γ ★))
+   (lev:HaskLevel Γ)
+   (vt:list (VV * HaskType Γ ★))
    : VV -> LeveledHaskType Γ ★ :=
   match vt with
     | nil => ξ
-    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ else (update_ξ ξ tl) v'
+    | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v'
   end.
 
+Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v,
+  not (In v (map (@fst _ _) varstypes)) ->
+  (update_ξ ξ lev varstypes) v = ξ v.
+  intros.
+  induction varstypes.
+  reflexivity.
+  simpl.
+  destruct a.
+  destruct (eqd_dec v0 v).
+  subst.
+  simpl in  H.
+  assert False. 
+  apply H.
+  auto.
+  inversion H0.
+  apply IHvarstypes.
+  unfold not; intros.
+  apply H.
+  simpl.
+  auto.
+  Defined.
 
 
 (***************************************************************************************************)