From a9bbdf55d01ad494d42018c0eaa252da1d7b5d97 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:41:35 -0800 Subject: [PATCH] add HaskWeakToCore --- src/HaskWeakToCore.v | 87 ++++++++++++++++++++++++++++++++++++++++++++++++++ src/Main.v | 5 ++- 2 files changed, 91 insertions(+), 1 deletion(-) create mode 100644 src/HaskWeakToCore.v diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v new file mode 100644 index 0000000..9de00e3 --- /dev/null +++ b/src/HaskWeakToCore.v @@ -0,0 +1,87 @@ +(*********************************************************************************************************************************) +(* HaskWeakToCore: convert HaskWeak to HaskCore *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Require Import HaskGeneral. +Require Import HaskLiterals. +Require Import HaskCoreVars. +Require Import HaskCoreTypes. +Require Import HaskCore. +Require Import HaskWeakVars. +Require Import HaskWeak. + +Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar. + Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet". + +Variable sortAlts : forall {a}{b}, list (@triple AltCon a b) -> list (@triple AltCon a b). + Extract Inlined Constant mkCoreLet => "sortAlts". + Implicit Arguments sortAlts [[a][b]]. + +Variable unsafeCoerce : CoreCoercion. + Extract Inlined Constant unsafeCoerce => "Coercion.unsafeCoerce". + +(* Coercion and Type are actually the same thing in GHC, but we don't tell Coq about that. This lets us get around it. *) +Variable coreCoercionsAreReallyTypes : CoreCoercion -> CoreType. + Extract Inlined Constant coreCoercionsAreReallyTypes => "(\x -> x)". + +(* a dummy variable which is never referenced but needed for a binder *) +Variable dummyVariable : CoreVar. + +Definition weakVarToCoreVar (wv:WeakVar) : CoreVar := +match wv with +| WExprVar (weakExprVar v _ ) => v +| WTypeVar (weakTypeVar v _ ) => v +| WCoerVar (weakCoerVar v _ _ ) => v +end. + +Section HaskWeakToCore. + + (* 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 _ => unsafeCoerce. + + Fixpoint weakExprToCoreExpr (me:WeakExpr) : @CoreExpr CoreVar := + match me with + | WEVar (weakExprVar v _) => CoreEVar v + | WELit lit => CoreELit lit + | WEApp e1 e2 => CoreEApp (weakExprToCoreExpr e1) (weakExprToCoreExpr e2) + | WETyApp e t => CoreEApp (weakExprToCoreExpr e ) (CoreEType t) + | WECoApp e co => CoreEApp (weakExprToCoreExpr e ) + (CoreEType (coreCoercionsAreReallyTypes (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 (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_brak_var) (CoreEType (TyVarTy ec))) (CoreEType t) + | WEEsc (weakTypeVar ec _) e t => CoreEApp (CoreEApp (CoreEVar hetmet_esc_var) (CoreEType (TyVarTy ec))) (CoreEType t) + | 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)) := + 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 + 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 e))::nil + | T_Branch b1 b2 => app (mkLetBindings b1) (mkLetBindings b2) + end) mlr)) + (weakExprToCoreExpr e) + end. + +End HaskWeakToCore. \ No newline at end of file diff --git a/src/Main.v b/src/Main.v index 9188e5d..bbadc14 100644 --- a/src/Main.v +++ b/src/Main.v @@ -14,7 +14,10 @@ Require Import HaskWeak. Require Import HaskCoreToWeak. Require Import HaskStrongTypes. Require Import HaskStrong. -(*Require Import HaskStrongToProof.*) Require Import HaskProof. +(*Require Import HaskProofToStrong.*) +(*Require Import HaskStrongToProof.*) +(*Require Import HaskStrongToWeak.*) (*Require Import HaskWeakToStrong.*) +Require Import HaskWeakToCore. Require Import HaskProofToLatex. -- 1.7.10.4