(* Time-stamp: <Tue Jan 08 2008 21:45:42 Stardate: [-29]8784.32 hwloidl>

   Formalisation of the HAM.
*)

header {* The HAM *}

(*<*)
theory VM = Basics + Lang:
(*>*)

subsection {* Values *}

(*
translations 
  "SVal" == "Ref"
*)

subsection {* Stack *}

text {* Stack values must be references, never literals *}

types 
 SVal = Ref
 (* stuff = nat list *)

text {* Frame record, containing return address, the arguments (just above FP),
 local variables (just below FP), and the expression stack as values.
 Note that we abstract over the exact location of args, locals and vals, and
 only model the order within each of these 3 components.
 We don't need an explicit FP or link field, since this is implicit in the
 modelling of the stack as a list of frames.
*}

record Frame =   ret :: LabName
           	 args :: "SVal list"
           	 locals :: "SVal list"
           	 vals :: "SVal list"

types 
 Stack = "Frame list"

syntax emptyStack :: "Stack"
translations "emptyStack" == "[]"

translations
 "Stack" <= (type) "\<lparr>ret :: char list, args :: Ref list, locals :: Ref list, vals :: Ref list\<rparr> list"
 "Frame" <= (type) "\<lparr>ret :: char list, args :: Ref list, locals :: Ref list, vals :: Ref list\<rparr>"

subsection {* Heap *}

text {* The heap is a finite map. Might be worthwhile switching to a more recent
 version of Isabelle to get a better finite map implementation. 
*}

types
 Heap = "Locn \<leadsto>\<^sub>f  HVal"
 LabTable = "LabName \<Rightarrow> Instr list"
 FunTable = "FunName \<Rightarrow> Instr list"
 RuleSet = "nat \<leadsto>\<^sub>f  Instr list"
 RuleTable = "BoxName \<Rightarrow> RuleSet"
 Stream = "int \<Rightarrow> HVal"
 ExnTable = "BoxName \<Rightarrow> int \<Rightarrow> Instr list"

text {* An IO record collects all state info, not recorded in stack or heap.
 These are mainly the wires, but also some pointers into the stack *}

types
 Wire = nat

record IO =  (* ins :: Stream *)
             (* outs :: Stream *)
             (* avb :: "int \<Rightarrow> bool" *)
             bname :: BoxName
             (* bon :: Wire *)
             blocked :: bool
             crp :: nat                (* current rule pointer *)
             rp :: nat                (* rule pointer *)
             inp :: Wire              (* input pointer *)
             mp :: nat                (* match pointer *)

             (* mb :: "SVal list"    match buffer; only needed if no mp is present *)

(* State = Heap \<times> Stack \<times> RuleSet \<times> IO *)
 
translations
 "Stack" <= (type) "\<lparr>ret :: LabName, args :: Ref list, locals :: Ref list, vals :: Ref list\<rparr> list"
 "Heap" <= (type) "nat \<leadsto>\<^sub>f HVal"
 "IO" <= (type) "\<lparr>bname :: BoxName, blocked :: bool, crp :: nat, rp :: nat, inp :: nat, mp :: nat\<rparr>"
 "LabTable" <= (type) "LabName \<Rightarrow> Instr list"
 "FunTable" <= (type) "FunName \<Rightarrow> Instr list"
 "RuleSet" <= (type) "nat \<leadsto>\<^sub>f Instr list"

subsection {* Global Tables *}

text {* We use these global tables that should come out of the compilation of
 Hume code. They never change and therefore don't need to be part of the state. *}

consts
 LabTab :: LabTable
 FunTab :: FunTable
 RuleTab :: RuleTable (* base ruleset *)
 ExnTab :: ExnTable   (* table of exception handlers; exceptions tagged by ints *)

subsection {* Aux definitions *}

(* State = Stack x Env x Heap *)

subsection {* Stack operations *}

text {* The usual operations on a stack. push and pop work on the vals component of the  top frame. *}

constdefs pushS :: "Stack \<Rightarrow> SVal \<Rightarrow> Stack"
"pushS s v == let fr = hd s 
             in 
               \<lparr> ret=(ret fr), args=(args fr), locals=(locals fr), vals=v#(vals fr) \<rparr>#(tl s) 
             "
(*
"push s v == ((hd s)\<lparr> ret=ret fr, args=args fr, locals=locals fr vals=(v#(hd s).vals) \<rparr>)#(tl s)"
*)

text {* Put N dummy values on top of the stack *}

consts pushN :: "nat \<Rightarrow> Stack \<Rightarrow> Stack"
primrec
"pushN 0 s = s"
"pushN (Suc n) s = pushN n 
                    (let fr = hd s
                     in
                     \<lparr> ret=(ret fr), args=(args fr), locals=(locals fr), vals=(Nullref#(vals fr)) \<rparr>#(tl s))"

constdefs popS :: "Stack \<Rightarrow> Stack"
"popS s == let fr = hd s
          in
          \<lparr> ret=(ret fr), args=(args fr), locals=(locals fr), vals=tl(vals fr) \<rparr>#(tl s)"

consts popN :: "nat \<Rightarrow> Stack \<Rightarrow> Stack"
primrec
"popN 0 s = s"
"popN (Suc n) s = popN n (popS s)"

text {* Remove top N elements, but keeping the top stack element *}

consts slideN :: "nat \<Rightarrow> Stack \<Rightarrow> SVal \<Rightarrow> Stack"
primrec
"slideN 0 s v = pushS s v"
"slideN (Suc n) s v = slideN n (((hd s)\<lparr> vals:=tl(vals (hd s)) \<rparr>)#(tl s)) v"

constdefs topS :: "Stack \<Rightarrow> SVal"
"topS s == hd (vals (hd s))"

constdefs takeS :: "nat \<Rightarrow> Stack \<Rightarrow> SVal list"
"takeS n s == take n (vals (hd s))" 

constdefs argN :: "nat \<Rightarrow> Stack \<Rightarrow> SVal"
"argN n s == nth (args (hd s)) n"

constdefs varN :: "nat \<Rightarrow> Stack \<Rightarrow>  SVal"
"varN n s == nth (vals (hd s)) n"

consts setVarN :: "nat \<Rightarrow> Stack \<Rightarrow> Stack"
primrec
"setVarN 0 s = ((hd s)\<lparr> vals:=(topS s)#(tl (vals (hd s))) \<rparr>)#(tl s)"
"setVarN (Suc n) s = ((hd s)\<lparr> vals:=(take n (vals (hd s)))@((topS s)#(drop (Suc n) (vals (hd s)))) \<rparr>)#(tl s)"

consts unpackTuple' :: "Ref list \<Rightarrow> nat \<Rightarrow> Stack \<Rightarrow> Stack"
primrec
"unpackTuple' [] m s = s"
"unpackTuple' (x#xs) m s = (unpackTuple' xs m (pushS s x))"

constdefs unpackTuple :: "nat \<Rightarrow> Ref list \<Rightarrow> Stack \<Rightarrow> Stack"
"unpackTuple m xs s == unpackTuple' xs m s"

(*
constdefs unpackCon :: "nat \<Rightarrow> nat \<Rightarrow> Ref list \<Rightarrow> Stack \<Rightarrow> Stack"
"unpackCon m xs s == unpackCon' m m xs s"

constdefs unpackCon' :: "nat \<Rightarrow> nat \<Rightarrow> Ref list \<Rightarrow> Stack \<Rightarrow> Stack"
primrec
"unpackCon' 0 m xs s == s"
"unpackCon' n m (x#xs) s == unpackTuple (n-1) m xs (pushS s x)"
*)

subsection {* Basic heap operations *}

constdefs mkBool :: "Heap \<Rightarrow> Locn \<Rightarrow> bool \<Rightarrow> Heap"
"mkBool h l b == h(l \<mapsto>\<^sub>f (B b))"

constdefs mkInt :: "Heap \<Rightarrow> Locn \<Rightarrow> int \<Rightarrow> Heap"
"mkInt h l i == h(l \<mapsto>\<^sub>f (I i))"
(*
constdefs mkChar :: "Heap \<Rightarrow> Locn \<Rightarrow> string \<Rightarrow> Heap"
"mkChar h l c == h(l \<mapsto>\<^sub>f (Y c))"

constdefs mkString :: "Heap \<Rightarrow> Locn \<Rightarrow> string \<Rightarrow> Heap"
"mkString h l s == h(l \<mapsto>\<^sub>f (S s))"

constdefs mkTuple :: "Heap \<Rightarrow> Locn \<Rightarrow> int \<Rightarrow> SVal list \<Rightarrow> Heap"
"mkTuple h l i xs == h(l \<mapsto>\<^sub>f (T i xs))"
*)

constdefs mkCon :: "ConName \<Rightarrow> Heap \<Rightarrow> Locn \<Rightarrow> SVal list \<Rightarrow> Heap"
"mkCon c h l xs == h(l \<mapsto>\<^sub>f (C c (int (length xs)) xs))"

(*
constdefs mkFun :: "Heap \<Rightarrow> Locn \<Rightarrow> LabName \<Rightarrow> int \<Rightarrow> int  \<Rightarrow> SVal list \<Rightarrow> Heap"
"mkFun h l f m n xs == h(l \<mapsto>\<^sub>f (F f m n xs))"

constdefs mkExn :: "Heap \<Rightarrow> Locn \<Rightarrow> LabName \<Rightarrow> int \<Rightarrow> Heap"
"mkExn h l f i == h(l \<mapsto>\<^sub>f (X f i))"

constdefs mkNone :: "Heap \<Rightarrow> Locn \<Rightarrow> Heap"
"mkNone h l == h(l \<mapsto>\<^sub>f N)"
*)

consts mkHVal :: "HVal \<Rightarrow> Heap \<Rightarrow> Locn \<Rightarrow> Heap"
primrec
 "mkHVal (I x) h l = h(l \<mapsto>\<^sub>f (I x))"
 "mkHVal (B x) h l = h(l \<mapsto>\<^sub>f (B x))"
 "mkHVal (Y x) h l = h(l \<mapsto>\<^sub>f (Y x))"
 "mkHVal (S x) h l = h(l \<mapsto>\<^sub>f (S x))"
 "mkHVal (R x) h l = h(l \<mapsto>\<^sub>f (R x))"
 "mkHVal (T i xs) h l = h(l \<mapsto>\<^sub>f (T i xs))"
 "mkHVal (C i j xs) h l = h(l \<mapsto>\<^sub>f (C i j xs))"

(*
 "mkHVal (F f m n xs) h l = h(l \<mapsto>\<^sub>f (F f m n xs))"
 "mkHVal (X f i) h l = h(l \<mapsto>\<^sub>f (X f i))"
 "mkHVal (N) h l = h(l \<mapsto>\<^sub>f (N))"
*)

constdefs newFrame :: "Stack \<Rightarrow> LabName \<Rightarrow> LabName \<Rightarrow> Stack"
"newFrame s l f == \<lparr> ret=l, args=[], locals=[], vals=[] \<rparr>#s"

constdefs oldFrame :: "Stack \<Rightarrow> Stack"
"oldFrame s == pushS (tl s) (topS s)"

(* TODO: check this with draft paper *)
constdefs modifyFrame :: "Stack \<Rightarrow> IO \<Rightarrow> LabName \<Rightarrow> LabName \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (Stack \<times> IO)"
"modifyFrame s io c f n d z == (let s' = (take ((length s) - d) s)
                                in ( ((hd s')\<lparr> vals := vals (hd s) \<rparr>)#(tl s')  , 
                                     io\<lparr> rp := 0 \<rparr>))"

subsection {* Manipulating rule-pointer and other stuff in the IO record *}

(*
constdefs writeW :: "IO \<Rightarrow> int \<Rightarrow> HVal \<Rightarrow> IO"
"writeW io n x == io\<lparr> ins := (ins io)(n := x) \<rparr>"

constdefs readW :: "IO \<Rightarrow> int \<Rightarrow> HVal"
"readW io n == ((ins io) n)"
*)

constdefs nextRule :: "RuleSet \<Rightarrow> IO \<Rightarrow> Instr list"
"nextRule rs io == case (fmap_lookup rs (rp io)) of
                      None \<Rightarrow> []
                    | (Some cs) \<Rightarrow> cs"

constdefs currentRuleIdx :: "IO \<Rightarrow> nat"
"currentRuleIdx io == crp io"

constdefs incRP :: "RuleSet \<Rightarrow> IO \<Rightarrow> IO"
"incRP rs io == if ((rp io)+1 \<in> fmap_dom rs)
                     then io\<lparr> crp := (rp io), rp := (rp io)+1 \<rparr>
                     else io\<lparr> crp := (rp io), rp := 0 \<rparr>"

(* TODO: model reordering as 2 queues in the IO record *)
consts reorderRules :: "IO \<Rightarrow> IO"

constdefs currArg :: "Stack \<Rightarrow> IO \<Rightarrow> SVal"
"currArg s io == nth (args (hd s)) (mp io)"

subsection {* System *}

text {*
Here is the design rationale for the components in the HAM on system level.
The entire system is modelled as a triple 
\[
 (bs,bm,wm)
\]
where
\begin{itemize}
 \item $bs$ is a list of box names, which still need to be processed in the
  current superstep (one round of executing, if possible, every box);
 \item $bm$ a mapping (as total function for ease of use) of boxnames to 
  box states
 \item $wm$ a mapping of wirenames to wire states.
\end{itemize}

Wire names are uniquely generated out of box names and wire indices, 
using the function $\mbox{wname}$.

\paragraph{BoxState}:
Since we will use a small-step semantics, the state of a box contains the
code that still has to be executed. The other components are of course,
stack and heap, and the IO record. The latter only contains a few pointers, 
mainly those neeeded for fair matching and for doing parameter matching.

\paragraph{Wiring}:
The wiring matches the $n$-th output wire of the current box, to a pair
$(b,w)$ for box name and input wire, to which it is connected.

\paragraph{Box}:
The static information of a Box consists of its RuleSet and the Wiring.

Note that the static components, $\mbox{BoxTab}$, $\mbox{Box}$, $\mbox{Wiring}$ can be generated automatically during compilation.

*}


types
 Wiring = "Wire => (BName \<times> Wire)"
 Box = "(RuleSet \<times> Wiring)"
 WState = "HVal option"
 BState = "Stack \<times> Heap \<times> IO \<times> Instr list"
 System = "BName list \<times> (BName \<Rightarrow> BState) \<times> (WName \<Rightarrow> WState)" 

consts BoxTab :: "BName \<leadsto>\<^sub>f Box"

translations 
 "BState" <= (type) "(Stack \<times> Heap \<times> IO \<times> Instr list)"
 "System" <= (type) "(BName list \<times> (BName \<Rightarrow> Stack \<times> Heap \<times> IO \<times> Instr list) \<times> (WName \<Rightarrow> HVal option))"

text {*
NeededIn maps each rule in the ruleset to the set of needed inputs, ie. a set of
wires on which input must be available for the rule to fire.
NeededOut maps each rule in the ruleset to the set of needed inputs, ie. a set of
wires to which this rule will write.
*}

consts NeededIn :: "RuleSet \<Rightarrow> Wire \<Rightarrow> Wire set"
consts NeededOut :: "RuleSet \<Rightarrow> Wire \<Rightarrow> Wire set"


consts theBx :: "Box option \<Rightarrow> Box"
primrec 
 "theBx (Some b) = b"

syntax link ::  "BName \<Rightarrow> Wire \<Rightarrow> (BName \<times> Wire)"
translations "link b w" == "(snd (theBx (fmap_lookup BoxTab b))) w"

text {*
Generates a unique name for a wire based on the box names and wire indices of both ends.
*}
             
(* needs to be commutative *)
constdefs wname :: "BName \<Rightarrow> Wire \<Rightarrow> WName"
"wname b w == case b of
              BN str \<Rightarrow> case (link b w) of 
                          (b',w') \<Rightarrow> case b' of 
                                       BN  str' \<Rightarrow> WN (str@str')"

text {*
Check availability of input data on an input wire.
*}

constdefs avb :: "(WName \<Rightarrow> WState) \<Rightarrow> WName \<Rightarrow> bool"
"avb wm w == case (wm w) of
              None \<Rightarrow> False
             | (Some x) \<Rightarrow> True"

constdefs avb' :: "IO \<Rightarrow> Wire \<Rightarrow> System \<Rightarrow> bool"
"avb' io w sys == (case ((thd3 sys) (wname (bname io) w)) of
                        None \<Rightarrow> False
                      | (Some x) \<Rightarrow> True)"

constdefs wval :: "IO \<Rightarrow> Wire \<Rightarrow> System \<Rightarrow> HVal"
"wval io w sys == (case ((thd3 sys) (wname (bname io) w)) of
                        None \<Rightarrow> R Nullref
                      | (Some x) \<Rightarrow> x)"

text {*
This predicate says that all output wires, needed by the current rule, are free.
This could be merged with restartable!

Note that this predicate specifies what needs to be checked in CheckOutputs.
*}

constdefs outputable :: "IO \<Rightarrow> (WName \<Rightarrow> WState) \<Rightarrow> bool"
"outputable io wm == (\<forall> w. w \<in> (NeededOut (RuleTab (bname io)) (currentRuleIdx io)) \<longrightarrow> avb wm (wname (bname io) w))"

constdefs blockBox :: "IO \<Rightarrow> IO"
"blockBox io == io\<lparr> blocked := True \<rparr>"

text {*
A box is runnable, if it is not marked as blocked, is not finished already ie. still has some code in its state, and if it has at least 1 rule for which inputs are available on all needed input wires.

Note that this predicate specifies what needs to be checked in the main scheduling loop.
*}

constdefs runnable :: "System \<Rightarrow> BState \<Rightarrow> bool"
"runnable sy b == (case b of
                   (s,h,io,cs) => (\<not>(blocked io) \<and> \<not>(null cs) \<and>
                      (\<exists> r. r \<in> fmap_dom (RuleTab (bname io)) \<and> 
                       (\<forall> w. w \<in> (NeededIn (RuleTab (bname io)) r) \<longrightarrow> avb' io w sy))))"

(* \<and>        (\<forall> w. w \<in> (NeededOut (RuleTab (bname io)) r) \<longrightarrow> avb' io w sy))))"*)

text {* 
A box is restartable if it is blocked now and all output wires are free.
*}

constdefs restartable :: "System \<Rightarrow>  BState \<Rightarrow> bool"
"restartable sy b == (case b of
                       (s,h,io,cs) => ((blocked io) \<and>
                          (\<forall> w. w \<in> (NeededOut (RuleTab (bname io)) (currentRuleIdx io)) \<longrightarrow> (avb' io w sy))))"

(*<*)
(* subsection {* Resources *} 

types
 Wiring = "Wire => (BName \<times> Wire)"
 Box = "(Instr list \<times> Wiring)"
 BoxState = "(BName \<times> Stack \<times> Heap \<times> RuleSet \<times> IO)"
 System = "BoxState set"
*)

(* This version is used only for the small-step semantics *)
(*
types
 SSWiring = "Wire => (BName \<times> Wire)"
 SSBox = "(Instr list \<times> Wiring)"
 SSBoxState = "(BName \<times> Stack \<times> Heap \<times> RuleSet \<times> IO \<times> Instr list)"
 SSSystem = "BoxState set"
*)

end
(*>*)