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)
69 Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
72 | a::b => unleaves_ (t,,[a @@ lev]) b lev
75 (* rules of skolemized proofs *)
76 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
77 Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
78 match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
79 Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
82 | T_Leaf (Some (_ @@ lev)) => lev
90 Fixpoint take_trustme {Γ}
92 (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
93 : list (HaskType Γ ★) :=
97 | S n' => (fun TV ite => match l TV ite with
98 | nil => Prelude_error "impossible"
102 take_trustme n' (fun TV ite => match l TV ite with
103 | nil => Prelude_error "impossible"
108 Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
111 (count_arg_types (ht _ (ite_unit _)))
112 (fun TV ite => take_arg_types (ht TV ite))).
114 Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
115 fun TV ite => drop_arg_types (ht TV ite).
117 Implicit Arguments take_arg_types_as_tree [[Γ]].
118 Implicit Arguments drop_arg_types_as_tree [[Γ]].
120 Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
121 take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
123 unfold take_arg_types_as_tree at 1.
128 Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
129 drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
131 unfold drop_arg_types_as_tree.
136 Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
137 (* | SFlat : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
138 | SFlat : forall h c, Rule h c -> SRule h c
139 | SBrak : forall Γ Δ t ec Σ l,
141 [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
142 [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
144 | SEsc : forall Γ Δ t ec Σ l,
146 [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
147 [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
150 Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
151 match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
153 Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
154 match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
156 Definition skolemize_judgment (j:Judg) : Judg :=
159 match getjlev Σ₂ with
161 | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
165 Definition check_hof : forall {Γ}(t:HaskType Γ ★),
168 (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
170 destruct (eqd_dec (take_arg_types_as_tree t) []);
171 destruct (eqd_dec (drop_arg_types_as_tree t) t).
178 Opaque take_arg_types_as_tree.
179 Definition skolemize_proof :
182 ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
184 eapply nd_map'; [ idtac | apply X ].
188 refine (match X as R in Rule H C with
189 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
190 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
191 | RLit Γ Δ l _ => let case_RLit := tt in _
192 | RVar Γ Δ σ lev => let case_RVar := tt in _
193 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
194 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
195 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
196 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
197 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
198 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
199 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
200 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
201 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
202 | RJoin Γ p lri m x q => let case_RJoin := tt in _
203 | RVoid _ _ => let case_RVoid := tt in _
204 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
205 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
206 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
207 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
210 destruct case_RArrange.
212 destruct (getjlev x).
225 destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
231 destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
251 set (check_hof (@literalType l Γ)) as hof.
252 destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
257 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
265 apply nd_rule; apply SFlat; apply RVar.
266 set (check_hof σ) as hof.
267 destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
272 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
277 destruct case_RGlobal.
280 apply nd_rule; apply SFlat; apply RGlobal.
281 set (check_hof (l wev)) as hof.
282 destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
287 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
313 apply (Prelude_error "found RCast at level >0").
317 destruct (getjlev x).
318 destruct (getjlev q).
322 apply (Prelude_error "found RJoin at level >0").
323 apply (Prelude_error "found RJoin at level >0").
333 set (check_hof tx) as hof_tx.
334 destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
339 set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
340 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
341 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
342 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
349 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
350 apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch.
358 set (check_hof σ₂) as hof_tx.
359 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
363 set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
364 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
365 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
366 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
367 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
374 eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
375 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
390 destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
391 apply (Prelude_error "RAppT at depth>0").
395 destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
396 apply (Prelude_error "RAbsT at depth>0").
398 destruct case_RAppCo.
400 destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
402 apply (Prelude_error "RAppCo at depth>0").
404 destruct case_RAbsCo.
406 destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
407 apply (Prelude_error "RAbsCo at depth>0").
409 destruct case_RLetRec.
412 destruct (getjlev (y @@@ nil)).
415 apply (@RLetRec Γ Δ lri x y nil).
416 apply (Prelude_error "RLetRec at depth>0").
417 apply (Prelude_error "RLetRec at depth>0").
421 apply (Prelude_error "CASE: BIG FIXME").
423 Transparent take_arg_types_as_tree.