Add try tactic (#1032)

* Add try tactic

If T is a tactic, then try T is a tactic that is just like T except that, if T fails, try T successfully does nothing at all (rather than failing).

CHANGES.md

@@ -8,6 +8,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### 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
 

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