package acgtk
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha512=5d380a947658fb1201895cb4cb449b1f60f54914c563e85181d628a89f045c1dd7b5b2226bb7865dd090f87caa9187e0ea6c7a4ee3dc3dda340d404c4e76c7c2
doc/acgtk.acgData/AcgData/Acg_lexicon/Data_Lexicon/index.html
Module Acg_lexicon.Data_LexiconSource
This module implements lexicons
Exceptions raised when interpretations of types or constants are duplicated
The type of the lexicon as abstract object
The type of the lexicon as abstract object when beeing dumped
prepare_dump lex returns a dumped_t data structure ready to be dumped on disk.
val recover_from_dump :
filename:string ->
get_sig:(string -> Signature.Data_Signature.t) ->
dumped_t ->
trecover_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.
The type of the resumption when parses of terms are computed
get_dependencies l returns the direct dependencies of l
val empty :
?non_linear:bool ->
abs:Signature.Data_Signature.t ->
obj:Signature.Data_Signature.t ->
(string * Logic.Abstract_syntax.Abstract_syntax.location) ->
tempty name returns the empty lexicon of name name
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
short_pp fmt lex pretty prints the name of the lexicon lex, and its abstract and object signatures, on the formatter fmt
pp fmt lex pretty prints the lexicon lex on the formatter fmt
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
val interpret :
Signature.Data_Signature.term ->
Signature.Data_Signature.stype ->
t ->
Signature.Data_Signature.term * Signature.Data_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.
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.
val parse :
alt_max:int ->
?magic:bool ->
(Signature.Data_Signature.term * Signature.Data_Signature.stype) ->
Signature.Data_Signature.stype ->
t ->
resumptionsparse ~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.
val get_analysis :
resumptions ->
t ->
(Logic.Lambda.Lambda.term * Containers.SharedForest.SharedForest.weight)
option
* resumptionsget_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').
is_empty r tells whether there is another solution to look in the resumption
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 compose_lexicons :
(t * Logic.Abstract_syntax.Abstract_syntax.location) list ->
(string * Logic.Abstract_syntax.Abstract_syntax.location) ->
tcompose [(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 ->
Format.formatter ->
(Signature.Data_Signature.term * Signature.Data_Signature.stype) ->
unitpp_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.