Email Gateway (Aug 19 2022 at 15:06): Email Gateway (Aug 19 2022 at 15:06):From: Joachim Breitner <breitner@kit.edu>
Hi,
I’m trying to learn hacking Isabelle/ML, and I started with the
seemingly simple task of “For all local facts with a name, add a "foo"
to their name”.
Here is what I tried:
theory Scratch imports Main keywords "foobar" :: prf_decl
begin
ML {*
fun named_local_facts ctxt =
let val facts = Proof_Context.facts_of ctxt;
in Facts.dest_static false [Global_Theory.facts_of (Proof_Context.theory_of ctxt)] facts
end;
val foobar_cmd =
Proof.map_context (fn ctxt =>
let
val facts = named_local_facts ctxt
val renamed = map (apfst (suffix "foo")) facts
in fold (Proof_Context.put_thms true) (map (apsnd SOME) renamed) ctxt
end );
Outer_Syntax.command @{command_spec "foobar"} "my test command" (Scan.succeed (Toplevel.proof foobar_cmd));
*}
notepad
begin
assume bar: "p = (a,b)" and X
foobar
end
end
Unfortunately, I get
Bad name binding: "local.barfoo"
It seems to me that Proof_Context provides a certain abstraction over
local facts, where I can still retrieve them in a raw way (“facts_of”),
but I can only add them via an interface (“put_thms”) that expect the
names in a certain, yet-to-be-mangled name. Is that roughly correct?
Is there a way to mess with the internals of the Proof_Context directly,
or would I have to change proof_context.ml for that (such as exposing
map_data)?
Or am I approach this task in a wrong way?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:06):From: Joachim Breitner <breitner@kit.edu>
Hi,
a bit of progress:
Tracing existing code a bit more, it seems that I have to go through
Proof_Context.note_thmss, which expects a binding.
So I tried to use Binding.qualified_name to turn the string
local.Cons.IHfoo into a binding. But if I add that using
Proof_Context.note_thmss, "print_facts" will list it as IHfoo, not as
Cons.IHfoo.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:07):From: Makarius <makarius@sketis.net>
On Tue, 29 Jul 2014, Joachim Breitner wrote:
and I started with the seemingly simple task of “For all local facts
with a name, add a "foo" to their name”.
That is not a simple task, and it does not quite fit to how Isabelle
conceptually works.
The "implementation" manual provides a lot of background information, but
it needs to be studied carefully together with some canonical application.
Section "1.2 Names" might help a bit as a start in this particular case.
I’m trying to learn hacking Isabelle/ML
Is there a way to mess with the internals of the Proof_Context directly,
or would I have to change proof_context.ml for that (such as exposing
map_data)?Or am I approach this task in a wrong way?
It depends whom you ask, and what you want to achieve. Proper
understanding the systems needs long time of study, not quick hacking. I
would go as far as to say that and "hacking" or "messing" is a not worth
the time spent on it.
Makarius
Email Gateway (Aug 19 2022 at 15:07):From: Joachim Breitner <breitner@kit.edu>
Hello,
there is always a first step, and different people learn in different
ways. I could have said “experimentation” if you like that word better.
I want to achieve sufficient knowledge of the Isabelle/ML layer to
implement a "unfold_in_context" command as outlined last week. I’d say
that learning to do that is worthwhile independent of whether such a
command is desirable.
So can I expect guidance from those on this list who already spent the
long time of study? Or is it expected for newcomers to study on their
own until they achieve mastery (or give up)?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:07):From: Lars Hupel <hupel@in.tum.de>
Hi Joachim,
there is always a first step, and different people learn in different
ways. I could have said “experimentation” if you like that word better.
I found that reading the sources and experimenting (in a type-driven
way) with them worked well for me. Also, the Isar Implementation Manual
and the Isabelle/ML Cookbook are valuable resources.
So can I expect guidance from those on this list who already spent the
long time of study? Or is it expected for newcomers to study on their
own until they achieve mastery (or give up)?
I'm sure you'll find helpful answers here.
Cheers
Lars
Email Gateway (Aug 19 2022 at 15:07):From: Joachim Breitner <breitner@kit.edu>
Dear Lars,
Am Mittwoch, den 30.07.2014, 08:15 +0200 schrieb Lars Hupel:
there is always a first step, and different people learn in different
ways. I could have said “experimentation” if you like that word better.I found that reading the sources and experimenting (in a type-driven
way) with them worked well for me. Also, the Isar Implementation Manual
and the Isabelle/ML Cookbook are valuable resources.
thanks; looks like I’m on the right paths.
Since you mention type-driven: Do you know of a way of having the system
tell me the types of non-exported functions in existing ML code in
Pure/? The exported functions have their types visible in the signature
specification. And for code in my own modules Ctrl-Hover is very
helpful, but that doesn’t work in ML files that have been loaded in the
heap. Is there maybe a way to get jEdit process Pure (instead of loading
a Heap)?
So can I expect guidance from those on this list who already spent the
long time of study? Or is it expected for newcomers to study on their
own until they achieve mastery (or give up)?I'm sure you'll find helpful answers here.
Great. Then let me try to ask better questions next times :-)
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:07):From: Lars Hupel <hupel@in.tum.de>
Since you mention type-driven: Do you know of a way of having the
system tell me the types of non-exported functions in existing ML
code in Pure/? The exported functions have their types visible in the
signature specification.
This is going to sound very low-tech, but I usually copy-paste
significant chunks or even a whole file into a "ML{* *}" block in a
theory. This usually works fine and gives you the full markup.
And for code in my own modules Ctrl-Hover is very helpful, but that
doesn’t work in ML files that have been loaded in the heap. Is there
maybe a way to get jEdit process Pure (instead of loading a Heap)?
As far as I know, that is only possible for theories loaded after Pure
has been bootstrapped. You're probably out of luck there.
Cheeers
Lars
Email Gateway (Aug 19 2022 at 15:07):From: Peter Lammich <lammich@in.tum.de>
I'm even more low-tech: I have a console open in src/, and use
grep "val <fun-name>:" -r .
this usually matches the line in the signature that declares the type.
The same could be achieved with jedits (mouse-intensive) hypersearch
feature.
Email Gateway (Aug 19 2022 at 15:08):From: Joachim Breitner <breitner@kit.edu>
Dear List,
Thanks for that suggestion. Unfortunately, that does not help with code
that doesn’t have type signatures.
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
That is why I have moved more and more tools within Pure into Pure.thy
itself, so that they can be loaded into another theory as well, for
inspecting within the Prover IDE.
Makarius
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
Hypersearch is indeed the one big thing of jEdit, independently of the
Prover IDE. It is my main tool for navigating the Isabelle bootstrap
sources: its uniform naming conventions make this work very well.
The "implementation" manual also explains how Isabelle/ML is usually
written, such that it is reasonably easy to read it systematically, with
or without tool support.
Makarius
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
Experimentation is at least proper terminology of empirical science.
More of its principles can be applied to explore the Isabelle sources, to
understand more aspects of it.
The "implementation" manual explains many things that help working
systematically with the sources, but it definitely needs serious efforts.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC