theory week09B_demo_records
imports Main
begin

record A =
  a :: nat
  b :: int

(* Note that the name is global; try to give longer names,
   otherwise 'a' is taken for the rest of the theory *)

(* record constructor syntax: *)
term "\<lparr>a = 3, b = 4\<rparr>"

(* field names are selector functions *)
term a
term b

(* generic update function for field a: *)
term a_update

(* syntax for record update; update field a in record x: *)
term "x \<lparr> a := 3 \<rparr>"

(* note type "'a A_scheme" in the output; it means A and any sub-record of A (more later) *)
typ "'a A_scheme"

consts r :: A
term r
term "a r"

(* A is really "unit A_scheme": *)
consts re :: "unit A_scheme"
consts rf :: "int A_scheme"
term re
term rf

(* the implicit field "more" accesses any future extensions of the record *)
term "A.more"
term "A.more rf"

(* record extension syntax: *)
record B = A +
  c :: "nat list"

consts rb :: B
(* rb is a B record: *)
term rb
(* B's extension is unit *)
term "B.more rb"
(* rb has all fields of A *)
term "A.a rb"

term B.more
term A.more

(* applies to all sub-records of A *)
consts f :: "'a A_scheme \<Rightarrow> unit"

(* applies to only A *)
consts g :: "A \<Rightarrow> unit"

term "f rb" \<comment> \<open>extended record types are subtypes of the record schemes they extend \<close>
term "f r"
term "g rb" \<comment> \<open>..but not of the unparameterised record type \<close>

end
