Stream: Beginner Questions

Topic: Executing functions defined in locales

Maximilian Vollath (Mar 03 2025 at 16:39):

I'm having trouble executing functions and definitions that are defined inside a locale. Do I have to first generate the code via something like code_pred?

theory Broken_Locales
imports Main
begin

locale my_locale =
  fixes x :: nat
begin
abbreviation "suc ≡ x + 1"
definition "sucsuc ≡ x + 2"
end

value "my_locale.suc 4" (* works *)
value "my_locale.sucsuc 4" (* No code equations for my_locale.sucsuc *)

interpretation my_x : my_locale 4 .
value "my_x.suc" (* works *)
value "my_x.sucsuc" (* "Num.nat_of_num" is not a constructor ... *)

end

The project I'm working in has an absolute ton of functions defined inside locales so I'm hoping for a solution where I won't have to re-define every single one.

Maximilian Schäffeler (Mar 03 2025 at 19:43):

There's a section on that in the codegen manual, let me know if you have problems getting it to work in your scenario.

Maximilian Vollath (Mar 04 2025 at 09:41):

Thank you! I got it.

Maximilian Vollath (Mar 04 2025 at 10:23):

Nevermind, I have a new issue with this: duplicate fact declaration.
To be concrete, I am working with AI_Planning_Languages_Semantics in the AFP.

theory Running_Example_wip
  imports
    "AI_Planning_Languages_Semantics.PDDL_STRIPS_Checker"
begin

definition "my_problem ≡ Problem (Domain [] [] [] []) [] [] ⊥"

global_interpretation inst0 : ast_problem my_problem
  defines def1 = inst0.of_type1
  (* TODO: add the other functions. *)
  .

(* Duplicate fact declaration "Running_Example_wip.inst0.mp_objT_correct" vs. "Running_Example_wip.inst0.mp_objT_correct"⌂
The above error(s) occurred while activating facts of locale instance
inst0 : ast_problem "my_problem" *)

end

The problem is that there are both ast_domain.mp_objT_correct and ast_problem.mp_objT_correct. Instantiating an ast_problem also instantiates a corresponding ast_domain. It goes away if I just locally change one of their names, but that's not sustainable. hide_fact also doesn't seem to solve it.

Fabian Huch (Mar 04 2025 at 10:39):

don't know if there is a trick, but this is a design problem of the locale hierarchy (can't be instantiated in a global context).

Maximilian Schäffeler (Mar 05 2025 at 12:23):

You could try to give the instantiation of the
corresponding domain an optional qualifier: sublocale dom?: ast_domain ….
I don’t know whether this helps with your specific hierarchy.
The feature is explained towards the end of section 5.4 of the locale manual.

Last updated: Mar 09 2025 at 12:28 UTC