separate type/coer/expr variables in HaskWeak case branches

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

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 061a6e6..3555a8a 100644 (file)
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -17,24 +17,24 @@ Require Import HaskWeak.
 Variable coreVarToWeakVar      : CoreVar  -> WeakVar.   Extract Inlined Constant coreVarToWeakVar    => "coreVarToWeakVar".
 
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_brak_name (coreVarCoreName v) then
       match coreVarToWeakVar v with
         | WExprVar _  => None
-        | WTypeVar tv => Some tv
+        | WTypeVar tv => Some (tv,tbody)
         | WCoerVar _  => None
       end else None
   | _ => None
 end.
-Definition isEsc (ce:CoreExpr CoreVar) : ??WeakTypeVar :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
 match ce with
   | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
     => if coreName_eq hetmet_esc_name (coreVarCoreName v) then
       match coreVarToWeakVar v with
         | WExprVar _  => None
-        | WTypeVar tv => Some tv
+        | WTypeVar tv => Some (tv,tbody)
         | WCoerVar _  => None
       end else None
   | _ => None
@@ -44,7 +44,7 @@ Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion :=
   let (t1,t2) := coreCoercionKind cc
   in  weakCoercion t1 t2 cc.
 
-Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
+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')
@@ -59,9 +59,9 @@ Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
                           end
 
     | CoreEApp   e1 e2 => match isBrak e1 with
-                            | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e')
+                            | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEBrak tv e' t)
                             | None    => match isEsc e1 with
-                                           | Some tv => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e')
+                                           | Some (tv,t) => coreExprToWeakExpr e2 >>= fun e' => OK (WEEsc tv e' t)
                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
                                              match e2 with
                                                | CoreEType t => OK (WETyApp e1' t)
@@ -87,7 +87,7 @@ Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
                        end
 
     | CoreELet   (CoreRec rb)      e =>
-      ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
+      ((fix coreExprToWeakExprList (cel:list (CoreVar * (@CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) :=
         match cel with
           | nil => OK nil
           | (v',e')::t => coreExprToWeakExprList t >>= fun t' =>
@@ -109,17 +109,22 @@ Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr :=
       >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' =>
       match te' with
         | TyConApp _ tc lt =>
-          ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar)))
-                : ???(list (AltCon*list WeakVar*WeakExpr)) :=
+          ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
+                : ???(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