## Stream: General

### Topic: Random idea: multiway if?

#### Manuel Eberl (Feb 10 2021 at 12:38):

There's a Haskell extention that allows multiway ifs:

``````if | x < 3     -> "small"
| x < 7     -> "medium"
| otherwise -> "large"
``````

It might be nice to have something like that in Isabelle to avoid some of those clunky nested `if then else` constructs.

Not sure if it's really worth it but one could try?

#### Mathias Fleury (Feb 10 2021 at 12:43):

I tend to use case for that, even if it has a slightly different semantics…

``````case (x < 3, x < 7) of
(True, _) => "small"
| (_, True) => "medium"
| _ => "large"
``````

#### Manuel Eberl (Feb 10 2021 at 13:38):

Possible solution:

``````syntax
"_multiway_if" :: "multiway_if ⇒ 'a" ("if {//(2 _)//}" [12] 62)
"_multiway_if_clause" :: "bool ⇒ 'a ⇒ multiway_if_clause" ("(2_ ⇒/ _)" 13)
"_multiway_if_cons" :: "multiway_if_clause ⇒ multiway_if ⇒ multiway_if" ("_;//_" [13, 12] 12)
"_multiway_if_final" :: "'a ⇒ multiway_if" ("otherwise ⇒ _")

translations
"_multiway_if (_multiway_if_cons (_multiway_if_clause b x) y)" == "CONST If b x (_multiway_if y)"
"_multiway_if (_multiway_if_final x)" => "x"

term "if {p ⇒ y; q ⇒ z; r ⇒ u; otherwise ⇒ x}"
``````

Possible other syntax:

``````f x = if {x ≥ 0 ⇒ 1; x ≤ 0 ⇒ -1; otherwise ⇒ 0}
f x = (if x ≥ 0 ⇒ 1 | x ≤ 0 ⇒ -1 | otherwise ⇒ 0)
f x = (1 if x ≥ 0; -1 if x ≤ 0; 0 otherwise)
``````

One could also replace `if` with `case` or drop it entirely, or replace `otherwise` with `else`, replace parentheses with bracets, semicolon with "|" etc.

Not sure how to make the translations work for output as well.

#### Manuel Eberl (Feb 10 2021 at 14:32):

Okay this works for output as well, but it has the disadvantage of also printing `if b then x else y` as `if {b ⇒ x; otherwise ⇒ y}`. One would have to tweak it a bit more to prevent that.

``````nonterminal if_clauses and if_clause

syntax
"_if_block" :: "if_clauses ⇒ 'a" ("if {//(2  _)//}" [12] 62)
"_if_clause"  :: "bool ⇒ 'a ⇒ if_clause" ("(2_ ⇒/ _)" 13)
"_if_final" :: "'a ⇒ if_clauses" ("otherwise ⇒ _")
"_if_cons" :: "[if_clause, if_clauses] ⇒ if_clauses" ("_;//_" [13, 12] 12)

syntax (ASCII)
"_if_clause" :: "[pttrn, 'a] ⇒ if_clause" ("(2_ =>/ _)" 13)

translations
"_if_block (_if_cons (_if_clause b t) (_if_final e))"
⇌ "CONST If b t e"
"_if_block (_if_cons b (_if_cons c cs))"
⇌ "_if_block (_if_cons b (_if_final (_if_block (_if_cons c cs))))"
"_if_block (_if_final e)" ⇀ "e"

term "if {P ⇒ x; Q ⇒ y; R ⇒ z; otherwise ⇒ bla}"
``````

Last updated: Jun 20 2024 at 12:31 UTC