package elpi

  1. Overview
  2. Docs

This module defines what embedding and readback functions are for datatypes that need the context of the program (hypothetical clauses and constraints)

type ty_ast = Conversion.ty_ast =
  1. | TyName of string
  2. | 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 = {
  1. ty : ty_ast;
  2. pp_doc : Format.formatter -> unit -> unit;
  3. pp : Format.formatter -> 'a -> unit;
  4. embed : ('a, 'h, 'c) embedding;
  5. 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