package acgtk
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=5d380a947658fb1201895cb4cb449b1f60f54914c563e85181d628a89f045c1dd7b5b2226bb7865dd090f87caa9187e0ea6c7a4ee3dc3dda340d404c4e76c7c2
doc/acgtk.acgData/AcgData/Acg_lexicon/Data_Lexicon/index.html
Module Acg_lexicon.Data_Lexicon
Source
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 ->
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.
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) ->
t
empty 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.stype
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
.
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 ->
resumptions
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.
val get_analysis :
resumptions ->
t ->
(Logic.Lambda.Lambda.term * Containers.SharedForest.SharedForest.weight)
option
* resumptions
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')
.
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) ->
t
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 ->
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
.