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.2.0.tbz
sha256=920de48ec6c2c3223b6b93879bb65d07ea24aa27f7f7176b3de16e5e467b9939
sha512=135f132730825adeb084669222e68bc999de97b12378fae6abcd9f91ae13093eab29fa49c854adb28d064d52c9890c0f5c8ff9d47a9916f66fe5e0fba3479759

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

Module Parsing.LpLexerSource

Sourceval __sedlex_table_19 : string
Sourceval __sedlex_table_24 : string
Sourceval __sedlex_table_47 : string
Sourceval __sedlex_table_17 : 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_14 : string
Sourceval __sedlex_table_15 : string
Sourceval __sedlex_table_16 : string
Sourceval __sedlex_table_18 : string
Sourceval __sedlex_table_21 : string
Sourceval __sedlex_table_22 : string
Sourceval __sedlex_table_23 : string
Sourceval __sedlex_table_25 : string
Sourceval __sedlex_table_26 : string
Sourceval __sedlex_table_28 : string
Sourceval __sedlex_table_29 : string
Sourceval __sedlex_table_30 : string
Sourceval __sedlex_table_31 : string
Sourceval __sedlex_table_33 : string
Sourceval __sedlex_table_34 : string
Sourceval __sedlex_table_35 : string
Sourceval __sedlex_table_36 : string
Sourceval __sedlex_table_37 : string
Sourceval __sedlex_table_38 : string
Sourceval __sedlex_table_40 : string
Sourceval __sedlex_table_41 : 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_48 : string
Sourceval __sedlex_table_49 : 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_57 : string
Sourceval __sedlex_table_59 : string
Sourceval __sedlex_table_60 : string
Sourceval __sedlex_table_61 : string
Sourceval __sedlex_table_62 : string
Sourceval __sedlex_table_63 : string
Sourceval __sedlex_table_64 : string
Sourceval __sedlex_table_65 : string
Sourceval __sedlex_table_32 : string
Sourceval __sedlex_table_56 : string
Sourceval __sedlex_table_13 : string
Sourceval __sedlex_table_39 : string
Sourceval __sedlex_table_20 : string
Sourceval __sedlex_table_27 : string
Sourceval __sedlex_table_58 : string
Sourceval __sedlex_partition_47 : 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_8 : int -> int
Sourceval __sedlex_partition_65 : int -> int
Sourceval __sedlex_partition_21 : int -> int
Sourceval __sedlex_partition_38 : int -> int
Sourceval __sedlex_partition_56 : int -> int
Sourceval __sedlex_partition_63 : int -> int
Sourceval __sedlex_partition_16 : int -> int
Sourceval __sedlex_partition_28 : int -> int
Sourceval __sedlex_partition_49 : int -> int
Sourceval __sedlex_partition_10 : int -> int
Sourceval __sedlex_partition_12 : int -> int
Sourceval __sedlex_partition_17 : int -> int
Sourceval __sedlex_partition_51 : int -> int
Sourceval __sedlex_partition_66 : 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_43 : int -> int
Sourceval __sedlex_partition_33 : int -> int
Sourceval __sedlex_partition_26 : int -> int
Sourceval __sedlex_partition_69 : int -> int
Sourceval __sedlex_partition_48 : int -> int
Sourceval __sedlex_partition_64 : int -> int
Sourceval __sedlex_partition_7 : int -> int
Sourceval __sedlex_partition_53 : int -> int
Sourceval __sedlex_partition_62 : int -> int
Sourceval __sedlex_partition_60 : int -> int
Sourceval __sedlex_partition_54 : int -> int
Sourceval __sedlex_partition_14 : int -> int
Sourceval __sedlex_partition_52 : 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_44 : int -> int
Sourceval __sedlex_partition_50 : int -> int
Sourceval __sedlex_partition_59 : int -> int
Sourceval __sedlex_partition_3 : int -> int
Sourceval __sedlex_partition_31 : int -> int
Sourceval __sedlex_partition_37 : int -> int
Sourceval __sedlex_partition_46 : int -> int
Sourceval __sedlex_partition_68 : int -> int
Sourceval __sedlex_partition_13 : int -> int
Sourceval __sedlex_partition_1 : int -> int
Sourceval __sedlex_partition_36 : int -> int
Sourceval __sedlex_partition_57 : int -> int
Sourceval __sedlex_partition_61 : int -> int
Sourceval __sedlex_partition_27 : int -> int
Sourceval __sedlex_partition_34 : int -> int
Sourceval __sedlex_partition_45 : int -> int
Sourceval __sedlex_partition_55 : int -> int
Sourceval __sedlex_partition_11 : int -> int
Sourceval __sedlex_partition_18 : int -> int
Sourceval __sedlex_partition_6 : int -> int
Sourceval __sedlex_partition_58 : int -> int
Sourceval __sedlex_partition_67 : int -> int
Sourceval __sedlex_partition_71 : int -> int
Sourceval __sedlex_partition_22 : int -> int
Sourceval __sedlex_partition_30 : int -> int
Sourceval __sedlex_partition_35 : int -> int
Sourceval __sedlex_partition_70 : 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. | 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.

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