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: https://github.com/mn200/HOL/issues/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: https://github.com/mn200/HOL/issues/65#issuecomment-6147028