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-3.0.0.tbz
sha256=1066aed2618fd8e6a400c5147dbf55ea977ce8d3fe2e518ac6785c6775a1b8be
sha512=f7f499626aba92e070ae69581299a58525973fdbfd04a160ed3ac89209fb6cbe307b816d0b23e1b75bc83467ce8b4b0530c6f9816eaf58f7a07fde65a450106c

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

Module Parsing.LpLexerSource

Sourceval __sedlex_table_22 : string
Sourceval __sedlex_table_26 : string
Sourceval __sedlex_table_14 : string
Sourceval __sedlex_table_49 : string
Sourceval __sedlex_table_51 : 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_18 : string
Sourceval __sedlex_table_19 : string
Sourceval __sedlex_table_20 : 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_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_50 : 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_59 : string
Sourceval __sedlex_table_61 : 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_69 : string
Sourceval __sedlex_table_33 : string
Sourceval __sedlex_table_60 : string
Sourceval __sedlex_table_17 : string
Sourceval __sedlex_table_40 : string
Sourceval __sedlex_table_23 : string
Sourceval __sedlex_table_48 : string
Sourceval __sedlex_table_62 : string
Sourceval __sedlex_partition_50 : int -> int
Sourceval __sedlex_partition_60 : 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_70 : int -> int
Sourceval __sedlex_partition_8 : int -> int
Sourceval __sedlex_partition_67 : int -> int
Sourceval __sedlex_partition_21 : int -> int
Sourceval __sedlex_partition_38 : int -> int
Sourceval __sedlex_partition_59 : int -> int
Sourceval __sedlex_partition_65 : int -> int
Sourceval __sedlex_partition_16 : int -> int
Sourceval __sedlex_partition_56 : int -> int
Sourceval __sedlex_partition_14 : int -> int
Sourceval __sedlex_partition_28 : int -> int
Sourceval __sedlex_partition_52 : int -> int
Sourceval __sedlex_partition_10 : int -> int
Sourceval __sedlex_partition_12 : int -> int
Sourceval __sedlex_partition_15 : int -> int
Sourceval __sedlex_partition_54 : int -> int
Sourceval __sedlex_partition_69 : int -> int
Sourceval __sedlex_partition_32 : int -> int
Sourceval __sedlex_partition_18 : int -> int
Sourceval __sedlex_partition_19 : int -> int
Sourceval __sedlex_partition_33 : int -> int
Sourceval __sedlex_partition_26 : int -> int
Sourceval __sedlex_partition_73 : int -> int
Sourceval __sedlex_partition_51 : int -> int
Sourceval __sedlex_partition_66 : int -> int
Sourceval __sedlex_partition_68 : int -> int
Sourceval __sedlex_partition_64 : int -> int
Sourceval __sedlex_partition_45 : int -> int
Sourceval __sedlex_partition_57 : int -> int
Sourceval __sedlex_partition_17 : int -> int
Sourceval __sedlex_partition_55 : 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_47 : int -> int
Sourceval __sedlex_partition_53 : int -> int
Sourceval __sedlex_partition_62 : int -> int
Sourceval __sedlex_partition_3 : int -> int
Sourceval __sedlex_partition_31 : int -> int
Sourceval __sedlex_partition_37 : int -> int
Sourceval __sedlex_partition_48 : int -> int
Sourceval __sedlex_partition_72 : int -> int
Sourceval __sedlex_partition_7 : int -> int
Sourceval __sedlex_partition_13 : int -> int
Sourceval __sedlex_partition_1 : int -> int
Sourceval __sedlex_partition_4 : int -> int
Sourceval __sedlex_partition_36 : int -> int
Sourceval __sedlex_partition_44 : int -> int
Sourceval __sedlex_partition_61 : int -> int
Sourceval __sedlex_partition_63 : int -> int
Sourceval __sedlex_partition_27 : int -> int
Sourceval __sedlex_partition_34 : int -> int
Sourceval __sedlex_partition_46 : int -> int
Sourceval __sedlex_partition_58 : int -> int
Sourceval __sedlex_partition_11 : int -> int
Sourceval __sedlex_partition_43 : int -> int
Sourceval __sedlex_partition_6 : int -> int
Sourceval __sedlex_partition_49 : int -> int
Sourceval __sedlex_partition_71 : int -> int
Sourceval __sedlex_partition_75 : int -> int
Sourceval __sedlex_partition_22 : int -> int
Sourceval __sedlex_partition_30 : int -> int
Sourceval __sedlex_partition_35 : int -> int
Sourceval __sedlex_partition_74 : 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. | CHANGE
  13. | COERCE_RULE
  14. | COMMUTATIVE
  15. | COMPUTE
  16. | CONSTANT
  17. | DEBUG
  18. | END
  19. | EVAL
  20. | FAIL
  21. | FLAG
  22. | GENERALIZE
  23. | HAVE
  24. | IN
  25. | INDUCTION
  26. | INDUCTIVE
  27. | INFIX
  28. | INJECTIVE
  29. | LET
  30. | NOTATION
  31. | OPAQUE
  32. | OPEN
  33. | ORELSE
  34. | POSTFIX
  35. | PREFIX
  36. | PRINT
  37. | PRIVATE
  38. | PROOFTERM
  39. | PROTECTED
  40. | PROVER
  41. | PROVER_TIMEOUT
  42. | QUANTIFIER
  43. | REFINE
  44. | REFLEXIVITY
  45. | REMOVE
  46. | REPEAT
  47. | REQUIRE
  48. | REWRITE
  49. | RULE
  50. | SEARCH
  51. | SEQUENTIAL
  52. | SET
  53. | SIMPLIFY
  54. | SOLVE
  55. | SYMBOL
  56. | SYMMETRY
  57. | TRY
  58. | TYPE_QUERY
  59. | TYPE_TERM
  60. | UNIF_RULE
  61. | VERBOSE
  62. | WHY3
  63. | WITH
  64. | DEBUG_FLAGS of bool * string
  65. | INT of string
  66. | FLOAT of string
  67. | SIDE of Pratter.associativity
  68. | STRINGLIT of string
  69. | SWITCH of bool
  70. | ARROW
  71. | ASSIGN
  72. | BACKQUOTE
  73. | COMMA
  74. | COLON
  75. | DOT
  76. | EQUIV
  77. | HOOK_ARROW
  78. | LAMBDA
  79. | L_CU_BRACKET
  80. | L_PAREN
  81. | L_SQ_BRACKET
  82. | PI
  83. | R_CU_BRACKET
  84. | R_PAREN
  85. | R_SQ_BRACKET
  86. | SEMICOLON
  87. | TURNSTILE
  88. | UNDERSCORE
  89. | VBAR
  90. | UID of string
  91. | UID_EXPL of string
  92. | UID_META of int
  93. | UID_PATT of string
  94. | QID of Common.Path.t
  95. | 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