Stream: General

Topic: Random idea: multiway if?


view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC