Theory Language

(*
 * 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
as 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 c1 b c2 = Catch c1 (Cond b c2 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