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_goalstype ('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_argumentsGADT for describing the type of the constructor:
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) constructortype ('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