Up to index of Isabelle/HOL/CoreSafe
theory SafeExpr(*
Title: SafeExpr.thy
Authors: Javier de Dios Castro, Ricardo Peņa
*)
header {* Normalized Safe Expressions *}
theory SafeExpr imports "../SafeImp/SafeHeap" "../SafeImp/HaskellLib"
begin
text {* This is a somewhat simplified copy of the abstract syntax used by
the Safe compiler. The idea is that the Haskell code generated by Isabelle
for the definition of the {\sl trProg} function, translating from CoreSafe
to SafeImp, can be directly used as a phase of the compiler. The
simplifications are in expresion LetE and in the definition of 'a Der, in
order to avoid unnecessary mutual recursion between types.
First, we define the key elements of CoreSafe abstract syntax.
*}
constdefs
intType :: string
"intType == ''Int'' "
boolType :: string
"boolType == ''Bool'' "
datatype ExpTipo = VarT string
| ConstrT string "ExpTipo list" bool "string list"
| Rec
datatype AltDato = ConstrA string "(ExpTipo list)" string
types DecData = "string × string list × string list × AltDato list"
datatype Lit = LitN int | LitB bool
datatype 'a Patron = ConstP Lit
| VarP string 'a
| ConstrP string "('a Patron) list" 'a
text{*
Now we define the CoreSafe expressions. *}
types
ProgVar = string
RegVar = string
datatype 'a Exp = ConstE Lit 'a
| ConstrE string "('a Exp) list" RegVar 'a
| VarE ProgVar 'a
| CopyE ProgVar RegVar 'a ( "_ @ _ _" 90)
| ReuseE ProgVar 'a
| AppE FunName "('a Exp) list" "RegVar list" 'a
| LetE string "('a Exp)" "('a Exp)" 'a
("Let _ = _ In _ _" 95)
(* | CaseIE expr "(int × expr) list" ("CaseN _ Of _" 95) *)
| CaseE "('a Exp)" "('a Patron × 'a Exp) list" 'a
("Case _ Of _ _" 95)
| CaseDE "('a Exp)" "('a Patron × 'a Exp) list" 'a
("CaseD _ Of _ _" 95)
text {* Now, the rest of the abstract syntax. *}
datatype 'a Der = Simple "('a Exp)" "int list"
types
'a Izq = "string × ('a Patron × bool) list × string list"
'a Def = "ExpTipo list × 'a Izq × 'a Der"
'a Prog = "DecData list × ('a Def) list × 'a Exp"
subsection{* Free Variables *}
fun pat2var :: "'a Patron => string"
where
"pat2var (VarP x _) = x"
fun extractP :: "'a Patron => (string × string list)"
where
"extractP (ConstrP C ps _) = (
let xs = map pat2var ps
in (C,xs))"
| "extractP _ = ([],[])"
fun extractVar :: "'a Patron => string list"
where
"extractVar (ConstrP C ps a) = map pat2var ps"
| "extractVar (ConstP l) = []"
| "extractVar (VarP v a) = [v]"
consts varProgPat :: "'a Patron => string set"
varProgPats :: "'a Patron list => string set"
primrec
"varProgPat (ConstP l) = {}"
"varProgPat (VarP x a) = {x}"
"varProgPat (ConstrP C pats a) = varProgPats pats"
"varProgPats [] = {}"
"varProgPats (pat#pats) = varProgPat pat ∪ varProgPats pats"
consts varProg :: "'a Exp => ProgVar set"
varProgs :: "'a Exp list => ProgVar set"
varProgs' :: "'a Exp list => ProgVar set"
varProgAlts :: "('a Patron × 'a Exp) list => string set"
varProgAlts' :: "('a Patron × 'a Exp) list => string set"
varProgTup :: "'a Patron × 'a Exp => string set"
varProgTup' :: "'a Patron × 'a Exp => string set"
primrec
"varProg (ConstE Lit a) = {}"
"varProg (ConstrE C exps r a) = varProgs exps"
"varProg (VarE x a) = {x}"
"varProg (CopyE x r a) = {x}"
"varProg (ReuseE x a) = {x}"
"varProg (AppE fn exps rs a) = varProgs' exps"
"varProg (LetE x1 e1 e2 a) = varProg e1 ∪ varProg e2 ∪ {x1}"
"varProg (CaseE exp alts a) = varProg exp ∪ varProgAlts alts"
"varProg (CaseDE exp alts a) = varProg exp ∪ varProgAlts' alts"
"varProgs [] = {}"
"varProgs (exp#exps) = varProg exp ∪ varProgs exps"
"varProgs' [] = {}"
"varProgs' (exp#exps) = varProg exp ∪ varProgs' exps"
"varProgAlts [] = {}"
"varProgAlts (alt#alts) = varProgTup alt ∪ varProgAlts alts"
"varProgAlts' [] = {}"
"varProgAlts' (alt#alts) = varProgTup' alt ∪ varProgAlts' alts"
"varProgTup (pat,e) = varProgPat pat ∪ varProg e"
"varProgTup' (pat,e) = varProgPat pat ∪ varProg e"
consts fv :: "'a Exp => string set"
fvs :: "'a Exp list => string set"
fvs' :: "'a Exp list => string set"
fvAlts :: "('a Patron × 'a Exp) list => string set"
fvAlts' :: "('a Patron × 'a Exp) list => string set"
fvTup :: "'a Patron × 'a Exp => string set"
fvTup' :: "'a Patron × 'a Exp => string set"
primrec
"fv (ConstE Lit a) = {}"
"fv (ConstrE C exps rv a) = fvs exps"
"fv (VarE x a) = {x}"
"fv (CopyE x rv a) = {x}"
"fv (ReuseE x a) = {x}"
"fv (AppE fn exps rvs a) = fvs' exps"
"fv (LetE x1 e1 e2 a) = fv e1 ∪ fv e2 - {x1}"
"fv (CaseE exp patexps a) = fvAlts patexps ∪ fv exp"
"fv (CaseDE exp patexps a) = fvAlts' patexps ∪ fv exp"
"fvs [] = {}"
"fvs (exp#exps) = fv exp ∪ fvs exps"
"fvs' [] = {}"
"fvs' (exp#exps) = fv exp ∪ fvs' exps"
"fvAlts [] = {}"
"fvAlts (alt#alts) = fvTup alt ∪ fvAlts alts"
"fvAlts' [] = {}"
"fvAlts' (alt#alts) = fvTup' alt ∪ fvAlts' alts"
"fvTup (pat,e) = fv e - set (snd (extractP pat))"
"fvTup' (pat,e) = fv e - set (snd (extractP pat))"
consts fvReg :: "'a Exp => string set"
fvsReg :: "'a Exp list => string set"
fvsReg' :: "'a Exp list => string set"
fvAltsReg :: "('a Patron × 'a Exp) list => string set"
fvAltsReg' :: "('a Patron × 'a Exp) list => string set"
fvTupReg :: "'a Patron × 'a Exp => string set"
fvTupReg' :: "'a Patron × 'a Exp => string set"
primrec
"fvReg (ConstE Lit a) = {}"
"fvReg (ConstrE C exps r a) = {r}"
"fvReg (VarE x a) = {}"
"fvReg (CopyE x r a) = {r}"
"fvReg (ReuseE x a) = {}"
"fvReg (AppE fn exps rvs a) = set rvs"
"fvReg (LetE x1 e1 e2 a) = fvReg e1 ∪ fvReg e2"
"fvReg (CaseE exp patexps a) = fvAltsReg patexps"
"fvReg (CaseDE exp patexps a) = fvAltsReg' patexps"
"fvAltsReg [] = {}"
"fvAltsReg (alt#alts) = fvTupReg alt ∪ fvAltsReg alts"
"fvAltsReg' [] = {}"
"fvAltsReg' (alt#alts) = fvTupReg' alt ∪ fvAltsReg' alts"
"fvTupReg (pat,e) = fvReg e"
"fvTupReg' (pat,e) = fvReg e"
consts boundVar :: "'a Exp => string set"
boundVars :: "'a Exp list => string set"
boundVars' :: "'a Exp list => string set"
boundVarAlts :: "('a Patron × 'a Exp) list => string set"
boundVarAlts' :: "('a Patron × 'a Exp) list => string set"
boundVarTup :: "'a Patron × 'a Exp => string set"
boundVarTup' :: "'a Patron × 'a Exp => string set"
primrec
"boundVar (ConstE Lit a) = {}"
"boundVar (ConstrE C exps rv a) = boundVars exps"
"boundVar (VarE x a) = {}"
"boundVar (CopyE x rv a) = {}"
"boundVar (ReuseE x a) = {}"
"boundVar (AppE fn exps rvs a) = {}"
"boundVar (LetE x1 e1 e2 a) = {x1}"
"boundVar (CaseE exp patexps a) = boundVarAlts patexps"
"boundVar (CaseDE exp patexps a) = boundVarAlts' patexps"
"boundVars [] = {}"
"boundVars (exp#exps) = boundVar exp ∪ boundVars exps"
"boundVarAlts [] = {}"
"boundVarAlts (alt#alts) = boundVarTup alt ∪ boundVarAlts alts"
"boundVarAlts' [] = {}"
"boundVarAlts' (alt#alts) = boundVarTup' alt ∪ boundVarAlts' alts"
"boundVarTup (pat,e) = set (extractVar pat)"
"boundVarTup' (pat,e) = set (extractVar pat)"
text{*
A runtime environment consists of two partial mappings: one from program
variables to normal form values, and one from region variables
to actual regions. *}
types
Environment = "(ProgVar \<rightharpoonup> Val) × (RegVar \<rightharpoonup> Region) "
text{*
The runtime system provides a 'copy' function which generates a new data structure
from a given location by copying those cells pointed to by recursive argument
positions of data constructors. The $\Sigma$ environment provides the textual
definitions of previously defined Safe functions.
Some auxiliary functions: 'extend' extends an environment with a collection
of bindings from variables to values; 'fresh' is a predicate telling
whether a variable is fresh with respect to a heap; 'atom2val', given an
environment and an atom (a program variable or a literal expression)
returns its corresponding value; 'atom2var', given and expression return its
corresponding variable; 'atom', is a predicate telling whether a expression is
a atom. *}
constdefs recursiveArgs :: "Constructor => bool list"
"recursiveArgs C ≡ (let
(_,_,args) = the (ConstructorTable C)
in map (%a. a = Recursive) args)"
function copy' :: "[Region,HeapMap,(Val × bool)] => (HeapMap × Val)"
where
"copy' j h (v,False) = (h,v)"
| "copy' j h (Val.Loc p,True) = (let
(k,C,ps) = the (h p);
bs = recursiveArgs C;
pbs = zip ps bs;
(h',ps') = mapAccumL (copy' j) h pbs;
p' = getFresh h'
in (h'(p'\<mapsto>(j,C,ps')),Val.Loc p'))"
| "copy' j h (IntT i,True) = (h,IntT i)"
| "copy' j h (BoolT b,True) = (h,BoolT b)"
by pat_completeness auto
function copy :: "[Heap, Location, Region] => (Heap × Location)"
where
"copy (h,k) p j = (let
(h',p') = copy' j h (Val.Loc p,True)
in case p' of (Val.Loc q) => ((h',k), q))"
by pat_completeness auto
termination by (relation "{}") simp
types FunDefEnv = "string \<rightharpoonup> ProgVar list × RegVar list × unit Exp"
consts
Σf :: "FunDefEnv"
constdefs bodyAPP :: "FunDefEnv => string => unit Exp"
"bodyAPP Σ f == (case Σ f of Some (xs,rs,ef) => ef)"
constdefs varsAPP :: "FunDefEnv => string => string list"
"varsAPP Σ f ≡ (case Σ f of Some (xs,rs,ef) => xs)"
constdefs regionsAPP :: "FunDefEnv => string => string list"
"regionsAPP Σ f ≡ (case Σ f of Some (xs,rs,ef) => rs)"
definition
extend :: "[string \<rightharpoonup> Val, ProgVar list, Val list] =>(ProgVar \<rightharpoonup> Val)" where
"extend E xs vs = E ++ map_of (zip xs vs)"
definition
def_extend :: "[string \<rightharpoonup> Val, ProgVar list, Val list] => bool" where
"def_extend E xs vs = (set xs ∩ dom E = {} ∧ length xs = length vs ∧ distinct xs ∧ (∀ x∈ set xs. x ≠ self))"
fun atom2val :: "(ProgVar \<rightharpoonup> Val) => 'a Exp => Val"
where
"atom2val E (ConstE (LitN i) a) = IntT i"
| "atom2val E (ConstE (LitB b) a) = BoolT b"
| "atom2val E (VarE x a) = the (E x)"
fun atom2var :: "'a Exp => string"
where
"atom2var (VarE x a) = x"
fun atom :: "'a Exp => bool"
where
"atom e = (case e of
(VarE x a) => True
| _ => False)"
text{*
Lemmas for extend function
*}
lemma extend_monotone: " x ∉ set xs ==> E x = extend E xs vs x"
apply (induct xs vs rule:list_induct2')
apply (simp add: extend_def)
apply (simp add: extend_def)
apply (simp add: extend_def)
apply (subgoal_tac "x ∉ set xs",simp)
apply (subgoal_tac "extend E (xa # xs) (y # ys) = (extend E xs ys)(xa \<mapsto>y)")
apply simp
apply (simp add: extend_def)
by simp
lemma list_induct3:
"[| P [] 0;
!!x xs. P (x#xs) 0;
!!i. P [] (Suc i);
!!x xs i. P xs i ==> P (x#xs) (Suc i) |]
==> P xs i"
by (induct xs arbitrary: i) (case_tac x, auto)+
lemma extend_monotone_i [rule_format]:
"i < length alts -->
length alts > 0 -->
x ∉ set (snd (extractP (fst (alts ! i)))) -->
E x = extend E (snd (extractP (fst (alts ! i)))) vs x"
apply (induct alts i rule: list_induct3, simp_all)
apply (rule impI)
apply (erule extend_monotone)
apply (rule impI, simp)
by (case_tac "xs=[]",simp_all)
lemma extend_prop1:
"[| z ∈ dom (extend E xs vs); z ∉ set xs; length xs = length vs |] ==> z ∈ dom E"
apply (simp add: extend_def)
apply (erule disjE)
apply (simp add: dom_def)
by simp
end
lemma extend_monotone:
x ∉ set xs ==> E x = extend E xs vs x
lemma list_induct3:
[| P [] 0; !!x xs. P (x # xs) 0; !!i. P [] (Suc i);
!!x xs i. P xs i ==> P (x # xs) (Suc i) |]
==> P xs i
lemma extend_monotone_i:
[| i < length alts; 0 < length alts;
x ∉ set (snd (extractP (fst (alts ! i)))) |]
==> E x = extend E (snd (extractP (fst (alts ! i)))) vs x
lemma extend_prop1:
[| z ∈ dom (extend E xs vs); z ∉ set xs; length xs = length vs |] ==> z ∈ dom E