1 (*********************************************************************************************************************************)
4 (* Skolemizes the portion of a proof which uses judgments at level >0 *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import Coq.Strings.String.
13 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskCoreVars.
18 Require Import HaskWeakTypes.
19 Require Import HaskWeakVars.
20 Require Import HaskLiterals.
21 Require Import HaskTyCons.
22 Require Import HaskStrongTypes.
23 Require Import HaskProof.
24 Require Import NaturalDeduction.
26 Require Import HaskStrongTypes.
27 Require Import HaskStrong.
28 Require Import HaskProof.
29 Require Import HaskStrongToProof.
30 Require Import HaskProofToStrong.
31 Require Import HaskWeakToStrong.
34 Set Printing Width 130.
36 Section HaskSkolemizer.
39 Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
42 | TAll _ y => TAll _ (fun v => debruijn2phoas (y (TVar v)))
43 | TApp _ _ x y => TApp (debruijn2phoas x) (debruijn2phoas y)
45 | TCoerc _ t1 t2 t => TCoerc (debruijn2phoas t1) (debruijn2phoas t2) (debruijn2phoas t)
47 | TCode v e => TCode (debruijn2phoas v) (debruijn2phoas e)
48 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
50 with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
51 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
52 | TyFunApp_nil => TyFunApp_nil
53 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas t) (debruijn2phoasyFunApp _ rest)
56 Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
58 | RBrak _ _ _ _ _ _ => False
59 | REsc _ _ _ _ _ _ => False
63 Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
66 | a::b => mkArrows b (a ---> t)
70 Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
73 | a::b => unleaves_ (t,,[a @@ lev]) b lev
76 (* weak inverse of "leaves" *)
77 Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
81 | (a::b) => [a],,(unleaves_ b)
84 (* rules of skolemized proofs *)
85 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
86 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
87 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
88 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
91 | T_Leaf (Some (_ @@ lev)) => lev
99 Fixpoint take_trustme {Γ}
101 (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
102 : list (HaskType Γ ★) :=
106 | S n' => (fun TV ite => match l TV ite with
107 | nil => Prelude_error "impossible"
111 take_trustme n' (fun TV ite => match l TV ite with
112 | nil => Prelude_error "impossible"
117 Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
118 (forall tv ite, f tv ite = g tv ite) -> f=g.
120 Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
123 (count_arg_types (ht _ (ite_unit _)))
124 (fun TV ite => take_arg_types (ht TV ite))).
126 Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
127 fun TV ite => drop_arg_types (ht TV ite).
129 Implicit Arguments take_arg_types_as_tree [[Γ]].
130 Implicit Arguments drop_arg_types_as_tree [[Γ]].
132 Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
133 Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
134 (take_arg_types_as_tree (tx ---> te) @@@ lev).
136 destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
140 unfold take_arg_types_as_tree.
141 Opaque take_arg_types_as_tree.
143 destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
145 replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
147 apply phoas_extensionality.
149 apply (Prelude_error "should not be possible").
151 Transparent take_arg_types_as_tree.
153 Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
154 Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
155 ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
157 destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
161 unfold take_arg_types_as_tree.
162 Opaque take_arg_types_as_tree.
164 destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
166 replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
168 apply phoas_extensionality.
170 apply (Prelude_error "should not be possible").
172 Transparent take_arg_types_as_tree.
174 Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
175 drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
177 unfold drop_arg_types_as_tree.
182 Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
183 (* | SFlat : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
184 | SFlat : forall h c, Rule h c -> SRule h c
185 | SBrak : forall Γ Δ t ec Σ l,
187 [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
188 [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
190 | SEsc : forall Γ Δ t ec Σ l,
192 [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
193 [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
196 Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
197 match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
199 Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
200 match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
202 Definition skolemize_judgment (j:Judg) : Judg :=
205 match getjlev Σ₂ with
207 | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
211 Definition check_hof : forall {Γ}(t:HaskType Γ ★),
214 (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
216 destruct (eqd_dec (take_arg_types_as_tree t) []);
217 destruct (eqd_dec (drop_arg_types_as_tree t) t).
224 Opaque take_arg_types_as_tree.
225 Definition skolemize_proof :
228 ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
230 eapply nd_map'; [ idtac | apply X ].
234 refine (match X as R in Rule H C with
235 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
236 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
237 | RLit Γ Δ l _ => let case_RLit := tt in _
238 | RVar Γ Δ σ lev => let case_RVar := tt in _
239 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
240 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
241 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
242 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
243 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
244 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
245 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
246 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
247 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
248 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
249 | RJoin Γ p lri m x q => let case_RJoin := tt in _
250 | RVoid _ _ => let case_RVoid := tt in _
251 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
252 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
253 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
254 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
257 destruct case_RArrange.
259 destruct (getjlev x).
272 destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
278 destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
298 set (check_hof (@literalType l Γ)) as hof.
299 destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
304 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
312 apply nd_rule; apply SFlat; apply RVar.
313 set (check_hof σ) as hof.
314 destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
319 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
324 destruct case_RGlobal.
327 apply nd_rule; apply SFlat; apply RGlobal.
328 set (check_hof (l wev)) as hof.
329 destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
334 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
362 apply (Prelude_error "found RCast at level >0").
366 destruct (getjlev x).
367 destruct (getjlev q).
371 apply (Prelude_error "found RJoin at level >0").
372 apply (Prelude_error "found RJoin at level >0").
381 set (check_hof tx) as hof_tx.
382 destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
388 eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
393 eapply take_unarrange.
395 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
396 eapply nd_rule; eapply SFlat; apply RWhere.
404 set (check_hof σ₁) as hof_tx.
405 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
411 eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR | eapply nd_id ].
413 set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
414 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
415 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
423 destruct case_RWhere.
429 set (check_hof σ₁) as hof_tx.
430 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
436 eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RCanR ].
437 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RAssoc ].
438 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply RLeft; eapply RAssoc ].
439 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
440 apply nd_prod; [ idtac | eapply nd_id ].
441 eapply nd_rule; apply SFlat; eapply RArrange.
455 destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
456 apply (Prelude_error "RAppT at depth>0").
460 destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
461 apply (Prelude_error "RAbsT at depth>0").
463 destruct case_RAppCo.
465 destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
467 apply (Prelude_error "RAppCo at depth>0").
469 destruct case_RAbsCo.
471 destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
472 apply (Prelude_error "RAbsCo at depth>0").
474 destruct case_RLetRec.
477 destruct (getjlev (y @@@ nil)).
480 apply (@RLetRec Γ Δ lri x y nil).
481 apply (Prelude_error "RLetRec at depth>0").
482 apply (Prelude_error "RLetRec at depth>0").
486 apply (Prelude_error "CASE: BIG FIXME").
488 Transparent take_arg_types_as_tree.