TypeBasePure.gen_datatype_info undocumented

[xrchz]

Indeed a lot of stuff about datatypes seems to be eerily under-specified, or maybe I'm not looking in the right places.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[konrad-slind]

I haven't documented the theTypeBase or the functions that
generate stuff and put them in the typeBase. Will so so
when I get a chance.

Konrad.

On Sat, May 26, 2012 at 4:36 PM, Ramana Kumar
reply@reply.github.com
wrote:

Indeed a lot of stuff about datatypes seems to be eerily under-specified, or maybe I'm not looking in the right places.

---

Reply to this email directly or view it on GitHub:
#65

[xrchz]

It would probably be more useful if there were suitable entrypoints for someone in the following situation (like me): I have manually proved

• ty_induction
• ty_11
• ty_distinct
• ty_nchotomy
• ty_Axiom
• ty_case_def
• ty_case_cong

And I think they are all of the correct form (but I don't know since those forms aren't documented), judging by the generated theorems for a very similar type.
Now I want to add ty to the type base and make it persistent etc.
(In particular I want to be able to use Define with my constructors and use tactics like Induct and Cases.)
How can I do that?

[konrad-slind]

Right, that's exactly the situation that should be documented. You
want to use

TypeBase.write
[TypeBasePure.mk_datatype_info {...}];

which creates the required tyinfo datastructure and installs it into
theTypeBase, which is the collection of useful type information used
by a variety of tools. There's a simple version of this invocation
at the end of

src/sum/sumScript.sml

There is something wrong with it, which I will discuss later. But first, let's
go through the supplied fields in the record.

 ax=TypeBasePure.ORIG sum_Axiom,

This is the prim.rec. axiom characterizing the datatype, in the format
determined by the datatype package. The "TypeBasePure.ORIG"
constructor is needed because each type in a mutually recursive type
declaration will end up having the same axiom, and I didn't want to
barf out the same redundant info when printing out tyinfo information
when TypeBase.elts() is invoked. When dealing with a non-mutually
recursive type, just use TypeBasePure.ORIG . If the type
is mutually recursive, you have to write each type separately; for
all but the first type, use TypeBasePure.COPY((thy,ty),axiom).

  case_def=sum_case_def,

Definition of the case construct for the type.

  case_cong=sum_case_cong,

Case cong theorem for the type.

  induction=TypeBasePure.ORIG sum_INDUCT,

Induction theorem for the type. See discussion on ORIG and COPY
above.

  nchotomy=sum_CASES,

Cases theorem for the type.

  size=NONE,

Definition of a size function for the type. This is used when synthesizing
termination measures used by Define's termination prover. In the case
of sums, size=NONE because of a bootstrapping issue: numbers haven't
been defined at this point in the system build, so I fill in the field
with NONE,
and replace it later (see src/num/theories/basicSize.sml).

  encode=NONE,

The encode field is a vestigal remainder from some work I did with Joe Hurd on
automatic generation and application of serializers for datatypes. Safe to leave
it as NONE.

  fields=[], accessors=[], updates=[],

These are needed for record types. The way to figure out what they do is to
defined some simple record type "foo" then invoke

TypeBase.fields_of :foo;
TypeBase.accessors_of :foo;
TypeBase.updates_of :foo;

  recognizers = [ISL,ISR],
  destructors = [OUTL,OUTR],

We allow destructors and recognizers to be defined over
datatypes. I use this feature in Guardol, but if you aren't
going to do that for your application, you can leave the
lists empty.

  lift=SOME(mk_var("sumSyntax.lift_sum",
                   Parse.Type`:'type -> ('a -> 'term) ->
                                        ('b -> 'term) ->

('a,'b)sum -> 'term`)),

lift is another vestigial field left over from the encoding experiment.
Actually, it is used to automate the extraction of HOL terms from
the results of ML evaluation. Unused at the moment.

  one_one=SOME INR_INL_11,
  distinct=SOME sum_distinct

You know what these are.

Now, returning to what's wrogn with this: it occurs at the end of sumScript.sml,
so a tyinfo for sum is duly made and installed in the TypeBase. However, then
evaluation of sumScript terminates and the sum tyinfo is thrown away.
So it seems
un-needed. However, the

val _ = adjoin_to_theory
{sig_ps = NONE,
struct_ps = SOME(fn ppstrm =>
let val S = PP.add_string ppstrm
fun NL() = PP.add_newline ppstrm
in
...
end)};

just before that is needed in order to make the tyinfo addition to the
TypeBase persistent.

You might also have a look at Datatype.build_tyinfos, which automates
much of the drudgery of mk_datatype_info. All you need to do is
give the induction and prim.rec. theorems as input.

val build_tyinfos : typeBase
-> {induction:thm, recursion:thm}
-> tyinfo list

See src/datatype/Datatype.{sig,sml} for more details.

Cheers,
Konrad.

On Wed, Jun 6, 2012 at 5:08 AM, Ramana Kumar
reply@reply.github.com
wrote:

It would probably be more useful if there were suitable entrypoints for someone in the following situation (like me): I have manually proved

• ty_induction
• ty_11
• ty_distinct
• ty_nchotomy
• ty_Axiom
• ty_case_def
• ty_case_cong

And I think they are all of the correct form (but I don't know since those forms aren't documented), judging by the generated theorems for a very similar type.
Now I want to add ty to the type base and make it persistent etc.
(In particular I want to be able to use Define with my constructors and use tactics like Induct and Cases.)
How can I do that?

---

Reply to this email directly or view it on GitHub:
#65 (comment)