Adding an if-then-else syntax to Ltac2.

This is a syntactic sugar that is compiled away to a simple case analysis.

3 files changed, 23 insertions, 0 deletions

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