package elpi

  1. Overview
  2. Docs

Declare data from the host application that has syntax, like list or pair but not like int. So far there is no support for data with binder using this API. The type of each constructor is described using a GADT so that the code to build or match the data can be given the right type. Example: define the ADT for "option a"

let option_declaration a = {
  ty = TyApp("option",a.ty,[]);
  doc = "The option type (aka Maybe)";
  pp = (fun fmt -> function
          | None -> Format.fprintf fmt "None"
          | Some x -> Format.fprintf fmt "Some %a" a.pp x);
  constructors = [
   K("none","nothing in this case",
     N,                                                   (* no arguments *)
     B None,                                                   (* builder *)
     M (fun ~ok ~ko -> function None -> ok | _ -> ko ()));     (* matcher *)
   K("some","something in this case",
     A (a,N),                                   (* one argument of type a *)
     B (fun x -> Some x),                                      (* builder *)
     M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ())); (* matcher *)
  ]
}

K stands for "constructor", B for "build", M for "match". Variants BS and MS give read/write access to the state.

type name = string
type doc = string
type ('match_stateful_t, 'match_t, 't) match_t =
  1. | M of ok:'match_t -> ko:(unit -> Data.term) -> 't -> Data.term
  2. | MS of ok:'match_stateful_t -> ko:(Data.state -> Data.state * Data.term * Conversion.extra_goals) -> 't -> Data.state -> Data.state * Data.term * Conversion.extra_goals
type ('build_stateful_t, 'build_t) build_t =
  1. | B of 'build_t
  2. | BS of 'build_stateful_t
type ('stateful_builder, 'builder, 'stateful_matcher, 'matcher, 'self, 'hyps, 'constraints) constructor_arguments =
  1. | N : (Data.state -> Data.state * 'self, 'self, Data.state -> Data.state * Data.term * Conversion.extra_goals, Data.term, 'self, 'hyps, 'constraints) constructor_arguments
  2. | A : 'a Conversion.t * ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
  3. | CA : ('a, 'hyps, 'constraints) ContextualConversion.t * ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
  4. | S : ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
  5. | C : (('self, 'hyps, 'constraints) ContextualConversion.t -> ('a, 'hyps, 'constraints) ContextualConversion.t) * ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self, 'hyps, 'constraints) constructor_arguments

GADT for describing the type of the constructor:

  • N is the terminator
  • A(a,...) is an argument of type a (a is a Conversion.t)
  • S stands for self
  • C stands for container
type ('t, 'h, 'c) constructor =
  1. | K : name * doc * ('build_stateful_t, 'build_t, 'match_stateful_t, 'match_t, 't, 'h, 'c) constructor_arguments * ('build_stateful_t, 'build_t) build_t * ('match_stateful_t, 'match_t, 't) match_t -> ('t, 'h, 'c) constructor
type ('t, 'h, 'c) declaration = {
  1. ty : Conversion.ty_ast;
  2. doc : doc;
  3. pp : Format.formatter -> 't -> unit;
  4. constructors : ('t, 'h, 'c) constructor list;
}
val declare : ('t, 'h, 'c) declaration -> ('t, 'h, 'c) ContextualConversion.t