package lambdapi

  1. Overview
  2. Docs
package lambdapi
Legend:
Library
Module
Module type
Parameter
Class
Class type
val __sedlex_table_19 : string
val __sedlex_table_24 : string
val __sedlex_table_47 : string
val __sedlex_table_17 : 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_14 : string
val __sedlex_table_15 : string
val __sedlex_table_16 : string
val __sedlex_table_18 : string
val __sedlex_table_21 : string
val __sedlex_table_22 : string
val __sedlex_table_23 : string
val __sedlex_table_25 : string
val __sedlex_table_26 : string
val __sedlex_table_28 : string
val __sedlex_table_29 : string
val __sedlex_table_30 : string
val __sedlex_table_31 : string
val __sedlex_table_33 : 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_40 : 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_48 : 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_57 : string
val __sedlex_table_59 : string
val __sedlex_table_60 : 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_32 : string
val __sedlex_table_56 : string
val __sedlex_table_13 : string
val __sedlex_table_39 : string
val __sedlex_table_20 : string
val __sedlex_table_27 : string
val __sedlex_table_58 : string
val __sedlex_partition_47 : 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_65 : int -> int
val __sedlex_partition_21 : int -> int
val __sedlex_partition_38 : int -> int
val __sedlex_partition_56 : int -> int
val __sedlex_partition_63 : int -> int
val __sedlex_partition_16 : int -> int
val __sedlex_partition_28 : int -> int
val __sedlex_partition_49 : int -> int
val __sedlex_partition_10 : int -> int
val __sedlex_partition_12 : int -> int
val __sedlex_partition_17 : int -> int
val __sedlex_partition_51 : int -> int
val __sedlex_partition_66 : 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_43 : int -> int
val __sedlex_partition_33 : int -> int
val __sedlex_partition_26 : int -> int
val __sedlex_partition_69 : int -> int
val __sedlex_partition_48 : int -> int
val __sedlex_partition_64 : int -> int
val __sedlex_partition_7 : int -> int
val __sedlex_partition_53 : int -> int
val __sedlex_partition_62 : int -> int
val __sedlex_partition_60 : int -> int
val __sedlex_partition_54 : int -> int
val __sedlex_partition_14 : int -> int
val __sedlex_partition_52 : 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_44 : int -> int
val __sedlex_partition_50 : int -> int
val __sedlex_partition_59 : int -> int
val __sedlex_partition_3 : int -> int
val __sedlex_partition_31 : int -> int
val __sedlex_partition_37 : int -> int
val __sedlex_partition_46 : int -> int
val __sedlex_partition_68 : int -> int
val __sedlex_partition_13 : int -> int
val __sedlex_partition_1 : int -> int
val __sedlex_partition_36 : int -> int
val __sedlex_partition_57 : int -> int
val __sedlex_partition_61 : int -> int
val __sedlex_partition_27 : int -> int
val __sedlex_partition_34 : int -> int
val __sedlex_partition_45 : int -> int
val __sedlex_partition_55 : int -> int
val __sedlex_partition_11 : int -> int
val __sedlex_partition_18 : int -> int
val __sedlex_partition_6 : int -> int
val __sedlex_partition_58 : int -> int
val __sedlex_partition_67 : int -> int
val __sedlex_partition_71 : int -> int
val __sedlex_partition_22 : int -> int
val __sedlex_partition_30 : int -> int
val __sedlex_partition_35 : int -> int
val __sedlex_partition_70 : 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 =
  1. | EOF
  2. | ABORT
  3. | ADMIT
  4. | ADMITTED
  5. | APPLY
  6. | AS
  7. | ASSERT of bool
  8. | ASSOCIATIVE
  9. | ASSUME
  10. | BEGIN
  11. | BUILTIN
  12. | COMMUTATIVE
  13. | COMPUTE
  14. | CONSTANT
  15. | DEBUG
  16. | END
  17. | FAIL
  18. | FLAG
  19. | GENERALIZE
  20. | HAVE
  21. | IN
  22. | INDUCTION
  23. | INDUCTIVE
  24. | INFIX
  25. | INJECTIVE
  26. | LET
  27. | NOTATION
  28. | OPAQUE
  29. | OPEN
  30. | PREFIX
  31. | PRINT
  32. | PRIVATE
  33. | PROOFTERM
  34. | PROTECTED
  35. | PROVER
  36. | PROVER_TIMEOUT
  37. | QUANTIFIER
  38. | REFINE
  39. | REFLEXIVITY
  40. | REQUIRE
  41. | REWRITE
  42. | RULE
  43. | SEQUENTIAL
  44. | SIMPLIFY
  45. | SOLVE
  46. | SYMBOL
  47. | SYMMETRY
  48. | TYPE_QUERY
  49. | TYPE_TERM
  50. | UNIF_RULE
  51. | VERBOSE
  52. | WHY3
  53. | WITH
  54. | DEBUG_FLAGS of bool * string
  55. | NAT of string
  56. | FLOAT of float
  57. | SIDE of Pratter.associativity
  58. | STRINGLIT of string
  59. | SWITCH of bool
  60. | ARROW
  61. | ASSIGN
  62. | BACKQUOTE
  63. | COMMA
  64. | COLON
  65. | DOT
  66. | EQUIV
  67. | HOOK_ARROW
  68. | LAMBDA
  69. | L_CU_BRACKET
  70. | L_PAREN
  71. | L_SQ_BRACKET
  72. | PI
  73. | R_CU_BRACKET
  74. | R_PAREN
  75. | R_SQ_BRACKET
  76. | SEMICOLON
  77. | TURNSTILE
  78. | UNDERSCORE
  79. | VBAR
  80. | UID of string
  81. | UID_EXPL of string
  82. | UID_META of int
  83. | UID_PATT of string
  84. | QID of Common.Path.t
  85. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct