Use dependent rewrites to reason about build_module'

DataflowRewriter/AssocList.lean

@@ -11,7 +11,7 @@ namespace Batteries.AssocList
 def append {α β} (a b : AssocList α β) : AssocList α β :=
   match a with
   | .nil => b
-  | .cons x y xs => 
+  | .cons x y xs =>
     .cons x y <| xs.append b
 
 def modifyKeys {α β} (map : AssocList α β) (f : α → α) : AssocList α β :=
@@ -23,4 +23,29 @@ def keysList {α β} (map : AssocList α β) : List α :=
 def filter {α β} (f : α → β → Bool) (l : AssocList α β) :=
   l.foldl (λ c a b => if f a b then c.cons a b else c) (∅ : AssocList α β)
 
+def mem {α β} [BEq α] (a : α) (b : β) (l : AssocList α β) : Prop :=
+  l.find? a = some b
+
+private theorem map_keys_list' {α β γ} [DecidableEq α] {f : α → β → γ} {l : List (α × β)} {ident val} :
+  List.find? (fun x => x.fst == ident) l = some val →
+  List.find? ((fun x => x.fst == ident) ∘ fun x => (x.fst, f x.fst x.snd)) l = some (ident, val.snd) := by
+  induction l generalizing ident val <;> simp_all
+  rename_i head tail iH
+  intro Hfirst
+  rcases Hfirst with ⟨ h1, h2 ⟩ | ⟨ h1, h2 ⟩
+  subst_vars; left; simp
+  right; and_intros; assumption
+  apply iH
+  assumption
+
+theorem map_keys_list {α β γ} [DecidableEq α] {ident} {l : AssocList α β} {f : α → β → γ} :
+    (l.mapVal f).find? ident = (l.find? ident).map (f ident) := by
+  simp [find?_eq]
+  cases h : List.find? (fun x => x.fst == ident) l.toList <;> simp_all
+  · assumption
+  · rename_i val
+    refine ⟨ ident, val.snd, ?_ ⟩
+    and_intros <;> try rfl
+    apply map_keys_list'; assumption
+
 end Batteries.AssocList

DataflowRewriter/ExprLow.lean

@@ -6,6 +6,7 @@ Authors: Yann Herklotz
 
 import DataflowRewriter.Module
 import DataflowRewriter.Simp
+import DataflowRewriter.HVector
 
 namespace DataflowRewriter
 
@@ -33,32 +34,96 @@ namespace ExprLow
 variable {Ident}
 variable [DecidableEq Ident]
 
-@[drunfold] def build_module' (ε : IdentMap Ident ((T: Type _) × Module Ident T))
-    : ExprLow Ident → Option ((T: Type _) × Module Ident T)
-  | .base i e => do
-    let mod ← ε.find? e
-    return ⟨ mod.1, mod.2.renamePorts (λ ⟨ _, y ⟩ => ⟨ .internal i, y ⟩ ) ⟩
+def get_types (ε : IdentMap Ident (Σ T, Module Ident T)) (i : Ident) : Type* :=
+  (ε.find? i) |>.map Sigma.fst |>.getD PUnit
+
+def ident_list : ExprLow Ident → List Ident
+  | .base i e => [e]
+  | .input _ _ e
+  | .output _ _ e
+  | .connect _ _ e => e.ident_list
+  | .product a b => a.ident_list ++ b.ident_list
+
+abbrev EType ε (e : ExprLow Ident) := (HVector (get_types ε) e.ident_list)
+
+@[drunfold] def build_module' (ε : IdentMap Ident ((T: Type) × Module Ident T))
+    : (e : ExprLow Ident) → Option (Module Ident (EType ε e))
+  | .base i e =>
+    match h : ε.find? e with
+    | some mod =>
+      have H : mod.1 = get_types ε e := by
+        simp [Batteries.AssocList.find?_eq] at h
+        rcases h with ⟨ l, r ⟩
+        simp_all [get_types]
+      some ((H ▸ mod.2).liftD)
+    | none => none
   | .input a b e' => do
     let e ← build_module' ε e'
-    return ⟨ e.1, e.2.renameToInput (λ p => if p == a then ⟨ .top, b ⟩ else p) ⟩
+    return e.renameToInput (λ p => if p == a then ⟨ .top, b ⟩ else p)
   | .output a b e' => do
     let e ← build_module' ε e'
-    return ⟨ e.1, e.2.renameToOutput (λ p => if p == a then ⟨ .top, b ⟩ else p) ⟩
+    return e.renameToOutput (λ p => if p == a then ⟨ .top, b ⟩ else p)
   | .connect o i e' => do
     let e ← build_module' ε e'
-    return ⟨e.1, e.2.connect' o i⟩
+    return e.connect' o i
   | .product a b => do
-    let a <- build_module' ε a;
-    let b <- build_module' ε b;
-    return ⟨a.1 × b.1, a.2.product b.2⟩
+    let a ← build_module' ε a;
+    let b ← build_module' ε b;
+    return a.productD b
 
-@[drunfold] def build_module (ε : IdentMap Ident (Σ (T : Type _), Module Ident T))
+@[drunfold] def build_moduleP (ε : IdentMap Ident (Σ T, Module Ident T))
     (e : ExprLow Ident)
     (h : (build_module' ε e).isSome = true := by rfl)
-    : (T : Type _) × Module Ident T := build_module' ε e |>.get h
+    : Module Ident (EType ε e) := build_module' ε e |>.get h
 
-theorem build_module_modify {ε : IdentMap Ident (Σ (T : Type), Module Ident T)} {expr} {m : (Σ (T : Type), Module Ident T)} {i : Ident} :
-  (build_module' ε expr).isSome → (build_module' (ε.modify i (λ _ _ => m)) expr).isSome := by sorry
+@[drunfold] def build_module (ε : IdentMap Ident (Σ T, Module Ident T))
+    (e : ExprLow Ident)
+    : Module Ident (EType ε e) := build_module' ε e |>.getD Module.empty
+
+@[drunfold] abbrev build_module_expr (ε : IdentMap Ident (Σ T, Module Ident T))
+    (e : ExprLow Ident)
+    : Module Ident (EType ε e) := build_module ε e
+
+notation:25 "[e| " e ", " ε " ]" => build_module_expr ε e
+notation:25 "[T| " e ", " ε " ]" => EType ε e
+
+-- theorem build_module_replace {ε : IdentMap Ident (Σ (T : Type), Module Ident T)} {expr} {m : (Σ (T : Type), Module Ident T)} {i : Ident} :
+--   (build_module' ε expr).isSome → (build_module' (ε.replace i m) expr).isSome := by sorry
+
+def _root_.DataflowRewriter.IdentMap.replace_env (ε : IdentMap Ident (Σ (T : Type _), Module Ident T)) {ident mod}
+  (h : ε.mem ident mod) mod' :=
+  (ε.replace ident mod')
+
+notation:25 "{" ε " | " h " := " mod' "}" => IdentMap.replace_env ε h mod'
+
+theorem find?_modify {modIdent ident m m'} {ε : IdentMap Ident (Σ (T : Type _), Module Ident T)}
+  (h : ε.mem ident m') :
+  Batteries.AssocList.find? modIdent ε = none →
+  Batteries.AssocList.find? modIdent ({ε | h := m}) = none := by sorry
+
+instance
+  {ε : IdentMap Ident (Σ (T : Type _), Module Ident T)}
+  {S ident iexpr} {mod : Σ T : Type _, Module Ident T}
+  {mod' : Σ T : Type _, Module Ident T} {smod : Module Ident S}
+  {h : ε.mem ident mod}
+  [MatchInterface mod.2 mod'.2]
+  [MatchInterface ([e| iexpr, ε ]) smod]
+  : MatchInterface ([e| iexpr, {ε | h := mod'} ]) smod := by sorry
+
+theorem build_module'.dep_rewrite {instIdent} : ∀ {modIdent : Ident} {ε a} (Hfind : ε.find? modIdent = a), (Option.rec (motive := fun x =>
+          Batteries.AssocList.find? modIdent ε = x →
+            Option (Module Ident ([T| base instIdent modIdent, ε ])))
+          (fun h_1 => none)
+          (fun val h_1 => some (build_module'.proof_2 ε modIdent val h_1 ▸ val.snd).liftD)
+          (Batteries.AssocList.find? modIdent ε)
+          (Eq.refl (Batteries.AssocList.find? modIdent ε))) =
+        (Option.rec (motive := fun x =>
+            a = x →
+              Option (Module Ident ([T| base instIdent modIdent, ε ])))
+            (fun h_1 => none)
+            (fun val h_1 => some (build_module'.proof_2 ε modIdent val (Hfind ▸ h_1) ▸ val.snd).liftD)
+            a
+            (Eq.refl a)) := by intro a b c d; cases d; rfl
 
 section Refinement
 
@@ -68,31 +133,47 @@ variable {Ident : Type w}
 variable [DecidableEq Ident]
 variable [Inhabited Ident]
 
-variable (ε : IdentMap Ident ((T : Type) × Module Ident T))
-variable (iexpr : ExprLow Ident)
-variable (hiexpr : (build_module' ε iexpr).isSome)
+variable (ε : IdentMap Ident ((T : Type _) × Module Ident T))
 
 variable {S : Type v}
 variable (smod : Module Ident S)
 
-variable [MatchInterface (build_module ε iexpr hiexpr).2 smod]
-
-def refines_φ (R : (build_module ε iexpr hiexpr).1 → S → Prop) :=
-  (build_module ε iexpr hiexpr).2 ⊑_{R} smod
-
-def refines := ∃ R, (build_module ε iexpr hiexpr).2 ⊑_{R} smod
-
-notation:35 x " ⊑ₑ_{" f:35 "} " y:34 => refines_φ x y f
-notation:35 x " ⊑ₑ " y:34 => refines x y
-
-theorem substitution {T ident mod} {mod' : Module Ident T}
-        [MatchInterface (build_module (ε.modify ident (λ _ _ => ⟨T, mod'⟩)) iexpr (build_module_modify hiexpr)).2 smod]
-        [MatchInterface mod mod']
-        (R : (build_module ε iexpr hiexpr).1 → S → Prop) :
-  (build_module ε iexpr hiexpr).2 ⊑ smod →
-  ε.find? ident = some ⟨ T, mod ⟩ →
-  mod ⊑ mod' →
-  (build_module (ε.modify ident (λ _ _ => ⟨T, mod'⟩)) iexpr (build_module_modify hiexpr)).2 ⊑ smod := by sorry
+#check Option.rec
+
+-- set_option debug.skipKernelTC true in
+set_option pp.proofs true in
+set_option pp.deepTerms true in
+variable {T T'}
+         {mod : Module Ident T}
+         {mod' : Module Ident T'}
+         [MatchInterface mod mod'] in
+theorem substitution (iexpr : ExprLow Ident)
+        (_ : MatchInterface ([e| iexpr, ε ]) smod)
+        {ident} (h : ε.mem ident ⟨ T, mod ⟩) :
+    mod ⊑ mod' →
+    [e| iexpr, ε ] ⊑ smod →
+    [e| iexpr, {ε | h := ⟨ T', mod' ⟩} ] ⊑ smod := by
+  unfold build_module_expr
+  induction iexpr with
+  | base instIdent modIdent =>
+    intro Hmod Hbase
+    dsimp [build_module_expr, build_module, build_module']
+    cases Hfind : ((Batteries.AssocList.find? modIdent ε)) with
+    | none =>
+      have Hfind' := find?_modify (m := ⟨T', mod'⟩) h Hfind
+      unfold DataflowRewriter.ExprLow.build_module'.match_1
+      simp only [build_module'.dep_rewrite Hfind', Option.getD]
+      rename_i Match
+      dsimp [build_module_expr, build_module, build_module'] at Hbase Match
+      unfold DataflowRewriter.ExprLow.build_module'.match_1 at Hbase Match
+      simp [build_module'.dep_rewrite Hfind] at Hbase Match
+      apply Module.empty_refines
+      assumption
+    | some curr_mod => sorry
+  | input iport name e iH => sorry
+  | output iport name e iH => sorry
+  | product e₁ e₂ iH₁ iH₂ => sorry
+  | connect p1 p2 e iH => sorry
 
 end Refinement
 

DataflowRewriter/Module.lean

@@ -11,6 +11,7 @@ import Qq
 import DataflowRewriter.Simp
 import DataflowRewriter.List
 import DataflowRewriter.AssocList
+import DataflowRewriter.HVector
 
 open Batteries (AssocList)
 
@@ -137,11 +138,13 @@ The empty module, which should also be the `default` module.
 
 theorem empty_is_default {Ident S} : @empty Ident S = default := Eq.refl _
 
-variable {Ident : Type _}
+universe i
+
+variable {Ident : Type i}
 variable [DecidableEq Ident]
 variable [Inhabited Ident]
 
-@[drunfold] def liftL {S S'} (x: (T : Type _) × (S → T → S → Prop))
+@[drunfold] def liftL {S S' : Type _} (x: (T : Type _) × (S → T → S → Prop))
     : (T : Type _) × (S × S' → T → S × S' → Prop) :=
   ⟨ x.1, λ (a,b) ret (a',b') => x.2 a ret a' ∧ b = b' ⟩
 
@@ -155,6 +158,30 @@ variable [Inhabited Ident]
 @[drunfold] def liftR' {S S'} (x:  S' → S' → Prop) : S × S' → S × S' → Prop :=
   λ (a,b) (a',b') => x b b' ∧ a = a'
 
+@[drunfold] def liftLD {α : Type _} {l₁ l₂ : List α} {f} (x: (T : Type _) × (HVector f l₁ → T → HVector f l₁ → Prop))
+    : (T : Type _) × (HVector f (l₁ ++ l₂) → T → HVector f (l₁ ++ l₂) → Prop) :=
+  ⟨ x.1, λ a ret a' => x.2 a.left ret a'.left ∧ a.right = a'.right ⟩
+
+@[drunfold] def liftRD {α : Type _} {l₁ l₂ : List α} {f} (x: (T : Type _) × (HVector f l₂ → T → HVector f l₂ → Prop))
+    : (T : Type _) × (HVector f (l₁ ++ l₂) → T → HVector f (l₁ ++ l₂) → Prop) :=
+  ⟨ x.1, λ a ret a' => x.2 a.right ret a'.right ∧ a.left = a'.left ⟩
+
+@[drunfold] def liftLD' {α : Type _} {l₁ l₂ : List α} {f} (x: HVector f l₁ → HVector f l₁ → Prop)
+    : HVector f (l₁ ++ l₂) → HVector f (l₁ ++ l₂) → Prop :=
+  λ a a' => x a.left a'.left ∧ a.right = a'.right
+
+@[drunfold] def liftRD' {α : Type _} {l₁ l₂ : List α} {f} (x: HVector f l₂ → HVector f l₂ → Prop)
+    : HVector f (l₁ ++ l₂) → HVector f (l₁ ++ l₂) → Prop :=
+  λ a a' => x a.right a'.right ∧ a.left = a'.left
+
+@[drunfold] def liftSingle.{u} {α} {a : α} {f} (x: Σ (T : Type u), (f a → T → f a → Prop))
+    : Σ (T : Type u), HVector f [a] → T → HVector f [a] → Prop :=
+  ⟨ x.1, λ | .cons a .nil, t, .cons a' .nil => x.2 a t a' ⟩
+
+@[drunfold] def liftSingle' {α} {a : α} {f} (x: f a → f a → Prop)
+    : HVector f [a] → HVector f [a] → Prop :=
+  λ | .cons a .nil, .cons a' .nil => x a a'
+
 /--
 `connect'` will produce a new rule that fuses an input with an output, with a
 precondition that the input and output type must match.
@@ -175,7 +202,19 @@ precondition that the input and output type must match.
     internals := mod1.internals.map liftL' ++ mod2.internals.map liftR'
   }
 
-@[drunfold] def renamePorts {S} (mod : Module Ident S) (f : InternalPort Ident → InternalPort Ident) : Module Ident S :=
+@[drunfold] def productD {α} {l₁ l₂ : List α} {f} (mod1 : Module Ident (HVector f l₁)) (mod2: Module Ident (HVector f l₂)) : Module Ident (HVector f (l₁ ++ l₂)) :=
+  { inputs := (mod1.inputs.mapVal (λ _ => liftLD)).append (mod2.inputs.mapVal (λ _ => liftRD)),
+    outputs := (mod1.outputs.mapVal (λ _ => liftLD)).append (mod2.outputs.mapVal (λ _ => liftRD)),
+    internals := mod1.internals.map liftLD' ++ mod2.internals.map liftRD'
+  }
+
+@[drunfold] def liftD {α} {e : α} {f} (mod : Module Ident (f e)) : Module Ident (HVector f [e]) :=
+  { inputs := mod.inputs.mapVal λ _ => liftSingle,
+    outputs := mod.outputs.mapVal λ _ => liftSingle,
+    internals := mod.internals.map liftSingle'
+  }
+
+@[drunfold] def renamePorts {S : Type _} (mod : Module Ident S) (f : InternalPort Ident → InternalPort Ident) : Module Ident S :=
   { inputs := mod.inputs.modifyKeys f,
     outputs := mod.outputs.modifyKeys f,
     internals := mod.internals
@@ -195,21 +234,31 @@ precondition that the input and output type must match.
 
 end Module
 
+section Match
+
 /-
 The following definition lives in `Type`, I'm not sure if a type class can live
 in `Prop` even though it seems to be accepted.
 -/
 
-variable {Ident} [DecidableEq Ident] [Inhabited Ident] in
+variable {Ident}
+variable [DecidableEq Ident]
+variable {I S}
 
 /--
 Match two interfaces of two modules, which implies that the types of all the
 input and output rules match.
 -/
-class MatchInterface {I S} (imod : Module Ident I) (smod : Module Ident S) where
+class MatchInterface (imod : Module Ident I) (smod : Module Ident S) : Prop where
   input_types : ∀ (ident : Ident), (imod.inputs.getIO ident).1 = (smod.inputs.getIO ident).1
   output_types : ∀ (ident : Ident), (imod.outputs.getIO ident).1 = (smod.outputs.getIO ident).1
 
+theorem match_interface_empty {smod : Module Ident S} [MatchInterface (@Module.empty Ident I) smod]
+  : ∀ I', MatchInterface (@Module.empty Ident I') smod := sorry
+
+end Match
+
+
 /--
 State that there exists zero or more internal rule executions to reach a final
 state from an initial state.
@@ -282,14 +331,13 @@ def refines_φ (R : I → S → Prop) :=
     R init_i init_s →
     comp_refines imod smod R init_i init_s
 
+notation:35 x " ⊑_{" R:35 "} " y:34 => refines_φ x y R
+
+omit mm in
 def refines :=
-  ∃ (R : I → S → Prop),
-    ∀ (init_i : I) (init_s : S),
-      R init_i init_s →
-      indistinguishable imod smod init_i init_s →
-      comp_refines imod smod (fun a b => indistinguishable imod smod a b ∧ R a b) init_i init_s
+  ∃ (mm : MatchInterface imod smod) (R : I → S → Prop),
+    imod ⊑_{fun x y => indistinguishable imod smod x y ∧ R x y} smod
 
-notation:35 x " ⊑_{" R:35 "} " y:34 => refines_φ x y R
 notation:35 x " ⊑ " y:34 => refines x y
 
 omit [Inhabited Ident] in
@@ -298,22 +346,27 @@ theorem refines_φ_refines {φ} :
   imod ⊑_{φ} smod →
   imod ⊑ smod := by
   intro Hind Href
-  exists φ
-  intro init_i init_s Hphi Hindis
-  specialize Href init_i init_s Hphi
-  rcases Href with ⟨ Hin, Hout, Hint ⟩; constructor
-  · intro ident mid_i v Hcont Hrule
-    specialize Hin ident mid_i v Hcont Hrule
-    tauto
-  · intro ident mid_i v Hcont Hrule
-    specialize Hout ident mid_i v Hcont Hrule
-    tauto
-  · intro rule mid_i Hcont Hrule
-    specialize Hint rule mid_i Hcont Hrule
-    tauto
+  -- exists φ
+  -- intro init_i init_s ⟨ Hphi, Hindis ⟩
+  -- specialize Href init_i init_s Hindis
+  -- rcases Href with ⟨ Hin, Hout, Hint ⟩; constructor
+  -- · intro ident mid_i v Hcont Hrule
+  --   specialize Hin ident mid_i v Hcont Hrule
+  --   tauto
+  -- · intro ident mid_i v Hcont Hrule
+  --   specialize Hout ident mid_i v Hcont Hrule
+  --   tauto
+  -- · intro rule mid_i Hcont Hrule
+  --   specialize Hint rule mid_i Hcont Hrule
+  --   tauto
+  sorry
 
 end Refinement
 
+theorem empty_refines {Ident S I₁ I₂} [DecidableEq Ident] {smod : Module Ident S} :
+  @empty Ident I₁ ⊑ smod →
+  @empty Ident I₂ ⊑ smod := by sorry
+
 end Module
 
 instance {n} : OfNat (InstIdent Nat) n where