Merge branch 'master' into new_exports

.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

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

src/handle/command.ml

@@ -218,12 +218,17 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
     (* Scope rules, and check that they preserve typing. Return the list of
        rules [srs] and also a map [map] mapping every symbol defined by a rule
        of [srs] to its defining rules. *)
-      let handle_rule (srs, map) r =
+      let handle_rule r (srs, map) =
         let (s,r) as sr = check_rule ss r in
         let h = function Some rs -> Some(r::rs) | None -> Some[r] in
         sr::srs, SymMap.update s h map
       in
-      let srs, map = List.fold_left handle_rule ([], SymMap.empty) rs in
+      (* The order of rules must be kept between [rs] and [srs].
+         That is, the following assertion should hold
+         [assert (srs = List.map (check_rule ss) rs);] if we could compare
+         functional values. Failure to keep that invariant breaks some
+         evaluation strategies. *)
+      let srs, map = List.fold_right handle_rule rs ([], SymMap.empty) in
       (* /!\ Update decision trees without adding the rules themselves. It is
          important for local confluence checking. *)
       SymMap.iter Tree.update_dtree map;

src/handle/tactic.ml

@@ -170,7 +170,7 @@ let count_products : ctxt -> term -> int = fun c ->
 
 (** [handle ss sym_pos prv ps tac] applies tactic [tac] in the proof state
    [ps] and returns the new proof state. *)
-let handle :
+let rec handle :
   Sig_state.t -> popt -> bool -> proof_state -> p_tactic -> proof_state =
   fun ss sym_pos prv ps {elt;pos} ->
   match ps.proof_goals with
@@ -367,6 +367,9 @@ let handle :
        | Typ gt::_ ->
          Why3_tactic.handle ss pos cfg gt; tac_admit ss sym_pos ps gt
        | _ -> assert false)
+  | P_tac_try tactic -> 
+    try handle ss sym_pos prv ps tactic 
+    with Fatal(_, _s) -> ps 
 
 (** Representation of a tactic output. *)
 type tac_output = proof_state * Query.result

src/parsing/lpLexer.ml

@@ -80,6 +80,7 @@ type token =
   | SOLVE
   | SYMBOL
   | SYMMETRY
+  | TRY
   | TYPE_QUERY
   | TYPE_TERM
   | UNIF_RULE
@@ -249,6 +250,7 @@ let rec token lb =
   | "solve" -> SOLVE
   | "symbol" -> SYMBOL
   | "symmetry" -> SYMMETRY
+  | "try" -> TRY
   | "type" -> TYPE_QUERY
   | "TYPE" -> TYPE_TERM
   | "unif_rule" -> UNIF_RULE

src/parsing/lpParser.mly

@@ -73,6 +73,7 @@
 %token SOLVE
 %token SYMBOL
 %token SYMMETRY
+%token TRY
 %token TYPE_QUERY
 %token TYPE_TERM
 %token UNIF_RULE
@@ -347,6 +348,7 @@ tactic:
   | SIMPLIFY i=qid_or_nat? { make_pos $sloc (P_tac_simpl i) }
   | SOLVE { make_pos $sloc P_tac_solve }
   | SYMMETRY { make_pos $sloc P_tac_sym }
+  | TRY t=tactic { make_pos $sloc (P_tac_try t) }
   | WHY3 s=STRINGLIT? { make_pos $sloc (P_tac_why3 s) }
 
 rw_patt:

src/parsing/pretty.ml

@@ -258,7 +258,7 @@ let query : p_query pp = fun ppf { elt; _ } ->
   | P_query_verbose i -> out ppf "verbose %s" i
   | P_query_search s -> out ppf "search \"%s\"" s
 
-let tactic : p_tactic pp = fun ppf { elt;  _ } ->
+let rec tactic : p_tactic pp = fun ppf { elt;  _ } ->
   begin match elt with
   | P_tac_admit -> out ppf "admit"
   | P_tac_apply t -> out ppf "apply %a" term t
@@ -281,6 +281,7 @@ let tactic : p_tactic pp = fun ppf { elt;  _ } ->
   | P_tac_simpl (Some qid) -> out ppf "simplify %a" qident qid
   | P_tac_solve -> out ppf "solve"
   | P_tac_sym -> out ppf "symmetry"
+  | P_tac_try t -> out ppf "try %a" tactic t 
   | P_tac_why3 p ->
       let prover ppf s = out ppf " \"%s\"" s in
       out ppf "why3%a" (Option.pp prover) p

src/parsing/syntax.ml

@@ -227,8 +227,8 @@ type p_tactic_aux =
   | P_tac_solve
   | P_tac_sym
   | P_tac_why3 of string option
-
-type p_tactic = p_tactic_aux loc
+  | P_tac_try of p_tactic
+and p_tactic = p_tactic_aux loc
 
 (** [is_destructive t] says whether tactic [t] changes the current goal. *)
 let is_destructive {elt;_} = match elt with P_tac_have _ -> false | _ -> true
@@ -569,7 +569,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
     | P_query_search _ -> a
   in
 
-  let fold_tactic : StrSet.t * 'a -> p_tactic -> StrSet.t * 'a =
+  let rec fold_tactic : StrSet.t * 'a -> p_tactic -> StrSet.t * 'a =
     fun (vs,a) t ->
     match t.elt with
     | P_tac_refine t
@@ -592,6 +592,7 @@ let fold_idents : ('a -> p_qident -> 'a) -> 'a -> p_command list -> 'a =
     | P_tac_fail
     | P_tac_generalize _
     | P_tac_induction -> (vs, a)
+    | P_tac_try tactic -> fold_tactic (vs,a) tactic
   in
 
   let fold_inductive_vars : StrSet.t -> 'a -> p_inductive -> 'a =

tests/OK/1033.lp

@@ -0,0 +1,9 @@
+// Test on the sequential reduction strategy
+constant symbol I: TYPE;
+constant symbol i: I;
+constant symbol j: I;
+sequential symbol k: I → I;
+rule k i ↪ i
+with k i ↪ j;
+
+assert ⊢ k i ≡ i;

tests/OK/try.lp

@@ -0,0 +1,77 @@
+
+// Type of data type codes and their interpretation as types.
+
+constant symbol U : TYPE;
+
+injective symbol T : U → TYPE;
+
+constant symbol Prop : TYPE;
+
+symbol P : Prop → TYPE;
+
+symbol o: U;
+rule T o ↪ Prop;
+
+constant symbol = [a] : T a → T a → Prop;
+
+notation = infix 0.1;
+
+constant symbol refl a (x:T a) : P (x = x);
+
+constant symbol eqind a (x y:T a) : P (x = y) → Π p, P (p y) → P (p x);
+
+builtin "P"     ≔ P;
+builtin "T"     ≔ T;
+builtin "eq"    ≔ =;
+builtin "eqind" ≔ eqind;
+builtin "refl"  ≔ refl;
+
+
+private symbol a: Prop;
+private symbol b: Prop;
+
+constant symbol ⊤: Prop;
+constant symbol ⊥: Prop;
+
+constant symbol ∧ : Prop → Prop → Prop; notation ∧ infix left 7; // /\ or \wedge
+
+constant symbol ∧ᵢ [p q] : P p → P q → P (p ∧ q);
+symbol ∧ₑ₁ [p q] : P (p ∧ q) → P p;
+symbol ∧ₑ₂ [p q] : P (p ∧ q) → P q;
+
+constant symbol ∨ : Prop → Prop → Prop; notation ∨ infix right 6; // \/ or \vee
+
+constant symbol ∨ᵢ₁ [p q] : P p → P (p ∨ q);
+constant symbol ∨ᵢ₂ [p q] : P q → P (p ∨ q);
+symbol ∨ₑ [p q r] : P (p ∨ q) → (P p → P r) → (P q → P r) → P r;
+
+symbol ¬: Prop → Prop; notation ¬ prefix 2;
+
+symbol eq_simp x : P ((x = x) = ⊤);
+symbol eq_simp_neg_l x : P ((¬ x = x) = ⊥);
+symbol eq_simp_refl_r x : P ((¬ x = x) = ⊥);
+symbol eq_simp_2 x : P ((⊥ = x) = ¬ x);
+
+opaque symbol test1 (x : Prop) : P ((¬ x = x) = ⊥)
+≔ begin
+  assume x;
+  try rewrite eq_simp x;  // (fail)
+  try rewrite eq_simp_neg_l x;
+  try rewrite eq_simp_refl_r x; // (fail)
+  try rewrite eq_simp_2 x; // (fail)
+  reflexivity
+end;
+
+symbol or_simplify_idem x : P ((x ∨ x) = x);
+symbol or_simplify_true_r x : P ((x ∨ ⊤) = ⊤);
+symbol or_simplify_true_l x : P ((⊤ ∨ x) = ⊤);
+
+opaque symbol test2 (a b c d : Prop) : P (a ∨ ⊤ ∨ c ∨ ⊤ ∨ d ∨ d = ⊤)
+≔ begin
+  assume a b c d;
+  rewrite (or_simplify_idem d);
+  try rewrite or_simplify_true_r; // (fail)
+  rewrite or_simplify_true_l;
+  rewrite or_simplify_true_r;
+  reflexivity
+end;