package elpi

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.