lambdapi 2.4.0 · OCaml Package

val __sedlex_table_21 : string

val __sedlex_table_25 : string

val __sedlex_table_48 : string

val __sedlex_table_19 : string

val __sedlex_table_1 : string

val __sedlex_table_2 : string

val __sedlex_table_3 : string

val __sedlex_table_4 : string

val __sedlex_table_5 : string

val __sedlex_table_6 : string

val __sedlex_table_7 : string

val __sedlex_table_8 : string

val __sedlex_table_9 : string

val __sedlex_table_10 : string

val __sedlex_table_11 : string

val __sedlex_table_12 : string

val __sedlex_table_13 : string

val __sedlex_table_14 : string

val __sedlex_table_16 : string

val __sedlex_table_17 : string

val __sedlex_table_18 : string

val __sedlex_table_20 : string

val __sedlex_table_23 : string

val __sedlex_table_24 : string

val __sedlex_table_26 : string

val __sedlex_table_27 : string

val __sedlex_table_29 : string

val __sedlex_table_30 : string

val __sedlex_table_31 : string

val __sedlex_table_32 : string

val __sedlex_table_34 : string

val __sedlex_table_35 : string

val __sedlex_table_36 : string

val __sedlex_table_37 : string

val __sedlex_table_38 : string

val __sedlex_table_39 : string

val __sedlex_table_41 : string

val __sedlex_table_42 : string

val __sedlex_table_43 : string

val __sedlex_table_44 : string

val __sedlex_table_45 : string

val __sedlex_table_46 : string

val __sedlex_table_47 : string

val __sedlex_table_49 : string

val __sedlex_table_50 : string

val __sedlex_table_51 : string

val __sedlex_table_52 : string

val __sedlex_table_53 : string

val __sedlex_table_54 : string

val __sedlex_table_55 : string

val __sedlex_table_56 : string

val __sedlex_table_57 : string

val __sedlex_table_59 : string

val __sedlex_table_61 : string

val __sedlex_table_62 : string

val __sedlex_table_63 : string

val __sedlex_table_64 : string

val __sedlex_table_65 : string

val __sedlex_table_66 : string

val __sedlex_table_67 : string

val __sedlex_table_33 : string

val __sedlex_table_58 : string

val __sedlex_table_15 : string

val __sedlex_table_40 : string

val __sedlex_table_22 : string

val __sedlex_table_28 : string

val __sedlex_table_60 : string

val __sedlex_partition_48 : int -> int

val __sedlex_partition_58 : int -> int

val __sedlex_partition_20 : int -> int

val __sedlex_partition_25 : int -> int

val __sedlex_partition_41 : int -> int

val __sedlex_partition_42 : int -> int

val __sedlex_partition_8 : int -> int

val __sedlex_partition_66 : int -> int

val __sedlex_partition_21 : int -> int

val __sedlex_partition_38 : int -> int

val __sedlex_partition_57 : int -> int

val __sedlex_partition_64 : int -> int

val __sedlex_partition_16 : int -> int

val __sedlex_partition_63 : int -> int

val __sedlex_partition_28 : int -> int

val __sedlex_partition_50 : int -> int

val __sedlex_partition_10 : int -> int

val __sedlex_partition_12 : int -> int

val __sedlex_partition_17 : int -> int

val __sedlex_partition_52 : int -> int

val __sedlex_partition_68 : int -> int

val __sedlex_partition_4 : int -> int

val __sedlex_partition_32 : int -> int

val __sedlex_partition_15 : int -> int

val __sedlex_partition_19 : int -> int

val __sedlex_partition_33 : int -> int

val __sedlex_partition_26 : int -> int

val __sedlex_partition_71 : int -> int

val __sedlex_partition_49 : int -> int

val __sedlex_partition_65 : int -> int

val __sedlex_partition_7 : int -> int

val __sedlex_partition_54 : int -> int

val __sedlex_partition_44 : int -> int

val __sedlex_partition_55 : int -> int

val __sedlex_partition_67 : int -> int

val __sedlex_partition_14 : int -> int

val __sedlex_partition_53 : int -> int

val __sedlex_partition_39 : int -> int

val __sedlex_partition_9 : int -> int

val __sedlex_partition_23 : int -> int

val __sedlex_partition_24 : int -> int

val __sedlex_partition_40 : int -> int

val __sedlex_partition_2 : int -> int

val __sedlex_partition_46 : int -> int

val __sedlex_partition_51 : int -> int

val __sedlex_partition_61 : int -> int

val __sedlex_partition_3 : int -> int

val __sedlex_partition_31 : int -> int

val __sedlex_partition_37 : int -> int

val __sedlex_partition_47 : int -> int

val __sedlex_partition_70 : int -> int

val __sedlex_partition_13 : int -> int

val __sedlex_partition_1 : int -> int

val __sedlex_partition_36 : int -> int

val __sedlex_partition_43 : int -> int

val __sedlex_partition_59 : int -> int

val __sedlex_partition_62 : int -> int

val __sedlex_partition_27 : int -> int

val __sedlex_partition_34 : int -> int

val __sedlex_partition_45 : int -> int

val __sedlex_partition_56 : int -> int

val __sedlex_partition_11 : int -> int

val __sedlex_partition_18 : int -> int

val __sedlex_partition_6 : int -> int

val __sedlex_partition_60 : int -> int

val __sedlex_partition_69 : int -> int

val __sedlex_partition_73 : int -> int

val __sedlex_partition_22 : int -> int

val __sedlex_partition_30 : int -> int

val __sedlex_partition_35 : int -> int

val __sedlex_partition_72 : int -> int

val __sedlex_partition_29 : int -> int

val __sedlex_partition_5 : int -> int

Lexer for Lambdapi syntax, using Sedlex, a Utf8 lexer generator.

val remove_first : Sedlexing.lexbuf -> string

val remove_last : Sedlexing.lexbuf -> string

val remove_ends : Sedlexing.lexbuf -> string

exception SyntaxError of Common.Pos.strloc

val syntax_error : 
  (Stdlib.Lexing.position * Stdlib.Lexing.position) ->
  string ->
  'a

val fail : Sedlexing.lexbuf -> string -> 'a

val invalid_character : Sedlexing.lexbuf -> 'a

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

val is_regid : string -> bool

val escape : string -> string

escape s converts a string s into an escaped identifier if it is not regular. We do not check whether s contains "|}". FIXME?

val remove_useless_escape : string -> string

remove_useless_escape s replaces escaped regular identifiers by their unescape form.

val qid : bool -> string list -> Sedlexing.lexbuf -> token

val comment : (Sedlexing.lexbuf -> token) -> int -> Sedlexing.lexbuf -> token

val token : 
  Sedlexing.lexbuf ->
  unit ->
  token * Stdlib.Lexing.position * Stdlib.Lexing.position

package lambdapi