X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=17346378feaca1ace6c65c926756da5048253a47;hp=a812483bc7ded9f0e91dddeb8c1188e55628ac23;hb=5cfd103cffd56381262b2d280cbba88e0932f78a;hpb=ee5aaad57d76400e9b8736d4a12d2804f99f329c

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index a812483..1734637 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -14,6 +14,7 @@ Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
+Require Import HaskWeakToCore.
 
 Axiom    tycons_distinct       : ~(ArrowTyCon=ModalBoxTyCon).
 Variable tyConOrTyFun          : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun      => "tyConOrTyFun".
@@ -74,6 +75,9 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
 Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
 
+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
+
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
 match ce with