(* Resource Algebra for the HAM.
   Collect everthing about resources here to make it easily replaceable.
   tickExp remains undefined in GRUMPY.thy; used in D17 on program logic
*)

header {* Resource Algebra *}

(*<*)
theory ResAlg = Basics + Grail:
(*>*)

text {* This file defines a resource algebra to be used by the HAM Semantics.
 The main function in here is the \verb+tick+ function, which is used in the
 semantics. The representation of the resources is up to this module. 

 At the moment this instance is a very naive clock counter. It also maintains 
 info on the number of function calls, method invocations and max invoke depths.
 All this is MRG heritage and should be replaced by more accurate stack size info.
*}

record Rescomp = clock :: int        -- {* execution time *}
                 callc :: int        -- {* call counter *}
                 invkc :: int        -- {* invoke counter *}
                 invkdpth :: nat     -- {* max invoke depth *}

text {*
To add up resource consumption, we use two combinators over resource tuples.
*}

translations 
 "Rescomp" <= (type) "\<lparr> clock :: int, callc :: int, invkc :: int, invkdpth :: nat \<rparr>"

constdefs Rescomp_plus:: "Rescomp \<Rightarrow> Rescomp \<Rightarrow> Rescomp"  (infixr "\<oplus>" 0)
"Rescomp_plus p1 p2 == \<lparr>clock = clock p1 + clock p2,
                     callc = callc p1 + callc p2,
                     invkc = invkc p1 + invkc p2,
                     invkdpth = invkdpth p1 + invkdpth p2\<rparr>"

constdefs Rescomp_cup :: "Rescomp \<Rightarrow> Rescomp \<Rightarrow> Rescomp" (infixr "\<smile>" 0)
"Rescomp_cup p1 p2 == \<lparr>clock = clock p1 + clock p2,
                    callc = callc p1 + callc p2,
                    invkc = invkc p1 + invkc p2,
                    invkdpth = max (invkdpth p1) (invkdpth p2)\<rparr>" 
(*<*)
declare Rescomp_plus_def [simp add]
declare Rescomp_cup_def [simp add]
(*>*)

text {* Some syntax for creating and manipulating resource tuples. *}

syntax mkRescomp:: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> Rescomp"
translations
"mkRescomp C CC IC ID" == "\<lparr>clock = C, callc = CC, invkc = IC, invkdpth = ID\<rparr>"

syntax mkRescomp_HWL :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> nat \<Rightarrow> Rescomp" ("\<langle>_ _ _ _\<rangle>")
translations
"\<langle>C CC IC ID\<rangle>" == "\<lparr>Rescomp.clock = C, callc = CC, invkc = IC, invkdpth = ID\<rparr>"

syntax tkn ::"int \<Rightarrow> Rescomp \<Rightarrow> Rescomp"
translations
"tkn n p" == "((mkRescomp n 0 0 0) \<smile> p)"

syntax tk::"Rescomp \<Rightarrow> Rescomp"
translations
"tk p" == "tkn 1 p"

syntax tkcall::"Rescomp \<Rightarrow> Rescomp"
translations
"tkcall p" == "((mkRescomp 1 1 0 0) \<smile> p)"

syntax tickRo::"Rescomp"
translations
"tickRo" == "mkRescomp 1 0 0 0"

text {* 
  We define the resources for a fixed set of resources here.
  This just shows the pattern of plugging in resoures. Ultimately,
  it should be a resource algebra that can be instantiated for
  different resources. For now I map tickExp always to a constant.
*}

syntax tickRox :: Rescomp
translations "tickRox" == "\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr>"

text {*
 ResConst defines program points where costs can be attached. Must match the
 data type definition in space-analysis/Costs.hs. Should be a parameter
 to the pickx function below.
*}

datatype ResPos = PBefore | PAfter (* | PInbetween *)

datatype Res3Pos = P3Before | P3Middle | P3After

datatype LetKind = GhostLet | TrueLet

datatype AppKind = TailApp | ExactApp | OverApp | UnderApp

datatype CaseKind = ExprCase "int option" | BoxCase "int option" | FunCase "int option"

datatype ResConst =  (* The parameters for all cost kinds *)
    RCpvar  int                    (* pushVar: pushing a variable on top of the stack, Integer tells FrameDepth*)
  | RCmk    Type (*HoVal*)         (* making a value of a certain type.*)
  (* | RCuop   UnaryOp Type *)
  | RCbop   "int => int => int" Type Type
  | RCcon   ConName bool                  (* Full Constructor Info (not rich), Construction=True/Destruction or Matching=False, Diamond Option signals a truly destructive match (not supported by HUME, but supported by this analysis*)
  | RCclcr  bool "Type list"              (* the cost for _creating_  closures storing arguments $2; "fun"-closures =True and "chain"-closures =False*)
  | RCcloh  bool "Type list" ResPos int   (* overhead for _executing_ closures storing arguments $2; "fun"-closures =True and "chain"-closures =False. The integer contains the number of all proper functions contained in the examined program. NOTE: This might be problematic for a compositonal analysis!*)
  | RCapp   bool VarName "Type list" ResPos AppKind int (* Function application 1)fun=true/closure 2) funid (unless closure) 3)argument types 4)Position 5)Either TailApp, OverApp oder ExactApp, but is NEVER UnderApp (see RCclcr instead). TailApp only uses PBefore! The FunId for true func calls can be used to insert the cost for built-in functions (like 'mod', etc.)*)
  | RClet   LetKind int Res3Pos           (* Cost of a multiple let-binding of k variables. EACH position is used once per let, not per variable. The "middle"-position is after the last binding and before the in-expression*)
  | RClvar  LetKind Type                  (* Cost of each let-variable binding (of given type) AFTER the defining body of EACH variable has been processed*)
  | RCif    bool ResPos                   (* Conditional, Bool signifies concerned branch*)
  | RCmatch CaseKind ResPos               (* General match bookkeeping, before the whole case and afterwards (ie after return from the branch-expression)*)
  | RCmrule CaseKind Res3Pos              (* Particular cost for each match rule. Pos3: PBefore: pattern, PMiddle= after unsuccessful pattern; PAfter=after successful match (ie next is the evaluation of the matrule expression) When P3After is used, also all the freed potential from the pattern match is added in at this point by the inference..*)
  (* *** CONTINUE NEXT LINE: Should P3Middle and P3After apply to constructors having 0 arguments???*)
  | RCpattern Pattern "Res3Pos option"    (* Cost to attempt a pattern match. ResPostition is only meaningful for pattern that have subpatterns themselves, such as Constructors: P3Before=matching constructor, P3Middle=before matching suppatterns, P3After=after matching suppatterms. Note that this cost is generally paid regardless of success, and also affects subsequent match rules. However, P3Middle and P3After do not apply if all subpatterns are irrefutable (only P3Before applies in that case)*)
  | RCraise  "string"  ResPos             (* Cost of raising a certain exception, before and after evaluation of the raiseexpression.*)
  | RCwithin "string"  ResPos             (* Cost when entering/exiting the scope of withon of a certain type. Do not include RCraise, this is used separately.*)
  | RCUndef

consts typsize :: "Type => int"
primrec
"typsize IntTy = 2"
"typsize BoolTy = 2"
"typsize (FunTy ty1 ty2) = 2"
"typsize (ConTy c n xs) = (2+(int n))" (* TODO: fix this *)

(* see space-analysis/Costs.hs *)
consts costsHeap :: "ResConst => int"
primrec
"costsHeap (RCpvar x)           = 0"
"costsHeap (RCmk ty)            = typsize ty"
"costsHeap (RCbop f o1ty o2ty)  = typsize IntTy"
"costsHeap (RCcon ci cd)        = 99 " (* TODO: fix this *)
"costsHeap (RCclcr chain ats)   = 0"  (* TODO: fix this *)
"costsHeap (RCcloh b tys rp n)  = 0"  (* there is no overhead for executing a closure *)
"costsHeap (RCapp b vn tys rp ak n) =  0"  (* there is no overhead for applying a function *)
"costsHeap (RClet x y z)        = 0"  (* there is no overhead for let-expressions in terms of heap space *)
"costsHeap (RClvar lk ty )      = 0"  (* there is no overhead for let-expressions in terms of heap space *)
"costsHeap (RCif b rp)          = 0"  (* the conditional has no intrinsic heap costs whatsoever *)
"costsHeap (RCmatch ck r3p)     = 0"  (* there is no overhead for case expressions in terms of heap space *)
"costsHeap (RCmrule ck r3p)     = 0"  (* no costs for each mrule in terms of heap *)
"costsHeap (RCpattern x r3p)    = 0"  (* no heap costs for pattern matching *)
"costsHeap (RCraise x rp)       = 0"  (* no heap costs for raising an exception *)
"costsHeap (RCwithin x rp)      = 0"  (* no heap cost overhead for entering a within scope *)


text {*
 The @{text tickExp} function assigns (exec time-, stack space-, heap space-) costs
 to language constructs. Some values might depend on env values, therefore they
 are parameterised with env etc.
 This should match the costs table of the space-analysis.
*}

consts tickExp :: "Exp \<Rightarrow> ResConst \<Rightarrow> Rescomp"
(* "tickExp e E h p == tickRox" *) (* \<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr>" *)
(*
primrec 
"tickExp (ValueExp i) E h p =      (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (VarExp x) E h p =        (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (ConstrExp c xs) E h p =  (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (PrimBin f x y) E h p =   (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)" 
"tickExp (IfExp x e1 e2) E h p =   (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (LetExp x e1 e2) E h p =  (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (CallFunExp f xs) E h p = (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (CallVarExp x xs) E h p = (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
"tickExp (CaseOneExp x b e e') E h p =    (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)"
*)
(* "tickExp (CaseExp x bs) E h p =    (\<lparr> clock=1, callc=0, invkc=0, invkdpth=0 \<rparr> \<smile> p)" *)
(*
text {*
The main cost function for the HAM; it should model the costs based on assembler code expansions of native codegen, and I still need to check these to produce accurate numbers. For now all costs are mapped to a constants *}

consts tick :: "Instr \<Rightarrow> Stack \<Rightarrow> Heap \<Rightarrow> Rescomp \<Rightarrow> Rescomp"
primrec
"tick (MkBool b) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MkInt i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MkTuple i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Push i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Pop i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Slide i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Copy i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (CopyArg i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (CreateFrame i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (PushVar i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (PushVarF d i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MakeVar i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Goto lbl) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (If lbl) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Call f) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Return lbl) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (CallPrim1 f) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (CallPrim2 f ) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (StartMatches) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MatchRule) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MatchNone) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MatchAvailable) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MatchBool b) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MatchInt i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (MatchTuple i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Unpack) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Reorder) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (CheckOutputs) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (CopyInput i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Consume i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Write i) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Input) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Output) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
"tick (Schedule) s h p = \<lparr>clock = 1, callc = 0, invkc = 0, invkdpth = 0\<rparr>"
*)
end