elpi 1.16.5 · OCaml Package

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 =

| M of ok:'match_t -> ko:(unit -> Data.term) -> 't -> Data.term
| 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 =

| B of 'build_t
| BS of 'build_stateful_t

type ('stateful_builder, 'builder, 'stateful_matcher, 'matcher, 'self, 'hyps, 'constraints)
  constructor_arguments =

| N : (Data.state -> Data.state * 'self, 'self, Data.state -> Data.state * Data.term * Conversion.extra_goals, Data.term, 'self, 'hyps, 'constraints) constructor_arguments
| 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
| 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
| S : ('bs, 'b, 'ms, 'm, 'self, 'hyps, 'constraints) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self, 'hyps, 'constraints) constructor_arguments
| 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 =

| 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 = {

ty : Conversion.ty_ast;
doc : doc;
pp : Stdlib.Format.formatter -> 't -> unit;
constructors : ('t, 'h, 'c) constructor list;

}

val declare : ('t, 'h, 'c) declaration -> ('t, 'h, 'c) ContextualConversion.t

package elpi