ContextualConversion (u.c73734534e52e3c7e3a6ab4ddda12c49.elpi.3.4.5.doc.elpi.runtime.Elpi

type ty_ast = Conversion.ty_ast =

| TyName of string
| TyApp of string * ty_ast * ty_ast list

val pp_ty_ast : 
  Ppx_deriving_runtime.Format.formatter ->
  ty_ast ->
  Ppx_deriving_runtime.unit

val show_ty_ast : ty_ast -> Ppx_deriving_runtime.string

type ('a, 'hyps, 'constraints) embedding =
  depth:int ->
  'hyps ->
  'constraints ->
  State.t ->
  'a ->
  State.t * term * Conversion.extra_goals

type ('a, 'hyps, 'constraints) readback =
  depth:int ->
  'hyps ->
  'constraints ->
  State.t ->
  term ->
  State.t * 'a * Conversion.extra_goals

type ('a, 'hyps, 'constraints) t = {

ty : ty_ast;
pp_doc : Format.formatter -> unit -> unit;
pp : Format.formatter -> 'a -> unit;
embed : ('a, 'hyps, 'constraints) embedding;
readback : ('a, 'hyps, 'constraints) readback;

}

val pp : 
  'a 'hyps 'constraints. (Ppx_deriving_runtime.Format.formatter ->
                           'a ->
                           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'hyps -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter ->
    'constraints ->
    Ppx_deriving_runtime.unit) ->
  Ppx_deriving_runtime.Format.formatter ->
  ('a, 'hyps, 'constraints) t ->
  Ppx_deriving_runtime.unit

val show : 
  'a 'hyps 'constraints. (Ppx_deriving_runtime.Format.formatter ->
                           'a ->
                           Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter -> 'hyps -> Ppx_deriving_runtime.unit) ->
  (Ppx_deriving_runtime.Format.formatter ->
    'constraints ->
    Ppx_deriving_runtime.unit) ->
  ('a, 'hyps, 'constraints) t ->
  Ppx_deriving_runtime.string

type ('hyps, 'constraints) ctx_readback =
  depth:int ->
  hyps ->
  constraints ->
  State.t ->
  State.t * 'hyps * 'constraints * Conversion.extra_goals

val unit_ctx : (unit, unit) ctx_readback

val raw_ctx : (hyps, constraints) ctx_readback

val (!<) : ('a, unit, unit) t -> 'a Conversion.t

val (!>) : 'a Conversion.t -> ('a, 'b, 'c) t

val (!<<) : 
  (('a, 'b, 'c) t -> ('d, unit, unit) t) ->
  'a Conversion.t ->
  'd Conversion.t

val (!>>) : 
  ('a Conversion.t -> 'b Conversion.t) ->
  ('a, 'c, 'd) t ->
  ('b, 'c, 'd) t

val (!>>>) : 
  ('a Conversion.t -> 'b Conversion.t -> 'c Conversion.t) ->
  ('a, 'd, 'e) t ->
  ('b, 'd, 'e) t ->
  ('c, 'd, 'e) t