Re: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML

Dear MLA,

(re-sending as I forgot to Cc the list)

Am 01.05.2019 um 01:06 schrieb mailing-list anonymous:
> I would like to understand if there exists a canonical method for creating
> cterms with automatic type inference from several distinct terms in
> Isabelle/ML, given that some of these distinct terms are supplied by the
> user.

I there is not really a well-established canonical method, since the
needs of tools are quite different in the details.

What tools usually do is try to get to a "fully typed" stage as soon as
possible in the outermost layers, and then work with full type
information internally, which means that you must usually carry types
around everywhere.

What I would try is this:

* Make sure you get the user-provided constants / terms in a polymorphic
version, i.e., with schematic type variables. Here, the function
"Variable.polymorphic" should help.

* Then, construct the combined terms as you need them, and run type
checking on this. (-> Syntax.check_terms). I think this should
instantiate the type variables properly.

* Then you should get terms on which Thm.cterm_of should work.

Note that Syntax.check_terms includes several specific things like
insertion of coercions etc. But it is the most general answer to "how do
I check / infer types".

Hope this helps.


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