src/HOL/BCV/Machine.thy

Goal: tuned pris;

(*  Title:      HOL/BCV/Machine.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM

A register machine.
*)

Machine = Types + DFAimpl +

datatype ('a,'b,'c)instr =
    Move nat nat
  | Aload 'a nat | Bload 'b nat | Cload 'c nat
  | Aop nat nat nat | Bop nat nat nat | Cop nat nat nat
  | Comp nat nat nat
  | Halt

consts maxreg :: ('a,'b,'c)instr => nat
       maxregs :: ('a,'b,'c)instr list => nat
primrec
"maxreg(Move m n) = max m n"
"maxreg(Aload x n) = n"
"maxreg(Bload x n) = n"
"maxreg(Cload x n) = n"
"maxreg(Aop i j k) = max i (max j k)"
"maxreg(Bop i j k) = max i (max j k)"
"maxreg(Cop i j k) = max i (max j k)"
"maxreg(Comp i j l) = max i j"
"maxreg Halt = 0"

primrec
"maxregs [] = 0"
"maxregs (x#xs) = max (maxreg x+1) (maxregs xs)"

constdefs

 wt_instr :: ('a,'b,'c)instr => nat => typ list option list => bool
"wt_instr b p T ==
 case T!p of
   None => True
 | Some ts =>
 case b of
   Move i j  => Some(ts[j:=ts!i]) <= T!(p+1)
 | Aload x i => Some(ts[i:=Atyp]) <= T!(p+1)
 | Bload x i => Some(ts[i:=Btyp]) <= T!(p+1)
 | Cload x i => Some(ts[i:=Ctyp]) <= T!(p+1)
 | Aop i j k => ts!i <= Atyp & ts!j <= Atyp & Some(ts[k:=Atyp]) <= T!(p+1)
 | Bop i j k => ts!i <= Btyp & ts!j <= Btyp & Some(ts[k:=Btyp]) <= T!(p+1)
 | Cop i j k => ts!i <= Ctyp & ts!j <= Ctyp & Some(ts[k:=Ctyp]) <= T!(p+1)
 | Comp i j q => (ts!i <= ts!j & ts!j ~= Top | ts!j <= ts!i & ts!i ~= Top) &
                 T!p <= T!(p+1) & T!p <= T!q
 | Halt =>      True"

 stype :: ('a,'b,'c)instr list => typ list set
"stype bs == listsn (maxregs bs) UNIV"

constdefs
 succs :: "('a,'b,'c)instr => nat => nat list"
"succs instr p ==
  case instr of
    Move i j  => [p+1]
  | Aload x i => [p+1]
  | Bload x i => [p+1]
  | Cload x i => [p+1]
  | Aop i j k => [p+1]
  | Bop i j k => [p+1]
  | Cop i j k => [p+1]
  | Comp i j q => [p+1,q]
  | Halt       => []"

 exec :: "('a,'b,'c)instr => typ list => typ list option"
"exec instr ts ==
  case instr of
    Move i j  => Some(ts[j := ts!i])
  | Aload x i => Some(ts[i := Atyp])
  | Bload x i => Some(ts[i := Btyp])
  | Cload x i => Some(ts[i := Ctyp])
  | Aop i j k => if ts!i <= Atyp & ts!j <= Atyp
                 then Some(ts[k := Atyp])
                 else None
  | Bop i j k => if ts!i <= Btyp & ts!j <= Btyp
                 then Some(ts[k := Btyp])
                 else None
  | Cop i j k => if ts!i <= Ctyp & ts!j <= Ctyp
                 then Some(ts[k := Ctyp])
                 else None
  | Comp i j q => if ts!i <= ts!j & ts!j ~= Top | ts!j <= ts!i & ts!i ~= Top
                  then Some ts
                  else None
  | Halt       => Some ts"
(*
  | Bop i j k => if ts!i <= Btyp & ts!j <= Btyp
                 then Some(ts[k := ts!i+ts!j])
                 else None
*)
end