From 86533ec8492c5736e8cc2bdd55b88fc013c21f89 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 9 May 2011 16:38:49 -0700 Subject: [PATCH] move general-purpose routines from HaskFlattener to HaskProof/General --- src/General.v | 58 +++++++++++++++++ src/HaskFlattener.v | 180 ++++++++++++--------------------------------------- src/HaskProof.v | 38 ++++++++++- 3 files changed, 137 insertions(+), 139 deletions(-) diff --git a/src/General.v b/src/General.v index d017894..cf9d28d 100644 --- a/src/General.v +++ b/src/General.v @@ -89,6 +89,13 @@ Fixpoint treeReduce {T:Type}{R:Type}(mapLeaf:T->R)(mergeBranches:R->R->R) (t:Tre Definition treeDecomposition {D T:Type} (mapLeaf:T->D) (mergeBranches:D->D->D) := forall d:D, { tt:Tree T & d = treeReduce mapLeaf mergeBranches 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. + Lemma tree_dec_eq : forall {Q}(t1 t2:Tree ??Q), (forall q1 q2:Q, sumbool (q1=q2) (not (q1=q2))) -> @@ -445,6 +452,55 @@ Instance EqDecidableList {T:Type}(eqd:EqDecidable T) : EqDecidable (list T). Defined. (*******************************************************************************) +(* Tree Flags *) + +(* TreeFlags is effectively a tree of booleans whose shape matches that of another tree *) +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). + +(* If flags are calculated using a local condition, this will build the flags *) +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. + +(* takeT and dropT are not exact inverses! *) + +(* drop replaces each leaf where the flag is set with a [] *) +Fixpoint dropT {T}{Σ:Tree ??T}(tf:TreeFlags Σ) : Tree ??T := + match tf with + | tf_leaf_true x => [] + | tf_leaf_false x => Σ + | tf_branch b1 b2 tb1 tb2 => (dropT tb1),,(dropT tb2) + end. + +(* takeT returns only those leaves for which the flag is set; all others are omitted entirely from the tree *) +Fixpoint takeT {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 takeT tb1 with + | None => takeT tb2 + | Some b1' => match takeT tb2 with + | None => Some b1' + | Some b2' => Some (b1',,b2') + end + end + end. + +(* lift a function T->bool to a function (option T)->bool by yielding (None |-> b) *) +Definition liftBoolFunc {T}(b:bool)(f:T -> bool) : ??T -> bool := + fun t => + match t with + | None => b + | Some x => f x + end. + +(*******************************************************************************) (* Length-Indexed Lists *) Inductive vec (A:Type) : nat -> Type := @@ -739,6 +795,8 @@ Lemma extensionality_composes : forall t1 t2 t3 (f f':t1->t2) (g g':t2->t3), Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))). +(* boolean "not" *) +Definition bnot (b:bool) : bool := if b then false else true. (* string stuff *) Variable eol : string. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index ae99605..6386c19 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -31,6 +31,7 @@ Require Import HaskProofToStrong. Require Import HaskWeakToStrong. Open Scope nd_scope. +Set Printing Width 130. (* * The flattening transformation. Currently only TWO-level languages are @@ -42,97 +43,9 @@ Open Scope nd_scope. *) Section HaskFlattener. - 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). - - 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)) Σ)))). + Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))). intros. induction Σ. simpl. @@ -144,7 +57,7 @@ Section HaskFlattener. simpl. apply RuCanL. simpl in *. - eapply RComp; [ idtac | apply swapMiddle ]. + eapply RComp; [ idtac | apply arrangeSwapMiddle ]. eapply RComp. eapply RLeft. apply IHΣ2. @@ -154,7 +67,7 @@ Section HaskFlattener. Definition arrange' : forall {T} (Σ:Tree ??T) (f:T -> bool), - Arrange (drop (mkFlags (setNone false f) Σ),,( (drop (mkFlags (setNone false (bnot ○ f)) Σ)))) Σ. + Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ. intros. induction Σ. simpl. @@ -166,7 +79,7 @@ Section HaskFlattener. simpl. apply RCanL. simpl in *. - eapply RComp; [ apply swapMiddle | idtac ]. + eapply RComp; [ apply arrangeSwapMiddle | idtac ]. eapply RComp. eapply RLeft. apply IHΣ2. @@ -174,15 +87,6 @@ Section HaskFlattener. apply IHΣ1. Defined. - Definition minus' n m := - match m with - | 0 => n - | _ => match n with - | 0 => 0 - | _ => n - m - end - end. - Ltac eqd_dec_refl' := match goal with | [ |- context[@eqd_dec ?T ?V ?X ?X] ] => @@ -190,15 +94,6 @@ Section HaskFlattener. [ clear eqd_dec1 | set (eqd_dec2 (refl_equal _)) as eqd_dec2'; inversion eqd_dec2' ] 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 (hetmet_flatten : WeakExprVar). Context (hetmet_unflatten : WeakExprVar). Context (hetmet_id : WeakExprVar). @@ -284,25 +179,31 @@ Section HaskFlattener. (* In a tree of types, replace any type at depth "lev" or greater None *) Definition mkDropFlags {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : TreeFlags tt := - mkFlags (setNone false (levelMatch lev)) tt. + mkFlags (liftBoolFunc false (levelMatch lev)) tt. Definition drop_lev {Γ}(lev:HaskLevel Γ)(tt:Tree ??(LeveledHaskType Γ ★)) : Tree ??(LeveledHaskType Γ ★) := - drop (mkDropFlags lev tt). + dropT (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. + mkFlags (liftBoolFunc 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)) (dropT (mkTakeFlags lev tt)). (* mapOptionTree (fun x => garrowfy_code_types (unlev x)) - (maybeTree (take tt (mkFlags ( + (maybeTree (takeT tt (mkFlags ( fun t => match t with | Some (ttype @@ tlev) => if eqd_dec tlev lev then true else false | _ => true end ) tt))). + + Definition maybeTree {T}(t:??(Tree ??T)) : Tree ??T := + match t with + | None => [] + | Some x => x + end. *) Lemma drop_lev_lemma : forall Γ (lev:HaskLevel Γ) x, drop_lev lev [x @@ lev] = []. @@ -361,11 +262,33 @@ Section HaskFlattener. change (@take_lev G N (T_Leaf (@None (LeveledHaskType G ★)))) with (T_Leaf (@None (LeveledHaskType G ★))) end. + (* AXIOMS *) + Axiom literal_types_unchanged : forall Γ l, garrowfy_code_types (literalType l) = literalType(Γ:=Γ) l. Axiom flatten_coercion : forall Γ Δ κ (σ τ:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ ∼∼∼ τ)), HaskCoercion Γ Δ (garrowfy_code_types σ ∼∼∼ garrowfy_code_types τ). + 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. + (* 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 * picks nil *) @@ -510,11 +433,12 @@ Section HaskFlattener. apply q. Defined. -(* + (* useful for cutting down on the pretty-printed noise + Notation "` x" := (take_lev _ x) (at level 20). Notation "`` x" := (mapOptionTree unlev x) (at level 20). Notation "``` x" := (drop_lev _ x) (at level 20). -*) + *) Definition garrowfy_arrangement' : forall Γ (Δ:CoercionEnv Γ) (ec:HaskTyVar Γ ECKind) (lev:HaskLevel Γ) (ant1 ant2:Tree ??(LeveledHaskType Γ ★)) (r:Arrange ant1 ant2), @@ -533,7 +457,7 @@ Section HaskFlattener. | RAssoc a b c => let case_RAssoc := tt in ga_assoc _ _ _ _ _ _ _ | RCossa a b c => let case_RCossa := tt in ga_unassoc _ _ _ _ _ _ _ | RExch a b => let case_RExch := tt in ga_swap _ _ _ _ _ _ - | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _ + | RWeak a => let case_RWeak := tt in ga_drop _ _ _ _ _ | 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 _ _ _ _ _ _ _) @@ -747,26 +671,6 @@ Section HaskFlattener. reflexivity. 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. diff --git a/src/HaskProof.v b/src/HaskProof.v index 0b0200b..d28db62 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -169,4 +169,40 @@ Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), Fa auto. Qed. - +(* "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. + +(* a frequently-used Arrange *) +Definition arrangeSwapMiddle {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. -- 1.7.10.4