Theory AutoCorres_Nondet_Syntax

theory AutoCorres_Nondet_Syntax
imports AutoCorres2.AutoCorres
begin

section ‹Hide legacy nondet monad from user›


hide_const L2Defs.gets_theE

unbundle no L1Valid.validE_syntax
hide_const L1Valid.validE


definition gets_theE ::
    "('s ⇒ 'b option) ⇒ ('e, 'b, 's) exn_monad" where 
    "gets_theE ≡ λx. (liftE (gets_the x))"

section ‹Legacy syntax layer to mimic the nondet monad›

abbreviation (input) bindE:: 
  "('e,'a,'s) exn_monad ⇒ ('a ⇒ ('e, 'b, 's) exn_monad) ⇒ ('e, 'b, 's) exn_monad"  (infixl ‹>>=E› 60) where 
  "bindE ≡ bind"

abbreviation (input) bind_nd:: 
  "('a,'s) res_monad ⇒ ('a ⇒ ('b, 's) res_monad) ⇒ ('b, 's) res_monad" where 
  "bind_nd ≡ bind"

abbreviation (input) throwError::"'e ⇒ ('e, 'a, 's) exn_monad" where 
  "throwError ≡ throw"

abbreviation (input) guardE:: "('s ⇒ bool) ⇒ ('e, unit, 's) exn_monad" where 
  "guardE ≡ guard"

abbreviation (input) returnOk:: "'a ⇒ ('e, 'a, 's) exn_monad" where 
  "returnOk ≡ return"
 
abbreviation (input) whenE:: "bool ⇒ ('e, unit, 's) exn_monad ⇒ ('e, unit, 's) exn_monad" where
  "whenE ≡ when"

abbreviation (input) unlessE:: "bool ⇒ ('e, unit, 's) exn_monad ⇒ ('e, unit, 's) exn_monad" where
  "unlessE ≡ unless"

abbreviation (input) modifyE:: "('s ⇒ 's) ⇒ ('e, unit, 's) exn_monad" where
  "modifyE ≡ modify"

abbreviation (input) selectE:: "'a set ⇒ ('e, 'a, 's) exn_monad" where
  "selectE ≡ select"

abbreviation (input) unknownE:: "('e, 'a, 's) exn_monad" where
  "unknownE ≡ unknown"

abbreviation (input) getsE:: "('s ⇒ 'a) ⇒ ('e, 'a, 's) exn_monad" where
  "getsE ≡ gets"

abbreviation (input) skipE:: "('e, unit, 's) exn_monad" where
  "skipE ≡ skip"

abbreviation (input) whileLoopE::
  "('a ⇒ 's ⇒ bool) ⇒ ('a ⇒ ('e, 'a, 's) exn_monad) ⇒ 'a ⇒ ('e, 'a, 's) exn_monad"
  where
  "whileLoopE ≡ whileLoop"

abbreviation (input) handleE':: 
  "('e, 'a, 's) exn_monad ⇒ ('e ⇒ ('f, 'a, 's) exn_monad) ⇒ ('f, 'a, 's) exn_monad" 
  (infix ‹<handle2>› 10)
  where
  "handleE' ≡ catch"

abbreviation (input) handleE:: 
  "('e, 'a, 's) exn_monad ⇒ ('e ⇒ ('e, 'a, 's) exn_monad) ⇒ ('e, 'a, 's) exn_monad" 
  (infix ‹<handle>› 10)
  where
  "handleE ≡ catch"

nonterminal
  dobinds and dobind and nobind

syntax (input)
  "_dobind"    :: "[pttrn, 'a] => dobind"  (‹(‹notation=‹infix bind››_ ←/ _)› 10)
  "_dobind"    :: "[pttrn, 'a] => dobind"  (‹(‹notation=‹infix bind››_ <-/ _)› 10)
  ""           :: "dobind => dobinds"  (‹_›)
  "_nobind"    :: "'a => dobind"  (‹_›)
  "_dobinds"   :: "[dobind, dobinds] => dobinds"  (‹(‹open_block notation=‹infix do next››(_);//(_))›)

  "_do"        :: "[dobinds, 'a] => 'a"  (‹(‹notation=‹mixfix do block››do ((_);//(_))//od)› 100)
  "_doE" :: "[dobinds, 'a] => 'a"  (‹(‹notation=‹mixfix doE block››doE ((_);//(_))//odE)› 100)

syntax_consts
  "_do" ⇌ bind_nd and
  "_doE" ⇌ bindE

translations
  "_do (_dobinds b bs) e"  ⇀ "_do b (_do bs e)"
  "_do (_nobind b) e"      ⇀ "CONST bind_nd b (λ_. e)"
  "do x <- a; e od"        ⇀ "CONST bind_nd a (λx. e)"

  "_doE (_dobinds b bs) e"  ⇀ "_doE b (_doE bs e)"
  "_doE (_nobind b) e"      ⇀ "CONST bindE b (λ_. e)"
  "doE x <- a; e odE"       ⇀ "CONST bindE a (λx. e)"

term "doE x <- f; g x odE"
term "do x <- f; g x od"

syntax
  "_doO" :: "[dobinds, 'a] => 'a"  (‹(‹notation=‹mixfix DO block››DO (_);//   (_)//OD)› 100)

syntax_consts
  "_doO" == obind

translations
  "_doO (_dobinds b bs) e" == "_doO b (_doO bs e)"
  "_doO (_nobind b) e"     == "b |>> (λ_.  e)"
  "DO x <- a; e OD"        == "a |>> (λx. e)"

term "DO x <- ogets (λ_. 2); oguard (λs. b ≠ 0); oreturn x OD"

end