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.
21 {eqdec_vv:EqDecidable VV}
22 {fresh: forall (l:list VV), { lf:VV & distinct (lf::l) }}.
24 Definition Exprs (Γ:TypeEnv)(Δ:CoercionEnv Γ)(ξ:VV -> LeveledHaskType Γ ★)(τ:Tree ??(LeveledHaskType Γ ★)) :=
25 ITree _ (fun τ => Expr Γ Δ ξ τ) τ.
27 Definition judg2exprType (j:Judg) : Type :=
29 (Γ > Δ > Σ |- τ) => { ξ:VV -> LeveledHaskType Γ ★ & Exprs Γ Δ ξ τ }
32 (* reminder: need to pass around uniq-supplies *)
36 ITree _ judg2exprType h ->
41 refine (match r as R in Rule H C return C=[Γ > Δ > t |- t0] -> _ with
42 | RURule a b c d e => let case_RURule := tt in _
43 | RNote x n z => let case_RNote := tt in _
44 | RLit Γ Δ l _ => let case_RLit := tt in _
45 | RVar Γ Δ σ p => let case_RVar := tt in _
46 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
47 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
48 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
49 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
50 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
51 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
52 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
53 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
54 | RLetRec Γ p lri x y => let case_RLetRec := tt in _
55 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
56 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
57 | RCase Σ Γ T κlen κ θ ldcd τ => let case_RCase := tt in _
58 | RBrak Σ a b c n m => let case_RBrak := tt in _
59 | REsc Σ a b c n m => let case_REsc := tt in _
60 end (refl_equal _) ); intros.
63 destruct d; [ destruct o | idtac ]; inversion H; subst.
66 refine (match e as R in URule H C return C=[a >> b > t1 |- t2] -> _ with
67 | RLeft h c ctx r => let case_RLeft := tt in _
68 | RRight h c ctx r => let case_RRight := tt in _
69 | RCanL t a => let case_RCanL := tt in _
70 | RCanR t a => let case_RCanR := tt in _
71 | RuCanL t a => let case_RuCanL := tt in _
72 | RuCanR t a => let case_RuCanR := tt in _
73 | RAssoc t a b c => let case_RAssoc := tt in _
74 | RCossa t a b c => let case_RCossa := tt in _
75 | RExch t a b => let case_RExch := tt in _
76 | RWeak t a => let case_RWeak := tt in _
77 | RCont t a => let case_RCont := tt in _
78 end (refl_equal _) ); intros.
80 destruct case_RCanL. admit.
81 destruct case_RCanR. admit.
82 destruct case_RuCanL. admit.
83 destruct case_RuCanR. admit.
84 destruct case_RAssoc. admit.
85 destruct case_RCossa. admit.
86 destruct case_RLeft. admit.
87 destruct case_RRight. admit.
88 destruct case_RExch. admit.
89 destruct case_RWeak. admit.
90 destruct case_RCont. admit.
91 destruct case_RBrak. admit.
92 destruct case_REsc. admit.
93 destruct case_RNote. admit.
94 destruct case_RLit. admit.
95 destruct case_RVar. admit.
96 destruct case_RLam. admit.
97 destruct case_RCast. admit.
98 destruct case_RBindingGroup. admit.
99 destruct case_RApp. admit.
100 destruct case_RLet. admit.
101 destruct case_REmptyGroup. admit.
102 destruct case_RAppT. admit.
103 destruct case_RAbsT. admit.
104 destruct case_RAppCo. admit.
105 destruct case_RAbsCo. admit.
106 destruct case_RLetRec. admit.
107 destruct case_RCase. admit.
110 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
112 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
113 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
114 | cnd_weak => let case_nil := tt in _
115 | cnd_rule h c cnd' r => let case_rule := tt in (fun rest => _) (closed2expr' _ cnd')
116 | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
117 end)); clear closed2expr'; intros; subst.
123 set (@rule2expr h) as q.
131 apply no_rules_with_empty_conclusion in r.
136 apply systemfc_all_rules_one_conclusion in r.
139 destruct case_branch.
145 Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ ★ & Expr Γ Δ ξ τ }.
147 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
148 apply closed2expr in cnd.
149 inversion cnd; subst.
159 End HaskProofToStrong.