# HG changeset patch # User paulson # Date 1635261723 -3600 # Node ID a0ab0dc28d3c19029fa8b7c89ed4a71df8dcc2a5 # Parent ee92a47b47cbf214c319128bb14e472491712f7c# Parent 00ffae972fc0625bdd9939399254751b02367824 merged diff -r 00ffae972fc0 -r a0ab0dc28d3c CONTRIBUTORS --- a/CONTRIBUTORS Tue Oct 26 11:15:40 2021 +0100 +++ b/CONTRIBUTORS Tue Oct 26 16:22:03 2021 +0100 @@ -22,6 +22,9 @@ complex numbers (theory HOL-Library.Complex_Order), and products of uniform spaces (theory HOL-Analysis.Product_Vector). +* November 2020 / July 2021: Norbert Schirmer, Apple + Various improvements and cleanup of session "HOL-Statespace". + * July 2021: Florian Haftmann Further consolidation of bit operations and word types. diff -r 00ffae972fc0 -r a0ab0dc28d3c NEWS --- a/NEWS Tue Oct 26 11:15:40 2021 +0100 +++ b/NEWS Tue Oct 26 16:22:03 2021 +0100 @@ -287,6 +287,8 @@ * Theory "HOL-Combinatorics.Transposition" provides elementary swap operation "transpose". +* Session "HOL-Statespace": various improvements and cleanup. + *** ML *** diff -r 00ffae972fc0 -r a0ab0dc28d3c src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 26 11:15:40 2021 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 26 16:22:03 2021 +0100 @@ -1,5 +1,6 @@ (* Title: HOL/Statespace/StateSpaceEx.thy - Author: Norbert Schirmer, TU Muenchen + Author: Norbert Schirmer, TU Muenchen, 2007 + Author: Norbert Schirmer, Apple, 2021 *) section \Examples \label{sec:Examples}\ @@ -12,6 +13,7 @@ "_statespace_updates" :: "('a \ 'b) \ updbinds \ ('a \ 'b)" ("_\_\" [900,0] 900) (*>*) + text \Did you ever dream about records with multiple inheritance? Then you should definitely have a look at statespaces. They may be what you are dreaming of. Or at least almost \dots\ @@ -31,7 +33,7 @@ text \\noindent This resembles a \<^theory_text>\record\ definition, but introduces sophisticated locale -infrastructure instead of HOL type schemes. The resulting context +infrastructure instead of HOL type schemes. The resulting context postulates two distinct names \<^term>\n\ and \<^term>\b\ and projection~/ injection functions that convert from abstract values to \<^typ>\nat\ and \bool\. The logical content of the locale is:\ @@ -52,17 +54,12 @@ locale. We also maintain non-logical context information to support the user: -\begin{itemize} - -\item Syntax for state lookup and updates that automatically inserts +\<^item> Syntax for state lookup and updates that automatically inserts the corresponding projection and injection functions. - -\item Setup for the proof tools that exploit the distinctness +\<^item> Setup for the proof tools that exploit the distinctness information and the cancellation of projections and injections in deductions and simplifications. -\end{itemize} - This extra-logical information is added to the locale in form of declarations, which associate the name of a variable to the corresponding projection and injection functions to handle the syntax @@ -71,8 +68,9 @@ extended there are multiple distinctness theorems in the context. Our declarations take care that the link always points to the strongest distinctness assumption. With these declarations in place, a lookup -can be written as \s\n\, which is translated to \project_nat (s n)\, and an update as \s\n := 2\\, which is -translated to \s(n := inject_nat 2)\. We can now establish the +can be written as \s\n\, which is translated to \project_nat (s n)\, and an +update as \s\n := 2\\, which is translated to \s(n := inject_nat 2)\. +We can now establish the following lemma:\ lemma (in vars) foo: "s\b = s\b" by simp @@ -91,7 +89,8 @@ \<^typ>\'a\. This type is fixed inside the state space but may get instantiated later on, analogous to type parameters of an ML-functor. The distinctness assumption is now \distinct [N, B, n, b, x]\, -from this we can derive both \<^term>\distinct [N,B]\ and \<^term>\distinct [n,b]\, the distinction assumptions for the two versions of +from this we can derive both \<^term>\distinct [N,B]\ and \<^term>\distinct [n,b]\, +the distinction assumptions for the two versions of locale \vars\ above. Moreover we have all necessary projection and injection assumptions available. These assumptions together allow us to establish state space \<^term>\varsX\ as an @@ -111,8 +110,8 @@ we get logarithmic certificates for the distinctness of two names by the distinctness of the paths in the tree. Asked for the distinctness of two names, our tool produces the paths of the variables in the tree -(this is implemented in SML, outside the logic) and returns a -certificate corresponding to the different paths. Merging state +(this is implemented in Isabelle/ML, outside the logic) and returns a +certificate corresponding to the different paths. Merging state spaces requires to prove that the combined distinctness assumption implies the distinctness assumptions of the components. Such a proof is of the order $m \cdot \log n$, where $n$ and $m$ are the number of @@ -192,39 +191,70 @@ shows "s\x = s\x" by simp - -(* -text "Hmm, I hoped this would work now..." +text \There were known problems with syntax-declarations. They only +worked when the context is already completely built. This is now overcome. e.g.:\ locale fooX = foo + assumes "s\b = k" -*) + + + +text \ +We can also put statespaces side-by-side by using ordinary @{command locale} expressions +(instead of the @{command statespace}). +\ + + +locale side_by_side = foo + bar where b="B::'a" and c=C for B C -(* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *) -text \There are known problems with syntax-declarations. They currently -only work, when the context is already built. Hopefully this will be -implemented correctly in future Isabelle versions.\ +context side_by_side +begin +text \Simplification within one of the statespaces works as expected.\ +lemma "s\C = s\C" + by simp + +lemma "s\b = s\b" + by simp + +text \In contrast to the statespace @{locale loo} there is no 'inter' statespace distinctness +between the names of @{locale foo} and @{locale bar}.\ +end + + +text \Sharing of names in side-by-side statespaces is also possible as long as they are mapped +to the same type.}\ -(* -lemma - assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4" - shows True -proof - interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact - term "s\a = i" -qed -*) -(* -lemma - includes foo - shows "s\a = i" -*) +statespace vars1 = n::nat m::nat +statespace vars2 = n::nat k::nat + +locale vars1_vars2 = vars1 + vars2 + +context vars1_vars2 +begin + +text \Note that the distinctness theorem for @{locale vars1} is selected here to do the proof.\ +lemma "s\m = s\m" + by simp + +text \Note that the distinctness theorem for @{locale vars2} is selected here to do the proof.\ +lemma "s\k = s\k" + by simp -text \It would be nice to have nested state spaces. This is -logically no problem. From the locale-implementation side this may be -something like an 'includes' into a locale. When there is a more -elaborate locale infrastructure in place this may be an easy exercise. -\ +text \Still there is no inter-statespace distinctness.\ +lemma "s\m = s\m" + (* apply simp *) + oops +end + +statespace merge_vars1_vars2 = vars1 + vars2 + +context merge_vars1_vars2 +begin +text \When defining a statespace instead of a side-by-side locale we get the distinctness of +all variables.\ +lemma "s\m = s\m" + by simp +end subsection \Benchmarks\ diff -r 00ffae972fc0 -r a0ab0dc28d3c src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Tue Oct 26 11:15:40 2021 +0100 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Tue Oct 26 16:22:03 2021 +0100 @@ -1,5 +1,6 @@ (* Title: HOL/Statespace/distinct_tree_prover.ML - Author: Norbert Schirmer, TU Muenchen + Author: Norbert Schirmer, TU Muenchen, 2007 + Author: Norbert Schirmer, Apple, 2021 *) signature DISTINCT_TREE_PROVER = @@ -9,6 +10,8 @@ val dest_tree : term -> term list val find_tree : term -> term -> direction list option + val in_set: Proof.context -> direction list -> cterm -> thm + val find_in_set: Proof.context -> term -> cterm -> thm val neq_to_eq_False : thm val distinctTreeProver : Proof.context -> thm -> direction list -> direction list -> thm val neq_x_y : Proof.context -> term -> term -> string -> thm option @@ -188,6 +191,41 @@ in (x, l) end; in + +fun in_set ctxt ps tree = + let + val in_set = in_set ctxt + val (_, [l, x, _, r]) = Drule.strip_comb tree; + val xT = Thm.ctyp_of_cterm x; + in + (case ps of + [] => + instantiate ctxt + [(Thm.ctyp_of_cterm x_in_set_root, xT)] + [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root} + | Left :: ps' => + let + val in_set_l = in_set ps' l; + val in_set_left' = + instantiate ctxt + [(Thm.ctyp_of_cterm x_in_set_left, xT)] + [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left}; + in discharge ctxt [in_set_l] in_set_left' end + | Right :: ps' => + let + val in_set_r = in_set ps' r; + val in_set_right' = + instantiate ctxt + [(Thm.ctyp_of_cterm x_in_set_right, xT)] + [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right}; + in discharge ctxt [in_set_r] in_set_right' end) + end; + +fun find_in_set ctxt t ct = + case find_tree t (Thm.term_of ct) of + SOME ps => in_set ctxt ps ct + | NONE => raise TERM ("find_in_set", [t, Thm.term_of ct]) + (* 1. First get paths x_path y_path of x and y in the tree. 2. For the common prefix descend into the tree according to the path @@ -210,34 +248,7 @@ val subtree = Thm.cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; val (_, [l, _, _, r]) = Drule.strip_comb subtree; - fun in_set ps tree = - let - val (_, [l, x, _, r]) = Drule.strip_comb tree; - val xT = Thm.ctyp_of_cterm x; - in - (case ps of - [] => - instantiate ctxt - [(Thm.ctyp_of_cterm x_in_set_root, xT)] - [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root} - | Left :: ps' => - let - val in_set_l = in_set ps' l; - val in_set_left' = - instantiate ctxt - [(Thm.ctyp_of_cterm x_in_set_left, xT)] - [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left}; - in discharge ctxt [in_set_l] in_set_left' end - | Right :: ps' => - let - val in_set_r = in_set ps' r; - val in_set_right' = - instantiate ctxt - [(Thm.ctyp_of_cterm x_in_set_right, xT)] - [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right}; - in discharge ctxt [in_set_r] in_set_right' end) - end; - + val in_set = in_set ctxt fun in_set' [] = raise TERM ("distinctTreeProver", []) | in_set' (Left :: ps) = in_set ps l | in_set' (Right :: ps) = in_set ps r; diff -r 00ffae972fc0 -r a0ab0dc28d3c src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Tue Oct 26 11:15:40 2021 +0100 +++ b/src/HOL/Statespace/state_fun.ML Tue Oct 26 16:22:03 2021 +0100 @@ -1,5 +1,6 @@ (* Title: HOL/Statespace/state_fun.ML - Author: Norbert Schirmer, TU Muenchen + Author: Norbert Schirmer, TU Muenchen, 2007 + Author: Norbert Schirmer, Apple, 2021 *) signature STATE_FUN = @@ -16,6 +17,8 @@ val ex_lookup_ss : simpset val lazy_conj_simproc : simproc val string_eq_simp_tac : Proof.context -> int -> tactic + + val trace_data : Context.generic -> unit end; structure StateFun: STATE_FUN = @@ -105,6 +108,17 @@ (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2); ); +fun trace_data context = + let + val (lookup_ss, ex_ss, active) = Data.get context + val pretty_ex_ss = Simplifier.pretty_simpset true (put_simpset ex_ss (Context.proof_of context)) + val pretty_lookup_ss = Simplifier.pretty_simpset true (put_simpset lookup_ss (Context.proof_of context)) + in + tracing ("state_fun ex_ss: " ^ Pretty.string_of pretty_ex_ss ^ + "\n ================= \n lookup_ss: " ^ Pretty.string_of pretty_lookup_ss ^ "\n " ^ + "active: " ^ @{make_string} active) + end + val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false))); val lookup_simproc = diff -r 00ffae972fc0 -r a0ab0dc28d3c src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Tue Oct 26 11:15:40 2021 +0100 +++ b/src/HOL/Statespace/state_space.ML Tue Oct 26 16:22:03 2021 +0100 @@ -1,5 +1,6 @@ (* Title: HOL/Statespace/state_space.ML - Author: Norbert Schirmer, TU Muenchen + Author: Norbert Schirmer, TU Muenchen, 2007 + Author: Norbert Schirmer, Apple, 2021 *) signature STATE_SPACE = @@ -42,19 +43,31 @@ val distinct_simproc : Simplifier.simproc - val get_comp : Context.generic -> string -> (typ * string) option + val is_statespace : Context.generic -> xstring -> bool + + val get_comp' : Context.generic -> string -> (typ * string list) option + val get_comp : Context.generic -> string -> (typ * string) option (* legacy wrapper, eventually replace by primed version *) + val get_comps : Context.generic -> (typ * string list) Termtab.table + val get_silent : Context.generic -> bool val set_silent : bool -> Context.generic -> Context.generic + val gen_lookup_tr : Proof.context -> term -> string -> term val lookup_swap_tr : Proof.context -> term list -> term val lookup_tr : Proof.context -> term list -> term val lookup_tr' : Proof.context -> term list -> term - val gen_update_tr : - bool -> Proof.context -> string -> term -> term -> term + val gen'_update_tr : + bool -> bool -> Proof.context -> string -> term -> term -> term + val gen_update_tr : (* legacy wrapper, eventually replace by primed version *) + bool -> Proof.context -> string -> term -> term -> term + val update_tr : Proof.context -> term list -> term val update_tr' : Proof.context -> term list -> term + + val trace_name_space_data: Context.generic -> unit + val trace_state_space_data: Context.generic -> unit end; structure StateSpace : STATE_SPACE = @@ -83,11 +96,66 @@ | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys else sorted_subset eq (x::xs) ys; +fun comps_of_distinct_thm thm = Thm.prop_of thm + |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free) |> sort_strings; + +fun insert_tagged_distinct_thms tagged_thm tagged_thms = + let + fun ins t1 [] = [t1] + | ins (t1 as (names1, _)) ((t2 as (names2, _))::thms) = + if Ord_List.subset string_ord (names1, names2) then t2::thms + else if Ord_List.subset string_ord (names2, names1) then ins t1 thms + else t2 :: ins t1 thms + in + ins tagged_thm tagged_thms + end + +fun join_tagged_distinct_thms tagged_thms1 tagged_thms2 = + tagged_thms1 |> fold insert_tagged_distinct_thms tagged_thms2 + +fun tag_distinct_thm thm = (comps_of_distinct_thm thm, thm) +val tag_distinct_thms = map tag_distinct_thm + +fun join_distinct_thms thms1 thms2 = + if pointer_eq (thms1, thms2) then thms1 + else join_tagged_distinct_thms (tag_distinct_thms thms1) (tag_distinct_thms thms2) + |> map snd + +fun insert_distinct_thm thm thms = join_distinct_thms thms [thm] + +val join_distinctthm_tab = Symtab.join (fn name => fn (thms1, thms2) => join_distinct_thms thms1 thms2) +fun join_declinfo_entry name (T1:typ, names1:string list) (T2, names2) = + let + fun typ_info T names = @{make_string} T ^ " " ^ Pretty.string_of (Pretty.str_list "(" ")" names); + in + if T1 = T2 then (T1, distinct (op =) (names1 @ names2)) + else error ("statespace component '" ^ name ^ "' disagrees on type:\n " ^ + typ_info T1 names1 ^ " vs. " ^ typ_info T2 names2 + ) + end +fun guess_name (Free (x,_)) = x + | guess_name _ = "unknown" + +val join_declinfo = Termtab.join (fn trm => uncurry (join_declinfo_entry (guess_name trm))) + + +(* + A component might appear in *different* statespaces within the same context. However, it must + be mapped to the same type. Note that this information is currently only properly maintained + within contexts where all components are actually "fixes" and not arbitrary terms. Moreover, on + the theory level the info stays empty. + + This means that on the theory level we do not make use of the syntax and the tree-based distinct simprocs. + N.B: It might still make sense (from a performance perspective) to overcome this limitation + and even use the simprocs when a statespace is interpreted for concrete names like HOL-strings. + Once the distinct-theorem is proven by the interpretation the simproc can use the positions in + the tree to derive distinctness of two strings vs. HOL-string comparison. + *) type namespace_info = - {declinfo: (typ*string) Termtab.table, (* type, name of statespace *) - distinctthm: thm Symtab.table, + {declinfo: (typ * string list) Termtab.table, (* type, names of statespaces of component *) + distinctthm: thm list Symtab.table, (* minimal list of maximal distinctness-assumptions for a component name *) silent: bool }; @@ -98,19 +166,24 @@ fun merge ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1}, {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T = - {declinfo = Termtab.merge (K true) (declinfo1, declinfo2), - distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2), + {declinfo = join_declinfo (declinfo1, declinfo2), + distinctthm = join_distinctthm_tab (distinctthm1, distinctthm2), silent = silent1 andalso silent2 (* FIXME odd merge *)} ); +fun trace_name_space_data context = + tracing ("NameSpaceData: " ^ @{make_string} (NameSpaceData.get context)) + fun make_namespace_data declinfo distinctthm silent = {declinfo=declinfo,distinctthm=distinctthm,silent=silent}; fun update_declinfo (n,v) ctxt = - let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt; + let + val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt; + val v = apsnd single v in NameSpaceData.put - (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt + (make_namespace_data (Termtab.map_default (n,v) (join_declinfo_entry (guess_name n) v) declinfo) distinctthm silent) ctxt end; fun set_silent silent ctxt = @@ -158,6 +231,12 @@ fun merge data : T = Symtab.merge (K true) data; ); +fun is_statespace context name = + Symtab.defined (StateSpaceData.get context) (Locale.intern (Context.theory_of context) name) + +fun trace_state_space_data context = + tracing ("StateSpaceData: " ^ @{make_string} (StateSpaceData.get context)) + fun add_statespace name args parents components types ctxt = StateSpaceData.put (Symtab.update_new (name, {args=args,parents=parents, @@ -171,27 +250,58 @@ fun mk_free ctxt name = if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name then - let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden; - in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end - else NONE + let + val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden; + val free = Free (n', Proof_Context.infer_type ctxt (n', dummyT)) + in SOME (free) end + else (tracing ("variable not fixed or declared: " ^ name); NONE) fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name; + +fun get_dist_thm2 ctxt x y = + (let + val dist_thms = [x, y] |> map (#1 o dest_Free) + |> map (these o get_dist_thm (Context.Proof ctxt)) |> flat; + + fun get_paths dist_thm = + let + val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; + val tree = Thm.term_of ctree; + val x_path = the (DistinctTreeProver.find_tree x tree); + val y_path = the (DistinctTreeProver.find_tree y tree); + in SOME (dist_thm, x_path, y_path) end + handle Option.Option => NONE + + val result = get_first get_paths dist_thms + in + result + end) + + +fun get_comp' ctxt name = + mk_free (Context.proof_of ctxt) name + |> Option.mapPartial (fn t => + let + val declinfo = #declinfo (NameSpaceData.get ctxt) + in + case Termtab.lookup declinfo t of + NONE => (* during syntax phase, types of fixes might not yet be constrained completely *) + AList.lookup (fn (x, Free (n,_)) => n = x | _ => false) (Termtab.dest declinfo) name + | some => some + end) + +(* legacy wrapper *) fun get_comp ctxt name = - Option.mapPartial - (Termtab.lookup (#declinfo (NameSpaceData.get ctxt))) - (mk_free (Context.proof_of ctxt) name); + get_comp' ctxt name |> Option.map (apsnd (fn ns => if null ns then "" else hd ns)) +fun get_comps ctxt = #declinfo (NameSpaceData.get ctxt) (*** Tactics ***) fun neq_x_y ctxt x y = (let - val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x))); - val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; - val tree = Thm.term_of ctree; - val x_path = the (DistinctTreeProver.find_tree x tree); - val y_path = the (DistinctTreeProver.find_tree y tree); + val (dist_thm, x_path, y_path) = the (get_dist_thm2 ctxt x y); val thm = DistinctTreeProver.distinctTreeProver ctxt dist_thm x_path y_path; in SOME thm end handle Option.Option => NONE) @@ -240,8 +350,6 @@ val dist_thm_name = distinct_compsN; val dist_thm_full_name = dist_thm_name; - fun comps_of_thm thm = Thm.prop_of thm - |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free); fun type_attr phi = Thm.declaration_attribute (fn thm => fn context => (case context of @@ -249,12 +357,8 @@ | Context.Proof ctxt => let val {declinfo,distinctthm=tt,silent} = NameSpaceData.get context; - val all_names = comps_of_thm thm; - fun upd name tt = - (case Symtab.lookup tt name of - SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names - then Symtab.update (name,thm) tt else tt - | NONE => Symtab.update (name,thm) tt) + val all_names = comps_of_distinct_thm thm; + fun upd name = Symtab.map_default (name, [thm]) (fn thms => insert_distinct_thm thm thms) val tt' = tt |> fold upd all_names; val context' = @@ -377,7 +481,8 @@ in Context.proof_map (update_declinfo (Morphism.term phi (Free (n,nT)),v)) end; - in ctxt |> fold upd updates end; + val ctxt' = ctxt |> fold upd updates + in ctxt' end; in Context.mapping I upd_prf ctxt end; @@ -545,20 +650,9 @@ (*** parse/print - translations ***) -local - -fun map_get_comp f ctxt (Free (name,_)) = - (case (get_comp ctxt name) of - SOME (T,_) => f T T dummyT - | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*))) - | map_get_comp _ _ _ = Syntax.free "arbitrary"; - -fun name_of (Free (n,_)) = n; - -in fun gen_lookup_tr ctxt s n = - (case get_comp (Context.Proof ctxt) n of + (case get_comp' (Context.Proof ctxt) n of SOME (T, _) => Syntax.const \<^const_name>\StateFun.lookup\ $ Syntax.free (project_name T) $ Syntax.free n $ s @@ -576,7 +670,7 @@ fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n; fun lookup_tr' ctxt [_ $ Free (prj, _), n as (_ $ Free (name, _)), s] = - (case get_comp (Context.Proof ctxt) name of + (case get_comp' (Context.Proof ctxt) name of SOME (T, _) => if prj = project_name T then Syntax.const "_statespace_lookup" $ s $ n @@ -584,33 +678,36 @@ | NONE => raise Match) | lookup_tr' _ _ = raise Match; -fun gen_update_tr id ctxt n v s = +fun gen'_update_tr const_val id ctxt n v s = let fun pname T = if id then \<^const_name>\Fun.id\ else project_name T; fun iname T = if id then \<^const_name>\Fun.id\ else inject_name T; + val v = if const_val then (Syntax.const \<^const_name>\K_statefun\ $ v) else v in - (case get_comp (Context.Proof ctxt) n of + (case get_comp' (Context.Proof ctxt) n of SOME (T, _) => Syntax.const \<^const_name>\StateFun.update\ $ Syntax.free (pname T) $ Syntax.free (iname T) $ - Syntax.free n $ (Syntax.const \<^const_name>\K_statefun\ $ v) $ s + Syntax.free n $ v $ s | NONE => if get_silent (Context.Proof ctxt) then Syntax.const \<^const_name>\StateFun.update\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.const \<^const_syntax>\undefined\ $ - Syntax.free n $ (Syntax.const \<^const_name>\K_statefun\ $ v) $ s + Syntax.free n $ v $ s else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined", [])) end; +val gen_update_tr = gen'_update_tr true + fun update_tr ctxt [s, x, v] = (case Term_Position.strip_positions x of - Free (n, _) => gen_update_tr false ctxt n v s + Free (n, _) => gen'_update_tr true false ctxt n v s | _ => raise Match); fun update_tr' ctxt [_ $ Free (prj, _), _ $ Free (inj, _), n as (_ $ Free (name, _)), (Const (k, _) $ v), s] = if Long_Name.base_name k = Long_Name.base_name \<^const_name>\K_statefun\ then - (case get_comp (Context.Proof ctxt) name of + (case get_comp' (Context.Proof ctxt) name of SOME (T, _) => if inj = inject_name T andalso prj = project_name T then Syntax.const "_statespace_update" $ s $ n $ v @@ -619,7 +716,7 @@ else raise Match | update_tr' _ _ = raise Match; -end; + (*** outer syntax *)