Exceptions raised when interpretations of types or constants are duplicated
module Signature :
Interface.Signature_sig
with type term = Logic.Lambda.Lambda.term
with type term = Logic.Lambda.Lambda.term
with type stype = Logic.Lambda.Lambda.stypeIt contains a module that allows for manipulating the associated signatures
type signature = Signature.tThe type of dependencies of lexicons, in order to compute when recompilation is required if a signature or a lexicon is extended
val get_dependencies : t -> dependencyget_dependencies l returns the direct dependencies of l
val empty :
(string * Logic.Abstract_syntax.Abstract_syntax.location) ->
?non_linear:bool ->
abs:signature ->
obj:signature ->
tempty name returns the empty lexicon of name name
val is_linear : t -> boolis_linear l returns true if the lexicon l is linear, and false otherwise
val name : t -> string * Logic.Abstract_syntax.Abstract_syntax.locationname l returns the name of the lexicon l and the location of its definition
val insert : Logic.Abstract_syntax.Abstract_syntax.lex_entry -> t -> tinsert e l returns a lexicon where the interpretation e has been added
val to_string : t -> stringto_string l returns a string describing the lexicon l. Should be parsable
val interpret_type : Signature.stype -> t -> Signature.stypeinterpret_type t l returns the interpreted (object) type of the (abstract) type t by the lexicon l
val interpret_term : Logic.Lambda.Lambda.term -> t -> Logic.Lambda.Lambda.terminterpret_term t l returns the interpreted (object) term of the (abstract) term t by the lexicon l
val interpret :
Signature.term ->
Signature.stype ->
t ->
Signature.term * Signature.stypeinterpret t ty l returns the interpreted (object) term and type of the (abstract) term t and type ty by the lexicon l
get_sig l returns a pair (abs_sig,obj_sig) consisting of the astract signature abs_sig and the object signature obj_sig of l.
val check : t -> unitcheck l checks whether a lexicon defines all the required interpretations. Raises an exception Error.Error (Error.Lexicon_error (e,pos)) Error.Error otherwise, where e is of type Error.lexicon_error.
val parse : Signature.term -> Signature.stype -> t -> resumeparse t stype lex tries to parse the (object) term t and find it an antecedent of type stype by lex. It returns a resumption that can be used to look for possible other parses
val get_analysis : resume -> t -> Logic.Lambda.Lambda.term option * resumeget_analysis r l processe the resumption r to check if another solution is available. In this case, it returns a pair (Some t,r') where t is another solution, and r' a new resumption. Otherwise it returns (None,r').
val is_empty : resume -> boolis_empty r tells whether there is another solution to look in the resumption
val compose :
t ->
t ->
(string * Logic.Abstract_syntax.Abstract_syntax.location) ->
tcompose l2 l1 (name,loc) returns a new lexicon which is the composition of l2 and l1 (l2 after l1) such that the abstract signature of the resulting lexicon is the same as the one of l1 and its object signature is the same as the one of l2.
val program_to_buffer : t -> Stdlib.Buffer.tprogram_to_buffer l returns a buffer containing a parsable version of l
val program_to_log : Logs.src -> Logs.level -> t -> unitprogram_to_log src level l logs the content of l according to the source src and the level level
val query_to_buffer : Signature.term -> Signature.stype -> t -> Stdlib.Buffer.tquery_to_buffer te ty l returns a buffer containing a datalog query corresponding to the (object) term te and the (abstract) type ty to be parsed with respect to l.
val query_to_log :
Logs.src ->
Logs.level ->
Signature.term ->
Signature.stype ->
t ->
unitquery_to_log src level te ty l logs the datalog query corresponding to the (object) term te and the (abstract) type ty to be parsed with respect to l on the src source according to the level level.