Re: [isabelle] ML functions



On Fri, 23 Sep 2011, Steve Wong wrote:

I have two questions regarding implementing ML functions:

1) If I have a file containing my own ML function "foo" in a structure
"bar", I seem to have to call "bar" using "foo.bar". I see that the
functions in BasicLibrary, Term, etc., one could call "maps" by just "maps"
and not "BasicLibrary.maps". So how should "bar" be defined in order to be
able to call "foo" with just "foo"?

The idea is to wrap things in structures by default, and only make parts of the content pervasive later, either by 'open' of a substructure or by individual 'val' declarations after the structure definition. Here are some representative examples for both ways:

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/Pure/goal.ML
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011/src/Pure/subgoal.ML

See the start and end of these files, respectively.


2) If my functions spread over numerous files, is there a neat way for including all these files in a .thy rather than 10 or so individual lines of 'use "..."'?

10 'use' commands are not so much -- we do this routinely with many more files.

You can also embed ML text directly in the theory body, using the 'ML' command, or variations of it.


	Makarius





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