type ('match_stateful_t, 'match_t, 't) match_t = | M of ok:'match_t -> ko:(unit -> term) -> 't -> term| MS of ok:'match_stateful_t ->
ko:(State.t -> State.t * term * Conversion.extra_goals) ->
't ->
State.t ->
State.t * term * Conversion.extra_goalstype ('stateful_builder, 'builder, 'stateful_matcher, 'matcher, 'self, 'hyps, 'constraints)
constructor_arguments =
| N : (State.t ->
State.t * 'self,
'self,
State.t ->
State.t * term * Conversion.extra_goals,
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_argumentstype ('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;}type ('b, 'm, 't, 'h, 'c) compiled_constructor_arguments = | XN : (State.t ->
State.t * 't,
State.t ->
State.t * term * Conversion.extra_goals,
't,
'h,
'c)
compiled_constructor_arguments| XA : ('a, 'h, 'c) ContextualConversion.t
* ('b, 'm, 't, 'h, 'c) compiled_constructor_arguments -> ('a ->
'b,
'a ->
'm,
't,
'h,
'c)
compiled_constructor_argumentstype ('match_t, 't) compiled_match_t =
ok:'match_t ->
ko:(State.t -> State.t * term * Conversion.extra_goals) ->
't ->
State.t ->
State.t * term * Conversion.extra_goalstype ('t, 'h, 'c) compiled_constructor = | XK : ('build_t, 'matched_t, 't, 'h, 'c) compiled_constructor_arguments
* 'build_t
* ('matched_t, 't) compiled_match_t -> ('t, 'h, 'c) compiled_constructortype ('t, 'h, 'c) compiled_adt =
('t, 'h, 'c) compiled_constructor Elpi_util.Util.Constants.Map.tval buildk :
mkConst:(Elpi_util.Util.constant -> term) ->
Elpi_util.Util.constant ->
term list ->
termval readback_args :
'a 'm 't 'h 'c. look:(depth:int -> term -> term) ->
Conversion.ty_ast ->
depth:int ->
'h ->
'c ->
State.t ->
Conversion.extra_goals list ->
term ->
('a, 'm, 't, 'h, 'c) compiled_constructor_arguments ->
'a ->
term list ->
State.t * 't * Conversion.extra_goalsval readback :
't 'h 'c. mkinterval:(int -> int -> int -> term list) ->
look:(depth:int -> term -> term) ->
alloc:(?name:string -> State.t -> State.t * 'uk) ->
mkUnifVar:('uk -> args:term list -> State.t -> term) ->
Conversion.ty_ast ->
('t, 'h, 'c) compiled_adt ->
depth:int ->
'h ->
'c ->
State.t ->
term ->
State.t * 't * Conversion.extra_goalsval adt_embed_args :
'm 'a 't 'h 'c. mkConst:(int -> term) ->
Conversion.ty_ast ->
('t, 'h, 'c) compiled_adt ->
Elpi_util.Util.constant ->
depth:int ->
'h ->
'c ->
('a, 'm, 't, 'h, 'c) compiled_constructor_arguments ->
(State.t -> State.t * term * Conversion.extra_goals) list ->
'mval embed :
'a 'h 'c. mkConst:(int -> term) ->
Conversion.ty_ast ->
(Stdlib.Format.formatter -> 'a -> unit) ->
('a, 'h, 'c) compiled_adt ->
depth:int ->
'h ->
'c ->
State.t ->
'a ->
State.t * term * Conversion.extra_goalsval compile_arguments :
'b 'bs 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
('t, 'h, 'c) ContextualConversion.t ->
('bs, 'ms, 't, 'h, 'c) compiled_constructor_argumentsval compile_builder_aux :
'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
'b ->
'bsval compile_builder :
'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
('bs, 'b) build_t ->
'bsval compile_matcher_ok :
'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
'ms ->
Conversion.extra_goals Stdlib.ref ->
State.t Stdlib.ref ->
'mval compile_matcher :
'bs 'b 'm 'ms 't 'h 'c. ('bs, 'b, 'ms, 'm, 't, 'h, 'c) constructor_arguments ->
('ms, 'm, 't) match_t ->
('ms, 't) compiled_match_tval tyargs_of_args :
'a 'b 'c 'd 'e. string ->
('a, 'b, 'c, 'd, 'e) compiled_constructor_arguments ->
(bool * string * string) listval compile_constructors :
Conversion.ty_ast ->
('a, 'b, 'c) ContextualConversion.t ->
string ->
('a, 'b, 'c) constructor list ->
('a, 'b, 'c) compiled_constructor Elpi_util.Util.Constants.Map.t
* (bool * string * string) list Elpi_util.Util.StrMap.tval document_kind : Fmt.formatter -> Conversion.ty_ast -> unitval document_adt :
string ->
Conversion.ty_ast ->
('a, 'b, 'c) constructor list ->
(bool * string * string) list Elpi_util.Util.StrMap.t ->
Fmt.formatter ->
unit ->
unit