elpi

ELPI - Embeddable λProlog Interpreter
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library elpi
Module Elpi . API . FlexibleData
module Elpi : sig ... end

key for Elpi's flexible data

module type Host = sig ... end
module Map (Host : Host) : sig ... end
module type Show = sig ... end

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.

val uvar : (Elpi.t * Data.term list) Conversion.t