|
27 | 27 | Alternatively: [3 @: "word" @:!! false] *) |
28 | 28 | type ('arrow, 'uarrow, 'ret) args |
29 | 29 |
|
30 | | -(** [last e], or equivalently [!! e], builds a one-element argument list *) |
| 30 | +(** [last e], or equivalently [!! e], builds a one-element argument list. *) |
31 | 31 | val last : |
32 | 32 | 'a -> |
33 | 33 | ('a -> 'ret, 'a -> unit, 'ret) args |
34 | 34 |
|
35 | 35 | (** [arg a l], or equivalently [a @: l], adds [a] in front of the |
36 | | - argument list [l] *) |
| 36 | + argument list [l]. *) |
37 | 37 | val arg : |
38 | 38 | 'a -> |
39 | 39 | ('ar -> 'row, 'ar -> 'urow, 'ret) args -> |
40 | 40 | ('a -> 'ar -> 'row, 'a -> 'ar -> 'urow, 'ret) args |
41 | 41 |
|
42 | | -(** Helper notation for [last] *) |
| 42 | +(** Helper notation for [last]. *) |
43 | 43 | val (!!) : |
44 | 44 | 'a -> |
45 | 45 | ('a -> 'ret, 'a -> unit, 'ret) args |
46 | 46 |
|
47 | | -(** Helper notation for [arg] *) |
| 47 | +(** Helper notation for [arg]. *) |
48 | 48 | val (@:) : |
49 | 49 | 'a -> |
50 | 50 | ('ar -> 'row, 'ar -> 'urow, 'ret) args -> |
51 | 51 | ('a -> 'ar -> 'row, 'a -> 'ar -> 'urow, 'ret) args |
52 | 52 |
|
53 | | -(** [a @:!! l] is another notation for [a @: !! l] (with a space) *) |
| 53 | +(** [a @:!! l] is another notation for [a @: !! l] (with a space). *) |
54 | 54 | val (@:!!) : |
55 | 55 | 'a -> 'b -> |
56 | 56 | ('a -> 'b -> 'ret, 'a -> 'b -> unit, 'ret) args |
57 | 57 |
|
58 | | -(** [apply f l] applies a n-ary function [f] to the arguments from [l] *) |
| 58 | +(** [apply f l] applies a n-ary function [f] to the arguments from [l]. *) |
59 | 59 | val apply : |
60 | 60 | ('ar -> 'row) -> ('ar -> 'row, 'ar -> 'urow, 'ret) args -> |
61 | 61 | 'ret |
62 | 62 |
|
63 | 63 | (** GADT for function types. |
64 | 64 |
|
65 | | - Given an arrow type ['a -> 'row], the following construct provides |
66 | | - a more precise representation of this function type than |
67 | | - [[%ty: 'a -> 'row] : ('a -> 'row) Ty.ty]: |
| 65 | + This abstract type fulfills a similar aim as the ['a Ty.ty] type: |
| 66 | + provide a type-safe way to build terms representing an OCaml type |
| 67 | + (relying on [Parsetree.core_type]), the type of these terms being |
| 68 | + themselves parameterized by the type at stake, in order to |
| 69 | + constrain the type of other arguments involved in the considered |
| 70 | + (grader) expression. |
68 | 71 |
|
69 | | - [[%funty: 'a -> 'row] : (('a -> 'row) Ty.ty, 'a -> 'urow, 'ret) fun_ty] |
| 72 | + For ['a Ty.ty], this aim can be achived with the ppx expression |
| 73 | + [[%ty: int]], which builds an abstract term of type [int Ty.ty] |
| 74 | + (this term also gathering an appropriate encoding of the [int] |
| 75 | + type in terms of [Parsetree.core_type]). |
70 | 76 |
|
71 | | - In particular, the codomain type ['ret] is made explicit, so that |
72 | | - if ['row = 'b -> 'c], we get ['urow = 'b -> unit] and ['ret = 'c]. |
| 77 | + For implementing n-ary graders, this information is not sufficient |
| 78 | + in practice, notably as we need to make it explicit in the type |
| 79 | + annotation, what is the co-domain of the n-ary function at stake. |
73 | 80 |
|
74 | | - Usage: [arg_ty [%ty: int] @@ arg_ty [%ty: string] @@ |
75 | | - last_ty [%ty: bool] [%ty: unit]] |
| 81 | + This is achieved by the GADT |
| 82 | + [(('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) fun_ty]. |
76 | 83 |
|
77 | | - Alternatively: [[%funty: int -> string -> bool -> unit]] *) |
| 84 | + There are two ways to build terms of this type: |
| 85 | +
|
| 86 | + 1. Use the two functions [arg_ty], [last_ty], and appropriate |
| 87 | + [[%ty: type]] expressions, for example: |
| 88 | +
|
| 89 | + [arg_ty [%ty: int] @@ |
| 90 | + last_ty [%ty: string] [%ty: bool]]; |
| 91 | +
|
| 92 | + 2. Use directly the [[%funty: 'ar -> 'row]] construct, for example: |
| 93 | +
|
| 94 | + [[%funty: int -> string -> bool]]. |
| 95 | +
|
| 96 | + For both cases in this example, we get a term of type: |
| 97 | +
|
| 98 | + [((int -> string -> bool) Ty.ty, int -> string -> unit, bool) fun_ty], |
| 99 | +
|
| 100 | + where the co-domain type [bool] is now explicit. *) |
78 | 101 | type ('arrow, 'uarrow, 'ret) fun_ty |
79 | 102 |
|
80 | | -(** [last_ty [%ty: a] [%ty: r]] builds a function type for [a -> r] *) |
| 103 | +(** [last_ty [%ty: a] [%ty: r]] builds a function type for [a -> r]. *) |
81 | 104 | val last_ty : |
82 | 105 | 'a Ty.ty -> |
83 | 106 | 'ret Ty.ty -> |
84 | 107 | (('a -> 'ret) Ty.ty, 'a -> unit, 'ret) fun_ty |
85 | 108 |
|
86 | 109 | (** [arg_ty [%ty: a] [%funty: b ->...-> r]] builds a function type for |
87 | | - [a -> b ->...-> r] *) |
| 110 | + [a -> b ->...-> r]. *) |
88 | 111 | val arg_ty : |
89 | 112 | 'a Ty.ty -> |
90 | 113 | (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) fun_ty -> |
91 | 114 | (('a -> 'ar -> 'row) Ty.ty, ('a -> 'ar -> 'urow), 'ret) fun_ty |
92 | 115 |
|
93 | 116 | (** [ty_of_fun_ty funty] returns a term of type [('ar -> 'row) Ty.ty], |
94 | | - assuming [funty : (('ar -> 'row) Ty.ty, _, _) fun_ty] *) |
| 117 | + assuming [funty : (('ar -> 'row) Ty.ty, _, _) fun_ty]. *) |
95 | 118 | val ty_of_fun_ty : |
96 | 119 | (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) fun_ty -> |
97 | 120 | ('ar -> 'row) Ty.ty |
98 | 121 |
|
99 | | -(** [get_ret_ty funty] returns a term of type ['ret Ty.ty], assuming |
100 | | - [funty : (_ , _, 'ret) fun_ty] *) |
| 122 | +(** [get_ret_ty ty l] returns a term of type ['ret Ty.ty] such that if |
| 123 | + [ty : ('ar -> 'row) Ty.ty] and [l] contains n arguments, ['ar -> 'row] |
| 124 | + is the arrow type of an n-argument function with co-domain ['ret]. *) |
101 | 125 | val get_ret_ty : |
102 | | - ('p -> 'a) Ty.ty -> ('p -> 'a, 'p -> 'c, 'ret) args -> 'ret Ty.ty |
103 | | - |
| 126 | + ('ar -> 'row) Ty.ty -> ('ar -> 'row, 'ar -> 'urow, 'ret) args -> 'ret Ty.ty |
104 | 127 |
|
105 | | -(** Signature [S] is intended to be instantiated in [Test_lib] with: |
106 | | - [module M = struct |
107 | | - let typed_printer ty ppf v = Introspection.print_value ppf v ty |
108 | | - let typed_sampler = Introspection.get_sampler |
109 | | - end] *) |
110 | 128 | module type S = sig |
111 | | - val typed_printer : |
112 | | - 'a Ty.ty -> Format.formatter -> 'a -> unit |
113 | | - val typed_sampler : |
114 | | - 'a Ty.ty -> unit -> 'a |
| 129 | + val typed_printer : 'a Ty.ty -> Format.formatter -> 'a -> unit |
| 130 | + val typed_sampler : 'a Ty.ty -> unit -> 'a |
115 | 131 | end |
116 | 132 |
|
117 | | -(** [Make(M)] provides a generic printer and sampler for the arguments |
118 | | - of n-ary functions specified using [args] and [fun_ty] GADTs *) |
| 133 | +(** [Make], used in [Test_lib], provides a generic printer and sampler |
| 134 | + for argument lists of n-ary functions, depending on their type. *) |
119 | 135 | module Make : functor (M : S) -> sig |
120 | 136 | val print : |
121 | | - (('p -> 'a) Ty.ty, 'p -> 'c, 'r) fun_ty -> |
122 | | - Format.formatter -> ('p -> 'a, 'p -> 'c, 'r) args -> unit |
| 137 | + (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) fun_ty -> |
| 138 | + Format.formatter -> ('ar -> 'row, 'ar -> 'urow, 'ret) args -> unit |
123 | 139 | val get_sampler : |
124 | | - (('p -> 'a) Ty.ty, 'p -> 'c, 'r) fun_ty -> |
125 | | - unit -> ('p -> 'a, 'p -> 'c, 'r) args |
| 140 | + (('ar -> 'row) Ty.ty, 'ar -> 'urow, 'ret) fun_ty -> |
| 141 | + unit -> ('ar -> 'row, 'ar -> 'urow, 'ret) args |
126 | 142 | end |
127 | 143 |
|
128 | 144 | (** [apply_args_1], [apply_args_2], [apply_args3], [apply_args_4] are |
129 | 145 | variants of the [apply] function, assuming a fixed number of args; |
130 | | - they have thus a more precise type and are used in [Test_lib] *) |
| 146 | + they have thus a more precise type and are used in [Test_lib]. *) |
131 | 147 | val apply_args_1 : |
132 | 148 | ('a -> 'b) -> ('a -> 'c, 'a -> unit, 'c) args -> 'b |
133 | 149 |
|
|
0 commit comments