Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] File.use function

Email Gateway (Aug 17 2022 at 14:43):

From: Clément Hurlin <Clement.Hurlin@esial.uhp-nancy.fr>
Hi,

As part of my work to extend the rv tactic, I'm trying to use a
file containing ML code using "File.use". The file used contained the
following code :
val proof_congr = X
val proof_inst = Y

And at the ML level, I do :

val proof_congr = []
val proof_inst = []

val _ = File.use (Path.unpack proof_hints_fn)

Even if the isabelle buffer in proofgeneral shows that proof_congr
and proof_inst are filled with X and Y, it is actually not the case at
the ML level : proof_congr and proof_inst are still the empty list :O(
Why ?

Thanks for your help,
Clément

Email Gateway (Aug 17 2022 at 14:43):

From: Makarius <makarius@sketis.net>
On Sun, 30 Apr 2006, Clément Hurlin wrote:

I'm trying to use a file containing ML code using "File.use".

Why use the internal File.use instead of the toplevel use (which is
ThyInfo.use)?

The file used contained the following code :

val proof_congr = X
val proof_inst = Y

And at the ML level, I do :

val proof_congr = []
val proof_inst = []

val _ = File.use (Path.unpack proof_hints_fn)

Even if the isabelle buffer in proofgeneral shows that proof_congr and
proof_inst are filled with X and Y, it is actually not the case at the
ML level : proof_congr and proof_inst are still the empty list :O( Why ?

I do not fully understand your setup. There might be a misunderstanding
concerning the meaning of ML toplevel declarations: proof_congr and
proof_inst cannot be ``filled'' with other values, because they are
statically fixed bindings to immutable values. Maybe you were actually
thinking about assignable references.

On the other hand, you may actually want to store your data within the
theory or proof context of Isabelle in a value oriented fashion. See
TheoryDataFun/ProofDataFun in src/Pure/context.ML and existing
applications in the sources. Especially see src/ZF/Tools/typechk.ML in
the development version for an up-to-date example.

Makarius

Email Gateway (Aug 17 2022 at 14:43):

From: Makarius <makarius@sketis.net>
Note that 'use' is a descendent of the venerable 'eval' of LISP, which
always operates on the toplevel environment. In fact use/eval is some
kind of magic that should not be invoked only in very special situations.

Better stay with ordinary value oriented functions ... -> theory -> theory
of Proof.context -> Proof.context (or mutable references as a last
resort).

Makarius

Email Gateway (Aug 17 2022 at 14:44):

From: Clément Hurlin <Clement.Hurlin@esial.uhp-nancy.fr>

because they are
statically fixed bindings to immutable values.

Understood.

Maybe you were actually
thinking about assignable references.

Yes I didn't tought of that but that's what I want to do : modify the
value of variables inside my code. Yet using references with this
following code fails :
val proof_congr = ref []
val proof_inst = ref []

val _ = use proof_hints_fn

proof_hints_fn containing :
(
proof_inst := X;
proof_congr := Y
)

When executing, it now says that 'proof_inst' and 'proof_congr' are
not declared. I guess that when calling use, the context of the call
isn't inherited. But this is bizarre since it works inside an
interactive session...

Clément

Last updated: May 03 2024 at 12:27 UTC