From 5cfd103cffd56381262b2d280cbba88e0932f78a Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 14 Mar 2011 02:54:02 -0700 Subject: [PATCH] remove weakTypeOfWeakExpr and replaceWeakTypeVar, no longer required --- src/HaskCoreToWeak.v | 4 ++++ src/HaskWeak.v | 43 +++---------------------------------------- src/HaskWeakToCore.v | 1 - src/HaskWeakToStrong.v | 1 + src/HaskWeakTypes.v | 24 ------------------------ 5 files changed, 8 insertions(+), 65 deletions(-) diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index a812483..1734637 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -14,6 +14,7 @@ Require Import HaskCore. Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. +Require Import HaskWeakToCore. Axiom tycons_distinct : ~(ArrowTyCon=ModalBoxTyCon). Variable tyConOrTyFun : CoreTyCon -> sum TyCon TyFun. Extract Inlined Constant tyConOrTyFun => "tyConOrTyFun". @@ -74,6 +75,9 @@ Fixpoint coreTypeToWeakType' (ct:CoreType) : ???WeakType := Variable coreViewDeep : CoreType -> CoreType. Extract Inlined Constant coreViewDeep => "coreViewDeep". Definition coreTypeToWeakType t := coreTypeToWeakType' (coreViewDeep t). +Definition weakTypeOfWeakExpr (we:WeakExpr) : ???WeakType := + coreTypeToWeakType (coreTypeOfCoreExpr (weakExprToCoreExpr we)). + (* detects our crude Core-encoding of modal type introduction/elimination forms *) Definition isBrak (ce:@CoreExpr CoreVar) : ??(CoreVar * WeakTypeVar * CoreType) := match ce with diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 013c62a..8f2a526 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -8,6 +8,7 @@ Require Import General. Require Import Coq.Lists.List. Require Import HaskKinds. Require Import HaskCoreLiterals. +Require Import HaskCore. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCoreTypes. @@ -98,43 +99,5 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr := Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType := (WTyCon (haskLiteralToTyCon lit)). -(* calculate the CoreType of a WeakExpr *) -Fixpoint weakTypeOfWeakExpr (ce:WeakExpr) : ???WeakType := - match ce with - | WEVar (weakExprVar v t) => OK t - | WELit lit => OK (weakTypeOfLiteral lit) - | WEApp e1 e2 => weakTypeOfWeakExpr e1 >>= fun t' => - match t' with - | (WAppTy (WAppTy WFunTyCon t1) t2) => OK t2 - | _ => Error ("found non-function type "+++t'+++" in EApp") - end - | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => - match te with - | WForAllTy v ct => OK (replaceWeakTypeVar ct v t) - | _ => Error ("found non-forall type "+++te+++" in ETyApp") - end - | WECoApp e co => weakTypeOfWeakExpr e >>= fun te => - match te with - | WCoFunTy t1 t2 t => OK t - | _ => Error ("found non-coercion type "+++te+++" in ETyApp") - end - | WELam (weakExprVar ev vt) e => weakTypeOfWeakExpr e >>= fun t' => OK (WAppTy (WAppTy WFunTyCon vt) t') - | WETyLam tv e => weakTypeOfWeakExpr e >>= fun t' => OK (WForAllTy tv t') - | WECoLam (weakCoerVar cv _ φ₁ φ₂) e => weakTypeOfWeakExpr e >>= fun t' => OK (WCoFunTy φ₁ φ₂ t') - | WELet ev ve e => weakTypeOfWeakExpr e - | WELetRec rb e => weakTypeOfWeakExpr e - | WENote n e => weakTypeOfWeakExpr e - | WECast e (weakCoercion _ t1 t2 _) => OK t2 - | 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') - | WEEsc _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => - match t' with - | (WAppTy (WAppTy WCodeTyCon (WTyVarTy ec')) t'') => - if eqd_dec ec ec' then OK t'' - else Error "level mismatch in escapification" - | _ => Error "ill-typed escapification" - end - end. - +Variable coreTypeOfCoreExpr : @CoreExpr CoreVar -> CoreType. + Extract Inlined Constant coreTypeOfCoreExpr => "CoreUtils.exprType". diff --git a/src/HaskWeakToCore.v b/src/HaskWeakToCore.v index cb3d7a3..7d0fac4 100644 --- a/src/HaskWeakToCore.v +++ b/src/HaskWeakToCore.v @@ -15,7 +15,6 @@ Require Import HaskCore. Require Import HaskWeakVars. Require Import HaskWeakTypes. Require Import HaskWeak. -Require Import HaskCoreToWeak. Variable mkCoreLet : @CoreBind CoreVar -> @CoreExpr CoreVar -> @CoreExpr CoreVar. Extract Inlined Constant mkCoreLet => "MkCore.mkCoreLet". diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index a15b81d..3d8137f 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -18,6 +18,7 @@ Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskCoreTypes. Require Import HaskCoreVars. +Require Import HaskCoreToWeak. Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, HaskTyVar Γ wt. diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index 6b6b61e..593bccf 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -67,30 +67,6 @@ Fixpoint isTyConApp (wt:WeakType)(acc:list WeakType) : ??(TyCon * list WeakType) | _ => None end. -(* messy first-order NON-CAPTURE-AVOIDING substitution on WeakType's *) -Fixpoint replaceWeakTypeVar (te:WeakType)(tv:WeakTypeVar)(tsubst:WeakType) : WeakType := - match te with - | WTyVarTy tv' => if eqd_dec tv tv' then tsubst else te - | WAppTy t1 t2 => WAppTy (replaceWeakTypeVar t1 tv tsubst) (replaceWeakTypeVar t2 tv tsubst) - | WForAllTy tv' t => if eqd_dec tv tv' then te else WForAllTy tv' (replaceWeakTypeVar t tv tsubst) - | WCoFunTy t1 t2 t => WCoFunTy (replaceWeakTypeVar t1 tv tsubst) - (replaceWeakTypeVar t2 tv tsubst) (replaceWeakTypeVar t tv tsubst) - | WIParam ip ty => WIParam ip (replaceWeakTypeVar ty tv tsubst) - | WClassP c lt => WClassP c ((fix replaceCoreDistinctList (lt:list WeakType) := - match lt with - | nil => nil - | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t) - end) lt) - | WTyFunApp tc lt => WTyFunApp tc ((fix replaceCoreDistinctList (lt:list WeakType) := - match lt with - | nil => nil - | h::t => (replaceWeakTypeVar h tv tsubst)::(replaceCoreDistinctList t) - end) lt) - | WTyCon tc => WTyCon tc - | WFunTyCon => WFunTyCon - | WModalBoxTyCon => WModalBoxTyCon - end. - (* we try to normalize the representation of a type as much as possible before feeding it back to GHCs type-comparison function *) Definition normalizeWeakType (wt:WeakType) : WeakType := wt. -- 1.7.10.4