BuiltInPredicate (elpi.Elpi.API.BuiltInPredicate)

exception No_clause

type name = string

type doc = string

type 'a oarg =

| Keep

| Discard

type 'a ioarg = private

| Data of 'a

| NoData

type once

type ('function_type, 'inernal_outtype_in, 'internal_hyps, 'internal_constraints)
  ffi =

| In : 't Conversion.t
  * doc
  * ( 'i, 'o, 'h, 'c ) ffi -> ( 't -> 'i, 'o, 'h, 'c ) ffi

| Out : 't Conversion.t
  * doc
  * ( 'i, 'o * 't option, 'h, 'c ) ffi -> ( 't oarg -> 'i, 'o, 'h, 'c ) ffi

| InOut : 't ioarg Conversion.t
  * doc
  * ( 'i, 'o * 't option, 'h, 'c ) ffi -> ( 't ioarg -> 'i, 'o, 'h, 'c ) ffi

| CIn : ( 't, 'h, 'c ) ContextualConversion.t
  * doc
  * ( 'i, 'o, 'h, 'c ) ffi -> ( 't -> 'i, 'o, 'h, 'c ) ffi

| COut : ( 't, 'h, 'c ) ContextualConversion.t
  * doc
  * ( 'i, 'o * 't option, 'h, 'c ) ffi -> ( 't oarg -> 'i, 'o, 'h, 'c ) ffi

| CInOut : ( 't ioarg, 'h, 'c ) ContextualConversion.t
  * doc
  * ( 'i, 'o * 't option, 'h, 'c ) ffi -> ( 't ioarg -> 'i, 'o, 'h, 'c ) ffi

| Easy : doc -> ( depth:int -> 'o, 'o, unit, unit ) ffi

| Read : ( 'h, 'c ) ContextualConversion.ctx_readback
  * doc -> ( depth:int -> 'h -> 'c -> Data.state -> 'o, 'o, 'h, 'c ) ffi

| Full : ( 'h, 'c ) ContextualConversion.ctx_readback
  * doc -> ( depth:int ->
             'h ->
             'c ->
             Data.state ->
             Data.state * 'o * Conversion.extra_goals,
             'o,
             'h,
             'c )
             ffi

| FullHO : ( 'h, 'c ) ContextualConversion.ctx_readback
  * doc -> ( once:once ->
             depth:int ->
             'h ->
             'c ->
             Data.state ->
             Data.state * 'o * Conversion.extra_goals,
             'o,
             'h,
             'c )
             ffi

| VariadicIn : ( 'h, 'c ) ContextualConversion.ctx_readback
  * ( 't, 'h, 'c ) ContextualConversion.t
  * doc -> ( 't list ->
             depth:int ->
             'h ->
             'c ->
             Data.state ->
             Data.state * 'o,
             'o,
             'h,
             'c )
             ffi

| VariadicOut : ( 'h, 'c ) ContextualConversion.ctx_readback
  * ( 't, 'h, 'c ) ContextualConversion.t
  * doc -> ( 't oarg list ->
             depth:int ->
             'h ->
             'c ->
             Data.state ->
             Data.state * ('o * 't option list option),
             'o,
             'h,
             'c )
             ffi

| VariadicInOut : ( 'h, 'c ) ContextualConversion.ctx_readback
  * ( 't ioarg, 'h, 'c ) ContextualConversion.t
  * doc -> ( 't ioarg list ->
             depth:int ->
             'h ->
             'c ->
             Data.state ->
             Data.state * ('o * 't option list option),
             'o,
             'h,
             'c )
             ffi

type t =

| Pred : name * ( 'a, unit, 'h, 'c ) ffi * 'a -> t

val mkData : 'a -> 'a ioarg

Tools for InOut arguments. * * InOut arguments need to be equipped with an 'a ioarg Conversion.t. * The ioarg adaptor here maps variables to NoData and anything else to the * to Data of the provided 'a Conversion.t. * * If the 'a is an atomic data type, eg int, then things are good. * If the 'a is an algebraic data type then some more work has to be done * in order to have a good implementation, but the type system cannot * enforce it hence this documentation. Let's take the example of int option. * The Conversion.t to be passed is int ioarg option ioarg Conversion.t, * that is, ioarg should wrap each type constructor. In this way the user * can pass non-ground terms. Eg * given term : X none some X some 3 * readback to: NoData Data None Data (Some NoData) Data (Some (Data 3)) * * Alternatively the data type 'a must be able to represent unification * variables, such as the raw terms, see ioarg_any below. It gives NoData * if the user passed _ (Discard) and Data t for any other t including * variables such as X (UnifVar). * * An example of an API taking advantage of this feature is * pred typecheck i:term, o:ty, o:diagnostic * that can be used to both check a term is well typed and backtrack if not * typecheck T TY ok * or assert a term is illtyped or to test weather it is illtyped * typecheck T TY (error _), typecheck T TY Diagnostic * The ML code can see in which case we are and for example optimize the * first case by not even generating the error message (since error "message" * would fail to unify with ok anyway) or the second one by not assigning TY.

val ioargC : 
  ( 't, 'h, 'c ) ContextualConversion.t ->
  ( 't ioarg, 'h, 'c ) ContextualConversion.t

val ioarg : 't Conversion.t -> 't ioarg Conversion.t

val ioargC_flex : 
  ( 't, 'h, 'c ) ContextualConversion.t ->
  ( 't ioarg, 'h, 'c ) ContextualConversion.t

val ioarg_flex : 't Conversion.t -> 't ioarg Conversion.t

val ioarg_any : Data.term ioarg Conversion.t

module Notation : sig ... end

module HOAdaptors : sig ... end

Adaptors for standard HO functions