From: Adam Megacz Date: Mon, 21 Mar 2011 00:30:30 +0000 (-0700) Subject: make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=b3214686b18b2d6f6905394494da8d1c17587bdb;hp=3d4dc42bf3f6e2ad7dc35b14ecb8facdb89e9324 make StrongAlt a parameter rather than field in StrongCaseBranch and ProofCaseBranch --- diff --git a/src/Extraction.v b/src/Extraction.v index d1c84e4..c23d1c5 100644 --- a/src/Extraction.v +++ b/src/Extraction.v @@ -25,10 +25,10 @@ Require Import HaskProof. Require Import HaskCoreToWeak. Require Import HaskWeakToStrong. Require Import HaskStrongToProof. -Require Import HaskProofToStrong. Require Import HaskProofToLatex. Require Import HaskStrongToWeak. Require Import HaskWeakToCore. +Require Import HaskProofToStrong. Open Scope string_scope. Extraction Language Haskell. diff --git a/src/General.v b/src/General.v index 4e73755..2a1a398 100644 --- a/src/General.v +++ b/src/General.v @@ -893,7 +893,7 @@ Lemma unleaves_injective : forall T (t1 t2:list T), unleaves t1 = unleaves t2 -> Lemma fst_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@fst _ _) (vec_zip v1 v2) = v1. admit. - Qed. + Defined. Lemma snd_zip : forall T Q n (v1:vec T n)(v2:vec Q n), vec_map (@snd _ _) (vec_zip v1 v2) = v2. admit. diff --git a/src/HaskProof.v b/src/HaskProof.v index 046e28e..55b0b03 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -50,15 +50,14 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := Coercion UJudg2judg : UJudg >-> Judg. (* information needed to define a case branch in a HaskProof *) -Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars} := -{ pcb_scb : @StrongAltCon tc -; pcb_freevars : Tree ??(LeveledHaskType Γ ★) -; pcb_judg := sac_Γ pcb_scb Γ > sac_Δ pcb_scb Γ avars (map weakCK' Δ) +Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} := +{ pcb_freevars : Tree ??(LeveledHaskType Γ ★) +; pcb_judg := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ) > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev) - (vec2list (sac_types pcb_scb Γ avars)))) + (vec2list (sac_types sac Γ avars)))) |- [weakLT' (branchtype @@ lev)] }. -Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon. +(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*) Implicit Arguments ProofCaseBranch [ ]. (* Figure 3, production $\vdash_E$, Uniform rules *) @@ -111,11 +110,11 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] | RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ] | RCase : forall Γ Δ lev tc Σ avars tbranches - (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)), + (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }), Rule - ((mapOptionTree pcb_judg alts),, + ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),, [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) - [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches @@ lev ] ] + [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches @@ lev ] ] . Coercion RURule : URule >-> Rule. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 6f75235..f907514 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -125,6 +125,14 @@ Section HaskProofToStrong. reflexivity. Qed. + Lemma fresh_lemma'' Γ + : forall types ξ lev, + FreshM { varstypes : _ + | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev) + /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }. + admit. + Defined. + Lemma fresh_lemma' Γ : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars -> FreshM { varstypes : _ @@ -415,72 +423,88 @@ Section HaskProofToStrong. apply IHvarstypes2; inversion X; auto. Defined. - Definition case_helper tc Γ Δ lev tbranches avars ξ (Σ:Tree ??VV) : - forall pcb : ProofCaseBranch tc Γ Δ lev tbranches avars, - judg2exprType (pcb_judg pcb) -> - (pcb_freevars pcb) = mapOptionTree ξ Σ -> - FreshM - {scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars & - Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars (weakCK'' Δ)) - (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev))}. + Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }. + refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with + | INone => T_Leaf None + | ILeaf x y => T_Leaf (Some _) + | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2) + end). + exists x; auto. + Defined. - intros. + Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x }) + : ITree { x:X & F x } (fun x => J (projT1 x)) t + -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t). + intro it. + induction it; simpl in *. + apply INone. + apply ILeaf. + apply f. + simpl; apply IBranch; auto. + Defined. + + Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }). + refine (fix rec t := match t with + | T_Leaf None => T_Leaf None + | T_Leaf (Some x) => T_Leaf (Some _) + | T_Branch b1 b2 => T_Branch (rec b1) (rec b2) + end). + destruct x as [x fx]. + refine (bind fx' = fx ; return _). + apply FreshMon. + exists x. + apply fx'. + Defined. + + Definition case_helper tc Γ Δ lev tbranches avars ξ : + forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac}, + 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)). + intro pcb. + intro X. simpl in X. - destruct pcb. + simpl. + destruct pcb as [sac pcb]. simpl in *. - set (sac_types pcb_scb _ avars) as boundvars. - refine (fresh_lemma' _ (unleaves (vec2list boundvars)) Σ (mapOptionTree weakLT' pcb_freevars) (weakLT' ○ ξ) (weakL' lev) _ - >>>= fun ξvars => _). apply FreshMon. - rewrite H. - rewrite <- mapOptionTree_compose. - reflexivity. - destruct ξvars as [ exprvars [pf1 [pf2 pfdistinct]]]. - set (list2vec (leaves (mapOptionTree (@fst _ _) exprvars))) as exprvars'. - - assert (distinct (vec2list exprvars')) as pfdistinct'. - unfold exprvars'. - rewrite vec2list_list2vec. - apply pfdistinct. - - assert (sac_numExprVars pcb_scb = Datatypes.length (leaves (mapOptionTree (@fst _ _) exprvars))) as H'. - rewrite <- mapOptionTree_compose in pf2. - simpl in pf2. - rewrite mapleaves. - rewrite <- map_preserves_length. - rewrite map_preserves_length with (f:= - (@update_ξ VV eqdec_vv (@sac_Γ tc pcb_scb Γ) - (@weakLT' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) ★ ○ ξ) - (@weakL' Γ (@vec2list (@sac_numExTyVars tc pcb_scb) Kind (@sac_ekinds tc pcb_scb)) lev) - (@leaves (VV * HaskType (@sac_Γ tc pcb_scb Γ) ★) exprvars) ○ @fst VV (HaskType (@sac_Γ tc pcb_scb Γ) ★))). - rewrite <- mapleaves. - rewrite pf2. - rewrite <- mapleaves'. - rewrite leaves_unleaves. - rewrite vec2list_map_list2vec. - rewrite vec2list_len. - reflexivity. - - clear pfdistinct'. - rewrite <- H' in exprvars'. - clear H'. - assert (distinct (vec2list exprvars')) as pfdistinct'. - admit. - - set (@Build_StrongCaseBranchWithVVs VV _ tc _ avars pcb_scb exprvars' pfdistinct') as scb. - set (scbwv_ξ scb ξ lev) as ξ'. - refine (X ξ' (Σ,,(unleaves (vec2list exprvars'))) _ >>>= fun X' => return _). apply FreshMon. + + destruct X. + destruct s as [vars vars_pf]. + + refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars + (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _). + apply FreshMon. + rewrite vars_pf. + rewrite <- mapOptionTree_compose. + reflexivity. + destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]]. + set (mapOptionTree (@fst _ _) localvars) as localvars'. + + set (list2vec (leaves localvars')) as localvars''. + cut (length (leaves localvars') = sac_numExprVars sac). intro H''. + rewrite H'' in localvars''. + 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 _). + apply FreshMon. simpl. - unfold ξ'. unfold scbwv_ξ. + rewrite vars_pf. + rewrite <- mapOptionTree_compose. + clear localvars_pf1. simpl. - admit. - - apply ileaf in X'. - simpl in X'. - exists scb. - unfold weakCK''. - unfold ξ' in X'. - apply X'. + rewrite mapleaves'. + + admit. + + exists scb. + apply ileaf in q. + apply q. + + admit. + admit. Defined. Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) := @@ -490,18 +514,46 @@ Section HaskProofToStrong. | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2') end. - Lemma itree_mapOptionTree : forall T T' F (f:T->T') t, - ITree _ F (mapOptionTree f t) -> - ITree _ (F ○ f) t. + Definition gather_branch_variables + Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon & + ProofCaseBranch tc Γ Δ lev tbranches avars sac}) + : + forall vars, + mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars + -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts) + -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q))) + { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' }) + alts. + induction alts; + intro vars; + intro pf; + intro source. + destruct a; [ idtac | apply INone ]. + simpl in *. + apply ileaf in source. + apply ILeaf. + destruct s as [sac pcb]. + simpl in *. + split. intros. - induction t; try destruct a; simpl in *. - apply ILeaf. - inversion X; auto. - apply INone. - apply IBranch. - apply IHt1; inversion X; auto. - apply IHt2; inversion X; auto. - Defined. + eapply source. + apply H. + clear source. + + exists vars. + auto. + + simpl in pf. + destruct vars; try destruct o; simpl in pf; inversion pf. + simpl in source. + inversion source. + subst. + apply IBranch. + apply (IHalts1 vars1 H0 X); auto. + apply (IHalts2 vars2 H1 X0); auto. + + Defined. + Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j. @@ -729,27 +781,33 @@ Section HaskProofToStrong. subst. apply ileaf in X0. simpl in X0. - set (mapOptionTreeAndFlatten pcb_freevars alts) as Σalts in *. - refine (bind ξvars = fresh_lemma' _ (mapOptionTree unlev (Σalts,,Σ)) _ _ _ lev H ; _). - apply FreshMon. - destruct vars; try destruct o; inversion H; clear H. - rename vars1 into varsalts. - rename vars2 into varsΣ. - refine ( _ >>>= fun Y => X0 ξ varsΣ _ >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto. + (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free + * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *) + rename Σ into body_freevars_types. + rename vars into all_freevars. + rename X0 into body_expr. + rename X into alts_exprs. + + destruct all_freevars; try destruct o; inversion H. + rename all_freevars2 into body_freevars. + rename all_freevars1 into alts_freevars. + + set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q. + set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'. + apply fix_indexing in alts_exprs'. + simpl in alts_exprs'. + apply unindex_tree in alts_exprs'. + simpl in alts_exprs'. + apply fix2 in alts_exprs'. + apply treeM in alts_exprs'. + + refine ( alts_exprs' >>>= fun Y => + body_expr ξ _ _ + >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto. apply FreshMon. - destruct ξvars as [varstypes [pf1 pf2]]. - - apply treeM. - apply itree_mapOptionTree in X. - refine (itree_to_tree (itmap _ X)). - intros. - eapply case_helper. - apply X1. - instantiate (1:=varsΣ). - rewrite <- H2. - admit. apply FreshMon. + apply H2. Defined. Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c. diff --git a/src/HaskStrong.v b/src/HaskStrong.v index 151e8d2..1f4d03b 100644 --- a/src/HaskStrong.v +++ b/src/HaskStrong.v @@ -20,15 +20,14 @@ Section HaskStrong. (* a StrongCaseBranchWithVVs contains all the data found in a case branch except the expression itself *) - Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)} := - { scbwv_sac : @StrongAltCon tc - ; scbwv_exprvars : vec VV (sac_numExprVars scbwv_sac) + Record StrongCaseBranchWithVVs {tc:TyCon}{Γ}{atypes:IList _ (HaskType Γ) (tyConKind tc)}{sac:@StrongAltCon tc} := + { scbwv_exprvars : vec VV (sac_numExprVars sac) ; scbwv_exprvars_distinct : distinct (vec2list scbwv_exprvars) - ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types scbwv_sac Γ atypes) + ; scbwv_varstypes := vec_zip scbwv_exprvars (sac_types sac Γ atypes) ; scbwv_ξ := fun ξ lev => update_ξ (weakLT'○ξ) (weakL' lev) (vec2list scbwv_varstypes) }. Implicit Arguments StrongCaseBranchWithVVs [[Γ]]. - Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon. + (*Coercion scbwv_sac : StrongCaseBranchWithVVs >-> StrongAltCon.*) Inductive Expr : forall Γ (Δ:CoercionEnv Γ), (VV -> LeveledHaskType Γ ★) -> LeveledHaskType Γ ★ -> Type := @@ -54,11 +53,12 @@ Section HaskStrong. Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)@@(weakL l))-> Expr Γ Δ ξ (HaskTAll κ σ @@ l) | ECase : forall Γ Δ ξ l tc tbranches atypes, Expr Γ Δ ξ (caseType tc atypes @@ l) -> - Tree ??{ scb : StrongCaseBranchWithVVs tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) + Tree ??{ sac : _ + & { scb : StrongCaseBranchWithVVs tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) } -> + (weakLT' (tbranches@@l)) } } -> Expr Γ Δ ξ (tbranches @@ l) | ELetRec : ∀ Γ Δ ξ l τ vars, diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index fa7dcae..79e16cd 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -348,15 +348,15 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ? in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts | ECase Γ Δ ξ l tc tbranches atypes e' alts => ((fix varsfromalts (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) + Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) } + (weakLT' (tbranches@@l)) } } ): Tree ??VV := match alts with | T_Leaf None => [] - | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h)) + | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h))) | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2) end) alts),,(expr2antecedent e') end @@ -368,15 +368,18 @@ match elrb with end. Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes} - (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) +(alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) }) - : ProofCaseBranch tc Γ Δ l tbranches atypes. + (weakLT' (tbranches@@l)) } }) + : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }. + destruct alt. + exists x. exact - {| pcb_scb := projT1 alt - ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt))) + {| pcb_freevars := mapOptionTree ξ + (stripOutVars (vec2list (scbwv_exprvars (projT1 s))) + (expr2antecedent (projT2 s))) |}. Defined. @@ -693,16 +696,16 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : apply disti. Defined. -Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} : - forall scb:StrongCaseBranchWithVVs _ _ tc atypes, +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 (fun t => t @@ weakL' l) (sac_types (scbwv_sac scb) _ atypes)). + vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)). intros. unfold scbwv_ξ. unfold scbwv_varstypes. set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l) - (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types (scbwv_sac scb) Γ atypes)))) + (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes)))) ) as q. rewrite <- mapleaves' in q. rewrite <- mapleaves' in q. @@ -722,18 +725,28 @@ Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _} : apply scbwv_exprvars_distinct. Qed. -Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts', - mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')) - = ((mapOptionTreeAndFlatten pcb_freevars (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)). + +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))}}), + + (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) + (mapOptionTree mkProofCaseBranch alts')) + ,, + mapOptionTree ξ (expr2antecedent e) = + mapOptionTree ξ + (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')). intros. simpl. Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end. hack. induction alts'. - simpl. - destruct a. + destruct a; simpl. + destruct s; simpl. unfold mkProofCaseBranch. - simpl. reflexivity. reflexivity. simpl. @@ -744,7 +757,6 @@ Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e alts', reflexivity. Qed. - Definition expr2proof : forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ), ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]]. @@ -783,18 +795,19 @@ Definition expr2proof : | ECase Γ Δ ξ l tc tbranches atypes e alts' => let dcsp := ((fix mkdcsp (alts: - Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes - & Expr (sac_Γ scb Γ) - (sac_Δ scb Γ atypes (weakCK'' Δ)) + Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac + & Expr (sac_Γ sac Γ) + (sac_Δ sac Γ atypes (weakCK'' Δ)) (scbwv_ξ scb ξ l) - (weakLT' (tbranches@@l)) }) - : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) := - match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with + (weakLT' (tbranches@@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 | T_Leaf None => let case_nil := tt in _ | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2) | T_Leaf (Some x) => - match x as X return ND Rule [] [(pcb_judg ○ mkProofCaseBranch) X] with - existT scbx ex => + 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) end end) alts') @@ -912,10 +925,6 @@ Definition expr2proof : clear o x alts alts' e. eapply nd_comp; [ apply e' | idtac ]. clear e'. - set (existT - (fun scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes => - Expr (sac_Γ scb Γ) (sac_Δ scb Γ atypes (weakCK'' Δ)) - (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))) scbx ex) as stuff. set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]). simpl in n. apply n. @@ -957,7 +966,8 @@ Definition expr2proof : apply b2'. destruct case_ECase. - rewrite case_lemma. + set (@RCase Γ Δ l tc) as q. + rewrite <- case_lemma. eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ]. eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod. rewrite <- mapOptionTree_compose. diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v index dacdcae..ad1dee7 100644 --- a/src/HaskStrongToWeak.v +++ b/src/HaskStrongToWeak.v @@ -156,11 +156,13 @@ Section HaskStrongToWeak. ; bind tbranches' = @typeToWeakType Γ _ tbranches ite ; bind escrut' = exprToWeakExpr χ escrut ite ; bind branches' = - ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & 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 [] - | T_Leaf (Some x) => let (scb,e) := x in + | T_Leaf (Some x) => + let (sac,scb_e) := x in + let (scb,e) := scb_e in let varstypes := vec2list (scbwv_varstypes scb) in bind evars_ite = mfresh _ ite ; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★ @@ -170,7 +172,7 @@ Section HaskStrongToWeak. varstypes) ; let χ' := update_χ' χ exprvars in bind e'' = exprToWeakExpr χ' e (snd evars_ite) - ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')] + ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')] | T_Branch b1 b2 => bind b1' = caseBranches b1 ; bind b2' = caseBranches b2 ; return (b1',,b2') diff --git a/src/HaskWeakToStrong.v b/src/HaskWeakToStrong.v index f2ceddf..bbc9cc7 100644 --- a/src/HaskWeakToStrong.v +++ b/src/HaskWeakToStrong.v @@ -656,8 +656,8 @@ Definition weakExprToStrongExpr : forall else mkAvars avars (tyConKind tc) φ >>= fun avars' => weakTypeToTypeOfKind φ tbranches ★ >>= fun tbranches' => (fix mkTree (t:Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) : ???(Tree - ??{scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' & - Expr (sac_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}) := + ??{ sac : _ & {scb : StrongCaseBranchWithVVs CoreVar CoreVarEqDecidable tc avars' sac & + Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ))(scbwv_ξ scb ξ lev)(weakLT' (tbranches' @@ lev))}}) := match t with | T_Leaf None => OK [] | T_Leaf (Some (ac,extyvars,coervars,exprvars,ebranch)) => @@ -666,7 +666,7 @@ 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_Γ scb Γ) (sac_Δ scb Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) + weakExprToStrongExpr (sac_Γ sac Γ) (sac_Δ sac Γ avars' (weakCK'' Δ)) (sacpj_φ sac _ φ) (sacpj_ψ sac _ _ avars' ψ) (scbwv_ξ scb ξ lev) (update_ig ig (map (@fst _ _) (vec2list (scbwv_varstypes scb)))) @@ -708,6 +708,7 @@ Definition weakExprToStrongExpr : forall apply OK; auto. destruct case_case. + exists sac. exists scb. apply ebranch'.