Module 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.

Semantics

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.

type 'a t
type 'a refiner = unit sort -> 'a sort option
val let| : 'b t -> (unit -> 'b) -> 'b
val can : 'a refiner -> unit value -> ('a value -> 'b) -> 'b t

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.