Module API.FlexibleDataSource

Flexible data is for unification variables. One can use Elpi's unification variables to represent the host equivalent, here the API the keep a link between the two.

Example from Hol-light + elpi:

     module UV2STV = FlexibleData.Map(struct
        type t = int
        let compare x y = x - y
        let pp fmt i = Format.fprintf fmt "%d" i
        let show = string_of_int
      end)

      let stv = ref 0
      let incr_get r = incr r; !r

      let record k state =
        State.update_return UV2STV.uvmap state (fun m ->
          try m, Stv (UV2STV.host k m)
          with Not_found ->
            let j = incr_get stv in
            UV2STV.add k j m, Stv j)

      (* The constructor name "uvar" is special and has to be used with the
         following Conversion.t *)

      let hol_pretype = AlgebraicData.declare {
        ty = TyName "pretype";
        doc = "The algebraic data type of pretypes";
        pp = (fun fmt t -> ...);
        constructors = [
          ...
          K("uvar","",A(uvar,N),
             BS (fun (k,_) state -> record k state),
             M (fun ~ok ~ko _ -> ko ()))
        ]
      }

In this way an Elpi term containig a variable X twice gets read back using Stv i for the same i.