Re: [isabelle] Creating the type required for DatatypePackage.add_datatype_i



Michael Norrish wrote:
               [([], "foo", NoSyn, (* no idea what 1st and 3rd elements
                                      do here *)

Dear Michael,

the 1st element is the list of type parameters of the type constructor "foo",
and the 3rd element is used for specifying additional mixfix syntax for the
type constructor.

but if I want to do this with add_datatype_i, I need something like

   add_datatype_i true
                  true
                  ["foo"]
                  [([], "foo", NoSyn,
                    [("zero", [], NoSyn),
                     ("suc", [????], NoSyn)])]

and I don't know what to put in ????

Simply trying

   Type("foo", [])

doesn't seem to work.

No, you have to give the full internal name of the type constructor, i.e.
"Foo.foo" instead of just "foo", where "Foo" is the name of the current theory.
You can compute the full name corresponding to a short name using the
function Sign.full_name. For example,

  Sign.full_name my_theory "foo"

will return something like "Foo.foo".
By the way, the second boolean argument of add_datatype_i indicates whether
the constructors "zero" and "suc" of the datatype should be declared at the
"top level" of the theory, i.e. their internal names will be "Foo.zero" and
"Foo.suc", or whether the names of the constructors should be prefixed with
both the name of the theory and the name of the datatype, i.e. their internal
names will be "Foo.foo.zero" and "Foo.foo.suc". The latter enables you to
define several datatypes with constructors having the same name. In order
to get the default behaviour, you have to set the second argument of
add_datatype_i to false.

Greetings,
Stefan

--
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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