package acgtk
Install
Dune Dependency
Authors
Maintainers
Sources
sha512=5d380a947658fb1201895cb4cb449b1f60f54914c563e85181d628a89f045c1dd7b5b2226bb7865dd090f87caa9187e0ea6c7a4ee3dc3dda340d404c4e76c7c2
doc/acgtk.grammars/Grammars/Parsers/index.html
Module Grammars.Parsers
Source
This module implements the parsing functions for ACG data files, terms, lexical entries, and signature entries
val parse_data :
?overwrite:bool ->
?output:Format.formatter ->
no_magic:bool ->
Sedlexing.lexbuf ->
AcgData.Environment.Environment.t ->
AcgData.Environment.Environment.t option
parse_data ~override:over ~output:out buf e
parses the file buf
. If the parse is successful, then it returns Some e'
where e'
is e
with the data from filenamne added
. Otherwise it returns None
. The two first parameters indicates whether it is allowed to overwrite an already present signature or lexicon, and whether to ouput the new environment.
val parse_term :
Sedlexing.lexbuf ->
AcgData.Signature.Data_Signature.t ->
(Logic.Lambda.Lambda.term * Logic.Lambda.Lambda.stype) option
parse_term buf sg
parses the term contained in the buffer buf
according to the signature sg
and returns None
if the parse fails and Some (term,stype)
where term
and stype
correspond to buf
.
val parse_type :
Sedlexing.lexbuf ->
AcgData.Signature.Data_Signature.t ->
Logic.Lambda.Lambda.stype option
parse_type buf sg
parses the type contained in the string buf
according to the signature sg
and returns None
if the parse fails and Some stype
where stype
correspond to buf
.
val parse_sig_entry :
Sedlexing.lexbuf ->
AcgData.Signature.Data_Signature.t ->
AcgData.Signature.Data_Signature.t option
parse_sig_entry buf sg e
parses the signature entry buf
and adds it to the signature sg
in the environment e
and returns None
if parsing fails or Some sg'
where sg'
is the new signature.
val parse_lex_entry :
Sedlexing.lexbuf ->
AcgData.Acg_lexicon.Data_Lexicon.t ->
AcgData.Acg_lexicon.Data_Lexicon.t option
parse_lex_entry buf lex e
parses the lexicon entry buf
and adds it to the lexicon lex
in the environment e
and returns None
if parsing fails or Some lex'
where lex'
is the new lexicon.