[isabelle] Syntax proposal: multiway if


there is a Haskell extension that allows writing nested ifs in the
following nice syntax:

if | P -> a
   | Q -> b
   | R -> c
   | otherwise -> d

I asked around and some people (e.g. Tobias Nipkow) agree that this
might be nice to have. My proposed syntax is inspired by the "case"
syntax and looks like this:

  if P ⇒ x | Q ⇒ y | R ⇒ z | otherwise ⇒ u

One could also do

  if P ⇒ x | Q ⇒ y | R ⇒ z | _ ⇒ u


I attached a small theory that implements this.

Not sure if this should be enabled for output by default as well –
probably not. One could switch it on only in a special "multi_if" print
mode, similarly to "do_notation" for monad syntax.

The current implementation has the problem that "if b then x else y"
gets output as "if b ⇒ x | otherwise ⇒ y", which we clearly don't want.
Not sure how to fix that.

theory Multiway_If
  imports Main (* "HOL-Library.Monad_Syntax" *)

abbreviation multi_If
  where "multi_If \<equiv> If"

nonterminal if_clauses and if_clause

  "_if_block" :: "if_clauses \<Rightarrow> 'a" ("(1if _)" [12] 10)
  "_if_clause"  :: "bool \<Rightarrow> 'a \<Rightarrow> if_clause" ("(2_ \<Rightarrow>/ _)" 13)
  "_if_final" :: "'a \<Rightarrow> if_clauses" ("otherwise \<Rightarrow> _")
  "_if_cons" :: "[if_clause, if_clauses] \<Rightarrow> if_clauses" ("_ /| _" [13, 12] 12)

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

  "_if_block (_if_cons (_if_clause b t) (_if_final e))"
    \<rightleftharpoons> "CONST multi_If b t e"
  "_if_block (_if_cons b (_if_cons c cs))"
    \<rightleftharpoons> "_if_block (_if_cons b (_if_final (_if_block (_if_cons c cs))))"
  "_if_block (_if_final e)" \<rightharpoonup> "e"

term "if P then a else b"

(* notice how it wraps:
  "f x =
   (if P \<Rightarrow> x | Q \<Rightarrow> y | R \<Rightarrow> z | A \<Rightarrow> x 
     | B \<Rightarrow> y | Z \<Rightarrow> z | otherwise \<Rightarrow> bla)"
    :: "bool"
term "f x = (if P \<Rightarrow> x | Q \<Rightarrow> y | R \<Rightarrow> z | A \<Rightarrow> x | B \<Rightarrow> y | Z \<Rightarrow> z | otherwise \<Rightarrow> bla)"


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.