package lambdapi

  1. Overview
  2. Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (12)

Authors

  1. D
    Deducteam

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-2.5.0.tbz
sha256=9bc8ae3694dd51bd5742e7aba760bd2878c4b0e5ef9b3d4a7b06f3cd303b611d
sha512=c812c3129b3d85b0c4d7e741d11137dbb4fe2a0aaba3a5968409080b742924ecb506280c19ad83ef6bc910346db96d87780313fa7683c29345edae16ae79c704

doc/lambdapi.parsing/Parsing/LpLexer/index.html

Module Parsing.LpLexerSource

Sourceval __sedlex_table_22 : string
Sourceval __sedlex_table_26 : string
Sourceval __sedlex_table_49 : string
Sourceval __sedlex_table_20 : string
Sourceval __sedlex_table_1 : string
Sourceval __sedlex_table_2 : string
Sourceval __sedlex_table_3 : string
Sourceval __sedlex_table_4 : string
Sourceval __sedlex_table_5 : string
Sourceval __sedlex_table_6 : string
Sourceval __sedlex_table_7 : string
Sourceval __sedlex_table_8 : string
Sourceval __sedlex_table_9 : string
Sourceval __sedlex_table_10 : string
Sourceval __sedlex_table_11 : string
Sourceval __sedlex_table_12 : string
Sourceval __sedlex_table_13 : string
Sourceval __sedlex_table_14 : string
Sourceval __sedlex_table_15 : string
Sourceval __sedlex_table_17 : string
Sourceval __sedlex_table_18 : string
Sourceval __sedlex_table_19 : string
Sourceval __sedlex_table_21 : string
Sourceval __sedlex_table_24 : string
Sourceval __sedlex_table_25 : string
Sourceval __sedlex_table_27 : string
Sourceval __sedlex_table_28 : string
Sourceval __sedlex_table_30 : string
Sourceval __sedlex_table_31 : string
Sourceval __sedlex_table_32 : string
Sourceval __sedlex_table_33 : string
Sourceval __sedlex_table_35 : string
Sourceval __sedlex_table_36 : string
Sourceval __sedlex_table_37 : string
Sourceval __sedlex_table_38 : string
Sourceval __sedlex_table_39 : string
Sourceval __sedlex_table_40 : string
Sourceval __sedlex_table_42 : string
Sourceval __sedlex_table_43 : string
Sourceval __sedlex_table_44 : string
Sourceval __sedlex_table_45 : string
Sourceval __sedlex_table_46 : string
Sourceval __sedlex_table_47 : string
Sourceval __sedlex_table_48 : string
Sourceval __sedlex_table_50 : string
Sourceval __sedlex_table_51 : string
Sourceval __sedlex_table_52 : string
Sourceval __sedlex_table_53 : string
Sourceval __sedlex_table_54 : string
Sourceval __sedlex_table_55 : string
Sourceval __sedlex_table_56 : string
Sourceval __sedlex_table_57 : string
Sourceval __sedlex_table_58 : string
Sourceval __sedlex_table_60 : string
Sourceval __sedlex_table_62 : string
Sourceval __sedlex_table_63 : string
Sourceval __sedlex_table_64 : string
Sourceval __sedlex_table_65 : string
Sourceval __sedlex_table_66 : string
Sourceval __sedlex_table_67 : string
Sourceval __sedlex_table_68 : string
Sourceval __sedlex_table_34 : string
Sourceval __sedlex_table_59 : string
Sourceval __sedlex_table_16 : string
Sourceval __sedlex_table_41 : string
Sourceval __sedlex_table_23 : string
Sourceval __sedlex_table_29 : string
Sourceval __sedlex_table_61 : string
Sourceval __sedlex_partition_48 : int -> int
Sourceval __sedlex_partition_58 : int -> int
Sourceval __sedlex_partition_20 : int -> int
Sourceval __sedlex_partition_25 : int -> int
Sourceval __sedlex_partition_41 : int -> int
Sourceval __sedlex_partition_42 : int -> int
Sourceval __sedlex_partition_69 : int -> int
Sourceval __sedlex_partition_8 : int -> int
Sourceval __sedlex_partition_66 : int -> int
Sourceval __sedlex_partition_21 : int -> int
Sourceval __sedlex_partition_38 : int -> int
Sourceval __sedlex_partition_57 : int -> int
Sourceval __sedlex_partition_64 : int -> int
Sourceval __sedlex_partition_16 : int -> int
Sourceval __sedlex_partition_63 : int -> int
Sourceval __sedlex_partition_28 : int -> int
Sourceval __sedlex_partition_50 : int -> int
Sourceval __sedlex_partition_10 : int -> int
Sourceval __sedlex_partition_12 : int -> int
Sourceval __sedlex_partition_17 : int -> int
Sourceval __sedlex_partition_52 : int -> int
Sourceval __sedlex_partition_68 : int -> int
Sourceval __sedlex_partition_4 : int -> int
Sourceval __sedlex_partition_32 : int -> int
Sourceval __sedlex_partition_15 : int -> int
Sourceval __sedlex_partition_19 : int -> int
Sourceval __sedlex_partition_33 : int -> int
Sourceval __sedlex_partition_26 : int -> int
Sourceval __sedlex_partition_72 : int -> int
Sourceval __sedlex_partition_49 : int -> int
Sourceval __sedlex_partition_65 : int -> int
Sourceval __sedlex_partition_7 : int -> int
Sourceval __sedlex_partition_54 : int -> int
Sourceval __sedlex_partition_44 : int -> int
Sourceval __sedlex_partition_55 : int -> int
Sourceval __sedlex_partition_67 : int -> int
Sourceval __sedlex_partition_14 : int -> int
Sourceval __sedlex_partition_53 : int -> int
Sourceval __sedlex_partition_39 : int -> int
Sourceval __sedlex_partition_9 : int -> int
Sourceval __sedlex_partition_23 : int -> int
Sourceval __sedlex_partition_24 : int -> int
Sourceval __sedlex_partition_40 : int -> int
Sourceval __sedlex_partition_2 : int -> int
Sourceval __sedlex_partition_46 : int -> int
Sourceval __sedlex_partition_51 : int -> int
Sourceval __sedlex_partition_61 : int -> int
Sourceval __sedlex_partition_3 : int -> int
Sourceval __sedlex_partition_31 : int -> int
Sourceval __sedlex_partition_37 : int -> int
Sourceval __sedlex_partition_47 : int -> int
Sourceval __sedlex_partition_71 : int -> int
Sourceval __sedlex_partition_13 : int -> int
Sourceval __sedlex_partition_1 : int -> int
Sourceval __sedlex_partition_36 : int -> int
Sourceval __sedlex_partition_43 : int -> int
Sourceval __sedlex_partition_59 : int -> int
Sourceval __sedlex_partition_62 : int -> int
Sourceval __sedlex_partition_27 : int -> int
Sourceval __sedlex_partition_34 : int -> int
Sourceval __sedlex_partition_45 : int -> int
Sourceval __sedlex_partition_56 : int -> int
Sourceval __sedlex_partition_11 : int -> int
Sourceval __sedlex_partition_18 : int -> int
Sourceval __sedlex_partition_6 : int -> int
Sourceval __sedlex_partition_60 : int -> int
Sourceval __sedlex_partition_70 : int -> int
Sourceval __sedlex_partition_74 : int -> int
Sourceval __sedlex_partition_22 : int -> int
Sourceval __sedlex_partition_30 : int -> int
Sourceval __sedlex_partition_35 : int -> int
Sourceval __sedlex_partition_73 : int -> int
Sourceval __sedlex_partition_29 : int -> int
Sourceval __sedlex_partition_5 : int -> int

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

Sourceval remove_first : Sedlexing.lexbuf -> string
Sourceval remove_last : Sedlexing.lexbuf -> string
Sourceval remove_ends : Sedlexing.lexbuf -> string
Sourceexception SyntaxError of Common.Pos.strloc
Sourceval syntax_error : (Lexing.position * Lexing.position) -> string -> 'a
Sourceval fail : Sedlexing.lexbuf -> string -> 'a
Sourceval invalid_character : Sedlexing.lexbuf -> 'a
Sourcetype 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. | COERCE_RULE
  13. | COMMUTATIVE
  14. | COMPUTE
  15. | CONSTANT
  16. | DEBUG
  17. | END
  18. | FAIL
  19. | FLAG
  20. | GENERALIZE
  21. | HAVE
  22. | IN
  23. | INDUCTION
  24. | INDUCTIVE
  25. | INFIX
  26. | INJECTIVE
  27. | LET
  28. | NOTATION
  29. | OPAQUE
  30. | OPEN
  31. | POSTFIX
  32. | PREFIX
  33. | PRINT
  34. | PRIVATE
  35. | PROOFTERM
  36. | PROTECTED
  37. | PROVER
  38. | PROVER_TIMEOUT
  39. | QUANTIFIER
  40. | REFINE
  41. | REFLEXIVITY
  42. | REMOVE
  43. | REQUIRE
  44. | REWRITE
  45. | RULE
  46. | SEARCH
  47. | SEQUENTIAL
  48. | SIMPLIFY
  49. | SOLVE
  50. | SYMBOL
  51. | SYMMETRY
  52. | TRY
  53. | TYPE_QUERY
  54. | TYPE_TERM
  55. | UNIF_RULE
  56. | VERBOSE
  57. | WHY3
  58. | WITH
  59. | DEBUG_FLAGS of bool * string
  60. | NAT of string
  61. | FLOAT of string
  62. | SIDE of Pratter.associativity
  63. | STRINGLIT of string
  64. | SWITCH of bool
  65. | ARROW
  66. | ASSIGN
  67. | BACKQUOTE
  68. | COMMA
  69. | COLON
  70. | DOT
  71. | EQUIV
  72. | HOOK_ARROW
  73. | LAMBDA
  74. | L_CU_BRACKET
  75. | L_PAREN
  76. | L_SQ_BRACKET
  77. | PI
  78. | R_CU_BRACKET
  79. | R_PAREN
  80. | R_SQ_BRACKET
  81. | SEMICOLON
  82. | TURNSTILE
  83. | UNDERSCORE
  84. | VBAR
  85. | UID of string
  86. | UID_EXPL of string
  87. | UID_META of int
  88. | UID_PATT of string
  89. | QID of Common.Path.t
  90. | 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.

Sourceval is_regid : string -> bool
Sourceval 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?

Sourceval remove_useless_escape : string -> string

remove_useless_escape s replaces escaped regular identifiers by their unescape form.

Sourceval qid : bool -> string list -> Sedlexing.lexbuf -> token
Sourceval comment : (Sedlexing.lexbuf -> token) -> int -> Sedlexing.lexbuf -> token