Require Import HaskProofToStrong.
Require Import HaskWeakToStrong.
+Require Import HaskSkolemizer.
+
Open Scope nd_scope.
Set Printing Width 130.
auto.
Qed.
+ Lemma take_lemma' : forall Γ (lev:HaskLevel Γ) x, take_lev lev (x @@@ lev) = x @@@ lev.
+ intros.
+ induction x.
+ destruct a; simpl; try reflexivity.
+ apply take_lemma.
+ simpl.
+ rewrite <- IHx1 at 2.
+ rewrite <- IHx2 at 2.
+ reflexivity.
+ Qed.
+(*
+ Lemma drop_lev_lemma' : forall Γ (lev:HaskLevel Γ) x, drop_lev lev (x @@@ lev) = [].
+ intros.
+ induction x.
+ destruct a; simpl; try reflexivity.
+ apply drop_lev_lemma.
+ simpl.
+ change (@drop_lev _ lev (x1 @@@ lev ,, x2 @@@ lev))
+ with ((@drop_lev _ lev (x1 @@@ lev)) ,, (@drop_lev _ lev (x2 @@@ lev))).
+ simpl.
+ rewrite IHx1.
+ rewrite IHx2.
+ reflexivity.
+ Qed.
+*)
Ltac drop_simplify :=
match goal with
| [ |- context[@drop_lev ?G ?L [ ?X @@ ?L ] ] ] =>
rewrite (drop_lev_lemma G L X)
+(*
+ | [ |- context[@drop_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
+ rewrite (drop_lev_lemma' G L X)
+*)
| [ |- context[@drop_lev ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] =>
rewrite (drop_lev_lemma_s G L E X)
| [ |- context[@drop_lev ?G ?N (?A,,?B)] ] =>
match goal with
| [ |- context[@take_lev ?G ?L [ ?X @@ ?L ] ] ] =>
rewrite (take_lemma G L X)
+ | [ |- context[@take_lev ?G ?L [ ?X @@@ ?L ] ] ] =>
+ rewrite (take_lemma' G L X)
| [ |- context[@take_lev ?G ?N (?A,,?B)] ] =>
change (@take_lev G N (A,,B)) with ((@take_lev G N A),,(@take_lev G N B))
| [ |- context[@take_lev ?G ?N (T_Leaf None)] ] =>
| TCon tc => TCon tc
| TCoerc _ t1 t2 t => TCoerc (flatten_rawtype t1) (flatten_rawtype t2) (flatten_rawtype t)
| TArrow => TArrow
- | TCode ec e => ga_mk_raw ec [] [flatten_rawtype e]
+ | TCode ec e => let e' := flatten_rawtype e
+ in ga_mk_raw ec (unleaves' (take_arg_types e')) [drop_arg_types e']
| TyFunApp tfc kl k lt => TyFunApp tfc kl k (flatten_rawtype_list _ lt)
end
with flatten_rawtype_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk :=
Fixpoint levels_to_tcode {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ :=
match lev with
- | nil => ht
- | ec::lev' => fun TV ite => TCode (v2t ec TV ite) (levels_to_tcode ht lev' TV ite)
+ | nil => flatten_type ht
+ | ec::lev' => @ga_mk _ (v2t ec) [] [levels_to_tcode ht lev']
end.
Definition flatten_leveled_type {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ :=
- flatten_type (levels_to_tcode (unlev ht) (getlev ht)) @@ nil.
+ levels_to_tcode (unlev ht) (getlev ht) @@ nil.
(* AXIOMS *)
apply ga_second.
Defined.
- Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ,
+ Lemma ga_unkappa : ∀ Γ Δ ec l z a b Σ,
ND Rule
- [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
- [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ].
+ [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ]
+ [Γ > Δ > Σ,,[@ga_mk Γ ec z a @@ l] |- [@ga_mk Γ ec z b @@ l] ].
intros.
- set (ga_comp Γ Δ ec l [] a b) as q.
+ set (ga_comp Γ Δ ec l z a b) as q.
set (@RLet Γ Δ) as q'.
- set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''.
+ set (@RLet Γ Δ [@ga_mk _ ec z a @@ l] Σ (@ga_mk _ ec z b) (@ga_mk _ ec a b) l) as q''.
eapply nd_comp.
Focus 2.
eapply nd_rule.
apply q.
Defined.
+ Lemma ga_unkappa' : ∀ Γ Δ ec l a b Σ x,
+ ND Rule
+ [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ]
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply ga_first.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod.
+ apply postcompose.
+ apply ga_uncancell.
+ apply precompose.
+ Defined.
+
+ Lemma ga_kappa' : ∀ Γ Δ ec l a b Σ x,
+ ND Rule
+ [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec x b @@ l] ]
+ [Γ > Δ > Σ |- [@ga_mk Γ ec (a,,x) b @@ l] ].
+ apply (Prelude_error "ga_kappa not supported yet (BIG FIXME)").
+ Defined.
+
(* useful for cutting down on the pretty-printed noise
Notation "` x" := (take_lev _ x) (at level 20).
Definition arrange_brak : forall Γ Δ ec succ t,
ND Rule
[Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
- [(@ga_mk _ (v2t ec) []
- (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ)))
- @@ nil] |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
- [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
+ [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]]
+ [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]].
intros.
unfold drop_lev.
set (@arrange' _ succ (levelMatch (ec::nil))) as q.
unfold flatten_leveled_type.
simpl.
unfold flatten_type.
+ simpl.
+ unfold ga_mk.
+ simpl.
apply RVar.
simpl.
apply ga_id.
Definition arrange_esc : forall Γ Δ ec succ t,
ND Rule
- [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]]
+ [Γ > Δ > mapOptionTree (flatten_leveled_type ) succ |- [t @@ nil]]
[Γ > Δ > mapOptionTree (flatten_leveled_type ) (drop_lev (ec :: nil) succ),,
- [(@ga_mk _ (v2t ec) []
- (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil]
- |- [(@ga_mk _ (v2t ec) [] [flatten_type t]) @@ nil]].
+ [(@ga_mk _ (v2t ec) [] (mapOptionTree (flatten_type ○ unlev) (take_lev (ec :: nil) succ))) @@ nil] |- [t @@ nil]].
intros.
unfold drop_lev.
set (@arrange _ succ (levelMatch (ec::nil))) as q.
right; auto.
Defined.
+ Lemma unlev_relev : forall {Γ}(t:Tree ??(HaskType Γ ★)) lev, mapOptionTree unlev (t @@@ lev) = t.
+ intros.
+ induction t.
+ destruct a; reflexivity.
+ rewrite <- IHt1 at 2.
+ rewrite <- IHt2 at 2.
+ reflexivity.
+ Qed.
+
+ Lemma tree_of_nothing : forall Γ ec t a,
+ Arrange (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))) a.
+ intros.
+ induction t; try destruct o; try destruct a0.
+ simpl.
+ drop_simplify.
+ simpl.
+ apply RCanR.
+ simpl.
+ apply RCanR.
+ Opaque drop_lev.
+ simpl.
+ Transparent drop_lev.
+ drop_simplify.
+ simpl.
+ eapply RComp.
+ eapply RComp.
+ eapply RAssoc.
+ eapply RRight.
+ apply IHt1.
+ apply IHt2.
+ Defined.
+
+ Lemma tree_of_nothing' : forall Γ ec t a,
+ Arrange a (a,,mapOptionTree flatten_leveled_type (drop_lev(Γ:=Γ) (ec :: nil) (t @@@ (ec :: nil)))).
+ intros.
+ induction t; try destruct o; try destruct a0.
+ simpl.
+ drop_simplify.
+ simpl.
+ apply RuCanR.
+ simpl.
+ apply RuCanR.
+ Opaque drop_lev.
+ simpl.
+ Transparent drop_lev.
+ drop_simplify.
+ simpl.
+ eapply RComp.
+ Focus 2.
+ eapply RComp.
+ Focus 2.
+ eapply RCossa.
+ Focus 2.
+ eapply RRight.
+ apply IHt1.
+ apply IHt2.
+ Defined.
+
+ Lemma krunk : forall Γ (ec:HaskTyVar Γ ECKind) t,
+ flatten_type (<[ ec |- t ]>)
+ = @ga_mk Γ (v2t ec)
+ (mapOptionTree flatten_type (take_arg_types_as_tree Γ t))
+ [ flatten_type (drop_arg_types_as_tree t)].
+
+ intros.
+ unfold flatten_type at 1.
+ simpl.
+ unfold ga_mk.
+ unfold v2t.
+ admit. (* BIG HUGE CHEAT FIXME *)
+ Qed.
+
Definition flatten_proof :
forall {h}{c},
- ND Rule h c ->
- ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
+ ND SRule h c ->
+ ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c).
intros.
eapply nd_map'; [ idtac | apply X ].
clear h c X.
intros.
simpl in *.
- refine (match X as R in Rule H C with
+ refine
+ (match X as R in SRule H C with
+ | SBrak Γ Δ t ec succ lev => let case_SBrak := tt in _
+ | SEsc Γ Δ t ec succ lev => let case_SEsc := tt in _
+ | SFlat h c r => let case_SFlat := tt in _
+ end).
+
+ destruct case_SFlat.
+ refine (match r as R in Rule H C with
| RArrange Γ Δ a b x d => let case_RArrange := tt in _
| RNote Γ Δ Σ τ l n => let case_RNote := tt in _
| RLit Γ Δ l _ => let case_RLit := tt in _
apply (flatten_arrangement'' Γ Δ a b x d).
destruct case_RBrak.
- simpl.
- destruct lev.
- change ([flatten_type (<[ ec |- t ]>) @@ nil])
- with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
- refine (ga_unkappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _
- (mapOptionTree (flatten_leveled_type) (drop_lev (ec::nil) succ)) ;; _ ).
- apply arrange_brak.
- apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
+ apply (Prelude_error "found unskolemized Brak rule; this shouldn't happen").
destruct case_REsc.
- simpl.
- destruct lev.
- simpl.
- change ([flatten_leveled_type (<[ ec |- t ]> @@ nil)])
- with ([ga_mk (v2t ec) [] [flatten_type t] @@ nil]).
- eapply nd_comp; [ apply arrange_esc | idtac ].
- set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
- destruct q'.
- destruct s.
- rewrite e.
- clear e.
-
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
- eapply nd_comp; [ apply nd_llecnac | idtac ].
- apply nd_prod; [ idtac | eapply boost ].
- induction x.
- apply ga_id.
- eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
- simpl.
- apply ga_join.
- apply IHx1.
- apply IHx2.
- simpl.
- apply postcompose.
- apply ga_drop.
-
- (* environment has non-empty leaves *)
- apply (ga_kappa Γ Δ (v2t ec) nil (mapOptionTree (flatten_type ○ unlev) (take_lev (ec::nil) succ)) _ _).
- apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
+ apply (Prelude_error "found unskolemized Esc rule; this shouldn't happen").
destruct case_RNote.
simpl.
destruct case_RCast.
simpl.
destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ].
+ simpl.
apply flatten_coercion; auto.
apply (Prelude_error "RCast at level >0; casting inside of code brackets is currently not supported").
destruct case_RCase.
simpl.
apply (Prelude_error "Case not supported (BIG FIXME)").
+
+ destruct case_SBrak.
+ simpl.
+ destruct lev.
+ drop_simplify.
+ set (drop_lev (ec :: nil) (take_arg_types_as_tree Γ t @@@ (ec :: nil))) as empty_tree.
+ take_simplify.
+ rewrite take_lemma'.
+ simpl.
+ rewrite mapOptionTree_compose.
+ rewrite mapOptionTree_compose.
+ rewrite unlev_relev.
+ rewrite <- mapOptionTree_compose.
+ unfold flatten_leveled_type at 4.
+ simpl.
+ rewrite krunk.
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
+ set (mapOptionTree (flatten_type ○ unlev)(take_lev (ec :: nil) succ)) as succ_guest.
+ set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args.
+ unfold empty_tree.
+ eapply nd_comp; [ eapply nd_rule; eapply RArrange; apply tree_of_nothing | idtac ].
+ refine (ga_unkappa' Γ Δ (v2t ec) nil _ _ _ _ ;; _).
+ unfold succ_host.
+ unfold succ_guest.
+ apply arrange_brak.
+ apply (Prelude_error "found Brak at depth >0 indicating 3-level code; only two-level code is currently supported").
+
+ destruct case_SEsc.
+ simpl.
+ destruct lev.
+ simpl.
+ unfold flatten_leveled_type at 2.
+ simpl.
+ rewrite krunk.
+ rewrite mapOptionTree_compose.
+ take_simplify.
+ drop_simplify.
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply tree_of_nothing' ].
+ simpl.
+ rewrite take_lemma'.
+ rewrite unlev_relev.
+ rewrite <- mapOptionTree_compose.
+ eapply nd_comp; [ apply (arrange_esc _ _ ec) | idtac ].
+
+ set (decide_tree_empty (take_lev (ec :: nil) succ)) as q'.
+ destruct q'.
+ destruct s.
+ rewrite e.
+ clear e.
+
+ set (mapOptionTree flatten_leveled_type (drop_lev (ec :: nil) succ)) as succ_host.
+ set (mapOptionTree flatten_type (take_arg_types_as_tree Γ t)) as succ_args.
+
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+ eapply nd_comp; [ apply nd_llecnac | idtac ].
+ apply nd_prod; [ idtac | eapply boost ].
+ induction x.
+ apply ga_id.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanR ].
+ simpl.
+ apply ga_join.
+ apply IHx1.
+ apply IHx2.
+ simpl.
+ apply postcompose.
+
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+ apply ga_cancell.
+ apply firstify.
+
+ induction x.
+ destruct a; simpl.
+ apply ga_id.
+ simpl.
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+ apply ga_cancell.
+ refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ _))).
+ eapply firstify.
+ apply IHx1.
+ apply secondify.
+ apply IHx2.
+
+ (* environment has non-empty leaves *)
+ apply ga_kappa'.
+
+ (* nesting too deep *)
+ apply (Prelude_error "found Esc at depth >0 indicating 3-level code; only two-level code is currently supported").
Defined.
--- /dev/null
+(*********************************************************************************************************************************)
+(* HaskSkolemizer: *)
+(* *)
+(* Skolemizes the portion of a proof which uses judgments at level >0 *)
+(* *)
+(*********************************************************************************************************************************)
+
+Generalizable All Variables.
+Require Import Preamble.
+Require Import General.
+Require Import NaturalDeduction.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+
+Require Import HaskKinds.
+Require Import HaskCoreTypes.
+Require Import HaskCoreVars.
+Require Import HaskWeakTypes.
+Require Import HaskWeakVars.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
+Require Import HaskStrongTypes.
+Require Import HaskProof.
+Require Import NaturalDeduction.
+
+Require Import HaskStrongTypes.
+Require Import HaskStrong.
+Require Import HaskProof.
+Require Import HaskStrongToProof.
+Require Import HaskProofToStrong.
+Require Import HaskWeakToStrong.
+
+Open Scope nd_scope.
+Set Printing Width 130.
+
+Section HaskSkolemizer.
+
+(*
+ Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
+ match exp with
+ | TVar _ x => x
+ | TAll _ y => TAll _ (fun v => debruijn2phoas (y (TVar v)))
+ | TApp _ _ x y => TApp (debruijn2phoas x) (debruijn2phoas y)
+ | TCon tc => TCon tc
+ | TCoerc _ t1 t2 t => TCoerc (debruijn2phoas t1) (debruijn2phoas t2) (debruijn2phoas t)
+ | TArrow => TArrow
+ | TCode v e => TCode (debruijn2phoas v) (debruijn2phoas e)
+ | TyFunApp tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
+ end
+ with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
+ match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
+ | TyFunApp_nil => TyFunApp_nil
+ | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas t) (debruijn2phoasyFunApp _ rest)
+ end.
+*)
+ Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
+ match r with
+ | RBrak _ _ _ _ _ _ => False
+ | REsc _ _ _ _ _ _ => False
+ | _ => True
+ end.
+
+ Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
+ match lt with
+ | nil => t
+ | a::b => mkArrows b (a ---> t)
+ end.
+
+ Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
+ match l with
+ | nil => t
+ | a::b => unleaves_ (t,,[a @@ lev]) b lev
+ end.
+
+ (* rules of skolemized proofs *)
+ Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ => Γ end.
+ Definition getSuc (j:Judg) : Tree ??(LeveledHaskType (getΓ j) ★) :=
+ match j as J return Tree ??(LeveledHaskType (getΓ J) ★) with Γ > _ > _ |- s => s end.
+ Fixpoint getjlev {Γ}(tt:Tree ??(LeveledHaskType Γ ★)) : HaskLevel Γ :=
+ match tt with
+ | T_Leaf None => nil
+ | T_Leaf (Some (_ @@ lev)) => lev
+ | T_Branch b1 b2 =>
+ match getjlev b1 with
+ | nil => getjlev b2
+ | lev => lev
+ end
+ end.
+
+ Definition ite_unit : ∀ Γ, InstantiatedTypeEnv (fun _ => unit) Γ.
+ intros.
+ induction Γ.
+ apply INil.
+ apply ICons; auto.
+ apply tt.
+ Defined.
+
+ Fixpoint grab (n:nat) {T} (l:list T) : T :=
+ match l with
+ | nil => Prelude_error "grab failed"
+ | h::t => match n with
+ | 0 => h
+ | S n' => grab n' t
+ end
+ end.
+
+ Fixpoint count' (n:nat)(ln:list nat) : list nat :=
+ match n with
+ | 0 => ln
+ | S n' => count' n' (n'::ln)
+ end.
+
+ Definition count (n:nat) := count' n nil.
+
+ Definition rebundle {Γ}(X:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★)) : list (HaskType Γ ★ ) :=
+ map (fun n => fun TV ite => grab n (X TV ite)) (count (length (X _ (ite_unit _)))).
+
+ Definition take_arg_types_as_tree Γ (ht:HaskType Γ ★) :=
+ (unleaves' (rebundle (fun TV ite => (take_arg_types (ht TV ite))))).
+
+ Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
+ fun TV ite => drop_arg_types (ht TV ite).
+
+ Implicit Arguments take_arg_types_as_tree [[Γ]].
+ Implicit Arguments drop_arg_types_as_tree [[Γ]].
+
+ Lemma take_works : forall {Γ}(t1 t2:HaskType Γ ★),
+ take_arg_types_as_tree (t1 ---> t2) = [t1],,(take_arg_types_as_tree t2).
+ intros.
+ unfold take_arg_types_as_tree; simpl.
+ unfold rebundle at 1.
+ admit.
+ Qed.
+
+ Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
+ drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
+ intros.
+ unfold drop_arg_types_as_tree.
+ simpl.
+ reflexivity.
+ Qed.
+
+ Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
+(* | SFlat : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
+ | SFlat : forall h c, Rule h c -> SRule h c
+ | SBrak : forall Γ Δ t ec Σ l,
+ SRule
+ [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
+ [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
+
+ | SEsc : forall Γ Δ t ec Σ l,
+ SRule
+ [Γ > Δ > Σ |- [<[ec |- t]> @@ l ]]
+ [Γ > Δ > Σ,, (take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t @@ (ec::l) ]]
+ .
+
+ Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
+ match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
+
+ Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
+ match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
+
+ Definition skolemize_judgment (j:Judg) : Judg :=
+ match j with
+ Γ > Δ > Σ₁ |- Σ₂ =>
+ match getjlev Σ₂ with
+ | nil => j
+ | lev => Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree' Σ₂) |- mapOptionTree drop_arg_types_as_tree' Σ₂
+ end
+ end.
+
+ Definition check_hof : forall {Γ}(t:HaskType Γ ★),
+ sumbool
+ True
+ (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
+ intros.
+ destruct (eqd_dec (take_arg_types_as_tree t) []);
+ destruct (eqd_dec (drop_arg_types_as_tree t) t).
+ right; auto.
+ left; auto.
+ left; auto.
+ left; auto.
+ Defined.
+
+ Definition skolemize_proof :
+ forall {h}{c},
+ ND Rule h c ->
+ ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
+ intros.
+ eapply nd_map'; [ idtac | apply X ].
+ clear h c X.
+ intros.
+
+ refine (match X as R in Rule H C with
+ | RArrange Γ Δ a b x d => let case_RArrange := tt in _
+ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
+ | RLit Γ Δ l _ => let case_RLit := tt in _
+ | RVar Γ Δ σ lev => let case_RVar := tt in _
+ | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
+ | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
+ | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
+ | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
+ | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
+ | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
+ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
+ | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
+ | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
+ | RJoin Γ p lri m x q => let case_RJoin := tt in _
+ | RVoid _ _ => let case_RVoid := tt in _
+ | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
+ | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
+ | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
+ | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
+ end); clear X h c.
+
+ destruct case_RArrange.
+ simpl.
+ destruct (getjlev x).
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply d.
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply RRight.
+ apply d.
+
+ destruct case_RBrak.
+ simpl.
+ destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
+ apply nd_rule.
+ apply SBrak.
+
+ destruct case_REsc.
+ simpl.
+ destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
+ apply nd_rule.
+ apply SEsc.
+
+ destruct case_RNote.
+ apply nd_rule.
+ apply SFlat.
+ simpl.
+ destruct l.
+ apply RNote.
+ apply n.
+ apply RNote.
+ apply n.
+
+ destruct case_RLit.
+ simpl.
+ destruct l0.
+ apply nd_rule.
+ apply SFlat.
+ apply RLit.
+ set (check_hof (@literalType l Γ)) as hof.
+ destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
+ destruct a.
+ rewrite H.
+ rewrite H0.
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply RuCanL ].
+ apply nd_rule.
+ apply SFlat.
+ apply RLit.
+
+ destruct case_RVar.
+ simpl.
+ destruct lev.
+ apply nd_rule; apply SFlat; apply RVar.
+ set (check_hof σ) as hof.
+ destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
+ destruct a.
+ rewrite H.
+ rewrite H0.
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+ apply nd_rule.
+ apply SFlat.
+ apply RVar.
+
+ destruct case_RGlobal.
+ simpl.
+ destruct σ.
+ apply nd_rule; apply SFlat; apply RGlobal.
+ set (check_hof (l wev)) as hof.
+ destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
+ destruct a.
+ rewrite H.
+ rewrite H0.
+ simpl.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RuCanR ].
+ apply nd_rule.
+ apply SFlat.
+ apply RGlobal.
+
+ destruct case_RLam.
+ simpl.
+ destruct lev.
+ apply nd_rule.
+ apply SFlat.
+ apply RLam.
+ rewrite take_works.
+ rewrite drop_works.
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply RCossa.
+
+ destruct case_RCast.
+ simpl.
+ destruct lev.
+ apply nd_rule.
+ apply SFlat.
+ apply RCast.
+ apply γ.
+ apply (Prelude_error "found RCast at level >0").
+
+ destruct case_RJoin.
+ simpl.
+ destruct (getjlev x).
+ destruct (getjlev q).
+ apply nd_rule.
+ apply SFlat.
+ apply RJoin.
+ apply (Prelude_error "found RJoin at level >0").
+ apply (Prelude_error "found RJoin at level >0").
+
+ destruct case_RApp.
+ simpl.
+ destruct lev.
+ apply nd_rule.
+ apply SFlat.
+ apply RApp.
+ rewrite take_works.
+ rewrite drop_works.
+ set (check_hof tx) as hof_tx.
+ destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
+ destruct a.
+ rewrite H.
+ rewrite H0.
+ simpl.
+ set (@RLet Γ Δ (Σ₂,,take_arg_types_as_tree te @@@ (h :: lev)) Σ₁ (drop_arg_types_as_tree te) tx (h::lev)) as q.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
+ clear q.
+ apply nd_prod.
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply RCanR.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+ apply nd_rule; apply SFlat; apply RArrange; apply RLeft; eapply RExch.
+
+ destruct case_RLet.
+ simpl.
+ destruct lev.
+ apply nd_rule.
+ apply SFlat.
+ apply RLet.
+ set (check_hof σ₂) as hof_tx.
+ destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
+ destruct a.
+ rewrite H.
+ rewrite H0.
+ set (@RLet Γ Δ (Σ₁,,(take_arg_types_as_tree σ₁ @@@ (h::lev))) Σ₂ (drop_arg_types_as_tree σ₁) σ₂ (h::lev)) as q.
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; eapply RLeft; apply RExch ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply q ].
+ clear q.
+ apply nd_prod.
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply RCanR.
+ eapply nd_comp; [ eapply nd_rule; apply SFlat; eapply RArrange; apply RCossa | idtac ].
+ eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply RAssoc ].
+ apply nd_rule.
+ apply SFlat.
+ apply RArrange.
+ apply RLeft.
+ eapply RExch.
+
+ destruct case_RVoid.
+ simpl.
+ apply nd_rule.
+ apply SFlat.
+ apply RVoid.
+
+ destruct case_RAppT.
+ simpl.
+ destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
+ apply (Prelude_error "RAppT at depth>0").
+
+ destruct case_RAbsT.
+ simpl.
+ destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
+ apply (Prelude_error "RAbsT at depth>0").
+
+ destruct case_RAppCo.
+ simpl.
+ destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
+ apply γ.
+ apply (Prelude_error "RAppCo at depth>0").
+
+ destruct case_RAbsCo.
+ simpl.
+ destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
+ apply (Prelude_error "RAbsCo at depth>0").
+
+ destruct case_RLetRec.
+ simpl.
+ destruct t.
+ destruct (getjlev (y @@@ nil)).
+ apply nd_rule.
+ apply SFlat.
+ apply (@RLetRec Γ Δ lri x y nil).
+ apply (Prelude_error "RLetRec at depth>0").
+ apply (Prelude_error "RLetRec at depth>0").
+
+ destruct case_RCase.
+ simpl.
+ apply (Prelude_error "CASE: BIG FIXME").
+ Defined.
+
+End HaskSkolemizer.
projects / coq-hetmet.git / commitdiff