# HG changeset patch # User Norbert Schirmer # Date 1605196912 -3600 # Node ID 5ac762b5311967e28fac4f8f2f1553850b7d3adf # Parent 42fb56041c11291c9d97c36f70886484f419f4c2 generalized component lookup for syntax and distinctness proofs. added some tracing. diff -r 42fb56041c11 -r 5ac762b53119 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Mon Oct 25 23:10:06 2021 +0200 +++ b/src/HOL/Statespace/StateSpaceEx.thy Thu Nov 12 17:01:52 2020 +0100 @@ -12,6 +12,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\ @@ -192,39 +193,69 @@ 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 on 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' statespece 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 \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 \Note that the distinctness theorem for @{locale vars2} is selected here to do the proof.\ +lemma "s\k = s\k" + by simp + +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 42fb56041c11 -r 5ac762b53119 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Mon Oct 25 23:10:06 2021 +0200 +++ b/src/HOL/Statespace/state_fun.ML Thu Nov 12 17:01:52 2020 +0100 @@ -16,6 +16,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 +107,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 42fb56041c11 -r 5ac762b53119 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Mon Oct 25 23:10:06 2021 +0200 +++ b/src/HOL/Statespace/state_space.ML Thu Nov 12 17:01:52 2020 +0100 @@ -42,19 +42,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 +95,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 +165,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 +230,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 +249,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 +349,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 +356,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 +480,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 +649,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 @@ -566,7 +659,8 @@ if get_silent (Context.Proof ctxt) then Syntax.const \<^const_name>\StateFun.lookup\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.free n $ s - else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", [])); + else (trace_name_space_data (Context.Proof ctxt); + raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []))); fun lookup_tr ctxt [s, x] = (case Term_Position.strip_positions x of @@ -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 *)