(*
 * Copyright 2016, Data61, CSIRO
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(DATA61_BSD)
 *)

section ‹The COMPLX Syntax›

theory Language
imports Main
begin

subsection ‹The Core Language›

text ‹We use a shallow embedding of boolean expressions as well as assertions
  sets of states.
 ›

type_synonym 's bexp = "'s set"
type_synonym 's assn = "'s set"

datatype ('s, 'p, 'f) com =
    Skip
  | Basic "'s → 's"
  | Spec "('s × 's) set"
  | Seq "('s ,'p, 'f) com" "('s,'p, 'f) com"    
  | Cond "'s bexp" "('s,'p,'f) com"  "('s,'p,'f) com"
  | While "'s bexp" "('s,'p,'f) com"
  | Call "'p"
  | DynCom "'s → ('s,'p,'f) com" 
  | Guard "'f" "'s bexp" "('s,'p,'f) com" 
  | Throw
  | Catch "('s,'p,'f) com" "('s,'p,'f) com"
  | Parallel "('s, 'p, 'f) com list"
  | Await "'s bexp" "('s,'p,'f) com"


subsection ‹Derived Language Constructs›

text ‹We inherit the remainder of derived language constructs from SIMPL›

definition
  raise:: "('s → 's) → ('s,'p,'f) com" where
  "raise f = Seq (Basic f) Throw"

definition
  condCatch:: "('s,'p,'f) com → 's bexp → ('s,'p,'f) com → ('s,'p,'f) com" where
  "condCatch c₁ b c₂ = Catch c₁ (Cond b c₂ Throw)"

definition
  bind:: "('s → 'v) → ('v → ('s,'p,'f) com) → ('s,'p,'f) com" where
  "bind e c = DynCom (λs. c (e s))"

definition
  bseq:: "('s,'p,'f) com → ('s,'p,'f) com → ('s,'p,'f) com" where
  "bseq = Seq"
 
definition
  block:: "['s→'s ,('s,'p,'f) com,'s→'s→'s,'s→'s→('s,'p,'f) com]→('s,'p,'f) com"
where
  "block init bdy restore return =
    DynCom (λs. (Seq (Catch (Seq (Basic init) bdy) (Seq (Basic (restore s)) Throw))
                            (DynCom (λt. Seq (Basic (restore s)) (return s t))))
                        )" 

definition
  call:: "('s→'s) → 'p → ('s → 's → 's)→('s→'s→('s,'p,'f) com)→('s,'p,'f)com" where
  "call init p restore return = block init (Call p) restore return"

definition
  dynCall:: "('s→'s) → ('s → 'p) → ('s → 's → 's) →
             ('s → 's → ('s,'p,'f) com) → ('s,'p,'f) com" where
  "dynCall init p restore return = DynCom (λs. call init (p s) restore return)"

definition
  fcall:: "('s→'s) → 'p → ('s → 's → 's)→('s → 'v) → ('v→('s,'p,'f) com)
            →('s,'p,'f) com" where
  "fcall init p restore result return = call init p restore (λs t. return (result t))"

definition
  lem:: "'x → ('s,'p,'f)com →('s,'p,'f)com" where
  "lem x c = c"

primrec switch:: "('s → 'v) → ('v set × ('s,'p,'f) com) list → ('s,'p,'f) com" 
where
"switch v [] = Skip" |
"switch v (Vc#vs) = Cond {s. v s ∈ fst Vc} (snd Vc) (switch v vs)"

definition guaranteeStrip:: "'f → 's set → ('s,'p,'f) com → ('s,'p,'f) com"
  where "guaranteeStrip f g c = Guard f g c"

definition guaranteeStripPair:: "'f → 's set → ('f × 's set)"
  where "guaranteeStripPair f g = (f,g)"

primrec guards:: "('f × 's set ) list → ('s,'p,'f) com → ('s,'p,'f) com"
where
"guards [] c = c" |
"guards (g#gs) c = Guard (fst g) (snd g) (guards gs c)"

definition
  while::  "('f × 's set) list → 's bexp → ('s,'p,'f) com → ('s, 'p, 'f) com"
where
  "while gs b c = guards gs (While b (Seq c (guards gs Skip)))"

definition
  whileAnno:: 
  "'s bexp → 's assn → ('s × 's) assn → ('s,'p,'f) com → ('s,'p,'f) com" where
  "whileAnno b I V c = While b c"

definition
  whileAnnoG:: 
  "('f × 's set) list → 's bexp → 's assn → ('s × 's) assn →
     ('s,'p,'f) com → ('s,'p,'f) com" where
  "whileAnnoG gs b I V c = while gs b c"
 
definition
  specAnno::  "('a → 's assn) → ('a → ('s,'p,'f) com) →
                         ('a → 's assn) → ('a → 's assn) → ('s,'p,'f) com"
  where "specAnno P c Q A = (c undefined)"

definition
  whileAnnoFix:: 
  "'s bexp → ('a → 's assn) → ('a → ('s × 's) assn) → ('a → ('s,'p,'f) com) →
     ('s,'p,'f) com" where
  "whileAnnoFix b I V c = While b (c undefined)"

definition
  whileAnnoGFix:: 
  "('f × 's set) list → 's bexp → ('a → 's assn) → ('a → ('s × 's) assn) →
     ('a → ('s,'p,'f) com) → ('s,'p,'f) com" where
  "whileAnnoGFix gs b I V c = while gs b (c undefined)"

definition if_rel::"('s → bool) → ('s → 's) → ('s → 's) → ('s → 's) → ('s × 's) set" 
  where "if_rel b f g h = {(s,t). if b s then t = f s else t = g s ∨ t = h s}"

lemma fst_guaranteeStripPair: "fst (guaranteeStripPair f g) = f"
  by (simp add: guaranteeStripPair_def)

lemma snd_guaranteeStripPair: "snd (guaranteeStripPair f g) = g"
  by (simp add: guaranteeStripPair_def)

end