elpi

ELPI - Embeddable λProlog Interpreter
Library elpi
type ty_ast = Conversion.ty_ast =
| TyName of string
| TyApp of string * ty_ast * ty_ast list
type ('a, 'hyps, 'constraints) embedding = depth:int -> 'hyps -> 'constraints -> Data.state -> 'a -> Data.state * Data.term * Conversion.extra_goals
type ('a, 'hyps, 'constraints) readback = depth:int -> 'hyps -> 'constraints -> Data.state -> Data.term -> Data.state * 'a * Conversion.extra_goals
type ('a, 'h, 'c) t = {
ty : ty_ast;
pp_doc : Format.formatter -> unit -> unit;
pp : Format.formatter -> 'a -> unit;
embed : ( 'a, 'h, 'c ) embedding;
readback : ( 'a, 'h, 'c ) readback;
}
type ('hyps, 'constraints) ctx_readback = depth:int -> Data.hyps -> Data.constraints -> Data.state -> Data.state * 'hyps * 'constraints * Conversion.extra_goals
val unit_ctx : ( unit, unit ) ctx_readback
val (!<) : ( 'a, unit, unit ) t -> 'a Conversion.t
val (!>) : 'a Conversion.t -> ( 'a, 'hyps, 'constraints ) t
val (!>>) : ( 'a Conversion.t -> 'b Conversion.t ) -> ( 'a, 'hyps, 'constraints ) t -> ( 'b, 'hyps, 'constraints ) t
val (!>>>) : ( 'a Conversion.t -> 'b Conversion.t -> 'c Conversion.t ) -> ( 'a, 'hyps, 'constraints ) t -> ( 'b, 'hyps, 'constraints ) t -> ( 'c, 'hyps, 'constraints ) t