Re: [isabelle] File.use function



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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.