From 02af384ece10c5aa927c7d7c1379e9d202926cc8 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:41:40 -0800 Subject: [PATCH] separate type/coer/expr variables in HaskWeak case branches --- src/HaskCoreToWeak.v | 13 +++++++++---- src/HaskWeak.v | 17 ++++++----------- src/HaskWeakToCore.v | 13 ++++++++++--- src/HaskWeakVars.v | 7 ++++++- 4 files changed, 31 insertions(+), 19 deletions(-) diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index c7fb0e9..3555a8a 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -110,16 +110,21 @@ Fixpoint coreExprToWeakExpr (ce:@CoreExpr CoreVar) : ???WeakExpr := match te' with | TyConApp _ tc lt => ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (@CoreExpr CoreVar))) - : ???(list (AltCon*list WeakVar*WeakExpr)) := + : ???(list (AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match branches with | nil => OK nil | (mkTriple alt vars e)::rest => mkBranches rest >>= fun rest' => coreExprToWeakExpr e >>= fun e' => match alt with - | DEFAULT => OK ((DEFAULT,nil,e')::rest') - | LitAlt lit => OK ((LitAlt lit,nil,e')::rest') - | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest') + | DEFAULT => OK ((DEFAULT,nil,nil,nil,e')::rest') + | LitAlt lit => OK ((LitAlt lit,nil,nil,nil,e')::rest') + | DataAlt _ _ _ _ tc' dc => let vars := map coreVarToWeakVar vars in + OK (((DataAlt _ dc), + (General.filter (map (fun x => match x with WTypeVar v => Some v | _ => None end) vars)), + (General.filter (map (fun x => match x with WCoerVar v => Some v | _ => None end) vars)), + (General.filter (map (fun x => match x with WExprVar v => Some v | _ => None end) vars)), + e')::rest') end end) alts) >>= fun branches => coreExprToWeakExpr e diff --git a/src/HaskWeak.v b/src/HaskWeak.v index a9f8bb6..ee2111c 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -36,7 +36,7 @@ Inductive WeakExpr := (tbranches:CoreType) {n:nat}(tc:TyCon n) (type_params:vec CoreType n) - (alts : Tree ??(AltCon*list WeakVar*WeakExpr)), + (alts : Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)), WeakExpr. (* calculate the free WeakVar's in a WeakExpr *) @@ -59,18 +59,13 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar := (* the messy fixpoints below are required by Coq's termination conditions *) | WECase scrutinee tbranches n tc type_params alts => mergeDistinctLists (getWeakExprFreeVars scrutinee) ( - ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) {struct alts} : list WeakExprVar := + ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) + {struct alts} : list WeakExprVar := match alts with | T_Leaf None => nil - | T_Leaf (Some (DEFAULT,_,e)) => getWeakExprFreeVars e - | T_Leaf (Some (LitAlt lit,_,e)) => getWeakExprFreeVars e - | T_Leaf (Some (DataAlt _ _ _ _ _ dc, vars,e)) => removeFromDistinctList' - (General.filter (map (fun v => match v with - | WExprVar ev => Some ev - | WTypeVar _ => None - | WCoerVar _ => None - end) vars)) - (getWeakExprFreeVars e) + | T_Leaf (Some (DEFAULT,_,_,_,e)) => getWeakExprFreeVars e + | T_Leaf (Some (LitAlt lit,_,_,_,e)) => getWeakExprFreeVars e + | T_Leaf (Some ((DataAlt _ _ _ _ _ dc), tvars, cvars, evars,e)) => removeFromDistinctList' evars (getWeakExprFreeVars e) | T_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2) end) alts)) | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) := diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index 9de00e3..959133d 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -38,6 +38,7 @@ match wv with | WTypeVar (weakTypeVar v _ ) => v | WCoerVar (weakCoerVar v _ _ ) => v end. +Coercion weakVarToCoreVar : WeakVar >-> CoreVar. Section HaskWeakToCore. @@ -66,12 +67,18 @@ Section HaskWeakToCore. | WELet (weakExprVar v _) ve e => mkCoreLet (CoreNonRec v (weakExprToCoreExpr ve)) (weakExprToCoreExpr e) | WECase e tbranches n tc types alts => CoreECase (weakExprToCoreExpr e) dummyVariable tbranches (sortAlts (( - fix mkCaseBranches (alts:Tree ??(AltCon*list WeakVar*WeakExpr)) := + fix mkCaseBranches (alts:Tree + ??(AltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match alts with | T_Leaf None => nil | T_Branch b1 b2 => app (mkCaseBranches b1) (mkCaseBranches b2) - | T_Leaf (Some (ac,lwv,e)) => - (mkTriple ac (map weakVarToCoreVar lwv) (weakExprToCoreExpr e))::nil + | T_Leaf (Some (ac,tvars,cvars,evars,e)) => + (mkTriple ac + (app (app + (map (fun v:WeakTypeVar => weakVarToCoreVar v) tvars) + (map (fun v:WeakCoerVar => weakVarToCoreVar v) cvars)) + (map (fun v:WeakExprVar => weakVarToCoreVar v) evars)) + (weakExprToCoreExpr e))::nil end ) alts)) | WELetRec mlr e => CoreELet (CoreRec diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index c43842f..2e242c8 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -24,13 +24,18 @@ Inductive WeakVar : Type := | WExprVar : WeakExprVar -> WeakVar | WTypeVar : WeakTypeVar -> WeakVar | WCoerVar : WeakCoerVar -> WeakVar. +Coercion WExprVar : WeakExprVar >-> WeakVar. +Coercion WTypeVar : WeakTypeVar >-> WeakVar. +Coercion WCoerVar : WeakCoerVar >-> WeakVar. + Definition haskLiteralToCoreType lit : CoreType := TyConApp (haskLiteralToTyCon lit) nil. Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt. -Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType. +Definition weakTypeToString : CoreType -> string := + coreTypeToString ○ weakTypeToCoreType. (* EqDecidable instances for all of the above *) Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar. -- 1.7.10.4