[isabelle-dev] Alternative thoughts about certifying and reading input parameters to Isabelle command functions
Thomas.Sewell at nicta.com.au
Mon Apr 29 05:01:25 CEST 2013
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
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 =
>> val x_1 = prep_1 ctxt raw_x_1;
>> val x_n = prep_n ctxt raw_x_n;
>> |> ...
>> 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 ...
> This pattern tends to obfuscate if foo again is parametrized, see e.g.
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev