Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML interface of *_interpretation


view this post on Zulip Email Gateway (Aug 22 2022 at 15:36):

From: Lars Hupel <hupel@in.tum.de>
Dear locale experts,

is there any reason why there is no ML interface for the various
interpretation commands that takes a tactic? Currently, I have to do
something like this:

lthy
|> Interpretation.global_interpretation ([expr], []) [] []
|> Proof.refine_singleton meth
|> Proof.global_done_proof

"expr" is also very cumbersome to construct (via "Expression.Positional").

Is there any way to simplify this?

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:36):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,

as far as I remember (from memory, I did not check against the sources),
the only long-standing programmatic application of locale interpretation
has been the class target (more exactly,
src/Pure/Isar/class_declaration.ML). At one stage in its development
(maybe around 2009), that stopped to use full-blown interpretation
interfaces at all and constructed the necessary canonical morphisms from
scratch instead (function »calculate«). This is maybe why these never
really emerged – also early implementations of the class target used
something similar to your code above, AFAIR.

The question seems to me, how complicated is your application actually?
Would a manual construction of the required morphisms and registering
them via Locale.add_registration suffice for that?

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 15:37):

From: Lars Hupel <hupel@in.tum.de>
Hi Florian,

in essence, what I have is a compiler that is defined within a locale,
parametrized on some values. When I prove the locale assumptions for a
particular instantiation, I want to get the executable compiler, i.e.,
"global_interpretation" with "defines" for the transitive closure of
involved constants.

Pseudocode:

embed test_code is id List.append List.rev

term test_code.compile
(* test_code.compile :: term => exp *)

value "test_code.compile (Const ''id'')"
(* ... result ... :: exp *)

Cheers
Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 15:39):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,

in essence, what I have is a compiler that is defined within a locale,> parametrized on some values. When I prove the locale assumptions for
a> particular instantiation, I want to get the executable compiler,
i.e.,> "global_interpretation" with "defines" for the transitive closure
of> involved constants.
Pseudocode:

embed test_code is id List.append List.rev

term test_code.compile
(* test_code.compile :: term => exp *)

value "test_code.compile (Const ''id'')"
(* ... result ... :: exp *)

maybe we should talk about that when we meet next time at TUM.

Cheers,
Florian
signature.asc


Last updated: Mar 29 2024 at 04:18 UTC