package acgtk

  1. Overview
  2. Docs
package acgtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module implements lexicons

Exceptions raised when interpretations of types or constants are duplicated

exception Duplicate_type_interpretation
exception Duplicate_constant_interpretation
exception Not_almost_linear
type t

The type of the lexicon as abstract object

type dumped_t

The type of the lexicon as abstract object when beeing dumped

val prepare_dump : t -> dumped_t

prepare_dump lex returns a dumped_t data structure ready to be dumped on disk.

val name_of_dumped : dumped_t -> string

name_of_dumped d_l returns the name of d_l

val recover_from_dump : filename:string -> get_sig:(string -> Signature.Data_Signature.t) -> dumped_t -> t

recover_frun_dump ~filename ~get_sig d_lex returns a t data structure from its dumped (on disk) version. filename is expected to be the file from which the lexicon is recovered, and get_sig a function that returns a signature (in an environment) from its name.

type resumptions

The type of the resumption when parses of terms are computed

type dependency =
  1. | Signatures of string * string
  2. | Lexicons of string list
    (*

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

    *)
type parsing =
  1. | Unavailable
  2. | Available_with_magic
  3. | Available_wo_magic
    (*

    the type to describe parsing capabilities of a lexicon

    *)
val get_dependencies : t -> dependency

get_dependencies l returns the direct dependencies of l

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 short_pp : Stdlib.Format.formatter -> t -> unit

short_pp fmt lex pretty prints the name of the lexicon lex, and its abstract and object signatures, on the formatter fmt

val pp : Stdlib.Format.formatter -> t -> unit

pp fmt lex pretty prints the lexicon lex on the formatter fmt

val get_program : t -> DatalogLib.Datalog.Datalog.Program.program option

get_program lex returns None if no datalog programm is associated to lex (for instance if lex is not 2d-order), and Some p if p is associated to lex

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

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 UtilsLib.Error.AcgtkError built out of Errors.Lexicon_l.MissingInterpretations error otherwise.

parse ~alt_max ~magic 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. If magic is set to true (default), uses magic set rewritten programs. Use datalog reduced programs if magic is set to false. 10^alt_max is the max number of delayed computations before moving to non-regular sorting.

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 : resumptions -> 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.

compose [(l1,pos1); (l2,pos2); (l3,pos3); … ; (ln,posn)] (name,loc) returns a new lexicon ln∘….∘l3∘l2∘l1 (note the order!)

val pp_query : t -> Stdlib.Format.formatter -> (Signature.Data_Signature.term * Signature.Data_Signature.stype) -> unit

pp_query lex fmt unit (term, ty) pretty prints the query associated to the object term term and the abstract type ty according to the lexicon lex on the formatter fmt.

val magic : t -> t

magic lex returns a new lexicon where the magic programs have been created

val has_magic : t -> parsing

magig lex returns true if magic programs are available for lex, and false otherwise