theory TermCodegen = Main
files "term_codegen.ML":

setup TermCodegen.setup

global

constdefs
  "term" :: "'a \<Rightarrow> 'a"
  "term x == x"

  "to_term" :: "'a \<Rightarrow> 'a"
  "to_term x == x"
(*
local
consts
  foo :: "nat \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> bool"

primrec
  "foo 0 P = term (\<lambda>y. True)"
  "foo (Suc x) P = term (\<lambda>y. to_term (P x) y \<and> to_term (foo x P) y)"

generate_code ("foo.ML") [term_of]
  test = "foo (Suc (Suc (Suc 0))) (\<lambda>x. term (\<lambda>y. to_term x = Suc y))"

datatype foo = C nat

consts
  bar :: "foo \<Rightarrow> nat \<Rightarrow> bool"

primrec
  "bar (C n) = term (\<lambda>n'. n' = to_term n)"

generate_code ("bar.ML") [term_of]
  test = "bar (C (Suc (Suc 0)))"
*)
end