X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskWeak.v;fp=src%2FHaskWeak.v;h=a9f8bb66f10529794544c68019ec9a50fdbfa414;hp=ff696cc3e664a17bf8240accc84ddffb09a8aae1;hb=703bff3b209bd7d114b49cb736da8af167a4ec71;hpb=5a0761840d89b82cdacb0bf9215fd41aba847b68

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index ff696cc..a9f8bb6 100644
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -26,8 +26,12 @@ Inductive WeakExpr :=
 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
-| WEBrak      : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
-| WEEsc       : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
+
+(* the CoreType argument is used only when going back from Weak to Core; it lets us dodge a possibly-failing type calculation *)
+| WEBrak      : WeakTypeVar                     -> WeakExpr  -> CoreType     -> WeakExpr
+| WEEsc       : WeakTypeVar                     -> WeakExpr  -> CoreType     -> WeakExpr
+
+(* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
 | WECase      : forall (scrutinee:WeakExpr)
                        (tbranches:CoreType)
                        {n:nat}(tc:TyCon n)
@@ -44,8 +48,8 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
     | WENote   n e      =>                            getWeakExprFreeVars e
     | WETyApp  e t      =>                            getWeakExprFreeVars e
     | WECoApp  e co     =>                            getWeakExprFreeVars e
-    | WEBrak   ec e     =>                            getWeakExprFreeVars e
-    | WEEsc    ec e     =>                            getWeakExprFreeVars e
+    | WEBrak   ec e _   =>                            getWeakExprFreeVars e
+    | WEEsc    ec e _   =>                            getWeakExprFreeVars e
     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
     | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
@@ -147,9 +151,11 @@ Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
     | WENote  n e                => coreTypeOfWeakExpr e
     | WECast  e (weakCoercion t1 t2 _) => OK t2
     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches
-    | WEBrak  ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+
+    (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
+    | WEBrak  ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
                                                            OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end
-    | WEEsc   ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+    | WEEsc   ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
       match t' with
         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
           if (tyCon_eq tc hetMetCodeTypeTyCon)