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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
