elpi

ELPI - Embeddable λProlog Interpreter
Library elpi
Module Elpi . API . AlgebraicData
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 : Format.formatter -> 't -> unit;
constructors : ( 't, 'h, 'c ) constructor list;
}
val declare : ( 't, 'h, 'c ) declaration -> ( 't, 'h, 'c ) ContextualConversion.t