theory SALSyntax = Main:

types
  val = nat
  loc = nat
  pname = nat
  pos = "pname \<times> nat"

datatype
  instr =
    SET loc val | 
    ADD loc loc |
    SUB loc loc |
    INC loc |
    JMPEQ loc loc nat |
    JMPL loc loc nat |
    JLE loc loc nat |
    JMPB nat |
    JMPI loc |
    CALL loc pname |
    RET loc |
    MOV loc loc | 
    HALT

consts
  delPos :: "pos list \<Rightarrow> pname \<Rightarrow> pos list"
primrec
 "delPos [] pn = []"
 "delPos (p # ps) pn = (let (pn', i)=p in (if pn' = pn then delPos ps pn else p # (delPos ps pn)))"

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)

end