(* Time-stamp: <Tue Nov 25 2008 20:37:04 Stardate: [-28]0394.08 hwloidl>

   The Grail language, adjusted to be used on top of the HAM.
*)

header {* The Core Hume Language *}

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

section {* Syntax of language and types *}

text {* 
The language corresponds to Arthur3 aka Core Hume aka Schopenhauer, as defined
in space-analysis/AbsSyn.hs of the hw-tinkering branch of the Hume CVS repository
:pserver:hwloidl@littlemill.dcs.st-and.ac.uk:/local/fp/hume

Current restrictions:
- ValueExp only takes an int; should cover entire Value data structure of Arthur3
- PrimBin only works on int; no PrimUn
- 2 forms of apps: 1st order and higher order
- LetExp takes only 1 binding
- patterns are not nested
- no 'as' patterns allowed
- no within, no raise
*}

subsection {* Language *}

datatype Pattern = PVar VarName
                 | PVal HoVal
                 | PCon ConName "VarName list"
                 | PWild int

datatype Exp = ValueExp "HoVal"
             | VarExp VarName
             | ConstrExp ConName "VarName list"
             | PrimBin "HoVal => HoVal => HoVal" "VarName" "VarName"
             | RPrimBin "HoVal => HoVal => HoVal" "VarName" "VarName"
             | IfExp VarName Exp Exp
             | LetExp VarName Exp Exp
             | CallFunExp FunName "VarName list"
             | CallVarExp VarName "VarName list"
             | CaseOneExp VarName "Pattern" "Exp" "Exp"
(*             | CaseExp VarName "(Pattern \<times> Exp) list" *)

text {* Some nice concrete syntax: *}

(* The following black magic is Isabelle gobbledygook to
   introduce some nice concrete syntax. *)

(* let syntax *)
nonterminals
 gletbind gletbinds
syntax
  "_Gbind"      :: "[VarName,Exp] => gletbind"                ("(1_ =/_)" 10)
(*
  "_Grefbind"   :: "[id,expr] => gletbind"                ("(1rf _ =/_)" 10)
  "_Gvoidbind"  :: "[expr] => gletbind"                      ("(1 '_ =/_ )" 10)
*)
  ""            :: "gletbind => gletbinds"               ("_")
  "_gbinds"     :: "[gletbind, gletbinds] => gletbinds"  ("_;/ _")
  "_GLets"      :: "[gletbinds, Exp] => Exp"     ("(LET (_)/ IN (_))" 60)
  

translations
  "_GLets (_gbinds b bs) e"  == "_GLets b (_GLets bs e)"
  "LET    v = e IN e'"    == "LetExp v e e'"

nonterminals
 gcase
syntax
 "_case"       :: "[VarName, Pattern, Exp, Exp] \<Rightarrow> Exp"  ("CASE _ OF _ / THN (_) / OTW (_)" 60)
translations
 "CASE v OF p THN e OTW e'" == "CaseOneExp v p e e'"

(*
  "LET    _ = e IN l END"    == "Letv e l"
  "LET rf v = e IN l END"    == "Letr v e l"
*)

subsection {* Types *}

text {*
 A standard, unannotated type systems. This should reflect the high-level,
 rich-types from the resource analysis, but doesn't at the moment.
 I first want to work out the logic below.
*}

datatype Type = BotTy
              | IntTy
              | BoolTy
              | RefTy "Type"
              | FunTy "Type" "Type"
              | ConTy "ConName" "nat" "Type list"
              | ClosureTy "(Type list) \<times> Type"

subsection {* Helper functions *}

(* free variables *)

consts freeVars :: "Exp \<Rightarrow> VarName set"
       freeVarsPat :: "Pattern \<Rightarrow> VarName set"

primrec
"freeVarsPat (PVar v)      = {v}"
"freeVarsPat (PVal i)      = {}"
"freeVarsPat (PCon c vs)   = set vs"
"freeVarsPat (PWild i)     = {}"

primrec
"freeVars (ValueExp i)  = {}"
"freeVars (VarExp v)  = {v}"
"freeVars (IfExp v e1 e2)  = insert v (freeVars e1 \<union> freeVars e2)"
"freeVars (LetExp v e e')    = (freeVars e \<union> freeVars e') - {v}"
"freeVars (CallFunExp f vs)  = set vs"
"freeVars (CallVarExp v vs)  = insert v (set vs)"
(* "freeVars (CaseExp v bs)     = {}" *)
"freeVars (CaseOneExp v b e e')     = insert v ((freeVars e - freeVarsPat b) \<union> freeVars e')"
(* should be:   insert v (Union (set (map (% (p,e). freeVars e) bs))) *)

(*<*)
end
(*>*)