From: Adam Megacz Date: Mon, 9 May 2011 04:21:59 +0000 (-0700) Subject: major improvements to flattener; almost finished now X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=cb424978e057bc2b4868517302738d52246fba04 major improvements to flattener; almost finished now --- diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 9f094bb..58bc13e 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -219,7 +219,7 @@ Section core2proof. exact O. apply t. Defined. - +(* Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := addErrorMessage ("input CoreSyn: " +++ toString ce) (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( @@ -255,9 +255,10 @@ Section core2proof. | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e) | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe) end. - + Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := map coreToCoreBind lbinds. + *) End CoreToCore. @@ -267,16 +268,258 @@ Section core2proof. | _ => Prelude_error "IMPOSSIBLE" end. - Definition coqPassCoreToCore + Definition curry {Γ}{Δ}{a}{s}{Σ}{lev} : + ND Rule + [ Γ > Δ > Σ |- [a ---> s @@ lev ] ] + [ Γ > Δ > Σ,,[a @@ lev] |- [ s @@ lev ] ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_id. + apply nd_rule. + apply RVar. + Defined. + + Definition fToC1 {Γ}{Δ}{a}{s}{lev} : + ND Rule [] [ Γ > Δ > [ ] |- [a ---> s @@ lev ] ] -> + ND Rule [] [ Γ > Δ > [a @@ lev] |- [ s @@ lev ] ]. + intro pf. + eapply nd_comp. + apply pf. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + apply curry. + Defined. + + Definition fToC2 {Γ}{Δ}{a1}{a2}{s}{lev} : + ND Rule [] [ Γ > Δ > [] |- [a1 ---> (a2 ---> s) @@ lev ] ] -> + ND Rule [] [ Γ > Δ > [a1 @@ lev],,[a2 @@ lev] |- [ s @@ lev ] ]. + intro pf. + eapply nd_comp. + eapply pf. + clear pf. + eapply nd_comp. + eapply curry. + eapply nd_comp. + eapply nd_rule. + eapply RArrange. + eapply RCanL. + apply curry. + Defined. + + Section coqPassCoreToCore. + Context + (hetmet_brak : CoreVar) + (hetmet_esc : CoreVar) + (uniqueSupply : UniqSupply) + (lbinds:list (@CoreBind CoreVar)) + (hetmet_PGArrowTyCon : TyFun) + (hetmet_pga_id : CoreVar) + (hetmet_pga_comp : CoreVar) + (hetmet_pga_first : CoreVar) + (hetmet_pga_second : CoreVar) + (hetmet_pga_cancell : CoreVar) + (hetmet_pga_cancelr : CoreVar) + (hetmet_pga_uncancell : CoreVar) + (hetmet_pga_uncancelr : CoreVar) + (hetmet_pga_assoc : CoreVar) + (hetmet_pga_unassoc : CoreVar) + (hetmet_pga_copy : CoreVar) + (hetmet_pga_drop : CoreVar) + (hetmet_pga_swap : CoreVar) + (hetmet_pga_applyl : CoreVar) + (hetmet_pga_applyr : CoreVar) + (hetmet_pga_curryl : CoreVar) + (hetmet_pga_curryr : CoreVar) + . + + Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil ★ TyFunApp_nil. + Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★ := + TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b. + Definition ga_type {TV}(a b c:RawHaskType TV ★) : RawHaskType TV ★ := + TApp (TApp (TApp (@TyFunApp TV + hetmet_PGArrowTyCon + nil _ TyFunApp_nil) a) b) c. + Definition ga := @ga_mk ga_unit ga_prod (@ga_type). + + Definition ga_type' {Γ}(a b c:HaskType Γ ★) : HaskType Γ ★ := + fun TV ite => TApp (TApp (TApp (@TyFunApp TV + hetmet_PGArrowTyCon + nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite). + + Definition mkGlob2' {Γ}{κ₁}{κ₂}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) : + IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::nil) -> HaskType Γ ★. + intros. + inversion X; subst. + inversion X1; subst. + apply f; auto. + Defined. + + Definition mkGlob2 {Γ}{Δ}{l}{κ₁}{κ₂}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ ★) x y + : ND Rule [] [ Γ > Δ > [] |- [f x y @@ l] ]. + apply nd_rule. + refine (@RGlobal Γ Δ l + {| glob_wv := coreVarToWeakExprVarOrError cv + ; glob_kinds := κ₁ :: κ₂ :: nil + ; glob_tf := mkGlob2'(Γ:=Γ) f + |} (ICons _ _ x (ICons _ _ y INil))). + Defined. + + Definition mkGlob3' {Γ}{κ₁}{κ₂}{κ₃}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) : + IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::nil) -> HaskType Γ ★. + intros. + inversion X; subst. + inversion X1; subst. + inversion X3; subst. + apply f; auto. + Defined. + + Definition mkGlob3 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ ★) x y z + : ND Rule [] [ Γ > Δ > [] |- [f x y z @@ l] ]. + apply nd_rule. + refine (@RGlobal Γ Δ l + {| glob_wv := coreVarToWeakExprVarOrError cv + ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: nil + ; glob_tf := mkGlob3'(Γ:=Γ) f + |} (ICons _ _ x (ICons _ _ y (ICons _ _ z INil)))). + Defined. + + Definition mkGlob4' {Γ}{κ₁}{κ₂}{κ₃}{κ₄}(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) : + IList Kind (fun κ : Kind => HaskType Γ κ) (κ₁::κ₂::κ₃::κ₄::nil) -> HaskType Γ ★. + intros. + inversion X; subst. + inversion X1; subst. + inversion X3; subst. + inversion X5; subst. + apply f; auto. + Defined. + + Definition mkGlob4 {Γ}{Δ}{l}{κ₁}{κ₂}{κ₃}{κ₄}(cv:CoreVar)(f:HaskType Γ κ₁ -> HaskType Γ κ₂ -> HaskType Γ κ₃ -> HaskType Γ κ₄ -> HaskType Γ ★) x y z q + : ND Rule [] [ Γ > Δ > [] |- [f x y z q @@ l] ]. + apply nd_rule. + refine (@RGlobal Γ Δ l + {| glob_wv := coreVarToWeakExprVarOrError cv + ; glob_kinds := κ₁ :: κ₂ :: κ₃ :: κ₄ :: nil + ; glob_tf := mkGlob4'(Γ:=Γ) f + |} (ICons _ _ x (ICons _ _ y (ICons _ _ z (ICons _ _ q INil))))). + Defined. + + Definition gat {Γ}(x:Tree ??(HaskType Γ ★)) := @ga_mk_tree ga_unit ga_prod _ x. + + Instance my_ga : garrow ga_unit ga_prod (@ga_type) := + { ga_id := fun Γ Δ ec l a => mkGlob2 hetmet_pga_id (fun ec a => ga_type' ec a a) ec (gat a) + ; ga_cancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancelr (fun ec a => ga_type' ec _ a) ec (gat a) + ; ga_cancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_cancell (fun ec a => ga_type' ec _ a) ec (gat a) + ; ga_uncancelr := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancelr (fun ec a => ga_type' ec a _) ec (gat a) + ; ga_uncancell := fun Γ Δ ec l a => mkGlob2 hetmet_pga_uncancell (fun ec a => ga_type' ec a _) ec (gat a) + ; ga_assoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_assoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c) + ; ga_unassoc := fun Γ Δ ec l a b c => mkGlob4 hetmet_pga_unassoc (fun ec a b c => ga_type' ec _ _) ec (gat a) (gat b) (gat c) + ; ga_swap := fun Γ Δ ec l a b => mkGlob3 hetmet_pga_swap (fun ec a b => ga_type' ec _ _) ec (gat a) (gat b) + ; ga_drop := fun Γ Δ ec l a => mkGlob2 hetmet_pga_drop (fun ec a => ga_type' ec _ _) ec (gat a) + ; ga_copy := fun Γ Δ ec l a => mkGlob2 hetmet_pga_copy (fun ec a => ga_type' ec _ _) ec (gat a) + ; ga_first := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_first (fun ec a b c => _) ec (gat a) (gat b) (gat x)) + ; ga_second := fun Γ Δ ec l a b x => fToC1 (mkGlob4 hetmet_pga_second (fun ec a b c => _) ec (gat a) (gat b) (gat x)) + ; ga_comp := fun Γ Δ ec l a b c => fToC2 (mkGlob4 hetmet_pga_comp (fun ec a b c => _) ec (gat a) (gat b) (gat c)) +(* ; ga_lit := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_lit))*) +(* ; ga_curry := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_curry))*) +(* ; ga_apply := fun Γ Δ ec l a => nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_apply))*) +(* ; ga_kappa := fun Γ Δ ec l a => fToC1 (nd_rule (RGlobal _ _ _ _ (coreVarToWeakExprVarOrError hetmet_pga_kappa)))*) + ; ga_lit := fun Γ Δ ec l a => Prelude_error "ga_lit" + ; ga_curry := fun Γ Δ ec l a b c => Prelude_error "ga_curry" + ; ga_apply := fun Γ Δ ec l a b c => Prelude_error "ga_apply" + ; ga_kappa := fun Γ Δ ec l a => Prelude_error "ga_kappa" + }. + + Definition hetmet_brak' := coreVarToWeakExprVarOrError hetmet_brak. + Definition hetmet_esc' := coreVarToWeakExprVarOrError hetmet_esc. + + Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := + addErrorMessage ("input CoreSyn: " +++ toString ce) + (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( + coreExprToWeakExpr ce >>= fun we => + addErrorMessage ("WeakExpr: " +++ toString we) + ((addErrorMessage ("CoreType of WeakExpr: " +++ toString (coreTypeOfCoreExpr (weakExprToCoreExpr we))) + ((weakTypeOfWeakExpr we) >>= fun t => + (addErrorMessage ("WeakType: " +++ toString t) + ((weakTypeToTypeOfKind φ t ★) >>= fun τ => + + ((weakExprToStrongExpr Γ Δ φ ψ ξ (fun _ => true) τ nil we) >>= fun e => + + (addErrorMessage ("HaskStrong...") + (let haskProof := flatten_proof my_ga (@expr2proof _ _ _ _ _ _ e) + in (* insert HaskProof-to-HaskProof manipulations here *) + OK ((@proof2expr nat _ FreshNat _ _ _ _ (fun _ => Prelude_error "unbound unique") _ haskProof) O) + >>= fun e' => + (snd e') >>= fun e'' => + strongExprToWeakExpr hetmet_brak' hetmet_esc' mkWeakTypeVar mkWeakCoerVar mkWeakExprVar uniqueSupply + (projT2 e'') INil + >>= fun q => + OK (weakExprToCoreExpr q) + )))))))))). + + Definition coreToCoreExpr (ce:@CoreExpr CoreVar) : (@CoreExpr CoreVar) := + match coreToCoreExpr' ce with + | OK x => x + | Error s => Prelude_error s + end. + + Definition coreToCoreBind (binds:@CoreBind CoreVar) : @CoreBind CoreVar := + match binds with + | CoreNonRec v e => CoreNonRec v (coreToCoreExpr e) + | CoreRec lbe => CoreRec (map (fun ve => match ve with (v,e) => (v,coreToCoreExpr e) end) lbe) + end. + + Definition coqPassCoreToCore' (lbinds:list (@CoreBind CoreVar)) : list (@CoreBind CoreVar) := + map coreToCoreBind lbinds. + + End coqPassCoreToCore. + + Definition coqPassCoreToCore (hetmet_brak : CoreVar) (hetmet_esc : CoreVar) (uniqueSupply : UniqSupply) - (lbinds:list (@CoreBind CoreVar) - ) : list (@CoreBind CoreVar) := + (lbinds:list (@CoreBind CoreVar)) + (hetmet_PGArrowTyCon : TyFun) + (hetmet_pga_id : CoreVar) + (hetmet_pga_comp : CoreVar) + (hetmet_pga_first : CoreVar) + (hetmet_pga_second : CoreVar) + (hetmet_pga_cancell : CoreVar) + (hetmet_pga_cancelr : CoreVar) + (hetmet_pga_uncancell : CoreVar) + (hetmet_pga_uncancelr : CoreVar) + (hetmet_pga_assoc : CoreVar) + (hetmet_pga_unassoc : CoreVar) + (hetmet_pga_copy : CoreVar) + (hetmet_pga_drop : CoreVar) + (hetmet_pga_swap : CoreVar) + (hetmet_pga_applyl : CoreVar) + (hetmet_pga_applyr : CoreVar) + (hetmet_pga_curryl : CoreVar) + (hetmet_pga_curryr : CoreVar) : list (@CoreBind CoreVar) := coqPassCoreToCore' - (coreVarToWeakExprVarOrError hetmet_brak) - (coreVarToWeakExprVarOrError hetmet_esc) - uniqueSupply - lbinds. + hetmet_brak + hetmet_esc + uniqueSupply + hetmet_PGArrowTyCon + hetmet_pga_id + hetmet_pga_comp + hetmet_pga_first + hetmet_pga_second + hetmet_pga_cancell + hetmet_pga_cancelr + hetmet_pga_uncancell + hetmet_pga_uncancelr + hetmet_pga_assoc + hetmet_pga_unassoc + hetmet_pga_copy + hetmet_pga_drop + hetmet_pga_swap + lbinds + (* + hetmet_pga_applyl + hetmet_pga_applyr + hetmet_pga_curryl + *) + . End core2proof. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index b55dcf5..6d9d7a6 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -18,31 +18,12 @@ Require Import HaskLiteralsAndTyCons. Require Import HaskStrongTypes. Require Import HaskProof. Require Import NaturalDeduction. -Require Import NaturalDeductionCategory. - -Require Import Algebras_ch4. -Require Import Categories_ch1_3. -Require Import Functors_ch1_4. -Require Import Isomorphisms_ch1_5. -Require Import ProductCategories_ch1_6_1. -Require Import OppositeCategories_ch1_6_2. -Require Import Enrichment_ch2_8. -Require Import Subcategories_ch7_1. -Require Import NaturalTransformations_ch7_4. -Require Import NaturalIsomorphisms_ch7_5. -Require Import BinoidalCategories. -Require Import PreMonoidalCategories. -Require Import MonoidalCategories_ch7_8. -Require Import Coherence_ch7_8. Require Import HaskStrongTypes. Require Import HaskStrong. Require Import HaskProof. Require Import HaskStrongToProof. Require Import HaskProofToStrong. -Require Import ProgrammingLanguage. -Require Import HaskProgrammingLanguage. -Require Import PCF. Open Scope nd_scope. @@ -56,10 +37,137 @@ Open Scope nd_scope. *) Section HaskFlattener. - (* this actually has nothing to do with categories; it shows that proofs [|-A]//[|-B] are one-to-one with []//[A|-B] *) - (* TODO Lemma hom_functor_full*) + Inductive TreeFlags {T:Type} : Tree T -> Type := + | tf_leaf_true : forall x, TreeFlags (T_Leaf x) + | tf_leaf_false : forall x, TreeFlags (T_Leaf x) + | tf_branch : forall b1 b2, TreeFlags b1 -> TreeFlags b2 -> TreeFlags (b1,,b2). - (* lemma: if a proof from no hypotheses contains no Brak's or Esc's, then the context contains no variables at level!=0 *) + Fixpoint mkFlags {T}(f:T -> bool)(t:Tree T) : TreeFlags t := + match t as T return TreeFlags T with + | T_Leaf x => if f x then tf_leaf_true x else tf_leaf_false x + | T_Branch b1 b2 => tf_branch _ _ (mkFlags f b1) (mkFlags f b2) + end. + + (* take and drop are not exact inverses *) + + (* drop replaces each leaf where the flag is set with a [] *) + Fixpoint drop {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T := + match tf with + | tf_leaf_true x => [] + | tf_leaf_false x => Σ + | tf_branch b1 b2 tb1 tb2 => (drop tb1),,(drop tb2) + end. + + (* take returns only those leaves for which the flag is set; all others are omitted entirely from the tree *) + Fixpoint take {T}{Σ:Tree T}(tf:TreeFlags Σ) : ??(Tree T) := + match tf with + | tf_leaf_true x => Some Σ + | tf_leaf_false x => None + | tf_branch b1 b2 tb1 tb2 => + match take tb1 with + | None => take tb2 + | Some b1' => match take tb2 with + | None => Some b1' + | Some b2' => Some (b1',,b2') + end + end + end. + + Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T := + match t with + | None => [] + | Some x => x + end. + + Definition setNone {T}(b:bool)(f:T -> bool) : ??T -> bool := + fun t => + match t with + | None => b + | Some x => f x + end. + + (* "Arrange" objects are parametric in the type of the leaves of the tree *) + Definition arrangeMap : + forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R), + Arrange Σ₁ Σ₂ -> + Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂). + intros. + induction X; simpl. + apply RCanL. + apply RCanR. + apply RuCanL. + apply RuCanR. + apply RAssoc. + apply RCossa. + apply RExch. + apply RWeak. + apply RCont. + apply RLeft; auto. + apply RRight; auto. + eapply RComp; [ apply IHX1 | apply IHX2 ]. + Defined. + + Definition bnot (b:bool) : bool := if b then false else true. + + Definition swapMiddle {T} (a b c d:Tree ??T) : + Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)). + eapply RComp. + apply RCossa. + eapply RComp. + eapply RLeft. + eapply RComp. + eapply RAssoc. + eapply RRight. + apply RExch. + eapply RComp. + eapply RLeft. + eapply RCossa. + eapply RAssoc. + Defined. + + Definition arrange : + forall {T} (Σ:Tree ??T) (f:T -> bool), + Arrange Σ (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))). + intros. + induction Σ. + simpl. + destruct a. + simpl. + destruct (f t); simpl. + apply RuCanL. + apply RuCanR. + simpl. + apply RuCanL. + simpl in *. + eapply RComp; [ idtac | apply swapMiddle ]. + eapply RComp. + eapply RLeft. + apply IHΣ2. + eapply RRight. + apply IHΣ1. + Defined. + + Definition arrange' : + forall {T} (Σ:Tree ??T) (f:T -> bool), + Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ. + intros. + induction Σ. + simpl. + destruct a. + simpl. + destruct (f t); simpl. + apply RCanL. + apply RCanR. + simpl. + apply RCanL. + simpl in *. + eapply RComp; [ apply swapMiddle | idtac ]. + eapply RComp. + eapply RLeft. + apply IHΣ2. + eapply RRight. + apply IHΣ1. + Defined. Definition minus' n m := match m with @@ -77,44 +185,146 @@ Section HaskFlattener. [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ] end. - (* The opposite: replace any type which is NOT at level "lev" with None *) - Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) := - mapTree (fun t => match t with - | Some (ttype @@ tlev) => if eqd_dec tlev lev then Some ttype else None - | _ => None - end) tt. + Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T := + match tt with + | T_Leaf None => unit + | T_Leaf (Some x) => x + | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2) + end. + + Set Printing Width 130. + + Context {unitTy : forall TV, RawHaskType TV ★ }. + Context {prodTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. + Context {gaTy : forall TV, RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ -> RawHaskType TV ★ }. + + Definition ga_mk_tree {Γ} (tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := + fun TV ite => reduceTree (unitTy TV) (prodTy TV) (mapOptionTree (fun x => x TV ite) tr). + + Definition ga_mk {Γ}(ec:HaskType Γ ★ )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := + fun TV ite => gaTy TV (ec TV ite) (ga_mk_tree ant TV ite) (ga_mk_tree suc TV ite). + + Class garrow := + { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a a @@ l] ] + ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,[]) a @@ l] ] + ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ([],,a) a @@ l] ] + ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,[]) @@ l] ] + ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a ([],,a) @@ l] ] + ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ] + ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ] + ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec (a,,b) (b,,a) @@ l] ] + ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a [] @@ l] ] + ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec a (a,,a) @@ l] ] + ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (a,,x) (b,,x) @@ l] ] + ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l] |- [@ga_mk Γ ec (x,,a) (x,,b) @@ l] ] + ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga_mk Γ ec [] [literalType lit] @@ l] ] + ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec (a,,[b]) [c] @@ l] |- [@ga_mk Γ ec a [b ---> c] @@ l] ] + ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga_mk Γ ec a b @@ l],,[@ga_mk Γ ec b c @@ l] |- [@ga_mk Γ ec a c @@ l] ] + ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule [] + [Γ > Δ > [@ga_mk Γ ec a [b ---> c] @@ l],,[@ga_mk Γ ec a' [b] @@ l] |- [@ga_mk Γ ec (a,,a') [c] @@ l] ] + ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ] + [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] + }. + Context `(gar:garrow). + + Notation "a ~~~~> b" := (@ga_mk _ _ a b) (at level 20). + + (* + * The story: + * - code types <[t]>@c become garrows c () t + * - free variables of type t at a level lev deeper than the succedent become garrows c () t + * - free variables at the level of the succedent become + *) + Fixpoint garrowfy_raw_codetypes {TV}{κ}(exp: RawHaskType TV κ) : RawHaskType TV κ := + match exp with + | TVar _ x => TVar x + | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes (y v)) + | TApp _ _ x y => TApp (garrowfy_raw_codetypes x) (garrowfy_raw_codetypes y) + | TCon tc => TCon tc + | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes t1) (garrowfy_raw_codetypes t2) + (garrowfy_raw_codetypes t) + | TArrow => TArrow + | TCode v e => gaTy TV v (unitTy TV) (garrowfy_raw_codetypes e) + | TyFunApp tfc kl k lt => TyFunApp tfc kl k (garrowfy_raw_codetypes_list _ lt) + end + with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk := + match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with + | TyFunApp_nil => TyFunApp_nil + | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes t) (garrowfy_raw_codetypes_list _ rest) + end. + Definition garrowfy_code_types {Γ}{κ}(ht:HaskType Γ κ) : HaskType Γ κ := + fun TV ite => + garrowfy_raw_codetypes (ht TV ite). + + Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite). + + Fixpoint garrowfy_leveled_code_types' {Γ}(ht:HaskType Γ ★)(lev:HaskLevel Γ) : HaskType Γ ★ := + match lev with + | nil => garrowfy_code_types ht + | ec::lev' => @ga_mk _ (v2t ec) [] [garrowfy_leveled_code_types' ht lev'] + end. + + Definition garrowfy_leveled_code_types {Γ}(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ := + match ht with + htt @@ lev => + garrowfy_leveled_code_types' htt lev @@ nil + end. + + Definition levelMatch {Γ}(lev:HaskLevel Γ) : LeveledHaskType Γ ★ -> bool := + fun t => match t with ttype@@tlev => if eqd_dec tlev lev then true else false end. (* In a tree of types, replace any type at depth "lev" or greater None *) - Definition drop_depth {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) := - mapTree (fun t => match t with - | Some (ttype @@ tlev) => if eqd_dec tlev lev then None else t - | _ => t - end) tt. + Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt := + mkFlags (setNone false (levelMatch lev)) tt. - Lemma drop_depth_lemma : forall Γ (lev:HaskLevel Γ) x, drop_depth lev [x @@ lev] = []. + Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) := + drop (mkDropFlags lev tt). + + (* The opposite: replace any type which is NOT at level "lev" with None *) + Definition mkTakeFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt := + mkFlags (setNone true (bnot ○ levelMatch lev)) tt. + + Definition take_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(HaskType Γ ★) := + mapOptionTree (fun x => garrowfy_code_types (unlev x)) (drop (mkTakeFlags lev tt)). +(* + mapOptionTree (fun x => garrowfy_code_types (unlev x)) + (maybeTree (take tt (mkFlags ( + fun t => match t with + | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false + | _ => true + end + ) tt))). +*) + + Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = []. intros; simpl. Opaque eqd_dec. - unfold drop_depth. + unfold drop_lev. + simpl. + unfold mkDropFlags. simpl. Transparent eqd_dec. eqd_dec_refl'. auto. Qed. - Lemma drop_depth_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_depth (ec::lev) [x @@ (ec :: lev)] = []. + Lemma drop_lev_lemma_s : forall Γ (lev:HaskLevel Γ) ec x, drop_lev (ec::lev) [x @@ (ec :: lev)] = []. intros; simpl. Opaque eqd_dec. - unfold drop_depth. + unfold drop_lev. + unfold mkDropFlags. simpl. Transparent eqd_dec. eqd_dec_refl'. auto. Qed. - Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [x]. + Lemma take_lemma : forall Γ (lev:HaskLevel Γ) x, take_lev lev [x @@ lev] = [garrowfy_code_types x]. intros; simpl. Opaque eqd_dec. unfold take_lev. + unfold mkTakeFlags. simpl. Transparent eqd_dec. eqd_dec_refl'. @@ -123,14 +333,14 @@ Section HaskFlattener. Ltac drop_simplify := match goal with - | [ |- context[@drop_depth ?G ?L [ ?X @@ ?L ] ] ] => - rewrite (drop_depth_lemma G L X) - | [ |- context[@drop_depth ?G (?E :: ?L) [ ?X @@ (?E :: ?L) ] ] ] => - rewrite (drop_depth_lemma_s G L E X) - | [ |- context[@drop_depth ?G ?N (?A,,?B)] ] => - change (@drop_depth G N (A,,B)) with ((@drop_depth G N A),,(@drop_depth G N B)) - | [ |- context[@drop_depth ?G ?N (T_Leaf None)] ] => - change (@drop_depth G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★))) + | [ |- 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)] ] => + change (@drop_lev G N (A,,B)) with ((@drop_lev G N A),,(@drop_lev G N B)) + | [ |- context[@drop_lev ?G ?N (T_Leaf None)] ] => + change (@drop_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★))) end. Ltac take_simplify := @@ -143,90 +353,10 @@ Section HaskFlattener. change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★))) end. - Fixpoint reduceTree {T}(unit:T)(merge:T -> T -> T)(tt:Tree ??T) : T := - match tt with - | T_Leaf None => unit - | T_Leaf (Some x) => x - | T_Branch b1 b2 => merge (reduceTree unit merge b1) (reduceTree unit merge b2) - end. - - Set Printing Width 130. - - Context {unitTy : forall TV, RawHaskType TV ★ }. - Context {prodTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★) }. - Context {gaTy : forall TV, RawHaskType TV (★ ⇛ ★ ⇛ ★ ⇛ ★)}. - - Definition ga_tree := fun TV tr => reduceTree (unitTy TV) (fun t1 t2 => TApp (TApp (prodTy TV) t1) t2) tr. - Definition ga' := fun TV ec ant' suc' => TApp (TApp (TApp (gaTy TV) ec) (ga_tree TV ant')) (ga_tree TV suc'). - Definition ga {Γ} : HaskType Γ ★ -> Tree ??(HaskType Γ ★) -> Tree ??(HaskType Γ ★) -> HaskType Γ ★ := - fun ec ant suc => - fun TV ite => - let ant' := mapOptionTree (fun x => x TV ite) ant in - let suc' := mapOptionTree (fun x => x TV ite) suc in - ga' TV (ec TV ite) ant' suc'. - - Class garrow := - { ga_id : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a a @@ l] ] - ; ga_cancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,[]) a @@ l] ] - ; ga_cancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec ([],,a) a @@ l] ] - ; ga_uncancelr : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a (a,,[]) @@ l] ] - ; ga_uncancell : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a ([],,a) @@ l] ] - ; ga_assoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga Γ ec ((a,,b),,c) (a,,(b,,c)) @@ l] ] - ; ga_unassoc : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,(b,,c)) ((a,,b),,c) @@ l] ] - ; ga_swap : ∀ Γ Δ ec l a b , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec (a,,b) (b,,a) @@ l] ] - ; ga_drop : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a [] @@ l] ] - ; ga_copy : ∀ Γ Δ ec l a , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec a (a,,a) @@ l] ] - ; ga_first : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l] |- [@ga Γ ec (a,,x) (b,,x) @@ l] ] - ; ga_second : ∀ Γ Δ ec l a b x, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l] |- [@ga Γ ec (x,,a) (x,,b) @@ l] ] - ; ga_lit : ∀ Γ Δ ec l lit , ND Rule [] [Γ > Δ > [] |- [@ga Γ ec [] [literalType lit] @@ l] ] - ; ga_curry : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec (a,,[b]) [c] @@ l] |- [@ga Γ ec a [b ---> c] @@ l] ] - ; ga_comp : ∀ Γ Δ ec l a b c, ND Rule [] [Γ > Δ > [@ga Γ ec a b @@ l],,[@ga Γ ec b c @@ l] |- [@ga Γ ec a c @@ l] ] - ; ga_apply : ∀ Γ Δ ec l a a' b c, ND Rule [] - [Γ > Δ > [@ga Γ ec a [b ---> c] @@ l],,[@ga Γ ec a' [b] @@ l] |- [@ga Γ ec (a,,a') [c] @@ l] ] - ; ga_kappa : ∀ Γ Δ ec l a b Σ, ND Rule - [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ] - [Γ > Δ > Σ |- [@ga Γ ec a b @@ l] ] - }. - Context `(gar:garrow). + Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l. - Notation "a ~~~~> b" := (@ga _ _ a b) (at level 20). - - (* - * The story: - * - code types <[t]>@c become garrows c () t - * - free variables of type t at a level lev deeper than the succedent become garrows c () t - * - free variables at the level of the succedent become - *) - Fixpoint garrowfy_raw_codetypes {TV}{κ}(depth:nat)(exp: RawHaskType TV κ) : RawHaskType TV κ := - match exp with - | TVar _ x => TVar x - | TAll _ y => TAll _ (fun v => garrowfy_raw_codetypes depth (y v)) - | TApp _ _ x y => TApp (garrowfy_raw_codetypes depth x) (garrowfy_raw_codetypes depth y) - | TCon tc => TCon tc - | TCoerc _ t1 t2 t => TCoerc (garrowfy_raw_codetypes depth t1) (garrowfy_raw_codetypes depth t2) - (garrowfy_raw_codetypes depth t) - | TArrow => TArrow - | TCode v e => match depth with - | O => ga' TV v [] [(*garrowfy_raw_codetypes depth*) e] - | (S depth') => TCode v (garrowfy_raw_codetypes depth' e) - end - | TyFunApp tfc lt => TyFunApp tfc (garrowfy_raw_codetypes_list _ depth lt) - end - with garrowfy_raw_codetypes_list {TV}(lk:list Kind)(depth:nat)(exp:@RawHaskTypeList TV lk) : @RawHaskTypeList TV lk := - match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with - | TyFunApp_nil => TyFunApp_nil - | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (garrowfy_raw_codetypes depth t) (garrowfy_raw_codetypes_list _ depth rest) - end. - Definition garrowfy_code_types {Γ}{κ}(n:nat)(ht:HaskType Γ κ) : HaskType Γ κ := - fun TV ite => - garrowfy_raw_codetypes n (ht TV ite). - Definition garrowfy_leveled_code_types {Γ}(n:nat)(ht:LeveledHaskType Γ ★) : LeveledHaskType Γ ★ := - match ht with htt @@ htlev => garrowfy_code_types (minus' n (length htlev)) htt @@ htlev end. - - Axiom literal_types_unchanged : forall n Γ l, garrowfy_code_types n (literalType l) = literalType(Γ:=Γ) l. - - Axiom flatten_coercion : forall n Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)), - HaskCoercion Γ Δ (garrowfy_code_types n σ ∼∼∼ garrowfy_code_types n τ). + Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)), + HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ). (* This tries to assign a single level to the entire succedent of a judgment. If the succedent has types from different * levels (should not happen) it just picks one; if the succedent has no non-None leaves (also should not happen) it @@ -245,58 +375,113 @@ Section HaskFlattener. end end. - Definition v2t {Γ}(ec:HaskTyVar Γ ★) := fun TV ite => TVar (ec TV ite). + Definition unlev' {Γ} (x:LeveledHaskType Γ ★) := + garrowfy_code_types (unlev x). (* "n" is the maximum depth remaining AFTER flattening *) - Definition flatten_judgment (n:nat)(j:Judg) := + Definition flatten_judgment (j:Judg) := match j as J return Judg with Γ > Δ > ant |- suc => - match (match getjlev suc with - | nil => inl _ tt - | (ec::lev') => if eqd_dec (length lev') n - (* If the judgment's level is the deepest in the proof, flatten it by turning - * all antecedent variables at this level into None's, garrowfying any other - * antecedent variables (from other levels) at the same depth, and turning the - * succedent into a garrow type *) - then inr _ (Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) (drop_depth (ec::lev') ant) - |- [ga (v2t ec) (take_lev (ec::lev') ant) (mapOptionTree unlev suc) @@ lev']) - else inl _ tt - end) with - - (* otherwise, just garrowfy all code types of the specified depth, throughout the judgment *) - | inl tt => Γ > Δ > mapOptionTree (garrowfy_leveled_code_types n) ant |- mapOptionTree (garrowfy_leveled_code_types n) suc - | inr r => r + match getjlev suc with + | nil => Γ > Δ > mapOptionTree garrowfy_leveled_code_types ant + |- mapOptionTree garrowfy_leveled_code_types suc + + | (ec::lev') => Γ > Δ > mapOptionTree garrowfy_leveled_code_types (drop_lev (ec::lev') ant) + |- [ga_mk (v2t ec) + (take_lev (ec::lev') ant) + (mapOptionTree unlev' suc) (* we know the level of all of suc *) + @@ nil] end end. - Definition boost : forall Γ Δ ant x y, - ND Rule [] [ Γ > Δ > x |- y ] -> - ND Rule [ Γ > Δ > ant |- x ] [ Γ > Δ > ant |- y ]. - admit. + Definition boost : forall Γ Δ ant x y {lev}, + ND Rule [] [ Γ > Δ > [x@@lev] |- [y@@lev] ] -> + ND Rule [ Γ > Δ > ant |- [x@@lev] ] [ Γ > Δ > ant |- [y@@lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [] ant y x lev) ]. + eapply nd_comp; [ apply nd_rlecnac | idtac ]. + apply nd_prod. + apply nd_id. + eapply nd_comp. + apply X. + eapply nd_rule. + eapply RArrange. + apply RuCanL. + Defined. + + Definition postcompose' : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec b c @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec a b) lev) ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply X. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ]. + apply ga_comp. Defined. - Definition postcompose : ∀ Γ Δ ec lev a b c, - ND Rule [] [ Γ > Δ > [] |- [@ga Γ ec a b @@ lev] ] -> - ND Rule [] [ Γ > Δ > [@ga Γ ec b c @@ lev] |- [@ga Γ ec a c @@ lev] ]. - admit. + Definition precompose' : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec b c @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ,,[@ga_mk Γ ec a b @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RExch ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (@RLet Γ Δ [@ga_mk _ ec a b @@lev] Σ (@ga_mk _ ec a c) (@ga_mk _ ec b c) lev) ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply X. + apply ga_comp. Defined. - Definition seq : ∀ Γ Δ lev a b, - ND Rule [] [ Γ > Δ > [] |- [a @@ lev] ] -> - ND Rule [] [ Γ > Δ > [] |- [b @@ lev] ] -> - ND Rule [] [ Γ > Δ > [] |- [a @@ lev],,[b @@ lev] ]. - admit. + Definition postcompose : ∀ Γ Δ ec lev a b c, + ND Rule [] [ Γ > Δ > [] |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > [@ga_mk Γ ec b c @@ lev] |- [@ga_mk Γ ec a c @@ lev] ]. + intros. + eapply nd_comp. + apply postcompose'. + apply X. + apply nd_rule. + apply RArrange. + apply RCanL. Defined. + Definition firstify : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (a,,c) (b,,c) @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply X. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. + apply ga_first. + Defined. + + Definition secondify : ∀ Γ Δ ec lev a b c Σ, + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ lev] ] -> + ND Rule [] [ Γ > Δ > Σ |- [@ga_mk Γ ec (c,,a) (c,,b) @@ lev] ]. + intros. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply RLet ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. + apply X. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RuCanL ]. + apply ga_second. + Defined. + Lemma ga_unkappa : ∀ Γ Δ ec l a b Σ, ND Rule - [Γ > Δ > Σ |- [@ga Γ ec a b @@ l] ] - [Γ > Δ > Σ,,[@ga Γ ec [] a @@ l] |- [@ga Γ ec [] b @@ l] ]. + [Γ > Δ > Σ |- [@ga_mk Γ ec a b @@ l] ] + [Γ > Δ > Σ,,[@ga_mk Γ ec [] a @@ l] |- [@ga_mk Γ ec [] b @@ l] ]. intros. set (ga_comp Γ Δ ec l [] a b) as q. set (@RLet Γ Δ) as q'. - set (@RLet Γ Δ [@ga _ ec [] a @@ l] Σ (@ga _ ec [] b) (@ga _ ec a b) l) as q''. + set (@RLet Γ Δ [@ga_mk _ ec [] a @@ l] Σ (@ga_mk _ ec [] b) (@ga_mk _ ec a b) l) as q''. eapply nd_comp. Focus 2. eapply nd_rule. @@ -320,18 +505,18 @@ Section HaskFlattener. (* Notation "` x" := (take_lev _ x) (at level 20). Notation "`` x" := (mapOptionTree unlev x) (at level 20). - Notation "``` x" := (drop_depth _ x) (at level 20). + Notation "``` x" := (drop_lev _ x) (at level 20). *) Definition garrowfy_arrangement' : forall Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), - ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev] ]. + ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil] ]. intros Γ Δ ec lev. refine (fix garrowfy ant1 ant2 (r:Arrange ant1 ant2): - ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ lev]] := + ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (take_lev (ec :: lev) ant1) @@ nil]] := match r as R in Arrange A B return - ND Rule [] [Γ > Δ > [] |- [@ga _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ lev]] + ND Rule [] [Γ > Δ > [] |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) B) (take_lev (ec :: lev) A) @@ nil]] with | RCanL a => let case_RCanL := tt in ga_uncancell _ _ _ _ _ | RCanR a => let case_RCanR := tt in ga_uncancelr _ _ _ _ _ @@ -344,32 +529,45 @@ Section HaskFlattener. | RCont a => let case_RCont := tt in ga_copy _ _ _ _ _ | RLeft a b c r' => let case_RLeft := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_second _ _ _ _ _ _ _) | RRight a b c r' => let case_RRight := tt in garrowfy _ _ r' ;; boost _ _ _ _ _ (ga_first _ _ _ _ _ _ _) - | RComp a b c r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2) + | RComp c b a r1 r2 => let case_RComp := tt in (fun r1' r2' => _) (garrowfy _ _ r1) (garrowfy _ _ r2) end); clear garrowfy; repeat take_simplify; repeat drop_simplify; intros. destruct case_RComp. - refine ( _ ;; boost _ _ _ _ _ (ga_comp _ _ _ _ _ _ _)). - apply seq. + set (take_lev (ec :: lev) a) as a' in *. + set (take_lev (ec :: lev) b) as b' in *. + set (take_lev (ec :: lev) c) as c' in *. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply + (@RLet Γ Δ [] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) a' b')) ]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + apply nd_prod. apply r2'. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RuCanL ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RCanR ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply + (@RLet Γ Δ [@ga_mk _ (v2t ec) a' b' @@ _] [] (@ga_mk _ (v2t ec) a' c') (@ga_mk _ (v2t ec) b' c'))]. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_prod. apply r1'. + apply ga_comp. Defined. Definition garrowfy_arrangement : forall Γ (Δ:CoercionEnv Γ) n (ec:HaskTyVar Γ ★) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2) succ, ND Rule - [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant1) - |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree unlev succ) @@ lev]] - [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth n ant2) - |- [@ga _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree unlev succ) @@ lev]]. + [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant1) + |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant1) (mapOptionTree (unlev' ) succ) @@ nil]] + [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev n ant2) + |- [@ga_mk _ (v2t ec) (take_lev (ec :: lev) ant2) (mapOptionTree (unlev' ) succ) @@ nil]]. intros. refine ( _ ;; (boost _ _ _ _ _ (postcompose _ _ _ _ _ _ _ (garrowfy_arrangement' Γ Δ ec lev ant1 ant2 r)))). apply nd_rule. apply RArrange. refine ((fix garrowfy ant1 ant2 (r:Arrange ant1 ant2) := match r as R in Arrange A B return - Arrange (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ A)) - (mapOptionTree (garrowfy_leveled_code_types ((length lev))) (drop_depth _ B)) with + Arrange (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ A)) + (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev _ B)) with | RCanL a => let case_RCanL := tt in RCanL _ | RCanR a => let case_RCanR := tt in RCanR _ | RuCanL a => let case_RuCanL := tt in RuCanL _ @@ -386,9 +584,9 @@ Section HaskFlattener. Defined. Definition flatten_arrangement : - forall n Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2), - ND Rule (mapOptionTree (flatten_judgment n) [Γ > Δ > ant1 |- succ]) - (mapOptionTree (flatten_judgment n) [Γ > Δ > ant2 |- succ]). + forall Γ Δ ant1 ant2 succ (r:Arrange ant1 ant2), + ND Rule (mapOptionTree (flatten_judgment ) [Γ > Δ > ant1 |- succ]) + (mapOptionTree (flatten_judgment ) [Γ > Δ > ant2 |- succ]). intros. simpl. set (getjlev succ) as succ_lev. @@ -412,49 +610,128 @@ Section HaskFlattener. apply RRight; auto. eapply RComp; [ apply IHr1 | apply IHr2 ]. - set (Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n) as lev_is_n. - assert (lev_is_n=Peano_dec.eq_nat_dec (Datatypes.length succ_lev) n). - reflexivity. - destruct lev_is_n. - rewrite <- e. - apply garrowfy_arrangement. + apply garrowfy_arrangement. apply r. - auto. - apply nd_rule. - apply RArrange. - induction r; simpl. - apply RCanL. - apply RCanR. - apply RuCanL. - apply RuCanR. - apply RAssoc. - apply RCossa. - apply RExch. - apply RWeak. - apply RCont. - apply RLeft; auto. - apply RRight; auto. - eapply RComp; [ apply IHr1 | apply IHr2 ]. Defined. + Definition ga_join Γ Δ Σ₁ Σ₂ a b ec : + ND Rule [] [Γ > Δ > Σ₁ |- [@ga_mk _ ec [] a @@ nil]] -> + ND Rule [] [Γ > Δ > Σ₂ |- [@ga_mk _ ec [] b @@ nil]] -> + ND Rule [] [Γ > Δ > Σ₁,,Σ₂ |- [@ga_mk _ ec [] (a,,b) @@ nil]]. + intro pfa. + intro pfb. + apply secondify with (c:=a) in pfb. + eapply nd_comp. + Focus 2. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + eapply nd_comp; [ eapply nd_llecnac | idtac ]. + eapply nd_prod. + apply pfb. + clear pfb. + apply postcompose'. + eapply nd_comp. + apply pfa. + clear pfa. + apply boost. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply RCanL ]. + apply precompose'. + apply ga_uncancelr. + apply nd_id. + Defined. + Definition arrange_brak : forall Γ Δ ec succ t, - ND Rule - [Γ > Δ > - mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),, - [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- - [(@ga _ (v2t ec) [] [t]) @@ nil]] - [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@ nil]]. - admit. + ND Rule + [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),, + [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]] + [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]. + intros. + unfold drop_lev. + set (@arrange' _ succ (levelMatch (ec::nil))) as q. + set (arrangeMap _ _ garrowfy_leveled_code_types q) as y. + eapply nd_comp. + Focus 2. + eapply nd_rule. + eapply RArrange. + apply y. + idtac. + clear y q. + simpl. + eapply nd_comp; [ apply nd_llecnac | idtac ]. + eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ]. + apply nd_prod. + Focus 2. + apply nd_id. + idtac. + induction succ; try destruct a; simpl. + unfold take_lev. + unfold mkTakeFlags. + unfold mkFlags. + unfold bnot. + simpl. + destruct l as [t' lev']. + destruct lev' as [|ec' lev']. + simpl. + apply ga_id. + unfold levelMatch. + set (@eqd_dec (HaskLevel Γ) (haskLevelEqDecidable Γ) (ec' :: lev') (ec :: nil)) as q. + destruct q. + inversion e; subst. + simpl. + apply nd_rule. + apply RVar. + simpl. + apply ga_id. + apply ga_id. + unfold take_lev. + simpl. + apply ga_join. + apply IHsucc1. + apply IHsucc2. Defined. Definition arrange_esc : forall Γ Δ ec succ t, - ND Rule - [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types 0) succ |- [(@ga _ (v2t ec) [] [t]) @@ nil]] - [Γ > Δ > - mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec :: nil) succ),, - [(@ga _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga _ (v2t ec) [] [t]) @@ nil]]. - admit. - Defined. + ND Rule + [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) succ |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]] + [Γ > Δ > mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: nil) succ),, + [(@ga_mk _ (v2t ec) [] (take_lev (ec :: nil) succ)) @@ nil] |- [(@ga_mk _ (v2t ec) [] [garrowfy_code_types t]) @@ nil]]. + intros. + unfold drop_lev. + set (@arrange _ succ (levelMatch (ec::nil))) as q. + set (arrangeMap _ _ garrowfy_leveled_code_types q) as y. + eapply nd_comp. + eapply nd_rule. + eapply RArrange. + apply y. + idtac. + clear y q. + + induction succ. + destruct a. + destruct l. + simpl. + unfold mkDropFlags; simpl. + unfold take_lev. + unfold mkTakeFlags. + simpl. + destruct (General.list_eq_dec h0 (ec :: nil)). + simpl. + unfold garrowfy_leveled_code_types'. + rewrite e. + apply nd_id. + simpl. + apply nd_rule. + apply RArrange. + apply RLeft. + apply RWeak. + simpl. + apply nd_rule. + unfold take_lev. + simpl. + apply RArrange. + apply RLeft. + apply RWeak. + apply (Prelude_error "escapifying code with multi-leaf antecedents is not supported"). + Defined. Lemma mapOptionTree_distributes : forall T R (a b:Tree ??T) (f:T->R), @@ -462,35 +739,57 @@ Section HaskFlattener. reflexivity. Qed. - Lemma garrowfy_commutes_with_substT : - forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ), - garrowfy_code_types n (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v)) - (garrowfy_code_types n τ). - admit. - Qed. - - Lemma garrowfy_commutes_with_HaskTAll : - forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), - garrowfy_code_types n (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v)). - admit. - Qed. - - Lemma garrowfy_commutes_with_HaskTApp : - forall n κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), - garrowfy_code_types n (HaskTApp (weakF σ) (FreshHaskTyVar κ)) = - HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes n (σ TV ite v))) (FreshHaskTyVar κ). - admit. - Qed. - - Lemma garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ n t, - garrowfy_leveled_code_types n (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types n t). - admit. - Qed. + Axiom garrowfy_commutes_with_substT : + forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★) (τ:HaskType Γ κ), + garrowfy_code_types (substT σ τ) = substT (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)) + (garrowfy_code_types τ). + + Axiom garrowfy_commutes_with_HaskTAll : + forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), + garrowfy_code_types (HaskTAll κ σ) = HaskTAll κ (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v)). + + Axiom garrowfy_commutes_with_HaskTApp : + forall κ Γ (Δ:CoercionEnv Γ) (σ:∀ TV, InstantiatedTypeEnv TV Γ → TV κ → RawHaskType TV ★), + garrowfy_code_types (HaskTApp (weakF σ) (FreshHaskTyVar κ)) = + HaskTApp (weakF (fun TV ite v => garrowfy_raw_codetypes (σ TV ite v))) (FreshHaskTyVar κ). + + Axiom garrowfy_commutes_with_weakLT : forall (Γ:TypeEnv) κ t, + garrowfy_leveled_code_types (weakLT(Γ:=Γ)(κ:=κ) t) = weakLT(Γ:=Γ)(κ:=κ) (garrowfy_leveled_code_types t). + + Axiom globals_do_not_have_code_types : forall (Γ:TypeEnv) (g:Global Γ) v, + garrowfy_code_types (g v) = g v. + + Definition decide_tree_empty : forall {T:Type}(t:Tree ??T), + sum { q:Tree unit & t = mapTree (fun _ => None) q } unit. + intro T. + refine (fix foo t := + match t with + | T_Leaf x => _ + | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _ + end). + intros. + destruct x. + right; apply tt. + left. + exists (T_Leaf tt). + auto. + destruct b1'. + destruct b2'. + destruct s. + destruct s0. + subst. + left. + exists (x,,x0). + reflexivity. + right; auto. + right; auto. + Defined. + Definition flatten_proof : - forall n {h}{c}, + forall {h}{c}, ND Rule h c -> - ND Rule (mapOptionTree (flatten_judgment n) h) (mapOptionTree (flatten_judgment n) c). + ND Rule (mapOptionTree (flatten_judgment ) h) (mapOptionTree (flatten_judgment ) c). intros. eapply nd_map'; [ idtac | apply X ]. clear h c X. @@ -520,45 +819,54 @@ Section HaskFlattener. end); clear X h c. destruct case_RArrange. - apply (flatten_arrangement n Γ Δ a b x d). + apply (flatten_arrangement Γ Δ a b x d). destruct case_RBrak. simpl. - destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n). destruct lev. - simpl. - simpl. - destruct n. - change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@ nil]) - with ([ga (v2t ec) [] [t] @@ nil]). - refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t] - (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ)) ;; _). + change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil]) + with ([ga_mk (v2t ec) [] [garrowfy_code_types t] @@ nil]). + refine (ga_unkappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ + (mapOptionTree (garrowfy_leveled_code_types) (drop_lev (ec::nil) succ)) ;; _ ). apply arrange_brak. - inversion e. - apply (Prelude_error "found Brak at depth >0"). - apply (Prelude_error "found Brak at depth >0"). + apply (Prelude_error "found Brak at depth >0 (a)"). destruct case_REsc. simpl. - destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n). destruct lev. simpl. - destruct n. - change ([garrowfy_code_types 0 (<[ ec |- t ]>) @@ nil]) - with ([ga (v2t ec) [] [t] @@ nil]). - refine (_ ;; ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) [t] - (mapOptionTree (garrowfy_leveled_code_types 0) (drop_depth (ec::nil) succ))). - apply arrange_esc. - inversion e. - apply (Prelude_error "found Esc at depth >0"). - apply (Prelude_error "found Esc at depth >0"). + change ([garrowfy_code_types (<[ ec |- t ]>) @@ nil]) + with ([ga_mk (v2t ec) [] [garrowfy_code_types 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 ]. + apply ga_join. + apply IHx1. + apply IHx2. + unfold unlev'. + simpl. + apply postcompose. + apply ga_drop. + + (* environment has non-empty leaves *) + apply (ga_kappa Γ Δ (v2t ec) nil (take_lev (ec::nil) succ) _ _). + apply (Prelude_error "found Esc at depth >0 (a)"). destruct case_RNote. simpl. destruct l; simpl. apply nd_rule; apply RNote; auto. - destruct (Peano_dec.eq_nat_dec (Datatypes.length l) n). - apply nd_rule; apply RNote; auto. apply nd_rule; apply RNote; auto. destruct case_RLit. @@ -566,13 +874,12 @@ Section HaskFlattener. destruct l0; simpl. rewrite literal_types_unchanged. apply nd_rule; apply RLit. - destruct (Peano_dec.eq_nat_dec (Datatypes.length l0) n); unfold mapTree; unfold mapOptionTree; simpl. unfold take_lev; simpl. - unfold drop_depth; simpl. - apply ga_lit. + unfold drop_lev; simpl. + unfold unlev'. + simpl. rewrite literal_types_unchanged. - apply nd_rule. - apply RLit. + apply ga_lit. destruct case_RVar. Opaque flatten_judgment. @@ -583,30 +890,24 @@ Section HaskFlattener. unfold getjlev. destruct lev. apply nd_rule. apply RVar. - destruct (eqd_dec (Datatypes.length lev) n). - repeat drop_simplify. + unfold unlev'. repeat take_simplify. simpl. apply ga_id. - apply nd_rule. - apply RVar. - destruct case_RGlobal. simpl. - destruct l as [|ec lev]; simpl; [ apply nd_rule; apply RGlobal; auto | idtac ]. - destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RGlobal; auto ]; simpl. + rename l into g. + rename σ into l. + destruct l as [|ec lev]; simpl; [ apply nd_rule; rewrite globals_do_not_have_code_types; apply RGlobal; auto | idtac ]. apply (Prelude_error "found RGlobal at depth >0"). destruct case_RLam. - Opaque drop_depth. + Opaque drop_lev. Opaque take_lev. simpl. destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLam; auto | idtac ]. - destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLam; auto ]; simpl. - rewrite <- e. - clear e n. repeat drop_simplify. repeat take_simplify. eapply nd_comp. @@ -616,14 +917,12 @@ Section HaskFlattener. apply RCanR. apply boost. apply ga_curry. - + destruct case_RCast. simpl. destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RCast; auto | idtac ]. apply flatten_coercion; auto. - destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RCast; auto ]; simpl. apply (Prelude_error "RCast at level >0"). - apply flatten_coercion; auto. destruct case_RJoin. simpl. @@ -638,37 +937,30 @@ Section HaskFlattener. simpl. destruct lev as [|ec lev]. simpl. apply nd_rule. - replace (garrowfy_code_types n (tx ---> te)) with ((garrowfy_code_types n tx) ---> (garrowfy_code_types n te)). + replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)). apply RApp. - unfold garrowfy_code_types. - simpl. reflexivity. - destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n). - eapply nd_comp. - eapply nd_rule. - apply RJoin. - repeat drop_simplify. + repeat drop_simplify. repeat take_simplify. - apply boost. - apply ga_apply. - - replace (garrowfy_code_types (minus' n (length (ec::lev))) (tx ---> te)) - with ((garrowfy_code_types (minus' n (length (ec::lev))) tx) ---> - (garrowfy_code_types (minus' n (length (ec::lev))) te)). - apply nd_rule. - apply RApp. - unfold garrowfy_code_types. - simpl. + rewrite mapOptionTree_distributes. + set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₁)) as Σ₁'. + set (mapOptionTree (garrowfy_leveled_code_types ) (drop_lev (ec :: lev) Σ₂)) as Σ₂'. + set (take_lev (ec :: lev) Σ₁) as Σ₁''. + set (take_lev (ec :: lev) Σ₂) as Σ₂''. + replace (garrowfy_code_types (tx ---> te)) with ((garrowfy_code_types tx) ---> (garrowfy_code_types te)). + apply (Prelude_error "FIXME: ga_apply"). reflexivity. (* Notation "` x" := (take_lev _ x) (at level 20). Notation "`` x" := (mapOptionTree unlev x) (at level 20). - Notation "``` x" := ((drop_depth _ x)) (at level 20). + Notation "``` x" := ((drop_lev _ x)) (at level 20). Notation "!<[]> x" := (garrowfy_code_types _ x) (at level 1). Notation "!<[@]>" := (garrowfy_leveled_code_types _) (at level 1). *) destruct case_RLet. + apply (Prelude_error "FIXME: RLet"). +(* simpl. destruct lev as [|ec lev]; simpl; [ apply nd_rule; apply RLet; auto | idtac ]. destruct (Peano_dec.eq_nat_dec (Datatypes.length lev) n); [ idtac | apply nd_rule; apply RLet; auto ]; simpl. @@ -678,9 +970,9 @@ Section HaskFlattener. rename σ₂ into b. rewrite mapOptionTree_distributes. rewrite mapOptionTree_distributes. - set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₁)) as A. + set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A. set (take_lev (ec :: lev) Σ₁) as A'. - set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_depth (ec :: lev) Σ₂)) as B. + set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B. set (take_lev (ec :: lev) Σ₂) as B'. simpl. @@ -723,7 +1015,7 @@ Section HaskFlattener. eapply RVar. apply nd_id. - +*) destruct case_RVoid. simpl. apply nd_rule. @@ -737,7 +1029,7 @@ Section HaskFlattener. apply RAppT. apply Δ. apply Δ. - apply (Prelude_error "AppT at depth>0"). + apply (Prelude_error "ga_apply"). destruct case_RAbsT. simpl. destruct lev; simpl. @@ -745,8 +1037,8 @@ Section HaskFlattener. rewrite garrowfy_commutes_with_HaskTApp. eapply nd_comp; [ idtac | eapply nd_rule; eapply RAbsT ]. simpl. - set (mapOptionTree (garrowfy_leveled_code_types n) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a. - set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types n) Σ)) as q'. + set (mapOptionTree (garrowfy_leveled_code_types ) (mapOptionTree (weakLT(κ:=κ)) Σ)) as a. + set (mapOptionTree (weakLT(κ:=κ)) (mapOptionTree (garrowfy_leveled_code_types ) Σ)) as q'. assert (a=q'). unfold a. unfold q'.