From 9241d797587022ecd51e3c38cd34588de6745524 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 27 May 2011 19:50:34 -0700 Subject: [PATCH 1/1] migrate HaskStrong away from using LeveledHaskType --- src/ExtractionMain.v | 6 ++--- src/HaskProofToStrong.v | 25 ++++++++++++--------- src/HaskStrong.v | 54 +++++++++++++++++++++----------------------- src/HaskStrongToProof.v | 57 +++++++++++++++++++++++------------------------ src/HaskStrongToWeak.v | 10 ++++----- src/HaskWeakToStrong.v | 38 +++++++++++++++---------------- 6 files changed, 94 insertions(+), 96 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 77326e0..4da66c7 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -132,7 +132,7 @@ Section core2proof. OK (eol+++eol+++eol+++ "\begin{preview}"+++eol+++ "$\displaystyle "+++ - toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ e))+++ + toString (nd_ml_toLatexMath (@expr2proof _ _ _ _ _ _ _ e))+++ " $"+++eol+++ "\end{preview}"+++eol+++eol+++eol) )))))))). @@ -432,9 +432,9 @@ Section core2proof. (addErrorMessage ("HaskStrong...") (let haskProof := skolemize_and_flatten_proof hetmet_flatten' hetmet_unflatten' - hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ e) + hetmet_flattened_id' my_ga (@expr2proof _ _ _ _ _ _ _ e) in (* insert HaskProof-to-HaskProof manipulations here *) - OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ@@nil) _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) + OK ((@proof2expr nat _ FreshNat _ _ (flatten_type τ) nil _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) >>= fun e' => (snd e') >>= fun e'' => strongExprToWeakExpr hetmet_brak' hetmet_esc' diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 78c2e41..97ef42b 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -28,10 +28,10 @@ Section HaskProofToStrong. Definition judg2exprType (j:Judg) : Type := match j with (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars -> - FreshM (ITree _ (fun t => Expr Γ Δ ξ (t @@ l)) τ) + FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ) end. - Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ. + Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l. intros. inversion X; auto. Defined. @@ -223,7 +223,7 @@ Section HaskProofToStrong. Defined. Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type := - forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ (t@@l)) τ). + forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ). Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), ujudg2exprType Γ ξ Δ h t l -> @@ -354,7 +354,7 @@ Section HaskProofToStrong. Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' : ITree (HaskType Γ ★) - (fun t : HaskType Γ ★ => Expr Γ Δ ξ' (t @@ l)) + (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l) (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes) -> ELetRecBindings Γ Δ ξ' l varstypes. intros. @@ -421,7 +421,8 @@ Section HaskProofToStrong. prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} -> ((fun sac => FreshM { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac - & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)). + & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) + (weakT' tbranches) (weakL' lev) }) (projT1 pcb)). intro pcb. intro X. simpl in X. @@ -567,8 +568,11 @@ Section HaskProofToStrong. destruct case_RVar. apply ILeaf; simpl; intros; refine (return ILeaf _ _). - destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2. - apply EVar. + destruct vars; simpl in H; inversion H; destruct o. inversion H1. + set (@EVar _ _ _ Δ ξ v) as q. + rewrite <- H2 in q. + simpl in q. + apply q. inversion H. destruct case_RGlobal. @@ -852,9 +856,9 @@ Section HaskProofToStrong. admit. Defined. - Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★) - {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [unlev τ] @ getlev τ] -> - FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}). + Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★) + {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] -> + FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}). intro pf. set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd. apply closed2expr in cnd. @@ -872,7 +876,6 @@ Section HaskProofToStrong. exists ξ. apply ileaf in it. simpl in it. - destruct τ. apply it. apply INone. Defined. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index ed3cd92..bf51e1a 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -29,55 +29,53 @@ Section HaskStrong. }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. - Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type := + Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> HaskType Γ ★ -> HaskLevel Γ -> Type := (* an "EGlobal" is any variable which is free in the expression which was passed to -fcoqpass (ie bound outside it) *) - | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v @@ lev) + | EGlobal: forall Γ Δ ξ (g:Global Γ) v lev, Expr Γ Δ ξ (g v) lev - | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (ξ ev) - | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit@@l) - | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) -> Expr Γ Δ ξ (t1 @@ l) - | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) - | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@l) - | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]> @@ l) -> Expr Γ Δ ξ (t @@ (ec::l)) - | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (t @@ (ec::l)) -> Expr Γ Δ ξ (<[ ec |- t ]> @@ l) - | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, - Expr Γ Δ ξ (t1 @@ l) -> Expr Γ Δ ξ (t2 @@ l) - | ENote : ∀ Γ Δ ξ t, Note -> Expr Γ Δ ξ t -> Expr Γ Δ ξ t - | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ @@ l) -> Expr Γ Δ ξ (substT σ τ @@ l) - | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, - Expr Γ (σ₁∼∼∼σ₂::Δ) ξ (σ @@ l) -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ @@ l) - | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, - Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ @@ l) -> Expr Γ Δ ξ (σ @@l) + | EVar : ∀ Γ Δ ξ ev, Expr Γ Δ ξ (unlev (ξ ev)) (getlev (ξ ev)) + | ELit : ∀ Γ Δ ξ lit l, Expr Γ Δ ξ (literalType lit) l + | EApp : ∀ Γ Δ ξ t1 t2 l, Expr Γ Δ ξ (t2--->t1) l -> Expr Γ Δ ξ t2 l -> Expr Γ Δ ξ (t1) l + | ELam : ∀ Γ Δ ξ t1 t2 l ev, Expr Γ Δ (update_xi ξ l ((ev,t1)::nil)) t2 l -> Expr Γ Δ ξ (t1--->t2) l + | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ tv l ->Expr Γ Δ (update_xi ξ l ((ev,tv)::nil)) t l -> Expr Γ Δ ξ t l + | EEsc : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ (<[ ec |- t ]>) l -> Expr Γ Δ ξ t (ec::l) + | EBrak : ∀ Γ Δ ξ ec t l, Expr Γ Δ ξ t (ec::l) -> Expr Γ Δ ξ (<[ ec |- t ]>) l + | ECast : forall Γ Δ ξ t1 t2 (γ:HaskCoercion Γ Δ (t1 ∼∼∼ t2)) l, Expr Γ Δ ξ t1 l -> Expr Γ Δ ξ t2 l + | ENote : ∀ Γ Δ ξ t l, Note -> Expr Γ Δ ξ t l -> Expr Γ Δ ξ t l + | ETyApp : ∀ Γ Δ κ σ τ ξ l, Expr Γ Δ ξ (HaskTAll κ σ) l -> Expr Γ Δ ξ (substT σ τ) l + | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l -> Expr Γ Δ ξ (σ₁∼∼σ₂ ⇒ σ) l + | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l -> Expr Γ Δ ξ σ l | ETyLam : ∀ Γ Δ ξ κ σ l, - Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) + Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l | ECase : forall Γ Δ ξ l tc tbranches atypes, - Expr Γ Δ ξ (caseType tc atypes @@ l) -> + Expr Γ Δ ξ (caseType tc atypes) l -> Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs tc atypes sac & Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) - (weakLT' (tbranches@@l)) } } -> - Expr Γ Δ ξ (tbranches @@ l) + (weakT' tbranches) + (weakL' l) } } -> + Expr Γ Δ ξ tbranches l | ELetRec : ∀ Γ Δ ξ l τ vars, distinct (leaves (mapOptionTree (@fst _ _) vars)) -> let ξ' := update_xi ξ l (leaves vars) in - ELetRecBindings Γ Δ ξ' l vars -> - Expr Γ Δ ξ' (τ@@l) -> - Expr Γ Δ ξ (τ@@l) + ELetRecBindings Γ Δ ξ' l vars -> + Expr Γ Δ ξ' τ l -> + Expr Γ Δ ξ τ l (* can't avoid having an additional inductive: it is a tree of Expr's, each of whose ξ depends on the type of the entire tree *) with ELetRecBindings : ∀ Γ, CoercionEnv Γ -> (VV -> LeveledHaskType Γ ★) -> HaskLevel Γ -> Tree ??(VV*HaskType Γ ★) -> Type := | ELR_nil : ∀ Γ Δ ξ l , ELetRecBindings Γ Δ ξ l [] - | ELR_leaf : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ (t @@ l) -> ELetRecBindings Γ Δ ξ l [(v,t)] + | ELR_leaf : ∀ Γ Δ ξ l v t, Expr Γ Δ ξ t l -> ELetRecBindings Γ Δ ξ l [(v,t)] | ELR_branch : ∀ Γ Δ ξ l t1 t2, ELetRecBindings Γ Δ ξ l t1 -> ELetRecBindings Γ Δ ξ l t2 -> ELetRecBindings Γ Δ ξ l (t1,,t2) . Context {ToStringVV:ToString VV}. Context {ToLatexVV:ToLatex VV}. - Fixpoint exprToString {Γ}{Δ}{ξ}{τ}(exp:Expr Γ Δ ξ τ) : string := + Fixpoint exprToString {Γ}{Δ}{ξ}{τ}{l}(exp:Expr Γ Δ ξ τ l) : string := match exp with | EVar Γ' _ ξ' ev => "var."+++ toString ev | EGlobal Γ' _ ξ' g v _ => "global." +++ toString (g:CoreVar) @@ -87,7 +85,7 @@ Section HaskStrong. | EApp Γ' _ _ _ _ _ e1 e2 => "("+++exprToString e1+++")("+++exprToString e2+++")" | EEsc Γ' _ _ ec t _ e => "~~("+++exprToString e+++")" | EBrak Γ' _ _ ec t _ e => "<["+++exprToString e+++"]>" - | ENote _ _ _ _ n e => "note."+++exprToString e + | ENote _ _ _ _ n _ e => "note."+++exprToString e | ETyApp Γ Δ κ σ τ ξ l e => "("+++exprToString e+++")@("+++toString τ+++")" | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e => "("+++exprToString e+++")~(co)" | ECast Γ Δ ξ t1 t2 γ l e => "cast ("+++exprToString e+++"):t2" @@ -96,7 +94,7 @@ Section HaskStrong. | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME" | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e end. - Instance ExprToString Γ Δ ξ τ : ToString (Expr Γ Δ ξ τ) := { toString := exprToString }. + Instance ExprToString Γ Δ ξ τ l : ToString (Expr Γ Δ ξ τ l) := { toString := exprToString }. End HaskStrong. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 791fdf5..8a49c81 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -520,8 +520,8 @@ Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstyp apply q. Qed. -Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV := - match exp as E in Expr Γ Δ ξ τ with +Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : Tree ??VV := + match exp as E in Expr Γ Δ ξ τ l with | EGlobal Γ Δ ξ _ _ _ => [] | EVar Γ Δ ξ ev => [ev] | ELit Γ Δ ξ lit lev => [] @@ -531,7 +531,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | EEsc Γ Δ ξ ec t lev e => expr2antecedent e | EBrak Γ Δ ξ ec t lev e => expr2antecedent e | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e - | ENote Γ Δ ξ t n e => expr2antecedent e + | ENote Γ Δ ξ t l n e => expr2antecedent e | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e @@ -546,7 +546,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? & Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) - (weakLT' (tbranches@@l)) } } + (weakT' tbranches) (weakL' l)} } ): Tree ??VV := match alts with | T_Leaf None => [] @@ -566,7 +566,7 @@ Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} & Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) - (weakLT' (tbranches@@l)) } }) + (weakT' tbranches) (weakL' l) } }) : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. destruct alt. exists x. @@ -1067,7 +1067,7 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e ??{sac : StrongAltCon & {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac & Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) - (scbwv_xi scb ξ l) (weakLT' (tbranches @@ l))}}), + (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}), (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) (mapOptionTree mkProofCaseBranch alts')) @@ -1094,40 +1094,40 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e Qed. Definition expr2proof : - forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), - ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev τ] @ getlev τ]. + forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l), + ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l]. - refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp} - : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [unlev τ'] @ getlev τ'] := - match exp as E in Expr Γ Δ ξ τ with + refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp} + : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] := + match exp as E in Expr Γ Δ ξ τ l with | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _ | EVar Γ Δ ξ ev => let case_EVar := tt in _ | ELit Γ Δ ξ lit lev => let case_ELit := tt in _ | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in - (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2) - | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e) + (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2) + | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in - (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) + (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree disti branches ebody => let ξ' := update_xi ξ lev (leaves tree) in - let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) + let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody) ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree') : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' := match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _ - | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e) + | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e) | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2) end ) _ _ _ _ tree branches) - | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e) - | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e) + | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) + | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) | ECase Γ Δ ξ l tc tbranches atypes e alts' => let dcsp := ((fix mkdcsp (alts: @@ -1135,7 +1135,7 @@ Definition expr2proof : & Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) (scbwv_xi scb ξ l) - (weakLT' (tbranches@@l)) } }) + (weakT' tbranches) (weakL' l) } }) : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with @@ -1144,12 +1144,12 @@ Definition expr2proof : | T_Leaf (Some x) => match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with existT sac (existT scbx ex) => - (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex) + (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex) end end) alts') - in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e) + in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e) end - ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp. + ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp. destruct case_EGlobal. apply nd_rule. @@ -1228,7 +1228,6 @@ Definition expr2proof : auto. destruct case_ENote. - destruct t. eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ]. apply e'. auto. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index d86d05b..deb7adc 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -107,10 +107,10 @@ Section HaskStrongToWeak. | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev end. - Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ) + Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}{l}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ l) : InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ -> UniqM WeakExpr := - match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with + match exp as E in @Expr _ _ G D X T L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with | EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end | EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v)) ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g)) @@ -133,7 +133,7 @@ Section HaskStrongToWeak. | EBrak Γ' _ _ ec t _ e => fun ite => bind t' = typeToWeakType t ite ; bind e' = exprToWeakExpr χ e ite ; return WEBrak hetmet_brak (ec _ ite) e' t' - | ENote _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite + | ENote _ _ _ _ _ n e => fun ite => bind e' = exprToWeakExpr χ e ite ; return WENote n e' | ETyApp Γ Δ κ σ τ ξ l e => fun ite => bind t' = typeToWeakType τ ite ; bind e' = exprToWeakExpr χ e ite @@ -158,7 +158,7 @@ Section HaskStrongToWeak. ; bind tbranches' = @typeToWeakType Γ _ tbranches ite ; bind escrut' = exprToWeakExpr χ escrut ite ; bind branches' = - ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } }) + ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ _ } }) : UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) := match tree with | T_Leaf None => return [] @@ -208,7 +208,7 @@ Section HaskStrongToWeak. end. - Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ) + Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}{l}(exp:@Expr _ eqVV Γ Δ ξ τ l) (ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ) : ???WeakExpr := match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 1565637..156c2ce 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -399,12 +399,10 @@ Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Defined. (* attempt to "cast" an expression by simply checking if it already had the desired type, and failing otherwise *) -Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} τ' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ) - : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ'). +Definition castExpr (we:WeakExpr)(err_msg:string) {Γ} {Δ} {ξ} {τ} {l} τ' l' (e:@Expr _ CoreVarEqDecidable Γ Δ ξ τ l) + : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ' l'). apply (addErrorMessage ("castExpr " +++ err_msg)). intros. - destruct τ as [τ l]. - destruct τ' as [τ' l']. destruct (eqd_dec l l'); [ idtac | apply (Error ("level mismatch in castExpr, invoked by "+++err_msg+++eol+++ " got: " +++(fold_left (fun x y => y+++","+++y) (map (toString ○ haskTyVarToType) l) "")+++eol+++ @@ -543,7 +541,7 @@ Definition weakExprToStrongExpr : forall (ig:CoreVar -> bool) (τ:HaskType Γ ★) (lev:HaskLevel Γ), - WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ). + WeakExpr -> ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ). refine (( fix weakExprToStrongExpr (Γ:TypeEnv) @@ -554,15 +552,15 @@ Definition weakExprToStrongExpr : forall (ig:CoreVar -> bool) (τ:HaskType Γ ★) (lev:HaskLevel Γ) - (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ (τ @@ lev) ) := + (we:WeakExpr) : ???(@Expr _ CoreVarEqDecidable Γ Δ ξ τ lev ) := addErrorMessage ("in weakExprToStrongExpr " +++ toString we) match we with | WEVar v => if ig v - then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ (τ@@lev)) - else castExpr we ("WEVar "+++toString (v:CoreVar)) (τ @@ lev) (EVar Γ Δ ξ v) + then OK ((EGlobal Γ Δ ξ (mkGlobal Γ τ v) INil lev) : Expr Γ Δ ξ τ lev) + else castExpr we ("WEVar "+++toString (v:CoreVar)) τ lev (EVar Γ Δ ξ v) - | WELit lit => castExpr we ("WELit "+++toString lit) (τ @@ lev) (ELit Γ Δ ξ lit lev) + | WELit lit => castExpr we ("WELit "+++toString lit) τ lev (ELit Γ Δ ξ lit lev) | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv => weakTypeOfWeakExpr ebody >>= fun tbody => @@ -570,24 +568,24 @@ Definition weakExprToStrongExpr : forall let ξ' := update_xi ξ lev (((ev:CoreVar),tv)::nil) in let ig' := update_ig ig ((ev:CoreVar)::nil) in weakExprToStrongExpr Γ Δ φ ψ ξ' ig' tbody' lev ebody >>= fun ebody' => - castExpr we "WELam" (τ@@lev) (ELam Γ Δ ξ tv tbody' lev ev ebody') + castExpr we "WELam" τ lev (ELam Γ Δ ξ tv tbody' lev ev ebody') | WEBrak _ ec e tbody => φ (`ec) >>= fun ec' => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => weakExprToStrongExpr Γ Δ φ ψ ξ ig tbody' ((ec')::lev) e >>= fun e' => - castExpr we "WEBrak" (τ@@lev) (EBrak Γ Δ ξ ec' tbody' lev e') + castExpr we "WEBrak" τ lev (EBrak Γ Δ ξ ec' tbody' lev e') | WEEsc _ ec e tbody => φ ec >>= fun ec'' => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => match lev with | nil => Error "ill-leveled escapification" | ec'::lev' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (<[ ec' |- tbody' ]>) lev' e - >>= fun e' => castExpr we "WEEsc" (τ@@lev) (EEsc Γ Δ ξ ec' tbody' lev' e') + >>= fun e' => castExpr we "WEEsc" τ lev (EEsc Γ Δ ξ ec' tbody' lev' e') end | WECSP _ ec e tbody => Error "FIXME: CSP not supported beyond HaskWeak stage" - | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ n e') + | WENote n e => weakExprToStrongExpr Γ Δ φ ψ ξ ig τ lev e >>= fun e' => OK (ENote _ _ _ _ _ n e') | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => @@ -607,7 +605,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ2 te ★ >>= fun τ' => weakExprToStrongExpr _ (weakCE Δ) φ2 (fun x => (ψ x) >>= fun y => OK (weakCV y)) (weakLT○ξ) ig _ (weakL lev) e - >>= fun e' => castExpr we "WETyLam2" _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e') + >>= fun e' => castExpr we "WETyLam2" _ _ (ETyLam Γ Δ ξ tv (mkTAll' τ') lev e') | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => match te with @@ -616,7 +614,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ2 te' ★ >>= fun te'' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (mkTAll te'') lev e >>= fun e' => weakTypeToTypeOfKind φ t (wtv:Kind) >>= fun t' => - castExpr we "WETyApp" _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e') + castExpr we "WETyApp" _ _ (ETyApp Γ Δ wtv (mkTAll' te'') t' ξ lev e') | _ => Error ("weakTypeToType: WETyApp body with type "+++toString te) end @@ -629,7 +627,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ t2 κ >>= fun t2'' => weakTypeToTypeOfKind φ t3 ★ >>= fun t3'' => weakExprToStrongExpr Γ Δ φ ψ ξ ig (t1'' ∼∼ t2'' ⇒ τ) lev e >>= fun e' => - castExpr we "WECoApp" _ e' >>= fun e'' => + castExpr we "WECoApp" _ _ e' >>= fun e'' => OK (ECoApp Γ Δ κ t1'' t2'' (weakCoercionToHaskCoercion _ _ _ co) τ ξ lev e'') end @@ -642,13 +640,13 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ t1 cv >>= fun t1' => weakTypeToTypeOfKind φ t2 cv >>= fun t2' => weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' => - castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') + castExpr we "WECoLam" _ _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') | WECast e co => let (t1,t2) := weakCoercionTypes co in weakTypeToTypeOfKind φ t1 ★ >>= fun t1' => weakTypeToTypeOfKind φ t2 ★ >>= fun t2' => weakExprToStrongExpr Γ Δ φ ψ ξ ig t1' lev e >>= fun e' => - castExpr we "WECast" _ + castExpr we "WECast" _ _ (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => @@ -679,7 +677,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac & - Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakLT' (tbranches' @@ lev))}}) := + Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakT' tbranches')(weakL' lev)}}) := match t with | T_Leaf None => OK [] | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => @@ -701,7 +699,7 @@ Definition weakExprToStrongExpr : forall end) alts >>= fun tree => weakExprToStrongExpr Γ Δ φ ψ ξ ig (caseType tc avars') lev escrut >>= fun escrut' => - castExpr we "ECase" (τ@@lev) (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree) + castExpr we "ECase" τ lev (ECase Γ Δ ξ lev tc tbranches' avars' escrut' tree) end)); try clear binds; try apply ConcatenableString. destruct case_some. -- 1.7.10.4