From 2559f0474c8cd66b5020524d1e758ea7a19bc8fb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 21 Oct 2020 14:41:53 +0200 Subject: Document the syntax addition. --- .../05-tactic-language/13232-ltac2-if-then-else.rst | 5 +++++ doc/sphinx/proof-engine/ltac2.rst | 17 +++++++++++------ 2 files changed, 16 insertions(+), 6 deletions(-) create mode 100644 doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst (limited to 'doc') 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 `_, + fixes `#10110 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 64fc1133f0..d4e49dda5b 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 @@ -267,6 +266,7 @@ There is dedicated syntax for list and array literals. | @ltac2_expr5 ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr + | if @ltac2_expr5 then @ltac2_expr5 else @ltac2_expr5 | @ltac2_expr3 ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } @@ -345,12 +345,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 +1147,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 ` 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. -- cgit v1.2.3 From 1b0e754ccf22cc1a7ae50a7b1d8350197ec2981b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 2 Nov 2020 13:45:08 +0100 Subject: Regenerate the grammar description file. --- doc/sphinx/proof-engine/ltac2.rst | 1 - doc/tools/docgram/common.edit_mlg | 1 + doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + 4 files changed, 3 insertions(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index d4e49dda5b..41f376c43d 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -266,7 +266,6 @@ There is dedicated syntax for list and array literals. | @ltac2_expr5 ltac2_expr5 ::= fun {+ @tac2pat0 } => @ltac2_expr | let {? rec } @ltac2_let_clause {* with @ltac2_let_clause } in @ltac2_expr - | if @ltac2_expr5 then @ltac2_expr5 else @ltac2_expr5 | @ltac2_expr3 ltac2_let_clause ::= {+ @tac2pat0 } := @ltac2_expr ltac2_expr3 ::= {+, @ltac2_expr2 } 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 ] -- cgit v1.2.3