From c11037f09ec3e3d9e2895e13a017d630e38303fc Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 27 Aug 2024 14:32:58 +1000 Subject: [PATCH] lib: Requalify: better document annotation Previous attempts to update the code to allow ctrl+clicking on names resulted in markup overlap errors for arch_requalify commands. This was due to a misconception that YXML strings already containing correct position information (e.g. obtained via Parse.const) would be used directly by Proof_context.read_const/read_type_name. This is not the case. Instead, position information is adjusted for the content length, and since we add a prefix for L4V_ARCH, we got annotation that did not match the document text. After hours of digging to uncover the above issue, we get this: * the "check_parsed_nm" in gen_requalify was not an extra check, but a hook to do document annotation; updated comments * use Proof_Context.check_const/check_type_name with parsed position of Parse.name, and manually report resulting markup * since the above works for arch_requalify_const, the normal requalify_const becomes a simpler instance * the whole Parse.const/Parse.typ was a red herring and ultimately did not add anything to the code except for read_const/read_type_name interaction; removed The resulting code is simpler; a large cautionary comment remains for future generations. Signed-off-by: Rafal Kolanski --- lib/Requalify.thy | 81 ++++++++++++++++++++++++----------------------- 1 file changed, 41 insertions(+), 40 deletions(-) diff --git a/lib/Requalify.thy b/lib/Requalify.thy index 133806fe75..59ae3a37b8 100644 --- a/lib/Requalify.thy +++ b/lib/Requalify.thy @@ -98,21 +98,22 @@ val arch_global_opts = Scan.optional (Args.parens arch_suffix) "" in -fun gen_requalify get_proper_nm parse_nm check_parsed_nm alias_fn arch = +fun gen_requalify get_proper_nm check_parsed_nm alias_fn arch = let val options = if arch then arch_options else generic_options in - (Parse.opt_target -- options -- Scan.repeat1 (Parse.position (Scan.ahead parse_nm -- Parse.name)) + (Parse.opt_target -- options -- Scan.repeat1 (Parse.position Parse.name) >> (fn ((target, (aliasing, arch_suffix)), names) => Toplevel.local_theory NONE target (fn lthy => let val global_ctxt = Proof_Context.theory_of lthy |> Proof_Context.init_global - fun requalify_entry ((entry, orig_name), pos) lthy = + fun requalify_entry (orig_name, pos) lthy = let val name = if arch then arch_prefix arch_suffix ^ "." ^ orig_name else orig_name val local_name = get_proper_nm lthy name; - val _ = check_parsed_nm lthy (entry, (local_name, pos)); + (* look up name again for purposes of document markup (i.e. ctrl+click on names) *) + val _ = check_parsed_nm lthy (local_name, pos); (* Check whether the short (base) name is already available in theory context if no locale target is supplied and the "aliasing" option is not supplied. @@ -136,48 +137,53 @@ val get_const_nm = ((fst o dest_Const) oo (Proof_Context.read_const {proper = tr val get_type_nm = ((fst o dest_Type) oo (Proof_Context.read_type_name {proper = true, strict = false})) val get_fact_nm = (fst oo global_fact) -(* For a theorem name, we want to additionally make sure that global fact names found by - global_fact are accessible in the current context. *) -fun check_fact lthy (_, (nm, pos)) = Proof_Context.get_fact lthy (Facts.Named ((nm,pos), NONE)) +(* For the arch_requalify commands, we prefix the const/type name based on L4V_ARCH and A/H option. + This means we have to be careful when resolving names and marking up the document. -(* replace text in all Text nodes in YXML-encoded string entry with new_text *) -fun replace_yxml_text new_text = -let - fun tree_text (XML.Text _) = XML.Text new_text - | tree_text (XML.Elem (node, trees)) = (XML.Elem (node, map tree_text trees)) -in - YXML.string_of o tree_text o YXML.parse -end + What is completely non-obvious is that Proof_Context.read_const and Proof_Context.read_type_name + are sensitive to YXML markup information embedded in the supplied string. When such information + is available, they will use it to mark up the document. However, in the process they will invoke + Input.source_content, which will make sure that the position information conforms to the content + length. This is *bad news* for arch_requalify, because when the user asks for "name", we treat it + as something like "ARM_A.name". + So if we use Parse.const/Parse.typ we'll get an annotated string: + name + If we tweak "name" to become "ARM_A.name" instead, the read_const/read_type_name functions will + sync the length and attempt to annotate it as: + name + which is a larger range than the user gave us, leading to errors about overlapping ranges. + This means that the nice option of using Parse.const + Proof_Context.read_const can't be used + here. -(* These versions, prior to resolving the const/type name, override that name in the parsed - YXML-encoded string entry with a name that will actually resolve to something, while preserving - other parse data such as parsed document location. - This updates the document markup at the original parse location of entry with a reference to the - const/type named by "name", allowing the user to ctrl+click to jump to the const/type definition. + Instead, we use read_const/read_type_name on user-supplied names to get resolved names as normal + strings, which we then supply to Proof_Context.check_const/check_type_name along with the + position from Parse.position to get markup reports which we apply manually. - For example, if the user requested "arch_requalify_consts (A) some_const", then they are - targeting something like "ARM_A.some_const", and expect to be able to jump to its definition. + For theorems, document annotation appears to be included in Proof_context.get_fact. *) - This isn't necessary for facts, as those use parsed position of "name" directly via - Proof_Context.get_fact, which appears not available for read_const/read_type_name. *) -fun arch_const_nm lthy entry name = get_const_nm lthy (replace_yxml_text name entry) -fun arch_type_nm lthy entry name = get_type_nm lthy (replace_yxml_text name entry) +fun check_const lthy (nm, pos) = + Proof_Context.check_const {proper = true, strict = false} lthy (nm, [pos]) + |> #2 |> Context_Position.reports @{context} + +fun check_type_name lthy (nm, pos) = + Proof_Context.check_type_name {proper = true, strict = false} lthy (nm, pos) + |> #2 |> Context_Position.reports @{context} + +fun check_fact lthy (nm, pos) = Proof_Context.get_fact lthy (Facts.Named ((nm, pos), NONE)) in val _ = Outer_Syntax.command @{command_keyword requalify_consts} "alias const with current naming" - (gen_requalify get_const_nm Parse.const (fn lthy => fn (e, _) => get_const_nm lthy e) const_alias - false) + (gen_requalify get_const_nm check_const const_alias false) val _ = Outer_Syntax.command @{command_keyword requalify_types} "alias type with current naming" - (gen_requalify get_type_nm Parse.typ (fn lthy => fn (e, _) => get_type_nm lthy e) type_alias - false) + (gen_requalify get_type_nm check_type_name type_alias false) val _ = Outer_Syntax.command @{command_keyword requalify_facts} "alias fact with current naming" - (gen_requalify get_fact_nm Parse.thm check_fact alias_fact false) + (gen_requalify get_fact_nm check_fact alias_fact false) val _ = Outer_Syntax.command @{command_keyword global_naming} "change global naming of context block" @@ -188,27 +194,22 @@ val _ = (* Arch variants use the L4V_ARCH variable and an additional A/H option, so that when L4V_ARCH=ARM "arch_requalify_consts (H) const" becomes "requalify_consts ARM_H.const" - This allows them to be used in a architecture-generic theory. - - For consts and types, we need to perform text replacement in the YXML entry to combine the parse - location with the right const/type name (see arch_const_nm and arch_type_nm). *) + This allows them to be used in a architecture-generic theory. *) val _ = Outer_Syntax.command @{command_keyword arch_requalify_consts} "alias const with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" - (gen_requalify get_const_nm Parse.const (fn lthy => fn (e, (nm, _)) => arch_const_nm lthy e nm) - const_alias true) + (gen_requalify get_const_nm check_const const_alias true) val _ = Outer_Syntax.command @{command_keyword arch_requalify_types} "alias type with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" - (gen_requalify get_type_nm Parse.typ (fn lthy => fn (e, (nm, _)) => arch_type_nm lthy e nm) - type_alias true) + (gen_requalify get_type_nm check_type_name type_alias true) val _ = Outer_Syntax.command @{command_keyword arch_requalify_facts} "alias fact with current naming, but prepend \"($L4V_ARCH)_[A|H].\" using env. variable" - (gen_requalify get_fact_nm Parse.thm check_fact alias_fact true) + (gen_requalify get_fact_nm check_fact alias_fact true) val _ = Outer_Syntax.command @{command_keyword arch_global_naming}