Email Gateway (Aug 23 2022 at 08:20): Email Gateway (Aug 23 2022 at 08:20):From: Peter Lammich <lammich@in.tum.de>
Hi List,
I'm writing a tool that converts a term into an equivalent term.
It works by first generating the new term, and then using the
simplifier to prove equality. However, when generating the new term, I
can save a lot of book-keeping work if I insert "dummyT" types in the
term, and then run type inference later to resolve them.
Here my question: Syntax.check_term seems to do a lot more than type
inference. Can I expect that it will leave the rest of my term intact,
and only replace the dummyT types by something sensible?
If not, can I run type-inference in isolation?
Thanks for any help,
Peter
Email Gateway (Aug 23 2022 at 08:20):From: Makarius <makarius@sketis.net>
Syntax.check_term is a bit like "by simp" for abstract syntax: it can
potentially do many more things than you would normally expect, depending on
instrumentation in the application context. (Just accidentally, the default
setup does mostly simple type inference.)
Here is a more robust way to invoke just the core type-inference:
ML ‹
fun infer_types_simple ctxt =
singleton (Type_Infer_Context.infer_types ctxt) #>
singleton (Type_Infer.fixate ctxt false);
›
ML ‹infer_types_simple \<^context> (Free ("f", dummyT) $ Free ("x", dummyT))›
That is not an "official" API, but it is reasonably well-defined to be re-used
by other tools.
Makarius
Email Gateway (Aug 23 2022 at 08:20):From: Manuel Eberl <eberlm@in.tum.de>
This is not really an answer to your question and I don't know what your
exact use case is, but I just as a reminder: type inference might not
always be enough to determine the type. One example are things like "if
(2::nat) = 0 then A else B". If you copy that term without types and run
type inference on it, you will get a new type variable in there and it
won't be pretty.
Manuel
Email Gateway (Aug 23 2022 at 08:53):From: Peter Lammich <lammich@in.tum.de>
Hi Makarius
Here is a more robust way to invoke just the core type-inference:
ML ‹
fun infer_types_simple ctxt =
singleton (Type_Infer_Context.infer_types ctxt) #>
singleton (Type_Infer.fixate ctxt false);
›ML ‹infer_types_simple \<^context> (Free ("f", dummyT) $ Free ("x",
dummyT))›
This code worked fine until I had a schematic type variable in the
term, which raises an "Illegal schematic type variable" error.
As this code is called from inside a conversion, importing and
exporting the term does not work, as this will rename schematic type
variables, causing the conversion to fail.
I now do "Proof_Context.set_mode mode_schematic", which makes the error
go away. However, the fact that I got this error makes me curious how
much more than "core type inference" this does, and what other
surprises to expect, e.g. on terms with internal variable names, etc.
Best,
Peter
That is not an "official" API, but it is reasonably well-defined to
be re-used
by other tools.Makarius
Email Gateway (Aug 23 2022 at 08:54):From: Makarius <makarius@sketis.net>
On 12/04/2020 21:53, Peter Lammich wrote:
Here is a more robust way to invoke just the core type-inference:
ML ‹
fun infer_types_simple ctxt =
singleton (Type_Infer_Context.infer_types ctxt) #>
singleton (Type_Infer.fixate ctxt false);
›ML ‹infer_types_simple \<^context> (Free ("f", dummyT) $ Free ("x",
dummyT))›
This code worked fine until I had a schematic type variable in the
term, which raises an "Illegal schematic type variable" error.
As this code is called from inside a conversion, importing and
exporting the term does not work, as this will rename schematic type
variables, causing the conversion to fail.I now do "Proof_Context.set_mode mode_schematic", which makes the error
go away.
Proof_Context.set_mode mode_schematic should be OK, it was introduced many
years ago for exactly such situations.
However, the fact that I got this error makes me curious how
much more than "core type inference" this does, and what other
surprises to expect, e.g. on terms with internal variable names, etc.
Type_Infer_Context.infer_types is already the core of type inference, but it
uses a full Syntax.check_typs here
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020-RC5/src/Pure/type_infer_context.ML#l293
in order to prepare the types occurring within the given terms.
This is in principle subject to plugins of the context, but de-facto it is
always Proof_Context.standard_typ_check provided by Isabelle/Pure.
Makarius
Last updated: Apr 19 2024 at 20:15 UTC