Theory SafeHeap

(*  Title:      Safe Heap
    Author:     Ricardo Peña and Javier de Dios
    Copyright:  March 2008, Universidad Complutense de Madrid
*)

header {* Normal form values and heap *}

theory SafeHeap
imports Main 
begin

types 
  Location = nat
  Constructor = string
  FunName = string

-- "Normal form values"
datatype Val = Loc Location | IntT int | BoolT bool


-- "Destructions of datatype val" 
consts the_IntT :: "Val => int"
 primrec
   "the_IntT (IntT i) = i"

consts the_BoolT :: "Val => bool"
  primrec
    "the_BoolT (BoolT b) = b"

-- "check if is constant bool"
constdefs isBool :: "Val => bool"
  "isBool v ≡  (case v of (BoolT _ ) => True
                       | _ => False )"

text{* A heap is a partial mapping from locations to cells. But, as it is
split into regions, the mapping tells also the region where the cell lives.
The second component is the highest live region $k$. A consistent heap
$(h,k)$ has cells only in regions $0\ldots k$. 
*} 

types
  Cell = "Constructor × Val list"
  Region = nat
  HeapMap   = "Location \<rightharpoonup> (Region × Cell)"
  Heap = "HeapMap × nat"

consts
  restrictToRegion :: "Heap => Region => Heap"   (infix "\<down>" 110) 

primrec
  "(h,k) \<down> k0 = (let A = { p .  p ∈ dom h & fst (the (h p)) <= k0} 
                       in (h |` A,k0))" 

definition
  rangeHeap :: "HeapMap => Val set" where
  "rangeHeap h = {v. EX p j C vn. h p = Some (j,C,vn) ∧ v ∈ set vn}"

definition
  fresh :: "Location => HeapMap  => bool" where
  "fresh p h = (p ∉ dom h ∧ (Loc p) ∉ rangeHeap h)"

definition domLoc :: "HeapMap => Val set" where
 "domLoc h = {l. EX p. p ∈ dom h ∧ l = Loc p}"

declare rangeHeap_def [simp del]
declare fresh_def [simp del]
declare domLoc_def [simp del]



constdefs
  getFresh :: "HeapMap  => Location"
  "getFresh h ≡ SOME b. fresh b h"

 
constdefs
   self :: string  -- "this identifies the topmost region referenced in a function body"
  "self ≡ ''self''"

text{* The constructor table tells, for each constructor, the number of
arguments and a description of each one. The second nat gives the
alternative $0..n-1$ corresponding to this constructor in every {\bf case} of its
type *}

datatype ArgType = IntArg | BoolArg | NonRecursive | Recursive


types
  ConstructorTableType = "(Constructor × (nat × nat × ArgType list)) list"
  ConstructorTableFun = "Constructor \<rightharpoonup> (nat × nat × ArgType list)"



text{* This is the constructor table of the Safe expressions semantics. 
It is assumed to be a constant which somebody else will provide. 
It is used in the semantic function 'copy'*}

consts
    ConstructorTable :: ConstructorTableFun

(* Operations on cells *)
constdefs getConstructorCell :: "Cell => Constructor"
"getConstructorCell c ≡ fst c"

constdefs getValuesCell :: "Cell => Val list"
"getValuesCell c ≡ snd c"

constdefs getCell :: "Heap => Location => Cell"
"getCell h l ≡ snd (the ((fst h) l))"

constdefs getRegion :: "Heap => Location => Region"
"getRegion h l ≡ fst (the ((fst h) l))"

constdefs domHeap :: "Heap => Location set"
"domHeap h ≡ dom (fst h)"

constdefs isNonBasicValue :: "ArgType => bool"
"isNonBasicValue a == (a = NonRecursive) ∨ (a = Recursive)"

constdefs isRecursive :: "ArgType => bool"
"isRecursive a == (a = Recursive)"

consts 
 theLocation :: "Val => Location"
primrec "theLocation (Loc l) = l" 


constdefs
"getArgType C  ≡ snd (snd (the (ConstructorTable C)))"

constdefs getRecursiveValuesCell :: "Cell => Location set"
"getRecursiveValuesCell c == set (map (theLocation o snd) 
                             (filter (isRecursive o fst) (zip (getArgType (getConstructorCell c)) (getValuesCell c))))"

constdefs recDescendants :: "Location => Heap => Location set"
"recDescendants l h ≡ case ((fst h) l) of Some c => getRecursiveValuesCell (snd c)
                                        | None => {}"

constdefs getNonBasicValuesCell :: "Cell => Location set"
"getNonBasicValuesCell c == set (map (theLocation o snd) 
                           (filter (isNonBasicValue o fst) (zip (getArgType (getConstructorCell c)) (getValuesCell c))))"


constdefs descendants :: "Location => Heap => Location set"
"descendants l h ≡ case ((fst h) l) of Some c => getNonBasicValuesCell (snd c)
                                        | None => {}"


constdefs isConstant :: "Val => bool"
 "isConstant v ≡ (case v of (IntT _)  => True
                         | (BoolT _)  => True
                         | _          => False)"
end