diff --git a/.github/dependabot.yml b/.github/dependabot.yml new file mode 100644 index 000000000..bc9a4d59b --- /dev/null +++ b/.github/dependabot.yml @@ -0,0 +1,7 @@ +version: 2 + +updates: + - package-ecosystem: github-actions + directory: / + schedule: + interval: weekly diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index a5e92521e..0fb5cc31a 100644 --- a/.github/workflows/main.yml +++ b/.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 }} diff --git a/CHANGES.md b/CHANGES.md index fbcdb973c..d7a7eece9 100644 --- a/CHANGES.md +++ b/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) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 56a707455..60f84490c 100644 --- a/CONTRIBUTING.md +++ b/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 diff --git a/doc/Makefile.bnf b/doc/Makefile.bnf index 3d2d515ef..d98702b79 100644 --- a/doc/Makefile.bnf +++ b/doc/Makefile.bnf @@ -68,6 +68,7 @@ lambdapi.bnf: Makefile.bnf ../src/parsing/lpParser.mly -e 's/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' \ diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf index ff67cb2fd..6251318e9 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -153,6 +153,7 @@ QID ::= [UID "."]+ UID | "simplify" [] | "solve" | "symmetry" + | "try" | "why3" [] ::= diff --git a/doc/tactics.rst b/doc/tactics.rst index c2d96776d..021502b3d 100644 --- a/doc/tactics.rst +++ b/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`` diff --git a/editors/emacs/lambdapi-smie.el b/editors/emacs/lambdapi-smie.el index 229f3b0f5..0802c6d5e 100644 --- a/editors/emacs/lambdapi-smie.el +++ b/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)) diff --git a/editors/emacs/lambdapi-vars.el b/editors/emacs/lambdapi-vars.el index 37130744e..b51bd6810 100644 --- a/editors/emacs/lambdapi-vars.el +++ b/editors/emacs/lambdapi-vars.el @@ -18,6 +18,7 @@ "simplify" "solve" "symmetry" + "try" "why3") "Proof tactics.") diff --git a/editors/vim/syntax/lambdapi.vim b/editors/vim/syntax/lambdapi.vim index a2e8acd53..4fe2371e4 100644 --- a/editors/vim/syntax/lambdapi.vim +++ b/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 diff --git a/editors/vscode/syntaxes/lp.tmLanguage.json b/editors/vscode/syntaxes/lp.tmLanguage.json index 0edac9c72..2ad60a20e 100644 --- a/editors/vscode/syntaxes/lp.tmLanguage.json +++ b/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" }, diff --git a/src/core/tree.ml b/src/core/tree.ml index 1e96ae00a..e94d8cbf7 100644 --- a/src/core/tree.ml +++ b/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 diff --git a/src/export/coq.ml b/src/export/coq.ml index 7b0e10ce9..9a6f51bd9 100644 --- a/src/export/coq.ml +++ b/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 diff --git a/src/handle/command.ml b/src/handle/command.ml index f99821097..25bb420bb 100644 --- a/src/handle/command.ml +++ b/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; diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 00bdb88c3..abee6a8eb 100644 --- a/src/handle/tactic.ml +++ b/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 diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 6ae3cbb43..f3265a471 100644 --- a/src/parsing/lpLexer.ml +++ b/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 diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly index f791f6191..a3e672440 100644 --- a/src/parsing/lpParser.mly +++ b/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: diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index e9a4c8793..935e7cd75 100644 --- a/src/parsing/pretty.ml +++ b/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 diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index b9cb8c920..b87d279dd 100644 --- a/src/parsing/syntax.ml +++ b/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 = diff --git a/tests/OK/1033.lp b/tests/OK/1033.lp new file mode 100644 index 000000000..e2b4c5e82 --- /dev/null +++ b/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; diff --git a/tests/OK/try.lp b/tests/OK/try.lp new file mode 100644 index 000000000..065506da3 --- /dev/null +++ b/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; diff --git a/tests/regressions/xtc.expected b/tests/regressions/xtc.expected index 94f5c4035..7510feae8 100644 --- a/tests/regressions/xtc.expected +++ b/tests/regressions/xtc.expected @@ -5,34 +5,34 @@ - tests.OK.boolean.bool_and1_0tests.OK.boolean.false + tests.OK.boolean.bool_andtests.OK.boolean.true1_0 - tests.OK.boolean.false + 1_0 - tests.OK.boolean.bool_and2_0tests.OK.boolean.true + tests.OK.boolean.bool_andtests.OK.boolean.false2_0 - 2_0 + tests.OK.boolean.false - tests.OK.boolean.bool_andtests.OK.boolean.false3_0 + tests.OK.boolean.bool_and3_0tests.OK.boolean.true - tests.OK.boolean.false + 3_0 - tests.OK.boolean.bool_andtests.OK.boolean.true4_0 + tests.OK.boolean.bool_and4_0tests.OK.boolean.false - 4_0 + tests.OK.boolean.false @@ -45,50 +45,50 @@ - tests.OK.boolean.bool_negtests.OK.boolean.false + tests.OK.boolean.bool_negtests.OK.boolean.true - tests.OK.boolean.true + tests.OK.boolean.false - tests.OK.boolean.bool_negtests.OK.boolean.true + tests.OK.boolean.bool_negtests.OK.boolean.false - tests.OK.boolean.false + tests.OK.boolean.true - tests.OK.boolean.bool_or7_0tests.OK.boolean.false + tests.OK.boolean.bool_ortests.OK.boolean.true7_0 - 7_0 + tests.OK.boolean.true - tests.OK.boolean.bool_or8_0tests.OK.boolean.true + tests.OK.boolean.bool_ortests.OK.boolean.false8_0 - tests.OK.boolean.true + 8_0 - tests.OK.boolean.bool_ortests.OK.boolean.false9_0 + tests.OK.boolean.bool_or9_0tests.OK.boolean.true - 9_0 + tests.OK.boolean.true - tests.OK.boolean.bool_ortests.OK.boolean.true10_0 + tests.OK.boolean.bool_or10_0tests.OK.boolean.false - tests.OK.boolean.true + 10_0