Email Gateway (Aug 19 2022 at 16:00): Email Gateway (Aug 19 2022 at 16:00):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear all,
I wonder whether there is any way in Isabelle to include formal, checked comments within
inner syntax in Isabelle. In Haskell, for example, one frequently sees function signatures
of the following layout:
myFun
:: [a] -- meaning of first parameter
-> Integer -- meaning of second parameter
-> (a, [a]) -- description of results
I find this format very convenient to document functions with a large number of
parameters. However, in Isabelle, I have not yet found a satisfactory solution. The
following is already close to the above, however it relies on comments within inner
syntax. Hence, the documentation is not formally checked and I cannot use antiquotations
and all the other conveniences from formal text blocks.
definition my_fun
:: "'a list (* meaning of first parameter *)
=> int (* meaning of second parameter *)
=> ('a, 'a list)" (* description of results *)
where ...
Can such comments be made such that they are checked formally? Or does any of you have
other convenient ways of documenting parameters and results of functions?
Andreas
Email Gateway (Aug 19 2022 at 16:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
a radical answer would be to allow inner syntax to contain arbitrary
text cartouches ‹…› but I guess this would be a too massive change.
Alternatively you could devise a suitable set of antiquoations, e.g.
‹@{spec "f xs k = ys"} …
@{arg xs} …
@{arg k} …
@{arg ys} …
›
The disadvantage is that these can only follow the specification an
question. But it will still leave the freedom to skip the Isar
specification totally and antiquote the specification theorems
explicitly, e.g.
‹@{spec "f xs k = ys"} …
@{arg xs} …
@{arg k} …
@{arg ys} …
@{thms f.simps}
›
Hope this helps,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:02):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,
Your suggestion looks very much like JavaDoc comments. However, I am less interested in
formally checking that every parameter is documented rather than formally checking the
documentation. So your suggested approach provides only little over what is currently
available without the antiquotations @{spec} and @{arg}. In particular, the problem of
linking the parameter positions and types remains.
Do you have any idea how one could escape from inner syntax to the language context
"document"?
Andreas
Email Gateway (Aug 19 2022 at 16:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Well, my idea was that additional checks behind the back ensure the
@{arg …}s appear in the right order and completely.
Florian
signature.asc
Email Gateway (Aug 19 2022 at 16:03):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
I see, this indeed ensures a correct link, the link is still not as visible as with the
interleaved comments in Haskell.
Andreas
Email Gateway (Aug 19 2022 at 16:04):From: Makarius <makarius@sketis.net>
Inner syntax already allows cartouches, e.g. see the isar-ref manual about
outer and inner syntax, or more practically
$ISABELLE_HOME/src/HOL/ex/Cartouche_Examples.thy (which is just a
playground of possibilities collected in chronological order over some
weeks).
It remains to be seen where cartouches make most sense in actual use in
Isabelle/Pure and Isabelle/HOL. The full potential still needs to be
fathomed.
For the concrete problem of inner text blocks, I reckon that it could be
done, assuming that the document preparation system finally manages to
warp forwards in time from 1999 to 2014. So many important reforms are
still in the pipeline, such as proper support for nested markup and nested
formal languages for LaTeX rendering. With that available, the "escape"
from inner syntax to the document language would just be normal nesting of
languages with corresponding change of rendering.
I have envisioned something like that many years ago, but it did not get
through the pipeline so far, due to the tight entanglement of the document
preparation system and its many sophisticated tricks. There is also a
correspondence to the "too many modes" problem of checking Isabelle
theories in batch build mode, versus PIDE interaction mode, versus two
obsolete TTY modes.
Makarius
Last updated: Apr 26 2024 at 12:28 UTC