Email Gateway (Aug 22 2022 at 18:03): Email Gateway (Aug 22 2022 at 18:03):From: Burkhart Wolff <wolff@lri.fr>
Dear all,
what is the recommended way in Isabelle17/18 to instantiate a polymorphic term,
so, e.g. Const ("Option.option.None", "'a option”) ( or alternatively: Const ("Option.option.None", “?'a option”) )
to
Const ("Option.option.None", “int option”)
???
infer_type apparently does not do the trick.
Many thanks for some advice.
bu
Email Gateway (Aug 22 2022 at 18:03):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Burkhart,
As Makarius would say, it all depends on your application. In general, a substitution is what would be called for. But if you built your term yourself, maybe you can use Sign.mk_const and pass the correct type arguments right away, e.g.
Sign.mk_const thy (@{const_name None}, @{typ int})
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 18:03):From: Burkhart Wolff <wolff@lri.fr>
Thanks Jasmin.
Meanwhile, I found out myself.
Since it might be of wider interest for Isabelle users
(and since it is not totally obvious) I present the solution:
First step: Type generalisation.
Since type unification and type matching work on schematic type
variables, one has to generalise the free type variables.
There are more general and complex functions for this in structure
Term_Subst, but for the purpose here the following suffices:
ML‹
val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
val generalize_term = Term.map_types generalize_typ;
›
(the index 0 is, as I said, sufficient for this special solution)
Example:
ML‹val t = generalize_term @{term "[]”}›
yields now the system output: “val t = Const ("List.list.Nil", "?'a list"): term”
indicating that the free type variable has been replaced by a schematic type variable.
In slow motion: "?'a list” is a system pretty printing for:
ML‹ val t_schematic = Type("List.list",[TVar(("'a",0),@{sort "HOL.type"})]); ›
Note that type antiquotations do not permit to denotate types with schematic type variables directly,
following an Isabelle development trend to hide schematic variables from the Isar interface.
Second Step: Type Matching (or unification, but watch out for the indexes)
The trick is most easily done by a high-level interface in structure Sign that covers more low-level
operations on the Term level.
Matching and unifications produce a type environment @{ML_type "Type.tyenv”} which is basically
a type synonym to Vartabs which is basically a synonym to Symtabs … So:
ML‹
val tyenv = Sign.typ_match @{theory} (t_schematic, @{typ "int list"}) (Vartab.empty);
val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv;
›
Third step: Type instantiation.
Apparently, a bizarre conversion between the old-style interface and
the new-style @{ML "tyenv"} is necessary. See the following example.
ML‹
val S = Vartab.dest tyenv;
val S' = (map (fn (s,(t,u)) => ((s,t),u)) S) : ((indexname * sort) * typ) list;
(* it took me quite some time to find out that these two type representations,
obscured by a number of type-synonyms, where actually identical. *)
val ty = t_schematic;
val ty' = Term_Subst.instantiateT S' t_schematic;
val t = (generalize_term @{term "[]"});
val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
(* or alternatively : *)
val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
›
The system output for the latter is:
val ty = "?'a list": typ
val ty' = "int list": typ
val t = Const ("List.list.Nil", "?'a list"): term
val t' = Const ("List.list.Nil", "int list"): term
Voila.
Once upon a time, there was this the idea of an "Isabelle programmers cookbook”,
where this kind of information on this level of abstraction could be gathered.
Was this project abandoned ?
bu
Last updated: Apr 18 2024 at 12:27 UTC