[isabelle-dev] Alternative thoughts about certifying and reading input parameters to Isabelle command functions

[Makarius]

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