X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;fp=src%2FHaskCoreToWeak.v;h=63c7e956f3b62db9e81bbdccb13fbf00db787e27;hp=1cbaf228293a9bb6c296ce7efc69523ecf3a2292;hb=635ee434c9edbad1bc6c9bf5ba2b91cb8c51be8e;hpb=f49db0fc38c6c430585e4e48304510212c3f1a0f

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1cbaf22..63c7e95 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -107,6 +107,15 @@ Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
           OK (WCoUnsafe t1' t2').
 *)
 
+(* if this is a (WAppTy (WAppTy ... (WTyCon tc) .. ) .. ), return (tc,[...]) *)
+Fixpoint expectTyConApp (wt:WeakType)(acc:list WeakType) : ???(TyCon * list WeakType) :=
+  match wt with
+    | WTyCon tc        => OK (tc,acc)
+    | WAppTy t1 t2     => expectTyConApp t1 (t2::acc)
+    | WTyFunApp tc tys => Error ("expectTyConApp encountered TyFunApp: " +++ wt)
+    | _                => Error ("expectTyConApp encountered " +++ wt)
+  end.
+
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)
@@ -178,8 +187,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | WExprVar ev => 
         coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
         coreExprToWeakExpr e >>= fun e' =>
-          (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
-             >>= fun tca =>
+          expectTyConApp te' nil >>= fun tca =>
             let (tc,lt) := tca in
           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=