module MakeParse: functor (
C
:
PARSABLE_CONST
) ->
functor (
TD
:
S
with type Const.t = C.t
) ->
PARSE
with type term = TD.T.t and type lit = TD.Lit.t and type clause = TD.C.t
type
term
type
lit
type
clause
type
name_ctx = (string, term) Hashtbl.t
val create_ctx : unit -> name_ctx
val term_of_ast : ctx:name_ctx -> TopDownAst.term -> term
val lit_of_ast : ctx:name_ctx -> TopDownAst.literal -> lit
val clause_of_ast : ?ctx:name_ctx -> TopDownAst.clause -> clause
val clauses_of_ast : ?ctx:name_ctx ->
TopDownAst.clause list -> clause list
val parse_chan : Pervasives.in_channel ->
[ `Error of string | `Ok of clause list ]
val parse_file : string -> [ `Error of string | `Ok of clause list ]
val parse_string : string -> [ `Error of string | `Ok of clause list ]
val clause_of_string : string -> clause
Parse a clause from a string, or fail. Useful shortcut to define
properties of relations without building terms by hand.
- Raises
Failure
if the string is not a valid clause
val term_of_string : string -> term
- Raises
Failure
if the string is not a valid term