Paolo Giarrusso (Nov 14 2020 at 01:40): Paolo Giarrusso (Nov 14 2020 at 01:40):IMHO, making Definition foo local should prevent it from being _imported_. That works.
However, as soon as the containing module bar is required, bar.foo should IMHO work. That doesn't always work.
inside a file, Local Definition works as I'd expect:
Module Import A.
Local Definition test1 := 1.
Definition test2 := 1.
End A.
Local Definition test2 := A.test1.
Definition test3 := A.test1.
I'm more confused by the semantics wrt Require:
Require Import D.testLocalDefA.
(* OK *)
Definition test3' := test3.
Definition test3'a := testLocalDefA.test3.
(* OK *)
Fail Definition test3 := test2.
Definition test3 := testLocalDefA.test2.
(* WAT? *)
Fail Definition test4 := A.test1.
Definition test4 := testLocalDefA.A.test1.
Definition test5 := A.test2.
Definition test5' := testLocalDefA.A.test2.
AFAICS, using A.test1 requires one more qualification than I'd expect. I have no idea why.
Paolo Giarrusso (Nov 14 2020 at 01:44):Possible explanation: Import skips local definitions recursively?
Paolo Giarrusso (Nov 14 2020 at 01:45):so Import A skips making test1 available, correctly, but when Import D.testLocalDefA imports testLocalDefA, and it makes A globally available, it recursively filters out test1.
Li-yao (Nov 14 2020 at 01:46):Local makes it so the only way to use a name is to qualify it completely.
Paolo Giarrusso (Nov 14 2020 at 01:46):"qualify it completely" is not true
Paolo Giarrusso (Nov 14 2020 at 01:46):see above
Paolo Giarrusso (Nov 14 2020 at 01:47):I can skip the initial prefix D for some reason, and however many levels appear there.
Paolo Giarrusso (Nov 14 2020 at 01:48):so if D.testLocalDefA. where instead A.B.C.D.testLocalDefA., I'd just need to repeat testLocalDefA
Paolo Giarrusso (Nov 14 2020 at 01:48):(as if Require ignored local instead? dunno)
Paolo Giarrusso (Nov 14 2020 at 01:48):(this assumes that Import works by deep-copying dictionaries, instead of linking them, which is a pretty weird idea, but you can ignore that part if it doesn't help)
Paolo Giarrusso (Nov 14 2020 at 01:49):@Li-yao but would that semantics be useful/desirable/predictable?
Paolo Giarrusso (Nov 14 2020 at 01:51):things work as I'd expect without nested modules... so I noticed because I failed to make sense of the behavior
Li-yao (Nov 14 2020 at 01:52):Okay I thought it was a little stricter than that. :shrug:
Paolo Giarrusso (Nov 14 2020 at 01:53):Well you weren't alone:
They [Definition and Example] can take the local attribute, which makes the defined ident accessible by Import and its variants only through their fully qualified names.
https://coq.github.io/doc/v8.12/refman/language/core/definitions.html#coq:cmd.definition
Li-yao (Nov 14 2020 at 01:57):Modulo the prefix D, your examples seem to work as described by that sentence, don't they?
Paolo Giarrusso (Nov 14 2020 at 01:58):Sorta. In another example, after From bedrock.lang.cpp.logic Require Import simple_pointers., I can just start from simple_pointers.
Paolo Giarrusso (Nov 14 2020 at 02:00):that is, if simple_pointers contains Module A with local def test1, you must write simple_pointers.A.test1
Paolo Giarrusso (Nov 14 2020 at 02:01):so, my theory works if simple_pointers is bound into the top-level by Require (which ignores the Local attribute), while A is bound by Import (which discards definitions marked Local).
Théo Zimmermann (Nov 14 2020 at 11:14):Probably worth an issue, to decide whether the documentation should be fixed or the behavior changed.
Gaëtan Gilbert (Nov 14 2020 at 11:34):Local Definition means Import does nothing, but Require still has an effect
Require Foo makes Foo available without needing to prefix it
so for instance after Require List. you can do Import List. instead of having to do Import Coq.Lists.List.
Last updated: Oct 13 2024 at 01:02 UTC