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.
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.
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 *)
[Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@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.
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 : _
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) :=
| 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.
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.
(* 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 :=
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,
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
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.
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.
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.
reflexivity.
Qed.
-
Definition expr2proof :
forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
| 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')
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.
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.
; 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 _ ★
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')
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)) =>
>>= 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))))
apply OK; auto.
destruct case_case.
+ exists sac.
exists scb.
apply ebranch'.