(* Time-stamp: <Mon May 05 2008 22:05:37 Stardate: [-29]9374.18 hwloidl>

   Basic definition and memory model for Core Hume.
*)

header {* Basics for Core Hume *}
(*<*)
theory Basics = Finmap:
(*>*)

subsection {* Basic definitions *}

text {* Different kind of names as a syntax level distinction *}

datatype  BoxName = BN string  --  {* names of boxes *}
datatype  WirName = WN string  --  {* names of wires *}

datatype  VarName = VN string
datatype  LabName = LN string

datatype FunName = FN string  -- {* names of functions *}
datatype ConName = CN string  -- {* names of constructors *}

(*<*)
lemma cl: "(VN ''a'') = (VN ''b'') \<Longrightarrow> P" 
apply simp
done
(*>*)

subsection {* Locations and references *}
text {*
  We model locations as natural numbers.  This is somewhat concrete, but 
  avoids constructing an abstract type or assuming the properties we expect.
  References are either null or locations. *}

types Locn = nat
datatype Ref = Nullref | Ref Locn  

text {* We define a partial projection on non-null locations. *}
consts theloc :: "Ref \<Rightarrow> Locn"
primrec "theloc (Ref a) = a"

text {* Given a finite set of locations, we can always find a new fresh one.*}
constdefs freshloc  :: "Locn set \<Rightarrow> Locn"         
 "freshloc L == Suc (Max (insert 0 L))" 

lemma freshloc: "finite L \<Longrightarrow> freshloc L \<notin> L"
(*<*)
  apply (simp add: freshloc_def)
  apply (case_tac "L={}")
   apply simp
   apply auto
   apply (frule Max_ge)
   defer 1
   apply auto
done
(*>*)

subsection {* Values *}

text {* We define these here to use a shallow embedding of primitives *}

text {* heap values in a higher-order heap i.e. with closures *}

datatype
 HoVal = BOTTOM
      | I "int"  -- {* boxed integer values *}
      | B "bool" 
      | R "Ref" 
      | C "ConName" "Ref list" 
      | X "FunName" "nat" "Ref list"   -- {* closure *}

text {* syntax for undefined *}

syntax "_bottom"     :: "HoVal"		("\<bottom>" 1000)
translations "_bottom" == "BOTTOM"

syntax nochar :: "string"
translations "nochar" == "''X''"

syntax nostring :: "string"
translations "nostring" == "''XXX''"


consts
  theInt      :: "HoVal \<Rightarrow> int"
  theBool     :: "HoVal \<Rightarrow> bool"
  theRef      :: "HoVal \<Rightarrow> Ref"
  theConName  :: "HoVal \<Rightarrow> ConName"
  theConArgs  :: "HoVal \<Rightarrow> Ref list"
  theFunName  :: "HoVal \<Rightarrow> FunName"
  theFunArgs  :: "HoVal \<Rightarrow> Ref list"

primrec "theInt  (I i) = i"
primrec "theBool (B b) = b"
primrec "theRef  (R r) = r"
primrec "theConName  (C c xs) =  c"
primrec "theConArgs  (C c xs) =  xs"
primrec "theFunName  (X f n xs) =  f"
primrec "theFunArgs  (X f n xs) =  xs"

(*
text {* These are HAM level heap values; UNUSED in GRUMPY *}

datatype
 HAMVal = I "int"  -- {* boxed integer values *}
      | B "bool" 
      | Y "string" 
      | S "string" 
      | R "Ref" 
      | T "int" "Ref list" 
      | C "int" "int" "Ref list" 
      | F "LabName" "int" "int" "Ref list" 
      | X "LabName" "int" 
      | N

text {* GRUMPY-level heap values *}

datatype
 HVal = I "int"  -- {* boxed integer values *}
      | B "bool" 
      | R "Ref" 
      | C "ConName" "int" "Ref list" 

consts theHVal :: "HVal option \<Rightarrow> HVal"
primrec 
 "theHVal (Some x) = x"

consts
  theint :: "HVal \<Rightarrow> int"
  thebool :: "HVal \<Rightarrow> bool"
  theref :: "HVal \<Rightarrow> Ref"
primrec "theint  (I i) = i"
primrec "thebool (B b) = b"
primrec "theref  (R r) = r"

*)

(*
syntax fst3 :: "('a \<times> 'b \<times> 'c) => 'a"
translations  "fst3 (x,_,_)" == "x"

syntax snd3 :: "('a \<times> 'b \<times> 'c) => 'b"
translations  "snd3 (_,y,_)" == "y"

syntax thd3 :: "('a \<times> 'b \<times> 'c) => 'c"
translations  "thd3 (_,_,z)" == "z"
*)

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. 
 We use ZZZ for undefined, only in case statements, when a pattern doesn't match.
 A constructur C has name, arity and list of args.
 A closure (X) has function name, number of fixed args and alist of these args.
 Hume doesn't allow anonymous functions, so all closures must be PAPs of a
 named, top-level function.
*}

types
 Heap = "Locn \<leadsto>\<^sub>f  HoVal"

text {* A std variable environment is used as an abstraction over the stack 
 (there is no HAM-style stack in GRUMPY; should discussed how size can be retrived) *}

types
 Env = "VarName =>  HoVal"

translations
 "Env" <= (type) "VarName \<Rightarrow> HoVal"

constdefs
  emptyEnv    :: "Env"
  "emptyEnv x \<equiv> (I 0)"

(*
syntax "_get_var"     :: "Env \<Rightarrow> Var \<Rightarrow> HoVal"		("_<_>" [1000,1000] 1000)
translations "_get_var E x" == "E x"

constdefs 
varupdate :: "Env \<Rightarrow> Var \<Rightarrow> HoVal \<Rightarrow> Env"	("_<_:=_>" [1000,1000,0] 1000)
  "varupdate E v x \<equiv> E(v := x)"
*)


subsection {* Helper functions *}

text {* Projections on triples *}

constdefs fst3 :: "('a \<times> 'b \<times> 'c) => 'a"
 "fst3 q == (case q of (x,y,z) => x)"

constdefs snd3 :: "('a \<times> 'b \<times> 'c) => 'b"
 "snd3 q == (case q of (x,y,z) => y)"

constdefs thd3 :: "('a \<times> 'b \<times> 'c) => 'c"
 "thd3 q == (case q of (x,y,z) => z)"


(*<*)
end
(*>*)