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 judg2exprType (j:Judg) : Type :=
30 (Γ > Δ > Σ |- τ) => forall (ξ:ExprVarResolver Γ) vars, Σ = mapOptionTree ξ vars ->
31 FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ)
34 Definition justOne Γ Δ ξ τ : ITree _ (fun t => Expr Γ Δ ξ t) [τ] -> Expr Γ Δ ξ τ.
39 Definition ileaf `(it:ITree X F [t]) : F t.
44 Lemma update_branches : forall Γ (ξ:VV -> LeveledHaskType Γ ★) lev l1 l2 q,
45 update_ξ ξ lev (app l1 l2) q = update_ξ (update_ξ ξ lev l2) lev l1 q.
55 Lemma quark {T} (l1:list T) l2 vf :
56 (In vf (app l1 l2)) <->
57 (In vf l1) \/ (In vf l2).
84 right; apply H0; auto.
85 right; apply H0; auto.
88 Lemma splitter {T} (l1:list T) l2 vf :
89 (In vf (app l1 l2) → False)
90 -> (In vf l1 → False) /\ (In vf l2 → False).
92 split; intros; apply H; rewrite quark.
98 : forall T Z {eqdt:EqDecidable T}(tl:Tree ??T)(vf:T) ξ (q:Z),
99 (In vf (leaves tl) -> False) ->
100 mapOptionTree (fun v' => if eqd_dec vf v' then q else ξ v') tl =
106 set (eqd_dec vf t) as x in *.
122 Lemma fresh_lemma'' Γ
123 : forall types ξ lev,
124 FreshM { varstypes : _
125 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
126 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
131 : forall types vars Σ ξ lev, Σ = mapOptionTree ξ vars ->
132 FreshM { varstypes : _
133 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev (leaves varstypes)) vars = Σ
134 /\ mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) = (types @@@ lev)
135 /\ distinct (leaves (mapOptionTree (@fst _ _) varstypes)) }.
138 refine (bind vf = fresh (leaves vars) ; return _).
140 destruct vf as [ vf vf_pf ].
144 set (helper VV _ vars vf ξ (h@@lev) vf_pf) as q.
148 destruct (eqd_dec vf vf); [ idtac | set (n (refl_equal _)) as n'; inversion n' ]; auto.
164 intros vars Σ ξ lev pf; refine (bind x2 = IHtypes2 vars Σ ξ lev pf; _).
166 destruct x2 as [vt2 [pf21 [pf22 pfdist]]].
167 refine (bind x1 = IHtypes1 (vars,,(mapOptionTree (@fst _ _) vt2)) (Σ,,(types2@@@lev)) (update_ξ ξ lev
168 (leaves vt2)) _ _; return _).
174 clear IHtypes1 IHtypes2.
175 destruct x1 as [vt1 [pf11 pf12]].
176 exists (vt1,,vt2); split; auto.
178 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
179 set (mapOptionTree_extensional _ _ q) as q'.
186 set (update_branches Γ ξ lev (leaves vt1) (leaves vt2)) as q.
187 set (mapOptionTree_extensional _ _ q) as q'.
191 rewrite <- mapOptionTree_compose.
192 rewrite <- mapOptionTree_compose.
193 rewrite <- mapOptionTree_compose in *.
198 rewrite <- mapOptionTree_compose.
204 Lemma fresh_lemma Γ ξ vars Σ Σ' lev
205 : Σ = mapOptionTree ξ vars ->
207 | mapOptionTree (update_ξ(Γ:=Γ) ξ lev ((vars',Σ')::nil)) vars = Σ
208 /\ mapOptionTree (update_ξ ξ lev ((vars',Σ')::nil)) [vars'] = [Σ' @@ lev] }.
210 set (fresh_lemma' Γ [Σ'] vars Σ ξ lev H) as q.
211 refine (q >>>= fun q' => return _).
214 destruct q' as [varstypes [pf1 [pf2 pfdist]]].
215 destruct varstypes; try destruct o; try destruct p; simpl in *.
216 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
217 inversion pf2; subst.
219 destruct (eqd_dec v v); [ idtac | set (n (refl_equal _)) as n'; inversion n' ].
225 Definition ujudg2exprType Γ (ξ:ExprVarResolver Γ)(Δ:CoercionEnv Γ) Σ τ : Type :=
226 forall vars, Σ = mapOptionTree ξ vars -> FreshM (ITree _ (fun t => Expr Γ Δ ξ t) τ).
228 Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★),
229 ujudg2exprType Γ ξ Δ h t ->
230 ujudg2exprType Γ ξ Δ j t
233 refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} :
234 ujudg2exprType Γ ξ Δ h t ->
235 ujudg2exprType Γ ξ Δ j t :=
236 match r as R in Arrange H C return
237 ujudg2exprType Γ ξ Δ H t ->
238 ujudg2exprType Γ ξ Δ C t
240 | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r)
241 | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r)
242 | RCanL a => let case_RCanL := tt in _
243 | RCanR a => let case_RCanR := tt in _
244 | RuCanL a => let case_RuCanL := tt in _
245 | RuCanR a => let case_RuCanR := tt in _
246 | RAssoc a b c => let case_RAssoc := tt in _
247 | RCossa a b c => let case_RCossa := tt in _
248 | RExch a b => let case_RExch := tt in _
249 | RWeak a => let case_RWeak := tt in _
250 | RCont a => let case_RCont := tt in _
251 | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g)
252 end); clear urule2expr; intros.
255 simpl; unfold ujudg2exprType; intros.
257 apply (X ([],,vars)).
258 simpl; rewrite <- H; auto.
261 simpl; unfold ujudg2exprType; intros.
263 apply (X (vars,,[])).
264 simpl; rewrite <- H; auto.
266 destruct case_RuCanL.
267 simpl; unfold ujudg2exprType; intros.
268 destruct vars; try destruct o; inversion H.
270 apply (X vars2); auto.
272 destruct case_RuCanR.
273 simpl; unfold ujudg2exprType; intros.
274 destruct vars; try destruct o; inversion H.
276 apply (X vars1); auto.
278 destruct case_RAssoc.
279 simpl; unfold ujudg2exprType; intros.
281 destruct vars; try destruct o; inversion H.
282 destruct vars1; try destruct o; inversion H.
283 apply (X (vars1_1,,(vars1_2,,vars2))).
286 destruct case_RCossa.
287 simpl; unfold ujudg2exprType; intros.
289 destruct vars; try destruct o; inversion H.
290 destruct vars2; try destruct o; inversion H.
291 apply (X ((vars1,,vars2_1),,vars2_2)).
295 simpl; unfold ujudg2exprType ; intros.
297 destruct vars; try destruct o; inversion H.
298 apply (X (vars2,,vars1)).
299 inversion H; subst; auto.
302 simpl; unfold ujudg2exprType; intros.
308 simpl; unfold ujudg2exprType ; intros.
310 apply (X (vars,,vars)).
316 intro vars; unfold ujudg2exprType; intro H.
317 destruct vars; try destruct o; inversion H.
318 apply (fun q => e ξ q vars2 H2).
322 unfold ujudg2exprType.
324 apply X with (vars:=vars1,,vars).
330 destruct case_RRight.
331 intro vars; unfold ujudg2exprType; intro H.
332 destruct vars; try destruct o; inversion H.
333 apply (fun q => e ξ q vars1 H1).
337 unfold ujudg2exprType.
339 apply X with (vars:=vars,,vars2).
351 Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' :
352 ITree (LeveledHaskType Γ ★)
353 (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t)
354 (mapOptionTree (ξ' ○ (@fst _ _)) varstypes)
355 -> ELetRecBindings Γ Δ ξ' l varstypes.
358 destruct a; simpl in *.
361 apply ileaf in X. simpl in X.
364 destruct (eqd_dec (unlev (ξ' v)) τ).
368 destruct (eqd_dec h0 l).
371 apply (Prelude_error "level mismatch; should never happen").
372 apply (Prelude_error "letrec type mismatch; should never happen").
376 apply IHvarstypes1; inversion X; auto.
377 apply IHvarstypes2; inversion X; auto.
380 Definition unindex_tree {V}{F} : forall {t:Tree ??V}, ITree V F t -> Tree ??{ v:V & F v }.
381 refine (fix rec t it := match it as IT return Tree ??{ v:V & F v } with
382 | INone => T_Leaf None
383 | ILeaf x y => T_Leaf (Some _)
384 | IBranch _ _ b1 b2 => (rec _ b1),,(rec _ b2)
389 Definition fix_indexing X (F:X->Type)(J:X->Type)(t:Tree ??{ x:X & F x })
390 : ITree { x:X & F x } (fun x => J (projT1 x)) t
391 -> ITree X (fun x:X => J x) (mapOptionTree (@projT1 _ _) t).
393 induction it; simpl in *.
397 simpl; apply IBranch; auto.
400 Definition fix2 {X}{F} : Tree ??{ x:X & FreshM (F x) } -> Tree ??(FreshM { x:X & F x }).
401 refine (fix rec t := match t with
402 | T_Leaf None => T_Leaf None
403 | T_Leaf (Some x) => T_Leaf (Some _)
404 | T_Branch b1 b2 => T_Branch (rec b1) (rec b2)
406 destruct x as [x fx].
407 refine (bind fx' = fx ; return _).
413 Definition case_helper tc Γ Δ lev tbranches avars ξ :
414 forall pcb:{sac : StrongAltCon & ProofCaseBranch tc Γ Δ lev tbranches avars sac},
415 prod (judg2exprType (pcb_judg (projT2 pcb))) {vars' : Tree ??VV & pcb_freevars (projT2 pcb) = mapOptionTree ξ vars'} ->
417 { scb : StrongCaseBranchWithVVs VV eqdec_vv tc avars sac
418 & Expr (sac_Γ sac Γ) (sac_Δ sac Γ avars (weakCK'' Δ)) (scbwv_ξ scb ξ lev) (weakLT' (tbranches @@ lev)) }) (projT1 pcb)).
423 destruct pcb as [sac pcb].
427 destruct s as [vars vars_pf].
429 refine (bind localvars = fresh_lemma' _ (unleaves (vec2list (sac_types sac _ avars))) vars
430 (mapOptionTree weakLT' (pcb_freevars pcb)) (weakLT' ○ ξ) (weakL' lev) _ ; _).
433 rewrite <- mapOptionTree_compose.
435 destruct localvars as [localvars [localvars_pf1 [localvars_pf2 localvars_dist ]]].
436 set (mapOptionTree (@fst _ _) localvars) as localvars'.
438 set (list2vec (leaves localvars')) as localvars''.
439 cut (length (leaves localvars') = sac_numExprVars sac). intro H''.
440 rewrite H'' in localvars''.
441 cut (distinct (vec2list localvars'')). intro H'''.
442 set (@Build_StrongCaseBranchWithVVs _ _ _ _ avars sac localvars'' H''') as scb.
444 refine (bind q = (f (scbwv_ξ scb ξ lev) (vars,,(unleaves (vec2list (scbwv_exprvars scb)))) _) ; return _).
449 rewrite <- mapOptionTree_compose.
464 Definition gather_branch_variables
465 Γ Δ (ξ:VV -> LeveledHaskType Γ ★) tc avars tbranches lev (alts:Tree ?? {sac : StrongAltCon &
466 ProofCaseBranch tc Γ Δ lev tbranches avars sac})
469 mapOptionTreeAndFlatten (fun x => pcb_freevars(Γ:=Γ) (projT2 x)) alts = mapOptionTree ξ vars
470 -> ITree Judg judg2exprType (mapOptionTree (fun x => pcb_judg (projT2 x)) alts)
471 -> ITree _ (fun q => prod (judg2exprType (pcb_judg (projT2 q)))
472 { vars' : _ & pcb_freevars (projT2 q) = mapOptionTree ξ vars' })
478 destruct a; [ idtac | apply INone ].
480 apply ileaf in source.
482 destruct s as [sac pcb].
494 destruct vars; try destruct o; simpl in pf; inversion pf.
499 apply (IHalts1 vars1 H0 X); auto.
500 apply (IHalts2 vars2 H1 X0); auto.
505 Definition rule2expr : forall h j (r:Rule h j), ITree _ judg2exprType h -> ITree _ judg2exprType j.
509 refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with
510 | RArrange a b c d e r => let case_RURule := tt in _
511 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
512 | RLit Γ Δ l _ => let case_RLit := tt in _
513 | RVar Γ Δ σ p => let case_RVar := tt in _
514 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
515 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
516 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
517 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
518 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
519 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
520 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
521 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
522 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
523 | RJoin Γ p lri m x q => let case_RJoin := tt in _
524 | RVoid _ _ => let case_RVoid := tt in _
525 | RBrak Σ a b c n m => let case_RBrak := tt in _
526 | REsc Σ a b c n m => let case_REsc := tt in _
527 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
528 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
529 end); intro X_; try apply ileaf in X_; simpl in X_.
531 destruct case_RURule.
532 apply ILeaf. simpl. intros.
533 set (@urule2expr a b _ _ e r0 ξ) as q.
534 set (fun z => q z) as q'.
536 apply q' with (vars:=vars).
538 unfold ujudg2exprType.
540 apply X_ with (vars:=vars0).
545 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
550 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
555 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
560 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
564 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
565 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
569 destruct case_RGlobal.
570 apply ILeaf; simpl; intros; refine (return ILeaf _ _).
577 refine (fresh_lemma _ ξ vars _ tx x H >>>= (fun pf => _)).
579 destruct pf as [ vnew [ pf1 pf2 ]].
580 set (update_ξ ξ x (((vnew, tx )) :: nil)) as ξ' in *.
581 refine (X_ ξ' (vars,,[vnew]) _ >>>= _).
591 apply ELam with (ev:=vnew).
598 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
601 apply ileaf in X. simpl in X.
605 apply ILeaf; simpl; intros.
610 destruct vars; inversion H.
611 destruct o; inversion H3.
612 refine (X ξ vars1 H3 >>>= fun X' => X0 ξ vars2 H4 >>>= fun X0' => return _).
624 destruct vars. try destruct o; inversion H.
627 set (X1 ξ vars1 H5) as q1.
628 set (X2 ξ vars2 H6) as q2.
629 refine (q1 >>>= fun q1' => q2 >>>= fun q2' => return _).
636 apply (EApp _ _ _ _ _ _ q1' q2').
641 destruct vars; try destruct o; inversion H.
642 refine (fresh_lemma _ ξ vars1 _ σ₂ p H1 >>>= (fun pf => _)).
644 destruct pf as [ vnew [ pf1 pf2 ]].
645 set (update_ξ ξ p (((vnew, σ₂ )) :: nil)) as ξ' in *.
650 refine (X ξ vars2 _ >>>= fun X0' => _).
654 refine (X0 ξ' (vars1,,[vnew]) _ >>>= fun X1' => _).
668 apply ELet with (ev:=vnew)(tv:=σ₂).
673 apply ILeaf; simpl; intros.
678 apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon.
683 apply ILeaf; simpl; intros; refine (X_ (weakLT ○ ξ) vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
684 rewrite mapOptionTree_compose.
687 apply ileaf in X. simpl in *.
691 destruct case_RAppCo.
692 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
698 destruct case_RAbsCo.
699 apply ILeaf; simpl; intros; refine (X_ ξ vars _ >>>= fun X => return ILeaf _ _). apply FreshMon.
704 destruct case_RLetRec.
705 apply ILeaf; simpl; intros.
706 refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
707 destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
708 refine (X_ ((update_ξ ξ t (leaves varstypes)))
709 (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_. apply FreshMon.
715 inversion X; subst; clear X.
717 apply (@ELetRec _ _ _ _ _ _ _ varstypes).
718 apply (@letrec_helper Γ Δ t varstypes).
719 rewrite <- pf2 in X1.
720 rewrite mapOptionTree_compose.
726 apply ILeaf; simpl; intros.
733 (* body_freevars and alts_freevars are the types of variables in the body and alternatives (respectively) which are free
734 * from the viewpoint just outside the case block -- i.e. not bound by any of the branches *)
735 rename Σ into body_freevars_types.
736 rename vars into all_freevars.
737 rename X0 into body_expr.
738 rename X into alts_exprs.
740 destruct all_freevars; try destruct o; inversion H.
741 rename all_freevars2 into body_freevars.
742 rename all_freevars1 into alts_freevars.
744 set (gather_branch_variables _ _ _ _ _ _ _ _ _ H1 alts_exprs) as q.
745 set (itmap (fun pcb alt_expr => case_helper tc Γ Δ lev tbranches avars ξ pcb alt_expr) q) as alts_exprs'.
746 apply fix_indexing in alts_exprs'.
747 simpl in alts_exprs'.
748 apply unindex_tree in alts_exprs'.
749 simpl in alts_exprs'.
750 apply fix2 in alts_exprs'.
751 apply treeM in alts_exprs'.
753 refine ( alts_exprs' >>>= fun Y =>
755 >>>= fun X => return ILeaf _ (@ECase _ _ _ _ _ _ _ _ _ (ileaf X) Y)); auto.
761 Fixpoint closed2expr h j (pn:@SIND _ Rule h j) {struct pn} : ITree _ judg2exprType h -> ITree _ judg2exprType j :=
762 match pn in @SIND _ _ H J return ITree _ judg2exprType H -> ITree _ judg2exprType J with
763 | scnd_weak _ => let case_nil := tt in fun _ => INone _ _
764 | scnd_comp x h c cnd' r => let case_rule := tt in fun q => rule2expr _ _ r (closed2expr _ _ cnd' q)
765 | scnd_branch _ _ _ c1 c2 => let case_branch := tt in fun q => IBranch _ _ (closed2expr _ _ c1 q) (closed2expr _ _ c2 q)
768 Lemma manyFresh : forall Γ Σ (ξ0:VV -> LeveledHaskType Γ ★),
769 FreshM { vars : _ & { ξ : VV -> LeveledHaskType Γ ★ & Σ = mapOptionTree ξ vars } }.
771 induction Σ; intro ξ.
774 set (fresh_lemma' Γ [τ] [] [] ξ l (refl_equal _)) as q.
775 refine (q >>>= fun q' => return _).
778 destruct q' as [varstypes [pf1 [pf2 distpf]]].
779 exists (mapOptionTree (@fst _ _) varstypes).
780 exists (update_ξ ξ l (leaves varstypes)).
785 refine (bind f1 = IHΣ1 ξ ; _).
787 destruct f1 as [vars1 [ξ1 pf1]].
788 refine (bind f2 = IHΣ2 ξ1 ; _).
790 destruct f2 as [vars2 [ξ2 pf22]].
792 exists (vars1,,vars2).
800 Definition proof2expr Γ Δ τ Σ (ξ0: VV -> LeveledHaskType Γ ★)
801 {zz:ToString VV} : ND Rule [] [Γ > Δ > Σ |- [τ]] ->
802 FreshM (???{ ξ : _ & Expr Γ Δ ξ τ}).
804 set (mkSIND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) as cnd.
805 apply closed2expr in cnd.
809 refine (bind ξvars = manyFresh _ Σ ξ0; _).
811 destruct ξvars as [vars ξpf].
812 destruct ξpf as [ξ pf].
813 refine (cnd ξ vars _ >>>= fun it => _).
816 refine (return OK _).
822 End HaskProofToStrong.