Theory AutoCorres2.CLocals
section ‹Modelling Local Variables›
theory CLocals
imports UMM
"HOL-Library.Code_Binary_Nat"
"ML_Record_Antiquotation"
begin
ML ‹
structure Code_Simproc =
struct
val meta_eq_to_prop = @{lemma ‹(PROP P ≡ Trueprop True) ⟹ PROP P› for P by simp}
fun solved_eq eq =
case Thm.prop_of eq of
@{term_pat "_ ≡ Trueprop True"} => true
| _ => false
fun code_prove ctxt prop =
let
val code_eq = SOME (Code_Runtime.dynamic_holds_conv ctxt prop) handle ERROR x => (warning x; NONE)
val _ = Utils.verbose_msg 4 ctxt (fn _ => "code_prove: " ^ @{make_string} code_eq)
in
code_eq |> Option.mapPartial (fn eq =>
if solved_eq eq then
SOME (meta_eq_to_prop OF [Code_Simp.dynamic_conv ctxt prop])
else NONE)
end
fun fill_default default xs =
let
fun fill ys _ [] = rev ys
| fill ys n (zs as ((i, z)::zs')) =
if n = i then
fill (z::ys) (n + 1) zs'
else
if n < i then fill (default::ys) (n + 1) zs
else error ("fill_default: expecting indexes in ascending order" ^ @{make_string} (map fst xs))
in
fill [] 0 xs
end
fun code_simp_prems cond_eq_rule0 ps ctxt ct =
let
val cond_eq_rule = Thm.transfer' ctxt cond_eq_rule0
val _ = Utils.verbose_msg 4 ctxt (fn _ => "code_simp_prems: " ^ @{make_string} (ct, cond_eq_rule))
val ps = sort int_ord ps
val lhs = cond_eq_rule |> Thm.cconcl_of |> Thm.dest_equals_lhs
val eq = Thm.instantiate (Thm.match (lhs, ct)) cond_eq_rule
val prems = Thm.cprems_of eq
fun solve i = code_prove ctxt (nth prems i)
val solved = map_filter solve ps
in
if length solved = length ps then
SOME (eq OF (fill_default Drule.asm_rl (ps ~~ solved)))
else
NONE
end
fun is_eq (@{term_pat "Trueprop (_ = _)"}) = true
| is_eq (@{term_pat "_ ≡ _"}) = true
| is_eq _ = false
fun positions_of len interval =
case interval of
Facts.FromTo (i, j) => (@{assert} (j <= len) ; (i - 1) upto (j - 1))
| Facts.From i => (@{assert} (i <= len) ; (i - 1) upto (len - 1))
| Facts.Single i => (@{assert} (i <= len); [i - 1])
fun positions_of_intervals len =
map (positions_of len) #> flat #> sort_distinct int_ord
fun lhs_pattern ctxt eq =
let
val ((_, [eq]), _) = Variable.import false [eq] ctxt
in
eq |> Thm.concl_of |> Logic.dest_equals |> fst
end
structure Data = Generic_Data (
type T = simproc list Symtab.table
val empty = Symtab.empty
val merge = Symtab.merge (K false))
fun get_simprocs ctxt named_thms =
let
val simprocs = Data.get (Context.Proof ctxt)
in
Symtab.lookup_list simprocs named_thms
end
fun check context named_thms =
let
val ctxt = Context.proof_of context
val facts = (Proof_Context.facts_of ctxt);
in
Facts.check context facts named_thms
end
fun add_simproc pos named_thms (intervals: Facts.interval list) thm context =
let
val ctxt = Context.proof_of context
val named_thms = if fst (named_thms) = "" then "" else (check context named_thms )
val _ = is_eq (Thm.concl_of thm) orelse error ("Code_Simproc.add_simproc: conclusion is not an equality")
val _ = Thm.has_name_hint thm orelse error ("Code_Simproc.add_simproc: theorem has no name")
val name_hint = Thm.get_name_hint thm
val base_name = Long_Name.base_name name_hint
val thm1 = safe_mk_meta_eq thm
val nprems = Thm.nprems_of thm1
val _ = nprems > 0 orelse error ("Code_Simproc.add_simprocs: theorem has no premises")
val positions = if null intervals then 0 upto nprems - 1 else positions_of_intervals nprems intervals
val patterns = thm1 |> lhs_pattern ctxt |> single
val thm2 = Thm.trim_context thm1
in
if Local_Theory.level ctxt = 0 then context
else
context
|> Context.map_proof_result (Simplifier.define_simproc {name = Binding.make (base_name, pos), passive=false, identifier=[],
lhss = patterns, proc = fn _ => code_simp_prems thm2 positions})
|-> (fn simproc => Context.map_proof (
Local_Theory.declaration {pervasive=false, syntax=false, pos = ⌂} (fn _ =>
(Data.map (Symtab.map_default (named_thms, [simproc]) (cons simproc))))))
end
end
›
setup ‹
let
fun position scan = (Scan.ahead (Scan.one (K true)) >> Token.pos_of) -- scan >> Library.swap;
in
Attrib.setup \<^binding>‹code_simproc›
(Scan.lift (position
(Scan.optional Parse.name_position ("", Position.none) -- Scan.optional Parse.thm_sel []) >>
(fn ((named_thms, intervals), pos) =>
Thm.declaration_attribute (fn thm => Code_Simproc.add_simproc pos named_thms intervals thm))))
"solve preconditions with code_simp" #>
ML_Antiquotation.value_embedded \<^binding>‹code_simprocs›
(Args.context -- Scan.lift Parse.embedded_position >>
(fn (ctxt, name) => "Code_Simproc.get_simprocs ML_context " ^
ML_Syntax.print_string (Code_Simproc.check (Context.Proof ctxt) name)))
end
›
ML ‹
String.str
›
type_synonym locals = "nat ⇒ byte list"
definition "clookup" :: "nat ⇒ locals ⇒ 'a::mem_type" where
"clookup n l = from_bytes (l n)"
definition "cupdate" :: "nat ⇒ ('a::mem_type ⇒ 'a) ⇒ locals ⇒ locals" where
"cupdate n f l = l(n := to_bytes (f (from_bytes (l (n)))) (replicate (size_of TYPE('a)) 0))"
lemma clookup_cupdate_same[simp, state_simp]: "clookup n (cupdate n f l) = f (clookup n l)"
by (simp add: clookup_def cupdate_def)
lemma clookup_cupdate_same_cond[code_simproc state_simp]:
"n = 0 ⟹ clookup n (cupdate 0 f l) = f (clookup n l)"
"n = 0 ⟹ clookup 0 (cupdate n f l) = f (clookup n l)"
"n = 1 ⟹ clookup n (cupdate 1 f l) = f (clookup n l)"
"n = Suc 0 ⟹ clookup n (cupdate (Suc 0) f l) = f (clookup n l)"
"n = 1 ⟹ clookup 1 (cupdate n f l) = f (clookup n l)"
"n = Suc 0 ⟹ clookup (Suc 0) (cupdate n f l) = f (clookup n l)"
"n = numeral m ⟹ clookup n (cupdate (numeral m) f l) = f (clookup n l)"
"n = numeral m ⟹ clookup (numeral m) (cupdate n f l) = f (clookup n l)"
by (auto simp add: clookup_def cupdate_def)
lemma clookup_refl_cond[code_simproc state_simp]:
"n = m ⟹ clookup n l = clookup m l ⟷ True"
by (simp_all add: clookup_def)
lemma clookup_cupdate_other[code_simproc state_simp]: "n ≠ m ⟹ clookup n (cupdate m f l) = (clookup n l)"
by (auto simp add: clookup_def cupdate_def)
lemma cupdate_compose[simp, state_simp]: "cupdate n f (cupdate n g l) = cupdate n (f o g) l"
by (simp add: cupdate_def)
lemma cupdate_compose_cond[code_simproc state_simp]:
"n = 0 ⟹ cupdate n f (cupdate 0 g l) = cupdate n (f o g) l"
"n = 0 ⟹ cupdate 0 f (cupdate n g l) = cupdate n (f o g) l"
"n = 1 ⟹ cupdate n f (cupdate 1 g l) = cupdate n (f o g) l"
"n = Suc 0 ⟹ cupdate n f (cupdate (Suc 0) g l) = cupdate n (f o g) l"
"n = Suc 0 ⟹ cupdate (Suc 0) f (cupdate n g l) = cupdate n (f o g) l"
"n = numeral m ⟹ cupdate n f (cupdate (numeral m) g l) = cupdate n (f o g) l"
"n = numeral m ⟹ cupdate (numeral m) f (cupdate n g l) = cupdate n (f o g) l"
by (auto simp add: cupdate_def)
lemma clookup_cupdate_other_numeral[simplified, simp, state_simp]:
"clookup 0 (cupdate 1 f l) = (clookup 0 l)"
"clookup 0 (cupdate (numeral m) f l) = (clookup 0 l)"
"clookup 1 (cupdate 0 f l) = (clookup 1 l)"
"numeral m ≠ (1::nat) ⟹
clookup 1 (cupdate (numeral m) f l) = (clookup 1 l)"
"clookup (numeral n) (cupdate 0 f l) = (clookup (numeral n) l)"
"numeral n ≠ (1::nat) ⟹
clookup (numeral n) (cupdate 1 f l) = (clookup (numeral n) l)"
"n ≠ m ⟹
clookup (numeral n) (cupdate (numeral m) f l) = (clookup (numeral n) l)"
by (auto simp add: clookup_def cupdate_def)
lemma cupdate_commute: "n ≠ m ⟹ cupdate n f (cupdate m g l) = cupdate m g (cupdate n f l)"
by (auto simp add: cupdate_def fun_upd_def)
lemma cupdate_commute_ordered[code_simproc state_simp]: "n < m ⟹ cupdate n f (cupdate m g l) = cupdate m g (cupdate n f l)"
by (auto simp add: cupdate_def fun_upd_def)
lemma cupdate_commute_numeral_simp[simplified, simp, state_simp]:
"cupdate 0 f (cupdate 1 g l) = cupdate 1 g (cupdate 0 f l)"
"cupdate 0 f (cupdate (numeral m) g l) = cupdate (numeral m) g (cupdate 0 f l)"
"numeral m ≠ (1::nat) ⟹
cupdate 1 f (cupdate (numeral m) g l) = cupdate (numeral m) g (cupdate 1 f l)"
"n < m ⟹ cupdate (numeral n) f (cupdate (numeral m) g l) = cupdate (numeral m) g (cupdate (numeral n) f l)"
by (auto simp add: cupdate_def fun_upd_def)
lemma const_compose [simp, state_simp]:
"cupdate n ((λ_. x) ∘ f) = cupdate n (λ_. x)"
"cupdate n (f ∘ (λ_. x)) = cupdate n (λ_. f x)"
by (auto simp add: comp_def)
lemma K_eq_cong: "((λ_. x) = (λ_. y)) ⟷ x = y"
by (simp add: fun_eq_iff)
ML_file ‹positional_symbol_table.ML›
named_theorems locals
consts clocals_string_embedding :: "string ⇒ nat"
consts exit_'::nat
definition "global_exn_var_clocal = clocals_string_embedding ''global_exn_var''"
bundle clocals_string_embedding
begin
notation clocals_string_embedding ("𝒮")
end
ML ‹
structure CLocals =
struct
structure Locals = Positional_Symbol_Table(type key = string val ord = fast_string_ord);
@{record ‹datatype entry = Entry of {typ : typ, term: term, def: thm, kind: NameGeneration.var_kind}›}
fun morph_entry phi {typ, term, def, kind} = make_entry
{typ = Morphism.typ phi typ, term = Morphism.term phi term, def = Morphism.thm phi def, kind = kind};
fun entry_ord (Entry {kind = kind1, typ = T1, term = t1, def = thm1}, Entry {kind = kind2, typ = T2, term = t2, def = thm2})
= prod_ord NameGeneration.var_kind_ord (prod_ord Term_Ord.typ_ord (prod_ord Term_Ord.fast_term_ord Thm.thm_ord))
((kind1, (T1, (t1, thm1))), (kind2, ((T2, (t2, thm2)))))
val entry_eq = is_equal o entry_ord
type locals_scope = {locals: entry Locals.symbol_table, scope: Locals.qualifier}
structure Data = Generic_Data (struct
type T = locals_scope
val empty = {locals = Locals.empty, scope = []}
fun merge ({locals=locals1, ...}, {locals=locals2, ...}) =
{locals = Locals.merge entry_eq (locals1, locals2),
scope = []}
end)
fun map_locals f ({locals, scope}:locals_scope) =
({locals = f locals, scope = scope}:locals_scope)
fun map_scope f ({locals, scope}:locals_scope) = ({locals = locals, scope = f scope}:locals_scope)
fun locals_map f = Data.map (map_locals f)
fun scope_map f = Data.map (map_scope f)
fun enter_scope n = map_scope (fn xs => xs @ [n])
val exit_scope = map_scope (fst o split_last)
fun switch_scope fname =
Context.proof_map (Data.map (exit_scope #> enter_scope fname))
fun program_name ctxt =
case #scope (Data.get (Context.Proof ctxt)) of
(prog_name::_) => prog_name
| _ => ""
fun function_name ctxt =
case #scope (Data.get (Context.Proof ctxt)) of
[_, fun_name] => fun_name
| _ => ""
fun read_function_pointer ctxt s =
let
val s = if Long_Name.is_qualified s then s else Long_Name.qualify (program_name ctxt) s
in
Proof_Context.read_const {proper=true, strict=true} ctxt s
end
fun mk_lookup_positional T i =
\<^Const>‹clookup T› $ HOLogic.mk_number @{typ nat} i
fun lookup_by_short_name ctxt x =
let
val {scope, locals} = Data.get (Context.Proof ctxt)
val x = NameGeneration.un_varname x
val (qualifier, base) = Long_Name.explode x |> split_last
val common_scope = rev scope |> drop (length qualifier) |> rev
val full_scope = (if null common_scope then scope else common_scope) @ qualifier
fun proj (name, (pos, Entry {typ, term,...})) = (name, (typ, term))
val hits =
Locals.lookup locals full_scope base |> Option.map (proj o pair x)
in
case hits of
SOME v => v
| NONE => error ("lookup_by_short_name: " ^ quote base ^ " not defined in scope " ^ @{make_string} full_scope)
end
fun info_from_term ctxt t =
let
val {scope, locals} = Data.get (Context.Proof ctxt)
in
case t of
Const (n, _) =>
let
val name = NameGeneration.un_varname (Long_Name.base_name n)
in Locals.lookup locals scope name |> Option.map (fn (p, x) => (name, (p, x))) end
| _ => try Utils.dest_nat_or_number t
|> Option.mapPartial (fn p =>
Locals.lookup_positional locals scope p
|> Option.map (fn (name, x) => (name, (p, x))))
end
fun kind_from_term ctxt t = info_from_term ctxt t
|> Option.map (fn (_, (_, Entry {kind, ...})) => kind)
fun is_defined ctxt x =
is_some (try (lookup_by_short_name ctxt) x)
fun gen_mk_lookup ctxt (NameGeneration.Named x) =
let val (_, (typ, term)) = lookup_by_short_name ctxt x
in (\<^Const>‹clookup typ› $ term, typ) end
| gen_mk_lookup _ (NameGeneration.Positional (i, T)) =
(\<^Const>‹clookup T› $ HOLogic.mk_number @{typ nat} i, T)
fun get_position ctxt n =
let
val {scope, locals} = Data.get (Context.Proof ctxt)
in Locals.lookup locals scope n |> Option.map fst end
fun get_default_position ctxt n = the_default (~1) (get_position ctxt n)
fun positional_ord ctxt = int_ord o apply2 (get_default_position ctxt)
fun get_locals ctxt =
let
val {scope, locals} = Data.get (Context.Proof ctxt)
val locals = Locals.get_scope (locals) scope
in
locals
|> Locals.Keytab.dest
|> map (fn (n, (_, Entry {typ, term, ...})) =>
(Long_Name.base_name n, (typ, (\<^Const>‹clookup typ› $ term))))
end
fun mk_lookup ctxt x = fst (gen_mk_lookup ctxt (NameGeneration.Named x))
fun mk_update ctxt x =
let val (_, (typ, term)) = lookup_by_short_name ctxt x
in \<^Const>‹cupdate typ› $ term end
fun mk_update_positional T i =
\<^Const>‹cupdate T› $ HOLogic.mk_number @{typ nat} i
fun get_name ctxt n = \<^try>‹
let val (n, (typ, _)) = lookup_by_short_name ctxt n
in (n, typ) end
catch _ => raise Match›
fun return_name_hint "ret" = "ret'"
| return_name_hint x = x
fun dest_return_name_hint "ret'" = "ret"
| dest_return_name_hint x = x
fun embedded_name_hint n = @{const clocals_string_embedding} $ Utils.encode_isa_string n
fun name_hint ctxt n =
if n = NameGeneration.global_exn_var_name then
@{const global_exn_var_clocal}
else
(case try (lookup_by_short_name ctxt) (return_name_hint n) of
SOME (_, (_, term)) => term
| NONE =>
let
val _ = warning ("name_tag: no match for " ^ quote n ^ ". Using string embedding.")
in
embedded_name_hint n
end)
fun name_hints ctxt = map (name_hint ctxt) #> Utils.encode_isa_list @{typ nat}
fun dest_name_hint (\<^Const_>‹clocals_string_embedding for s›) = HOLogic.dest_string s
| dest_name_hint (\<^const>‹global_exn_var_clocal›) = NameGeneration.global_exn_var_name
| dest_name_hint (Const (n, @{typ nat})) = dest_return_name_hint (NameGeneration.un_varname (Long_Name.base_name n))
| dest_name_hint _ = raise Match
val dest_name_hints = Utils.decode_isa_list #> map dest_name_hint
fun split_scope n =
case rev (Long_Name.explode n) of
(base:: fname :: prog_name:: _) => ([prog_name, fname], base)
| _ => raise Match
fun strip_common [] [] = []
| strip_common (x::xs) (y::ys) = if x = y then strip_common xs ys else (y::ys)
| strip_common [] ys = ys
| strip_common _ [] = []
val short_names = Attrib.setup_config_bool \<^binding>‹clocals_short_names› (K false);
fun print_tr ctxt (c as (Const (n, T))) =
let
val {scope, locals} = Data.get (Context.Proof ctxt)
val (name_scope, base_name) = split_scope n
val base_name = NameGeneration.un_varname base_name
val min_scope = strip_common scope name_scope
val short_name = base_name
|> not (Config.get ctxt short_names) ? fold Long_Name.qualify min_scope
in
case Locals.lookup locals name_scope base_name of
SOME (_, Entry {typ, ...}) =>
Syntax.const \<^syntax_const>‹_constrain› $ Const (short_name, T) $ Syntax_Phases.term_of_typ ctxt typ
| _ => raise Match
end
| print_tr _ t = raise Match
fun is_lookup ctxt (Const (@{const_name clookup}, _ ) $ _) = true
| is_lookup ctxt (Const (@{const_syntax clookup}, _ ) $ _) = true
| is_lookup ctxt _ = raise Match
fun lookup_tr' ctxt (Const (@{const_name clookup}, _ ) $ (c as Const _)) = print_tr ctxt c
| lookup_tr' ctxt (Const (@{const_syntax clookup}, _ ) $ (c as Const _)) = print_tr ctxt c
| lookup_tr' ctxt t = raise Match
fun dest_update_tr' ctxt ((c as (Const (@{const_syntax cupdate}, _ ) $ Const _ )) $ v $ s) =
(c, v, SOME s)
| dest_update_tr' ctxt ((c as (Const (@{const_name cupdate}, _ ) $ Const _ )) $ v $ s) =
(c, v, SOME s)
| dest_update_tr' ctxt ((c as (Const (@{const_syntax cupdate}, _ ) $ Const _ )) $ v) =
(c, v, NONE)
| dest_update_tr' ctxt ((c as (Const (@{const_name cupdate}, _ ) $ Const _ )) $ v) =
(c, v, NONE)
| dest_update_tr' ctxt t = raise Match
fun update_tr' ctxt (Const (@{const_name cupdate}, _ ) $ (c as Const _)) = print_tr ctxt c
| update_tr' ctxt (Const (@{const_syntax cupdate}, _ ) $ (c as Const _)) = print_tr ctxt c
| update_tr' ctxt t = t
fun locals_insert qualifier pos name typ kind def tab =
let
val tab' = tab |> Locals.update_new qualifier (name,
Entry {typ=typ, term = Thm.concl_of def |> Utils.lhs_of_eq, def = Thm.trim_context def, kind = kind})
val _ = @{assert} ((Locals.lookup tab' qualifier name |> Option.map fst) = SOME pos)
in
tab'
end
fun add_entry qualifier pos name typ kind def =
locals_map (locals_insert qualifier pos name typ kind def)
fun add_entry_attr qualifier pos name typ kind =
Thm.declaration_attribute (add_entry qualifier pos name typ kind)
fun define_locals qualifier decls thy =
let
val _ = @{assert} (not (null qualifier))
val fname = split_last qualifier |> snd
val lthy = Named_Target.theory_init thy
fun define (i, (name, typ, kind)) lthy =
let
val vname = NameGeneration.ensure_varname name
val b = Binding.make (vname, ⌂) |> fold_rev (Binding.qualify true) qualifier
val attrib = Attrib.internal ⌂ (fn _ => add_entry_attr qualifier i name typ kind)
val rhs = HOLogic.mk_number @{typ nat} i
val ((t, (s, thm)), lthy) = lthy
|> Local_Theory.define ((b, Mixfix.NoSyn), ((Binding.suffix_name "_def" b, [attrib] @ @{attributes [locals]} ), rhs))
in
lthy |> Code.declare_default_eqns [(thm, true)]
end
val lthy = lthy
|> fold define (tag_list 0 decls)
|> Bundle.bundle (Binding.make (suffix "_scope" fname, ⌂),
Attrib.internal_declaration ⌂ (Morphism.entity (fn _ => scope_map (K (qualifier))))) []
in
lthy |> Local_Theory.exit_global
end
fun symmetric ctxt thm = fst (Thm.apply_attribute Calculation.symmetric thm (Context.Proof ctxt))
fun gen_unfolded {sym} qualifier ctxt thm =
let
val {scope, locals} = Data.get (Context.Proof ctxt)
val qualifier = if null qualifier then scope else qualifier
val defs0 = Locals.get_scope locals qualifier |> Locals.Keytab.dest
|> map (fn (_, (_, Entry {def,...})) => Thm.transfer' ctxt def)
val defs = defs0 |> sym ? map (symmetric ctxt)
in
Simplifier.simplify (Simplifier.put_simpset HOL_basic_ss ctxt addsimps defs) thm
end
val unfolded_with = gen_unfolded {sym = false}
val folded_with = gen_unfolded {sym = true}
val unfolded = unfolded_with []
val folded = folded_with []
fun check_scope ctxt (qualifier, pos) =
let
val {locals, scope} = Data.get (Context.Proof ctxt)
val exploded = Long_Name.explode qualifier
val extended = if length exploded = 1 then
take 1 scope @ exploded
else
exploded
in
if null extended orelse Locals.defined_scope locals extended then
extended
else
error ("undefined scope: " ^ quote (Long_Name.implode extended) ^ Position.here pos)
end
end
›
setup ‹
Attrib.setup \<^binding>‹fold_locals›
(Args.context -- Scan.lift (Scan.optional Parse.name_position ("", Position.none)) >>
(fn (ctxt, (qualifier, pos)) =>
let
val exploded = CLocals.check_scope ctxt (qualifier, pos)
in
Thm.rule_attribute [] (CLocals.folded_with exploded o Context.proof_of)
end))
"fold local variables within optional scope qualifier" #>
Attrib.setup \<^binding>‹unfold_locals›
(Args.context -- Scan.lift (Scan.optional Parse.name_position ("", Position.none)) >>
(fn (ctxt, (qualifier, pos)) =>
let
val exploded = CLocals.check_scope ctxt (qualifier, pos)
in
Thm.rule_attribute [] (CLocals.unfolded_with exploded o Context.proof_of)
end))
"unfold local variables within optional scope qualifier"
›
nonterminal localsupdbinds and localsupdbind
syntax
"_localsupdbind" :: "'a ⇒ 'a ⇒ localsupdbind" ("(2_ :=⇩ℒ/ _)")
"" :: "localsupdbind ⇒ localsupdbinds" ("_")
"_localsupdbinds":: "localsupdbind ⇒ localsupdbinds ⇒ localsupdbinds" ("_,/ _")
syntax
"_statespace_lookup" :: "locals ⇒ 'name ⇒ 'c" ("_ ⋅ _" [60, 60] 60)
"_statespace_locals_lookup" :: "('g, locals, 'e, 'x) state_scheme ⇒ 'name ⇒ 'c"
("_ ⋅⇩ℒ _" [60, 60] 60)
"_statespace_update" :: "locals ⇒ 'name ⇒ ('c ⇒ 'c) ⇒ locals"
"_statespace_updates" :: "locals ⇒ updbinds ⇒ locals" ("_⟨_⟩" [900, 0] 900)
"_statespace_locals_update" :: "('g, locals, 'e, 'x) state_scheme ⇒ 'name ⇒ ('c ⇒ 'c) ⇒ ('g, locals, 'e, 'x) state_scheme"
"_statespace_locals_updates" :: "locals ⇒ localsupdbinds ⇒ locals" ("_⟨_⟩" [900, 0] 900)
"_statespace_locals_map" ::
"'name ⇒ ('c ⇒ 'c) ⇒ ('g, locals, 'e, 'x) state_scheme ⇒ ('g, locals, 'e, 'x) state_scheme"
("(2_:=⇩ℒ/ _)" [1000, 1000] 1000)
translations
"_statespace_updates f (_updbinds b bs)" ==
"_statespace_updates (_statespace_updates f b) bs"
"s⟨x := y⟩" == "_statespace_update s x y"
"_statespace_locals_updates f (_localsupdbinds b bs)" ==
"_statespace_locals_updates (_statespace_locals_updates f b) bs"
"s⟨x :=⇩ℒ y⟩" == "_statespace_locals_update s x y"
parse_translation
‹
let
fun lookup_tr ctxt [s, x] =
let
in
(case Term_Position.strip_positions x of
Free (n,_) => CLocals.mk_lookup ctxt n $ s
| _ => raise Match)
end
fun locals_lookup_tr ctxt [s, x] =
(case Term_Position.strip_positions x of
Free (n,_) =>
CLocals.mk_lookup ctxt n $ (Syntax.const \<^const_name>‹locals› $ s)
| _ => raise Match);
fun update_tr ctxt [s, x, v] =
(case Term_Position.strip_positions x of
Free (n, _) =>
let
val upd = CLocals.mk_update ctxt n
in upd $ v $ s end
| _ => raise Match);
fun locals_update_tr ctxt [s, x, v] =
let
val upd $ n $ v' $ _ = update_tr ctxt [s, x, v]
in
Syntax.const \<^const_name>‹locals_update› $ (upd $ n $ v') $ s
end
fun locals_map_tr ctxt [x, v] =
let
val upd $ s = locals_update_tr ctxt [Bound 0, x, v]
in
upd
end
in
[(\<^syntax_const>‹_statespace_lookup›, lookup_tr),
(\<^syntax_const>‹_statespace_locals_lookup›, locals_lookup_tr),
(\<^syntax_const>‹_statespace_update›, update_tr),
(\<^syntax_const>‹_statespace_locals_update›, locals_update_tr),
(\<^syntax_const>‹_statespace_locals_map›, locals_map_tr)]
end
›
print_translation ‹
let
fun dest_number (Const (\<^const_syntax>‹Groups.zero›, _)) = 0
| dest_number (Const (\<^const_syntax>‹Groups.one›, _)) = 1
| dest_number (Const (\<^const_syntax>‹numeral›, _) $ n) = Numeral.dest_num_syntax n
fun lookup_tr' ctxt (args as [n, s]) =
let
val n' = CLocals.print_tr ctxt n
in
case s of
Const (\<^const_syntax>‹locals›, _) $ s'' =>
Syntax.const \<^syntax_const>‹_statespace_locals_lookup› $ s'' $ n'
| Const (\<^syntax_const>‹_antiquoteCur›, _) $ Const ("get_actuals", _) =>
Syntax.const \<^syntax_const>‹_antiquoteCur› $ n'
| _ => Syntax.const \<^syntax_const>‹_statespace_lookup› $ s $ n'
end
fun update_tr' ctxt (args as [n, v, s]) =
let
val n' = CLocals.print_tr ctxt n
in
Syntax.const \<^syntax_const>‹_statespace_update› $ s $ n' $ v
end
fun locals_update_tr' ctxt (args as [upd, s]) =
let
val _ $ s' $ n' $ v = update_tr' ctxt ((snd (strip_comb upd)) @ [s])
in
Syntax.const \<^syntax_const>‹_statespace_locals_update› $ s' $ n' $ v
end
| locals_update_tr' ctxt (args as [upd]) =
let
val _ $ _ $ n' $ v = update_tr' ctxt ((snd (strip_comb upd)) @ [Bound 0])
in
Syntax.const \<^syntax_const>‹_statespace_locals_map› $ n' $ v
end
fun assign_tr' ctxt (args as [(aq as Const ("_antiquoteCur", _)) $ (c as Const ("locals", _)), upd]) =
let
fun dest_K (Abs ("_", _, v)) = v
| dest_K t = t
val s = Bound 0
val _ $ _ $ n $ v = locals_update_tr' ctxt [upd, s]
in
Syntax.const \<^syntax_const>‹_Assign› $ (aq $ n) $ (dest_K v)
end
| assign_tr' ctxt t = raise Match
in
[(\<^const_syntax>‹clookup›, lookup_tr'),
(\<^const_syntax>‹cupdate›, update_tr'),
(\<^const_syntax>‹locals_update›, locals_update_tr'),
(\<^syntax_const>‹_Assign›, assign_tr')]
end
›
end