elpi

ELPI - Embeddable λProlog Interpreter
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library elpi
Module Elpi . API . Conversion
type ty_ast =
| TyName of string
| TyApp of string * ty_ast * ty_ast list
type extra_goal = ..
type extra_goal +=
| Unify of Data.term * Data.term
type extra_goals = extra_goal list
type 'a embedding = depth:int -> Data.state -> 'a -> Data.state * Data.term * extra_goals
type 'a readback = depth:int -> Data.state -> Data.term -> Data.state * 'a * extra_goals
type 'a t = {
ty : ty_ast;
pp_doc : Format.formatter -> unit -> unit;
pp : Format.formatter -> 'a -> unit;
embed : 'a embedding;
readback : 'a readback;
}
exception TypeErr of ty_ast * int * Data.term