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.1.tbz
sha256=ba73f288e435130293408bd44732f1dfc5ec8a8db91c7453c9baf9c740095829
sha512=f88bb92fdb8aee8add60588673040fac012b2eab17c2a1d529c4b7c795cf0e1a9168122dc19889f04a31bda2bb2cf820237cbbe7e319121618aba3d134381756

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

Module Parsing.LpLexerSource

Sourceval __sedlex_table_20 : string
Sourceval __sedlex_table_25 : string
Sourceval __sedlex_table_48 : string
Sourceval __sedlex_table_18 : 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_15 : string
Sourceval __sedlex_table_16 : string
Sourceval __sedlex_table_17 : string
Sourceval __sedlex_table_19 : string
Sourceval __sedlex_table_22 : string
Sourceval __sedlex_table_23 : string
Sourceval __sedlex_table_24 : string
Sourceval __sedlex_table_26 : string
Sourceval __sedlex_table_27 : string
Sourceval __sedlex_table_29 : string
Sourceval __sedlex_table_30 : string
Sourceval __sedlex_table_31 : string
Sourceval __sedlex_table_32 : 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_39 : 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_47 : 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_56 : string
Sourceval __sedlex_table_58 : 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_66 : string
Sourceval __sedlex_table_33 : string
Sourceval __sedlex_table_57 : string
Sourceval __sedlex_table_14 : string
Sourceval __sedlex_table_40 : string
Sourceval __sedlex_table_21 : string
Sourceval __sedlex_table_28 : string
Sourceval __sedlex_table_59 : string
Sourceval __sedlex_partition_47 : int -> int
Sourceval __sedlex_partition_57 : 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_66 : int -> int
Sourceval __sedlex_partition_21 : int -> int
Sourceval __sedlex_partition_38 : int -> int
Sourceval __sedlex_partition_56 : int -> int
Sourceval __sedlex_partition_64 : 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_67 : 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_70 : int -> int
Sourceval __sedlex_partition_48 : int -> int
Sourceval __sedlex_partition_65 : int -> int
Sourceval __sedlex_partition_7 : int -> int
Sourceval __sedlex_partition_53 : int -> int
Sourceval __sedlex_partition_63 : int -> int
Sourceval __sedlex_partition_61 : 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_60 : 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_69 : int -> int
Sourceval __sedlex_partition_13 : int -> int
Sourceval __sedlex_partition_1 : int -> int
Sourceval __sedlex_partition_36 : int -> int
Sourceval __sedlex_partition_58 : 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_55 : int -> int
Sourceval __sedlex_partition_11 : int -> int
Sourceval __sedlex_partition_18 : int -> int
Sourceval __sedlex_partition_6 : int -> int
Sourceval __sedlex_partition_59 : int -> int
Sourceval __sedlex_partition_68 : int -> int
Sourceval __sedlex_partition_72 : int -> int
Sourceval __sedlex_partition_22 : int -> int
Sourceval __sedlex_partition_30 : int -> int
Sourceval __sedlex_partition_35 : int -> int
Sourceval __sedlex_partition_71 : 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. | POSTFIX
  31. | PREFIX
  32. | PRINT
  33. | PRIVATE
  34. | PROOFTERM
  35. | PROTECTED
  36. | PROVER
  37. | PROVER_TIMEOUT
  38. | QUANTIFIER
  39. | REFINE
  40. | REFLEXIVITY
  41. | REQUIRE
  42. | REWRITE
  43. | RULE
  44. | SEQUENTIAL
  45. | SIMPLIFY
  46. | SOLVE
  47. | SYMBOL
  48. | SYMMETRY
  49. | TYPE_QUERY
  50. | TYPE_TERM
  51. | UNIF_RULE
  52. | VERBOSE
  53. | WHY3
  54. | WITH
  55. | DEBUG_FLAGS of bool * string
  56. | NAT of string
  57. | FLOAT of float
  58. | SIDE of Pratter.associativity
  59. | STRINGLIT of string
  60. | SWITCH of bool
  61. | ARROW
  62. | ASSIGN
  63. | BACKQUOTE
  64. | COMMA
  65. | COLON
  66. | DOT
  67. | EQUIV
  68. | HOOK_ARROW
  69. | LAMBDA
  70. | L_CU_BRACKET
  71. | L_PAREN
  72. | L_SQ_BRACKET
  73. | PI
  74. | R_CU_BRACKET
  75. | R_PAREN
  76. | R_SQ_BRACKET
  77. | SEMICOLON
  78. | TURNSTILE
  79. | UNDERSCORE
  80. | VBAR
  81. | UID of string
  82. | UID_EXPL of string
  83. | UID_META of int
  84. | UID_PATT of string
  85. | QID of Common.Path.t
  86. | 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