On Sat, 27 Apr 2013, Florian Haftmann wrote:
fun gen_foo prep_1 … prep_n raw_x_1 … raw_x_n ctxt =
let
val x_1 = prep_1 ctxt raw_x_1;
…
val x_n = prep_n ctxt raw_x_n;
in
ctxt
|> …
end;
val foo = gen_foo cert_1 … cert_n;
val foo_cmd = gen_foo read_1 … read_n;
Here, raw_x_1 … raw_x_n are unchecked arguments to the abstract
interface foo; these must be checked if provided from outside (via
cert_1 … cert_n) or parse if fed from Isar source text (via read_1 …
read_n).
This pattern tends to obfuscate if foo again is parametrized, see e.g.
http://isabelle.in.tum.de/repos/isabelle/file/182454c06a80/src/Pure/Isar/expression.ML#l848
ff.
The file src/Pure/Isar/expression.ML (which was once part of
src/Pure/Isar/locale.ML) is historically the main source of this extreme
form of nested "prep_foo" usage. I had introduced that around 2002 in the
first Isar version of locales and then tried hard to get rid of it again.
That trend has slowly continued in recent years, but is not finished.
Instead of more funny combinators, we should try to get it further down to
more elementary expression in plain ML, without too much "pointless"
programming.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
