X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=17346378feaca1ace6c65c926756da5048253a47;hb=0126c02cc846952aa847660475e88a152c9a2574;hp=b538417f84e5c0b0f67422c941ef4fa046b884a0;hpb=1f411b48dd607e76a65903e8506d0ae5e7470321;p=coq-hetmet.git

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index b538417..1734637 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -14,6 +14,7 @@ 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".
@@ -74,25 +75,28 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
 Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreViewDeep => "coreViewDeep".
 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
 
+Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType :=
+  coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)).
+
 (* detects our crude Core-encoding of modal type introduction/elimination forms *)
-Definition isBrak (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+Definition isBrak (ce:@CoreExpr CoreVar) : ??(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
+      match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (tv,tbody)
+        | WTypeVar tv => Some (v,tv,tbody)
         | WCoerVar _  => None
       end else None
   | _ => None
 end.
-Definition isEsc (ce:@CoreExpr CoreVar) : ??(WeakTypeVar * CoreType) :=
+Definition isEsc (ce:@CoreExpr CoreVar) : ??(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
+      match coreVarToWeakVar ec with
         | WExprVar _  => None
-        | WTypeVar tv => Some (tv,tbody)
+        | WTypeVar tv => Some (v,tv,tbody)
         | WCoerVar _  => None
       end else None
   | _ => None
@@ -120,15 +124,15 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
                           end
 
     | CoreEApp   e1 e2 => match isBrak e1 with
-                            | Some (tv,t) =>
+                            | Some (v,tv,t) =>
                               coreExprToWeakExpr e2 >>= fun e' =>
                                 coreTypeToWeakType t >>= fun t' =>
-                                OK (WEBrak tv e' t')
+                                OK (WEBrak v tv e' t')
                             | None    => match isEsc e1 with
-                                           | Some (tv,t) =>
+                                           | Some (v,tv,t) =>
                                              coreExprToWeakExpr e2 >>= fun e' =>
                                                coreTypeToWeakType t >>= fun t' =>
-                                                 OK (WEEsc tv e' t')
+                                                 OK (WEEsc v tv e' t')
                                            | None    => coreExprToWeakExpr e1 >>= fun e1' =>
                                              match e2 with
                                                | CoreEType t => 
@@ -200,7 +204,10 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
           >>= fun branches =>
             coreExprToWeakExpr e >>= fun scrutinee =>
               coreTypeToWeakType tbranches >>= fun tbranches' =>
-                  OK (WELet ev scrutinee (WECase (WEVar ev) tbranches' tc lt (unleaves branches)))
+                  OK (WECase ev scrutinee tbranches' tc lt (unleaves branches))
       end
   end.
 
+
+
+