package lambdapi
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704
doc/lambdapi.parsing/Parsing/LpLexer/index.html
Module Parsing.LpLexer
Source
Lexer for Lambdapi syntax, using Sedlex, a Utf8 lexer generator.
type token =
| EOF
| ABORT
| ADMIT
| ADMITTED
| APPLY
| AS
| ASSERT of bool
| ASSOCIATIVE
| ASSUME
| BEGIN
| BUILTIN
| COERCE_RULE
| COMMUTATIVE
| COMPUTE
| CONSTANT
| DEBUG
| END
| FAIL
| FLAG
| GENERALIZE
| HAVE
| IN
| INDUCTION
| INDUCTIVE
| INFIX
| INJECTIVE
| LET
| NOTATION
| OPAQUE
| OPEN
| POSTFIX
| PREFIX
| PRINT
| PRIVATE
| PROOFTERM
| PROTECTED
| PROVER
| PROVER_TIMEOUT
| QUANTIFIER
| REFINE
| REFLEXIVITY
| REMOVE
| REQUIRE
| REWRITE
| RULE
| SEARCH
| SEQUENTIAL
| SIMPLIFY
| SOLVE
| SYMBOL
| SYMMETRY
| TRY
| TYPE_QUERY
| TYPE_TERM
| UNIF_RULE
| VERBOSE
| WHY3
| WITH
| DEBUG_FLAGS of bool * string
| NAT of string
| FLOAT of string
| SIDE of Pratter.associativity
| STRINGLIT of string
| SWITCH of bool
| ARROW
| ASSIGN
| BACKQUOTE
| COMMA
| COLON
| DOT
| EQUIV
| HOOK_ARROW
| LAMBDA
| L_CU_BRACKET
| L_PAREN
| L_SQ_BRACKET
| PI
| R_CU_BRACKET
| R_PAREN
| R_SQ_BRACKET
| SEMICOLON
| TURNSTILE
| UNDERSCORE
| VBAR
| UID of string
| UID_EXPL of string
| UID_META of int
| UID_PATT of string
| QID of Common.Path.t
| QID_EXPL of Common.Path.t
Tokens.
Identifiers.
There are two kinds of identifiers: regular identifiers and escaped identifiers of the form "{|...|}"
.
Modulo those surrounding brackets, escaped identifiers allow to use as identifiers keywords or filenames that are not regular identifiers.
An escaped identifier denoting a filename or directory is unescaped before accessing to it. Hence, the module "{|a b|}"
refers to the file "a b"
.
Identifiers need to be normalized so that an escaped identifier, once unescaped, is not regular. To this end, every identifier of the form "{|s|}"
with s regular, is understood as "s"
(function remove_useless_escape
below).
Finally, identifiers must not be empty, so that we can use the empty string for the path of ghost signatures.
escape s
converts a string s
into an escaped identifier if it is not regular. We do not check whether s
contains "|}"
. FIXME?
remove_useless_escape s
replaces escaped regular identifiers by their unescape form.