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 Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskStrongTypes.
14 Require Import HaskStrong.
15 Require Import HaskProof.
17 Section HaskProofToStrong.
19 Context {VV:Type} {eqdec_vv:EqDecidable VV} {freshM:FreshMonad VV}.
21 Definition fresh := FMT_fresh freshM.
22 Definition FreshM := FMT freshM.
23 Definition FreshMon := FMT_Monad freshM.
24 Existing Instance FreshMon.
26 Definition ExprVarResolver Γ := VV -> LeveledHaskType Γ ★.
28 Definition ujudg2exprType {Γ}{Δ}(ξ:ExprVarResolver Γ)(j:UJudg Γ Δ) : Type :=
30 mkUJudg Σ τ => forall vars, Σ = mapOptionTree ξ vars ->
31 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
34 Definition judg2exprType (j:Judg) : Type :=
36 (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
37 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
40 Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
45 Definition ileaf `(it:ITree X F [t]) : F t.
50 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
51 update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
61 Lemma quark {T} (l1:list T) l2 vf :
62 (In vf (app l1 l2)) <->
63 (In vf l1) \/ (In vf l2).
90 right; apply H0; auto.
91 right; apply H0; auto.
94 Lemma splitter {T} (l1:list T) l2 vf :
95 (In vf (app l1 l2) → False)
96 -> (In vf l1 → False) /\ (In vf l2 → False).
98 split; intros; apply H; rewrite quark.
104 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
105 (In vf (leaves tl) -> False) ->
106 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
112 set (eqd_dec vf t) as x in *.
128 Lemma fresh_lemma'' Γ
129 : forall types ξ lev,
130 FreshM { varstypes : _
131 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
132 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
137 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
138 FreshM { varstypes : _
139 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
140 /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
141 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
144 refine (bind vf = fresh (leaves vars) ; return _).
146 destruct vf as [ vf vf_pf ].
150 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
154 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
170 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
172 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
173 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
174 (leaves vt2)) _ _; return _).
180 clear IHtypes1 IHtypes2.
181 destruct x1 as [vt1 [pf11 pf12]].
182 exists (vt1,,vt2); split; auto.
184 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
185 set (mapOptionTree_extensional _ _ q) as q'.
192 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
193 set (mapOptionTree_extensional _ _ q) as q'.
197 rewrite <- mapOptionTree_compose.
198 rewrite <- mapOptionTree_compose.
199 rewrite <- mapOptionTree_compose in *.
204 rewrite <- mapOptionTree_compose.
210 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
211 : Σ = mapOptionTree ξ vars ->
213 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
214 /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
216 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
217 refine (q >>>= fun q' => return _).
220 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
221 destruct varstypes; try destruct o; try destruct p; simpl in *.
222 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
223 inversion pf2; subst.
225 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
231 Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
232 ujudg2exprType ξ (Γ >> Δ > h |- t) ->
233 ujudg2exprType ξ (Γ >> Δ > j |- t)
236 refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
237 ujudg2exprType ξ (Γ >> Δ > h |- t) ->
238 ujudg2exprType ξ (Γ >> Δ > j |- t) :=
239 match r as R in Arrange H C return ujudg2exprType ξ (Γ >> Δ > H |- t) ->
240 ujudg2exprType ξ (Γ >> Δ > C |- t) with
241 | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
242 | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
243 | RCanL a => let case_RCanL := tt in _
244 | RCanR a => let case_RCanR := tt in _
245 | RuCanL a => let case_RuCanL := tt in _
246 | RuCanR a => let case_RuCanR := tt in _
247 | RAssoc a b c => let case_RAssoc := tt in _
248 | RCossa a b c => let case_RCossa := tt in _
249 | RExch a b => let case_RExch := tt in _
250 | RWeak a => let case_RWeak := tt in _
251 | RCont a => let case_RCont := tt in _
252 | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
253 end); clear urule2expr; intros.
258 apply (X ([],,vars)).
259 simpl; rewrite <- H; auto.
264 apply (X (vars,,[])).
265 simpl; rewrite <- H; auto.
267 destruct case_RuCanL.
269 destruct vars; try destruct o; inversion H.
271 apply (X vars2); auto.
273 destruct case_RuCanR.
275 destruct vars; try destruct o; inversion H.
277 apply (X vars1); auto.
279 destruct case_RAssoc.
282 destruct vars; try destruct o; inversion H.
283 destruct vars1; try destruct o; inversion H.
284 apply (X (vars1_1,,(vars1_2,,vars2))).
287 destruct case_RCossa.
290 destruct vars; try destruct o; inversion H.
291 destruct vars2; try destruct o; inversion H.
292 apply (X ((vars1,,vars2_1),,vars2_2)).
298 destruct vars; try destruct o; inversion H.
299 apply (X (vars2,,vars1)).
300 inversion H; subst; auto.
311 apply (X (vars,,vars)).
318 destruct vars; try destruct o; inversion H.
319 apply (fun q => e ξ q vars2 H2).
324 apply X with (vars:=vars1,,vars).
330 destruct case_RRight.
332 destruct vars; try destruct o; inversion H.
333 apply (fun q => e ξ q vars1 H1).
338 apply X with (vars:=vars,,vars2).
350 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
351 ITree (LeveledHaskType Γ ★)
352 (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
353 (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
354 -> ELetRecBindings Γ Δ ξ' l varstypes.
357 destruct a; simpl in *.
360 apply ileaf in X. simpl in X.
363 destruct (eqd_dec (unlev (ξ' v)) τ).
367 destruct (eqd_dec h0 l).
370 apply (Prelude_error "level mismatch; should never happen").
371 apply (Prelude_error "letrec type mismatch; should never happen").
375 apply IHvarstypes1; inversion X; auto.
376 apply IHvarstypes2; inversion X; auto.
379 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
380 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
381 | INone => T_Leaf None
382 | ILeaf x y => T_Leaf (Some _)
383 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
388 Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
389 : ITree { x:X & F x } (fun x => J (projT1 x)) t
390 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
392 induction it; simpl in *.
396 simpl; apply IBranch; auto.
399 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
400 refine (fix rec t := match t with
401 | T_Leaf None => T_Leaf None
402 | T_Leaf (Some x) => T_Leaf (Some _)
403 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
405 destruct x as [x fx].
406 refine (bind fx' = fx ; return _).
412 Definition case_helper tc Γ Δ lev tbranches avars ξ :
413 forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
414 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
416 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
417 & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
422 destruct pcb as [sac pcb].
426 destruct s as [vars vars_pf].
428 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
429 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
432 rewrite <- mapOptionTree_compose.
434 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
435 set (mapOptionTree (@fst _ _) localvars) as localvars'.
437 set (list2vec (leaves localvars')) as localvars''.
438 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
439 rewrite H'' in localvars''.
440 cut (distinct (vec2list localvars'')). intro H'''.
441 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
443 refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
448 rewrite <- mapOptionTree_compose.
463 Definition gather_branch_variables
464 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
465 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
468 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
469 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
470 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
471 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
477 destruct a; [ idtac | apply INone ].
479 apply ileaf in source.
481 destruct s as [sac pcb].
493 destruct vars; try destruct o; simpl in pf; inversion pf.
498 apply (IHalts1 vars1 H0 X); auto.
499 apply (IHalts2 vars2 H1 X0); auto.
504 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
508 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
509 | RArrange a b c d e r => let case_RURule := tt in _
510 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
511 | RLit Γ Δ l _ => let case_RLit := tt in _
512 | RVar Γ Δ σ p => let case_RVar := tt in _
513 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
514 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
515 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
516 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
517 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
518 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
519 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
520 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
521 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
522 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
523 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
524 | RBrak Σ a b c n m => let case_RBrak := tt in _
525 | REsc Σ a b c n m => let case_REsc := tt in _
526 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
527 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
528 end); intro X_; try apply ileaf in X_; simpl in X_.
530 destruct case_RURule.
531 apply ILeaf. simpl. intros.
532 set (@urule2expr a b _ _ e r0 ξ) as q.
533 set (fun z => q z) as q'.
535 apply q' with (vars:=vars).
538 apply X_ with (vars:=vars0).
543 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
548 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
553 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
558 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
562 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
563 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
567 destruct case_RGlobal.
568 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
575 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
577 destruct pf as [ vnew [ pf1 pf2 ]].
578 set (update_ξ ξ x ((⟨vnew, tx ⟩) :: nil)) as ξ' in *.
579 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
589 apply ELam with (ev:=vnew).
596 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
599 apply ileaf in X. simpl in X.
602 destruct case_RBindingGroup.
603 apply ILeaf; simpl; intros.
608 destruct vars; inversion H.
609 destruct o; inversion H3.
610 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
622 destruct vars. try destruct o; inversion H.
625 set (X1 ξ vars1 H5) as q1.
626 set (X2 ξ vars2 H6) as q2.
627 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
634 apply (EApp _ _ _ _ _ _ q1' q2').
639 destruct vars; try destruct o; inversion H.
640 refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
642 destruct pf as [ vnew [ pf1 pf2 ]].
643 set (update_ξ ξ p ((⟨vnew, σ₂ ⟩) :: nil)) as ξ' in *.
648 refine (X0 ξ vars2 _ >>>= fun X0' => _).
651 refine (X ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
664 apply ELet with (ev:=vnew)(tv:=σ₂).
668 destruct case_REmptyGroup.
669 apply ILeaf; simpl; intros.
674 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
679 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
680 rewrite mapOptionTree_compose.
683 apply ileaf in X. simpl in *.
687 destruct case_RAppCo.
688 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
694 destruct case_RAbsCo.
695 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
700 destruct case_RLetRec.
701 apply ILeaf; simpl; intros.
702 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
703 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
704 refine (X_ ((update_ξ ξ t (leaves varstypes)))
705 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
711 inversion X; subst; clear X.
713 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
714 apply (@letrec_helper Γ Δ t varstypes).
715 rewrite <- pf2 in X1.
716 rewrite mapOptionTree_compose.
722 apply ILeaf; simpl; intros.
729 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
730 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
731 rename Σ into body_freevars_types.
732 rename vars into all_freevars.
733 rename X0 into body_expr.
734 rename X into alts_exprs.
736 destruct all_freevars; try destruct o; inversion H.
737 rename all_freevars2 into body_freevars.
738 rename all_freevars1 into alts_freevars.
740 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
741 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
742 apply fix_indexing in alts_exprs'.
743 simpl in alts_exprs'.
744 apply unindex_tree in alts_exprs'.
745 simpl in alts_exprs'.
746 apply fix2 in alts_exprs'.
747 apply treeM in alts_exprs'.
749 refine ( alts_exprs' >>>= fun Y =>
751 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
757 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
759 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
760 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
761 | cnd_weak => let case_nil := tt in INone _ _
762 | cnd_rule h c cnd' r => let case_rule := tt in rule2expr _ _ r (closed2expr' _ cnd')
763 | cnd_branch _ _ c1 c2 => let case_branch := tt in IBranch _ _ (closed2expr' _ c1) (closed2expr' _ c2)
764 end)); clear closed2expr'; intros; subst.
767 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
768 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
770 induction Σ; intro ξ.
773 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
774 refine (q >>>= fun q' => return _).
777 destruct q' as [varstypes [pf1 [pf2 distpf]]].
778 exists (mapOptionTree (@fst _ _) varstypes).
779 exists (update_ξ ξ l (leaves varstypes)).
784 refine (bind f1 = IHΣ1 ξ ; _).
786 destruct f1 as [vars1 [ξ1 pf1]].
787 refine (bind f2 = IHΣ2 ξ1 ; _).
789 destruct f2 as [vars2 [ξ2 pf22]].
791 exists (vars1,,vars2).
799 Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
800 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
801 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
803 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
804 apply closed2expr in cnd.
808 refine (bind ξvars = manyFresh _ Σ ξ0; _).
810 destruct ξvars as [vars ξpf].
811 destruct ξpf as [ξ pf].
812 refine (cnd ξ vars _ >>>= fun it => _).
815 refine (return OK _).
820 End HaskProofToStrong.