Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Delete code_const declaration in sub-target

Email Gateway (Aug 19 2022 at 11:45):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I have set up the code generator with code_const and code_type to use the type and
operations from the SML standard basis library, namely the Word16 structure.
Unfortunately, PolyML does not provide this optional structure, so I would like to
configure the Eval target of the code generator such that the code generator forgets about
these configurations from the super-target SML and uses the Isabelle code equations for
evaluation. How can I delete a code_const / code_type declaration in a sub-target? None of
the following seems worked:

1. code_type ... (Eval "")
   raises Match in code_printer.ML upon export_code

2. code_type ... (Eval -)
   (inspired by the Haskell code_instance example in the code generator tutorial)
   gives an outer syntax error at -

3. code_type ... (Eval "-")
   raises Match in code_printer.ML upon value [code]

Andreas

Email Gateway (Aug 19 2022 at 11:46):

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

Indeed. I will consider multi-inheritance for code targets, but not in
the near future. In the meanwhile maybe it's best to clone the target
setup from Heap_Monad.thy for a target SML_word_imp.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 11:55):

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

How can I delete a code_const / code_type
the short answer is: that is not possible – it's the ancient issue that
monotonicity does not go well along with deletions.

Concerning your problem, I would recommend to setup a separate target
e.g. »SML_word« derived from »SML« (see Imperative-HOL for examples).
This is IMHO even the cleaner approach, because target setup for »SML«
should not rely on anything not in PolyML.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 12:01):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,

Thanks for the suggestion with a separate sub-target. Before I go that way, I would like
to double check that I understand the implications. AFAIK the targets in the code
generator are arranged in an inheritance tree, i.e., one cannot "merge" different setups.
So, if I introduce such a target SML_word, then I won't be able to use the Imperative_HOL
variant SML_imp. Right?

Best,
Andreas

Last updated: Apr 24 2024 at 04:17 UTC