ContextualConversion (elpi.Elpi.API.ContextualConversion)

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