update for new GHC coercion representation

[coq-hetmet.git] / src / HaskCoreToWeak.v

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 1734637..7669e5d 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -4,27 +4,47 @@
 
 Generalizable All Variables.
 Require Import Preamble.
 
 Generalizable All Variables.
 Require Import Preamble.

-Require Import General.

 Require Import Coq.Lists.List.
 Require Import Coq.Lists.List.

+Require Import General.

 Require Import HaskKinds.
 Require Import HaskKinds.

-Require Import HaskCoreLiterals.
+Require Import HaskLiterals.
+Require Import HaskTyCons.

 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 Require Import HaskCore.
 Require Import HaskWeakVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeak.
 Require Import HaskCoreVars.
 Require Import HaskCoreTypes.
 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".
+Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun.          Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun".
+Variable coreViewDeep : CoreType  -> CoreType.                 Extract Inlined Constant coreViewDeep => "coreViewDeep".
+Variable coercionKind : CoreCoercion -> (CoreType * CoreType).
+   Extract Inlined Constant coercionKind => "(\x -> Pair.unPair (Coercion.coercionKind x))".
+
+(* extracts the Name from a CoreVar *)
+Variable coreVarCoreName    : CoreVar -> CoreName.   Extract Inlined Constant coreVarCoreName  => "Var.varName".
+
+(* the magic wired-in name for the modal type introduction/elimination forms *)
+Variable hetmet_brak_name   : CoreName.              Extract Inlined Constant hetmet_brak_name => "PrelNames.hetmet_brak_name".
+Variable hetmet_esc_name    : CoreName.              Extract Inlined Constant hetmet_esc_name  => "PrelNames.hetmet_esc_name".
+Variable hetmet_csp_name    : CoreName.              Extract Inlined Constant hetmet_csp_name  => "PrelNames.hetmet_csp_name".
+
+Definition mkTyFunApplication (tf:TyFun)(lwt:list WeakType) : ???WeakType :=
+  split_list lwt (length (fst (tyFunKind tf))) >>=
+  fun argsrest =>
+    let (args,rest) := argsrest in
+      OK (fold_left (fun x y => WAppTy x y) rest (WTyFunApp tf args)).
+
+(* a hack to evade the guardedness check of Fixpoint *)
+Variable coreTypeToWeakTypeCheat' : CoreType -> ???WeakType.
+Extract Inlined Constant coreTypeToWeakTypeCheat' => "coreTypeToWeakType'".

 
 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   match ct with
   | TyVarTy  cv              => match coreVarToWeakVar cv with
 
 Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   match ct with
   | TyVarTy  cv              => match coreVarToWeakVar cv with

-                                  | WExprVar _  => Error "encountered expression variable in a type"
-                                  | WTypeVar tv => OK (WTyVarTy tv)
-                                  | WCoerVar _  => Error "encountered coercion variable in a type"
+                                  | CVTWVR_EVar  ct    => Error "encountered expression variable in a type"
+                                  | CVTWVR_TyVar k     => OK (WTyVarTy (weakTypeVar cv k))
+                                  | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a type"

                                 end
 
   | AppTy    t1 t2           => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')
                                 end
 
   | AppTy    t1 t2           => coreTypeToWeakType' t2 >>= fun t2' => coreTypeToWeakType' t1 >>= fun t1' => OK (WAppTy t1' t2')

@@ -35,16 +55,17 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                   | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
                                 end) lct)
       in match tyConOrTyFun tc_ with
                                   | a::b => coreTypeToWeakType' a >>= fun a' => rec b >>= fun b' => OK (a'::b')
                                 end) lct)
       in match tyConOrTyFun tc_ with

-           | inr tf => recurse >>= fun recurse' => OK (WTyFunApp tf recurse')
+           | inr tf => recurse >>= fun recurse' => mkTyFunApplication tf recurse'

            | inl tc => if eqd_dec tc ModalBoxTyCon
                          then match lct with
                                 | ((TyVarTy ec)::tbody::nil) =>
                                   match coreVarToWeakVar ec with
            | inl tc => if eqd_dec tc ModalBoxTyCon
                          then match lct with
                                 | ((TyVarTy ec)::tbody::nil) =>
                                   match coreVarToWeakVar ec with

-                                    | WTypeVar ec' => coreTypeToWeakType' tbody >>= fun tbody' => OK (WCodeTy ec' tbody')
-                                    | WExprVar _  => Error "encountered expression variable in a modal box type"
-                                    | WCoerVar _  => Error "encountered coercion variable in a modal box type"
+                                    | CVTWVR_EVar  ct    => Error "encountered expression variable in a modal box type"
+                                    | CVTWVR_CoVar t1 t2 => Error "encountered coercion variable in a modal box type"
+                                    | CVTWVR_TyVar k     => coreTypeToWeakType' tbody >>= fun tbody' => 
+                                                              OK (WCodeTy (weakTypeVar ec k) tbody')

                                   end
                                   end

-                                | _                           => Error "mis-applied modal box tycon"
+                                | _                      => Error ("mis-applied modal box tycon: " +++ toString ct)

                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon
                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon

@@ -59,9 +80,12 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                 coreTypeToWeakType' t2 >>= fun t2' => 
                                   OK (WAppTy (WAppTy WFunTyCon t1') t2')
   | ForAllTy cv t            => match coreVarToWeakVar cv with
                                 coreTypeToWeakType' t2 >>= fun t2' => 
                                   OK (WAppTy (WAppTy WFunTyCon t1') t2')
   | ForAllTy cv t            => match coreVarToWeakVar cv with

-                                  | WExprVar _  => Error "encountered expression variable in a type"
-                                  | WTypeVar tv => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy tv t')
-                                  | WCoerVar _  => Error "encountered coercion variable in a type"
+                                  | CVTWVR_EVar  ct    => Error "encountered expression variable in a type abstraction"
+                                  | CVTWVR_TyVar k     => coreTypeToWeakType' t >>= fun t' => OK (WForAllTy (weakTypeVar cv k) t')
+                                  | CVTWVR_CoVar t1 t2 => coreTypeToWeakTypeCheat' t1 >>= fun t1' => 
+                                                            coreTypeToWeakTypeCheat' t2 >>= fun t2' => 
+                                                              coreTypeToWeakType' t >>= fun t3' => 
+                                                                OK (WCoFunTy t1' t2' t3')

                                 end
   | PredTy (ClassP  cl lct) => ((fix rec tl := match tl with 
                                                   | nil => OK nil
                                 end
   | PredTy (ClassP  cl lct) => ((fix rec tl := match tl with 
                                                   | nil => OK nil

@@ -72,52 +96,106 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
   end.
 
   | PredTy (EqPred _ _)   => Error "hit a bare EqPred"
   end.
 

-Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreViewDeep => "coreViewDeep".
-Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
+Definition coreTypeToWeakType t :=
+  addErrorMessage ("during coreTypeToWeakType on " +++ toString t +++ eol) (coreTypeToWeakType' (coreViewDeep t)).

 
 

-Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
-  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
+Definition coreVarToWeakVar' (cv:CoreVar) : ???WeakVar :=
+  addErrorMessage ("during coreVarToWeakVar on " +++ toString cv +++ eol)
+  match coreVarToWeakVar cv with
+    | CVTWVR_EVar  ct    => coreTypeToWeakType ct >>= fun t' => OK (WExprVar (weakExprVar cv t'))
+    | CVTWVR_TyVar k     =>                                     OK (WTypeVar (weakTypeVar cv k))
+    | CVTWVR_CoVar t1 t2 =>
+      (* this will choke if given a coercion-between-coercions (EqPred (EqPred c1 c2) (EqPred c3 c4)) *)
+      addErrorMessage ("with t2=" +++ toString t2 +++ eol)
+      ((coreTypeToWeakType t2) >>= fun t2' =>
+      addErrorMessage ("with t1=" +++ toString t1 +++ eol)
+      (coreTypeToWeakType t1) >>= fun t1' =>
+                                OK (WCoerVar (weakCoerVar cv t1' t2')))
+  end.
+Definition tyConTyVars (tc:CoreTyCon) :=
+  filter (map (fun x => match coreVarToWeakVar' x with OK (WTypeVar v) => Some v | _ => None end) (getTyConTyVars_ tc)).
+  Opaque tyConTyVars.
+Definition tyConKind (tc:TyCon) : list Kind := map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc).

 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)

-Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=

 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then

-      match coreVarToWeakVar ec with
-        | WExprVar _  => None
-        | WTypeVar tv => Some (v,tv,tbody)
-        | WCoerVar _  => None
+      match coreVarToWeakVar' ec with
+        | OK (WTypeVar tv) => match coreVarToWeakVar' v with
+                           | OK (WExprVar v') => Some (v',tv,tbody)
+                           | _ => None
+                         end
+        | _  => None

       end else None
   | _ => None
 end.
       end else None
   | _ => None
 end.

-Definition isEsc (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) :=
+
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=

 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then

-      match coreVarToWeakVar ec with
-        | WExprVar _  => None
-        | WTypeVar tv => Some (v,tv,tbody)
-        | WCoerVar _  => None
+      match coreVarToWeakVar' ec with
+        | OK (WTypeVar tv) => match coreVarToWeakVar' v with
+                           | OK (WExprVar v') => Some (v',tv,tbody)
+                           | _ => None
+                         end
+        | _  => None
+      end else None
+  | _ => None
+end.
+
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
+match ce with
+  | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+    => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
+      match coreVarToWeakVar' ec with
+        | OK (WTypeVar tv) => match coreVarToWeakVar' v with
+                           | OK (WExprVar v') => Some (v',tv,tbody)
+                           | _ => None
+                         end
+        | _  => None

       end else None
   | _ => None
 end.
 
       end else None
   | _ => None
 end.
 

-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
-  let (t1,t2) := coreCoercionKind cc
-  in  coreTypeToWeakType t1 >>= fun t1' =>
-    coreTypeToWeakType t2 >>= fun t2' =>
-    OK (weakCoercion (kindOfCoreType t1) t1' t2' cc).
+(* 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: " +++ toString wt)
+    | _                => Error ("expectTyConApp encountered " +++ toString wt)
+  end.
+
+(* expects to see an EType with a coercion payload *)
+Definition coreExprToWeakCoercion t1 t2 (ce:@CoreExpr CoreVar) : ???WeakCoercion :=
+  match ce with
+    | CoreEType t => (*OK (coreCoercionToWeakCoercion t)*) OK (WCoUnsafe t1 t2)
+    | _           => Error ("coreExprToWeakCoercion got a " +++ toString ce)
+  end.
+
+(* expects to see an EType *)
+Definition coreExprToWeakType (ce:@CoreExpr CoreVar) : ???WeakType := 
+  match ce with
+    | CoreEType t => coreTypeToWeakType t
+    | _           => Error ("coreExprToWeakType got a " +++ toString ce)
+  end.

 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
     | CoreELit   lit   => OK (WELit lit)
     | CoreENote  n e   => coreExprToWeakExpr e >>= fun e' => OK (WENote n e')
     | CoreEType  t     => Error "encountered CoreEType in a position where an Expr should have been"

+    | CoreECoercion co => Error "encountered CoreECoercion in a position where an Expr should have been"

     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>

-                            coreCoercionToWeakCoercion co >>= fun co' =>
-                              OK (WECast e' co')
+                            let (ct1,ct2) := coercionKind co
+                             in coreTypeToWeakType ct1 >>= fun t1 =>
+                                  coreTypeToWeakType ct2 >>= fun t2 =>
+                                    OK (WECast e' (WCoUnsafe t1 t2))

 
 

-    | CoreEVar   v     => match coreVarToWeakVar v with
+    | CoreEVar   v     => coreVarToWeakVar' v >>= fun v' => match v' with

                             | WExprVar ev => OK (WEVar ev)
                             | WTypeVar _  => Error "found a type variable inside an EVar!"
                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"
                             | WExprVar ev => OK (WEVar ev)
                             | WTypeVar _  => Error "found a type variable inside an EVar!"
                             | WCoerVar _  => Error "found a coercion variable inside an EVar!"

@@ -133,30 +211,42 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
                                                  OK (WEEsc v tv e' t')
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
                                                  OK (WEEsc v tv e' t')

-                                           | None    => coreExprToWeakExpr e1 >>= fun e1' =>
-                                             match e2 with
-                                               | CoreEType t => 
-                                                 coreTypeToWeakType t >>= fun t' =>
-                                                   OK (WETyApp e1' t')
-                                               | _           => coreExprToWeakExpr e2 >>= fun e2' => OK (WEApp e1' e2')
-                                             end
+                                           | None    => match isCSP e1 with
+                                                          | Some (v,tv,t) =>
+                                                            coreExprToWeakExpr e2 >>= fun e' =>
+                                                              coreTypeToWeakType t >>= fun t' =>
+                                                                OK (WECSP v tv e' t')
+                                                          | None    => coreExprToWeakExpr e1 >>= fun e1' =>
+                                                            match e2 with
+                                                              | CoreEType t => 
+                                                                coreTypeToWeakType t >>= fun t' =>
+                                                                  OK (WETyApp e1' t')
+                                                              | _           => coreExprToWeakExpr e2
+                                                                >>= fun e2' => OK (WEApp e1' e2')
+                                                            end
+                                                        end

                                          end
                           end
 
                                          end
                           end
 

-    | CoreELam   v e => match coreVarToWeakVar v with
+    | CoreELam   v e => coreVarToWeakVar' v >>= fun v' => match v' with

                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
                        end
 
                          | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam   ev e')
                          | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e')
                          | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e')
                        end
 

-    | CoreELet   (CoreNonRec v ve) e => match coreVarToWeakVar v with
+    | CoreELet   (CoreNonRec v ve) e => coreVarToWeakVar' v >>= fun v' => match v' with

                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')
                          | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' =>
                                             coreExprToWeakExpr e  >>= fun e'  => OK (WELet ev ve' e')

-                         | WTypeVar _ => match e with
-                                              | CoreEType t => Error "saw a type-let"
+                         | WTypeVar tv => match e with
+                                              | CoreEType t => coreExprToWeakExpr e >>= fun e'  =>
+                                                                 coreExprToWeakType ve >>= fun ty' =>
+                                                                   OK (WETyApp (WETyLam tv e') ty')

                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
                                             end
                                               | _           => Error "saw (ELet <tyvar> e) where e!=EType"
                                             end

-                         | WCoerVar _ => Error "saw an (ELet <coercionVar>)"
+                         | WCoerVar (weakCoerVar cv t1 t2) =>
+                                       coreExprToWeakExpr e  >>= fun e'  =>
+                                           coreExprToWeakCoercion t1 t2 ve >>= fun co' =>
+                                              OK (WECoApp (WECoLam (weakCoerVar cv t1 t2) e') co')

                        end
 
     | CoreELet   (CoreRec rb)      e =>
                        end
 
     | CoreELet   (CoreRec rb)      e =>

@@ -164,7 +254,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         match cel with
           | nil => OK nil
           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
         match cel with
           | nil => OK nil
           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>

-            match coreVarToWeakVar v' with
+            coreVarToWeakVar' v' >>= fun v'' => match v'' with

               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
               | WTypeVar _  => Error "found a type variable in a recursive let"
               | WCoerVar _  => Error "found a coercion variable in a recursive let"
               | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t')
               | WTypeVar _  => Error "found a type variable in a recursive let"
               | WCoerVar _  => Error "found a coercion variable in a recursive let"

@@ -174,30 +264,28 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
       OK (WELetRec (unleaves' rb') e')
 
     | CoreECase  e v tbranches alts => 
       OK (WELetRec (unleaves' rb') e')
 
     | CoreECase  e v tbranches alts => 

-      match coreVarToWeakVar v with
+      coreVarToWeakVar' v >>= fun v' => match v' with

         | WTypeVar _  => Error "found a type variable in a case"
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 
         | WTypeVar _  => Error "found a type variable in a case"
         | WCoerVar _  => Error "found a coercion variable in a case"
         | WExprVar ev => 

-      coreExprToWeakExpr e >>= fun e' =>
-        weakTypeOfWeakExpr e' >>= fun te' =>
-          (match isTyConApp te' nil with None => Error "expectTyConApp encountered strange type" | Some x => OK x end)
-             >>= 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)) :=
+        coreTypeToWeakType (coreTypeOfCoreExpr e) >>= fun te' =>
+          expectTyConApp te' nil >>= fun tca =>
+            let (tc,lt) := tca:(TyCon * list WeakType) in
+          ((fix mkBranches (branches: list (@triple CoreAltCon (list CoreVar) (@CoreExpr CoreVar)))
+                : ???(list (WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=

             match branches with
               | nil => OK nil
               | (mkTriple alt vars e)::rest =>
                   mkBranches rest >>= fun rest' => 
                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with
             match branches with
               | nil => OK nil
               | (mkTriple alt vars e)::rest =>
                   mkBranches rest >>= fun rest' => 
                     coreExprToWeakExpr e >>= fun e' => 
                     match alt with

-                      | DEFAULT                => OK ((DEFAULT,nil,nil,nil,e')::rest')
-                      | LitAlt lit             => OK ((LitAlt lit,nil,nil,nil,e')::rest')
-                      | DataAlt dc             => let vars := map coreVarToWeakVar vars in
-                        OK (((DataAlt dc),
-                        (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)),
-                        (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)),
-                        (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)),
+                      | DEFAULT                => OK ((WeakDEFAULT,nil,nil,nil,e')::rest')
+                      | LitAlt lit             => OK ((WeakLitAlt lit,nil,nil,nil,e')::rest')
+                      | DataAlt dc             => let vars := map coreVarToWeakVar' vars in
+                        OK (((WeakDataAlt dc),
+                        (filter (map (fun x => match x with OK (WTypeVar v) => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with OK (WCoerVar v) => Some v | _ => None end) vars)),
+                        (filter (map (fun x => match x with OK (WExprVar v) => Some v | _ => None end) vars)),

                         e')::rest')
                     end
             end) alts)
                         e')::rest')
                     end
             end) alts)

@@ -207,7 +295,3 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                   OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
       end
   end.
                   OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
       end
   end.

-
-
-
-