Email Gateway (Aug 22 2022 at 19:06): Email Gateway (Aug 22 2022 at 19:06):From: Moa Johansson <moa.johansson@chalmers.se>
Hi,
I’m writing some code that should create a snippet of Isar script. However, as part of this endevour it would be very convenient if there was a function (or option) similar to Syntax.string_of_term which also would include simple type annotations for variables.
Reading the documentation seems to suggest there is no such function ☹.
A small example:
I get: "z = Emp ⟹ app y z = y"
I would like "z = Emp ⟹ app (y :: 'a Lst) z = y"
I would like to have this because if the above term is appearing as an intermediate lemma in an Isar script, it is apparently necessary to explicitly state the types for y (and z), otherwise I cannot use the lemma. Or is it something else I’m missing?
I know there’s some “tricks” to write the script differently, so I don’t need the annotations, but that made it a bit longer and harder to read imho.
Best,
Moa
Email Gateway (Aug 22 2022 at 19:06):From: Peter Lammich <lammich@in.tum.de>
Hi Moa,
the configuration option show_types should do.
In ML:
ML_val ‹
val ctxt = Config.put show_types true @{context}
val test = Syntax.string_of_term ctxt @{term "a+b"} |> writeln
›
As attribute:
declare [[show_types]]
term "a+b"
Email Gateway (Aug 22 2022 at 19:07):From: Dominique Unruh <unruh@ut.ee>
Hi,
show_types will add types to variable names but not to polymorphic
constants.
So something like "card (UNIV::bool set) = 2" would be rendered as the
false fact "card UNIV = 2".
There is additionall show_consts, but that doesn't add the types inside the
term which makes it hard for reparsing.
(Also, if UNIV occurs twice with different types, it will not be clear
which UNIV is which.)
For example:
declare [[show_types, show_consts]]
term "card (UNIV::bool set) = 2"
shows:
"card UNIV = (2::nat)"
:: "bool"
in the output window. (I have no clue why 2 gets a type here.)
I would be very interested myself in some ML-code that gives re-parseable
code.
(Or at least, re-parseable most of the time. I don't think it's possible in
general in the presence of custom print translations etc.)
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:07):From: Dominique Unruh <unruh@ut.ee>
I discovered that there seems to be some code to print a term with
sufficient type information for reparsing, namely in the sledgehammer code.
theory Scratch
imports Main
begin
(* Function str_of converts a string into a term, but with some unwanted
boilerplate around *)
ML ‹
fun str_of t = Sledgehammer_Isar_Proof.Proof
([],[(Sledgehammer_Isar_Proof.no_label,t)],[])
|> Sledgehammer_Isar_Proof.string_of_isar_proof \<^context>
1 1
›
ML ‹str_of \<^term>‹card (UNIV::bool set)=2› |> writeln›
This will print
proof -
assume "card (UNIV::bool set) = 2"
qed
So it unfortunately has some extra stuff around, but it shows that it's
possible in principle by stealing the appropriate fragments of sledgehammer
code.
Best wishes,
Dominique.
Email Gateway (Aug 22 2022 at 19:08):From: Makarius <makarius@sketis.net>
This is how Sledgehammer approximates this:
(The module name already shows that the proper terminology is "Isar
proof" (or "Isar proof text"). Proof scripts are a thing from the past,
before Isar. You can emulate old-style proof scripts via a sequence of
'apply' commands, but this is improper Isar.)
Note that there is no standard function in Isabelle/Pure, because the
problem to print just the right amount of type information is very
complex and not fully solved. One day, after 1 or 2 rounds of
refinements over the above approach, it might become generally available.
Instead of printing type constraints inside a term you can try an
alternative approach with "eigen-context" for free variables, e.g.
have "x + y = z" for x y z :: nat
Makarius
Last updated: May 01 2024 at 20:18 UTC