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 Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
98 Fixpoint grab (n:nat) {T} (l:list T) : T :=
100 | nil => Prelude_error "grab failed"
101 | h::t => match n with
107 Fixpoint count' (n:nat)(ln:list nat) : list nat :=
110 | S n' => count' n' (n'::ln)
113 Definition count (n:nat) := count' n nil.
115 Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) :=
116 map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))).
118 Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) :=
119 (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))).
121 Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
122 fun TV ite => drop_arg_types (ht TV ite).
124 Implicit Arguments take_arg_types_as_tree [[Γ]].
125 Implicit Arguments drop_arg_types_as_tree [[Γ]].
127 Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
128 take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
130 unfold take_arg_types_as_tree; simpl.
131 unfold rebundle at 1.
135 Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
136 drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
138 unfold drop_arg_types_as_tree.
143 Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
144 (* | SFlat : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
145 | SFlat : forall h c, Rule h c -> SRule h c
146 | SBrak : forall Γ Δ t ec Σ l,
148 [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
149 [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
151 | SEsc : forall Γ Δ t ec Σ l,
153 [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
154 [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
157 Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
158 match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
160 Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
161 match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
163 Definition skolemize_judgment (j:Judg) : Judg :=
166 match getjlev Σ₂ with
168 | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
172 Definition check_hof : forall {Γ}(t:HaskType Γ ★),
175 (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
177 destruct (eqd_dec (take_arg_types_as_tree t) []);
178 destruct (eqd_dec (drop_arg_types_as_tree t) t).
185 Definition skolemize_proof :
188 ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
190 eapply nd_map'; [ idtac | apply X ].
194 refine (match X as R in Rule H C with
195 | RArrange Γ Δ a b x d => let case_RArrange := tt in _
196 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
197 | RLit Γ Δ l _ => let case_RLit := tt in _
198 | RVar Γ Δ σ lev => let case_RVar := tt in _
199 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
200 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
201 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
202 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
203 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
204 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
205 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
206 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
207 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
208 | RJoin Γ p lri m x q => let case_RJoin := tt in _
209 | RVoid _ _ => let case_RVoid := tt in _
210 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
211 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
212 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
213 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
216 destruct case_RArrange.
218 destruct (getjlev x).
231 destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
237 destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
257 set (check_hof (@literalType l Γ)) as hof.
258 destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
263 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
271 apply nd_rule; apply SFlat; apply RVar.
272 set (check_hof σ) as hof.
273 destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
278 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
283 destruct case_RGlobal.
286 apply nd_rule; apply SFlat; apply RGlobal.
287 set (check_hof (l wev)) as hof.
288 destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
293 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
318 apply (Prelude_error "found RCast at level >0").
322 destruct (getjlev x).
323 destruct (getjlev q).
327 apply (Prelude_error "found RJoin at level >0").
328 apply (Prelude_error "found RJoin at level >0").
338 set (check_hof tx) as hof_tx.
339 destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
344 set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
345 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
346 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
347 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
354 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
355 apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch.
363 set (check_hof σ₂) as hof_tx.
364 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
368 set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
369 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
370 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
371 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
372 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
379 eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
380 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
395 destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
396 apply (Prelude_error "RAppT at depth>0").
400 destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
401 apply (Prelude_error "RAbsT at depth>0").
403 destruct case_RAppCo.
405 destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
407 apply (Prelude_error "RAppCo at depth>0").
409 destruct case_RAbsCo.
411 destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
412 apply (Prelude_error "RAbsCo at depth>0").
414 destruct case_RLetRec.
417 destruct (getjlev (y @@@ nil)).
420 apply (@RLetRec Γ Δ lri x y nil).
421 apply (Prelude_error "RLetRec at depth>0").
422 apply (Prelude_error "RLetRec at depth>0").
426 apply (Prelude_error "CASE: BIG FIXME").