From ee5aaad57d76400e9b8736d4a12d2804f99f329c Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 02:44:09 -0700 Subject: [PATCH] store the scrutinee CoreVar in WeakExpr Case to simplify WeakExprToCoreExpr --- src/HaskCoreToWeak.v | 5 ++++- src/HaskStrongToWeak.v | 1 + src/HaskWeak.v | 6 +++--- src/HaskWeakToCore.v | 45 ++++++++++++++++++++------------------------- src/HaskWeakToStrong.v | 15 +++++++++------ 5 files changed, 37 insertions(+), 35 deletions(-) diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 6fc5b43..a812483 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -200,7 +200,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. + + + diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index ea76856..7fcea20 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -98,6 +98,7 @@ match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTyp | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => fun ite => WECoApp (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) | ECase Γ Δ ξ l tc tbranches atypes e alts => fun ite => WECase + FIXME (strongExprToWeakExpr ftv fcv e ite) (@typeToWeakType ftv Γ _ tbranches ite) tc diff --git a/src/HaskWeak.v b/src/HaskWeak.v index e5a2bfb..013c62a 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -35,8 +35,8 @@ Inductive WeakExpr := | 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) +| WECase : forall (vscrut:WeakExprVar) + (scrutinee:WeakExpr) (tbranches:WeakType) (tc:TyCon) (type_params:list WeakType) @@ -125,7 +125,7 @@ Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType := | WELetRec rb e => weakTypeOfWeakExpr e | WENote n e => weakTypeOfWeakExpr e | WECast e (weakCoercion _ t1 t2 _) => OK t2 - | WECase scrutinee tbranches tc type_params alts => OK tbranches + | WECase vscrut 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') diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 24eedc6..cb3d7a3 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -31,43 +31,38 @@ Variable trustMeCoercion : CoreCoercion. Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". -Section HaskWeakToCore. +Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := + fun _ => trustMeCoercion. - (* the CoreVar for the "magic" bracket/escape identifiers must be created from within one of the monads *) - Context (hetmet_brak_var : CoreVar). - Context (hetmet_esc_var : CoreVar). - Definition weakCoercionToCoreCoercion : WeakCoercion -> CoreCoercion := - fun _ => trustMeCoercion. - - Fixpoint weakExprToCoreExpr (f:Fresh unit (fun _ => WeakExprVar)) (me:WeakExpr) : @CoreExpr CoreVar := + Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := match me with | WEVar (weakExprVar v _) => CoreEVar v | WELit lit => CoreELit lit - | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr f e1) (weakExprToCoreExpr f e2) - | WETyApp e t => CoreEApp (weakExprToCoreExpr f e ) (CoreEType (weakTypeToCoreType t)) - | WECoApp e co => CoreEApp (weakExprToCoreExpr f e ) + | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) + | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType (weakTypeToCoreType t)) + | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) (CoreEType (coreCoercionsAreReallyTypes (weakCoercionToCoreCoercion co))) - | WENote n e => CoreENote n (weakExprToCoreExpr f e ) - | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr f e ) - | 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) + | WENote n e => CoreENote n (weakExprToCoreExpr e ) + | WELam (weakExprVar ev _ ) e => CoreELam ev (weakExprToCoreExpr e ) + | WETyLam (weakTypeVar tv _ ) e => CoreELam tv (weakExprToCoreExpr e ) + | WECoLam (weakCoerVar cv _ _ _) e => CoreELam cv (weakExprToCoreExpr e ) + | WECast e co => CoreECast (weakExprToCoreExpr e ) (weakCoercionToCoreCoercion co) | WEBrak v (weakTypeVar ec _) e t => fold_left CoreEApp ((CoreEType (TyVarTy ec)):: (CoreEType (weakTypeToCoreType t)):: - (weakExprToCoreExpr f e):: + (weakExprToCoreExpr e):: nil) (CoreEVar v) | WEEsc v (weakTypeVar ec _) e t => fold_left CoreEApp ((CoreEType (TyVarTy ec)):: (CoreEType (weakTypeToCoreType t)):: - (weakExprToCoreExpr f e):: + (weakExprToCoreExpr 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) + | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e) + | WECase vscrut e tbranches tc types alts => + CoreECase (weakExprToCoreExpr e) vscrut (weakTypeToCoreType tbranches) (sortAlts (( fix mkCaseBranches (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := @@ -80,19 +75,19 @@ Section HaskWeakToCore. (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) (map (fun v:WeakExprVar => weakVarToCoreVar v) evars)) - (weakExprToCoreExpr f' e))::nil + (weakExprToCoreExpr e))::nil end ) alts)) | WELetRec mlr e => CoreELet (CoreRec ((fix mkLetBindings (mlr:Tree ??(WeakExprVar * WeakExpr)) := match mlr with | T_Leaf None => nil - | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr f e))::nil + | T_Leaf (Some (weakExprVar cv _,e)) => (cv,(weakExprToCoreExpr e))::nil | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2) end) mlr)) - (weakExprToCoreExpr f e) + (weakExprToCoreExpr e) end. -End HaskWeakToCore. + diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index cd4b17b..a15b81d 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -558,16 +558,16 @@ Definition weakExprToStrongExpr : forall weakExprToStrongExpr Γ Δ φ ψ ξ' τ lev e >>= fun e' => OK (ELetRec Γ Δ ξ lev τ _ binds' e') - | WECase e tbranches tc avars alts => + | WECase vscrut e tbranches tc avars alts => mkAvars avars (tyConKind tc) φ >>= fun avars' => weakTypeToType'' φ tbranches ★ >>= fun tbranches' => - weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' => + let ξ' := update_ξ ξ (((vscrut:CoreVar), _ @@lev)::nil) in (fix mkTree (t:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' & Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) (weakLT' (tbranches' @@ lev))}) := + (scbwv_ξ scb ξ' lev) (weakLT' (tbranches' @@ lev))}) := match t with | T_Leaf None => OK [] | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => @@ -575,7 +575,7 @@ Definition weakExprToStrongExpr : forall list2vecOrFail (map (fun ev:WeakExprVar => ev:CoreVar) exprvars) _ (fun _ _ => "WECase") >>= fun exprvars' => let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' in weakExprToStrongExpr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ) - (scbwv_ξ scb ξ lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => + (scbwv_ξ scb ξ' lev) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => let case_case := tt in OK [ _ ] | T_Branch b1 b2 => mkTree b1 >>= fun b1' => @@ -583,7 +583,10 @@ Definition weakExprToStrongExpr : forall OK (b1',,b2') end ) alts >>= fun tree => - castExpr "ECase" _ (ECase Γ Δ ξ lev tc tbranches' avars' e' tree) + weakExprToStrongExpr Γ Δ φ ψ ξ (caseType tc avars') lev e >>= fun e' => + castExpr "ECaseScrut" _ (EVar Γ Δ ξ' vscrut) >>= fun evar => + castExpr "ECase" _ (ECase Γ Δ ξ' lev tc tbranches' avars' evar tree) >>= fun ecase' => + OK (ELet _ _ _ _ _ lev (vscrut:CoreVar) e' ecase') end)). destruct case_some. @@ -600,7 +603,7 @@ Definition weakExprToStrongExpr : forall apply e1. destruct case_case. - clear mkTree t o e' p e p0 p1 p2 alts weakExprToStrongExpr ebranch. + clear mkTree t o p e p0 p1 p2 alts weakExprToStrongExpr ebranch. exists scb. apply ebranch'. Defined. -- 1.7.10.4