package elpi

  1. Overview
  2. Docs

This module defines what embedding and readback functions are

type ty_ast =
  1. | TyName of string
  2. | TyApp of string * ty_ast * ty_ast list
type extra_goal = ..
type extra_goal +=
  1. | 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 = {
  1. ty : ty_ast;
  2. pp_doc : Format.formatter -> unit -> unit;
  3. pp : Format.formatter -> 'a -> unit;
  4. embed : 'a embedding;
  5. readback : 'a readback;
}
exception TypeErr of ty_ast * int * Data.term