X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeakToStrong.v;h=d77d07417da9cc5e691cc37c165173c8368b968f;hp=6d4bf16771bb39220b721f2dc498ecca01f37a05;hb=0bcb62ecea66324c01f73264ee7cbb4b441ada7c;hpb=1cfe65d4e2d3292cc038882d8518dd7a48e2c40a

diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v
index 6d4bf16..d77d074 100644
--- a/src/HaskWeakToStrong.v
+++ b/src/HaskWeakToStrong.v
@@ -10,7 +10,8 @@ Require Import Coq.Strings.String.
 Require Import Coq.Lists.List.
 Require Import Coq.Init.Specif.
 Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
 Require Import HaskWeak.
@@ -18,6 +19,7 @@ Require Import HaskWeakToCore.
 Require Import HaskStrongTypes.
 Require Import HaskStrong.
 Require Import HaskCoreVars.
+Require Import HaskCoreTypes.
 
 Open Scope string_scope.
 Definition TyVarResolver Γ   := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt).
@@ -124,7 +126,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' =>
@@ -176,7 +179,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)
     apply OK.
     eapply haskTypeOfSomeKind.
     unfold HaskType; intros.
-    apply TyFunApp.
+    apply (TyFunApp tc (fst (tyFunKind tc)) (snd (tyFunKind tc))).
     apply lt'.
     apply X.
 
@@ -414,7 +417,7 @@ Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Ex
   Defined.
 
 Definition coVarKind (wcv:WeakCoerVar) : Kind :=
-  match wcv with weakCoerVar _ κ _ _ => κ end.
+  match wcv with weakCoerVar _ t _ => (kindOfCoreType (weakTypeToCoreType t)) end.
   Coercion coVarKind : WeakCoerVar >-> Kind.
 
 Definition weakTypeToTypeOfKind : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType)(κ:Kind), ???(HaskType Γ κ).
@@ -519,6 +522,14 @@ Definition checkDistinct :
   exact (Error "checkDistinct failed").
   Defined.
 
+(* FIXME: check the kind of the type of the weakexprvar to support >0 *)
+Definition mkGlobal Γ (τ:HaskType Γ ★) (wev:WeakExprVar) : Global Γ.
+  refine {| glob_kinds := nil |}.
+  apply wev.
+  intros.
+  apply τ.
+  Defined.
+
 Definition weakExprToStrongExpr : forall
     (Γ:TypeEnv)
     (Δ:CoercionEnv Γ)
@@ -544,7 +555,7 @@ Definition weakExprToStrongExpr : forall
     match we with
 
     | WEVar   v                         => if ig v
-                                              then OK (EGlobal Γ Δ ξ (τ@@lev) v)
+                                              then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev))
                                               else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v)
 
     | WELit   lit                       => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev)
@@ -621,7 +632,7 @@ Definition weakExprToStrongExpr : forall
                                              | _                 => Error ("weakTypeToType: WECoApp body with type "+++toString te)
                                            end
 
-    | WECoLam cv e                      => let (_,_,t1,t2) := cv in
+    | WECoLam cv e                      => let (_,t1,t2) := cv in
                                            weakTypeOfWeakExpr e >>= fun te =>
                                              weakTypeToTypeOfKind φ te ★ >>= fun te' =>
                                                weakTypeToTypeOfKind φ t1 cv >>= fun t1' =>