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

[Thomas Sewell]

Hey Florian.

Just my two cents, but does uncurrying buy you anything here?

The function doing the actual work, "do_foo" in your example, has not 
been given a name and type before. So you're free to have it accept a tuple:

fun do_foo (x_1, x_2, ... x_n) = ...

And now val foo_cmd = read_foo_spec #> do_foo

It's possibly a slight nuisance to someone wanting to wrap some 
parameter adjustment around do_foo, although that was probably fiddly 
anyway.

Yours,
     Thomas.


On 28/04/13 00:31, Florian Haftmann wrote:
> Hi all,
>
> when Isabelle packages (in the widest sense) provide an interface to the
> user, the following pattern is common practice:
>
>> 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.
>
> I'm asking myself whether we could spend some combinators for that
> problem (cf. attached file).  The idea is that two separate functions
>
>    fun cert_foo_spec ctxt raw_x_1 ... raw_x_n = ...
>    fun read_foo_spec ctxt raw_x_1 ... raw_x_n = ...
>
> certify resp. parse their input arguments and provide the result as a
> tuple.  This would be connected to the process function proper using e.g.
>
>    val foo = cert_foo_spec #~~~>  do_foo
>    val foo_cmd = read_foo_spec #~~~>  do_foo
>
> The drawback is that the signatures of the combinators contain numerous
> type variables, and for each arity a separate combinator is needed
> (which, I guess, you cannot escape when you perform uncurrying of
> arbitrary-sized tuples). Maybe it is worth some thought nevertheless.
>
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130429/56d5aaed/attachment-0002.html>