Changed WEBrak/WEEsc to store a CoreType

diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs
index 595b8d1..28ea4f1 100644 (file)
--- a/src/Extraction-prefix.hs
+++ b/src/Extraction-prefix.hs
@@ -5,7 +5,6 @@ where
 --import TcType
 --import CoreFVs
 --import CoreUtils
---import MkCore
 --import Var
 --import BasicTypes
 --import Bag
@@ -13,6 +12,7 @@ where
 --import SrcLoc
 --import Data.List
 
+import qualified MkCore
 import qualified TysWiredIn
 import qualified TysPrim
 import qualified Outputable

diff --git a/src/Extraction.v b/src/Extraction.v
index 9e9622b..542b5d4 100644 (file)
--- a/src/Extraction.v
+++ b/src/Extraction.v
@@ -40,7 +40,7 @@ Extract Constant shift => "\ b c -> Data.Char.chr (((Char.code c) `shiftL` 1) .&
 Unset Extraction Optimize.
 Unset Extraction AutoInline.
 
-Definition coqCoreToStringPass (s:CoreExpr CoreVar) : string
+Definition coqCoreToStringPass (s:@CoreExpr CoreVar) : string
    := "FIXME".
 (*
 Definition coqCoreToCorePass (s:CoreExpr CoreVar) : CoreExpr CoreVar

diff --git a/src/HaskCore.v b/src/HaskCore.v
index e9f3929..64699fd 100644 (file)
--- a/src/HaskCore.v
+++ b/src/HaskCore.v
@@ -12,19 +12,19 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 
 (* this type must extract to EXACTLY match TypeRep.Type *)
-Inductive CoreExpr (b:Type) :=
-| CoreEVar   : CoreVar                          -> CoreExpr b
-| CoreELit   : HaskLiteral                      -> CoreExpr b
-| CoreEApp   : CoreExpr b      ->  CoreExpr b   -> CoreExpr b
-| CoreELam   :          b      ->  CoreExpr b   -> CoreExpr b
-| CoreELet   : CoreBind b      ->  CoreExpr b   -> CoreExpr b
-| CoreECase  : CoreExpr b -> b ->  CoreType     -> list (@triple AltCon (list b) (CoreExpr b)) -> CoreExpr b
-| CoreECast  : CoreExpr b      ->  CoreCoercion -> CoreExpr b
-| CoreENote  : Note            ->  CoreExpr b   -> CoreExpr b
-| CoreEType  : CoreType                         -> CoreExpr b
-with      CoreBind (b:Type) :=
-| CoreNonRec : b -> CoreExpr b       -> CoreBind b
-| CoreRec    : list (b * CoreExpr b) -> CoreBind b.
+Inductive CoreExpr {b:Type} :=
+| CoreEVar   : CoreVar                          -> CoreExpr
+| CoreELit   : HaskLiteral                      -> CoreExpr
+| CoreEApp   : CoreExpr        ->  CoreExpr     -> CoreExpr
+| CoreELam   : b               ->  CoreExpr     -> CoreExpr
+| CoreELet   : CoreBind        ->  CoreExpr     -> CoreExpr
+| CoreECase  : CoreExpr   -> b ->  CoreType     -> list (@triple AltCon (list b) CoreExpr) -> CoreExpr
+| CoreECast  : CoreExpr        ->  CoreCoercion -> CoreExpr
+| CoreENote  : Note            ->  CoreExpr     -> CoreExpr
+| CoreEType  : CoreType                         -> CoreExpr
+with      CoreBind {b:Type} :=
+| CoreNonRec : b -> CoreExpr         -> CoreBind  
+| CoreRec    : list (b * CoreExpr  ) -> CoreBind.
 Extract Inductive CoreExpr =>
    "CoreSyn.Expr" [
       "CoreSyn.Var"

diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v
index 061a6e6..c7fb0e9 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,7 +109,7 @@ 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)))
+          ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar)))
                 : ???(list (AltCon*list WeakVar*WeakExpr)) :=
             match branches with
               | nil => OK nil

diff --git a/src/HaskWeak.v b/src/HaskWeak.v
index ff696cc..a9f8bb6 100644 (file)
--- a/src/HaskWeak.v
+++ b/src/HaskWeak.v
@@ -26,8 +26,12 @@ Inductive WeakExpr :=
 | WELam       : WeakExprVar                     -> WeakExpr                  -> WeakExpr
 | WETyLam     : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
 | WECoLam     : WeakCoerVar                     -> WeakExpr                  -> WeakExpr
-| WEBrak      : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
-| WEEsc       : WeakTypeVar                     -> WeakExpr                  -> WeakExpr
+
+(* the CoreType argument is used only when going back from Weak to Core; it lets us dodge a possibly-failing type calculation *)
+| WEBrak      : WeakTypeVar                     -> WeakExpr  -> CoreType     -> WeakExpr
+| WEEsc       : WeakTypeVar                     -> WeakExpr  -> CoreType     -> WeakExpr
+
+(* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *)
 | WECase      : forall (scrutinee:WeakExpr)
                        (tbranches:CoreType)
                        {n:nat}(tc:TyCon n)
@@ -44,8 +48,8 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar :=
     | WENote   n e      =>                            getWeakExprFreeVars e
     | WETyApp  e t      =>                            getWeakExprFreeVars e
     | WECoApp  e co     =>                            getWeakExprFreeVars e
-    | WEBrak   ec e     =>                            getWeakExprFreeVars e
-    | WEEsc    ec e     =>                            getWeakExprFreeVars e
+    | WEBrak   ec e _   =>                            getWeakExprFreeVars e
+    | WEEsc    ec e _   =>                            getWeakExprFreeVars e
     | WELet    cv e1 e2 => mergeDistinctLists        (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2))
     | WEApp    e1 e2    => mergeDistinctLists        (getWeakExprFreeVars e1)                            (getWeakExprFreeVars e2)
     | WELam    cv e     => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e)
@@ -147,9 +151,11 @@ Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType :=
     | WENote  n e                => coreTypeOfWeakExpr e
     | WECast  e (weakCoercion t1 t2 _) => OK t2
     | WECase  scrutinee tbranches n tc type_params alts => OK tbranches
-    | WEBrak  ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+
+    (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
+    | WEBrak  ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
                                                            OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end
-    | WEEsc   ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
+    | WEEsc   ec e _ => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ =>
       match t' with
         | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) =>
           if (tyCon_eq tc hetMetCodeTypeTyCon)