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 -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
infix 1 #~> #~~> #~~~> #~~~~> #~~~~~>;
structure Prepare : sig
val p1 : ('a -> 'd -> 'c) -> ('c -> 'a -> 'b) -> 'd -> 'a -> 'b
val #~> : ('a -> 'd -> 'c) -> ('c -> 'a -> 'b) -> 'd -> 'a -> 'b
val p2 : ('a -> 'd -> 'f -> 'c * 'e) -> ('c -> 'e -> 'a -> 'b) -> 'd -> 'f ->
'a -> 'b
val #~~> : ('a -> 'd -> 'f -> 'c * 'e) -> ('c -> 'e -> 'a -> 'b) -> 'd -> 'f
-> 'a -> 'b
val p3 : ('a -> 'd -> 'f -> 'h -> 'c * 'e * 'g) -> ('c -> 'e -> 'g -> 'a ->
'b) -> 'd -> 'f -> 'h -> 'a -> 'b
val #~~~> : ('a -> 'd -> 'f -> 'h -> 'c * 'e * 'g) -> ('c -> 'e -> 'g -> 'a
-> 'b) -> 'd -> 'f -> 'h -> 'a -> 'b
val p4 : ('a -> 'd -> 'f -> 'h -> 'j -> 'c * 'e * 'g * 'i) -> ('c -> 'e -> 'g
-> 'i -> 'a -> 'b) -> 'd -> 'f -> 'h -> 'j -> 'a -> 'b
val #~~~~> : ('a -> 'd -> 'f -> 'h -> 'j -> 'c * 'e * 'g * 'i) -> ('c -> 'e
-> 'g -> 'i -> 'a -> 'b) -> 'd -> 'f -> 'h -> 'j -> 'a -> 'b
val p5 : ('a -> 'd -> 'f -> 'h -> 'j -> 'l -> 'c * 'e * 'g * 'i * 'k) -> ('c
-> 'e -> 'g -> 'i -> 'k -> 'a -> 'b) -> 'd -> 'f -> 'h -> 'j -> 'l -> 'a -> 'b
val #~~~~~> : ('a -> 'd -> 'f -> 'h -> 'j -> 'l -> 'c * 'e * 'g * 'i * 'k) ->
('c -> 'e -> 'g -> 'i -> 'k -> 'a -> 'b) -> 'd -> 'f -> 'h -> 'j -> 'l -> 'a ->
'b
end = struct
fun p1 p f x s = f (p s x) s;
val op #~> = p1;
fun p2 p f x y s = let val (x', y') = p s x y in f x' y' s end;
val op #~~> = p2;
fun p3 p f x y z s = let val (x', y', z') = p s x y z in f x' y' z' s end;
val op #~~~> = p3;
fun p4 p f x y z w s = let val (x', y', z', w') = p s x y z w in f x' y' z' w'
s end;
val op #~~~~> = p4;
fun p5 p f x y z w v s = let val (x', y', z', w', v') = p s x y z w v in f x'
y' z' w' v' s end;
val op #~~~~~> = p5;
end;
open Prepare;
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
