Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
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.
module Elpi : sig ... endkey for Elpi's flexible data
module type Host = sig ... endExample 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