From 53f44dea1e7763b94a98037629a3c608a9a06c44 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 27 Aug 2024 19:54:38 +1000 Subject: [PATCH] lib: Requalify_Test: add example of requalify-hide-requalify Document/test surprising interactions of hide_const, locales and requalify for the purposes of temporarily making arch-specific constants visible in theory scope. Signed-off-by: Rafal Kolanski --- lib/test/Requalify_Test.thy | 47 +++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/lib/test/Requalify_Test.thy b/lib/test/Requalify_Test.thy index 009eea83da..a3eda0fe83 100644 --- a/lib/test/Requalify_Test.thy +++ b/lib/test/Requalify_Test.thy @@ -269,6 +269,53 @@ arch_requalify_consts (in Arch) (A) arch_specific_const_a term Arch.arch_specific_const_a +section "Specific tests" + +subsection \Temporary requalification of, hiding of, and re-exposing of constants\ + +(* This kind of approach can be used for tools such at the C Parser, which are not aware of the Arch + locale and might need to refer to constants directly in internal annotations. *) + +context Arch begin arch_global_naming +datatype vmpage_size = + ARCHSmallPage +end +arch_requalify_types vmpage_size + +context Arch begin global_naming vmpage_size +requalify_consts ARCHSmallPage +end + +(* both now visible in generic context *) +typ vmpage_size +term vmpage_size.ARCHSmallPage +term ARCHSmallPage (* note: the direct constructor name is not accessible due to qualified export *) + +(* temporary global exposure is done, hide vmpage sizes again *) +hide_const + vmpage_size.ARCHSmallPage + +find_consts name:ARCHSmallPage +(* finds one constant (despite it being hidden), e.g. on ARM: + Requalify.ARM.vmpage_size.ARMSmallPage :: "vmpage_size" + but note that this constant is inaccessible from theory scope: + term Requalify_Test.AARCH64.vmpage_size.ARCHSmallPage + will result in Inaccessible constant: "Requalify_Test.ARM.vmpage_size.ARCHSmallPage" *) + +(* Arch-specific, in actual use replace ARCH with actual architecture such as ARM *) +context Arch begin +term vmpage_size.ARCHSmallPage (* despite being hidden in theory scope, it's still visible in Arch *) +global_naming "ARCH.vmpage_size" requalify_consts ARCHSmallPage +global_naming "ARCH" requalify_consts ARCHSmallPage +end + +term ARCH.ARCHSmallPage (* now accessible under specific qualified name *) +term ARCH.vmpage_size.ARCHSmallPage (* now accessible under specific qualified name *) +term Requalify_Test.ARCH.vmpage_size.ARCHSmallPage (* fully qualified name *) +(* but be aware, these are only aliases to the original constant! *) +find_consts name:ARCHSmallPage (* still only Requalify_Test.ARM.vmpage_size.ARCHSmallPage *) + + section "Misc tests / usage examples" locale Requalify_Locale