1 (*********************************************************************************************************************************)
2 (* HaskProofToStrong: convert HaskProof to HaskStrong *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import NaturalDeductionContext.
10 Require Import Coq.Strings.String.
11 Require Import Coq.Lists.List.
12 Require Import Coq.Init.Specif.
13 Require Import HaskKinds.
14 Require Import HaskStrongTypes.
15 Require Import HaskStrong.
16 Require Import HaskProof.
18 Section HaskProofToStrong.
20 Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
22 Definition fresh := FMT_fresh freshM.
23 Definition FreshM := FMT freshM.
24 Definition FreshMon := FMT_Monad freshM.
25 Existing Instance FreshMon.
27 Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
29 Definition judg2exprType (j:Judg) : Type :=
31 (Γ > Δ > Σ |- τ @ l) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
32 FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ)
35 Definition justOne Γ Δ ξ τ l : ITree _ (fun t => Expr Γ Δ ξ t l) [τ] -> Expr Γ Δ ξ τ l.
40 Definition ileaf `(it:ITree X F [t]) : F t.
45 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
46 update_xi ξ lev (app l1 l2) q = update_xi (update_xi ξ lev l2) lev l1 q.
56 Lemma quark {T} (l1:list T) l2 vf :
57 (In vf (app l1 l2)) <->
58 (In vf l1) \/ (In vf l2).
85 right; apply H0; auto.
86 right; apply H0; auto.
89 Lemma splitter {T} (l1:list T) l2 vf :
90 (In vf (app l1 l2) → False)
91 -> (In vf l1 → False) /\ (In vf l2 → False).
93 split; intros; apply H; rewrite quark.
99 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
100 (In vf (leaves tl) -> False) ->
101 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
107 set (eqd_dec vf t) as x in *.
123 Lemma fresh_lemma'' Γ
124 : forall types ξ lev,
125 FreshM { varstypes : _
126 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
127 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
132 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
133 FreshM { varstypes : _
134 | mapOptionTree (update_xi(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
135 /\ mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
136 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
139 refine (bind vf = fresh (leaves vars) ; return _).
141 destruct vf as [ vf vf_pf ].
145 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
149 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
165 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
167 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
168 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_xi ξ lev
169 (leaves vt2)) _ _; return _).
175 clear IHtypes1 IHtypes2.
176 destruct x1 as [vt1 [pf11 pf12]].
177 exists (vt1,,vt2); split; auto.
179 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
180 set (mapOptionTree_extensional _ _ q) as q'.
187 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
188 set (mapOptionTree_extensional _ _ q) as q'.
192 rewrite <- mapOptionTree_compose.
193 rewrite <- mapOptionTree_compose.
194 rewrite <- mapOptionTree_compose in *.
199 rewrite <- mapOptionTree_compose.
205 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
206 : Σ = mapOptionTree ξ vars ->
208 | mapOptionTree (update_xi(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
209 /\ mapOptionTree (update_xi ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
211 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
212 refine (q >>>= fun q' => return _).
215 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
216 destruct varstypes; try destruct o; try destruct p; simpl in *.
217 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
218 inversion pf2; subst.
220 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
226 Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ l : Type :=
227 forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t l) τ).
229 Definition urule2expr : forall Γ Δ h j t l (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
230 ujudg2exprType Γ ξ Δ h t l ->
231 ujudg2exprType Γ ξ Δ j t l
234 refine (fix urule2expr h j t l (r:@Arrange _ h j) ξ {struct r} :
235 ujudg2exprType Γ ξ Δ h t l ->
236 ujudg2exprType Γ ξ Δ j t l :=
237 match r as R in Arrange H C return
238 ujudg2exprType Γ ξ Δ H t l ->
239 ujudg2exprType Γ ξ Δ C t l
241 | ALeft h c ctx r => let case_ALeft := tt in (fun e => _) (urule2expr _ _ _ _ r)
242 | ARight h c ctx r => let case_ARight := tt in (fun e => _) (urule2expr _ _ _ _ r)
243 | AId a => let case_AId := tt in _
244 | ACanL a => let case_ACanL := tt in _
245 | ACanR a => let case_ACanR := tt in _
246 | AuCanL a => let case_AuCanL := tt in _
247 | AuCanR a => let case_AuCanR := tt in _
248 | AAssoc a b c => let case_AAssoc := tt in _
249 | AuAssoc a b c => let case_AuAssoc := tt in _
250 | AExch a b => let case_AExch := tt in _
251 | AWeak a => let case_AWeak := tt in _
252 | ACont a => let case_ACont := tt in _
253 | AComp a b c f g => let case_AComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ _ f) (urule2expr _ _ _ _ g)
254 end); clear urule2expr; intros.
260 simpl; unfold ujudg2exprType; intros.
262 apply (X ([],,vars)).
263 simpl; rewrite <- H; auto.
266 simpl; unfold ujudg2exprType; intros.
268 apply (X (vars,,[])).
269 simpl; rewrite <- H; auto.
271 destruct case_AuCanL.
272 simpl; unfold ujudg2exprType; intros.
273 destruct vars; try destruct o; inversion H.
275 apply (X vars2); auto.
277 destruct case_AuCanR.
278 simpl; unfold ujudg2exprType; intros.
279 destruct vars; try destruct o; inversion H.
281 apply (X vars1); auto.
283 destruct case_AAssoc.
284 simpl; unfold ujudg2exprType; intros.
286 destruct vars; try destruct o; inversion H.
287 destruct vars1; try destruct o; inversion H.
288 apply (X (vars1_1,,(vars1_2,,vars2))).
291 destruct case_AuAssoc.
292 simpl; unfold ujudg2exprType; intros.
294 destruct vars; try destruct o; inversion H.
295 destruct vars2; try destruct o; inversion H.
296 apply (X ((vars1,,vars2_1),,vars2_2)).
300 simpl; unfold ujudg2exprType ; intros.
302 destruct vars; try destruct o; inversion H.
303 apply (X (vars2,,vars1)).
304 inversion H; subst; auto.
307 simpl; unfold ujudg2exprType; intros.
313 simpl; unfold ujudg2exprType ; intros.
315 apply (X (vars,,vars)).
321 intro vars; unfold ujudg2exprType; intro H.
322 destruct vars; try destruct o; inversion H.
323 apply (fun q => e ξ q vars2 H2).
327 unfold ujudg2exprType.
329 apply X with (vars:=vars1,,vars).
335 destruct case_ARight.
336 intro vars; unfold ujudg2exprType; intro H.
337 destruct vars; try destruct o; inversion H.
338 apply (fun q => e ξ q vars1 H1).
342 unfold ujudg2exprType.
344 apply X with (vars:=vars,,vars2).
356 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
358 (fun t : HaskType Γ ★ => Expr Γ Δ ξ' t l)
359 (mapOptionTree (unlev ○ ξ' ○ (@fst _ _)) varstypes)
360 -> ELetRecBindings Γ Δ ξ' l varstypes.
363 destruct a; simpl in *.
366 apply ileaf in X. simpl in X.
369 destruct (eqd_dec (unlev (ξ' v)) τ).
373 destruct (eqd_dec h0 l).
378 apply (Prelude_error "level mismatch; should never happen").
379 apply (Prelude_error "letrec type mismatch; should never happen").
383 apply IHvarstypes1; inversion X; auto.
384 apply IHvarstypes2; inversion X; auto.
387 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
388 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
389 | INone => T_Leaf None
390 | ILeaf x y => T_Leaf (Some _)
391 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
396 Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
397 : ITree { x:X & F x } (fun x => J (projT1 x)) t
398 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
400 induction it; simpl in *.
404 simpl; apply IBranch; auto.
407 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
408 refine (fix rec t := match t with
409 | T_Leaf None => T_Leaf None
410 | T_Leaf (Some x) => T_Leaf (Some _)
411 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
413 destruct x as [x fx].
414 refine (bind fx' = fx ; return _).
420 Definition case_helper tc Γ Δ lev tbranches avars ξ :
421 forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
422 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
424 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
425 & Expr (sac_gamma sac Γ) (sac_delta sac Γ avars (weakCK'' Δ)) (scbwv_xi scb ξ lev)
426 (weakT' tbranches) (weakL' lev) }) (projT1 pcb)).
431 destruct pcb as [sac pcb].
435 destruct s as [vars vars_pf].
437 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
438 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
441 rewrite <- mapOptionTree_compose.
443 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
444 set (mapOptionTree (@fst _ _) localvars) as localvars'.
446 set (list2vec (leaves localvars')) as localvars''.
447 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
448 rewrite H'' in localvars''.
449 cut (distinct (vec2list localvars'')). intro H'''.
450 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
452 refine (bind q = (f (scbwv_xi scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
457 rewrite <- mapOptionTree_compose.
472 Definition gather_branch_variables
473 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
474 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
477 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
478 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
479 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
480 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
486 destruct a; [ idtac | apply INone ].
488 apply ileaf in source.
490 destruct s as [sac pcb].
502 destruct vars; try destruct o; simpl in pf; inversion pf.
507 apply (IHalts1 vars1 H0 X); auto.
508 apply (IHalts2 vars2 H1 X0); auto.
512 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
513 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
515 induction Σ; intro ξ.
518 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
519 refine (q >>>= fun q' => return _).
522 destruct q' as [varstypes [pf1 [pf2 distpf]]].
523 exists (mapOptionTree (@fst _ _) varstypes).
524 exists (update_xi ξ l (leaves varstypes)).
529 refine (bind f1 = IHΣ1 ξ ; _).
531 destruct f1 as [vars1 [ξ1 pf1]].
532 refine (bind f2 = IHΣ2 ξ1 ; _).
534 destruct f2 as [vars2 [ξ2 pf22]].
536 exists (vars1,,vars2).
541 admit. (* freshness assumption *)
544 Definition rlet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p :
545 forall (X_ : ITree Judg judg2exprType
546 ([Γ > Δ > Σ₁ |- [σ₁] @ p],, [Γ > Δ > [σ₁ @@ p],, Σ₂ |- [σ₂] @ p])),
547 ITree Judg judg2exprType [Γ > Δ > Σ₁,, Σ₂ |- [σ₂] @ p].
551 destruct vars; try destruct o; inversion H.
553 refine (fresh_lemma _ ξ _ _ σ₁ p H2 >>>= (fun pf => _)).
556 destruct pf as [ vnew [ pf1 pf2 ]].
557 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
563 refine (X ξ vars1 _ >>>= fun X0' => _).
568 refine (X0 ξ' ([vnew],,vars2) _ >>>= fun X1' => _).
580 apply ELet with (ev:=vnew)(tv:=σ₁).
585 Definition vartree Γ Δ Σ lev ξ :
586 forall vars, Σ @@@ lev = mapOptionTree ξ vars ->
587 ITree (HaskType Γ ★) (fun t : HaskType Γ ★ => Expr Γ Δ ξ t lev) Σ.
592 destruct vars; try destruct o; inversion H.
593 set (EVar Γ Δ ξ v) as q.
599 destruct vars; try destruct o; inversion H.
608 Definition rdrop Γ Δ Σ₁ Σ₁₂ a lev :
609 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a,,Σ₁₂ @ lev] ->
610 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
616 set (X ξ vars H) as q.
618 refine (q >>>= fun q' => return _).
624 Definition rdrop' Γ Δ Σ₁ Σ₁₂ a lev :
625 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂,,a @ lev] ->
626 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- a @ lev].
632 set (X ξ vars H) as q.
634 refine (q >>>= fun q' => return _).
640 Definition rdrop'' Γ Δ Σ₁ Σ₁₂ lev :
641 ITree Judg judg2exprType [Γ > Δ > [],,Σ₁ |- Σ₁₂ @ lev] ->
642 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev].
647 eapply X with (vars:=[],,vars).
648 rewrite H; reflexivity.
651 Definition rdrop''' Γ Δ a Σ₁ Σ₁₂ lev :
652 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
653 ITree Judg judg2exprType [Γ > Δ > a,,Σ₁ |- Σ₁₂ @ lev].
658 destruct vars; try destruct o; inversion H.
659 eapply X with (vars:=vars2).
663 Definition rassoc Γ Δ Σ₁ a b c lev :
664 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
665 ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev].
670 destruct vars; try destruct o; inversion H.
671 destruct vars2; try destruct o; inversion H2.
672 apply X with (vars:=(vars1,,vars2_1),,vars2_2).
676 Definition rassoc' Γ Δ Σ₁ a b c lev :
677 ITree Judg judg2exprType [Γ > Δ > (a,,(b,,c)) |- Σ₁ @ lev] ->
678 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev].
683 destruct vars; try destruct o; inversion H.
684 destruct vars1; try destruct o; inversion H1.
685 apply X with (vars:=vars1_1,,(vars1_2,,vars2)).
689 Definition swapr Γ Δ Σ₁ a b c lev :
690 ITree Judg judg2exprType [Γ > Δ > ((a,,b),,c) |- Σ₁ @ lev] ->
691 ITree Judg judg2exprType [Γ > Δ > ((b,,a),,c) |- Σ₁ @ lev].
696 destruct vars; try destruct o; inversion H.
697 destruct vars1; try destruct o; inversion H1.
698 apply X with (vars:=(vars1_2,,vars1_1),,vars2).
702 Definition rdup Γ Δ Σ₁ a c lev :
703 ITree Judg judg2exprType [Γ > Δ > ((a,,a),,c) |- Σ₁ @ lev] ->
704 ITree Judg judg2exprType [Γ > Δ > (a,,c) |- Σ₁ @ lev].
709 destruct vars; try destruct o; inversion H.
710 apply X with (vars:=(vars1,,vars1),,vars2). (* is this allowed? *)
714 (* holy cow this is ugly *)
715 Definition rcut Γ Δ Σ₃ lev Σ₁₂ :
717 ITree Judg judg2exprType [Γ > Δ > Σ₁ |- Σ₁₂ @ lev] ->
718 ITree Judg judg2exprType [Γ > Δ > Σ₁₂ @@@ lev,,Σ₂ |- [Σ₃] @ lev] ->
719 ITree Judg judg2exprType [Γ > Δ > Σ₁,,Σ₂ |- [Σ₃] @ lev].
738 set (IHΣ₁₂1 _ _ (rdrop _ _ _ _ _ _ X) X0) as q.
739 set (IHΣ₁₂2 _ (Σ₁,,Σ₂) (rdrop' _ _ _ _ _ _ X)) as q'.
744 apply rassoc' in q''.
749 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
753 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
754 | RArrange a b c d e l r => let case_RURule := tt in _
755 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
756 | RLit Γ Δ l _ => let case_RLit := tt in _
757 | RVar Γ Δ σ p => let case_RVar := tt in _
758 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
759 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
760 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
761 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
762 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
763 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
764 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
765 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
766 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
767 | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
768 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
769 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
770 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _
771 | RVoid _ _ l => let case_RVoid := tt in _
772 | RBrak Σ a b c n m => let case_RBrak := tt in _
773 | REsc Σ a b c n m => let case_REsc := tt in _
774 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
775 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
776 end); intro X_; try apply ileaf in X_; simpl in X_.
778 destruct case_RURule.
779 apply ILeaf. simpl. intros.
780 set (@urule2expr a b _ _ e l r0 ξ) as q.
781 unfold ujudg2exprType.
782 unfold ujudg2exprType in q.
783 apply q with (vars:=vars).
785 apply X_ with (vars:=vars0).
790 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
795 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
800 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
805 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
809 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
810 destruct vars; simpl in H; inversion H; destruct o. inversion H1.
811 set (@EVar _ _ _ Δ ξ v) as q.
817 destruct case_RGlobal.
818 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
824 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
826 destruct pf as [ vnew [ pf1 pf2 ]].
827 set (update_xi ξ x (((vnew, tx )) :: nil)) as ξ' in *.
828 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
838 apply ELam with (ev:=vnew).
845 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
848 apply ileaf in X. simpl in X.
858 destruct vars. try destruct o; inversion H.
861 set (X1 ξ vars1 H5) as q1.
862 set (X2 ξ vars2 H6) as q2.
863 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
870 apply (EApp _ _ _ _ _ _ q1' q2').
876 destruct case_RWhere.
879 destruct vars; try destruct o; inversion H.
880 destruct vars2; try destruct o; inversion H2.
883 assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto.
884 refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)).
887 destruct pf as [ vnew [ pf1 pf2 ]].
888 set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *.
894 refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _).
903 refine (X0 ξ vars2_1 _ >>>= fun X1' => _).
912 apply ELet with (ev:=vnew)(tv:=σ₁).
932 set (IHΣ₃1 (rdrop _ _ _ _ _ _ X0)) as q1.
933 set (IHΣ₃2 (rdrop' _ _ _ _ _ _ X0)) as q2.
940 refine (q1 _ _ H >>>= fun q1' => q2 _ _ H >>>= fun q2' => return _).
948 destruct vars; try destruct o; inversion H.
949 refine (X_ _ _ H2 >>>= fun X' => return _).
956 destruct case_RRight.
959 destruct vars; try destruct o; inversion H.
960 refine (X_ _ _ H1 >>>= fun X' => return _).
968 apply ILeaf; simpl; intros.
973 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
978 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
979 rewrite mapOptionTree_compose.
982 apply ileaf in X. simpl in *.
986 destruct case_RAppCo.
987 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
993 destruct case_RAbsCo.
994 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
999 destruct case_RLetRec.
1000 apply ILeaf; simpl; intros.
1001 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
1002 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
1003 refine (X_ ((update_xi ξ t (leaves varstypes)))
1004 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
1010 inversion X; subst; clear X.
1012 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
1014 apply (@letrec_helper Γ Δ t varstypes).
1015 rewrite mapOptionTree_compose.
1016 rewrite mapOptionTree_compose.
1018 replace ((mapOptionTree unlev (y @@@ t))) with y.
1020 clear pf1 X0 X1 pfdist pf2 vars varstypes.
1021 induction y; try destruct a; auto.
1029 destruct case_RCase.
1030 apply ILeaf; simpl; intros.
1037 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
1038 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
1039 rename Σ into body_freevars_types.
1040 rename vars into all_freevars.
1041 rename X0 into body_expr.
1042 rename X into alts_exprs.
1044 destruct all_freevars; try destruct o; inversion H.
1045 rename all_freevars2 into body_freevars.
1046 rename all_freevars1 into alts_freevars.
1048 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
1049 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
1050 apply fix_indexing in alts_exprs'.
1051 simpl in alts_exprs'.
1052 apply unindex_tree in alts_exprs'.
1053 simpl in alts_exprs'.
1054 apply fix2 in alts_exprs'.
1055 apply treeM in alts_exprs'.
1057 refine ( alts_exprs' >>>= fun Y =>
1059 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
1065 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
1066 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
1067 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
1068 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
1069 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
1072 Definition proof2expr Γ Δ τ l Σ (ξ0: VV -> LeveledHaskType Γ ★)
1073 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ] @ l] ->
1074 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ l}).
1076 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
1077 apply closed2expr in cnd.
1081 refine (bind ξvars = manyFresh _ Σ ξ0; _).
1083 destruct ξvars as [vars ξpf].
1084 destruct ξpf as [ξ pf].
1085 refine (cnd ξ vars _ >>>= fun it => _).
1088 refine (return OK _).
1096 End HaskProofToStrong.