X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=3555a8a6d473c07650142f10b60e6138084700c0;hb=02af384ece10c5aa927c7d7c1379e9d202926cc8;hp=c7fb0e93270951939ce2cc84eea098722cb6d605;hpb=94c8e7297c8026cb505bb0a8461da4a0b257b48a;p=coq-hetmet.git

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index c7fb0e9..3555a8a 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -110,16 +110,21 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
       match te' with
         | TyConApp _ tc lt =>
           ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
-                : ???(list (AltCon*list WeakVar*WeakExpr)) :=
+                : ???(list (AltCon*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
-                      | DEFAULT                => OK ((DEFAULT,nil,e')::rest')
-                      | LitAlt lit             => OK ((LitAlt lit,nil,e')::rest')
-                      | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest')
+                      | DEFAULT                => OK ((DEFAULT,nil,nil,nil,e')::rest')
+                      | LitAlt lit             => OK ((LitAlt lit,nil,nil,nil,e')::rest')
+                      | DataAlt _ _ _ _ tc' 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)),
+                        e')::rest')
                     end
             end) alts)
           >>= fun branches => coreExprToWeakExpr e