Up to index of Isabelle/HOL/SafeImp
theory CoreSafeToSVM(* Title: Safe Virtual Machine Semantics
Author: Ricardo Peņa, Javier de Dios
Copyright: May 2008, Universidad Complutense de Madrid
*)
header {* Translation from a CoreSafe program to a SafeImp program *}
theory CoreSafeToSVM
imports SVMState "../CoreSafe/SafeExpr" HaskellLib
begin
text{* {\sl FunMap} keeps the correspondence between a function name and the
label of its initial instruction sequence *}
types
FunMap = "FunName \<rightharpoonup> CodeLabel"
TagMap = "Constructor \<rightharpoonup> nat"
subsection{* Compile-time environment *}
text{* This part is devoted to compile-time environments. See the WFLP'08 paper.
*}
types
MiniEnv = "string \<rightharpoonup> nat"
Env = "(MiniEnv × nat × nat) list"
consts
envSearch' :: "Env => string => nat => nat"
fun envPlusPlus :: "Env => Env" ("_ ++" 120) where
"rho++ = (case rho of
(delta,m,n)#rest => (empty,0,0)#(delta,m+2,2)#rest)"
fun envAdd :: "Env => (string × nat) list => Env" (infix "+" 110) where
"rho + namNats = (case rho of (delta,m,n1)#rest =>
let n2 = length namNats;
g = λ (x,j) . (x,m+j);
delta' = map_of (map g namNats)
in (delta ++ delta',m+n2,0)#rest)"
fun envSearch :: "Env => string => nat" (infix "|>" 110 ) where
"rho |> x = envSearch' rho x 0"
primrec
"envSearch' (tup # rest) x l = (case tup of
(delta,m,n) =>
case delta x of
Some j => (l + m) - j
| None => envSearch' rest x (l+m))"
fun topDepth :: "Env => nat" where
"topDepth ((delta,m,0)#_) = m"
fun decreasing :: "nat => nat list" where
"decreasing n = (if n = 0 then []
else n # decreasing (n - 1))"
subsection {* Translation functions *}
text{* These are the main translation functions:
\begin{itemize}
\item {\sl trProg} translates a complete CoreSafe
program.
\item {\sl trF} translates a CoreSafe function definition. It receives a
not used CodeLabel and returns another one not used. All the CodeLabels in
between are used to translate this function. Also, it returns modified
FunMap and ContinuationMap, including a bindings Name -> CodeLabel and Name
-> CodeLabel list for this function.
\item {\sl trE} translates a CoreSafe expression. The CodeLabel returned
is a non used one, the CodeLabel list contains the labels corresponding to
continuations, the CodeSequence contains the instructions of the
translation and the SVMCode the auxiliary code sequences created. {\sl
trAlts} and {\sl trTup} are auxiliary functions needed in order to define
{\sl trE} as primitive recursive.
\end{itemize} *}
consts
trE :: "[CodeLabel,FunMap,FunName,Env,'a Exp]=>
CodeLabel× CodeLabel list × CodeSequence × SVMCode"
trAlts :: "[CodeLabel,FunMap,FunName,Env,
('a Patron × 'a Exp) list] =>
CodeLabel × (CodeLabel list × CodeLabel × SVMCode) list"
trAlts' :: "[CodeLabel,FunMap,FunName,Env,
('a Patron × 'a Exp) list] =>
CodeLabel × (CodeLabel list × CodeLabel × SVMCode) list"
trTup :: "[CodeLabel,FunMap,FunName,Env,
'a Patron × 'a Exp] =>
CodeLabel list × CodeLabel × SVMCode"
trTup' :: "[CodeLabel,FunMap,FunName,Env,
'a Patron × 'a Exp] =>
CodeLabel list × CodeLabel × SVMCode"
fun lit2val :: "Lit => Val" where
"lit2val (LitN i) = IntT i"
| "lit2val (LitB b) = BoolT b"
fun atom2item :: "Env => 'a Exp => Item" where
"atom2item rho (ConstE c _) = ItemConst (lit2val c)"
| "atom2item rho (VarE x _) = ItemVar (rho |> x)"
fun region2item :: "Env => RegVar => Item" where
"region2item rho r = (if r = self then ItemRegSelf
else ItemVar (rho |> r))"
constdefs mainName :: string
"mainName ≡ ''PSafeMain'' "
fun trF :: "(CodeLabel × FunMap × ContinuationMap) => 'a Def =>
(CodeLabel × FunMap × ContinuationMap) × SVMCode"
where
"trF (p,funm,contm) (t,izq,Simple e []) =
(let
(f,pbs,rs) = izq;
(ps,bs) = unzip pbs;
xs = map pat2var ps;
topdepth = length xs + length rs;
varnats = zip (append xs rs) (decreasing topdepth);
rho = [(empty,0,0)] + varnats;
funm' = funm (f\<mapsto> p);
(q,ls,is,cs) = trE (p+1) funm' f rho e
in ((q, funm',(f,p,ls)#contm), append cs [(p,is,f)]))"
constdefs
type2argType :: "ExpTipo => ArgType"
"type2argType t == (case t of
Rec => Recursive
| ConstrT name ts b rs => if name = intType then IntArg
else if name = boolType then BoolArg
else NonRecursive
| VarT a => IntArg)"
fun trAltDato :: "TagMap => ConstructorTableType => AltDato => ConstructorTableType"
where
"trAltDato tm ct (ConstrA C ts _) = (
let nargs = length ts;
argtypes = map type2argType ts
in (C, (nargs,the (tm C),argtypes))# ct)"
fun extractCons :: "AltDato => Constructor"
where
"extractCons (ConstrA C _ _) = C"
fun trData :: "ConstructorTableType => DecData => ConstructorTableType"
where
"trData ct (T,as,rs,alts) = (
let cs = map extractCons alts;
n = length cs;
tagmap = map_of (zip (sort cs) [0..<n])
in foldl (trAltDato tagmap) ct alts)"
fun trProg :: "'a Prog => SafeImpProg"
where
"trProg (datas,defs,e) = (
let
ctable = foldl trData [] datas;
((p,funm,contm),codes) = mapAccumL trF (1,empty,[]) defs;
(q,ls,is,cs) = trE p funm mainName [(empty,0,0)] e;
code = concat [concat codes, cs, [(q,is,mainName)]];
contmap = (mainName,q,ls)#contm
in ((code,contmap),q,ctable,(0,0,0)) )"
fun normalForm :: "Env => CodeSequence" where
"normalForm rho = (let td = (topDepth rho)
in if td ≠ 0 then [SLIDE 1 td,DECREGION,POPCONT]
else [DECREGION,POPCONT])"
text{* The translation of a expression does a recursive traversal of the
abstract syntax tree. *}
primrec
"trE p funm fname rho (ConstE c a) =
(p,[],BUILDENV [ItemConst (lit2val c)] # normalForm rho,[])"
"trE p funm fname rho (VarE x a) =
(p,[],BUILDENV [ItemVar (rho |> x)] # normalForm rho,[])"
"trE p funm fname rho (CopyE x r a) =
(p,[],BUILDENV [ItemVar (rho |> x),ItemVar (rho |> r)]
# COPY # normalForm rho,[])"
"trE p funm fname rho (ReuseE x a) =
(p,[],BUILDENV [ItemVar (rho |> x)] # REUSE # normalForm rho,[])"
"trE p funm fname rho (AppE f as rs a) = (
case primops f of
Some oper => case as of
a1#a2#[] =>
let i1 = atom2item rho a1;
i2 = atom2item rho a2
in (p,[],BUILDENV [i1,i2] # PRIMOP oper # normalForm rho,[])
| None =>
let its1 = map (atom2item rho) as;
its2 = map (region2item rho) rs;
is = [BUILDENV (append its1 its2),
SLIDE (length as + length rs) (topDepth rho),
CALL (the (funm f))]
in (p,[],is,[]))"
"trE p funm fname rho (Let x1 = e1 In e2 a) = (
let (q2,ls2,is2,cs2) = trE p funm fname (rho+[(x1,1)]) e2
in case e1 of
ConstrE C as r _ =>
let items = map (atom2item rho) as;
item = region2item rho r
in (q2,ls2,BUILDCLS C items item # is2,cs2)
| _ =>
let (q1,ls1,is1,cs1) = trE (q2+1) funm fname (rho++) e1;
cs = append cs2 ((q2,is2,fname) # cs1)
in (q1,q2#(append ls1 ls2),PUSHCONT q2 # is1,cs))"
"trE p funm fname rho (Case e Of alts a) = (
let (q,rss) = trAlts p funm fname rho alts;
(lss,qs,css) = unzip3 rss
in case e of
VarE x _ =>
let (pat1,e1) = hd alts
in case pat1 of
ConstrP _ _ _ => (q,concat lss,[MATCH (rho |> x) qs],concat css)
| ConstP (LitN i) =>
let m = length alts - 1;
v = nat i
in (q,concat lss,[MATCHN (rho |> x) v m qs],concat css)
| ConstP (LitB b) => (q,concat lss,[MATCHN (rho |> x) 0 2 qs],concat css))"
"trE p funm fname rho (CaseD e Of alts a) = (
let (q,rss) = trAlts' p funm fname rho alts;
(lss,qs,css) = unzip3 rss
in case e of
VarE x _ => (q,concat lss,[MATCHD (rho |> x) qs],concat css))"
"trAlts p funm fname rho [] = (p,[])"
"trAlts p funm fname rho (alt#alts) = (
let (ls,q,cs') = trTup p funm fname rho alt;
(q',tups) = trAlts (q+1) funm fname rho alts
in (q',(ls,q,cs')#tups))"
"trAlts' p funm fname rho [] = (p,[])"
"trAlts' p funm fname rho (alt#alts) = (
let (ls,q,cs') = trTup' p funm fname rho alt;
(q',tups) = trAlts' (q+1) funm fname rho alts
in (q',(ls,q,cs')#tups))"
"trTup p funm fname rho (pat,e) = (case pat of
ConstrP C ps _ =>
let xs = map pat2var ps;
rho' = rho + zip xs (decreasing (length xs));
(q,ls,is,cs) = trE p funm fname rho' e;
cs' = append cs [(q,is,fname)]
in (ls,q,cs')
| ConstP _ =>
let (q,ls,is,cs) = trE p funm fname rho e;
cs' = append cs [(q,is,fname)]
in (ls,q,cs'))"
"trTup' p funm fname rho (pat,e) = (case pat of
ConstrP C ps _ =>
let xs = map pat2var ps;
rho' = rho + zip xs (decreasing (length xs));
(q,ls,is,cs) = trE p funm fname rho' e;
cs' = append cs [(q,is,fname)]
in (ls,q,cs')
| _ =>
let (q,ls,is,cs) = trE p funm fname rho e;
cs' = append cs [(q,is,fname)]
in (ls,q,cs'))"
(*export_code trProg in Haskell file "./codetrProg"*)
subsection {* Auxiliary functions for the correctness theorem *}
text{* The following functions are useful for stating the correctness
theorem of the CoreSafe translation.
*}
-- "returns the set of function names called from an expression"
consts
called :: "'a Exp => FunName set"
calledList :: "('a Patron × 'a Exp) list => FunName set"
calledList' :: "('a Patron × 'a Exp) list => FunName set"
calledTup :: "('a Patron × 'a Exp) => FunName set"
calledTup' :: "('a Patron × 'a Exp) => FunName set"
primrec
"called (ConstE Lit a) = {}"
"called (ConstrE C exps rv a) = {}"
"called (VarE x a) = {}"
"called (CopyE x rv a) = {}"
"called (ReuseE x a) = {}"
"called (AppE f as rs a) = {f}"
"called (Let x1 = e1 In e2 a) = called e1 ∪ called e2"
"called (Case e Of alts a) = called e ∪ calledList alts"
"called (CaseD e Of alts a) = called e ∪ calledList' alts"
"calledList [] = {}"
"calledList (alt#alts) = calledTup alt ∪ calledList alts"
"calledList' [] = {}"
"calledList' (alt#alts) = calledTup' alt ∪ calledList' alts"
"calledTup (p,e) = called e"
"calledTup' (p,e) = called e"
consts
-- "returns the set of function names defined in a program"
definedFuns :: "('a Def ) list => FunName set"
primrec
"definedFuns [] = {}"
"definedFuns (def#defs) = (case def of (t,(f,pbs,rs),der) =>
{f} ∪ definedFuns defs)"
consts
-- "given a defined name and a program, it returns the function body"
extractBody :: "FunName => ('a Def) list => 'a Exp"
primrec
"extractBody f (def#defs) = (case def of (t,(g,pbs,rs),Simple e []) =>
if f = g then e else extractBody f defs)"
-- "It inductively defines the set of function names reached from an expression"
inductive_set
closureCalled :: "'a Exp => ('a Def ) list => FunName set"
for e :: "'a Exp" and ds :: "('a Def ) list"
where
init : "f ∈ called e ==> f ∈ closureCalled e ds"
| step : "[|
f ∈ closureCalled e ds;
f ∈ definedFuns ds;
ef = extractBody f ds;
g ∈ called ef
|] ==>
g ∈ closureCalled e ds"
end