elpi
ELPI - Embeddable λProlog Interpreter
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Library elpi
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, '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