Merge PR #13232: Adding an if-then-else syntax to Ltac2.

Reviewed-by: MSoegtropIMC
Ack-by: Zimmi48
Reviewed-by: jfehrle

8 files changed, 41 insertions, 6 deletions

diff --git a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst
new file mode 100644
index 0000000000..d105561a23
--- /dev/null
+++ b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  An if-then-else syntax to Ltac2
+  (`#13232 <https://github.com/coq/coq/pull/13232>`_,
+  fixes `#10110 <https://github.com/coq/coq/issues/10110>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 64fc1133f0..41f376c43d 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -38,7 +38,6 @@ Current limitations include:
   - Printing functions are limited and awkward to use.  Only a few data types are
     printable.
   - Deep pattern matching and matching on tuples don't work.
-  - If statements on Ltac2 boolean values
   - A convenient way to build terms with casts through the low-level API. Because the
     cast type is opaque, building terms with casts currently requires an awkward construction like the
     following, which also incurs extra overhead to repeat typechecking for each
@@ -345,12 +344,10 @@ Ltac2 Definitions
 
       .. coqtop:: all
 
-         Ltac2 mutable rec f b := match b with true => 0 | _ => f true end.
-         Ltac2 Set f := fun b =>
-                  match b with true => 1 | _ => f true end.
+         Ltac2 mutable rec f b := if b then 0 else f true.
+         Ltac2 Set f := fun b => if b then 1 else f true.
          Ltac2 Eval (f false).
-         Ltac2 Set f as oldf := fun b =>
-                  match b with true => 2 | _ => oldf false end.
+         Ltac2 Set f as oldf := fun b => if b then  2 else oldf false.
          Ltac2 Eval (f false).
 
       In the definition, the `f` in the body is resolved statically
@@ -1149,6 +1146,13 @@ Match on values
       | @tac2pat1 , {*, @tac2pat1 }
       | @tac2pat1
 
+.. tacn:: if @ltac2_expr5__test then @ltac2_expr5__then else @ltac2_expr5__else
+   :name: if-then-else (Ltac2)
+
+   Equivalent to a :tacn:`match <match (Ltac2)>` on a boolean value.  If the
+   :n:`@ltac2_expr5__test` evaluates to true, :n:`@ltac2_expr5__then`
+   is evaluated.  Otherwise :n:`@ltac2_expr5__else` is evaluated.
+
 .. note::
 
    For now, deep pattern matching is not implemented.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f6a684bbd7..a143a6c7cf 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -2198,6 +2198,7 @@ ltac2_expr5: [
 | REPLACE "let" OPT "rec" LIST1 ltac2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
 | WITH "let" OPT "rec" ltac2_let_clause LIST0 ( "with" ltac2_let_clause ) "in" ltac2_expr6 TAG Ltac2
 | MOVETO simple_tactic "match" ltac2_expr5 "with" OPT ltac2_branches "end"      (* Ltac2 plugin *)
+| MOVETO simple_tactic "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* Ltac2 plugin *)
 | DELETE simple_tactic
 ]
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index c764cb6f37..0638e1753b 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2586,6 +2586,7 @@ ltac2_expr5: [
 | "fun" LIST1 G_LTAC2_input_fun "=>" ltac2_expr6      (* Ltac2 plugin *)
 | "let" rec_flag LIST1 G_LTAC2_let_clause SEP "with" "in" ltac2_expr6      (* Ltac2 plugin *)
 | "match" ltac2_expr5 "with" G_LTAC2_branches "end"      (* Ltac2 plugin *)
+| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5      (* Ltac2 plugin *)
 | ltac2_expr4      (* Ltac2 plugin *)
 ]
 
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 12a7bc684d..7d773e3a5b 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1640,6 +1640,7 @@ simple_tactic: [
 | "ring" OPT ( "[" LIST1 one_term "]" )
 | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident )
 | "match" ltac2_expr5 "with" OPT ltac2_branches "end"
+| "if" ltac2_expr5 "then" ltac2_expr5 "else" ltac2_expr5
 | qualid LIST1 tactic_arg
 ]
 
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 6749169e8c..65b61a0d93 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -146,6 +146,8 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CTacLet (isrec, lc, e) }
       | "match"; e = ltac2_expr LEVEL "5"; "with"; bl = branches; "end" ->
         { CAst.make ~loc @@ CTacCse (e, bl) }
+      | "if"; e = ltac2_expr LEVEL "5"; "then"; e1 = ltac2_expr LEVEL "5"; "else"; e2 = ltac2_expr LEVEL "5" ->
+        { CAst.make ~loc @@ CTacIft (e, e1, e2) }
       ]
     | "4" LEFTA [ ]
     | "3" [ e0 = SELF; ","; el = LIST1 NEXT SEP "," ->
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index 548655f561..0ae016265a 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -105,6 +105,7 @@ type raw_tacexpr_r =
 | CTacLet of rec_flag * (raw_patexpr * raw_tacexpr) list * raw_tacexpr
 | CTacCnv of raw_tacexpr * raw_typexpr
 | CTacSeq of raw_tacexpr * raw_tacexpr
+| CTacIft of raw_tacexpr * raw_tacexpr * raw_tacexpr
 | CTacCse of raw_tacexpr * raw_taccase list
 | CTacRec of raw_recexpr
 | CTacPrj of raw_tacexpr * ltac_projection or_relid
diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml
index 797f72702d..ddf70a5a65 100644
--- a/user-contrib/Ltac2/tac2intern.ml
+++ b/user-contrib/Ltac2/tac2intern.ml
@@ -29,6 +29,7 @@ let t_string = coq_type "string"
 let t_constr = coq_type "constr"
 let t_ltac1 = ltac1_type "t"
 let t_preterm = coq_type "preterm"
+let t_bool = coq_type "bool"
 
 (** Union find *)
 
@@ -749,6 +750,15 @@ let rec intern_rec env {loc;v=e} = match e with
   let (e2, t2) = intern_rec env e2 in
   let () = check_elt_unit loc1 env t1 in
   (GTacLet (false, [Anonymous, e1], e2), t2)
+| CTacIft (e, e1, e2) ->
+  let loc = e.loc in
+  let loc1 = e1.loc in
+  let (e, t) = intern_rec env e in
+  let (e1, t1) = intern_rec env e1 in
+  let (e2, t2) = intern_rec env e2 in
+  let () = unify ?loc env t (GTypRef (Other t_bool, [])) in
+  let () = unify ?loc:loc1 env t1 t2 in
+  (GTacCse (e, Other t_bool, [|e1; e2|], [||]), t2)
 | CTacCse (e, pl) ->
   intern_case env loc e pl
 | CTacRec fs ->
@@ -1271,6 +1281,11 @@ let rec globalize ids ({loc;v=er} as e) = match er with
   let e1 = globalize ids e1 in
   let e2 = globalize ids e2 in
   CAst.make ?loc @@ CTacSeq (e1, e2)
+| CTacIft (e, e1, e2) ->
+  let e = globalize ids e in
+  let e1 = globalize ids e1 in
+  let e2 = globalize ids e2 in
+  CAst.make ?loc @@ CTacIft (e, e1, e2)
 | CTacCse (e, bl) ->
   let e = globalize ids e in
   let bl = List.map (fun b -> globalize_case ids b) bl in
@@ -1486,6 +1501,11 @@ let rec subst_rawexpr subst ({loc;v=tr} as t) = match tr with
   let e1' = subst_rawexpr subst e1 in
   let e2' = subst_rawexpr subst e2 in
   if e1' == e1 && e2' == e2 then t else CAst.make ?loc @@ CTacSeq (e1', e2')
+| CTacIft (e, e1, e2) ->
+  let e' = subst_rawexpr subst e in
+  let e1' = subst_rawexpr subst e1 in
+  let e2' = subst_rawexpr subst e2 in
+  if e' == e && e1' == e1 && e2' == e2 then t else CAst.make ?loc @@ CTacIft (e', e1', e2')
 | CTacCse (e, bl) ->
   let map (p, e as x) =
     let p' = subst_rawpattern subst p in