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}.
21 Definition Exprs Γ Δ ξ τ :=
22 ITree _ (fun τ => Expr Γ Δ ξ τ) τ.
24 Definition judg2exprType (j:Judg) : Type :=
26 (Γ > Δ > Σ |- τ) => forall (ξ:VV -> LeveledHaskType Γ ★ ) vars, Σ=mapOptionTree ξ vars -> Exprs Γ Δ ξ τ
29 Definition judges2exprType (j:Tree ??Judg) : Type :=
30 ITree _ judg2exprType j.
32 Definition urule2expr Γ Δ : forall h j (r:@URule Γ Δ h j),
33 judges2exprType (mapOptionTree UJudg2judg h) -> judges2exprType (mapOptionTree UJudg2judg j).
37 refine (match r as R in URule H C
38 return judges2exprType (mapOptionTree UJudg2judg H) -> judges2exprType (mapOptionTree UJudg2judg C) with
39 | RLeft h c ctx r => let case_RLeft := tt in _
40 | RRight h c ctx r => let case_RRight := tt in _
41 | RCanL t a => let case_RCanL := tt in _
42 | RCanR t a => let case_RCanR := tt in _
43 | RuCanL t a => let case_RuCanL := tt in _
44 | RuCanR t a => let case_RuCanR := tt in _
45 | RAssoc t a b c => let case_RAssoc := tt in _
46 | RCossa t a b c => let case_RCossa := tt in _
47 | RExch t a b => let case_RExch := tt in _
48 | RWeak t a => let case_RWeak := tt in _
49 | RCont t a => let case_RCont := tt in _
53 apply ILeaf; simpl; intros.
56 apply (X0 ξ ([],,vars)).
57 simpl; rewrite <- H; auto.
60 apply ILeaf; simpl; intros.
63 apply (X0 ξ (vars,,[])).
64 simpl; rewrite <- H; auto.
67 apply ILeaf; simpl; intros.
68 destruct vars; try destruct o; inversion H.
71 apply (X0 ξ vars2); auto.
74 apply ILeaf; simpl; intros.
75 destruct vars; try destruct o; inversion H.
78 apply (X0 ξ vars1); auto.
81 apply ILeaf; simpl; intros.
84 destruct vars; try destruct o; inversion H.
85 destruct vars1; try destruct o; inversion H.
86 apply (X0 ξ (vars1_1,,(vars1_2,,vars2))).
90 apply ILeaf; simpl; intros.
93 destruct vars; try destruct o; inversion H.
94 destruct vars2; try destruct o; inversion H.
95 apply (X0 ξ ((vars1,,vars2_1),,vars2_2)).
99 (* this will require recursion *)
102 destruct case_RRight.
103 (* this will require recursion *)
107 apply ILeaf; simpl; intros.
110 destruct vars; try destruct o; inversion H.
111 apply (X0 ξ (vars2,,vars1)).
112 inversion H; subst; auto.
115 apply ILeaf; simpl; intros.
122 apply ILeaf; simpl; intros.
125 apply (X0 ξ (vars,,vars)).
131 Definition rule2expr : forall h j (r:Rule h j), judges2exprType h -> judges2exprType j.
135 refine (match r as R in Rule H C return judges2exprType H -> judges2exprType C with
136 | RURule a b c d e => let case_RURule := tt in _
137 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
138 | RLit Γ Δ l _ => let case_RLit := tt in _
139 | RVar Γ Δ σ p => let case_RVar := tt in _
140 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
141 | RLam Γ Δ Σ tx te x => let case_RLam := tt in _
142 | RCast Γ Δ Σ σ τ γ x => let case_RCast := tt in _
143 | RAbsT Γ Δ Σ κ σ a => let case_RAbsT := tt in _
144 | RAppT Γ Δ Σ κ σ τ y => let case_RAppT := tt in _
145 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _
146 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _
147 | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _
148 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _
149 | RLetRec Γ p lri x y => let case_RLetRec := tt in _
150 | RBindingGroup Γ p lri m x q => let case_RBindingGroup := tt in _
151 | REmptyGroup _ _ => let case_REmptyGroup := tt in _
152 | RCase Σ Γ T κlen κ θ ldcd τ => let case_RCase := tt in _
153 | RBrak Σ a b c n m => let case_RBrak := tt in _
154 | REsc Σ a b c n m => let case_REsc := tt in _
157 destruct case_RURule.
163 apply ILeaf; simpl; intros; apply ILeaf.
166 set (X0 ξ vars H) as X'.
171 apply ILeaf; simpl; intros; apply ILeaf.
174 set (X0 ξ vars H) as X'.
179 apply ILeaf; simpl; intros; apply ILeaf.
184 set (X0 ξ vars H) as x1.
189 apply ILeaf; simpl; intros; apply ILeaf.
193 apply ILeaf; simpl; intros; apply ILeaf.
194 destruct vars; simpl in H; inversion H; destruct o. inversion H1. rewrite H2.
198 destruct case_RGlobal.
199 apply ILeaf; simpl; intros; apply ILeaf.
204 apply ILeaf; simpl; intros; apply ILeaf.
205 (* need a fresh variable here *)
209 apply ILeaf; simpl; intros; apply ILeaf.
214 set (X0 ξ vars H) as q.
218 destruct case_RBindingGroup.
219 apply ILeaf; simpl; intros.
223 destruct vars; inversion H.
224 destruct o; inversion H5.
225 set (X2 _ _ H5) as q1.
226 set (X3 _ _ H6) as q2.
230 apply ILeaf; simpl; intros; apply ILeaf.
234 destruct vars; try destruct o; inversion H.
235 set (X2 _ _ H5) as q1.
236 set (X3 _ _ H6) as q2.
244 apply ILeaf; simpl; intros; apply ILeaf.
245 (* FIXME: need a var here, and other work *)
248 destruct case_REmptyGroup.
249 apply ILeaf; simpl; intros.
253 apply ILeaf; simpl; intros; apply ILeaf.
261 apply ILeaf; simpl; intros; apply ILeaf.
265 set (X0 (weakLT ○ ξ) vars) as q.
266 rewrite mapOptionTree_compose in q.
268 set (q (refl_equal _)) as q'.
272 destruct case_RAppCo.
273 apply ILeaf; simpl; intros; apply ILeaf.
281 destruct case_RAbsCo.
282 apply ILeaf; simpl; intros; apply ILeaf.
288 destruct case_RLetRec.
296 Definition closed2expr : forall c (pn:@ClosedND _ Rule c), ITree _ judg2exprType c.
298 fix closed2expr' j (pn:@ClosedND _ Rule j) {struct pn} : ITree _ judg2exprType j :=
299 match pn in @ClosedND _ _ J return ITree _ judg2exprType J with
300 | cnd_weak => let case_nil := tt in _
301 | cnd_rule h c cnd' r => let case_rule := tt in (fun rest => _) (closed2expr' _ cnd')
302 | cnd_branch _ _ c1 c2 => let case_branch := tt in (fun rest1 rest2 => _) (closed2expr' _ c1) (closed2expr' _ c2)
303 end)); clear closed2expr'; intros; subst.
313 destruct case_branch.
319 Definition proof2expr Γ Δ τ Σ : ND Rule [] [Γ > Δ > Σ |- [τ]] -> { ξ:VV -> LeveledHaskType Γ ★ & Expr Γ Δ ξ τ }.
321 set (closedFromSCND _ _ (mkSCND systemfc_all_rules_one_conclusion _ _ _ pf (scnd_weak [])) cnd_weak) as cnd.
322 apply closed2expr in cnd.
323 inversion cnd; subst.
333 End HaskProofToStrong.