Email Gateway (Aug 22 2022 at 15:36): 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
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
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
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: Nov 21 2024 at 12:39 UTC