2.0.0

CHANGES:

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 ...