Value.MatchA 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
defaultwhere 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) -> 'blet| () = 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 tlet| () = 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.