Value.Match
A eDSL for dispatching on multiple types.
The syntax involves only two operators, can
that applys a sort refinining function, and let|
glues several cases together. Let's start with a simple example,
let f x = Match.(begin
let| x = can Bool.refine x @@ fun x ->
(* here x has type [Bool.t value] *)
`Bool x in
let| x = can Bitv.refine x @@ fun x ->
(* and here x is ['a Bitv.t value] *)
`Bitv x in
let| x = can Mem.refine x @@ fun x ->
(* and now x is [('a,'b) Mem.t value] *)
`Mem x in
`Other x
end)
In general, the syntax is
let| x = can s1 x @@ fun (x : t1) -> body1 in ... let| x = can sN x @@ fun (x : tN) -> bodyN in default
where s1
,...,sN
a refiners to types t1
,...,tN
, respectively.
If in can s1 x body
the sort of x
can be refined to t1
using the refiner s1
then body
is applied to the value x
with the refined sort (and freshly generated type index if needed) and the result of the whole expression is body x
and the nested below expressions are never evaluated. Otherwise, if there is no refinement, the expression can s1 x body
is evaluated to ()
and the next case is tried until the default
case is hit.
val let| : 'b t -> (unit -> 'b) -> 'b
let| () = can s x f in can't
refines x
to s
.
If the sort of x
could be refined with s
then f
is called with the refined value x'
and the whole expression is evaluated to f x'
. Otherwise, the control is passed to can't
.
val both :
'a refiner ->
unit value ->
'b refiner ->
unit value ->
('a value -> 'b value -> 'c) ->
'c t
let| () = both sx x sy y f in no
applies two refiners in parallel.
If both x
and y
could be refined with sx
and sy
respectively then f x' y'
is called with the refined values and becomes the value of the expression. Otherwise, no
is evaluated and becomes the value of the whole expression.