Email Gateway (Aug 18 2022 at 09:55): Email Gateway (Aug 18 2022 at 09:55):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
Greetings!
Right now I'm looking at the ISM package (=Interacting State Machines) in
order to make them work with Isabelle2005.
This package defines its own syntax extensions and parses them into
records (among lots of other things).
Now the CVS commit on "Mon May 3 21:22:17 2004 +0000", commit message
reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.
completely breaks this ML code.
I looked through the code and it seems like I have to reimplement most
of it. I tried to figure out how to create and manipulate records in ML,
but failed (HOL/Tools/record_package.ML is not very light reading).
Could someone give me some hints how to
Or alternatively point me to some modules from which I could borrow
code; I'd also welcome any documentation - I didn't find anything
relevant.
Thanks a lot,
Thomas
PS: If anyone is interested, I attached the relevant code.
ISM_package.thy contains the ML code, SLE66.thy is an example using this
theory. find_field_Typ is the first function which fails under the new
record implementation.
Email Gateway (Aug 18 2022 at 09:55):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
This time it is attached.
Thomas
ism.tar.gz
Email Gateway (Aug 18 2022 at 09:55):From: Thomas Bleher <bleher@informatik.uni-muenchen.de>
ML {*
Context.>> (TypedefPackage.add_typedecls ([("test_type":bstring,[],NoSyn)]));
*}
However, the next command then fails with
"exception TERM raised: Stale theory encountered: {<long list of theories>}"
Which magic incantation do I have to use to add a typedecl (or anything
else) to the current theory?
Any tips greatly appreciated!
While I'm at it, two other questions:
There are a lot of seemingly definitions like add_inductive and
add_inductive_i. What's the difference between them?
Where should I post bugs and corrections I found?
Thanks for your time!
Thomas
Email Gateway (Aug 18 2022 at 09:55):From: Norbert Schirmer <norbert.schirmer@web.de>
(* add_record_i (type-params,record-name) parent-name field-decls thy *)
setup {*
[RecordPackage.add_record_i ([],"foo") NONE
[("b",HOLogic.boolT,Syntax.NoSyn)]]*}
(*This is:
record foo =
b::bool
*)
(* Provided the type, you can get the fields of the record the following
way:*)
ML {*
val thy = the_context ();
RecordPackage.get_recT_fields thy
(Type ("Scratch.foo.foo_ext_type",[TFree ("'a",Sign.defaultS thy)]))
*}
As far as I can remember the signature of "add_record_i" did not change with
the reimplementation of records.
Hope this helps.
Norbert
Email Gateway (Aug 18 2022 at 09:56):From: Makarius <makarius@sketis.net>
On Mon, 13 Nov 2006, Thomas Bleher wrote:
I looked at
https://cgi.cse.unsw.edu.au/~formalmethods/wiki/isabelle/index.cgi/ProgrammingIsabelle
Maybe you want to take a look at the "implementation" manual, which is
part of recent development snapshots. (It is only about 25% finished, but
the already existing parts are in an orderly state.)
However, the next command then fails with
"exception TERM raised: Stale theory encountered: {<long list of theories>}"Which magic incantation do I have to use to add a typedecl (or anything
else) to the current theory?
The deeper problem here is what ``current theory'' refers to. The "Stale
theory encountered" indicates that some no longer valid theory value was
involved. Normally you just work with (fn thy => ...) abstractly -- where
the function body uses thy in a strictly linear fashion. Then plug in the
result as Toplevel.theory transaction. Alternatively you may experiment
with the 'setup' command in ProofGeneral/Isar mode. For example:
setup {* TypedefPackage.add_typedecls [("foo", ["'a", "'b"], NoSyn)] *}
typ "(nat, bool) foo"
Paradoxically, it is much easier to work with ML in the Isar interaction
mode, instead of the raw ML toplevel. (Sometimes some low-level output
only occurrs in the isabelle buffer in ProofGeneral.)
Makarius
Last updated: May 03 2024 at 08:18 UTC