Add try tactic

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

@@ -88,6 +88,7 @@ syntax keyword KeywordOK contained symbol
 syntax keyword KeywordOK contained symmetry
 syntax keyword KeywordOK contained type
 syntax keyword KeywordOK contained TYPE
+syntax keyword KeywordOK contained try
 syntax keyword KeywordOK contained unif_rule
 syntax keyword KeywordOK contained verbose
 syntax keyword KeywordOK contained why3
@@ -154,6 +155,7 @@ syntax keyword KeywordKO contained symbol
 syntax keyword KeywordKO contained symmetry
 syntax keyword KeywordKO contained type
 syntax keyword KeywordKO contained TYPE
+syntax keyword KeywordKO contained try
 syntax keyword KeywordKO contained unif_rule
 syntax keyword KeywordKO contained verbose
 syntax keyword KeywordKO contained why3

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|type|TYPE|try|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

@@ -82,6 +82,7 @@ type token =
   | SYMMETRY
   | TYPE_QUERY
   | TYPE_TERM
+  | TRY
   | UNIF_RULE
   | VERBOSE
   | WHY3
@@ -251,6 +252,7 @@ let rec token lb =
   | "symmetry" -> SYMMETRY
   | "type" -> TYPE_QUERY
   | "TYPE" -> TYPE_TERM
+  | "try" -> TRY
   | "unif_rule" -> UNIF_RULE
   | "verbose" -> VERBOSE
   | "why3" -> WHY3

src/parsing/lpParser.mly

@@ -75,6 +75,7 @@
 %token SYMMETRY
 %token TYPE_QUERY
 %token TYPE_TERM
+%token TRY
 %token UNIF_RULE
 %token VERBOSE
 %token WHY3
@@ -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,6 +227,7 @@ type p_tactic_aux =
   | P_tac_solve
   | P_tac_sym
   | P_tac_why3 of string option
+  | P_tac_try of p_tactic_aux loc
 
 type p_tactic = p_tactic_aux loc
 
@@ -569,7 +570,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 +593,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;