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

.github/dependabot.yml

@@ -0,0 +1,7 @@
+version: 2
+
+updates:
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: weekly

.github/workflows/main.yml

@@ -12,9 +12,9 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: checking out lambdapi repo ...
-        uses: actions/checkout@v2
+        uses: actions/checkout@v4
       - name: recovering cached opam files ...
-        uses: actions/cache@v2
+        uses: actions/cache@v4
         with:
           path: ~/.opam
           key: ${{ runner.os }}-ocaml-${{ matrix.ocaml-version }}

CHANGES.md

@@ -5,7 +5,16 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 ## [Unreleased]
 
-- Add the command `opaque` that opacifies a symbol already defined.
+### 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)
 

CONTRIBUTING.md

@@ -79,10 +79,11 @@ following files:
 - `editors/vscode/lp.configuration.json` (comments configuration),
 - `editors/vscode/syntaxes/lp.tmLanguage.json` (syntax highlighting),
 - `tools/listings.tex`
-- `doc/Makefile`
+- `doc/Makefile.bnf`
 - the User Manual files in the `doc/` repository
 
-and do `make doc` for generating BNF grammars.
+and do `make bnf` to generate the BNF grammar,
+and `make doc` to generate the Sphynx documentation.
 
 **Note:** the `lambdapi.opam` file is generated by dune using the `dune-project`
 file, it _should not be edited manually_. It is still versioned because opam

README.md

@@ -91,12 +91,14 @@ You can get the sources using `git` as follows:
 git clone https://github.com/Deducteam/lambdapi.git
 ```
 
-Dependencies are described in `lambdapi.opam`. The command `why3 config detect`
-must be run for Why3 to know the available provers.
+Dependencies are described in `lambdapi.opam`. The command `why3
+config detect` must be run for Why3 to know the available provers for
+the `why3` tactic.
 
 Using Opam, a suitable OCaml environment can be setup as follows:
 ```bash
-opam install dune bindlib timed sedlex menhir pratter yojson cmdliner why3 alcotest alt-ergo odoc
+cd lambdapi
+opam install .
 why3 config detect
 ```
 

doc/Makefile.bnf

@@ -68,6 +68,7 @@ lambdapi.bnf: Makefile.bnf ../src/parsing/lpParser.mly
         -e 's/STRINGLIT/<stringlit>/g' \
 	-e 's/SYMBOL/"symbol"/g' \
 	-e 's/SYMMETRY/"symmetry"/g' \
+	-e 's/TRY/"try"/g' \
 	-e 's/TYPE_QUERY/"type"/g' \
 	-e 's/TYPE_TERM/"TYPE"/g' \
 	-e 's/VERBOSE/"verbose"/g' \

doc/lambdapi.bnf

@@ -153,6 +153,7 @@ QID ::= [UID "."]+ UID
            | "simplify" [<qid_or_nat>]
            | "solve"
            | "symmetry"
+           | "try" <tactic>
            | "why3" [<stringlit>]
 
 <rw_patt> ::= <term>

doc/tactics.rst

@@ -156,6 +156,14 @@ focused goal.
 
 Simplify unification goals as much as possible.
 
+.. _try:
+
+``try``
+---------
+
+If ``T`` is a tactic, then ``try T`` is a tactic that applies ``T`` to the focused goal.
+If the application of ``T`` fails in the focused goal, it catches the error and leaves the goal unchanged.
+
 .. _why3:
 
 ``why3``

editors/emacs/lambdapi-smie.el

@@ -200,6 +200,7 @@ The default lexer is used because the syntax is primarily made of sexps."
     (`(:before . "simplify") `(column . ,lambdapi-indent-basic))
     (`(:before . "solve") `(column . ,lambdapi-indent-basic))
     (`(:before . "symmetry") `(column . ,lambdapi-indent-basic))
+    (`(:before . "try") `(column . ,lambdapi-indent-basic))
     (`(:before . "why3") `(column . ,lambdapi-indent-basic))
 
     (`(:before . ,(or "abort" "admitted" "end")) '(column . 0))

editors/emacs/lambdapi-vars.el

@@ -18,6 +18,7 @@
     "simplify"
     "solve"
     "symmetry"
+    "try"
     "why3")
   "Proof tactics.")
 

editors/vim/syntax/lambdapi.vim

@@ -86,6 +86,7 @@ syntax keyword KeywordOK contained simplify
 syntax keyword KeywordOK contained solve
 syntax keyword KeywordOK contained symbol
 syntax keyword KeywordOK contained symmetry
+syntax keyword KeywordOK contained try
 syntax keyword KeywordOK contained type
 syntax keyword KeywordOK contained TYPE
 syntax keyword KeywordOK contained unif_rule
@@ -152,6 +153,7 @@ syntax keyword KeywordKO contained simplify
 syntax keyword KeywordKO contained solve
 syntax keyword KeywordKO contained symbol
 syntax keyword KeywordKO contained symmetry
+syntax keyword KeywordKO contained try
 syntax keyword KeywordKO contained type
 syntax keyword KeywordKO contained TYPE
 syntax keyword KeywordKO contained unif_rule

editors/vscode/syntaxes/lp.tmLanguage.json

@@ -25,7 +25,7 @@
   ],
   "repository": {
     "commands": {
-      "match": "\\b(abort|admit|admitted|apply|as|assert|assertnot|associative|assume|begin|builtin|coerce_rule|commutative|compute|constant|debug|end|fail|flag|focus|generalize|have|in|induction|inductive|infix|injective|left|let|notation|off|on|open|opaque|postfix|prefix|print|private|proofterm|protected|prover|prover_timeout|quantifier|refine|reflexivity|remove|require|rewrite|rule|search|sequential|simplify|symbol|symmetry|type|TYPE|unif_rule|why3|with)\\b",
+      "match": "\\b(abort|admit|admitted|apply|as|assert|assertnot|associative|assume|begin|builtin|coerce_rule|commutative|compute|constant|debug|end|fail|flag|focus|generalize|have|in|induction|inductive|infix|injective|left|let|notation|off|on|open|opaque|postfix|prefix|print|private|proofterm|protected|prover|prover_timeout|quantifier|refine|reflexivity|remove|require|rewrite|rule|search|sequential|simplify|symbol|symmetry|try|type|TYPE|unif_rule|why3|with)\\b",
       "name": "keyword.control.lp"
     },
     "comments": {
@@ -44,7 +44,7 @@
     },
 
     "tactics": {
-      "match": "\\b(apply|assume|fail|focus|generalize|have|induction|refine|reflexivity|remove|rewrite|simplify|solve|symmetry|why3)\\b",
+      "match": "\\b(apply|assume|fail|focus|generalize|have|induction|refine|reflexivity|remove|rewrite|simplify|solve|symmetry|try|why3)\\b",
       "name": "keyword.control.tactics.lp"
     },
 

src/core/inverse.ml

@@ -7,8 +7,8 @@ open Print
 open Lplib
 
 (** Logging function for unification. *)
-let log_inv = Logger.make 'v' "invr" "inverse"
-let log_inv = log_inv.pp
+let log = Logger.make 'v' "invr" "inverse"
+let log = log.pp
 
 (** [cache f s] is equivalent to [f s] but [f s] is computed only once unless
    the rules of [s] are changed. *)
@@ -23,10 +23,10 @@ let cache : (sym -> 'a) -> (sym -> 'a) = fun f ->
 (** [const_graph s] returns the list of pairs [(s0,s1)] such that [s]
    has a rule of the form [s (s0 ...) ↪ s1 ...]. *)
 let const_graph : sym -> (sym * sym) list = fun s ->
-  if Logger.log_enabled () then log_inv "check rules of %a" sym s;
+  if Logger.log_enabled () then log "check rules of %a" sym s;
   let add s0 s1 l =
     if Logger.log_enabled () then
-      log_inv (Color.yel "%a %a ↪ %a") sym s sym s0 sym s1;
+      log (Color.yel "%a %a ↪ %a") sym s sym s0 sym s1;
     (s0,s1)::l
   in
   let f l rule =
@@ -59,12 +59,12 @@ let inverse_const : sym -> sym -> sym = fun s s' ->
    a rule of the form [s (s0 _ _) ↪ Π x:s1 _, s2 r] with [b=true] iff [x]
    occurs in [r]. *)
 let prod_graph : sym -> (sym * sym * sym * bool) list = fun s ->
-  if Logger.log_enabled () then log_inv "check rules of %a" sym s;
+  if Logger.log_enabled () then log "check rules of %a" sym s;
   let add (s0,s1,s2,b) l =
     if Logger.log_enabled () then
-      if b then log_inv (Color.yel "%a (%a _ _) ↪ Π x:%a _, %a _[x]")
+      if b then log (Color.yel "%a (%a _ _) ↪ Π x:%a _, %a _[x]")
                   sym s sym s0 sym s1 sym s2
-      else log_inv (Color.yel "%a (%a _ _) ↪ %a _ → %a _")
+      else log (Color.yel "%a (%a _ _) ↪ %a _ → %a _")
              sym s sym s0 sym s1 sym s2;
     (s0,s1,s2,b)::l
   in
@@ -115,7 +115,7 @@ let inverse_prod : sym -> sym -> sym * sym * sym * bool = fun s s' ->
 (** [inverse s v] tries to compute a term [u] such that [s(u)] reduces to [v].
 @raise [Not_found] otherwise. *)
 let rec inverse : sym -> term -> term = fun s v ->
-  if Logger.log_enabled () then log_inv "compute %a⁻¹(%a)" sym s term v;
+  if Logger.log_enabled () then log "compute %a⁻¹(%a)" sym s term v;
   match get_args v with
   | Symb s', [t] when s' == s -> t
   | Symb s', ts -> add_args (mk_Symb (inverse_const s s')) ts
@@ -137,5 +137,5 @@ let rec inverse : sym -> term -> term = fun s v ->
 let inverse : sym -> term -> term = fun s v ->
   let t = inverse s v in let v' = mk_Appl(mk_Symb s,t) in
   if Eval.eq_modulo [] v' v then t
-  else (if Logger.log_enabled() then log_inv "%a ≢ %a@" term v' term v;
+  else (if Logger.log_enabled() then log "%a ≢ %a@" term v' term v;
         raise Not_found)

src/core/libMeta.ml

@@ -3,6 +3,11 @@
 open Lplib
 open Term
 open Timed
+open Common
+
+(** Logging function for unification. *)
+let log = Logger.make 'a' "meta" "metavariables"
+let log = log.pp
 
 let meta_counter : int Stdlib.ref = Stdlib.ref (-1)
 
@@ -11,12 +16,13 @@ let reset_meta_counter () = Stdlib.(meta_counter := -1)
 
 (** [fresh p ?name a n] creates a fresh metavariable of type [a] and arity [n]
    with the optional name [name], and adds it to [p]. *)
-let fresh : problem -> term -> int -> meta =
-  fun p a n ->
+let fresh : problem -> term -> int -> meta = fun p a n ->
   let m = {meta_key = Stdlib.(incr meta_counter; !meta_counter);
-           meta_type = ref a; meta_arity = n;
-           meta_value = ref None } in
-  p := {!p with metas = MetaSet.add m !p.metas}; m
+           meta_type = ref a; meta_arity = n; meta_value = ref None } in
+  if Logger.log_enabled() then log "fresh ?%d" m.meta_key;
+  p := {!p with metas = MetaSet.add m !p.metas};
+  if Logger.log_enabled() then log "%a" Print.problem p;
+  m
 
 (** [set p m v] sets the metavariable [m] of [p] to [v]. WARNING: No specific
    check is performed, so this function may lead to cyclic terms. To use with
@@ -27,8 +33,7 @@ let set : problem -> meta -> mbinder -> unit = fun p m v ->
 
 (** [make p ctx a] creates a fresh metavariable term of type [a] in the
    context [ctx], and adds it to [p]. *)
-let make : problem -> ctxt -> term -> term =
-  fun p ctx a ->
+let make : problem -> ctxt -> term -> term = fun p ctx a ->
   let a, k = Ctxt.to_prod ctx a in
   let m = fresh p a k in
   let get_var (x,_,d) = if d = None then Some (mk_Vari x) else None in

src/core/tree.ml

@@ -240,7 +240,9 @@ module CM = struct
   (** Type of clause matrices. *)
   type t =
     { clauses   : clause list
-    (** The rules. *)
+    (** The rewrite rules. The order is significant when the {!Sequen}
+        strategy is used: the rewrite rules are ordered by decreasing
+        priority. *)
     ; slot      : int
     (** Index of next slot to use in [vars] array to store variables. *)
     ; positions : arg list

src/core/unif.ml

@@ -8,8 +8,8 @@ open LibTerm
 open Print
 
 (** Logging function for unification. *)
-let logger = Logger.make 'u' "unif" "unification"
-let log = logger.pp
+let log = Logger.make 'u' "unif" "unification"
+let log = log.pp
 
 (** Given a meta [m] of type [Πx1:a1,..,Πxn:an,b], [set_to_prod p m] sets [m]
    to a product term of the form [Πy:m1[x1;..;xn],m2[x1;..;xn;y]] with [m1]
@@ -31,8 +31,7 @@ let set_to_prod : problem -> meta -> unit = fun p m ->
   let b = bind_var y (mk_Meta (m2, Array.append xs [|mk_Vari y|])) in
   (* result *)
   let r = mk_Prod (a, b) in
-  if Logger.log_enabled () then
-    log (red "%a ≔ %a") meta m term r;
+  if Logger.log_enabled () then log (red "%a ≔ %a") meta m term r;
   LibMeta.set p m (bind_mvar vs r)
 
 (** [type_app c a ts] returns [Some u] where [u] is a type of [add_args x ts]
@@ -118,7 +117,7 @@ let instantiate : problem -> ctxt -> meta -> term array -> term -> bool =
   if Logger.log_enabled () then log "try instantiate";
   match instantiation c m ts u with
   | Some b when is_closed_mbinder b ->
-      let do_instantiate() =
+      let do_instantiate p =
         if Logger.log_enabled () then log (red "%a ≔ %a") meta m term u;
         LibMeta.set p m b;
         p := {!p with recompute = true}; true
@@ -131,13 +130,10 @@ let instantiate : problem -> ctxt -> meta -> term array -> term -> bool =
             | Some a -> a
             | None -> assert false
           in
-          let r = (*Logger.set_debug_in false 'i'*)
-            (Infer.check_noexn p c u) typ_mts
-          in
-          if r <> None then do_instantiate()
+          if Infer.check_noexn p c u typ_mts <> None then do_instantiate p
           else (if Logger.log_enabled () then log "typing failed"; false)
         end
-      else do_instantiate()
+      else do_instantiate p
   | i ->
       if Logger.log_enabled () then
         begin
@@ -280,8 +276,7 @@ let imitate_lam : problem -> ctxt -> meta -> unit = fun p c m ->
     let u1 = mk_Meta (m1, Env.to_terms env') in
     let xu1 = mk_Abst (a, bind_var x u1) in
     let v = bind_mvar (Env.vars env) xu1 in
-    if Logger.log_enabled () then
-      log (red "%a ≔ %a") meta m term xu1;
+    if Logger.log_enabled () then log (red "%a ≔ %a") meta m term xu1;
     LibMeta.set p m v
 
 (** [inverse_opt s ts v] returns [Some(t, inverse s v)] if [ts=[t]], [s] is
@@ -342,15 +337,15 @@ let sym_sym_whnf :
 Otherwise, [p.to_solve] is empty but [p.unsolved] may still contain
 constraints that could not be simplified. *)
 let solve : problem -> unit = fun p ->
-  while !p.to_solve <> [] || (!p.recompute && !p.unsolved <> []) do
+  while !p.to_solve <> [] || (!p.recompute && !p.unsolved <> []) do begin
+  log "solve %a" problem p;
   match !p.to_solve with
   | [] ->
       if Logger.log_enabled () then log "recompute";
       p := {!p with to_solve = !p.unsolved; unsolved = []; recompute = false}
   | (c,t1,t2)::to_solve ->
   (*if Logger.log_enabled () then
     log "%d constraints" (1 + List.length to_solve);*)
-  if Logger.log_enabled() then log "solve problem %a" problem p;
 
   (* We remove the first constraint from [p] for not looping. *)
   p := {!p with to_solve};
@@ -484,7 +479,7 @@ let solve : problem -> unit = fun p ->
   | _, Symb s -> inverse p c t2 s ts2 t1
 
   | _ -> add_to_unsolved p c t1 t2
-  done
+  end done
 
 (** [solve_noexn ~type_check p] tries to simplify the constraints of [p]. It
    returns [false] if it finds a constraint that cannot be

src/export/coq.ml

@@ -97,7 +97,9 @@ let set_erasing : string -> unit = fun f ->
         let id = snd lp_qid.elt in
         if Logger.log_enabled() then log "erase %s" id;
         erase := StrSet.add id !erase;
-        map_erased_qid_coq := QidMap.add lp_qid.elt coq_id !map_erased_qid_coq
+        map_erased_qid_coq := QidMap.add lp_qid.elt coq_id !map_erased_qid_coq;
+        if fst lp_qid.elt = [] && id <> coq_id then
+          rmap := StrMap.add id coq_id !rmap
     | {pos;_} -> fatal pos "Invalid command."
   in
   Stream.iter consume (Parser.parse_file f)
@@ -139,7 +141,7 @@ let set_encoding : string -> unit = fun f ->
 let translate_ident : string -> string = fun s ->
   try StrMap.find s !rmap with Not_found -> s
 
-let raw_ident : string pp = fun ppf s -> Print.uid ppf (translate_ident s)
+let raw_ident : string pp = fun ppf s -> string ppf (translate_ident s)
 
 let ident : p_ident pp = fun ppf {elt;_} -> raw_ident ppf elt
 
@@ -150,7 +152,7 @@ let param_id : p_ident option pp = fun ppf idopt ->
 
 let param_ids : p_ident option list pp = List.pp param_id " "
 
-let raw_path : Path.t pp = List.pp raw_ident "."
+let raw_path : Path.t pp = List.pp string "."
 
 let path : p_path pp = fun ppf {elt;_} -> raw_path ppf elt