From: Adam Megacz Date: Fri, 13 May 2011 07:36:09 +0000 (-0700) Subject: first draft of skolemization pass X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=4a32fb619ddda1fedb0855a0c7acad0a41704da8 first draft of skolemization pass --- diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index cd5bd57..46e6af5 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -30,6 +30,8 @@ Require Import HaskStrongToProof. Require Import HaskProofToStrong. Require Import HaskWeakToStrong. +Require Import HaskSkolemizer. + Open Scope nd_scope. Set Printing Width 130. @@ -165,10 +167,39 @@ Section HaskFlattener. 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)] ] => @@ -181,6 +212,8 @@ Section HaskFlattener. 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)] ] => @@ -226,7 +259,8 @@ Section HaskFlattener. | 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 := @@ -240,12 +274,12 @@ Section HaskFlattener. 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 *) @@ -428,15 +462,15 @@ Section HaskFlattener. 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. @@ -457,6 +491,31 @@ Section HaskFlattener. 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). @@ -607,10 +666,8 @@ Section HaskFlattener. 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. @@ -648,6 +705,9 @@ Section HaskFlattener. unfold flatten_leveled_type. simpl. unfold flatten_type. + simpl. + unfold ga_mk. + simpl. apply RVar. simpl. apply ga_id. @@ -661,11 +721,9 @@ Section HaskFlattener. 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. @@ -736,17 +794,97 @@ Section HaskFlattener. 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 _ @@ -772,46 +910,10 @@ Section HaskFlattener. 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. @@ -889,6 +991,7 @@ Section HaskFlattener. 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"). @@ -1028,6 +1131,95 @@ Section HaskFlattener. 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. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v new file mode 100644 index 0000000..c1b5708 --- /dev/null +++ b/src/HaskSkolemizer.v @@ -0,0 +1,429 @@ +(*********************************************************************************************************************************) +(* 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.