diff --git a/DataflowRewriter/Rewrites/Loop.lean b/DataflowRewriter/Rewrites/Loop.lean new file mode 100644 index 0000000..75a23b5 --- /dev/null +++ b/DataflowRewriter/Rewrites/Loop.lean @@ -0,0 +1,323 @@ + +import DataflowRewriter.Rewrites.LoopRewrite +import DataflowRewriter.ExprLowLemmas +import DataflowRewriter.Rewrites.LoopRewriteCorrect +import Mathlib +import Aesop + +--import DataflowRewriter.Rewrites.MatchGoal + +namespace DataflowRewriter.LoopRewrite + +open Batteries (AssocList) + +--open matchGoal + +open Lean hiding AssocList +open Meta Elab + +open StringModule + +section Proof + +variable {Data : Type} +variable (DataS : String) +variable (f : Data → Data × Bool) + +variable [Inhabited Data] + + + +def apply (n : Nat) (i : Data) : Data × Bool := +match n with +| 0 => f i +| n' + 1 => f (apply n' i).fst + +def iterate (i: Data) (n : Nat) (i': Data) : Prop := + (∀ m, m < n -> (apply f m i).snd = true) ∧ apply f n i = (i', false) + + +-- theorem compute_n (i : Data) : +-- ∃ n i', iterate f i n i' = true := by +-- constructor; constructor +-- . unfold iterate +-- simp +-- and_intros +-- . intro m h1 +-- unfold apply; + +omit [Inhabited Data] in +@[simp] +theorem input_rule_isData {input_rule} : + ((lhsEvaled f).inputs.find? ↑"i_in") = .some input_rule -> + Data = input_rule.fst := by + unfold lhsEvaled + simp; intro h1 + subst_vars; rfl + +#check lhsEvaled + + +-- theorem flushing (n : Nat) input_rule s i i' s' s_int +-- (h : ((lhsEvaled f).inputs.find? ↑"i_in") = .some input_rule) : +-- input_rule.snd s i s' -> +-- check_output f n (input_rule_isData f h i) i' -> +-- existSR (lhsEvaled f).internals s' s_int -> +-- ∃ s'', existSR (lhsEvaled f).internals s_int s'' ∧ s''.1 = i' := by admit + +--Invariant flush + + + +inductive flush_relation : lhsType Data -> Prop where +| intros : ∀ (s : lhsType Data) x_bag x_initL x_initB x_module x_splitD x_splitB x_branchD x_branchB x_forkR x_forkL x_muxB x_muxI x_muxC, + ⟨x_bag, ⟨x_initL, x_initB⟩, x_module, ⟨x_splitD, x_splitB⟩ ,⟨x_branchD, x_branchB⟩, ⟨x_forkR, x_forkL⟩, x_muxB, x_muxI, x_muxC ⟩ = s -> + (x_module.map Prod.fst ++ x_splitD ++ x_branchD ++ x_muxB = [] + ∨ + ∃ elem, x_module.map Prod.fst ++ x_splitD ++ x_branchD ++ x_muxB = [elem]) -> + (x_initB = false -> x_splitB ++ x_forkL ++ x_initL ++ x_muxC = []) -> + (x_initB = true -> ∃ elem, x_splitB ++ x_forkL ++ x_initL ++ x_muxC = [elem]) -> + flush_relation s + + +inductive computation_relation : (lhsType Data) -> (Data) -> Prop where +| intros : ∀ (s : lhsType Data) x_bag x_initL x_initB x_module x_splitD x_splitB x_branchD x_branchB x_forkR x_forkL x_muxB x_muxI x_muxC (i_in : Data), + ⟨x_bag, ⟨x_initL, x_initB⟩, x_module, ⟨x_splitD, x_splitB⟩ ,⟨x_branchD, x_branchB⟩, ⟨x_forkR, x_forkL⟩, x_muxB, x_muxI, x_muxC ⟩ = s -> + (∃ elem, x_branchD = [elem] -> x_splitB ++ x_forkL ++ x_initL ++ x_muxC = [true]) -> + ( ∀ n k i', + iterate f i_in n i' -> + (k < n -> x_module = [(apply f k i_in )] ∧ x_module.map Prod.snd = [true]) -> + (k = n -> x_module = [(apply f n i_in )] ∧ x_module.map Prod.snd = [false]) -> + (x_splitB = [true] -> k < n ∧ x_splitD = [(apply f k i_in )].map Prod.fst) -> + (x_splitB = [false] -> k = n ∧ x_splitD = [(apply f k i_in )].map Prod.fst)) -> + computation_relation s i_in + +inductive state_relation : lhsType Data -> Data -> Prop where +| base: ∀ (s : lhsType Data) i_in, + flush_relation s -> + computation_relation f s i_in -> + state_relation s i_in + + +#print lhsEvaled + + +@[aesop unsafe 90% forward] +theorem one_element {α : Type _ } (l1 l2 l3 l4 : List α) ( a : α) : + l1 ++ (l2 ++ ([a] ++ (l3 ++ l4))) = [a] -> l1 = [] ∧ l2 = [] ∧ l3 = [] ∧ l4 = [] := by +--aesop (add norm [List.append_right_eq_self, List.append_left_eq_self ]) +admit + +@[aesop unsafe 90% forward] +theorem one_element2 {α : Type _ } (l1 l2 l3 l4 : List α) ( a : α) : + l1 ++ ([a] ++ (l2 ++ (l3 ++ l4))) = [a] -> l1 = [] ∧ l2 = [] ∧ l3 = [] ∧ l4 = [] := by +--aesop (add norm [List.append_right_eq_self, List.append_left_eq_self ]) +admit + +@[aesop unsafe 10% forward] +theorem one_element1 {α : Type _ } (l1 l2 l3 : List α) ( a : α) : + l1 ++ ([a] ++ (l2 ++ l3)) = [a] -> l1 = [] ∧ l2 = [] ∧ l3 = [] := by +--aesop (add norm [List.append_right_eq_self, List.append_left_eq_self ]) +admit + + +-- @[aesop safe apply] +-- theorem one_element_different {α : Type _ } (i : Nat) (l1 l2 l3 l4 : List α) (a b : α): +-- List.insertIdx i a (l1 ++ l2 ++ l3 ++ l4) = [b] -> (a = b) := by admit + + +@[aesop safe forward] +theorem one_element_different {α : Type _ } (l1 l2 l3 l4 : List α) (a b : α): + l1 ++ (l2 ++ ([a] ++ (l3 ++ l4))) = [b] -> (a = b) := by admit + + +@[aesop safe forward] +theorem one_element_different2 {α : Type _ } (l1 l2 l3 l4 : List α) (a b : α): + l1 ++ ([a] ++ (l2 ++ (l3 ++ l4))) = [b] -> (a = b) := by admit + +@[aesop safe forward] +theorem one_element_different1 {α : Type _ } (l1 l2 l3: List α) (a b : α): + l1 ++ ([a] ++ (l2 ++ l3)) = [b] -> (a = b) := by admit + +set_option maxHeartbeats 1000000 + +--add_aesop_rules simp [List.append_cons] + +-- attribute [-simp] List.singleton_append +-- attribute [-simp] List.append_cons + +theorem only_one_data_in_flight: + ∀ (s s' : lhsType Data) i_in rule, + rule ∈ (lhsEvaled f).internals -> + rule s s' -> + state_relation f s i_in -> + state_relation f s' i_in := by + intro s s' i_in rule h1 h2 h3 + let ⟨x_bag, ⟨x_initL, x_initB⟩, x_module, ⟨x_splitD, x_splitB⟩ ,⟨x_branchD, x_branchB⟩, ⟨x_forkR, x_forkL⟩, x_muxB, x_muxI, x_muxC ⟩ := s + let ⟨x_bag', ⟨x_initL', x_initB'⟩, x_module', ⟨x_splitD', x_splitB'⟩ ,⟨x_branchD', x_branchB'⟩, ⟨x_forkR', x_forkL'⟩, x_muxB', x_muxI', x_muxC'⟩ := s' + fin_cases h1 + . dsimp at h2 + obtain ⟨h2, _⟩ := h2 + specialize h2 rfl + obtain ⟨cons, newC, h⟩ := h2 + obtain ⟨x_bag'_int, ⟨x_initL'_int, x_initB'_int⟩, x_module'_int, ⟨x_splitD'_int, x_splitB'_int⟩ ,⟨x_branchD'_int, x_branchB'_int⟩, ⟨x_forkR'_int, x_forkL'_int⟩, x_muxB'_int, x_muxI'_int, x_muxC'_int⟩ := cons + dsimp at h + simp_all; repeat cases ‹_ ∧ _› + --let ⟨⟨⟨h4, ⟨h15, ⟨⟨h20, h26⟩, ⟨h21, h27⟩, ⟨h22, h28⟩, h23, h24, h25⟩⟩⟩, h5⟩ , ⟨⟨⟨⟨⟨⟨ h6, h13, h14⟩, ⟨h12, h17⟩⟩, ⟨h11, h16⟩⟩, ⟨h10, h18⟩⟩, h8⟩, ⟨h9, h19⟩⟩, h7⟩ := h + subst_vars + rcases h3 with ⟨ h3, h3'⟩ + constructor + . cases h3 + rename_i h3 _ _ + constructor + . rfl + . cases h3 <;> simp_all + . cases h3 + . cases x_initB <;> simp_all + . cases x_initB <;> simp_all + . cases x_initB <;> simp_all + . repeat cases ‹_ ∧ _›; subst_vars + rename_i H3 + cases H3 <;> rename_i H3 + . simp_all; apply Or.inl + cases newC + . rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . simp_all; apply Or.inr + cases newC + . rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . cases h3'; constructor <;> try rfl + . rename_i H1 H2 _ + simp at H1 + repeat cases ‹_ ∧ _› + subst_vars + cases H2; rename_i elem H2 + apply Exists.intro elem + intro h; specialize H2 h + rename_i B _ _ _ _ _ _ _ _ _ _ _ _ + cases B + . rename_i H1; simp at H1 + repeat cases ‹_ ∧ _› + subst_vars + cases h3 + rename_i h3 _ _ _ + simp at h3 + repeat cases ‹_ ∧ _› + subst_vars + simp_all only [List.map_cons, List.map_nil, List.append_assoc, List.cons_ne_self, + imp_false, not_true_eq_false] + . rename_i H1; simp at H1 + repeat cases ‹_ ∧ _› + subst_vars + cases h3 + rename_i h3 _ _ _ + simp at h3 + repeat cases ‹_ ∧ _› + subst_vars + cases newC + . rename_i h1 h2 h3 h4; clear h1 + rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rename_i h1 h2 h3 h4; clear h1 + rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rename_i H1 _ _ + simp at H1 + repeat cases ‹_ ∧ _› + subst_vars + assumption + . dsimp at h2 + obtain ⟨h2, _⟩ := h2 + specialize h2 rfl + obtain ⟨cons, newC, h⟩ := h2 + obtain ⟨x_bag'_int, ⟨x_initL'_int, x_initB'_int⟩, x_module'_int, ⟨x_splitD'_int, x_splitB'_int⟩ ,⟨x_branchD'_int, x_branchB'_int⟩, ⟨x_forkR'_int, x_forkL'_int⟩, x_muxB'_int, x_muxI'_int, x_muxC'_int⟩ := cons + dsimp at h + repeat cases ‹_ ∧ _› + subst_vars + rcases h3 with ⟨ h3, h3'⟩ + unfold lhsType at * + constructor + . cases h3 + rename_i h3 _ _ + constructor <;> try rfl + . cases h3 + . simp_all + . repeat cases ‹_ ∧ _› + subst_vars + simp_all + . cases h3 + . simp_all + . simp_all + . simp_all + repeat cases ‹_ ∧ _› + subst_vars + rename_i H3 + cases H3 <;> rename_i H3 + . apply Or.inl + cases newC + . rw[List.append_cons] at *; ac_nf at *; clear h3 h3' + aesop (config := {useDefaultSimpSet := false}) --(erase one_element1) + . rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . apply Or.inr + cases newC + . rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rw[List.append_cons] at *; ac_nf at *; clear ‹_ ∨ _› + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) --(erase one_element1) + . cases h3'; constructor <;> try rfl + . simp_all; rename_i H1 H2 _ + repeat cases ‹_ ∧ _› + subst_vars + cases H2; rename_i elem H2 + apply Exists.intro elem + intro h; specialize H2 h + rename_i B _ _ _ _ _ _ _ _ _ _ _ + cases B + . cases h3 + rename_i h3 _ _ _ + simp at h3 + repeat cases ‹_ ∧ _› + subst_vars; simp_all + cases newC + . rename_i h1 h2 h3 ; clear h1 + rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rename_i h1 h2 h3 ; clear h1 + rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . cases h3 + rename_i h3 _ _ _ + simp at h3 + repeat cases ‹_ ∧ _› + subst_vars; simp_all + cases newC + . rename_i h1 h2 h3 ; clear h1 + rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rename_i h1 h2 h3 ; clear h1 + rw[List.append_cons] at *; ac_nf at * + aesop (add safe (by contradiction)) (config := {useDefaultSimpSet := false}) + . rename_i H1 _ _ + simp at H1 + repeat cases ‹_ ∧ _› + subst_vars + simp_all + assumption + + + + + + + + + + +end Proof +end DataflowRewriter.LoopRewrite diff --git a/DataflowRewriter/Rewrites/LoopRewrite.lean b/DataflowRewriter/Rewrites/LoopRewrite.lean index 7352ce8..f5016f1 100644 --- a/DataflowRewriter/Rewrites/LoopRewrite.lean +++ b/DataflowRewriter/Rewrites/LoopRewrite.lean @@ -34,7 +34,7 @@ def lhs (T : Type) [Inhabited T] (Tₛ : String) (f : T → T × Bool) o_out [type = "io"]; mux [typeImp = $(⟨_, mux T⟩), type = $("mux " ++ Tₛ)]; - condition_fork [typeImp = $(⟨_, fork Bool 2⟩), type = "fork Bool 2"]; + condition_fork [typeImp = $(⟨_, fork2 Bool ⟩), type = "fork2 Bool"]; branch [typeImp = $(⟨_, branch T⟩), type = $("branch " ++ Tₛ)]; tag_split [typeImp = $(⟨_, split T Bool⟩), type = $("split " ++ Tₛ ++ " Bool")]; mod [typeImp = $(⟨_, pure f⟩), type = "pure f"]; diff --git a/DataflowRewriter/Rewrites/LoopRewriteCorrect.lean b/DataflowRewriter/Rewrites/LoopRewriteCorrect.lean index a265fab..e37eb1c 100644 --- a/DataflowRewriter/Rewrites/LoopRewriteCorrect.lean +++ b/DataflowRewriter/Rewrites/LoopRewriteCorrect.lean @@ -49,13 +49,13 @@ def environmentLhs : IdentMap String (TModule1 String) := lhs Data DataS f |>.sn def environmentRhs : IdentMap String (TModule1 String) := rhs Data DataS f |>.snd /-- -info: ["branch T", "pure f", "mux T", "fork Bool 2", "init Bool false", "split T Bool", "bag T"] +info: ["branch T", "pure f", "mux T", "init Bool false", "fork2 Bool", "split T Bool", "bag T"] -/ #guard_msgs in #eval @environmentLhs Unit "T" (λ _ => default) _ |>.keysList /-- -info: ["pure f", "merge T 2", "branch T", "split T Bool"] +info: ["pure f", "branch T", "split T Bool", "merge T 2"] -/ #guard_msgs in #eval @environmentRhs Unit "T" (λ _ => default) _ |>.keysList @@ -87,13 +87,13 @@ open Lean Meta Simp in @[drcompute] theorem find?_branch_data : (Batteries.AssocList.find? ("branch " ++ DataS) (environmentLhs DataS f)) = .some ⟨_, branch Data⟩ := sorry @[drcompute] theorem find?_pure_f : (Batteries.AssocList.find? ("pure f") (environmentLhs DataS f)) = .some ⟨_, pure f⟩ := sorry @[drcompute] theorem find?_mux_data : (Batteries.AssocList.find? ("mux " ++ DataS) (environmentLhs DataS f)) = .some ⟨_, mux Data⟩ := sorry -@[drcompute] theorem find?_fork_bool : (Batteries.AssocList.find? ("fork Bool 2") (environmentLhs DataS f)) = .some ⟨_, fork Bool 2⟩ := sorry +@[drcompute] theorem find?_fork_bool : (Batteries.AssocList.find? ("fork2 Bool") (environmentLhs DataS f)) = .some ⟨_, fork2 Bool⟩ := sorry @[drcompute] theorem find?_split_data : (Batteries.AssocList.find? ("split " ++ DataS ++ " Bool") (environmentLhs DataS f)) = .some ⟨_, split Data Bool⟩ := sorry @[drcompute] theorem find?_branch_data2 : (Batteries.AssocList.find? ("branch " ++ DataS) (environmentRhs DataS f)) = .some ⟨_, branch Data⟩ := sorry @[drcompute] theorem find?_pure_f2 : (Batteries.AssocList.find? ("pure f") (environmentRhs DataS f)) = .some ⟨_, pure f⟩ := sorry @[drcompute] theorem find?_merge_data2 : (Batteries.AssocList.find? ("merge " ++ DataS ++ " 2") (environmentRhs DataS f)) = .some ⟨_, merge Data 2⟩ := sorry -@[drcompute] theorem find?_fork_bool2 : (Batteries.AssocList.find? ("fork Bool 2") (environmentRhs DataS f)) = .some ⟨_, fork Bool 2⟩ := sorry +@[drcompute] theorem find?_fork_bool2 : (Batteries.AssocList.find? ("fork2 Bool") (environmentRhs DataS f)) = .some ⟨_, fork2 Bool⟩ := sorry @[drcompute] theorem find?_split_data2 : (Batteries.AssocList.find? ("split " ++ DataS ++ " Bool") (environmentRhs DataS f)) = .some ⟨_, split Data Bool⟩ := sorry def lhsTypeEvaled : Type := by @@ -115,12 +115,14 @@ def lhsTypeEvaled : Type := by #eval ([e| (rewriteLhsRhs "T").input_expr, environmentLhs "T" (λ _ => ((), true)) ]).outputs.keysList -set_option maxHeartbeats 0 in -def lhsEvaled : Module String - (List Data × +variable (Data) in +abbrev lhsType := (List Data × (List Bool × Bool) × List (Data × Bool) × - (List Data × List Bool) × (List Data × List Bool) × List Bool × List Data × List Data × List Bool) := by + (List Data × List Bool) × (List Data × List Bool) × (List Bool × List Bool) × List Data × List Data × List Bool) + +set_option maxHeartbeats 0 in +def lhsEvaled : Module String (lhsType Data) := by precomputeTac [e| (rewriteLhsRhs DataS).input_expr, environmentLhs DataS f ] by simp [drunfold,seval,drcompute,drdecide,-AssocList.find?_eq] rw [find?_bag_data,find?_init_data,find?_branch_data,find?_pure_f,find?_mux_data,find?_fork_bool,find?_split_data] @@ -141,9 +143,11 @@ def lhsEvaled : Module String unfold Module.connect'' dsimp +variable (Data) in +abbrev rhsType := (List (Data × Bool) × (List Data × List Bool) × List Data × List Data × List Bool) set_option maxHeartbeats 0 in -def rhsEvaled : Module String (List (Data × Bool) × (List Data × List Bool) × List Data × List Data × List Bool) := by +def rhsEvaled : Module String (rhsType Data) := by precomputeTac [e| (rewriteLhsRhs DataS).output_expr, environmentRhs DataS f ] by simp [drunfold,seval,drcompute,drdecide,-AssocList.find?_eq] rw [find?_branch_data2,find?_pure_f2,find?_split_data2,find?_merge_data2] @@ -162,6 +166,128 @@ def rhsEvaled : Module String (List (Data × Bool) × (List Data × List Bool) #print lhsEvaled +--Invariants + +-- def apply (n : Nat) (i : Data) : Data × Bool := +-- match n with +-- | 0 => f i +-- | n' + 1 => f (apply n' i).fst + +-- def iterate (i: Data) (n : Nat) (i': Data) : Prop := +-- (∀ m, m < n -> (apply f m i).snd = true) ∧ apply f n i = (i', false) + + +-- -- theorem compute_n (i : Data) : +-- -- ∃ n i', iterate f i n i' = true := by +-- -- constructor; constructor +-- -- . unfold iterate +-- -- simp +-- -- and_intros +-- -- . intro m h1 +-- -- unfold apply; + +-- omit [Inhabited Data] in +-- @[simp] +-- theorem input_rule_isData {input_rule} : +-- ((lhsEvaled f).inputs.find? ↑"i_in") = .some input_rule -> +-- Data = input_rule.fst := by +-- unfold lhsEvaled +-- simp; intro h1 +-- subst_vars; rfl + +-- #check lhsEvaled + + +-- -- theorem flushing (n : Nat) input_rule s i i' s' s_int +-- -- (h : ((lhsEvaled f).inputs.find? ↑"i_in") = .some input_rule) : +-- -- input_rule.snd s i s' -> +-- -- check_output f n (input_rule_isData f h i) i' -> +-- -- existSR (lhsEvaled f).internals s' s_int -> +-- -- ∃ s'', existSR (lhsEvaled f).internals s_int s'' ∧ s''.1 = i' := by admit + +-- --Invariant flush + + + +-- inductive flush_relation : lhsType Data -> Prop where +-- | intros : ∀ (s : lhsType Data) x_bag x_initL x_initB x_module x_splitD x_splitB x_branchD x_branchB x_forkR x_forkL x_muxB x_muxI x_muxC, +-- ⟨x_bag, ⟨x_initL, x_initB⟩, x_module, ⟨x_splitD, x_splitB⟩ ,⟨x_branchD, x_branchB⟩, ⟨x_forkR, x_forkL⟩, x_muxB, x_muxI, x_muxC ⟩ = s -> +-- (x_module.map Prod.fst ++ x_splitD ++ x_branchD ++ x_muxB = [] +-- ∨ +-- ∃ elem, x_module.map Prod.fst ++ x_splitD ++ x_branchD ++ x_muxB = [elem]) -> +-- (x_initB = true -> x_splitB ++ x_forkL ++ x_initL ++ x_muxC = []) -> +-- (x_initB = false -> ∃ elem, x_splitB ++ x_forkL ++ x_initL ++ x_muxC = [elem]) -> +-- flush_relation s + + +-- inductive computation_relation : (lhsType Data) -> (Data) -> Prop where +-- | intros : ∀ (s : lhsType Data) (i_in : Data) k n x_bag x_initL x_initB x_module x_splitD x_splitB x_branchD x_branchB x_forkR x_forkL x_muxB x_muxI x_muxC, +-- ⟨x_bag, ⟨x_initL, x_initB⟩, x_module, ⟨x_splitD, x_splitB⟩ ,⟨x_branchD, x_branchB⟩, ⟨x_forkR, x_forkL⟩, x_muxB, x_muxI, x_muxC ⟩ = s -> +-- (∃ elem, x_branchD = [elem] -> x_splitB ++ x_forkL ++ x_initL ++ x_muxC = [true]) -> +-- (∀ n i', iterate f i_in n i' -> +-- ( +-- k < n -> x_module = [(apply f k i_in )] ∧ x_module.map Prod.snd = [true] +-- ∧ +-- k = n -> x_module = [(apply f n i_in )] ∧ x_module.map Prod.snd = [false]) -> +-- x_splitB = [true] -> ∃ k, k < n ∧ x_splitD = [(apply f k i_in )].map Prod.fst -> +-- x_splitB = [false] -> ∃ k, k = n ∧ x_splitD = [(apply f k i_in )].map Prod.fst )-> +-- computation_relation s i_in + +-- inductive state_relation : lhsType Data -> Data -> Prop where +-- | base: ∀ (s : lhsType Data) i_in, +-- flush_relation s -> +-- computation_relation f s i_in -> +-- state_relation s i_in + + +-- #print lhsEvaled + + +-- theorem only_one_data_in_flight: +-- ∀ (s s' : lhsType Data) i_in rule, +-- rule ∈ (lhsEvaled f).internals -> +-- rule s s' -> +-- state_relation f s i_in -> +-- state_relation f s' i_in := by +-- intro s s' i_in rule h1 h2 h3 +-- let ⟨x_bag, ⟨x_initL, x_initB⟩, x_module, ⟨x_splitD, x_splitB⟩ ,⟨x_branchD, x_branchB⟩, ⟨x_forkR, x_forkL⟩, x_muxB, x_muxI, x_muxC ⟩ := s +-- let ⟨x_bag', ⟨x_initL', x_initB'⟩, x_module', ⟨x_splitD', x_splitB'⟩ ,⟨x_branchD', x_branchB'⟩, ⟨x_forkR', x_forkL'⟩, x_muxB', x_muxI', x_muxC'⟩ := s' +-- fin_cases h1 +-- . dsimp at h2 +-- obtain ⟨h2, _⟩ := h2 +-- specialize h2 rfl +-- obtain ⟨cons, newC, h⟩ := h2 +-- obtain ⟨x_bag'_int, ⟨x_initL'_int, x_initB'_int⟩, x_module'_int, ⟨x_splitD'_int, x_splitB'_int⟩ ,⟨x_branchD'_int, x_branchB'_int⟩, ⟨x_forkR'_int, x_forkL'_int⟩, x_muxB'_int, x_muxI'_int, x_muxC'_int⟩ := cons +-- dsimp at h +-- simp at * +-- rcases h with ⟨⟨⟨h4, ⟨h15, ⟨⟨h20, h26⟩, ⟨h21, h27⟩, ⟨h22, h28⟩, h23, h24, h25⟩⟩⟩, h5⟩ , ⟨⟨⟨⟨⟨⟨ h6, h13, h14⟩, ⟨h12, h17⟩⟩, ⟨h11, h16⟩⟩, ⟨h10, h18⟩⟩, h8⟩, ⟨h9, h19⟩⟩, h7⟩ +-- subst_vars +-- rcases h3 with ⟨ h3, h3'⟩ +-- constructor +-- . cases h3 +-- rename_i h3 _ _ +-- cases h3 +-- constructor +-- . rfl +-- . simp at *; rename_i H1 H2 H3 H4 +-- rcases H1 with ⟨_ ,⟨ _, _ , _ , _, _, _, _ ⟩⟩ +-- rename_i H5 H6 H7 H8 H9 H10 H11 H12 +-- cases H12; cases H10; cases H9; cases H8; cases H6; rcases H4 with ⟨ _, _, _ ⟩ +-- rename_i H; cases H +-- subst_vars + + + + + + + + + + + + + end Proof end DataflowRewriter.LoopRewrite diff --git a/DataflowRewriter/Rewrites/MatchGoal.lean b/DataflowRewriter/Rewrites/MatchGoal.lean new file mode 100644 index 0000000..45ca947 --- /dev/null +++ b/DataflowRewriter/Rewrites/MatchGoal.lean @@ -0,0 +1,231 @@ +import Lean +import Leanses + +open Lean +open Leanses +open Lean Elab Meta Tactic + +namespace matchGoal + + +/-- +Tactic to specialize all the hypotheses in the context that contain a binding +of that term. +-/ +syntax (name := specializeAll) "specializeAll " term : tactic + +-- We use a structure storage to save the state of our bounded vars +structure Storage where + bef : Array Expr + aft : Array Expr + +-- We use these auxiliary methods to create and set the content of our storage +def globalStorageRef : IO (IO.Ref Storage) := + IO.mkRef { bef := #[], aft := #[]} + +def setStorage (ref : IO.Ref Storage) (vars : Array Expr) (index : Array Expr): IO Unit := do + ref.set { bef := vars, aft := index} + +@[tactic specializeAll] def specializeAllTactic : Tactic -- Syntax -> TacticM Unit + | `(tactic| specializeAll $t:term) => withMainContext do + let ref <- globalStorageRef + let t ← elabTerm t none + let termType ← inferType t + let lctx ← getLCtx + lctx.forM fun decl : LocalDecl => do + if decl.isImplementationDetail then return () + if (← forallTelescopeReducing decl.type fun vars _ => do + if vars.size > 0 then + -- we identify which variable needs to be specialized and save + -- all other bounded variables + let mut bef : Array Expr := #[] + let mut aft : Array Expr := #[] + for i in [0:vars.size] do + let varType ← inferType vars[i]! + if (← isDefEq varType termType) then + for j in [i+1:vars.size] do + aft := aft.push vars[j]! + setStorage ref bef aft + return true + else + bef := bef.push vars[i]! + return false + ) + -- We don't want to instantiate arrow types (only dependent types). + && decl.type.arrow?.isNone + then + let var <- ref.get + -- We unbind the bvars before the var to be specialized, apply it, then + -- bind it again with mkLambdaFvars + let e ← forallBoundedTelescope decl.type var.bef.size fun fvars _ => do + let y <- mkAppM' (mkAppN decl.toExpr fvars) #[t] + mkLambdaFVars fvars y + -- We create a new assertion in the current goal and also infer the type + -- of `e` again. Instead we could generate the correct type as well. + let mvarId ← (← getMainGoal).assert decl.userName (← inferType e).headBeta e + let (_, mvarId) ← mvarId.intro1P + let mvarId ← mvarId.tryClear decl.fvarId + replaceMainGoal [mvarId] + else + return () + | _ => throwUnsupportedSyntax + +------------------- TESTS ----------------------- + +theorem sp_a : (∀ a b c : Bool, a /\ b /\ c) -> false := by + intros + specializeAll false + sorry + +theorem sp_b : (∀ a : Nat, ∀ b c : Bool, (a = 1) /\ b /\ c) -> false := by + intros + specializeAll true + sorry + +theorem sp_c : (∀ a b : Nat, ∀ c : Bool, (a = 1) /\ (b = 2) /\ c) -> false := by + intros + specializeAll false + sorry +------------------- END ----------------------- + + +/-- +Tactic to match a hypothesis in the context with its pattern before applying +a given tactic to the goal. +-/ + +syntax (name := matchGoal) "matchGoal" sepBy1("("sepBy1(ident " : " term, ",") ")" "("term")" "("tactic")", "|") : tactic + +@[tactic matchGoal] +def matchGoalTactic : Tactic + | `(tactic| matchGoal $[($[$ids:ident : $patts:term],*) ($goal:term) ($tac:tactic)]|*) => withMainContext do + -- we zip all our args together to have a clause tuple with hypothesis patterns, goal pattern, and tactics to try + let clauses := (List.zip (List.zip (List.zip ids.toList patts.toList) goal.toList) tac.toList).map (λ (((ids, patts), goal), tac) => (ids, patts, goal, tac)) + -- we iterate over each clause to match its patterns and apply its tactics if applicable + for (ids, patts, goal, tac) in clauses do + -- we save state in case no pattern is found and an exception is thrown + let original <- saveState + -- we catch any terminating error for the currently inspected clause + try{ + -- we use an hashset to store previously matched patterns + let fk <- IO.mkRef (HashSet.empty : HashSet FVarId) + + let fvarIds <- (ids.zip patts).mapM fun (id, patt) => do + -- we try to find our matching hypothesis without modifying the state of our goal + let fvarId ← withoutModifyingState do + -- we create a new metavar context depth to try different assignments and try to match them to our hypothesis + let fvarId? ← (← getLCtx).findDeclRevM? fun localDecl => withNewMCtxDepth do + -- we elab our term + let hypPatt ← elabTerm patt none + -- we check if we previously matched that hypothesis + let fkarr <- fk.get + if fkarr.contains localDecl.fvarId then + return none + -- we try to assign its metavars with our localdecl + if (← withAssignableSyntheticOpaque <| isDefEq hypPatt localDecl.type) then + return some localDecl.fvarId + else + return none + -- at the end of our iteration, we throw an error if no matching type or return the id of the fvar matched + match fvarId? with + | none => throwError "failed to match hyps to patt {indentExpr (<- elabTerm patt none)}" + | some fvarId => + fk.modify fun f => f.insert fvarId + return fvarId + return (id, fvarId) + + -- we get the old username for renaming purposes + let names <- fvarIds.mapM fun (id, fvar) => do + -- we rename the matched pattern if needed (it is not a single metavar) + replaceMainGoal [← (← getMainGoal).rename fvar id.getId] + return (id, fvar, fvar.getUserName) + + -- we pattern match on the current goal to see if we can apply the tactics (similar to above) + let patt <- withoutModifyingState do + withNewMCtxDepth do + let goalPatt ← elabTerm goal none + let goalType <- (<- getMainGoal).getType + if (← withAssignableSyntheticOpaque <| isDefEq goalPatt goalType) then + return some (<- getMainGoal) + return none + match patt with + | none => throwError "failed to match pattern to curr goal {indentExpr (<- elabTerm goal none)}" + | some _ => + -- if the goal pattern matched the current goal, we try to eval the tactic + evalTactic tac + -- if no exception is thrown and a goal still exists we rename the variables and return + if(<- getUnsolvedGoals).isEmpty then return + (← getLCtx).findDeclRevM? fun localDecl => do + let bgg? <- names.mapM fun (_, _, name) => do + if ((<- name) == (<- localDecl.fvarId.getUserName)) then + for goal in (<- getUnsolvedGoals).reverse do + let i <- goal.rename localDecl.fvarId (<- name) + appendGoals [i] + return some localDecl.fvarId + else + return none + match bgg? with + | _ => pure (none : Option FVarId) + return + } + -- if we have a terminating error, we restore state and move to next clause + catch _ => + restoreState original + -- if no clause evaluation succeeded, we throw an error + throwError "No pattern found or tactic failed" + | _ => throwUnsupportedSyntax + + +-------- TESTS ------------ + +example α : + False → α := by + intros; matchGoal(h : False) (_) (cases h) + +example α : + False → α := by + intros; matchGoal(h : True, v : _) (_) (cases h) | (h : False) (_) (cases h) + + +example : + True := by + intros; matchGoal (h : ?a) (True) (constructor) + +example: + True ∧ True := by + repeat matchGoal (h : _) (?a ∧ ?b) (constructor) | (h : _) (_) (constructor) + +-- not in the right order to show that it doesn't matter, no failure +example (b: Bool) (v : b) : + True -> False ∨ b := by + repeat matchGoal (h : _) (?a ∨ ?b) (right) | (h :_) (_ -> _) (intros) | (k : _ = true)(_)(exact k) + +example (a b c d: Bool) (j: c = false)(k : a = true)(g : b = true): + (a ∧ b) ∨ (c ∧ d) := by + repeat matchGoal (l : _ = true, v: _ = true) (_ ∧ _) (apply And.intro v l) | (r : _) (_ ∨_) (constructor) + +-- we add the middle pattern to show if tactic fails it doesn't stop exec +example a b c d : + a ∧ b -> c ∨ d -> a ∧ b := by + repeat matchGoal (h: _) (_ -> _) (intros) | (h: _ ∨ _) (_) (exact h) | (h: _ ∧ _) (_) (exact h) + +theorem sp_a_m : (∀ a b c : Bool, a /\ b /\ c) -> false := by + intros + matchGoal(h : ∀ _ : Bool, _)(_)(specialize h false) + sorry + +theorem sp_b_m : (∀ a : Nat, ∀ b c : Bool, (a = 1) ∧ b /\ c) -> (z : Bool) -> True := by + intros + matchGoal(h : ∀ _ (_ : ?b) _, _, q : ?b)(_)(replace h := fun a c => h a q c) + + trivial + +theorem sp_c_m : (∀ a b : Nat, ∀ c : Bool, (a = 1) /\ (b = 2) /\ c) -> false := by + intros + matchGoal (h : ∀ _ _ (_ : Bool), _, z : _) (_) (replace h := fun a b => h a b false) + sorry + +------------------- END ----------------------- + +theorem s : ∀ (y : True) (h : False) (z : True), False := by + matchGoal (h : ?f) (?f) (apply h) diff --git a/DataflowRewriter/Rewrites/MuxTaggedRewriteCorrect.lean b/DataflowRewriter/Rewrites/MuxTaggedRewriteCorrect.lean index 04d7e3e..320b691 100644 --- a/DataflowRewriter/Rewrites/MuxTaggedRewriteCorrect.lean +++ b/DataflowRewriter/Rewrites/MuxTaggedRewriteCorrect.lean @@ -180,7 +180,7 @@ attribute [dmod] Batteries.AssocList.find? BEq.beq -- def φ {Tag T} (state_rhs : rhsModuleType Tag T) (state_lhs : lhs_intModuleType Tag T) : Prop := --- let ⟨⟨x_branch_tag, x_branchC ⟩, x_fork, ⟨x_muxT, x_muxF, x_muxC⟩, ⟨x_join1_l, x_join1_r⟩, ⟨x_join2_l, x_join2_r⟩⟩ := state_rhs +-- omit [Inhabited Data] in theorem -- let ⟨⟨y_join_tag, y_join_r⟩, ⟨y_muxT, y_muxF, y_muxC⟩⟩ := state_lhs -- x_muxT.map Prod.snd ++ x_join1_r = List.map Prod.fst (List.filter (fun x => x.2 == true) y_join_r) ++ y_muxT ∧ -- x_muxF.map Prod.snd ++ x_join2_r = List.map Prod.fst (List.filter (fun x => x.2 == false) y_join_r) ++ y_muxF ∧