Merge branch 'master' into fix/parsing

CONTRIBUTING.md

@@ -78,7 +78,7 @@ following files:
 - `editors/emacs/lambdapi-smie.el` (grammar and indentation)
 - `editors/vscode/lp.configuration.json` (comments configuration),
 - `editors/vscode/syntaxes/lp.tmLanguage.json` (syntax highlighting),
-- `tools/listings.tex`
+- `misc/lambdapi.tex`
 - `doc/Makefile.bnf`
 - the User Manual files in the `doc/` repository
 

doc/Makefile.bnf

@@ -39,6 +39,7 @@ lambdapi.bnf: Makefile.bnf ../src/parsing/lpParser.mly
 	-e 's/INFIX/"infix"/g' \
 	-e 's/INJECTIVE/"injective"/g' \
 	-e 's/LET/"let"/g' \
+        -e 's/NEG_NAT/"-"<nat>/g' \
 	-e 's/NAT/<nat>/g' \
 	-e 's/NOTATION/"notation"/g' \
 	-e 's/OPEN/"open"/g' \

doc/commands.rst

@@ -224,7 +224,7 @@ priority levels ``6`` and ``7`` respectively.
 The modifier ``infix``, ``infix right`` and ``infix left`` can be used
 to specify whether the defined symbol is non-associative, associative to
 the right, or associative to the left.
-Priority levels are non-negative floating point numbers, hence a
+Priority levels are floating point numbers, hence a
 priority can (almost) always be inserted between two different levels.
 
 As explained above, at this point, ``+`` is not a valid term anymore, as it was
@@ -251,8 +251,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``
 
-* Parsing of operators is performed with the `pratter`_ library.
-
 
 **quantifier** Allows to write ```f x, t`` instead of ``f (λ x, t)``:
 

doc/emacs.rst

@@ -38,13 +38,16 @@ keybindings, you can change them easily!
 Installation
 ------------
 
-The ``lambdapi-mode`` can be installed from `MELPA
-<https://melpa.org>`__ using any package manager
-(``package.el``, `straight
-<https://github.com/raxod502/straight.el>`__, …). Provided that Emacs
-is properly configured (see https://melpa.org/#/getting-started to
-configure Emacs to use MELPA), the mode can be installed with ``M-x
-package-install RET lambdapi-mode``.
+The ``lambdapi-mode`` is distributed through `MELPA <https://melpa.org>`__,
+so you can use any package manager for Emacs.
+
+Or, provided that MELPA is correctly
+`configured <https://melpa.org/#/getting-started>`__,
+use the following command inside Emacs::
+
+    M-x package-install RET lambdapi-mode RET
+
+where ``M-x`` is usually Alt+x and ``RET`` denotes the Return or Enter key.
 
 Usage
 -----

doc/lambdapi.bnf

@@ -176,12 +176,13 @@ QID ::= [UID "."]+ UID
 
 <equation> ::= <term> "≡" <term>
 
-<notation> ::= "infix" [<side>] <float_or_nat>
-             | "postfix" <float_or_nat>
-             | "prefix" <float_or_nat>
+<notation> ::= "infix" [<side>] <float_or_int>
+             | "postfix" <float_or_int>
+             | "prefix" <float_or_int>
              | "quantifier"
 
-<float_or_nat> ::= <float>
+<float_or_int> ::= <float>
+                 | "-"<nat>
                  | <nat>
 
 <maybe_generalize> ::= ["generalize"]

doc/options.rst

@@ -110,6 +110,8 @@ For the format ``stt_coq``, several other options are available:
 
 It tells Lambdapi which symbols of the input files are used for the encoding. Example: `encoding.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/encoding.lp>`__. The first argument ``a`` of the symbols corresponding to the builtins ``"eq"``, ``"all"`` and ``"ex"`` need not be declared as implicit.
 
+In symbol declarations or definitions, parameters with no type are assumed to be of type the term associated with the builtin ``"Set"``.
+
 * ``--no-implicits`` instructs Lambdapi that the symbols of the encoding have no implicit arguments.
 
 * ``--renaming <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations of the form

doc/queries.rst

@@ -49,7 +49,7 @@ functionalities, run the command ``lambdapi check --help``.
 --------
 
 Sets some flags ``on`` or ``off``, mainly for modifying the printing
-behavior. Only the flag ``"eta_equalify"`` changes the behavior of the
+behavior. Only the flag ``"eta_equality"`` changes the behavior of the
 rewrite engine by reducing η-redexes.
 
 ::
@@ -59,6 +59,7 @@ rewrite engine by reducing η-redexes.
    flag "print_contexts" on; // default is off
    flag "print_domains" on; // default is off
    flag "print_meta_types" on; // default is off
+   flag "print_meta_args" on; // default is off
 
 .. _print:
 

dune-project

@@ -52,7 +52,7 @@ the Why3 platform.")
  (depends
   (ocaml (>= 4.08.0))
   (menhir (>= 20200624))
-  (sedlex (>= 2.2))
+  (sedlex (>= 3.2))
   (alcotest :with-test)
   (dedukti (and :with-test (>= 2.7)))
   (bindlib (>= 5.0.1))

editors/emacs/.gitignore

@@ -1,3 +1,2 @@
 *.elc
-dist/
-.cask/
+*.tar

editors/emacs/Makefile

@@ -1,52 +1,49 @@
-VERSION = 1.0
-
-CASK    =
-EMACS   = emacs
-INSTALL = install
-
-INSTALL_DIR = $(shell opam config var share)/emacs/site-lisp
-CURDIR = $(shell pwd)
-
-SRC = $(wildcard *.el)
-BUILD_FILES =
-
-# If not using Cask, build only the site file
-ifndef CASK
-BUILD_FILES += lambdapi-site-file.elc
-endif
-
-.PHONY: build
-build: $(SRC)
-ifdef CASK
-	$(CASK) build
-else
-	$(MAKE) $(BUILD_FILES)
-endif
-
-.SUFFIXES = .elc .el
-.el.elc:
-	$(EMACS) --batch --eval "(add-to-list 'load-path \"$(CURDIR)\")" \
---eval '(byte-compile-file "$<")'
+.POSIX:
+
+VERSION = 1.1.0
+NAME = lambdapi-mode
+# The path to lambdapi built by dune
+LAMBDAPI = ../../_build/install/default/bin/lambdapi
+
+EMACS = emacs
+
+SRC =
+SRC += lambdapi-abbrev.el
+SRC += lambdapi-capf.el
+SRC += lambdapi-input.el
+SRC += lambdapi-layout.el
+SRC += lambdapi-mode.el
+SRC += lambdapi-mode-pkg.el
+SRC += lambdapi-proofs.el
+SRC += lambdapi-smie.el
+SRC += lambdapi-vars.el
+
+$(NAME)-$(VERSION).tar: $(SRC)
+	mkdir -p "$(NAME)-$(VERSION)"
+	cp *.el "$(NAME)-$(VERSION)"
+	tar -cf "$(NAME)-$(VERSION)".tar "$(NAME)-$(VERSION)"
 
 .PHONY: install
-install: $(SRC) lambdapi-site-file.elc
-	$(INSTALL) -m 644 -t $(INSTALL_DIR) $^
-	$(MAKE) clean
+install:
+	@echo "See https://lambdapi.readthedocs.io/en/latest/emacs.html \
+	for instructions on how to install the lambdapi mode for Emacs. \
+	If you know what you're doing, you can install the development version with" \
+	| fmt
+	@echo "$$ make dist"
+	@echo "and in emacs"
+	@echo "M-x package-install-file RET $(NAME)-$(VERSION).tar RET"
 
 .PHONY: dist
-dist:
-ifdef CASK
-	$(CASK) package
-endif
+dist: $(NAME)-$(VERSION).tar
 
-.PHONY: test
-tests: dist
-	./test.sh $(VERSION)
+.PHONY: check
+check: dist
+	# This rule depends on the layout of dune. It builds the lambdapi
+	# binary so that the "sandboxed" emacs can access it.
+	cd ../.. && $(MAKE) lambdapi
+	./test.sh "$(NAME)" "$(VERSION)" "$(LAMBDAPI)"
 
 .PHONY: clean
 clean:
-ifdef CASK
-	$(CASK) clean-elc
-else
-	find . -name '*.elc' -exec rm -f {} \;
-endif
+	rm -f "$(NAME)-$(VERSION)".tar
+	rm -rf "$(NAME)-$(VERSION)"

editors/emacs/lambdapi-mode-pkg.el

@@ -0,0 +1,5 @@
+(define-package "lambdapi-mode" "1.1.0"
+  "A major mode to edit Lambdapi files."
+  '((eglot "1.6")
+    (math-symbol-lists "1.2.1")
+    (highlight "20190710.1527")))

editors/emacs/lambdapi-mode.el

@@ -1,15 +1,15 @@
 ;;; lambdapi-mode.el --- A major mode for editing Lambdapi source code -*- lexical-binding: t; -*-
 
-;; Copyright (C) 2020 Deducteam
+;; Copyright (C) 2020-2024 Deducteam
 
 ;; Authors: Ashish Barnawal, Diego Riviero, Gabriel Hondet, Rodolphe Lepigre
 ;; Maintainer: Deducteam <[email protected]>
-;; Version: 1.0
+;; Version: 1.1.0
 ;; SPDX-License-Identifier: CECILL-2.1
 ;; Homepage: https://github.com/Deducteam/lambdapi
 ;; Keywords: languages
-;; Compatibility: GNU Emacs 26.1
-;; Package-Requires: ((emacs "26.1") (eglot "1.5") (math-symbol-lists "1.2.1") (highlight "20190710.1527"))
+;; Compatibility: GNU Emacs 28.1
+;; Package-Requires: ((emacs "28.1") (eglot "1.6") (math-symbol-lists "1.2.1") (highlight "20190710.1527"))
 
 ;;; Commentary:
 

editors/emacs/test.sh

@@ -1,20 +1,31 @@
 #!/bin/sh
-## Test the lambdapi-mode built from '*.el' files.
-## The script  downloads a  fresh and basic  configuration, creates  a temporary
-## directory and launches emacs in it. You  can create a new 'foo.lp' to try the
-## mode.
-##
-## Takes the version of the mode as first argument
+# Test the lambdapi-mode.
+# The script
+# - downloads a fresh and basic configuration,
+# - creates a temporary directory
+# - copies the lambdapi binary in the directory
+# - and launches emacs in it.
+# You  can create a new 'foo.lp' to try the mode.
+
+# Usage: tests.sh NAME VERSION LAMBDAPI
+
 set -eu
+NAME="$1"
+VERSION="$2"
+BIN="$3"
 tmp="$(mktemp -d)"
-cp "dist/lambdapi-mode-$1.tar" "${tmp}"
+make dist
+cp "${NAME}-${VERSION}.tar" "${tmp}"
+mkdir -p "${tmp}"/bin
+cp ${BIN} "${tmp}"/bin/lambdapi
 (cd "${tmp}" || exit 1
  curl https://sanemacs.com/sanemacs.el > sanemacs.el
  {
+     echo '(setq package-check-signature nil)';
      echo '(use-package eglot)';
      echo '(use-package math-symbol-lists)';
      echo '(use-package highlight)';
  } >> sanemacs.el
- emacs --quick -l sanemacs.el \
-     --eval "(package-install-file \"lambdapi-mode-$1.tar\")")
+PATH="bin:$PATH" emacs --quick -l sanemacs.el \
+     --eval "(package-install-file \"${NAME}-${VERSION}.tar\")")
 rm -rf "${tmp}"

editors/vscode/INSTALL.md

@@ -6,7 +6,7 @@ Installation from the sources
 - extract node:
 
 ```bash
-sudo apt-get install xz-utils # if you do not have xz already installed
+sudo apt-get install jq xz-utils
 tar xfa $node_file.tar.xz # creates $node_dir
 ```
 
@@ -35,7 +35,7 @@ If you intend to do this often, it is recomanded to add the two `export` command
 
 ```bash
 npm install -g @types/vscode
-npm install -g vsce # for creating VSCE packages only
+npm install -g @vscode/vsce # to create VSCE packages
 ```
 
 - compilation:

lambdapi.opam

@@ -50,7 +50,7 @@ depends: [
   "dune" {>= "3.7"}
   "ocaml" {>= "4.08.0"}
   "menhir" {>= "20200624"}
-  "sedlex" {>= "2.2"}
+  "sedlex" {>= "3.2"}
   "alcotest" {with-test}
   "dedukti" {with-test & >= "2.7"}
   "bindlib" {>= "6.0.0"}

src/core/dune

@@ -2,7 +2,7 @@
  (targets version.ml)
  (action
   (with-stdout-to version.ml
-    (run ocaml unix.cma %{dep:../../misc/gen_version.ml})))
+    (run ocaml -I +unix unix.cma %{dep:../../misc/gen_version.ml})))
  (mode fallback))
 
 (library

src/core/print.ml

@@ -36,6 +36,9 @@ let print_meta_types : bool ref =
 (** Flag for printing contexts in unification problems. *)
 let print_contexts : bool ref = Console.register_flag "print_contexts" false
 
+(** Flag for printing metavariable arguments. *)
+let print_meta_args : bool ref = Console.register_flag "print_meta_args" false
+
 let assoc : Pratter.associativity pp = fun ppf assoc ->
   match assoc with
   | Neither -> ()
@@ -249,7 +252,8 @@ and term : term pp = fun ppf t ->
     | Type        -> out ppf "TYPE"
     | Kind        -> out ppf "KIND"
     | Symb(s)     -> sym ppf s
-    | Meta(m,e)   -> out ppf "%a%a" meta m env e
+    | Meta(m,e)   ->
+        if !print_meta_args then out ppf "%a%a" meta m env e else meta ppf m
     | Plac(_)     -> out ppf "_"
     | Patt(_,n,e) -> out ppf "$%a%a" uid n env e
     | TEnv(t,e)   -> out ppf "$%a%a" term_env t env e