theory SALSemantics = Semantics + TermCodegen:

section {*  SAL Semantics  *}

datatype
  tval = ILLEGAL | NAT nat

types
  val   = nat -- "or anything else, @{text nat} used in examples"
  loc   = nat
  state = "loc \<Rightarrow> tval" -- "value and type information are stored together"

constdefs
  lift :: "(val \<Rightarrow> val \<Rightarrow> val) \<Rightarrow> tval \<Rightarrow> tval \<Rightarrow> tval"
 "lift f a b \<equiv> (case a of
    ILLEGAL \<Rightarrow> ILLEGAL
  | NAT m \<Rightarrow> (case b of
      ILLEGAL \<Rightarrow> ILLEGAL
    | NAT n \<Rightarrow> NAT (f m n)))"

(* other possibilities:
(1) datatype type = ILLEGAL | NAT
types state = "loc \<Rightarrow> val * type"

(2) datatype type = ILLEGAL | NAT
types state = "(loc \<Rightarrow> val) * (loc \<Rightarrow> type)"

(3) datatype 'a err = Err | OK 'a
datatype tval = nat err
types state = "loc \<Rightarrow> tval"
*)

(*<*)
--{* aus IMP/Natural.thy *}
constdefs
  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
  "update == fun_upd"
syntax (xsymbols)
  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
(*>*)

datatype instr = SET loc val | 
                 ADD loc loc | 
                 INC loc | 
                 JMPEQ loc loc nat | 
                 JMPB nat


types SALstate = "nat \<times> state"
types SALform = "SALstate \<Rightarrow> bool"
types SALprogram = "(instr \<times> (SALform option)) list"


constdefs cmd::"SALprogram \<Rightarrow> (nat \<Rightarrow> instr option)"
"cmd p \<equiv> \<lambda> i. if (i < length p) then Some (fst (p!i)) else None"

constdefs domC::"SALprogram \<Rightarrow> (nat list)"
"domC p \<equiv> upt 0 (length p)"

constdefs an:: "SALprogram \<Rightarrow> (nat \<Rightarrow> SALform option)"
"an p \<equiv> \<lambda> i. if (i < length p) then snd (p!i) else None"

consts
  step::"SALprogram \<Rightarrow> SALstate \<Rightarrow> SALstate option"
primrec
 "step p (i, m) = (case (cmd p i) of 
    None \<Rightarrow> None 
  | Some ins \<Rightarrow> (case ins of
      SET x n \<Rightarrow> Some (i + 1, m[x \<mapsto> NAT n])
    | ADD x y \<Rightarrow> Some (i + 1, m[x \<mapsto> lift (op +) (m x) (m y)])
    | INC x   \<Rightarrow> Some (i + 1, m[x \<mapsto> lift (op +) (m x) (NAT 1)])
    | JMPEQ x y t \<Rightarrow> (if m x = m y then Some (i + t, m) else Some (i + 1, m)) 
    | JMPB t \<Rightarrow> Some (i - t, m)))"

constdefs effS:: "SALprogram \<Rightarrow> ((nat \<times> (loc \<Rightarrow> tval)) \<times> (nat \<times> (loc \<Rightarrow> tval))) set"
"effS (p::SALprogram) \<equiv> {(s::SALstate,s'::SALstate). (step p s = Some s') }"

(*<*)
consts  evaln::"SALprogram \<Rightarrow> SALstate \<Rightarrow> nat \<Rightarrow> SALstate list"

primrec evaln:
"evaln p s 0 = []"
"evaln p s (Suc n) = (case (step p s) of None \<Rightarrow> []
                                      | Some s' \<Rightarrow> s' # (evaln p s' n))" 

constdefs showstate::"nat \<Rightarrow> SALstate \<Rightarrow> int \<times> (tval list)"
"showstate mx s \<equiv> let (pc,m)=s in (int pc, (map m (upt 0 (Suc mx))))"
(*>*)
end