X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=src%2FHaskCoreToWeak.v;h=1cbaf228293a9bb6c296ce7efc69523ecf3a2292;hb=4fec54f1f2cdb072d03928f94f1d45f58755bc13;hp=644d04d8e70f629c235f28f053c0abcd2dc2b8f1;hpb=8c26722a1ee110077968a8a166eb7130266b2035;p=coq-hetmet.git

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 644d04d..1cbaf22 100644
--- a/src/HaskCoreToWeak.v
+++ b/src/HaskCoreToWeak.v
@@ -43,7 +43,7 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType :=
                                     | WExprVar _  => Error "encountered expression variable in a modal box type"
                                     | WCoerVar _  => Error "encountered coercion variable in a modal box type"
                                   end
-                                | _                           => Error "mis-applied modal box tycon"
+                                | _                           => Error ("mis-applied modal box tycon: " +++ ct)
                               end
                          else let tc' := if eqd_dec tc ArrowTyCon
                                          then WFunTyCon
@@ -75,34 +75,37 @@ Variable coreViewDeep : CoreType -> CoreType.  Extract Inlined Constant coreView
 Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t).
 
 (* 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
 end.
 
-Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : ???WeakCoercion :=
+Variable coreCoercionToWeakCoercion : CoreCoercion -> WeakCoercion.
+  Extract Inlined Constant coreCoercionToWeakCoercion => "coreCoercionToWeakCoercion".
+(*
   let (t1,t2) := coreCoercionKind cc
   in  coreTypeToWeakType t1 >>= fun t1' =>
-    coreTypeToWeakType t2 >>= fun t2' =>
-    OK (weakCoercion t1' t2' cc).
+        coreTypeToWeakType t2 >>= fun t2' =>
+          OK (WCoUnsafe t1' t2').
+*)
 
 Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
   match ce with
@@ -110,8 +113,7 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
     | 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"
     | CoreECast  e co  => coreExprToWeakExpr e >>= fun e' =>
-                            coreCoercionToWeakCoercion co >>= fun co' =>
-                              OK (WECast e' co')
+                              OK (WECast e' (coreCoercionToWeakCoercion co))
 
     | CoreEVar   v     => match coreVarToWeakVar v with
                             | WExprVar ev => OK (WEVar ev)
@@ -120,15 +122,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 => 
@@ -174,8 +176,8 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr :=
         | 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' =>
+        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 =>
             let (tc,lt) := tca in
@@ -200,7 +202,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.
 
+
+
+