X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;h=e5a2bfb8b2fc11da5f2fd2c39fa0afd7b94ad3ad;hp=f177e1f144b52704b4687cc476ee1be809476d53;hb=26733c04106397dc8a10396ce688e908e8d0cde7;hpb=65a6d16ea7d8a07fe8e162151b76cf40a41d8c31

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index f177e1f..e5a2bfb 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -28,11 +28,12 @@ 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)
@@ -127,8 +128,8 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType :=
     | 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' =>
+    | 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''