Theory CZH_Sets_MIF

(* Copyright 2021 (C) Manuel Eberl *)

section‹Mutliway If›
theory CZH_Sets_MIF
  imports Main
begin

text‹
The code that is presented in this section was originally written 
by Manuel Eberl and appeared in a post on the mailing list of Isabelle:
\<^cite>‹"eberl_syntax_2021"›.
The code was ported with minor amendments by the author of this work.
›

abbreviation multi_If :: "bool ⇒ 'a ⇒ 'a ⇒ 'a"
  where "multi_If ≡ If"

nonterminal if_clauses and if_clause

syntax
  "_if_block" :: "if_clauses ⇒ 'a" (‹(1if _)› [12] 10)
  "_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)

syntax_consts
  "_if_block" "_if_clause" "_if_final" "_if_cons" ⇌ multi_If

translations
  "_if_block (_if_cons (_if_clause b t) (_if_final e))"
    ⇌ "CONST multi_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"

text‹\newpage›

end