From 26733c04106397dc8a10396ce688e908e8d0cde7 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 02:25:55 -0700 Subject: [PATCH] store the magic CoreVar for hetmet brak/esc in WeakExpr Esc/Brak --- src/HaskCoreToWeak.v | 20 ++++++++++---------- src/HaskStrongToWeak.v | 11 +++++++++-- src/HaskWeak.v | 15 ++++++++------- src/HaskWeakToCore.v | 16 ++++++++++++---- src/HaskWeakToStrong.v | 4 ++-- 5 files changed, 41 insertions(+), 25 deletions(-) diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index b538417..6fc5b43 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -75,24 +75,24 @@ 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 @@ -120,15 +120,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 => diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index a7f6b77..ea76856 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -72,6 +72,12 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH} Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) := tv::::ite. +Section strongExprToWeakExpr. + + Context (hetmet_brak : CoreVar). + Context (hetmet_esc : CoreVar). +Axiom FIXME : forall {t}, t. + Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ} (ftv:Fresh Kind (fun _ => WeakTypeVar)) (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) @@ -83,8 +89,8 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) | ELam Γ' _ _ _ t _ cv e => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite) | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) -| EEsc Γ' _ _ ec t _ e => fun ite => WEEsc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) -| EBrak Γ' _ _ ec t _ e => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) +| EEsc Γ' _ _ ec t _ e => fun ite => WEEsc hetmet_esc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) +| EBrak Γ' _ _ ec t _ e => fun ite => WEBrak hetmet_brak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) | ENote _ _ _ _ n e => fun ite => WENote n (strongExprToWeakExpr ftv fcv e ite) | ETyApp Γ Δ κ σ τ ξ l e => fun ite => WETyApp (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv τ ite) @@ -137,3 +143,4 @@ match elrb as E in ELetRecBindings G D X L V | ELR_leaf _ _ ξ' cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv (unlev (ξ' v)) ite)),(strongExprToWeakExpr ftv fcv e ite))] | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite) end. +End strongExprToWeakExpr. \ No newline at end of file diff --git a/src/HaskWeak.v b/src/HaskWeak.v index f177e1f..e5a2bfb 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -28,11 +28,12 @@ Inductive WeakExpr := | WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr | WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr -(* the WeakType argument in WEBrak/WEEsc is used only when going back *) -(* from Weak to Core; it lets us dodge a possibly-failing type *) -(* calculation *) -| WEBrak : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr -| WEEsc : WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr +(* The WeakType argument in WEBrak/WEEsc is used only when going back *) +(* from Weak to Core; it lets us dodge a possibly-failing type *) +(* calculation. The CoreVar argument is the GlobalVar for the hetmet_brak *) +(* or hetmet_esc identifier *) +| WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr +| WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr (* note that HaskWeak "Case" does not bind a variable; coreExprToWeakExpr adds a let-binder *) | WECase : forall (scrutinee:WeakExpr) @@ -127,8 +128,8 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType := | WECase scrutinee tbranches tc type_params alts => OK tbranches (* note that we willfully ignore the type stashed in WEBrak/WEEsc here *) - | WEBrak ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t') - | WEEsc ec e _ => weakTypeOfWeakExpr e >>= fun t' => + | WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t') + | WEEsc _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => match t' with | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') => if eqd_dec ec ec' then OK t'' diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index cfaf65e..24eedc6 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -53,10 +53,18 @@ Section HaskWeakToCore. | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr f e ) | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr f e ) | WECast e co => CoreECast (weakExprToCoreExpr f e ) (weakCoercionToCoreCoercion co) - | WEBrak (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var) - (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t)) - | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) - (CoreEType (TyVarTy ec))) (CoreEType (weakTypeToCoreType t)) + | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp + ((CoreEType (TyVarTy ec)):: + (CoreEType (weakTypeToCoreType t)):: + (weakExprToCoreExpr f e):: + nil) + (CoreEVar v) + | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp + ((CoreEType (TyVarTy ec)):: + (CoreEType (weakTypeToCoreType t)):: + (weakExprToCoreExpr f e):: + nil) + (CoreEVar v) | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr f ve)) (weakExprToCoreExpr f e) | WECase e tbranches tc types alts => let (v,f') := next _ _ f tt in CoreECase (weakExprToCoreExpr f' e) v (weakTypeToCoreType tbranches) diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 3317445..cd4b17b 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -465,10 +465,10 @@ Definition weakExprToStrongExpr : forall τ' _ e >>= fun e' => castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e') - | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => + | WEBrak _ ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => castExpr "WEBrak" _ (EBrak _ _ _ (φ (`ec)) _ lev e') - | WEEsc ec e tbody => weakTypeToType'' φ tbody ★ >>= fun tbody' => + | WEEsc _ ec e tbody => weakTypeToType'' φ tbody ★ >>= fun tbody' => match lev with | nil => Error "ill-leveled escapification" | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ (<[ φ (`ec) |- tbody' ]>) lev e -- 1.7.10.4