Email Gateway (Aug 22 2022 at 19:41): Email Gateway (Aug 22 2022 at 19:41):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
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. Unfortunately, given that some of the consts that are used in the
terms provided by the user are not known in advance, the methods that I am
aware of do not seem to be directly applicable or may, potentially, result
in certain malpractices.
For example, I would like to perform an automatic type inference and create
a certified term in the context of the following (significantly) simplified
use case:
ML ‹
val A = @{term "A::'al⇒'ar⇒bool"};
val B = @{term "B::'bl⇒'br⇒bool"};
val RF = @{term rel_fun} (*in the use case, RF can represent an arbitrary
const accepting an arbitrary number of arguments, as supplied by the user*)
val uterm = RF $ A $ B;
(* fails because type inference is not applicable: *)
val cterm = Thm.cterm_of @{context} uterm;
›
Of course, the default names of the 'TFree' types that are generated for
rel_fun in the example above are not suitable when $ is used for combining
terms. *It is very important to note that in my use case RF is provided
by the user and, therefore, it may be different from rel_fun.*
I am aware of two methods that can be used for the solution of the problem.
However, these methods do not seem to be ideal for my application, given
that the consts are provided by the user:
Provide "tailor-made" type inference for each const, similar to the
methodology used in hologic.ml, e.g. HOLogic.mk_eq. Unfortunately, in my
use case, functions like HOLogic.mk_eq need to be generated 'on the fly'
based on the user input. This solution seems to require an investment of a
certain amount of effort.
Define terms as strings and use Syntax.read_term to generate terms from
the strings. This solution does not seem to be safe, although, its
implementation is almost trivial.
I provide a code that demonstrates the methods that I am referring to in
the clauses above after my signature. However, please note that the code is
merely an example that is meant for the demonstration of the problem and it
does not contain (almost) any parts of the intended solution. Therefore,
please ignore various malpractices that are not related to the problem (in
particular, the code does not provide guarantees that unique names are used
and omits all error checks).
*Lastly, I would like to provide a summary of the question : *
- If there is a canonical method for combining arbitrary terms with type
inference that is different from the methods suggested in clauses 1 and 2
above, then I would highly appreciate if you could let me know about it. If
such a method does not exist, then I would like to know whether the
solution in clause 2 above is considered to be a standard practice or not.
Thank you
ML ‹
(* -------------------------------------------- *)
(* auxiliary functions - provided for completeness *)
fun delete_elem _ [] = []
| delete_elem a (x::xs) =
if (a = x) then (delete_elem a xs) else x::(delete_elem a xs);
(* remove duplicates from a list *)
fun remdups [] = []
| remdups (x::xs) = x::(remdups (delete_elem x xs));
(* get unique free type variables *)
fun get_unique_tfree t =
remdups(
rev(
fold_atyps
(fn t => fn ts => case t of TFree td => (TFree td)::ts | _ => ts) t
[]
)
);
val A = @{term "A::'al⇒'ar⇒bool"};
val B = @{term "B::'bl⇒'br⇒bool"};
(* -------------------------------------------- *)
(*
Solution 1: the solution was inferred from the method suggested in section
3.2
(and other sections) in the document "The Isabelle Cookbook"
(May 28, 2015 draft) by Christian Urban. According to this solution,
a tailor-made type inference procedure needs to be provided for each const.
Of course, for many existing standard consts this functionality has
already been provided in hologic.ML (e.g. HOLogic.mk_eq).
The solution is difficult to implement because the consts are
supplied by the user. Therefore, functions similar to HOLogic.mk_eq need to
be
generated 'on the fly'. Effectively, this would require the development of
the functionality
that would enable automatic generation of a significant part of the content
of hologic.ml.
*)
val boolT = Type ("HOL.bool", []);
fun rel_fun_const (A, B, C, D) =
Const
(\<^const_name>‹BNF_Def.rel_fun›,
(A --> B --> boolT) -->
(C --> D --> boolT) -->
(A --> C) -->
(B --> D) -->
boolT);
fun get_types_rel_fun fts gts = (nth fts 0, nth fts 1, nth gts 0, nth gts
1);
fun mk_rel_fun (R1, R2) =
(
(get_types_rel_fun
(R1 |> type_of |> get_unique_tfree)
(R2 |> type_of |> get_unique_tfree)) |> rel_fun_const
)
$ R1 $ R2;
val cterm = Thm.cterm_of @{context} (mk_rel_fun (A, B));
(*
Solution 2: inferred from the code on page 118 in
the document "The Isabelle/Isar Implementation" by Makarius Wenzel.
Can be implemented with ease, but requires the construction of terms
from strings. I am not certain if this is considered to be a standard
practice.
*)
val ctxt' = @{context} |> Variable.declare_term A |> Variable.declare_term
B;
val uterm' = Syntax.read_term ctxt' "BNF_Def.rel_fun A B";
val cterm' = Thm.cterm_of @{context} uterm';
›
Email Gateway (Aug 22 2022 at 19:48):From: Alexander Krauss <krauss@in.tum.de>
Dear MLA,
(re-sending as I forgot to Cc the list)
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.
Alex
Email Gateway (Aug 22 2022 at 19:49):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Alexander Krauss,
Thank you for your email. Indeed, your reply pointed me in the right
direction.
It seems that there is a nearly canonical solution for my problem (without
the explicit use of the schematic type variables). The solution involves
the use of the “place-holder” type dummyT, which is defined in term.ML (I
can only assume it was defined specifically for this use case), e.g.
ML ‹
val f = Const ("HOL.eq", dummyT);
val A = @{term "A::'b"};
val q = (f $ A $ A)
|> Syntax.check_term @{context}
|> Thm.cterm_of @{context};
›
This method is presented in Section 3.5 in "The Isabelle Cookbook" (May 28,
2015 draft) by Christian Urban. I can hardly believe that I missed the
relevant example upon the first reading. Regretfully, I only have several
days of experience in Isabelle/ML coding, therefore, please accept my
apologies for the naive question.
Thank you
Email Gateway (Aug 22 2022 at 19:51):From: Alexander Krauss <krauss@in.tum.de>
Glad you got it to work. Yes, dummyT is treated like a type variable by
type inference, so this is the simplest solution if you just have a
single constant and must figure out the correct type.
Alex
Last updated: Nov 21 2024 at 12:39 UTC