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

[Florian Haftmann]

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
-------------- next part --------------

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;
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130427/e4d50882/attachment.asc>