Email Gateway (Aug 18 2022 at 18:16): Email Gateway (Aug 18 2022 at 18:16):From: Steve Wong <s.wong.731@gmail.com>
Hi,
What is a better way to beta-apply two terms without using betapply, which
can cause a type mismatch. For example:
consts
a :: nat
F :: "'a => nat"
ML {*
val ftrm = @{term "F"};
val atrm = @{term "a"};
val res = betapply((ftrm,atrm));
type_of res
*}
The application succeeds, but the resulting term isn't well-typed (thus
type_of fails). betapply doesn't seem to change the input type of F from a
variable to "Nat.nat". Is there a better way of beta applying such that the
input type can automatically be updated?
Thanks for the help in advance!
Steve
Email Gateway (Aug 18 2022 at 18:17):From: Makarius <makarius@sketis.net>
Term.betapply is not used that often, although there is nothing wrong with
it. Other term constructions (even plain Abs and $) are used more
frequently.
The experiment above has failed for other reasons: the example terms are
internalized independently, i.e. the system did not know they are
correlated. Normally you use something like Syntax.read_terms,
Syntax.check_terms or even Specification.read_specification /
check_specification for simultaneous processing of formal input in an
shared syntactic context.
An alternative is to compose untyped preterms (using dummyT) in some
places and then let Syntax.check_term(s) work out the details. (It also
requires some care because many basic term operations assume fully typed
terms.)
Another note concerning readability of ML sources: "ftrm" and "atrm" are
rather long and unwieldy names for plain formal entities that could be
just called "f" and "a", or "t" and "u".
Makarius
Email Gateway (Aug 18 2022 at 18:33):From: Makarius <makarius@sketis.net>
Depends what you want to do exactly. The following reconstructs types for
the given schematic term, treating schematic type variables as fixed in
type-inference. The context needs to be configured to allow
schematic terms explicitly:
ML {*
val ctxt = @{context} |> Proof_Context.set_mode
Proof_Context.mode_schematic;
val s = Var (("s", 0), dummyT);
val t = Var (("t", 0), TVar (("'a", 0), HOLogic.typeS));
Syntax.check_term ctxt (s $ t)
*}
Note that I have used proper type variable name "'a" here. The system
does not insist in that, but the behaviour for a TVar called "a" is
undefined.
This variant is slightly different, it uses a named type inference
parameter that may get instantiated in type-inference:
ML {*
val ctxt = @{context} |> Proof_Context.set_mode
Proof_Context.mode_schematic;
val s = Var (("s", 0), dummyT);
val t = Var (("t", 0), Type_Infer.mk_param 0 @{sort HOL.type});
Syntax.check_term ctxt (s $ t)
*}
Makarius
Last updated: May 01 2024 at 20:18 UTC