Module `Acg_lexicon.Data_Lexicon`Source

Exceptions raised when interpretations of types or constants are duplicated

Sourceexception Duplicate_type_interpretation

Sourceexception Duplicate_constant_interpretation

Sourcetype t

The type of the lexicon as abstract object

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

It contains a module that allows for manipulating the associated signatures

Sourcetype signature = Signature.t

Sourcetype resume

Sourcetype dependency =

| Signatures of signature * signature
| 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

Sourcetype data =

| Signature of signature
| Lexicon of t

Sourceval get_dependencies : t -> dependency

get_dependencies l returns the direct dependencies of l

Source

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

Sourceval is_linear : t -> bool

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

Sourceval name : t -> string * Logic.Abstract_syntax.Abstract_syntax.location

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

Sourceval insert : Logic.Abstract_syntax.Abstract_syntax.lex_entry -> t -> t

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

Sourceval to_string : t -> string

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

Sourceval 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

Sourceval interpret_term : Logic.Lambda.Lambda.term -> t -> Logic.Lambda.Lambda.term

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

Source

val interpret : 
  Signature.term ->
  Signature.stype ->
  t ->
  Signature.term * Signature.stype

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

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

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

Sourceval 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

Sourceval 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').

Sourceval is_empty : resume -> bool

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

Source

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.

Sourceval program_to_buffer : t -> Buffer.t

program_to_buffer l returns a buffer containing a parsable version of l

Sourceval 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

Sourceval query_to_buffer : Signature.term -> Signature.stype -> t -> 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.

Source

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.

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/acgtkLib.acgData/AcgData/Acg_lexicon/Data_Lexicon/index.html

Module `Acg_lexicon.Data_Lexicon`Source

package acgtk

Install

Dune Dependency

Authors

Maintainers

Sources

doc/acgtkLib.acgData/AcgData/Acg_lexicon/Data_Lexicon/index.html

Module Acg_lexicon.Data_LexiconSource

Module `Acg_lexicon.Data_Lexicon`Source