ContextualConversion (p.elpi.2.0.7.doc.elpi.runtime.Elpi

Sourcetype 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

Sourceval show_ty_ast : ty_ast -> Ppx_deriving_runtime.string

Source

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

Source

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

Sourcetype ('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;

}

Source

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

Source

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

Source

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

Sourceval unit_ctx : (unit, unit) ctx_readback

Sourceval raw_ctx : (hyps, constraints) ctx_readback

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

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

Source

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

Source

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