package lambdapi

CHANGES.md

All notable changes to this project will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.

2.5.0 (2024-02-25)

Added

• Add the opaque command to turn a defined symbol into a constant

• Add the tactic try that tries to apply a tactic to the focused goal. If the application of the tactic fails, it catches the error and leaves the goal unchanged.

Fixed

• Coq export: do not rename module names

• Sequential symbols: fix order of rules

2.4.1 (2023-11-22)

Added

• support for Pratter 3.0.0

• printing of unification and coercion rules

Improved

• unification

Fixed

• Coq export

• matita.sh script

2.4.0 (2023-07-28)

Added

• Several options for export -o stt_coq.

• Tactic remove.

• Option --no-sr-check to disable subject reduction checking.

• CLI command index to build ~/.LPSearch.db.

• Indexed terms can be normalized wrt rules with the option --rules (note that this new option --rules could be used to implement the equivalent of dkmeta later).

• CLI command search and LP command search to send queries to the index.

• Query language.

• CLI command websearch to run a webserver that can answer search queries.

• Option --port to specify the port to use.

Improved

• Output for export -o stt_coq.

Changed

• Private definitions are not kept in memory and in lpo files anymore.

• The record type Eval.config is extended with a new field allowing to specify which dtree to use for each symbol.

2.3.1 (2023-03-13)

Fixed

• Opaque definitions are not kept in memory and in lpo files anymore

• A few bug fixes.

Changed

• Why3 dependency updated to 1.6.

2.3.0 (2023-01-03)

Added

• Export to Coq.

• (API) the rewrite engine can match on the constant TYPE.

• Automatic coercion insertion mechanism. For example, the command coerce_rule coerce Int Float $x ↪ FloatOfInt $x; can be used to instruct Lambdapi to automatically coerce integers to floats using the function FloatOfInt.

Fixed

• Generation of metavariables through the rewriting engine.

• Application of pattern variables in rewrite rules RHS in the Dedukti export.

• Dedukti export: invalid Dedukti module name were not brace-quoted, for instance, #REQUIRE module-name. could be exported, while module-name is not recognised by Dedukti2. It is now exported as #REQUIRE {|module-name|}, and symbols are exported as {|module-name|}.foo.

• HRS and XTC exports.

Changed

• Do not propose installation of Emacs mode via opam anymore as it can easily be installed from Emacs.

2.2.1 (2022-07-04)

Added

• Propagate recompile flag to dependencies.

• Postfix operators with the notation <op> postfix <priority>;

Removed

• Logic directory since it is now available on the Lambdapi Opam repository.

• Option --recompile.

Changed

• Use short options in system commands to be POSIX compliant.

2.2.0 (2022-03-18)

Added

• Incremental local confluence checking for non higher-order and non AC rules.

• Add options -o hrs and -o xtc to the export command.

Changed

• whnf function takes a problem as argument and a list of tags that configure the rewriting. Tags may block beta reduction, block definition expansion or block rewriting.

• Do not print empty term environments .[].

• Allow users to use the pattern variables $0, $1, etc. and internally name pattern variables by their index.

• Fixed debug flag printing in Pretty.

• Compatibility with Cmdliner 1.1.0 and Bindlib 6.0.0.

Removed

• tree_walk is no longer in the API

2.1.0 (2022-01-17)

Added

• In Logic/, a library of logics.

• The command export to translate signatures to the lp or dk files formats.

• New release of the VSCode extension.

• A small tutorial in tests/OK/tutorial.lp.

• The why3 tactic handles universal and existential quantifiers through two new builtins ("ex" and "all"). Codewise, it requires a new translation from encoded types to Why3 types.

• Terms may be placeholders. Placeholders are holes in the concrete syntax. They are refined into metavariables. Placeholders cannot appear nonlinearly in terms. From A Bidirectional Refinement Algorithm..., p. 31,

Changed

• Moved the files tool/hrs.ml and tool/xtc.ml into the new export/ directory.

• Because placeholders are simple holes, the term _ → _ is scoped into a full dependent product Π x: M, N where N is a metavariable that depend on x (see file tests/OK/767.lp)

• Type checking is slower following #696 because of refinement (not only the type but also the term must be destructured and rebuilt), | | master | refiner | |---------|--------|---------| | holide | 7:0 | 11:33 | | iprover | 5:58 | 6:50 |

Removed

• The command beautify superseded by the new command export.

• Unused variable warning: whether a variable is used or not cannot be decided while scoping (following #696) since placeholders that do not depend on variables may be refined later into metavariables that may depend on them.

• Metavariables cannot be referenced by their name anymore, hence the syntax ?M.[x;y] is obsolete, but ?0.[x;y] isn't.

2.0.0 (2021-12-15)

Release of the VSCode extension on the Marketplace (2021-12-10)

• Add editors/vscode/CHANGES.md and editors/vscode/CONTRIBUTING.md.

• Update documentation and README.md files.

Structured proof scripts (2021-12-07)

A tactic replacing the current goal by n new goals must be followed by n proof scripts enclosed in curly brackets. For instance, instead of writing induction; /* case 0 */ t1; ..; tm; /* case s */ q1; ..; qn, we must now write induction {t1; ..; tm} {q1; ..; qn}.

Exception for tactics not really changing the current goal like "have": /* proof of u */ have h: t; /* proof of t */ t1; ..; tm; /* proof of u continued */ q1; ..; qn must now be written have h: t {t1; ..; tm}; q1; ..; qn.

Other modifications in the grammar:

• Curly brackets are reserved for proof script structuration.

• Implicit arguments must be declared using square brackets instead of curly brackets: we must write [a:Set] instead of {a:Set}.

• Term environments and rewrite patterns must be preceded by a dot: we must now write $f.[x] instead of $f[x].

• The focus command is removed since it breaks structuration.

Improve and simplify LP lexer (2021-12-07)

• allow nested comments (fix #710)

• replace everywhere %S by \"%s\"

• move checking compatibility with Bindlib of identifiers from lexer to scope

• move is_keyword from lexer to pretty

• move package.ml from common/ to parsing/

• change Config.map_dir field type to (Path.t * string) list, Library.add_mapping type to Path.t * string -> unit and Compile.compile argument lm type to Path.t * string

Update dkParser to be in sync with dkcheck (2021-11-30)

Add option --record-time (2021-11-30)

Improve evaluation and convertibility test (2021-06-02)

• fix _LLet by calling mk_LLet

• substitute arguments in TEnv's at construction time (mk_TEnv)

• improve eq_modulo to avoid calling whnf when possible

• use Eval.pure_eq_modulo in Infer and Unif (fix #693)

Improve logs (2021-06-01)

• add Base.out = Format.fprintf

• uniformize printing code using Base.out

• rename oc arguments into ppf

• complete Term.pp_term

• improve some functions in Debug.D

• improve logging messages in Infer by adding a level argument

Better handling of let's (2021-05-26)

• mk_LLet removes useless let's

• rename Eval.config into strat

• factorize whnf_beta and whnf

• fix handling of variable unfoldings in whnf_stk

• optimize context lookup by using a map

• gather problem, context, map and rewrite into a record data type

• abstract whnf in hnf, snf and eq_modulo

• fix typing of let's

• improve printing

Interface Improvements (2021-05-20)

• Error messages are shown in logs buffer

• Improvements in behaviour of Emacs interface

• New shortcuts C-c C-k and C-c C-r for killing and reconnecting to the LSP server

Record metavariable creation and instantiation during scoping, type inference and unification (2021-05-20)

• the record type problem gets a new field metas, and all its fields are now mutable

• many functions now take as argument a problem

• the functions infer_noexn, check_noexn and check_sort are moved to Query (they do not need to take a solver as argument anymore)

• in Unif, add_constr was defined twice; this is now fixed

• the modules Meta in Term and LibTerm are moved to the new file libMeta

• various mli files are created

• in Unif, initial is removed and instantiation is allowed to generate new constraints

Bugfixes in rewriting engine (2021-05-06)

• Add tests on product matching

• Fixed scoping of product in LHS

• Wildcard created during tree compilation are the most general ones, any free variable may appear.

• Updated documentation of decision trees

Factorize type rw_patt (2021-04-07)

The types Term.rw_patt and Syntax.p_rw_patt_aux are merged into a single polymorphic type Syntax.rw_patt.

API modification (2021-04-07)

Several functions are exposed,

• Parsing.Scope.rule_of_pre_rule: converts a pre rewriting rule into a rewriting rule,

• Handle.Command.handle: now processes proof data,

• Handle.Command.get_proof_data: is the old handle,

• Handle.Compile.compile_with: allows to provide a command handler to compile modules

Add commutative and associative-commutative symbols (2021-04-07)

• Add term.mli and turn the term type into a private type so that term constructors are not exported anymore (they are available for pattern-matching though). For constructing terms, one now needs to use the provided construction functions mk_Vari for Vari, mk_Appl for Appl, etc.

• Move some functions LibTerm to Term, in particular get_args, add_args and cmp_term.

• Rename the field sym_tree into sym_dtree.

• Redefine the type rhs as (term_env, term) Bindlib.mbinder instead of (term_env, term) Bindlib.mbinder * int so that the old rhs needs to be replaced by rhs * int in a few places.

Improvements in some tactics (2021-04-05)

• fix have

• improve the behavior of apply

• assume not needed before reflexivity anymore

• assume checks that identifiers are distinct

• solve: simplify goals afterwards

• libTerm: permute arguments of unbind_name, and add add_args_map and unbind2_name

• syntax: add check_notin and check_distinct

• split misc/listings.tex into misc/lambdapi.tex and misc/example.tex

Extend command inductive to strictly-positive inductive types (2021-04-02)

Renamings (2021-04-01)

• ./tools/ -> ./misc

• ./src/core/tree_types.ml -> ./src/core/tree_type.ml

Do not unescape identifiers anymore, and move scope.ml from Core to Parsing (2021-03-30)

• escaped regular identifiers are automatically unescaped in lexing

• unescaping is done in filenames only

• Escape.add_prefix and Escape.add_suffix allow to correctly extend potentially escaped identifiers

• move scope.ml from Core to Parsing

Forbid bound variable names ending with a positive integer with leading zeros since there are not compatible with Bindlib (2021-03-29)

Fix #341: remove spurious warnings on bound variables (2021-03-29)

• scope.ml:

  • the inner functions of scope are brought to the top-level

  • scope_term_with_params is introduced: it is similar to scope_term but does not check that top-level bound variables are used

  • _Meta_Type is moved to env.ml as fresh_meta_type

• command.ml:

  • use scope_term_with_params and check that parameters are indeed used

  • get_implicitness moved to syntax.ml as get_impl_term

  • fix implicit arguments computation in case of no type by introducing Syntax.get_impl_params_list

• in various places: use pp_var instead of Bindlib.name_of

• replace expo argument in scoping and handling by boolean telling if private symbols are allowed

• allow private symbols in queries

Introduce new_tvar = Bindlib.new_var mkfree (2021-03-26)

Add tactic generalize, and rename tactic simpl into simplify (2021-03-25)

Use Dune for opam integration (2021-03-25)

• Content of lambdapi.opam is moved to dune-project and the former is generated using dune build @install.

• Vim files are installed in opam prefix using dune.

• The emacs mode is declared as a sub-package.

Add tactic have (2021-03-24)

Compatibility with Why3 1.4.0

Add tactic simpl <id> for unfolding a specific symbol only (2021-03-22)

and slightly improve Ctxt.def_of

Bug fixes (2021-03-22)

• fix type inference in the case of an application (t u) where the type of t is not a product yet (uncomment code commented in #596)

• fix the order in which emacs prints hypotheses

• fix opam dependencies: add constraint why3 <= 1.3.3

Fix and improve inverse image computation (2021-03-16)

• fix and improve in inverse.ml the computation of the inverse image of a term wrt an injective function (no unification rule is needed anymore in common examples, fix #342)

• fix management of "initial" constraints in unification (initial is now a global variable updated whenever a new constraint is added)

• when applying a unification rule, add constraints on types too (fix #466)

• turn Infer.make_prod into Infer.set_to_prod

• add pp_constrs for printing lists of constraints

• make time printing optional

• improve visualization of debugging data using colors: . blue: top-level type inference/checking . magenta: new constraint . green: constraint to solve . yellow: data from signature or context . red: instantiations (and handled commands)

Add tactic admit (2021-03-12)

• rename command admit into admitted

• admitted: admit the initial goal instead of the remaining goals (when the proof is an opaque definition)

• move code on admit from command.ml to tactic.ml

• add tactic admit (fix #380) As a consequence, tactics can change the signature state now.

Improvements in type inference, unification and printing (2021-03-11)

• improve type inference and unification

• add flag "print_meta_args"

• print metavariables unescaped, add parentheses in domains

• replace (current_sign()).sign_path by current_path()

• improve logging: . debug +h now prints data on type inference/checking . provide time of type inference/checking and constraint solving . give more feedback when instantiation fails

Remove set keyword (2021-03-04)

Various bug fixes (2021-03-02)

• allow matching on abstraction/product type annotations (fix #573)

• Infer: do not check constraint duplication and return constraints in the order they have been added (fix #579)

• inductive type symbols are now declared as constant (fix #580)

• fix parsing and printing of unification rules

• Extra.files returns only the files that satisfy some user-defined condition

• tests/ok_ko.ml: test only .dk and .lp files

• Pretty: checking that identifiers are LP keywords is now optional (useful for debug)

Fix notation declarations (2021-02-19)

• set infix ... "<string>" := <qid> is replaced by set notation <qid> infix ...

• set prefix ... "<string>" := <qid> is replaced by set notation <qid> prefix ...

• set quantifier <qid> is replaced by set notation <qid> quantifier

• the flag print_meta_type is renamed into print_meta_types

• LibTerm.expl_args is renamed into remove_impl_args

Improve handling of ghost symbols and metavariable identifier (2021-02-18)

• Ghost paths and unification rule symbols managed in LpLexer now (no hard-coded strings anymore except for their definition)

• Allow users to type system-generated metavariable identifiers (integers)

• Fix printing of metavariable identifiers

• key_counter renamed into meta_counter

• Meta.name does not return a ?-prefixed string anymore

• code factorization and reorganization in query.ml

Improve navigation in Emacs/VSCode (2021-02-18)

• Electric mode for Emacs

• Buttons for Proof Navigation in Emacs

• Navigate by commands/tactics in Emacs and VScode

• Evaluated region shrinks on edit in Emacs and VScode

• Evaluated region changes colour after error in Emacs and VScode

• LSP server sends logs only from last command/tactic

• Few minor corrections in LSP server

• Improve VSCode indentation

Add tactic induction (2021-02-17)

• env.ml: add functions for generating fresh metavariable terms (factorizes some code in scope.ml and tactics.ml)

• add fields in type Sign.inductive renamed into ind_data

• functions from rewrite.ml now take a goal_typ as argument

• code factorization in tactic.ml

• remove type aliases p_type and p_patt

• rename P_Impl into P_Arro, and P_tac_intro into P_tac_assume

• variable renamings in sig_state

File renamings and splitting and better handling of escaped identifier (2021-02-12)

• File renamings and splittings:

  • lpLexer -> escape, lpLexer

  • console -> base, extra, debug, error, console

  • module -> filename, path, library

  • cliconf -> config

  • install_cmd -> install

  • init_cmd -> init

• Improve handling of escaped identifiers in escape.ml and fix printing

• Improve tests/ok_ko.ml to allow sub-directories in tests/OK/ or tests/KO/

File renamings and source code segmentation (2021-02-08)

• File renamings:

  • terms -> term

  • basics -> libTerm

  • tactics -> tactic

  • queries -> query

  • stubs -> realpath

  • files -> module

  • handle -> command

• Core library divided into the following sub-libraries:

  • Common that contains shared basic files (pos, console, module and package)

  • Parsing that contains everything related to parsing (syntax, pretty, lexers and parser)

  • Handle that uses Core to type check commands and modules (contains query, tactic, command, compile, inductive, rewrite, proof and why3_tactic)

  • Tool that provides miscellaneous tools that use Core (external, hrs, xtc, tree_graphviz, sr)

Add parameters to inductive definitions (2021-02-02)

Parser (2021-01-30)

Replace Earley by Menhir, Pratter and Sedlex

Syntax modifications:

• Add multi-lines comments /* ... */.

• Commands and tactics must now be ended by a semi-colon ;.

• The syntax λx y z: nat, ... with multiple variables is not authorised anymore, but λ(x y z: nat), ... is, as well as λ x : N, t with a single variable.

• In unification rules, the right hand-side must now be enclosed between square brackets, so

  set unif_rule $x + $y ≡ 0 ↪ $x ≡ 0; $y ≡ 0
  

  becomes

  set unif_rule $x + $y ≡ 0 ↪ [ $x ≡ 0; $y ≡ 0 ];
  

• set declared has been removed.

• Any (depending on accepted codepoints) UTF8 identifier is by default valid. Warning: string λx is now a valid identifier. Hence, expression λx, t isn't valid, but λ x, t is.

• Declared quantifiers now need a backquote to be applied. The syntax `f x, t represents f (λ x, t) (and a fortiori f {T} (λ x, t)).

• assert always takes a turnstile (or vdash) to specify a (even empty) context, so the syntax is assert ⊢ t: A;

• The minus sign - in the rewrite tactic has been replaced by the keyword left.

Code modifications:

• Parsing and handling are interleaved (except in the LSP server): the parser returns a stream of parsed commands. Requesting an item of the stream parses one command in the file.

• The type pp_hint is renamed to notation and moved to sign.ml.

• Notations (that is, ex-pp_hint) are kept in a SymMap, which allowed to simplify some code in sig_state.ml and sign.ml.

• Positions are not lazy anymore, because Sedlex doesn't use lazy positions.

• p_terms do not have P_BinO and P_UnaO constructors anymore.

Unification goals (2020-12-15)

changes in the syntax:

• definition -> symbol

• theorem -> opaque symbol

• proof -> begin

• qed -> end

Mutually defined inductive types (2020-12-09)

Inductive types (2020-09-29)

Documentation in Sphinx (2020-07-31)

Goals display in Emacs (2020-07-06)

Sequential symbol (2020-07-06)

• Added sequential keyword for symbol declarations

• Removed --keep-rule-order option

Change semantics of environments (2020-06-10)

• $F is shorthand for $F[]

• Empty environment mandatory under binders

Add tactic fail (2020-05-26)

Matching on products (2020-05-18)

Allow users to match on product Πx: t, u and on the domain of binders.

Quantifier parsing and pretty-printing (2020-05-08)

• Allow users to declare a symbol [f] as quantifier. Then, [f x,t] stands for [f(λx,t)].

Unification rules (2020-04-29)

Introduction of unification rules, taken from http://www.cs.unibo.it/~asperti/PAPERS/tphol09.pdf. A unification rule can be set with

set unif_rule t ≡ u ↪ v ≡ w, x ≡ y

Pretty-printing (2020-04-25)

• Pretty-printing hints managed in signature state now.

Syntax change (2020-04-16)

• → is replaced by ↪ in rewriting rules,

• & is replaced by $ for pattern variables in rewriting rules,

• the syntax rule ... and ... becomes rule ... with ...,

• ⇒ is replaced by → for implication, and

• ∀ is replaced by Π for the dependent product type

Let bindings (2020-03-31)

Adding let-bindings to the terms structure.

• Contexts can now contain term definitions.

• Unification is carried out with a context.

• Reduction functions (whnf, hnf, snf &c.) are called with a context.

• Type annotation for let in the concrete syntax.

Prepare for modern versions of OCaml (2020-03-26)

• Use Stdlib instead of Pervasives (enforced by sanity checks).

• Rely on stdlib-shims to provide Stdlib on older version of OCaml.

File management and module mapping (2020-03-20)

• New module system.

• Revised command line arguments parsing and introduce subcommands.

• LSP server is now a Lambdapi subcommand: run with lambdapi lsp.

• New --no-warning option (fixes #296).

Trees simplification (2019-12-05)

Simplification of the decision tree structure

• trees do not depend on term variables;

• tree constructor type depends on generated at compile-time branch-wise unique integral identifiers;

• graph output is more consistent: variables are the same in the nodes and the leaves.

Protected symbols (2019-11-14)

Introducing protected and private symbols.

Calling provers with Why3 (2019-10-29)

Introducing the why3 tactic to call external provers.

Eta equality as a flag (2019-10-21)

Rewriting using decision trees (2019-09-17)

1.0.0 (2018-11-28)

First major release of Lambdapi. It introduces:

• a new syntax for developing proofs in the system,

• basic support for infix operators,

• call to external confluence checker with the same API as Dedukti,

• more things.

• Consolidate the LSP OPAM package into the main one (@ejgallego)

0.1.0 (2018-09-19)

First release of Lambdapi.