package elpi

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module API.AlgebraicDataSource

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.

Sourcetype name = string
Sourcetype doc = string
Sourcetype ('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
Sourcetype ('build_stateful_t, 'build_t) build_t =
  1. | B of 'build_t
  2. | BS of 'build_stateful_t
Sourcetype ('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
Sourcetype ('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
Sourcetype ('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;
}
Sourceval declare : ('t, 'h, 'c) declaration -> ('t, 'h, 'c) ContextualConversion.t
OCaml

Innovation. Community. Security.