From: Adam Megacz Date: Mon, 7 Mar 2011 13:41:30 +0000 (-0800) Subject: Changed WEBrak/WEEsc to store a CoreType X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=703bff3b209bd7d114b49cb736da8af167a4ec71 Changed WEBrak/WEEsc to store a CoreType --- diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 595b8d1..28ea4f1 100644 --- 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 --- 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 --- 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 --- 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 --- 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)