Theory Examples_Compiler

section ‹Compiler-style equality-saturation certificates›

theory Examples_Compiler
  imports
    EGraph_Explanations
    Extraction_Certificates
    Bounded_Certificate_Search
begin

datatype csym = CMul | CAdd | CShl | COne | CTwo
datatype cvar = VX | VY

abbreviation (input) cmul ::
  "(csym, cvar) term ⇒ (csym, cvar) term ⇒ (csym, cvar) term"
  (infixl ‹⊗› 70) where
  "a ⊗ b ≡ Fun CMul [a, b]"

abbreviation (input) cadd ::
  "(csym, cvar) term ⇒ (csym, cvar) term ⇒ (csym, cvar) term"
  (infixl ‹⊕› 65) where
  "a ⊕ b ≡ Fun CAdd [a, b]"

abbreviation (input) cshl ::
  "(csym, cvar) term ⇒ (csym, cvar) term ⇒ (csym, cvar) term"
  (infixl ‹≪› 60) where
  "a ≪ b ≡ Fun CShl [a, b]"

abbreviation (input) cone :: "(csym, cvar) term" where
  "cone ≡ Fun COne []"
abbreviation (input) ctwo :: "(csym, cvar) term" where
  "ctwo ≡ Fun CTwo []"
abbreviation (input) vx :: "(csym, cvar) term" where
  "vx ≡ Var VX"
abbreviation (input) vy :: "(csym, cvar) term" where
  "vy ≡ Var VY"

definition R_comp :: "(csym, cvar) rule list" where
  "R_comp =
    [ (vx ⊗ ctwo, vx ⊕ vx)
    , (vx ≪ cone, vx ⊕ vx) ]"

subsection ‹Positional rule explanations›

definition t_strength :: "(csym, cvar) term" where
  "t_strength = (vx ≪ cone) ⊕ (vy ⊗ ctwo)"

definition u_strength :: "(csym, cvar) term" where
  "u_strength = (vx ⊕ vx) ⊕ (vy ⊕ vy)"

definition strength_steps :: "(csym, cvar) certificate_step list" where
  "strength_steps =
    [ Rule_At [0] 1 Forward Var
    , Rule_At [Suc 0] 0 Forward
        (λv. if v = VX then vy else Var v) ]"

lemma strength_certificate:
  "check_explanation R_comp [] strength_steps t_strength u_strength"
  by (simp add: check_explanation_def R_comp_def strength_steps_def
      t_strength_def u_strength_def)

theorem strength_reduction_conversion:
  "(t_strength, u_strength) ∈ (rstep (set R_comp))⇧↔⇧*"
  by (rule check_rule_explanation_sound[OF strength_certificate])

subsection ‹Chronological merge reuse›

definition compiler_log :: "(csym, cvar) merge_log" where
  "compiler_log =
    [ ((vx ⊗ ctwo, vx ⊕ vx),
        [Rule_At [] 0 Forward Var])
    , ((vy ⊗ ctwo, vy ⊕ vy),
        [Rule_At [] 0 Forward
          (λv. if v = VX then vy else Var v)]) ]"

lemma compiler_log_accepted:
  "check_merge_log R_comp compiler_log"
  by (simp add: check_merge_log_def compiler_log_def
      check_explanation_def R_comp_def)

definition t_merge :: "(csym, cvar) term" where
  "t_merge = (vx ⊗ ctwo) ⊕ (vy ⊗ ctwo)"

definition u_merge :: "(csym, cvar) term" where
  "u_merge = (vx ⊕ vx) ⊕ (vy ⊕ vy)"

definition merge_reuse_steps :: "(csym, cvar) certificate_step list" where
  "merge_reuse_steps =
    [ Merge_At [0] 0 Forward
    , Merge_At [Suc 0] 1 Forward ]"

lemma merge_reuse_accepted:
  "check_explanation R_comp (recorded_merges compiler_log)
     merge_reuse_steps t_merge u_merge"
  by (simp add: check_explanation_def recorded_merges_def compiler_log_def
      merge_reuse_steps_def t_merge_def u_merge_def)

theorem recorded_merges_are_reusable:
  "(t_merge, u_merge) ∈ (rstep (set R_comp))⇧↔⇧*"
  by (rule egraph_explanation_sound[
        OF compiler_log_accepted merge_reuse_accepted])

subsection ‹Candidate-set extraction›

fun compiler_cost :: "csym ⇒ nat" where
  "compiler_cost CMul = 4"
| "compiler_cost CShl = 4"
| "compiler_cost CAdd = 2"
| "compiler_cost COne = 1"
| "compiler_cost CTwo = 1"

definition compiler_extraction :: "(csym, cvar) extraction" where
  "compiler_extraction =
    ⦇ ex_source = vx ⊗ ctwo
    , ex_chosen = vx ⊕ vx
    , ex_candidates =
        [ (vx ⊕ vx, [Merge_At [] 0 Forward])
        , (vx ⊗ ctwo, []) ] ⦈"

lemma compiler_extraction_accepted:
  "check_extraction compiler_cost R_comp
     (recorded_merges compiler_log) compiler_extraction"
  by (simp add: check_extraction_def check_explanation_def
      recorded_merges_def compiler_log_def compiler_extraction_def)

theorem compiler_extraction_correct:
  "(ex_source compiler_extraction, ex_chosen compiler_extraction)
     ∈ (rstep (set R_comp))⇧↔⇧*"
  "∀v ∈ set (map fst (ex_candidates compiler_extraction)).
     term_cost compiler_cost (ex_chosen compiler_extraction)
       ≤ term_cost compiler_cost v"
  using extraction_over_checked_log_correct[
    OF compiler_log_accepted compiler_extraction_accepted] .

subsection ‹Certificate production with AFP position enumeration›

definition forward_generator ::
  "('f, 'v) rule list ⇒ ('f, 'v) term ⇒
    ('f, 'v) certificate_step list" where
  "forward_generator R t =
    [Rule_At p i Forward Var.
      p ← poss_list t, i ← [0 ..< length R]]"

definition zero :: "(string, string) term" where
  "zero = Fun ''0'' []"
definition aval :: "(string, string) term" where
  "aval = Fun ''a'' []"
definition bval :: "(string, string) term" where
  "bval = Fun ''b'' []"
definition plus_term ::
  "(string, string) term ⇒ (string, string) term ⇒
    (string, string) term" where
  "plus_term s t = Fun ''+'' [s, t]"
definition times_term ::
  "(string, string) term ⇒ (string, string) term ⇒
    (string, string) term" where
  "times_term s t = Fun ''*'' [s, t]"

definition demo_rules :: "(string, string) rule list" where
  "demo_rules =
    [(plus_term aval zero, aval), (plus_term bval zero, bval)]"
definition demo_start :: "(string, string) term" where
  "demo_start = times_term (plus_term aval zero) (plus_term bval zero)"
definition demo_result :: "(string, string) term" where
  "demo_result = times_term aval bval"

lemma demo_search_succeeds:
  "find_explanation demo_rules [] (forward_generator demo_rules) 2
     demo_start demo_result ≠ None"
  by eval

theorem produced_certificate_is_sound:
  "(demo_start, demo_result) ∈ (rstep (set demo_rules))⇧↔⇧*"
proof -
  from demo_search_succeeds obtain sts where found:
    "find_explanation demo_rules [] (forward_generator demo_rules) 2
       demo_start demo_result = Some sts"
    by blast
  show ?thesis by (rule find_explanation_sound[OF _ found]) simp
qed

end