package elpi

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

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 =

| 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 : Stdlib.Format.formatter -> unit -> unit;
pp : Stdlib.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 raw_ctx : (Data.hyps, Data.constraints) 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