(* Time-stamp: <Wed Dec 13 2006 16:26:04 Stardate: [-29]6828.21 hwloidl>

   HAM language.
*)

header {* The HAM Language *}

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

text {*
Simplifications over the HAM lang made here:
\begin{itemize}
\item only one Int type
\item no floats
\item no strings
\item no exact values for Input/Output, but correct resource consumption
\end{itemize}

On this level we don't have functions any more, just labels.

*}

datatype Instr =
 (* Expr Lang *)
   MkBool bool
 | MkChar string
 | MkString string
 | MkInt int
 | MkTuple int
 | MkCon int int
 | MkFun LabName int int
 (* | MkExn LabName int *)
 | MkNone
 | Push int
 | Pop int
 | Slide int
 | Copy int
 | CopyArg int
 | CreateFrame int
 | PushVar int
 | PushVarF int int
 | MakeVar int
 | Goto LabName
 | IfX LabName
 | Call LabName
 | TailCall LabName nat nat nat
 | CallVar  int
 | CallVarF int int
 | Return
 | CallPrim1 "Ref => Ref"
 | CallPrim2 "Ref => Ref => Ref"
 (* Box Lang *)  
 | StartMatches
 | MatchRule
 | MatchNone
 | MatchAvailable
 | MatchBool bool
 | MatchChar string
 | MatchString string
 | MatchInt int
 | MatchTuple int
 | MatchCon int int
 | MatchExn int
 | Unpack
 | Reorder
 | CopyInput int
 | CheckOutputs
 | Consume int
 | MaybeConsume int
 | Write int
 | Input
 | Output
 | Raise LabName int
 | Schedule

(* free labels *)
consts fLi :: "Instr \<Rightarrow> LabName set"
primrec 
"fLi (Goto l)  = {l}"
"fLi (IfX l)    = {l}"
"fLi (Return) = {}"
"fLi (Call f) = {f}"
"fLi (CallVar i) = {}"
"fLi (CallVarF i j) = {}"
"fLi (MkBool b) = {}"
"fLi (MkChar x) = {}"
"fLi (MkString x) = {}"
"fLi (MkInt i) = {}"
"fLi (MkTuple i) = {}"
"fLi (MkCon m n) = {}"
"fLi (MkFun f x y) = {f}"
(* "fLi (MkExn f m) = {f}"*)
"fLi (Push i) = {}"
"fLi (Pop i) = {}"
"fLi (Slide i) = {}"
"fLi (Copy i) = {}"
"fLi (CopyArg i) = {}"
"fLi (CreateFrame i) = {}"
"fLi (PushVar i) = {}"
"fLi (PushVarF i j) = {}"
"fLi (MakeVar i) = {}"
"fLi (CallPrim1 f) = {}"
"fLi (CallPrim2 f) = {}"
"fLi (StartMatches) = {}"
"fLi (MatchRule) = {}"
"fLi (MatchNone) = {}"
"fLi (MatchAvailable) = {}"
"fLi (MatchBool b) = {}"
"fLi (MatchChar x) = {}"
"fLi (MatchString x) = {}"
"fLi (MatchInt i) = {}"
"fLi (MatchTuple i) = {}"
"fLi (MatchCon i j) = {}"
"fLi (MatchExn i) = {}"
"fLi (Unpack) = {}"
"fLi (Reorder) = {}"
"fLi (CopyInput i) = {}"
"fLi (Consume i) = {}"
"fLi (Write i) = {}"
"fLi (Schedule) = {}"
"fLi (Input) = {}"
"fLi (Output) = {}"
"fLi (Raise f i) = {f}"

text {*
This function extracts all free labels from a list of instructions.
It is used in the translation function from Hume to HAM.
*}

constdefs fL :: "Instr list \<Rightarrow> LabName set"
"fL == Union o set o (map fLi)"

end