theory SALSemantics_deep = DeepLogic:

section {* SAL Semantics *}

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)
    | POS ra \<Rightarrow> ILLEGAL)
  | POS ra \<Rightarrow> ILLEGAL)"

types
  tram = "loc \<Rightarrow> tval"

record env =
  cs :: "(nat \<times> tram) list"
  h :: "pos list"

types
  SALstate = "pos \<times> tram \<times> env"
  SALform = "form"
  SALprocedure = "pname \<times> ((instr \<times> (SALform option)) list)"
  SALprogram = "SALprocedure list"

consts 
  noProc :: "SALprogram \<Rightarrow> pname \<Rightarrow> bool"
primrec
 "noProc [] pn = True"
 "noProc (p # ps) pn = (let (pn', bdy) = p in (if pn' = pn then False else noProc ps pn))"

consts
  cmd :: "SALprogram \<Rightarrow> (pos \<Rightarrow> instr option)"
primrec
 "cmd [] pc = None"
 "cmd (p # ps) pc = (let (pn, bdy) = p; (pn', i) = pc in 
    if pn = pn' then 
     (if (i < length bdy & (noProc ps pn))
      then Some (fst (bdy!i))
      else None)
    else (cmd ps pc))"

consts
  domC :: "SALprogram \<Rightarrow> (pos list)"
primrec
 "domC [] = []"
 "domC (p # ps) = (let (pn, bdy) = p in
    ((if (noProc ps pn) then (map (\<lambda>i. (pn, i)) (upt 0 (length bdy))) else []) @ (delPos (domC ps) pn)))"

consts
  anF:: "SALprogram \<Rightarrow> (pos \<Rightarrow> SALform option)"
primrec
 "anF [] pc = None"
 "anF (p # ps) pc = (let (pn, bdy) = p; (pn', i) = pc in 
    if pn = pn' then
     (if (i < length bdy & (noProc ps pn)) 
      then snd (bdy!i) 
      else None)
    else (anF ps pc))"


constdefs
  step :: "SALprogram \<Rightarrow> SALstate \<Rightarrow> SALstate option"
 "step p \<equiv> (\<lambda>((pn,i), m, e). (case (cmd p (pn,i)) of
    None \<Rightarrow> None 
  | Some ins \<Rightarrow>
     (case ins of 
        SET x n \<Rightarrow> Some ((pn, i + 1), m[x ::= NAT n], e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
      | ADD x y \<Rightarrow> Some ((pn, i + 1), m[x ::= lift (op +) (m x) (m y)], e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
      | SUB x y \<Rightarrow> Some ((pn, i + 1), m[x ::= lift (op -) (m x) (m y)], e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
      | INC x \<Rightarrow> Some ((pn, i + 1), m[x ::= lift (op +) (m x) (NAT 1)], e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
      | JMPEQ x y t \<Rightarrow> (if (\<exists>n n'. m x = NAT n \<and> m y = NAT n') then (if (\<exists>n n'. m x = NAT n \<and> m y = NAT n' \<and> n = n')
          then Some ((pn, i + t), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
          else Some ((pn, i + 1), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>))
        else None)
      | JMPL x y t \<Rightarrow> (if (\<exists>n n'. m x = NAT n \<and> m y = NAT n') then (if (\<exists>n n'. m x = NAT n \<and> m y = NAT n' \<and> n < n')
          then Some ((pn, i + t), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
          else Some ((pn, i + 1), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>))
        else None)
      | JLE x y t \<Rightarrow> (if (\<exists>n n'. m x = NAT n \<and> m y = NAT n') then (if (\<exists>n n'. m x = NAT n \<and> m y = NAT n' \<and> n \<le> n')
          then Some ((pn, i + t), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
          else Some ((pn, i + 1), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>))
        else None)
      | JMPB t \<Rightarrow> Some ((pn, i - t), m, e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
      | JMPI x \<Rightarrow> (case (m x) of ILLEGAL \<Rightarrow> None
                   | NAT n \<Rightarrow> Some ((pn,n),m,e\<lparr>h:= (h e)@[(pn,i)]\<rparr>)
                   | POS r \<Rightarrow> None)
      | CALL x pn' \<Rightarrow> Some ((pn', 0), m[x ::= POS (pn, i + 1)], e \<lparr>h := (h e)@[(pn,i)], cs := (length (h e), m) # (cs e)\<rparr>)
      | RET x \<Rightarrow> (case (m x) of ILLEGAL \<Rightarrow> None | NAT n \<Rightarrow> None | POS ra \<Rightarrow> Some (ra, m, e \<lparr>h := (h e)@[(pn,i)], cs := tl (cs e)\<rparr>))
      | MOV s t \<Rightarrow> (case (m s) 
                    of ILLEGAL \<Rightarrow> None 
                    | NAT sa \<Rightarrow> (case (m t) 
                                 of ILLEGAL \<Rightarrow> None
                                 | NAT ta \<Rightarrow> Some ((pn,i+1),m[ta ::= (m sa)],e \<lparr>h := (h e)@[(pn, i)]\<rparr>)
                                 | POS ra \<Rightarrow> None
                                 )
                    | POS ra \<Rightarrow> None
                    )
      | HALT \<Rightarrow> None
        )))"

constdefs
  effS :: "SALprogram \<Rightarrow> ((pos \<times> tram \<times> env) \<times> (pos \<times> tram \<times> env)) set"
 "effS p \<equiv> {(s, s'). (step p s = Some s')}"


constdefs 
 initialState::"SALstate"
 "initialState \<equiv> ((0,0),\<lambda> a. ILLEGAL,\<lparr>cs = [(0,\<lambda> a. ILLEGAL)], h = []\<rparr>)"

constdefs
  callstate :: "env \<Rightarrow> SALstate"
 "callstate \<equiv> \<lambda> e. (case (cs e) 
                     of [] \<Rightarrow> initialState
                     | (k, m') # css \<Rightarrow> (case css 
                                         of [] \<Rightarrow> initialState
                                         | c'#css' \<Rightarrow> ((h e)!k, m', e\<lparr>cs := css, h := take k (h e)\<rparr>)))" 

constdefs
 callmem :: "env \<Rightarrow> tram" 
"callmem e \<equiv> fst (snd (callstate e))" 


constdefs
 callpc :: "env \<Rightarrow> pos" 
 "callpc e \<equiv> fst (callstate e)"

constdefs
  incA :: "pos \<Rightarrow> pos"
 "incA \<equiv> \<lambda> (pn,i). (pn,Suc i)"

constdefs 
 callenv :: "env \<Rightarrow> env" 
"callenv e \<equiv> snd (snd (callstate e))"


(*<*)
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))" 
(*>*)

end