theory Scratch
imports Main
begin

record foo =
  foo1 :: int
  foo2 :: int
  foo3 :: bool

record foo_bar = foo +
  bar1 :: nat
  bar2 :: "bool set"

text {* Problem: Convert @{typ "'a foo_scheme"} into @{typ "'b foo_scheme"}. A special variant is
@{typ foo} (= @{typ "unit foo_scheme"}) to @{typ foo_bar} (= @{typ "unit foo_bar_ext foo_scheme"})*}

definition cast1 :: "foo \<Rightarrow> foo_bar" where
"cast1 g = foo.extend g (foo_bar.fields 0 {})"

export_code cast1 checking SML -- "fails"

definition cast2 :: "foo \<Rightarrow> foo_bar" where
"cast2 = g(| bar1 := 0, bar2 := {} |)" -- "fails: Type mismatch"

definition cast3 :: "foo \<Rightarrow> foo_bar" where
"cast3 g = g\<lparr> \<dots> := \<lparr> bar1 = 0, bar2 = {}\<rparr>\<rparr>" -- "fails: Syntax error"

definition cast4:: "foo \<Rightarrow> foo_bar" where
"cast4 g = foo.more_update (\<lambda>_. \<lparr> bar1 = 0, bar2 = {} \<rparr>) g" -- "fails: Type mismatch"

text {* The previous definition fails, as @{const foo.more_update} has type 
@{typ "('a \<Rightarrow> 'a) \<Rightarrow> 'a foo_scheme \<Rightarrow> 'a foo_scheme"} and not
@{typ "('a \<Rightarrow> 'b) \<Rightarrow> 'a foo_scheme \<Rightarrow> 'b foo_scheme"} *}

text {* The following works, but is rather clumsy. In particular, it needs to specify
all fields of @{typ foo}.*}

function cast5 where
 "cast5 \<lparr> foo1 = x1, foo2 = x2, foo3 = x3 \<rparr> = \<lparr> foo1 = x1, foo2 =
x2, foo3 = x3, bar1 = 0, bar2 = {}\<rparr>"
by (metis foo.cases) (metis foo.ext_inject)
termination by lexicographic_order

export_code cast5 checking SML -- "works"

end