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. * * 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.