Merge remote-tracking branch 'dk/master' into db

.github/workflows/main.yml

@@ -4,7 +4,7 @@ on:
   push:
   workflow_dispatch:
 jobs:
-  build_lambdapi:
+  lambdapi:
     strategy:
       fail-fast: false
       matrix:
@@ -13,13 +13,13 @@ jobs:
     steps:
       - name: checking out lambdapi repo ...
         uses: actions/checkout@v4
-      - name: recovering cached opam files ...
-        uses: actions/cache@v4
-        with:
-          path: ~/.opam
-          key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
+      # - name: recovering cached opam files ...
+      #   uses: actions/cache@v4
+      #   with:
+      #     path: ~/.opam
+      #     key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}
       - name: setting up opam ...
-        uses: avsm/setup-ocaml@v3
+        uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: ${{ matrix.ocaml-version }}
       - name: installing dependencies ...
@@ -34,7 +34,7 @@ jobs:
           eval $(opam env)
           #why3 config detect
           make tests
-  build_vscode_extension:
+  vscode:
     strategy:
       fail-fast: false
     runs-on: ubuntu-latest
@@ -58,3 +58,23 @@ jobs:
         with: 
           name: assets-for-download
           path: editors/vscode/extensionFolder
+  # lint-fmt:
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     - name: Checkout tree
+  #       uses: actions/checkout@v4
+  #     - name: Set-up OCaml
+  #       uses: ocaml/setup-ocaml@v3
+  #       with:
+  #         ocaml-compiler: 5
+  #     - uses: ocaml/setup-ocaml/lint-fmt@v3
+  # lint-opam:
+  #   runs-on: ubuntu-latest
+  #   steps:
+  #     - name: Checkout tree
+  #       uses: actions/checkout@v4
+  #     - name: Set-up OCaml
+  #       uses: ocaml/setup-ocaml@v3
+  #       with:
+  #         ocaml-compiler: 5
+  #     - uses: ocaml/setup-ocaml/lint-opam@v3

CHANGES.md

@@ -8,15 +8,17 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Added
 
 - Add tactic `set`.
+- Decimal notation for integers.
 
 ### Fixed
 
 - Induction tactic.
 
 ### Changed
 
-- Option '--erasing' renamed into '--mapping'.
 - The export option `--requiring` does not require as argument a file with extension `.v` anymore: the argument must be a module name.
+- Option '--erasing' renamed into '--mapping'.
+- Builtins necessary for the decimal notation.
 
 ## 2.5.1 (2024-07-22)
 

doc/README.md

@@ -21,9 +21,11 @@ The Lamdbapi user manual can also be generated from the sources and browsed loca
 browser.
 
 To generate the documentation, [Sphinx](https://www.sphinx-doc.org/)
-and `sphinx_rtd_theme` are required.  They can be installed using
-`pip` as follows:
-
+and `sphinx_rtd_theme` are required. They can be globally installed with:
+```bash
+sudo apt install python3-sphinx-rtd-theme
+```
+and locally with:
 ```bash
 sudo apt install python3-pip
 pip install -U sphinx sphinx_rtd_theme

doc/commands.rst

@@ -206,11 +206,10 @@ commands :ref:`notation` and :ref:`builtin`.
 
 The ``notation`` command allows to change the behaviour of the parser.
 
-When declared as notations, identifiers then must be used at correct places
-and as such cannot make valid terms on their own anymore.
-To reaccess the value of the identifier without the notation properties,
-wrap it in parentheses.
-
+When declared as notations, identifiers must be used at correct places
+and are not valid terms on their own anymore.  To reaccess the value
+of the identifier without the notation properties, wrap it in
+parentheses like in ``(+)`` if ``+`` is declared ``infix``.
 
 **infix** The following code defines infix symbols for addition
 and multiplication. Both are associative to the left, and they have
@@ -251,7 +250,6 @@ negation with some priority level.
 * The functional arrow has a lower binding power than any operator, therefore
   for any prefix operator ``-``, ``- A → A`` is always parsed ``(- A) → A``
 
-
 **quantifier** Allows to write ```f x, t`` instead of ``f (λ x, t)``:
 
 ::
@@ -262,28 +260,39 @@ negation with some priority level.
    type λ p, `∀ x, p; // quantifiers can be written as such
    type λ p, `f x, p; // works as well if f is any symbol
 
+**printing numbers in decimal notation** It is possible to print various number types in decimal notation by defining the following builtins:
+
+* Natural numbers in base 1 (Peano numbers):
+
+::
+   
+   builtin "nat_zero" ≔ ...; // : N
+   builtin "nat_succ" ≔ ...; // : N → N
+
+* Positive natural numbers in base 2:
+
+::
+   
+   builtin "pos_one" ≔ ...; // : P
+   builtin "pos_double" ≔ ...; // : P → P
+   builtin "pos_succ_double" ≔ ...; // : P → P
+
+* Integer numbers in base 2:
+
+::
+   
+   builtin "int_zero" ≔ ...; // : Z
+   builtin "int_positive" ≔ ...; // : P → Z
+   builtin "int_negative" ≔ ...; // : P → Z
+
 .. _builtin:
 
 ``builtin``
 ---------------
 
 The command ``builtin`` allows to map a “builtin“
 string to a user-defined symbol identifier. Those mappings are
-necessary for other commands or tactics. For instance, to use decimal
-numbers, one needs to map the builtins “0“ and “+1“ to some symbol
-identifiers for zero and the successor function (see hereafter); to
-use tactics on equality, one needs to define some specific builtins;
-etc.
-
-**notation for natural numbers** It is possible to use the standard
-decimal notation for natural numbers by defining the builtins ``"0"``
-and ``"+1"`` as follows:
-
-::
-
-   builtin "0"  ≔ zero; // : N
-   builtin "+1" ≔ succ; // : N → N
-   type 42;
+necessary for other commands, tactics or notations to work.
 
 .. _opaque:
 

doc/lambdapi.bnf

@@ -18,22 +18,22 @@ QID ::= [UID "."]+ UID
 
 <search_query_alone> ::= <search_query> EOF
 
-<command> ::= "opaque" <qid_or_int> ";"
+<command> ::= "opaque" <qid> ";"
             | "require" "open" <path>* ";"
             | "require" <path>* ";"
             | "require" <path> "as" <uid> ";"
             | "open" <path>* ";"
-            | <modifier>* "symbol" <uid_or_int> <param_list>* ":" <term>
-              [<proof>] ";"
-            | <modifier>* "symbol" <uid_or_int> <param_list>* [":" <term>]
-              "≔" <term_proof> ";"
+            | <modifier>* "symbol" <uid> <param_list>* ":" <term> [<proof>]
+              ";"
+            | <modifier>* "symbol" <uid> <param_list>* [":" <term>] "≔"
+              <term_proof> ";"
             | [<exposition>] <param_list>* "inductive" <inductive> ("with"
               <inductive>)* ";"
             | "rule" <rule> ("with" <rule>)* ";"
-            | "builtin" <stringlit> "≔" <qid_or_int> ";"
+            | "builtin" <stringlit> "≔" <qid> ";"
             | "coerce_rule" <rule> ";"
             | "unif_rule" <unif_rule> ";"
-            | "notation" <qid_or_int> <notation> ";"
+            | "notation" <qid> <notation> ";"
             | <query> ";"
 
 
@@ -45,8 +45,8 @@ QID ::= [UID "."]+ UID
           | "debug" ("+"|"-") <string>
           | "flag" <stringlit> <switch>
           | "prover" <stringlit>
-          | "prover_timeout" <nat>
-          | "verbose" <nat>
+          | "prover_timeout" "in"T
+          | "verbose" "in"T
           | "type" <term>
           | "search" <stringlit>
 
@@ -70,18 +70,11 @@ QID ::= [UID "."]+ UID
 
 <uid> ::= UID
 
-<uid_or_int> ::= <uid>
-               | <int>
-
-<qid_or_int> ::= <qid>
-               | <int>
-
 <param_list> ::= <param>
                | "(" <param>+ ":" <term> ")"
                | "[" <param>+ [":" <term>] "]"
 
 <param> ::= <uid>
-          | <nat>
           | "_"
 
 <term> ::= <bterm>
@@ -103,8 +96,7 @@ QID ::= [UID "."]+ UID
           | "$" UID [<env>]
           | "(" <term> ")"
           | "[" <term> "]"
-          | <nat>
-          | "-"<nat>
+          | "in"T
 
 <env> ::= "." "[" [<term> (";" <term>)*] "]"
 
@@ -152,7 +144,7 @@ QID ::= [UID "."]+ UID
            | "reflexivity"
            | "remove" <uid>+
            | "rewrite" [<side>] [<rw_patt_spec>] <term>
-           | "simplify" [<qid_or_int>]
+           | "simplify" [<qid>]
            | "solve"
            | "symmetry"
            | "try" <tactic>
@@ -169,7 +161,7 @@ QID ::= [UID "."]+ UID
 <inductive> ::= <uid> <param_list>* ":" <term> "≔" ["|"] [<constructor>
                 ("|" <constructor>)*]
 
-<constructor> ::= <uid_or_int> <param_list>* ":" <term>
+<constructor> ::= <uid> <param_list>* ":" <term>
 
 <rule> ::= <term> "↪" <term>
 
@@ -184,10 +176,7 @@ QID ::= [UID "."]+ UID
              | "quantifier"
 
 <float_or_int> ::= <float>
-                 | <int>
-
-<int> ::= "-"<nat>
-        | <nat>
+                 | "in"T
 
 <maybe_generalize> ::= ["generalize"]
 

doc/terms.rst

@@ -8,7 +8,8 @@ Identifiers
 An identifier can be:
 
 * a *regular* identifier: ``/`` or an arbitrary non-empty sequence of
-  UTF-8 codepoints not among ``\t\r\n :,;`(){}[]".@$|?/``
+  UTF-8 codepoints not among ``\t\r\n :,;`(){}[]".@$|?/`` that is not
+  an integer number
 
 * an *escaped* identifier: an arbitrary sequence of characters
   enclosed between ``{|`` and ``|}``
@@ -72,10 +73,24 @@ A user-defined term can be either:
   variable in a rule left-hand side, applied to all the variables of
   the context.
 
-* an integer between 0 and 2^30-1 if the :ref:`builtins <builtin>`
-  ``"0"`` and ``"+1"`` are defined
+* an integer if the appropriate builtins are defined (see below)
 
 * a term enclosed between square brackets ``[`` … ``]`` for explicitly
   giving the value of an argument declared as implicit
 
 Subterms can be parenthesized to avoid ambiguities.
+
+**decimal notation for integers** It is possible to use the standard
+decimal notation for integers by defining the following :ref:`builtins
+<builtin>`:
+
+::
+
+   builtin "0"  ≔ ...;  // : T
+   builtin "1"  ≔ ...;  // : T
+   ...
+   builtin "10" := ...; // : T
+   builtin "+" := ....; // : T → T → T
+   builtin "*" := ....; // : T → T → T
+   builtin "-" := ....; // : T → T // (optional)
+   type 42;

editors/emacs/lambdapi-input.el

@@ -30,14 +30,16 @@
  ("\\and" ?∧) ("&&" ?∧) ("/\\" ?∧)
  ("\\or" ?∨) ("||" ?∨) ("\\/" ?∨)
  ("=>" ?⇒)
+ ("<=>" ?⇔)
  ("!!" ?∀)
  ("??" ?∃)
 
  ;; Miscellaneous
 
  ("\\Box" ?□)
  ("::" ?⸬)
- ("<=" ?≤)
+ ("<=" ?≤) (">=" ?≥)
+ ("--" ?—)
 
  ;; Greek letters