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 | RJoin Γ p lri m x q => let case_RJoin := tt in _
249 | RVoid _ _ => let case_RVoid := tt in _
250 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
251 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
252 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
253 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
256 destruct case_RArrange.
258 destruct (getjlev x).
271 destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
277 destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
297 set (check_hof (@literalType l Γ)) as hof.
298 destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
303 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
311 apply nd_rule; apply SFlat; apply RVar.
312 set (check_hof σ) as hof.
313 destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
318 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
323 destruct case_RGlobal.
326 apply nd_rule; apply SFlat; apply RGlobal.
327 set (check_hof (l wev)) as hof.
328 destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
333 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
361 apply (Prelude_error "found RCast at level >0").
365 destruct (getjlev x).
366 destruct (getjlev q).
370 apply (Prelude_error "found RJoin at level >0").
371 apply (Prelude_error "found RJoin at level >0").
380 set (check_hof tx) as hof_tx.
381 destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
386 set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
387 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
388 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
389 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
399 eapply RComp; [ idtac | eapply RAssoc ].
401 eapply RComp; [ idtac | apply RExch ].
402 apply take_unarrange.
410 set (check_hof σ₂) as hof_tx.
411 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
415 set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
416 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
417 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
418 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
419 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
426 eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
427 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
442 destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
443 apply (Prelude_error "RAppT at depth>0").
447 destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
448 apply (Prelude_error "RAbsT at depth>0").
450 destruct case_RAppCo.
452 destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
454 apply (Prelude_error "RAppCo at depth>0").
456 destruct case_RAbsCo.
458 destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
459 apply (Prelude_error "RAbsCo at depth>0").
461 destruct case_RLetRec.
464 destruct (getjlev (y @@@ nil)).
467 apply (@RLetRec Γ Δ lri x y nil).
468 apply (Prelude_error "RLetRec at depth>0").
469 apply (Prelude_error "RLetRec at depth>0").
473 apply (Prelude_error "CASE: BIG FIXME").
475 Transparent take_arg_types_as_tree.