From: Adam Megacz Date: Fri, 27 May 2011 02:39:58 +0000 (-0700) Subject: rename variables to avoid Coq pickiness during extraction X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=5deda3b8240059e9969a31706d89b8a3818b184c rename variables to avoid Coq pickiness during extraction --- diff --git a/src/HaskProof.v b/src/HaskProof.v index a8b311e..2b6aa3c 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -36,7 +36,7 @@ Inductive Judg := (* information needed to define a case branch in a HaskProof *) Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} := { pcb_freevars : Tree ??(LeveledHaskType Γ ★) -; pcb_judg := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ) +; pcb_judg := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ) > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev) (vec2list (sac_types sac Γ avars)))) |- [weakLT' (branchtype @@ lev)] diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 6ba094e..69e8bb1 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -42,7 +42,7 @@ Section HaskProofToStrong. Defined. Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q, - update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q. + update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q. intros. induction l1. reflexivity. @@ -122,7 +122,7 @@ Section HaskProofToStrong. Lemma fresh_lemma'' Γ : forall types ξ lev, FreshM { varstypes : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. admit. Defined. @@ -130,8 +130,8 @@ Section HaskProofToStrong. Lemma fresh_lemma' Γ : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars -> FreshM { varstypes : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ - /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ + /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. induction types. intros; destruct a. @@ -164,7 +164,7 @@ Section HaskProofToStrong. intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _). apply FreshMon. destruct x2 as [vt2 [pf21 [pf22 pfdist]]]. - refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev + refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev (leaves vt2)) _ _; return _). apply FreshMon. simpl. @@ -204,8 +204,8 @@ Section HaskProofToStrong. Lemma fresh_lemma Γ ξ vars Σ Σ' lev : Σ = mapOptionTree ξ vars -> FreshM { vars' : _ - | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ - /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }. + | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ + /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }. intros. set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q. refine (q >>>= fun q' => return _). @@ -419,7 +419,7 @@ 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_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)). + & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)). intro pcb. intro X. simpl in X. @@ -445,10 +445,10 @@ Section HaskProofToStrong. cut (distinct (vec2list localvars'')). intro H'''. set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb. - refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _). + refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _). apply FreshMon. simpl. - unfold scbwv_ξ. + unfold scbwv_xi. rewrite vars_pf. rewrite <- mapOptionTree_compose. clear localvars_pf1. @@ -581,7 +581,7 @@ Section HaskProofToStrong. refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)). apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *. + set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *. refine (X_ ξ' (vars,,[vnew]) _ >>>= _). apply FreshMon. simpl. @@ -648,7 +648,7 @@ Section HaskProofToStrong. apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. @@ -687,7 +687,7 @@ Section HaskProofToStrong. apply FreshMon. destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_ξ ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. + set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. inversion X_. apply ileaf in X. apply ileaf in X0. @@ -751,7 +751,7 @@ Section HaskProofToStrong. apply ILeaf; simpl; intros. refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon. destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]]. - refine (X_ ((update_ξ ξ t (leaves varstypes))) + refine (X_ ((update_xi ξ t (leaves varstypes))) (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon. simpl. rewrite pf2. @@ -824,7 +824,7 @@ Section HaskProofToStrong. clear q. destruct q' as [varstypes [pf1 [pf2 distpf]]]. exists (mapOptionTree (@fst _ _) varstypes). - exists (update_ξ ξ l (leaves varstypes)). + exists (update_xi ξ l (leaves varstypes)). symmetry; auto. refine (return _). exists []. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index d52acb9..ed3cd92 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -25,7 +25,7 @@ Section HaskStrong. { scbwv_exprvars : vec VV (sac_numExprVars sac) ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars) ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types sac Γ atypes) - ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) + ; scbwv_xi := fun ξ lev => update_xi (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. @@ -37,8 +37,8 @@ Section HaskStrong. | 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_ξ ξ l ((ev,t1)::nil)) (t2@@l) -> Expr Γ Δ ξ (t1--->t2@@l) - | ELet : ∀ Γ Δ ξ tv t l ev,Expr Γ Δ ξ (tv@@l)->Expr Γ Δ (update_ξ ξ l ((ev,tv)::nil))(t@@l) -> Expr Γ Δ ξ (t@@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, @@ -55,15 +55,15 @@ Section HaskStrong. Expr Γ Δ ξ (caseType tc atypes @@ l) -> Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } } -> Expr Γ Δ ξ (tbranches @@ l) | ELetRec : ∀ Γ Δ ξ l τ vars, distinct (leaves (mapOptionTree (@fst _ _) vars)) -> - let ξ' := update_ξ ξ l (leaves vars) in + let ξ' := update_xi ξ l (leaves vars) in ELetRecBindings Γ Δ ξ' l vars -> Expr Γ Δ ξ' (τ@@l) -> Expr Γ Δ ξ (τ@@l) diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 5f3baa3..0ad9214 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -330,7 +330,7 @@ Lemma updating_stripped_tree_is_inert' {Γ} lev (ξ:VV -> LeveledHaskType Γ ★) lv tree2 : - mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) + mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2) = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2). induction tree2. @@ -459,10 +459,10 @@ Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (ap inversion H; auto. Qed. -Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : +Lemma update_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : forall v1 v2, distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) -> - mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (update_xi ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) = mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). induction varstypes; intros. destruct a; simpl; [ idtac | reflexivity ]. @@ -510,11 +510,11 @@ Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstyp repeat rewrite ass_app in *; auto. Qed. -Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : +Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) : distinct (map (@fst _ _) (leaves varstypes)) -> - mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = + mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes). - set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q. + set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q. simpl in q. rewrite <- app_nil_end in q. apply q. @@ -543,9 +543,9 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } } ): Tree ??VV := match alts with @@ -563,9 +563,9 @@ end. Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } }) : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. destruct alt. @@ -943,7 +943,7 @@ Definition factorContextRightAndWeaken'' Defined. Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : - mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) + mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) = mapOptionTree ξ (stripOutVars (v :: nil) tree). set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p. rewrite p. @@ -980,8 +980,8 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches : Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))), - ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> - LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches -> + ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] -> + LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches -> ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]]. (* NOTE: how we interpret stuff here affects the order-of-side-effects *) @@ -995,10 +995,10 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : apply disti. rewrite mapleaves in disti'. - set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma. + set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma. rewrite <- mapOptionTree_compose in ξlemma. - set ((update_ξ ξ lev (leaves tree))) as ξ' in *. + set ((update_xi ξ lev (leaves tree))) as ξ' in *. set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx. set (mapOptionTree (@fst _ _) tree) as pctx. set (mapOptionTree ξ' pctx) as passback. @@ -1037,12 +1037,12 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac, forall l ξ, - vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) = + vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) = vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)). intros. - unfold scbwv_ξ. + unfold scbwv_xi. unfold scbwv_varstypes. - set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) + set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l) (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes)))) ) as q. rewrite <- mapleaves' in q. @@ -1068,8 +1068,8 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e (alts':Tree ??{sac : StrongAltCon & {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac & - Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}), + Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches @@ l))}}), (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) (mapOptionTree mkProofCaseBranch alts')) @@ -1111,7 +1111,7 @@ Definition expr2proof : | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody) | ELetRec Γ Δ ξ lev t tree disti branches ebody => - let ξ' := update_ξ ξ lev (leaves tree) in + let ξ' := update_xi ξ lev (leaves tree) in let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody) ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★)) (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree') @@ -1134,9 +1134,9 @@ Definition expr2proof : let dcsp := ((fix mkdcsp (alts: Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac - & Expr (sac_Γ sac Γ) - (sac_Δ sac Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) + & Expr (sac_gamma sac Γ) + (sac_delta sac Γ atypes (weakCK'' Δ)) + (scbwv_xi scb ξ l) (weakLT' (tbranches@@l)) } }) : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) := match alts as ALTS return ND Rule [] @@ -1179,13 +1179,13 @@ Definition expr2proof : destruct case_ELam; intros. unfold mapOptionTree; simpl; fold (mapOptionTree ξ). eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. - set (update_ξ ξ lev ((v,t1)::nil)) as ξ'. + set (update_xi ξ lev ((v,t1)::nil)) as ξ'. set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. eapply RArrange in pfx. unfold mapOptionTree in pfx; simpl in pfx. unfold ξ' in pfx. rewrite updating_stripped_tree_is_inert in pfx. - unfold update_ξ in pfx. + unfold update_xi in pfx. destruct (eqd_dec v v). eapply nd_comp; [ idtac | apply (nd_rule pfx) ]. clear pfx. @@ -1203,15 +1203,15 @@ Definition expr2proof : eapply nd_comp; [ apply pf_body | idtac ]. fold (@mapOptionTree VV). fold (mapOptionTree ξ). - set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. + set (update_xi ξ v ((lev,tv)::nil)) as ξ'. set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. unfold ξ' in n. rewrite updating_stripped_tree_is_inert in n. - unfold update_ξ in n. + unfold update_xi in n. destruct (eqd_dec lev lev). unfold ξ'. - unfold update_ξ. + unfold update_xi. eapply RArrange in n. apply (nd_rule n). assert False. apply n0; auto. inversion H. @@ -1266,15 +1266,15 @@ Definition expr2proof : rewrite mapleaves'. simpl. rewrite <- mapOptionTree_compose. - unfold scbwv_ξ. + unfold scbwv_xi. rewrite <- mapleaves'. rewrite vec2list_map_list2vec. - unfold sac_Γ. + unfold sac_gamma. rewrite <- (scbwv_coherent scbx l ξ). rewrite <- vec2list_map_list2vec. rewrite mapleaves'. set (@factorContextRightAndWeaken'') as q. - unfold scbwv_ξ. + unfold scbwv_xi. set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z. unfold scbwv_varstypes in z. rewrite vec2list_map_list2vec in z. @@ -1285,7 +1285,7 @@ Definition expr2proof : replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). apply q. - apply (sac_Δ sac Γ atypes (weakCK'' Δ)). + apply (sac_delta sac Γ atypes (weakCK'' Δ)). rewrite leaves_unleaves. apply (scbwv_exprvars_distinct scbx). rewrite leaves_unleaves. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index 25ecd7b..d86d05b 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -95,16 +95,16 @@ Section HaskStrongToWeak. Context {VV}{eqVV:EqDecidable VV}{toStringVV:ToString VV}. - Definition update_χ (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar := + Definition update_chi (χ:VV->???WeakExprVar)(vv:VV)(ev':WeakExprVar) : VV->???WeakExprVar := fun vv' => if eqd_dec vv vv' then OK ev' else χ vv'. - Fixpoint update_χ' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar := + Fixpoint update_chi' (χ:VV->???WeakExprVar)(varsexprs:list (VV * WeakExprVar)) : VV->???WeakExprVar := match varsexprs with | nil => χ - | (vv,wev)::rest => update_χ (update_χ' χ rest) vv wev + | (vv,wev)::rest => update_chi (update_chi' χ rest) vv wev end. Fixpoint exprToWeakExpr {Γ}{Δ}{ξ}{τ}(χ:VV->???WeakExprVar)(exp:@Expr _ eqVV Γ Δ ξ τ) @@ -116,12 +116,12 @@ Section HaskStrongToWeak. ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g)) | ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite ; bind ev' = mkWeakExprVar tv' - ; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite + ; bind e' = exprToWeakExpr (update_chi χ cv ev') e ite ; return WELam ev' e' | ELet Γ' _ _ t _ _ ev e1 e2 => fun ite => bind tv' = typeToWeakType t ite ; bind e1' = exprToWeakExpr χ e1 ite ; bind ev' = mkWeakExprVar tv' - ; bind e2' = exprToWeakExpr (update_χ χ ev ev') e2 ite + ; bind e2' = exprToWeakExpr (update_chi χ ev ev') e2 ite ; return WELet ev' e1' e2' | ELit _ _ _ lit _ => fun ite => return WELit lit | EApp Γ' _ _ _ _ _ e1 e2 => fun ite => bind e1' = exprToWeakExpr χ e1 ite @@ -172,7 +172,7 @@ Section HaskStrongToWeak. ; bind v' = mkWeakExprVar tleaf ; return ((fst vt),v')) varstypes) - ; let χ' := update_χ' χ exprvars in + ; let χ' := update_chi' χ exprvars in bind e'' = exprToWeakExpr χ' e (snd evars_ite) ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')] | T_Branch b1 b2 => bind b1' = caseBranches b1 @@ -188,7 +188,7 @@ Section HaskStrongToWeak. ; bind v' = mkWeakExprVar tleaf ; return ((fst vt),v')) (leaves vars)) - ; let χ' := update_χ' χ vars' in + ; let χ' := update_chi' χ vars' in bind elrb' = exprLetRec2WeakExprLetRec χ' elrb ite ; bind e' = exprToWeakExpr χ' e ite ; return WELetRec elrb' e' diff --git a/src/HaskStrongTypes.v b/src/HaskStrongTypes.v index 764e95f..1287b0b 100644 --- a/src/HaskStrongTypes.v +++ b/src/HaskStrongTypes.v @@ -439,10 +439,10 @@ Record StrongAltCon {tc:TyCon} := ; sac_numExprVars : nat ; sac_ekinds : vec Kind sac_numExTyVars ; sac_kinds := app (tyConKind tc) (vec2list sac_ekinds) -; sac_Γ := fun Γ => app (vec2list sac_ekinds) Γ -; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_Γ Γ)) sac_numCoerVars -; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_Γ Γ) ★) sac_numExprVars -; sac_Δ := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ +; sac_gamma := fun Γ => app (vec2list sac_ekinds) Γ +; sac_coercions : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskCoercionKind (sac_gamma Γ)) sac_numCoerVars +; sac_types : forall Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)), vec (HaskType (sac_gamma Γ) ★) sac_numExprVars +; sac_delta := fun Γ (atypes:IList _ (HaskType Γ) (tyConKind tc)) Δ => app (vec2list (sac_coercions Γ atypes)) Δ }. Coercion sac_tc : StrongAltCon >-> TyCon. Coercion sac_altcon : StrongAltCon >-> WeakAltCon. @@ -462,7 +462,7 @@ Definition literalType (lit:HaskLiteral){Γ} : HaskType Γ ★. Notation "a ∼∼∼ b" := (@mkHaskCoercionKind _ _ a b) (at level 18). -Fixpoint update_ξ +Fixpoint update_xi `{EQD_VV:EqDecidable VV}{Γ} (ξ:VV -> LeveledHaskType Γ ★) (lev:HaskLevel Γ) @@ -470,12 +470,12 @@ Fixpoint update_ξ : VV -> LeveledHaskType Γ ★ := match vt with | nil => ξ - | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_ξ ξ lev tl) v' + | (v,τ)::tl => fun v' => if eqd_dec v v' then τ @@ lev else (update_xi ξ lev tl) v' end. -Lemma update_ξ_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v, +Lemma update_xi_lemma0 `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:list (VV*_)) v, not (In v (map (@fst _ _) varstypes)) -> - (update_ξ ξ lev varstypes) v = ξ v. + (update_xi ξ lev varstypes) v = ξ v. intros. induction varstypes. reflexivity. diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index 7dd93ad..1565637 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -25,7 +25,7 @@ Open Scope string_scope. Definition TyVarResolver Γ := forall wt:WeakTypeVar, ???(HaskTyVar Γ wt). Definition CoVarResolver Γ Δ := forall wt:WeakCoerVar, ???(HaskCoVar Γ Δ). -Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). +Definition upPhi {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:Kind)::Γ). unfold TyVarResolver. refine (fun tv' => if eqd_dec tv tv' @@ -34,12 +34,12 @@ Definition upφ {Γ}(tv:WeakTypeVar)(φ:TyVarResolver Γ) : TyVarResolver ((tv:K rewrite <- _H; apply fresh. Defined. -Definition upφ' {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) +Definition upPhi2 {Γ}(tvs:list WeakTypeVar)(φ:TyVarResolver Γ) : (TyVarResolver (app (map (fun tv:WeakTypeVar => tv:Kind) tvs) Γ)). induction tvs. apply φ. simpl. - apply upφ. + apply upPhi. apply IHtvs. Defined. @@ -54,7 +54,7 @@ Definition substPhi {Γ:TypeEnv}(κ κ':Kind)(θ:HaskType Γ κ) : HaskType (κ: apply X. Defined. -Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. +Definition substphi {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ κ) lk){κ} : HaskType (app lk Γ) κ -> HaskType Γ κ. induction lk. intro q; apply q. simpl. @@ -71,8 +71,8 @@ Definition substφ {Γ:TypeEnv}(lk:list Kind)(θ:IList _ (fun κ => HaskType Γ (* this is a StrongAltCon plus some stuff we know about StrongAltCons which we've built ourselves *) Record StrongAltConPlusJunk {tc:TyCon} := { sacpj_sac : @StrongAltCon tc -; sacpj_φ : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_Γ sacpj_sac Γ)) -; sacpj_ψ : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_Δ sacpj_sac Γ atypes (weakCK'' Δ)) +; sacpj_phi : forall Γ (φ:TyVarResolver Γ ), (TyVarResolver (sac_gamma sacpj_sac Γ)) +; sacpj_psi : forall Γ Δ atypes (ψ:CoVarResolver Γ Δ), CoVarResolver _ (sac_delta sacpj_sac Γ atypes (weakCK'' Δ)) }. Implicit Arguments StrongAltConPlusJunk [ ]. Coercion sacpj_sac : StrongAltConPlusJunk >-> StrongAltCon. @@ -83,9 +83,9 @@ Variable emptyφ : TyVarResolver nil. Definition mkPhi (lv:list WeakTypeVar) : (TyVarResolver (map (fun x:WeakTypeVar => x:Kind) lv)). - set (upφ'(Γ:=nil) lv emptyφ) as φ'. - rewrite <- app_nil_end in φ'. - apply φ'. + set (upPhi2(Γ:=nil) lv emptyφ) as φ2. + rewrite <- app_nil_end in φ2. + apply φ2. Defined. Definition dataConExKinds dc := vec_map (fun x:WeakTypeVar => (x:Kind)) (list2vec (dataConExTyVars dc)). @@ -125,7 +125,7 @@ Definition weakTypeToType : forall {Γ:TypeEnv}(φ:TyVarResolver Γ)(t:WeakType) | WIParam _ ty => let case_WIParam := tt in Error "weakTypeToType: WIParam not implemented" | WAppTy t1 t2 => let case_WAppTy := tt in weakTypeToType _ φ t1 >>= fun t1' => weakTypeToType _ φ t2 >>= fun t2' => _ | WTyVarTy v => let case_WTyVarTy := tt in φ v >>= fun v' => _ - | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upφ wtv φ) t >>= fun t => _ + | WForAllTy wtv t => let case_WForAllTy := tt in weakTypeToType _ (upPhi wtv φ) t >>= fun t => _ | WCodeTy ec tbody => let case_WCodeTy := tt in weakTypeToType _ φ tbody >>= fun tbody' => φ (@fixkind ECKind ec) >>= fun ec' => _ | WCoFunTy t1 t2 t3 => let case_WCoFunTy := tt in @@ -240,9 +240,9 @@ Definition weakTypeToType' {Γ} : IList Kind (HaskType Γ) (vec2list (tyConKinds intro ct. apply (addErrorMessage "weakTypeToType'"). set (ilmap (@weakT' _ (vec2list (dataConExKinds dc))) avars) as avars'. - set (@substφ _ _ avars') as q. - set (upφ' (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ'. - set (@weakTypeToType _ φ' ct) as t. + set (@substphi _ _ avars') as q. + set (upPhi2 (tyConTyVars tc) (mkPhi (dataConExTyVars dc))) as φ2. + set (@weakTypeToType _ φ2 ct) as t. destruct t as [|t]; try apply (Error error_message). destruct t as [tk t]. matchThings tk ★ "weakTypeToType'". @@ -327,17 +327,17 @@ Lemma weakCV' : forall {Γ}{Δ} Γ', Definition mkStrongAltConPlusJunk : StrongAltConPlusJunk tc. refine {| sacpj_sac := mkStrongAltCon - ; sacpj_φ := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv')) - ; sacpj_ψ := + ; sacpj_phi := fun Γ φ => (fun htv => φ htv >>= fun htv' => OK (weakV' htv')) + ; sacpj_psi := fun Γ Δ avars ψ => (fun htv => ψ htv >>= fun htv' => OK (_ (weakCV' (vec2list (sac_ekinds mkStrongAltCon)) htv'))) |}. intro. - unfold sac_Γ. + unfold sac_gamma. unfold HaskCoVar in *. intros. apply (x TV CV env). simpl in cenv. - unfold sac_Δ in *. + unfold sac_delta in *. unfold InstantiatedCoercionEnv in *. apply vec_chop' in cenv. apply cenv. @@ -371,13 +371,13 @@ Definition mkStrongAltConPlusJunk' (tc : TyCon)(alt:WeakAltCon) : ???(@StrongAlt ; sac_altcon := WeakLitAlt h |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. rewrite weakCK'_nil_inert. apply ψ. apply OK; refine {| sacpj_sac := {| sac_ekinds := vec_nil ; sac_coercions := fun _ _ => vec_nil ; sac_types := fun _ _ => vec_nil ; sac_altcon := WeakDEFAULT |} |}. intro; intro φ; apply φ. - intro; intro; intro; intro ψ. simpl. unfold sac_Γ; simpl. unfold sac_Δ; simpl. + intro; intro; intro; intro ψ. simpl. unfold sac_gamma; simpl. unfold sac_delta; simpl. rewrite weakCK'_nil_inert. apply ψ. Defined. @@ -387,7 +387,7 @@ Definition weakExprVarToWeakType : WeakExprVar -> WeakType := Variable weakCoercionToHaskCoercion : forall Γ Δ κ, WeakCoercion -> HaskCoercion Γ Δ κ. -Definition weakψ {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) : +Definition weakPsi {Γ}{Δ:CoercionEnv Γ} {κ}(ψ:WeakCoerVar -> ???(HaskCoVar Γ Δ)) : WeakCoerVar -> ???(HaskCoVar Γ (κ::Δ)). intros. refine (ψ X >>= _). @@ -567,7 +567,7 @@ Definition weakExprToStrongExpr : forall | WELam ev ebody => weakTypeToTypeOfKind φ ev ★ >>= fun tv => weakTypeOfWeakExpr ebody >>= fun tbody => weakTypeToTypeOfKind φ tbody ★ >>= fun tbody' => - let ξ' := update_ξ ξ lev (((ev:CoreVar),tv)::nil) in + 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') @@ -591,7 +591,7 @@ Definition weakExprToStrongExpr : forall | WELet v ve ebody => weakTypeToTypeOfKind φ v ★ >>= fun tv => weakExprToStrongExpr Γ Δ φ ψ ξ ig tv lev ve >>= fun ve' => - weakExprToStrongExpr Γ Δ φ ψ (update_ξ ξ lev (((v:CoreVar),tv)::nil)) + weakExprToStrongExpr Γ Δ φ ψ (update_xi ξ lev (((v:CoreVar),tv)::nil)) (update_ig ig ((v:CoreVar)::nil)) τ lev ebody >>= fun ebody' => OK (ELet _ _ _ tv _ lev (v:CoreVar) ve' ebody') @@ -602,18 +602,18 @@ Definition weakExprToStrongExpr : forall weakExprToStrongExpr Γ Δ φ ψ ξ ig (t2'--->τ) lev e1 >>= fun e1' => OK (EApp _ _ _ _ _ _ e1' e2') - | WETyLam tv e => let φ' := upφ tv φ in + | WETyLam tv e => let φ2 := upPhi tv φ in weakTypeOfWeakExpr e >>= fun te => - weakTypeToTypeOfKind φ' te ★ >>= fun τ' => - weakExprToStrongExpr _ (weakCE Δ) φ' + 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') | WETyApp e t => weakTypeOfWeakExpr e >>= fun te => match te with | WForAllTy wtv te' => - let φ' := upφ wtv φ in - weakTypeToTypeOfKind φ' te' ★ >>= fun te'' => + let φ2 := upPhi wtv φ in + 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') @@ -641,7 +641,7 @@ Definition weakExprToStrongExpr : forall weakTypeToTypeOfKind φ te ★ >>= fun te' => weakTypeToTypeOfKind φ t1 cv >>= fun t1' => weakTypeToTypeOfKind φ t2 cv >>= fun t2' => - weakExprToStrongExpr Γ (_ :: Δ) φ (weakψ ψ) ξ ig te' lev e >>= fun e' => + weakExprToStrongExpr Γ (_ :: Δ) φ (weakPsi ψ) ξ ig te' lev e >>= fun e' => castExpr we "WECoLam" _ (ECoLam Γ Δ cv te' t1' t2' ξ lev e') | WECast e co => let (t1,t2) := weakCoercionTypes co in @@ -652,7 +652,7 @@ Definition weakExprToStrongExpr : forall (ECast Γ Δ ξ t1' t2' (weakCoercionToHaskCoercion _ _ _ co) lev e') | WELetRec rb e => - let ξ' := update_ξ ξ lev _ in + let ξ' := update_xi ξ lev _ in let ig' := update_ig ig (map (fun x:(WeakExprVar*_) => (fst x):CoreVar) (leaves rb)) in let binds := (fix binds (t:Tree ??(WeakExprVar * WeakExpr)) @@ -679,7 +679,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_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) := + Expr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ))(scbwv_xi scb ξ lev)(weakLT' (tbranches' @@ lev))}}) := match t with | T_Leaf None => OK [] | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => @@ -688,9 +688,9 @@ Definition weakExprToStrongExpr : forall >>= fun exprvars' => (let case_pf := tt in _) >>= fun pf => let scb := @Build_StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc Γ avars' sac exprvars' pf in - weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) - (sacpj_ψ sac _ _ avars' ψ) - (scbwv_ξ scb ξ lev) + weakExprToStrongExpr (sac_gamma sac Γ) (sac_delta sac Γ avars' (weakCK'' Δ)) (sacpj_phi sac _ φ) + (sacpj_psi sac _ _ avars' ψ) + (scbwv_xi scb ξ lev) (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb)))) (weakT' tbranches') (weakL' lev) ebranch >>= fun ebranch' => let case_case := tt in OK [ _ ]