section \<open>Tests\<close>

theory Test_BNF_Record
imports BNF_Record
begin

subsection \<open>Standard usage\<close>

bnf_record ('a, 'b) foo =
  field_1 :: 'a
  field_2 :: 'b

lemma "\<lparr> field_1 = 3, field_2 = () \<rparr> = (make_foo 3 () :: (nat, unit) foo)" ..

lemma "(make_foo a b) \<lparr> field_1 := y \<rparr> = make_foo y b"
  by (simp add: bnf_record_update)

lemma "(make_foo a b) \<lparr> foo.field_1 := y \<rparr> = make_foo y b"
  by (simp add: bnf_record_update)

subsection \<open>Existing datatypes\<close>

datatype x = X (a: int) (b: int)

lemma "\<lparr> a = 1, b = 2 \<rparr> = X 1 2" ..

local_setup \<open>BNF_Record.mk_update_defs @{type_name x}\<close>

lemma "(X 1 2) \<lparr> b := 3 \<rparr> = X 1 3"
  by (simp add: bnf_record_update)

subsection \<open>Nested recursion\<close>

bnf_record 'a container =
  content :: "'a option"

datatype 'a contrived = Contrived "'a contrived container"

term "Contrived \<lparr> content = None \<rparr>"

end