package acgtk

  1. Overview
  2. Docs

Exceptions raised when interpretations of types or constants are duplicated

exception Duplicate_type_interpretation
exception Duplicate_constant_interpretation

The type of the lexicon as abstract object

It contains a module that allows for manipulating the associated signatures

type signature = Signature.t
type resume
type dependency =
  1. | Signatures of signature * signature
  2. | Lexicons of t * t

The type of dependencies of lexicons, in order to compute when recompilation is required if a signature or a lexicon is extended

type data =
  1. | Signature of signature
  2. | Lexicon of t
val get_dependencies : t -> dependency

get_dependencies l returns the direct dependencies of l

val empty : ?non_linear:bool -> abs:signature -> obj:signature -> (string * Logic.Abstract_syntax.Abstract_syntax.location) -> t

empty name returns the empty lexicon of name name

val is_linear : t -> bool

is_linear l returns true if the lexicon l is linear, and false otherwise

name l returns the name of the lexicon l and the location of its definition

insert e l returns a lexicon where the interpretation e has been added

val to_string : t -> string

to_string l returns a string describing the lexicon l. Should be parsable

val interpret_type : Signature.stype -> t -> Signature.stype

interpret_type t l returns the interpreted (object) type of the (abstract) type t by the lexicon l

interpret_term t l returns the interpreted (object) term of the (abstract) term t by the lexicon l

interpret t ty l returns the interpreted (object) term and type of the (abstract) term t and type ty by the lexicon l

val get_sig : t -> signature * signature

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 -> unit

check 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 -> resume

parse 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 * resume

get_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 -> bool

is_empty r tells whether there is another solution to look in the resumption

val compose : t -> t -> (string * Logic.Abstract_syntax.Abstract_syntax.location) -> t

compose 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.t

program_to_buffer l returns a buffer containing a parsable version of l

val program_to_log : Logs.src -> Logs.level -> t -> unit

program_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.t

query_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 -> unit

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

val update : t -> (string -> data) -> t