Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
- Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
- match j with
- mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
- FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
- end.
-
Definition judg2exprType (j:Judg) : Type :=
match j with
(Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
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 : _
inversion pf2.
Defined.
- Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★),
- ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j.
-
- refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} :
- ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j :=
- match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with
- | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r)
- | RCanL t a => let case_RCanL := tt in _
- | RCanR t a => let case_RCanR := tt in _
- | RuCanL t a => let case_RuCanL := tt in _
- | RuCanR t a => let case_RuCanR := tt in _
- | RAssoc t a b c => let case_RAssoc := tt in _
- | RCossa t a b c => let case_RCossa := tt in _
- | RExch t a b => let case_RExch := tt in _
- | RWeak t a => let case_RWeak := tt in _
- | RCont t a => let case_RCont := tt in _
+ Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
+ forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
+
+ Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t
+ .
+ intros Γ Δ.
+ refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
+ ujudg2exprType Γ ξ Δ h t ->
+ ujudg2exprType Γ ξ Δ j t :=
+ match r as R in Arrange H C return
+ ujudg2exprType Γ ξ Δ H t ->
+ ujudg2exprType Γ ξ Δ C t
+ with
+ | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
+ | RId a => let case_RId := tt in _
+ | RCanL a => let case_RCanL := tt in _
+ | RCanR a => let case_RCanR := tt in _
+ | RuCanL a => let case_RuCanL := tt in _
+ | RuCanR a => let case_RuCanR := tt in _
+ | RAssoc a b c => let case_RAssoc := tt in _
+ | RCossa a b c => let case_RCossa := tt in _
+ | RExch a b => let case_RExch := tt in _
+ | RWeak a => let case_RWeak := tt in _
+ | RCont a => let case_RCont := tt in _
+ | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
end); clear urule2expr; intros.
+ destruct case_RId.
+ apply X.
+
destruct case_RCanL.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 ([],,vars)).
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X ([],,vars)).
simpl; rewrite <- H; auto.
destruct case_RCanR.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 (vars,,[])).
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X (vars,,[])).
simpl; rewrite <- H; auto.
destruct case_RuCanL.
- apply ILeaf; simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
- inversion X.
- simpl in X0.
- apply (X0 vars2); auto.
+ simpl in X.
+ apply (X vars2); auto.
destruct case_RuCanR.
- apply ILeaf; simpl; intros.
+ simpl; unfold ujudg2exprType; intros.
destruct vars; try destruct o; inversion H.
- inversion X.
- simpl in X0.
- apply (X0 vars1); auto.
+ simpl in X.
+ apply (X vars1); auto.
destruct case_RAssoc.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
destruct vars; try destruct o; inversion H.
destruct vars1; try destruct o; inversion H.
- apply (X0 (vars1_1,,(vars1_2,,vars2))).
+ apply (X (vars1_1,,(vars1_2,,vars2))).
subst; auto.
destruct case_RCossa.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
destruct vars; try destruct o; inversion H.
destruct vars2; try destruct o; inversion H.
- apply (X0 ((vars1,,vars2_1),,vars2_2)).
+ apply (X ((vars1,,vars2_1),,vars2_2)).
subst; auto.
+ destruct case_RExch.
+ simpl; unfold ujudg2exprType ; intros.
+ simpl in X.
+ destruct vars; try destruct o; inversion H.
+ apply (X (vars2,,vars1)).
+ inversion H; subst; auto.
+
+ destruct case_RWeak.
+ simpl; unfold ujudg2exprType; intros.
+ simpl in X.
+ apply (X []).
+ auto.
+
+ destruct case_RCont.
+ simpl; unfold ujudg2exprType ; intros.
+ simpl in X.
+ apply (X (vars,,vars)).
+ simpl.
+ rewrite <- H.
+ auto.
+
destruct case_RLeft.
- destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
- destruct o; [ idtac | apply INone ].
- destruct u; simpl in *.
- apply ILeaf; simpl; intros.
+ intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
- set (fun q => ileaf (e ξ q)) as r'.
- simpl in r'.
- apply r' with (vars:=vars2).
- clear r' e.
- clear r0.
- induction h0.
- destruct a.
- destruct u.
+ apply (fun q => e ξ q vars2 H2).
+ clear r0 e H2.
simpl in X.
- apply ileaf in X.
- apply ILeaf.
simpl.
- simpl in X.
+ unfold ujudg2exprType.
intros.
apply X with (vars:=vars1,,vars).
- simpl.
rewrite H0.
rewrite H1.
+ simpl.
reflexivity.
- apply INone.
- apply IBranch.
- apply IHh0_1. inversion X; auto.
- apply IHh0_2. inversion X; auto.
- auto.
-
+
destruct case_RRight.
- destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ].
- destruct o; [ idtac | apply INone ].
- destruct u; simpl in *.
- apply ILeaf; simpl; intros.
+ intro vars; unfold ujudg2exprType; intro H.
destruct vars; try destruct o; inversion H.
- set (fun q => ileaf (e ξ q)) as r'.
- simpl in r'.
- apply r' with (vars:=vars1).
- clear r' e.
- clear r0.
- induction h0.
- destruct a.
- destruct u.
+ apply (fun q => e ξ q vars1 H1).
+ clear r0 e H2.
simpl in X.
- apply ileaf in X.
- apply ILeaf.
simpl.
- simpl in X.
+ unfold ujudg2exprType.
intros.
apply X with (vars:=vars,,vars2).
- simpl.
rewrite H0.
- rewrite H2.
+ inversion H.
+ simpl.
reflexivity.
- apply INone.
- apply IBranch.
- apply IHh0_1. inversion X; auto.
- apply IHh0_2. inversion X; auto.
- auto.
- destruct case_RExch.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- destruct vars; try destruct o; inversion H.
- apply (X0 (vars2,,vars1)).
- inversion H; subst; auto.
-
- destruct case_RWeak.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 []).
- auto.
-
- destruct case_RCont.
- apply ILeaf; simpl; intros.
- inversion X.
- simpl in X0.
- apply (X0 (vars,,vars)).
- simpl.
- rewrite <- H.
- auto.
+ destruct case_RComp.
+ apply e2.
+ apply e1.
+ apply X.
Defined.
- Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ :
- ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c.
- intro it.
- induction c.
- destruct a.
- destruct u; simpl in *.
- apply ileaf in it.
- apply ILeaf.
- simpl in *.
- intros; apply it with (vars:=vars); auto.
- apply INone.
- apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto.
- Defined.
-
Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
ITree (LeveledHaskType Γ ★)
(fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
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.
+
+ 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.
- intros.
+ 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'.
- Defined.
+ rewrite mapleaves'.
- Fixpoint treeM {T}(t:Tree ??(FreshM T)) : FreshM (Tree ??T) :=
- match t with
- | T_Leaf None => return []
- | T_Leaf (Some x) => bind x' = x ; return [x']
- | T_Branch b1 b2 => bind b1' = treeM b1 ; bind b2' = treeM b2 ; return (b1',,b2')
- end.
+ admit.
+
+ exists scb.
+ apply ileaf in q.
+ apply q.
- Lemma itree_mapOptionTree : forall T T' F (f:T->T') t,
- ITree _ F (mapOptionTree f t) ->
- ITree _ (F ○ f) t.
+ admit.
+ admit.
+ Defined.
+
+ 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.
intros h j r.
refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
- | RURule a b c d e => let case_RURule := tt in _
+ | RArrange a b c d e r => let case_RURule := tt in _
| RNote Γ Δ Σ τ l n => let case_RNote := tt in _
| RLit Γ Δ l _ => let case_RLit := tt in _
| RVar Γ Δ σ p => let case_RVar := tt in _
| RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
| RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
| RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
- | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
- | REmptyGroup _ _ => let case_REmptyGroup := tt in _
+ | RJoin Γ p lri m x q => let case_RJoin := tt in _
+ | RVoid _ _ => let case_RVoid := tt in _
| RBrak Σ a b c n m => let case_RBrak := tt in _
| REsc Σ a b c n m => let case_REsc := tt in _
| RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
| RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
end); intro X_; try apply ileaf in X_; simpl in X_.
- destruct case_RURule.
- destruct d; try destruct o.
- apply ILeaf; destruct u; simpl; intros.
- set (@urule2expr a b _ _ e ξ) as q.
- set (fun z => ileaf (q z)) as q'.
+ destruct case_RURule.
+ apply ILeaf. simpl. intros.
+ set (@urule2expr a b _ _ e r0 ξ) as q.
+ set (fun z => q z) as q'.
simpl in q'.
apply q' with (vars:=vars).
clear q' q.
- apply bridge.
- apply X_.
+ unfold ujudg2exprType.
+ intros.
+ apply X_ with (vars:=vars0).
+ auto.
auto.
- apply no_urules_with_empty_conclusion in e; inversion e; auto.
- apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto.
destruct case_RBrak.
apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
destruct case_RGlobal.
apply ILeaf; simpl; intros; refine (return ILeaf _ _).
apply EGlobal.
- apply wev.
destruct case_RLam.
apply ILeaf.
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_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *.
refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
apply FreshMon.
simpl.
apply ileaf in X. simpl in X.
apply X.
- destruct case_RBindingGroup.
+ destruct case_RJoin.
apply ILeaf; simpl; intros.
inversion X_.
apply ileaf in X.
apply ileaf in q1'.
apply ileaf in q2'.
simpl in *.
- apply (EApp _ _ _ _ _ _ q1' q2').
+ apply (EApp _ _ _ _ _ _ q2' q1').
destruct case_RLet.
apply ILeaf.
refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
apply FreshMon.
destruct pf as [ vnew [ pf1 pf2 ]].
- set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
+ set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
inversion X_.
apply ileaf in X.
apply ileaf in X0.
simpl in *.
- refine (X0 ξ vars2 _ >>>= fun X0' => _).
+ refine (X ξ vars2 _ >>>= fun X0' => _).
apply FreshMon.
auto.
- refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
+
+ refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
apply FreshMon.
rewrite H1.
simpl.
rewrite pf1.
rewrite H1.
reflexivity.
+
refine (return _).
apply ILeaf.
apply ileaf in X0'.
apply X0'.
apply X1'.
- destruct case_REmptyGroup.
+ destruct case_RVoid.
apply ILeaf; simpl; intros.
refine (return _).
apply INone.
inversion X; subst; clear X.
apply (@ELetRec _ _ _ _ _ _ _ varstypes).
+ auto.
apply (@letrec_helper Γ Δ t varstypes).
rewrite <- pf2 in X1.
rewrite mapOptionTree_compose.
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.
- refine ((
- fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
- match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
- | cnd_weak => let case_nil := tt in INone _ _
- | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
- | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
- end)); clear closed2expr'; intros; subst.
- Defined.
+ Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
+ match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
+ | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
+ | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
+ | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
+ end.
Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
{zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
intro pf.
- set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
+ set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
apply closed2expr in cnd.
apply ileaf in cnd.
simpl in *.
refine (return OK _).
exists ξ.
apply (ileaf it).
+ apply INone.
Defined.
End HaskProofToStrong.
projects / coq-hetmet.git / blobdiff