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
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 ('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 ('stateful_builder, 'builder, 'stateful_matcher, 'matcher, 'self)
constructor_arguments =
| N : (Data.state -> Data.state * 'self, 'self, Data.state -> Data.state * Data.term * Conversion.extra_goals, Data.term, 'self) constructor_arguments| A : 'a Conversion.t * ('bs, 'b, 'ms, 'm, 'self) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self) constructor_arguments| S : ('bs, 'b, 'ms, 'm, 'self) constructor_arguments -> ('self -> 'bs, 'self -> 'b, 'self -> 'ms, 'self -> 'm, 'self) constructor_arguments| C : ('self Conversion.t -> 'a Conversion.t) * ('bs, 'b, 'ms, 'm, 'self) constructor_arguments -> ('a -> 'bs, 'a -> 'b, 'a -> 'ms, 'a -> 'm, 'self) 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)
type 't constructor = | K : name * doc * ('build_stateful_t, 'build_t, 'match_stateful_t, 'match_t, 't) constructor_arguments * ('build_stateful_t, 'build_t) build_t * ('match_stateful_t, 'match_t, 't) match_t -> 't constructor
type 't declaration = {ty : Conversion.ty_ast;doc : doc;pp : Format.formatter -> 't -> unit;constructors : 't constructor list;
}val declare : 'a declaration -> 'a Conversion.t