From 5c493a75fbaf8454d8a21e55edc5b193e2c5879c Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 12 Mar 2011 16:30:33 -0800 Subject: [PATCH] Eliminate the need for WeakVar decidable equality axiom --- src/Extraction.v | 12 ++++++++---- src/HaskStrongToWeak.v | 22 +++++++++++++--------- src/HaskWeak.v | 3 ++- src/HaskWeakToStrong.v | 19 ++++++++++--------- src/HaskWeakTypes.v | 5 ++--- src/HaskWeakVars.v | 4 ++-- 6 files changed, 37 insertions(+), 28 deletions(-) diff --git a/src/Extraction.v b/src/Extraction.v index e2e3800..3371ed5 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -77,10 +77,14 @@ Section core2proof. (* We need to be able to resolve unbound exprvars, but we can be sure their types will have no * free tyvars in them *) - Definition ξ (wev:WeakExprVar) : LeveledHaskType Γ ★ := - match weakTypeToType' φ wev ★ with - | Error s => fail ("Error in top-level xi: " +++ s) - | OK t => t @@ nil + Definition ξ (cv:CoreVar) : LeveledHaskType Γ ★ := + match coreVarToWeakVar cv with + | WExprVar wev => match weakTypeToType' φ wev ★ with + | Error s => fail ("Error in top-level xi: " +++ s) + | OK t => t @@ nil + end + | WTypeVar _ => fail "top-level xi got a type variable" + | WCoerVar _ => fail "top-level xi got a coercion variable" end. Definition header : string := diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 759dcb9..1530e91 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -11,6 +11,7 @@ Require Import Coq.Lists.List. Require Import Coq.Init.Specif. Require Import HaskKinds. Require Import HaskCoreLiterals. +Require Import HaskCoreVars. Require Import HaskWeakTypes. Require Import HaskWeakVars. Require Import HaskWeak. @@ -67,17 +68,20 @@ Definition reindexStrongExpr {VV}{HH}{eqVV:EqDecidable VV}{eqHH:EqDecidable HH} Definition updateITE {Γ:TypeEnv}{TV:Kind->Type}{κ}(tv:TV κ)(ite:InstantiatedTypeEnv TV Γ) : InstantiatedTypeEnv TV (κ::Γ) := tv::::ite. -Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{lev} +Definition unlev {Γ}{κ}(lht:LeveledHaskType Γ κ) := + match lht with t@@l => t end. + +Fixpoint strongExprToWeakExpr {Γ}{Δ}{ξ}{τ} (ftv:Fresh Kind (fun _ => WeakTypeVar)) (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) - (exp:@Expr WeakExprVar _ Γ Δ ξ lev) + (exp:@Expr _ CoreVarEqDecidable Γ Δ ξ τ) : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> WeakExpr := -match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with -| EVar _ _ _ ev => fun ite => WEVar ev +match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> WeakExpr with +| EVar Γ' _ ξ' ev => fun ite => WEVar (weakExprVar ev (@typeToWeakType ftv Γ' ★ (unlev (ξ' ev)) ite)) | ELit _ _ _ lit _ => fun ite => WELit lit | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => WEApp (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) -| ELam Γ' _ _ _ _ _ cv e => fun ite => WELam cv (strongExprToWeakExpr ftv fcv e ite) -| ELet Γ' _ _ _ _ _ ev e1 e2 => fun ite => WELet ev (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) +| ELam Γ' _ _ _ t _ cv e => fun ite => WELam (weakExprVar cv (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e ite) +| ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => WELet (weakExprVar ev (typeToWeakType ftv t ite)) (strongExprToWeakExpr ftv fcv e1 ite) (strongExprToWeakExpr ftv fcv e2 ite) | EEsc Γ' _ _ ec t _ e => fun ite => WEEsc (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) | EBrak Γ' _ _ ec t _ e => fun ite => WEBrak (ec _ ite) (strongExprToWeakExpr ftv fcv e ite) (typeToWeakType ftv t ite) | ECast Γ Δ ξ t1 t2 γ l e => fun ite => WECast (strongExprToWeakExpr ftv fcv e ite) (strongCoercionToWeakCoercion γ ite) @@ -117,14 +121,14 @@ match exp as E in Expr G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) let t2' := typeToWeakType ftv σ₂ ite in let (cv,fcv') := next _ _ fcv (t1',t2') in WECoLam cv (strongExprToWeakExpr ftv fcv' e ite) end -with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{lev}{vars} +with exprLetRec2WeakExprLetRec {Γ}{Δ}{ξ}{τ}{vars} (ftv:Fresh Kind (fun _ => WeakTypeVar)) (fcv:Fresh (WeakType*WeakType) (fun _ => WeakCoerVar)) - (elrb:@ELetRecBindings WeakExprVar _ Γ Δ ξ lev vars) + (elrb:@ELetRecBindings _ CoreVarEqDecidable Γ Δ ξ τ vars) : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> Tree ??(WeakExprVar * WeakExpr) := match elrb as E in ELetRecBindings G D X L V return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> Tree ??(WeakExprVar * WeakExpr) with | ELR_nil _ _ _ _ => fun ite => [] -| ELR_leaf _ _ _ _ cv v e => fun ite => [(v,(strongExprToWeakExpr ftv fcv e ite))] +| ELR_leaf _ _ _ t cv v e => fun ite => [((weakExprVar v (typeToWeakType ftv t ite)),(strongExprToWeakExpr ftv fcv e ite))] | ELR_branch _ _ _ _ _ _ b1 b2 => fun ite => (exprLetRec2WeakExprLetRec ftv fcv b1 ite),, (exprLetRec2WeakExprLetRec ftv fcv b2 ite) end. diff --git a/src/HaskWeak.v b/src/HaskWeak.v index 537bfbe..78cd6ae 100644 --- a/src/HaskWeak.v +++ b/src/HaskWeak.v @@ -43,6 +43,7 @@ Inductive WeakExpr := WeakExpr. (* calculate the free WeakVar's in a WeakExpr *) +(* Fixpoint getWeakExprFreeVars (me:WeakExpr) : list WeakExprVar := match me with | WELit _ => nil @@ -92,7 +93,7 @@ Definition makeClosedExpression : WeakExpr -> WeakExpr := | nil => me | cv::cvl' => WELam cv (closeExpression me cvl') end) me (getWeakExprFreeVars me). - +*) Definition weakTypeOfLiteral (lit:HaskLiteral) : WeakType := (WTyCon (haskLiteralToTyCon lit)). diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index e70e17d..fbd47fb 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -347,8 +347,8 @@ Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> HaskCoVar Γ Δ Defined. (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *) -Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ) - : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ τ'). +Definition castExpr (err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ) + : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ'). intros. destruct τ as [τ l]. destruct τ' as [τ' l']. @@ -375,20 +375,20 @@ Definition weakExprToStrongExpr : forall (Δ:CoercionEnv Γ) (φ:TyVarResolver Γ) (ψ:CoVarResolver Γ Δ) - (ξ:WeakExprVar -> LeveledHaskType Γ ★) + (ξ:CoreVar -> LeveledHaskType Γ ★) (τ:HaskType Γ ★) (lev:HaskLevel Γ), - WeakExpr -> ???(Expr Γ Δ ξ (τ @@ lev) ). + WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ). refine (( fix weakExprToStrongExpr (Γ:TypeEnv) (Δ:CoercionEnv Γ) (φ:TyVarResolver Γ) (ψ:CoVarResolver Γ Δ) - (ξ:WeakExprVar -> LeveledHaskType Γ ★) + (ξ:CoreVar -> LeveledHaskType Γ ★) (τ:HaskType Γ ★) (lev:HaskLevel Γ) - (we:WeakExpr) : ???(@Expr _ WeakExprVarEqDecidable Γ Δ ξ (τ @@ lev) ) := + (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) := match we with | WEVar v => castExpr "WEVar" (τ @@ lev) (EVar Γ Δ ξ v) @@ -398,7 +398,8 @@ Definition weakExprToStrongExpr : forall | WELam ev e => weakTypeToType' φ ev ★ >>= fun tv => weakTypeOfWeakExpr e >>= fun t => weakTypeToType' φ t ★ >>= fun τ' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((ev,tv@@lev)::nil)) τ' _ e >>= fun e' => + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((ev:CoreVar),tv@@lev)::nil)) + τ' _ e >>= fun e' => castExpr "WELam" _ (ELam Γ Δ ξ tv _ _ ev e') | WEBrak ec e tbody => weakExprToStrongExpr Γ Δ φ ψ ξ τ ((φ (`ec))::lev) e >>= fun e' => @@ -415,9 +416,9 @@ Definition weakExprToStrongExpr : forall | WELet v ve ebody => weakTypeToType' φ v ★ >>= fun tv => weakExprToStrongExpr Γ Δ φ ψ ξ tv lev ve >>= fun ve' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ ((v,tv@@lev)::nil)) τ lev ebody + weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ (((v:CoreVar),tv@@lev)::nil)) τ lev ebody >>= fun ebody' => - OK (ELet _ _ _ tv _ lev v ve' ebody') + OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') | WEApp e1 e2 => weakTypeOfWeakExpr e2 >>= fun t2 => weakTypeToType' φ t2 ★ >>= fun t2' => diff --git a/src/HaskWeakTypes.v b/src/HaskWeakTypes.v index 82cf8ad..56c2f48 100644 --- a/src/HaskWeakTypes.v +++ b/src/HaskWeakTypes.v @@ -120,9 +120,7 @@ Definition compare_weakTypes (w1 w2:WeakType) := then true else false. -(* Coq's "decide equality" can't cope here; we have to cheat for now *) -Axiom compare_weakTypes_axiom : forall w1 w2, if compare_weakTypes w1 w2 then w1=w2 else not (w1=w2). - +(* Instance EqDecidableWeakType : EqDecidable WeakType. apply Build_EqDecidable. intros. @@ -133,6 +131,7 @@ Instance EqDecidableWeakType : EqDecidable WeakType. left; auto. right; auto. Defined. +*) Instance WeakTypeToString : ToString WeakType := { toString := coreTypeToString ○ weakTypeToCoreType }. diff --git a/src/HaskWeakVars.v b/src/HaskWeakVars.v index ee8d3cf..8d84610 100644 --- a/src/HaskWeakVars.v +++ b/src/HaskWeakVars.v @@ -58,6 +58,7 @@ Variable tyFunResultKind : CoreTyCon -> Kind. Extract Inlined Constant tyFunResu Definition tyFunKind (tc:TyFun) : ((list Kind) * Kind) := ((map (fun (x:WeakTypeVar) => x:Kind) (tyConTyVars tc)) , (tyFunResultKind tc)). +(* (* EqDecidable instances for all of the above *) Instance WeakCoerVarEqDecidable : EqDecidable WeakCoerVar. apply Build_EqDecidable. @@ -96,8 +97,7 @@ Instance WeakVarEqDecidable : EqDecidable WeakVar. left; auto. right; intro X; apply n; inversion X; auto. Defined. - - +*) Instance WeakVarToString : ToString WeakVar := { toString := fun x => toString (weakVarToCoreVar x) }. \ No newline at end of file -- 1.7.10.4