Question: construct a prot term from the string representation of the type

[erikmd]

Context

With the current API of test_lib, fixed-arity primitives such as test_function_1 take as argument some _ Ty.ty:

val test_function_1 : ?test: 'b tester -> …
  ('a -> 'b) Ty.ty -> string -> ('a * 'b * string * string) list -> Learnocaml_report.report

while the n-arity primitives take as argument some (_, _, _) prot, the advantage of which being thus that the co-domain type 'ret is clearly specified:

val test_function : ?test: 'ret tester -> …
  (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) prot -> ('ar -> 'row) lookup ->
  (('ar -> 'row, 'ar -> 'urow, 'ret) args * (unit -> 'ret)) list -> Learnocaml_report.report

In learn-ocaml-editor we decided to preferably rely on test_function (and test_function_against) to have more generic code, while providing notations to easily construct some term of type (('ar -> 'row, 'ar -> 'urow, 'ret) args * (unit -> 'ret)) list.

The current bottleneck for specifying such test cases is that the syntax to construct a term of type (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) prot is not very user-friendly. We thus obtain some code like this:

type test_qst_typed =
  | TestAgainstSol :
      { name: string
      ; prot: (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) prot
      ; gen: int
      ; suite: ('ar -> 'row, 'ar -> 'urow, 'ret) args list } -> test_qst_typed
  …
  | TestSuite :
      { name: string
      ; prot: (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) prot
      ; suite: (('ar -> 'row, 'ar -> 'urow, 'ret) args * (unit -> 'ret)) list } -> test_qst_typed

let example_constr_sol =
  TestAgainstSol
    { name = "min";
      prot = (arg_ty [%ty: int] (last_ty [%ty: int] [%ty: int]));
      gen = 4;
      suite = []
    }

Question

The question is: would it be feasible to add to the test_lib API a facility to get a prot from a string representation of the type? Basically one of the two approaches would be OK for us:

1. Either implement a syntax [%prot: a -> b] similar to [%ty: a -> b]
2. Or implement a function that has a type such as prot_of_string: string -> (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) prot

Remarks

• Using approach 1. would thus allow us to write:

let example_constr_sol =
  TestAgainstSol
    { name = "min";
      prot = [%prot: int -> int -> int];
      gen = 4;
      suite = []
    }

• If I'm not mistaken, approach 1. could be implemented either directly, or by implementing 2. first and relying on it.

• We already have a prototype implementation of a function parse_type : string -> string that yields the following trace:

# let str = parse_type "int->(int->int)->int";;
val str : string = "arg_ty [%ty :int ] (last_ty [%ty :(int->int) ] [%ty :int ])"

Kind regards, Erik

[AltGr]

I am investigating, but this doesn't seem trivial. In particular, wouldn't the second option:

prot_of_string: string -> (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) prot

be wholly unsafe ? The point of the ppx is to extract both a witness and its type consistently.