Email Gateway (Aug 18 2022 at 16:18): Email Gateway (Aug 18 2022 at 16:18):From: John Munroe <munddr@gmail.com>
Hi all,
I'm trying to increase the unification depth in the theory using
declare [[unification_search_bound = 70]], but it seems there's no
effect and stays at 60.
theory Test
imports Complex_Main
begin
declare [[unification_search_bound = 70]]
...
Using an unsynchronized reference, changing the last line of Unify.hounifiers to
in (ref := search_bnd; add_unify 1 ((env,dps), Seq.empty)) end;
and reading off ref, it still shows 60.
It seems that Unify.search_bound is fixed to the value of
Unify.search_bound_value, which is default to 60 due to
val search_bound_value = Config.declare true "unify_search_bound" (K
(Config.Int 60));
val search_bound = Config.int search_bound_value;
...
fun hounifiers...
val search_bnd = Config.get_global thy search_bound
...
if tdepth > search_bnd then
(warning "Unification bound exceeded"; (Seq.pull reseq))
...
Any help will be appreciated.
Thanks
John
Email Gateway (Aug 18 2022 at 16:18):From: Makarius <makarius@sketis.net>
Did you really try it as above? The configuration option is called
"unify_search_bound". Here is an example in Isabelle2009-2:
declare [[unify_search_bound = 70]]
ML {* Config.get_global @{theory} Unify.search_bound *}
ML {* Config.get @{context} Unify.search_bound *}
For historical reasons there is a snag: unify options can only be modified
in a global context. E.g. consider:
lemma A
using [[unify_search_bound = 42]]
### Ignoring local change of global option "unify_search_bound"
As usual in Proof General, such warnings are easily overlooked. As usual,
it will be much more visible in the Isabelle/jEdit prover IDE, although
I've already had some complaints that warnings are too prominent there.
Makarius
Email Gateway (Aug 18 2022 at 16:19):From: John Munroe <munddr@gmail.com>
Sorry, my mistake. Indeed I tried unify_search_bound = 5. I see that
the configuration itself has changed, but the function hounifiers
doesn't seem to see the update:
If I do:
declare [[unify_search_bound = 70]]
ML {* Config.get_global @{theory} Unify.search_bound *}
ML {* Config.get @{context} Unify.search_bound *}
I do see 70 for both.
But if I do
ML {!Unify.ref}
even after having run hounifiers, via, e.g., Unify.matchers, I see 60.
Here's how ref is assigned:
fun hounifiers (thy,env, tus : (term*term)list)
: (Envir.env * (term*term)list)Seq.seq =
let
...
in (ref := search_bnd; add_unify 1 ((env, dps), Seq.empty)) end;
So It seems hounifiers can't see the update. If I change it to
something more extreme, like 5, the unifier itself doesn't behave as
if it was 5 but as if it was 60.
Thanks
John
Email Gateway (Aug 18 2022 at 16:20):From: munddr@gmail.com
Here's how ref is assigned:
fun hounifiers (thy,env, tus : (term*term)list)
: (Envir.env * (term*term)list)Seq.seq =
let
...
in (ref := search_bnd; add_unify 1 ((env, dps), Seq.empty)) end;
Just a follow-up question: If unify_search_bound is updated, I should
expect to see ref to be updated there, right?
Thanks
John
So It seems hounifiers can't see the update. If I change it to
something more extreme, like 5, the unifier itself doesn't behave as
if it was 5 but as if it was 60.
Thanks
John
On Fri, Nov 26, 2010 at 1:00 PM, Makarius makarius@sketis.net> wrote:
On Fri, 26 Nov 2010, John Munroe wrote:
>
theory Test
imports Complex_Main
begin
>
declare [[unification_search_bound = 70]]
...
>
It seems that Unify.search_bound is fixed to the value of
Unify.search_bound_value, which is default to 60 due to
>
Did you really try it as above? The configuration option is called
"unify_search_bound". Here is an example in Isabelle2009-2:
>
declare [[unify_search_bound = 70]]
>
ML {* Config.get_global @{theory} Unify.search_bound *}
ML {* Config.get @{context} Unify.search_bound *}
>
For historical reasons there is a snag: unify options can only be
modified
in a global context. Eg consider:
>
lemma A
using [[unify_search_bound = 42]]
>
Ignoring local change of global option "unify_search_bound"
>
As usual in Proof General, such warnings are easily overlooked. As
usual,
it will be much more visible in the Isabelle/jEdit prover IDE, although
I've
already had some complaints that warnings are too prominent there.
>
>
Makarius
>
Email Gateway (Aug 18 2022 at 16:20):From: Makarius <makarius@sketis.net>
Hard to say from this tiny extract of the source above. There could be
some unexpected effects due to lazy evaluation or parallelism. Mutable
references are a source of many problems and being gradually removed from
the system.
For experimentation, it is usually easier to print out something using
writeln or similar.
Makarius
Email Gateway (Aug 18 2022 at 16:21):From: John Munroe <munddr@gmail.com>
Hard to say from this tiny extract of the source above. There could be some
unexpected effects due to lazy evaluation or parallelism. Mutable references
are a source of many problems and being gradually removed from the system.For experimentation, it is usually easier to print out something using
writeln or similar.
OK. I've tried it with "writeln (Int.toString search_bnd)" instead and
I get a reading of 60 as well, even after I've changed it to 5 with
"declare [[unify_search_bound=5]]". I've looked at some of the
unifiers and they are definitely deeper than 5 levels, e.g.,
%a::nat => nat.
a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a ((h::(nat => bool) => nat)
(s::nat => bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
Thanks
John
Makarius
Email Gateway (Aug 18 2022 at 16:21):From: Makarius <makarius@sketis.net>
That's very strange. Are you sure you have the correct context in your
example? One where the "declare [[unify_search_bound=5]]" is effective?
Can you show a self-contained snippet of theory source text?
Makarius
Email Gateway (Aug 18 2022 at 16:22):From: munddr@gmail.com
On Nov 28, 2010 4:22pm, Makarius <makarius@sketis.net> wrote:
On Sun, 28 Nov 2010, John Munroe wrote:
I've tried it with "writeln (Int.toString search_bnd)" instead and I get
a reading of 60 as well, even after I've changed it to 5 with "declare
[[unify_search_bound=5]]". I've looked at some of the unifiers and they
are definitely deeper than 5 levels, eg,
%a::nat => nat.
a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a (a
(a (a (a (a (a (a (a (a (a (a (a (a ((h::(nat => bool) => nat)
(s::nat => bool))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
That's very strange. Are you sure you have the correct context in your
example? One where the "declare [[unify_search_bound=5]]" is effective?
Indeed, it was a problem with my context.
Thanks
John
Can you show a self-contained snippet of theory source text?
Makarius
Last updated: Apr 25 2024 at 16:19 UTC