From 5a0761840d89b82cdacb0bf9215fd41aba847b68 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 7 Mar 2011 05:41:27 -0800 Subject: [PATCH] Added WeakVar, a separate variable representation for HaskWeak --- src/Extraction-prefix.hs | 5 +- src/General.v | 1 - src/HaskCore.v | 17 ------- src/HaskCoreToWeak.v | 85 +++++++++++++++++++++++---------- src/HaskCoreTypes.v | 22 ++++----- src/HaskCoreVars.v | 2 +- src/HaskGeneral.v | 27 ++++++----- src/HaskStrongTypes.v | 34 -------------- src/HaskWeak.v | 117 ++++++++++++++++++++++------------------------ src/HaskWeakVars.v | 88 ++++++++++++++++++++++++++++++++++ src/Main.v | 1 + 11 files changed, 233 insertions(+), 166 deletions(-) create mode 100644 src/HaskWeakVars.v diff --git a/src/Extraction-prefix.hs b/src/Extraction-prefix.hs index 68c40e5..595b8d1 100644 --- a/src/Extraction-prefix.hs +++ b/src/Extraction-prefix.hs @@ -36,7 +36,8 @@ import qualified Data.Char import Data.Bits ((.&.), shiftL, (.|.)) import Prelude ( (++), (+), (==), Show, show, Char ) -{- +dataConEqTheta' dc = map (\p -> {-FIXME-}) (DataCon.dataConEqTheta dc) + nat2int :: Nat -> Prelude.Int nat2int O = 0 nat2int (S x) = 1 + (nat2int x) @@ -74,4 +75,4 @@ coreVarSort v | otherwise = Prelude.error "Var.Var that is neither an expres outputableToString :: Outputable -> String outputableToString = (\x -> Outputable.showSDoc (Outputable.ppr x)) --} + diff --git a/src/General.v b/src/General.v index ad8e590..c78daa1 100644 --- a/src/General.v +++ b/src/General.v @@ -17,7 +17,6 @@ Require Import Omega. Class EqDecidable (T:Type) := { eqd_type := T ; eqd_dec : forall v1 v2:T, sumbool (v1=v2) (not (v1=v2)) -; eqd_dec_reflexive : forall v, (eqd_dec v v) = (left _ (refl_equal _)) }. Coercion eqd_type : EqDecidable >-> Sortclass. diff --git a/src/HaskCore.v b/src/HaskCore.v index 2242e48..e9f3929 100644 --- a/src/HaskCore.v +++ b/src/HaskCore.v @@ -42,9 +42,6 @@ Extract Inductive CoreBind => (* extracts the Name from a CoreVar *) Variable coreVarCoreName : CoreVar -> CoreName. Extract Inlined Constant coreVarCoreName => "Var.varName". -Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)). - Extract Inlined Constant coretype_eq_dec => "Type.coreEqType". - Extract Constant ArrowTyCon => "Type.funTyCon". (* Figure 7, (->) *) Extract Constant CoFunConst => "TyCon.TyCon". Extraction Implicit CoFunConst [ 1 ]. Extract Constant TyFunConst => "TyCon.TyCon". Extraction Implicit TyFunConst [ 1 ]. @@ -59,18 +56,4 @@ Variable hetmet_brak_name : CoreName. Extract Inlined Constant he (* the magic wired-in name for the modal type elimination form *) Variable hetmet_esc_name : CoreName. Extract Inlined Constant hetmet_esc_name => "PrelNames.hetmet_esc_name". -(* detects our crude Core-encoding of modal type introduction/elimination forms *) -Definition isBrak (ce:CoreExpr CoreVar) : ??CoreVar := -match ce with - | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) - => if coreName_eq hetmet_brak_name (coreVarCoreName v) then Some ec else None - | _ => None -end. -Definition isEsc (ce:CoreExpr CoreVar) : ??CoreVar := -match ce with - | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody)) - => if coreName_eq hetmet_esc_name (coreVarCoreName v) then Some ec else None - | _ => None -end. - diff --git a/src/HaskCoreToWeak.v b/src/HaskCoreToWeak.v index 1b3ffcf..061a6e6 100644 --- a/src/HaskCoreToWeak.v +++ b/src/HaskCoreToWeak.v @@ -5,24 +5,57 @@ Generalizable All Variables. Require Import Preamble. Require Import General. +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 coreVarToWeakVar : CoreVar -> WeakVar. Extract Inlined Constant coreVarToWeakVar => "coreVarToWeakVar". + +(* detects our crude Core-encoding of modal type introduction/elimination forms *) +Definition isBrak (ce:CoreExpr CoreVar) : ??WeakTypeVar := +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 + | WExprVar _ => None + | WTypeVar tv => Some tv + | WCoerVar _ => None + end else None + | _ => None +end. +Definition isEsc (ce:CoreExpr CoreVar) : ??WeakTypeVar := +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 + | WExprVar _ => None + | WTypeVar tv => Some tv + | WCoerVar _ => None + end else None + | _ => None +end. + +Definition coreCoercionToWeakCoercion (cc:CoreCoercion) : WeakCoercion := + let (t1,t2) := coreCoercionKind cc + in weakCoercion t1 t2 cc. + Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr := match ce with | CoreELit lit => OK (WELit lit) | CoreENote n e => coreExprToWeakExpr e >>= fun e' => OK (WENote n e') | CoreEType t => Error "encountered CoreEType in a position where an Expr should have been" - | CoreECast e co => coreExprToWeakExpr e >>= fun e' => OK (WECast e' co) + | CoreECast e co => coreExprToWeakExpr e >>= fun e' => + OK (WECast e' (coreCoercionToWeakCoercion co)) - | CoreEVar v => match coreVarSort v with - | CoreExprVar _ => OK (WEVar v) - | CoreTypeVar _ => Error "found a type variable inside an EVar!" - | CoreCoerVar _ => Error "found a coercion variable inside an EVar!" + | CoreEVar v => match coreVarToWeakVar v with + | WExprVar ev => OK (WEVar ev) + | WTypeVar _ => Error "found a type variable inside an EVar!" + | WCoerVar _ => Error "found a coercion variable inside an EVar!" end | CoreEApp e1 e2 => match isBrak e1 with @@ -37,60 +70,64 @@ Fixpoint coreExprToWeakExpr (ce:CoreExpr CoreVar) : ???WeakExpr := end end - | CoreELam v e => match coreVarSort v with - | CoreExprVar _ => coreExprToWeakExpr e >>= fun e' => OK (WELam v e') - | CoreTypeVar _ => coreExprToWeakExpr e >>= fun e' => OK (WETyLam v e') - | CoreCoerVar _ => coreExprToWeakExpr e >>= fun e' => OK (WECoLam v e') + | CoreELam v e => match coreVarToWeakVar v with + | WExprVar ev => coreExprToWeakExpr e >>= fun e' => OK (WELam ev e') + | WTypeVar tv => coreExprToWeakExpr e >>= fun e' => OK (WETyLam tv e') + | WCoerVar cv => coreExprToWeakExpr e >>= fun e' => OK (WECoLam cv e') end - | CoreELet (CoreNonRec v ve) e => match coreVarSort v with - | CoreExprVar _ => coreExprToWeakExpr ve >>= fun ve' => - coreExprToWeakExpr e >>= fun e' => OK (WELet v ve' e') - | CoreTypeVar _ => match e with + | CoreELet (CoreNonRec v ve) e => match coreVarToWeakVar v with + | WExprVar ev => coreExprToWeakExpr ve >>= fun ve' => + coreExprToWeakExpr e >>= fun e' => OK (WELet ev ve' e') + | WTypeVar _ => match e with | CoreEType t => Error "saw a type-let" | _ => Error "saw (ELet e) where e!=EType" end - | CoreCoerVar _ => Error "saw an (ELet )" + | WCoerVar _ => Error "saw an (ELet )" end | CoreELet (CoreRec rb) e => - ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (CoreVar * WeakExpr)) := + ((fix coreExprToWeakExprList (cel:list (CoreVar * (CoreExpr CoreVar))) : ???(list (WeakExprVar * WeakExpr)) := match cel with | nil => OK nil | (v',e')::t => coreExprToWeakExprList t >>= fun t' => - match coreVarSort v' with - | CoreExprVar _ => coreExprToWeakExpr e' >>= fun e' => OK ((v',e')::t') - | CoreTypeVar _ => Error "found a type variable in a recursive let" - | CoreCoerVar _ => Error "found a coercion variable in a recursive let" + match coreVarToWeakVar v' with + | WExprVar ev => coreExprToWeakExpr e' >>= fun e' => OK ((ev,e')::t') + | WTypeVar _ => Error "found a type variable in a recursive let" + | WCoerVar _ => Error "found a coercion variable in a recursive let" end end) rb) >>= fun rb' => coreExprToWeakExpr e >>= fun e' => OK (WELetRec (unleaves' rb') e') | CoreECase e v tbranches alts => + match coreVarToWeakVar v with + | WTypeVar _ => Error "found a type variable in a case" + | WCoerVar _ => Error "found a coercion variable in a case" + | WExprVar ev => coreExprToWeakExpr e >>= fun e' => coreTypeOfWeakExpr e' >>= fun te' => match te' with | TyConApp _ tc lt => ((fix mkBranches (branches: list (@triple AltCon (list CoreVar) (CoreExpr CoreVar))) - : ???(list (AltCon*list CoreVar*WeakExpr)) := + : ???(list (AltCon*list WeakVar*WeakExpr)) := match branches with | nil => OK nil | (mkTriple alt vars e)::rest => - mkBranches rest - >>= fun 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),vars,e')::rest') + | DataAlt _ _ _ _ tc' dc => OK (((DataAlt _ dc),(map coreVarToWeakVar vars),e')::rest') end end) alts) >>= fun branches => coreExprToWeakExpr e >>= fun scrutinee => list2vecOrError lt _ >>= fun lt' => - OK (WELet v scrutinee (WECase (WEVar v) tbranches tc lt' (unleaves branches))) + OK (WELet ev scrutinee (WECase (WEVar ev) tbranches tc lt' (unleaves branches))) | _ => Error "found a case whose scrutinee's type wasn't a TyConApp" end + end end. diff --git a/src/HaskCoreTypes.v b/src/HaskCoreTypes.v index ec9ffcc..a567196 100644 --- a/src/HaskCoreTypes.v +++ b/src/HaskCoreTypes.v @@ -15,7 +15,6 @@ Variable coreName_eq : forall (a b:CoreName), sumbool (a=b) (not (a=b)) Axiom coreName_eq_refl : ∀ v, (coreName_eq v v)=(left _ (refl_equal v)). Instance CoreNameEqDecidable : EqDecidable CoreName := { eqd_dec := coreName_eq -; eqd_dec_reflexive := coreName_eq_refl }. Inductive CoreIPName : Type -> Type := . Extract Inductive CoreIPName => "CoreSyn.IPName" [ ]. @@ -37,18 +36,6 @@ Extract Inductive CoreType => Extract Inductive PredType => "TypeRep.PredType" [ "TypeRep.ClassP" "TypeRep.IParam" "TypeRep.EqPred" ]. -Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". - -Definition haskLiteralToCoreType lit : CoreType := - TyConApp (haskLiteralToTyCon lit) nil. - -Inductive CoreVarSort : Type := -| CoreExprVar : CoreType -> CoreVarSort -| CoreTypeVar : Kind -> CoreVarSort -| CoreCoerVar : CoreType * CoreType -> CoreVarSort. - -Variable coreVarSort : CoreVar -> CoreVarSort. Extract Inlined Constant coreVarSort => "coreVarSort". - Variable coreTypeToString : CoreType -> string. Extract Inlined Constant coreTypeToString => "outputableToString". Variable coreNameToString : CoreName -> string. Extract Inlined Constant coreNameToString => "outputableToString". @@ -56,3 +43,12 @@ Variable CoreCoercion : Type. Extract Inlined Cons Variable coreCoercionToString : CoreCoercion -> string. Extract Inlined Constant coreCoercionToString => "outputableToString". Variable coreCoercionKind : CoreCoercion -> CoreType*CoreType. Extract Inlined Constant coreCoercionKind => "Coercion.coercionKind". + +Variable coretype_eq_dec : forall (c1 c2:CoreType), sumbool (eq c1 c2) (not (eq c1 c2)). + Extract Inlined Constant coretype_eq_dec => "Type.coreEqType". + Instance CoreTypeEqDecidable : EqDecidable CoreType. + apply Build_EqDecidable. + apply coretype_eq_dec. + Defined. + +Variable kindOfCoreType : CoreType -> Kind. Extract Inlined Constant kindOfCoreType => "(coreKindToKind . Coercion.typeKind)". diff --git a/src/HaskCoreVars.v b/src/HaskCoreVars.v index be64e5b..a55c09b 100644 --- a/src/HaskCoreVars.v +++ b/src/HaskCoreVars.v @@ -13,6 +13,6 @@ Variable coreVar_eq : forall (a b:CoreVar), sumbool (a=b) (not (a=b)). Axiom coreVar_eq_refl : forall v, (coreVar_eq v v) = (left _ (refl_equal v)). Instance CoreVarEqDecidable : EqDecidable CoreVar := { eqd_dec := coreVar_eq -; eqd_dec_reflexive := coreVar_eq_refl +(*; eqd_dec_reflexive := coreVar_eq_refl*) }. diff --git a/src/HaskGeneral.v b/src/HaskGeneral.v index 186ad1c..0c9ba33 100644 --- a/src/HaskGeneral.v +++ b/src/HaskGeneral.v @@ -44,6 +44,19 @@ Inductive Kind : Type := Notation "'★'" := KindType. Notation "a ⇛ b" := (KindTypeFunction a b). +Instance KindEqDecidable : EqDecidable Kind. + apply Build_EqDecidable. + induction v1. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; auto. + destruct (IHv1_1 v2_1); destruct (IHv1_2 v2_2); subst; auto; + right; intro; subst; inversion H; subst; apply n; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + destruct v2; try (right; intro q; inversion q; fail) ; left ; auto. + Defined. + Variable tyConToString : forall n, TyCon n -> string. Extract Inlined Constant tyConToString => "outputableToString". Variable tyFunToString : ∀ n, TyFunConst n -> string. Extract Inlined Constant tyFunToString => "outputableToString". Variable coFunToString : ∀ n, CoFunConst n -> string. Extract Inlined Constant coFunToString => "outputableToString". @@ -56,15 +69,5 @@ Variable tyCon_eq : forall {k}(n1 n2:TyCon k), sumbool (n1=n2) (not (n1=n2)). Extract Inlined Constant tyCon_eq => "(==)". Variable dataCon_eq : forall {n}{tc:TyCon n}{q}{r}{s}(n1 n2:DataCon tc q r s), sumbool (n1=n2) (not (n1=n2)). Extract Inlined Constant dataCon_eq => "(==)". -Axiom tyCon_eq_reflexive : forall `(tc:TyCon n), (tyCon_eq tc tc) = (left _ (refl_equal tc)). -Axiom dataCon_eq_reflexive : forall `(tc:@DataCon y z q r p) , (dataCon_eq tc tc) = (left _ (refl_equal tc)). - -Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := -{ eqd_dec := tyCon_eq -; eqd_dec_reflexive := tyCon_eq_reflexive -}. - -Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := -{ eqd_dec := dataCon_eq -; eqd_dec_reflexive := dataCon_eq_reflexive -}. +Instance TyConEqDecidable {n} : EqDecidable (TyCon n) := { eqd_dec := tyCon_eq }. +Instance DataConEqDecidable {n}{tc:TyCon n}{a}{b}{c} : EqDecidable (@DataCon _ tc a b c) := { eqd_dec := dataCon_eq }. diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index d6c5ecc..e9f3520 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -405,40 +405,6 @@ Fixpoint update_ξ -(* -Definition literalType (lit:Literal) : ∀ Γ, HaskType Γ := fun Γ TV ite => (TCon (literalTyCon lit)). -Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end. -Definition getlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskLevel Γ := match lht with t @@ l => l end. -(* the type of the scrutinee in a case branch *) -Require Import Coq.Arith.EqNat. -Definition bump (n:nat) : {z:nat & lt z n} -> {z:nat & lt z (S n)}. - intros. - destruct H. - exists x; omega. - Defined. -Definition vecOfNats (n:nat) : vec {z:nat & lt z n} n. - induction n. - apply vec_nil. - apply vec_cons. - exists n; omega. - apply (vec_map (bump _)); auto. - Defined. -Definition var_eq_dec {Γ:TypeEnv}(hv1 hv2:HaskTyVar Γ) : sumbool (eq hv1 hv2) (not (eq hv1 hv2)). - set (hv1 _ (vecOfNats _)) as hv1'. - set (hv2 _ (vecOfNats _)) as hv2'. - destruct hv1' as [hv1_n hv1_pf]. - destruct hv2' as [hv2_n hv2_pf]. - clear hv1_pf. - clear hv2_pf. - set (eq_nat_decide hv1_n hv2_n) as dec. - destruct dec. - left. admit. - right. intro. apply n. assert (hv1_n=hv2_n). admit. rewrite H0. apply eq_nat_refl. - Defined. -(* equality on levels is decidable *) -Definition lev_eq_dec {Γ:TypeEnv}(l1 l2:HaskLevel Γ) : sumbool (eq l1 l2) (not (eq l1 l2)) - := @list_eq_dec (HaskTyVar Γ) (@var_eq_dec Γ) l1 l2. -*) diff --git a/src/HaskWeak.v b/src/HaskWeak.v index b450330..ff696cc 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -5,35 +5,38 @@ Generalizable All Variables. Require Import Preamble. Require Import General. +Require Import Coq.Lists.List. Require Import HaskGeneral. Require Import HaskLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. +Require Import HaskCoreTypes. +Require Import HaskWeakVars. Inductive WeakExpr := -| WEVar : CoreVar -> WeakExpr -| WELit : HaskLiteral -> WeakExpr -| WELet : CoreVar -> WeakExpr -> WeakExpr -> WeakExpr -| WELetRec : Tree ??(CoreVar * WeakExpr) -> WeakExpr -> WeakExpr -| WECast : WeakExpr -> CoreCoercion -> WeakExpr -| WENote : Note -> WeakExpr -> WeakExpr -| WEApp : WeakExpr -> WeakExpr -> WeakExpr -| WETyApp : WeakExpr -> CoreType -> WeakExpr -| WECoApp : WeakExpr -> CoreCoercion -> WeakExpr -| WELam : CoreVar -> WeakExpr -> WeakExpr -| WETyLam : CoreVar -> WeakExpr -> WeakExpr -| WECoLam : CoreVar -> WeakExpr -> WeakExpr -| WEBrak : CoreVar -> WeakExpr -> WeakExpr -| WEEsc : CoreVar -> WeakExpr -> WeakExpr +| WEVar : WeakExprVar -> WeakExpr +| WELit : HaskLiteral -> WeakExpr +| WELet : WeakExprVar -> WeakExpr -> WeakExpr -> WeakExpr +| WELetRec : Tree ??(WeakExprVar * WeakExpr) -> WeakExpr -> WeakExpr +| WECast : WeakExpr -> WeakCoercion -> WeakExpr +| WENote : Note -> WeakExpr -> WeakExpr +| WEApp : WeakExpr -> WeakExpr -> WeakExpr +| WETyApp : WeakExpr -> CoreType -> WeakExpr +| WECoApp : WeakExpr -> WeakCoercion -> WeakExpr +| WELam : WeakExprVar -> WeakExpr -> WeakExpr +| WETyLam : WeakTypeVar -> WeakExpr -> WeakExpr +| WECoLam : WeakCoerVar -> WeakExpr -> WeakExpr +| WEBrak : WeakTypeVar -> WeakExpr -> WeakExpr +| WEEsc : WeakTypeVar -> WeakExpr -> WeakExpr | WECase : forall (scrutinee:WeakExpr) (tbranches:CoreType) {n:nat}(tc:TyCon n) (type_params:vec CoreType n) - (alts : Tree ??(AltCon*list CoreVar*WeakExpr)), + (alts : Tree ??(AltCon*list WeakVar*WeakExpr)), WeakExpr. -(* calculate the free CoreVar's in a WeakExpr *) -Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar := +(* calculate the free WeakVar's in a WeakExpr *) +Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar := match me with | WELit _ => nil | WEVar cv => cv::nil @@ -45,28 +48,34 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar := | WEEsc ec e => getWeakExprFreeVars e | WELet cv e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (removeFromDistinctList cv (getWeakExprFreeVars e2)) | WEApp e1 e2 => mergeDistinctLists (getWeakExprFreeVars e1) (getWeakExprFreeVars e2) - | WELam cv e => removeFromDistinctList cv (getWeakExprFreeVars e) - | WETyLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e) - | WECoLam cv e => removeFromDistinctList cv (getWeakExprFreeVars e) + | WELam cv e => @removeFromDistinctList _ WeakExprVarEqDecidable cv (getWeakExprFreeVars e) + | WETyLam cv e => getWeakExprFreeVars e + | WECoLam cv e => getWeakExprFreeVars e (* 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 CoreVar*WeakExpr)) {struct alts} : list CoreVar := + ((fix getWeakExprFreeVarsAlts (alts:Tree ??(AltCon*list WeakVar*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' vars (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_Branch b1 b2 => mergeDistinctLists (getWeakExprFreeVarsAlts b1) (getWeakExprFreeVarsAlts b2) end) alts)) - | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr))(cvl:list CoreVar) := + | WELetRec mlr e => (fix removeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr))(cvl:list WeakExprVar) := match mlr with | T_Leaf None => cvl | T_Leaf (Some (cv,e)) => removeFromDistinctList cv cvl | T_Branch b1 b2 => removeVarsLetRec b1 (removeVarsLetRec b2 cvl) end) mlr (mergeDistinctLists (getWeakExprFreeVars e) - ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(CoreVar * WeakExpr)) := + ((fix getWeakExprFreeVarsLetRec (mlr:Tree ??(WeakExprVar * WeakExpr)) := match mlr with | T_Leaf None => nil | T_Leaf (Some (cv,e)) => getWeakExprFreeVars e @@ -74,21 +83,21 @@ Fixpoint getWeakExprFreeVars (me:WeakExpr) : list CoreVar := end) mlr)) end. -(* wrap lambdas around an expression until it has no free variables *) +(* wrap lambdas around an expression until it has no free expression variables *) Definition makeClosedExpression : WeakExpr -> WeakExpr := - fun me => (fix closeExpression (me:WeakExpr)(cvl:list CoreVar) := + fun me => (fix closeExpression (me:WeakExpr)(cvl:list WeakExprVar) := match cvl with | nil => me | cv::cvl' => WELam cv (closeExpression me cvl') end) me (getWeakExprFreeVars me). (* messy first-order capture-avoiding substitution on CoreType's *) -Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) := +Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) : CoreType := match te with | TyVarTy tv' => if eqd_dec tv tv' then tsubst else te - | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) + | AppTy t1 t2 => AppTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) | FunTy t1 t2 => FunTy (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst) - | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst) + | ForAllTy tv' t => if eqd_dec tv tv' then te else ForAllTy tv' (replaceCoreVar t tv tsubst) | PredTy (EqPred t1 t2) => PredTy (EqPred (replaceCoreVar t1 tv tsubst) (replaceCoreVar t2 tv tsubst)) | PredTy (IParam ip ty) => PredTy (IParam ip (replaceCoreVar ty tv tsubst)) | PredTy (ClassP _ c lt) => PredTy (ClassP c ((fix replaceCoreDistinctList (lt:list CoreType) := @@ -106,64 +115,48 @@ Fixpoint replaceCoreVar (te:CoreType)(tv:CoreVar)(tsubst:CoreType) := (* calculate the CoreType of a WeakExpr *) Fixpoint coreTypeOfWeakExpr (ce:WeakExpr) : ???CoreType := match ce with - | WEVar v => match coreVarSort v with - | CoreExprVar t => OK t - | CoreTypeVar _ => Error "found tyvar in expression" - | CoreCoerVar _ => Error "found coercion variable in expression" - end + | WEVar (weakExprVar v t) => OK t | WELit lit => OK (haskLiteralToCoreType lit) | WEApp e1 e2 => coreTypeOfWeakExpr e1 >>= fun t' => match t' with - | FunTy t1 t2 => OK t2 | (TyConApp 2 tc (t1::t2::nil)) => if (tyCon_eq tc ArrowTyCon) then OK t2 - else Error ("found non-function type "+++(coreTypeToString t')+++" in EApp") - | _ => Error ("found non-function type "+++(coreTypeToString t')+++" in EApp") + else Error ("found non-function type "+++(weakTypeToString t')+++" in EApp") + | _ => Error ("found non-function type "+++(weakTypeToString t')+++" in EApp") end | WETyApp e t => coreTypeOfWeakExpr e >>= fun te => match te with - | ForAllTy v ct => match coreVarSort v with - | CoreExprVar _ => Error "found an expression variable inside an forall-type!" - | CoreTypeVar _ => OK (replaceCoreVar ct v t) - | CoreCoerVar _ => Error "found a coercion variable inside an forall-type!" - end - | _ => Error ("found non-forall type "+++(coreTypeToString te)+++" in ETyApp") + | ForAllTy v ct => OK (replaceCoreVar ct v t) + | _ => Error ("found non-forall type "+++(weakTypeToString te)+++" in ETyApp") end | WECoApp e co => coreTypeOfWeakExpr e >>= fun te => match te with - | FunTy (PredTy (EqPred t1 t2)) t3 => OK t3 | TyConApp 2 tc ((PredTy (EqPred t1 t2))::t3::nil) => if (tyCon_eq tc ArrowTyCon) then OK t3 - else Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp") - | _ => Error ("found non-coercion type "+++(coreTypeToString te)+++" in ETyApp") + else Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp") + | _ => Error ("found non-coercion type "+++(weakTypeToString te)+++" in ETyApp") end - | WELam ev e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort ev with - | CoreExprVar vt => OK (FunTy vt t') - | CoreTypeVar _ => Error "found a type variable in a WELam!" - | CoreCoerVar _ => Error "found a coercion variable in a WELam!" - end - | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => OK (ForAllTy tv t') - | WECoLam cv e => coreTypeOfWeakExpr e >>= fun t' => match coreVarSort cv with - | CoreExprVar vt => Error "found an expression variable in a WECoLam!" - | CoreTypeVar _ => Error "found a type variable in a WECoLam!" - | CoreCoerVar (φ₁,φ₂) => OK (FunTy (PredTy (EqPred φ₁ φ₂)) t') - end + | WELam (weakExprVar ev vt) e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon (vt::t'::nil)) + | WETyLam tv e => coreTypeOfWeakExpr e >>= fun t' => match tv with weakTypeVar tvc _ => OK (ForAllTy tvc t') end + | WECoLam (weakCoerVar cv φ₁ φ₂) e => + coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp ArrowTyCon ((PredTy (EqPred φ₁ φ₂))::t'::nil)) | WELet ev ve e => coreTypeOfWeakExpr e | WELetRec rb e => coreTypeOfWeakExpr e | WENote n e => coreTypeOfWeakExpr e - | WECast e co => OK (snd (coreCoercionKind co)) + | WECast e (weakCoercion t1 t2 _) => OK t2 | WECase scrutinee tbranches n tc type_params alts => OK tbranches - | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ec)::t'::nil)) - | WEEsc ec e => coreTypeOfWeakExpr e >>= fun t' => + | WEBrak ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ => + OK (TyConApp hetMetCodeTypeTyCon ((TyVarTy ecc)::t'::nil)) end + | WEEsc ec e => coreTypeOfWeakExpr e >>= fun t' => match ec with weakTypeVar ecc _ => match t' with | (TyConApp 2 tc ((TyVarTy ec')::t''::nil)) => if (tyCon_eq tc hetMetCodeTypeTyCon) - then if eqd_dec ec ec' then OK t'' + then if eqd_dec ecc ec' then OK t'' else Error "level mismatch in escapification" else Error "ill-typed escapification" | _ => Error "ill-typed escapification" - end + end end end. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v new file mode 100644 index 0000000..c43842f --- /dev/null +++ b/src/HaskWeakVars.v @@ -0,0 +1,88 @@ +(*********************************************************************************************************************************) +(* HaskWeakVars: types and variables for HaskWeak *) +(*********************************************************************************************************************************) + +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. + +Inductive WeakTypeVar := weakTypeVar : CoreVar -> Kind -> WeakTypeVar. + +Inductive WeakCoercion : Type := weakCoercion : CoreType -> CoreType -> CoreCoercion -> WeakCoercion. + +Inductive WeakCoerVar := weakCoerVar : CoreVar -> CoreType -> CoreType -> WeakCoerVar. + +Inductive WeakExprVar := weakExprVar : CoreVar -> CoreType -> WeakExprVar. + +Inductive WeakVar : Type := +| WExprVar : WeakExprVar -> WeakVar +| WTypeVar : WeakTypeVar -> WeakVar +| WCoerVar : WeakCoerVar -> WeakVar. + +Definition haskLiteralToCoreType lit : CoreType := + TyConApp (haskLiteralToTyCon lit) nil. + +Definition weakTypeToCoreType (wt:CoreType) : CoreType := wt. + +Definition weakTypeToString : CoreType -> string := coreTypeToString ○ weakTypeToCoreType. + +(* EqDecidable instances for all of the above *) +Instance CoreTypeVarEqDecidable : EqDecidable WeakTypeVar. + apply Build_EqDecidable. + intros. + destruct v1 as [cv1 k1]. + destruct v2 as [cv2 k2]. + destruct (eqd_dec cv1 cv2); subst. + destruct (eqd_dec k1 k2); subst. + left; auto. + right; intro; apply n; inversion H; subst; auto. + right; intro; apply n; inversion H; subst; auto. + Defined. + +Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar. + apply Build_EqDecidable. + intros. + destruct v1 as [cv1 t1a t1b]. + destruct v2 as [cv2 t2a t2b]. + destruct (eqd_dec cv1 cv2); subst. + destruct (eqd_dec t1a t2a); subst. + destruct (eqd_dec t1b t2b); subst. + left; auto. + right; intro; apply n; inversion H; subst; auto. + right; intro; apply n; inversion H; subst; auto. + right; intro; apply n; inversion H; subst; auto. + Defined. + +Instance WeakExprVarEqDecidable : EqDecidable WeakExprVar. + apply Build_EqDecidable. + intros. + destruct v1 as [cv1 k1]. + destruct v2 as [cv2 k2]. + destruct (eqd_dec cv1 cv2); subst. + destruct (eqd_dec k1 k2); subst. + left; auto. + right; intro; apply n; inversion H; subst; auto. + right; intro; apply n; inversion H; subst; auto. + Defined. + +Instance WeakVarEqDecidable : EqDecidable WeakVar. + apply Build_EqDecidable. + induction v1; destruct v2; try (right; intro q; inversion q; fail) ; auto; + destruct (eqd_dec w w0); subst. + left; auto. + right; intro X; apply n; inversion X; auto. + left; auto. + right; intro X; apply n; inversion X; auto. + left; auto. + right; intro X; apply n; inversion X; auto. + Defined. + + + + diff --git a/src/Main.v b/src/Main.v index 300dfb8..9188e5d 100644 --- a/src/Main.v +++ b/src/Main.v @@ -9,6 +9,7 @@ Require Import HaskLiterals. Require Import HaskCoreVars. Require Import HaskCoreTypes. Require Import HaskCore. +Require Import HaskWeakVars. Require Import HaskWeak. Require Import HaskCoreToWeak. Require Import HaskStrongTypes. -- 1.7.10.4