X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=8f2a5268739ee86e8435612a16cbe402135cdaf4;hp=31accd29a2e1dae3d03187191b76d13d94833e74;hb=5cfd103cffd56381262b2d280cbba88e0932f78a;hpb=bcb16a7fa1ff772f12807c4587609fd756b7762e

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index 31accd2..8f2a526 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -8,6 +8,7 @@ Require Import General.
 Require Import Coq.Lists.List.
 Require Import HaskKinds.
 Require Import HaskCoreLiterals.
+Require Import HaskCore.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCoreTypes.
@@ -28,14 +29,15 @@ Inductive WeakExpr :=
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
 
-(* the WeakType argument in WEBrak/WEEsc is used only when going back    *)
-(* from Weak to Core; it lets us dodge a possibly-failing type           *)
-(* calculation                                                           *)
-| WEBrak      : WeakTypeVar                     -> WeakExpr  -> WeakType     -> WeakExpr
-| WEEsc       : WeakTypeVar                     -> WeakExpr  -> WeakType     -> WeakExpr
+(* The WeakType argument in WEBrak/WEEsc is used only when going back      *)
+(* from Weak to Core; it lets us dodge a possibly-failing type             *)
+(* calculation.  The CoreVar argument is the GlobalVar for the hetmet_brak *)
+(* or hetmet_esc identifier                                                *)
+| WEBrak      : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
+| WEEsc       : CoreVar -> WeakTypeVar          -> WeakExpr  -> WeakType     -> WeakExpr
 
-(* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
-| WECase      : forall (scrutinee:WeakExpr)
+| WECase      : forall (vscrut:WeakExprVar)
+                       (scrutinee:WeakExpr)
                        (tbranches:WeakType)
                        (tc:TyCon)
                        (type_params:list WeakType)
@@ -43,6 +45,7 @@ Inductive WeakExpr :=
                        WeakExpr.
 
 (* calculate the free WeakVar's in a WeakExpr *)
+(*
 Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
   match me with
     | WELit    _        =>     nil
@@ -92,47 +95,9 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr :=
     | nil      => me
     | cv::cvl' => WELam cv (closeExpression me cvl')
   end) me (getWeakExprFreeVars me).
-
+*)
 Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType :=
   (WTyCon (haskLiteralToTyCon lit)).
 
-(* calculate the CoreType of a WeakExpr *)
-Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
-  match ce with
-    | WEVar   (weakExprVar v t) => OK t
-    | WELit   lit   => OK (weakTypeOfLiteral lit)
-    | WEApp   e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' =>
-                       match t' with
-                         | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2
-                         | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp")
-                       end
-    | WETyApp e t    => weakTypeOfWeakExpr e >>= fun te =>
-                        match te with
-                          | WForAllTy v ct => OK (replaceWeakTypeVar ct v t)
-                          | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp")
-                        end
-    | WECoApp e co   => weakTypeOfWeakExpr e >>= fun te =>
-                        match te with
-                          | WCoFunTy t1 t2 t => OK t
-                          | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp")
-                        end
-    | WELam   (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t')
-    | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t')
-    | WECoLam (weakCoerVar cv φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t')
-    | WELet   ev ve e            => weakTypeOfWeakExpr e
-    | WELetRec rb e              => weakTypeOfWeakExpr e
-    | WENote  n e                => weakTypeOfWeakExpr e
-    | WECast  e (weakCoercion t1 t2 _) => OK t2
-    | WECase  scrutinee tbranches tc type_params alts => OK tbranches
-
-    (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
-    | WEBrak  ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
-    | WEEsc   ec e _ => weakTypeOfWeakExpr e >>= fun t' =>
-      match t' with
-        | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') =>
-          if eqd_dec ec ec' then OK t''
-            else Error "level mismatch in escapification"
-        | _ => Error "ill-typed escapification"
-      end
-  end.
-
+Variable coreTypeOfCoreExpr    : @CoreExpr CoreVar -> CoreType.
+  Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType".