# Theory Evaluate

```chapter ‹Generated by Lem from ‹semantics/evaluate.lem›.›

theory "Evaluate"

imports
Main
"HOL-Library.Datatype_Records"
"LEM.Lem_pervasives_extra"
"Lib"
"Namespace"
"Ast"
"SemanticPrimitives"
"Ffi"

begin

― ‹‹open import Pervasives_extra››
― ‹‹open import Lib››
― ‹‹open import Ast››
― ‹‹open import Namespace››
― ‹‹open import SemanticPrimitives››
― ‹‹open import Ffi››

― ‹‹ The semantics is defined here using fix_clock so that HOL4 generates
* provable termination conditions. However, after termination is proved, we
* clean up the definition (in HOL4) to remove occurrences of fix_clock. ››

fun fix_clock  :: " 'a state ⇒ 'b state*'c ⇒ 'b state*'c "  where
" fix_clock s (s',res) = (
(( s' (| clock := (if(clock   s') ≤(clock   s)
then(clock   s') else(clock   s)) |)),res))"

definition dec_clock  :: " 'a state ⇒ 'a state "  where
" dec_clock s = ( ( s (| clock := ((clock   s) -( 1 :: nat)) |)))"

― ‹‹ list_result is equivalent to map_result (\v. [v]) I, where map_result is
* defined in evalPropsTheory ››
fun
list_result  :: "('a,'b)result ⇒(('a list),'b)result "  where
"
list_result (Rval v2) = ( Rval [v2])"
|"
list_result (Rerr e) = ( Rerr e )"

― ‹‹val evaluate : forall 'ffi. state 'ffi -> sem_env v -> list exp -> state 'ffi * result (list v) v››
― ‹‹val evaluate_match : forall 'ffi. state 'ffi -> sem_env v -> v -> list (pat * exp) -> v -> state 'ffi * result (list v) v››
function (sequential,domintros)
fun_evaluate_match  :: " 'ffi state ⇒(v)sem_env ⇒ v ⇒(pat*exp0)list ⇒ v ⇒ 'ffi state*(((v)list),(v))result "
and
fun_evaluate  :: " 'ffi state ⇒(v)sem_env ⇒(exp0)list ⇒ 'ffi state*(((v)list),(v))result "  where
"
fun_evaluate st env [] = ( (st, Rval []))"
|"
fun_evaluate st env (e1 # e2 # es) = (
(case  fix_clock st (fun_evaluate st env [e1]) of
(st', Rval v1) =>
(case  fun_evaluate st' env (e2 # es) of
(st'', Rval vs) => (st'', Rval (List.hd v1 # vs))
| res => res
)
| res => res
))"
|"
fun_evaluate st env [Lit l] = ( (st, Rval [Litv l]))"
|"
fun_evaluate st env [Raise e] = (
(case  fun_evaluate st env [e] of
(st', Rval v2) => (st', Rerr (Rraise (List.hd v2)))
| res => res
))"
|"
fun_evaluate st env [Handle e pes] = (
(case  fix_clock st (fun_evaluate st env [e]) of
(st', Rerr (Rraise v2)) => fun_evaluate_match st' env v2 pes v2
| res => res
))"
|"
fun_evaluate st env [Con cn es] = (
if do_con_check(c   env) cn (List.length es) then
(case  fun_evaluate st env (List.rev es) of
(st', Rval vs) =>
(case  build_conv(c   env) cn (List.rev vs) of
Some v2 => (st', Rval [v2])
| None => (st', Rerr (Rabort Rtype_error))
)
| res => res
)
else (st, Rerr (Rabort Rtype_error)))"
|"
fun_evaluate st env [Var n] = (
(case  nsLookup(v   env) n of
Some v2 => (st, Rval [v2])
| None => (st, Rerr (Rabort Rtype_error))
))"
|"
fun_evaluate st env [Fun x e] = ( (st, Rval [Closure env x e]))"
|"
fun_evaluate st env [App op1 es] = (
(case  fix_clock st (fun_evaluate st env (List.rev es)) of
(st', Rval vs) =>
if op1 = Opapp then
(case  do_opapp (List.rev vs) of
Some (env',e) =>
if(clock   st') =( 0 :: nat) then
(st', Rerr (Rabort Rtimeout_error))
else
fun_evaluate (dec_clock st') env' [e]
| None => (st', Rerr (Rabort Rtype_error))
)
else
(case  do_app ((refs   st'),(ffi   st')) op1 (List.rev vs) of
Some ((refs1,ffi1),r) => (( st' (| refs := refs1, ffi := ffi1 |)), list_result r)
| None => (st', Rerr (Rabort Rtype_error))
)
| res => res
))"
|"
fun_evaluate st env [Log lop e1 e2] = (
(case  fix_clock st (fun_evaluate st env [e1]) of
(st', Rval v1) =>
(case  do_log lop (List.hd v1) e2 of
Some (Exp e) => fun_evaluate st' env [e]
| Some (Val v2) => (st', Rval [v2])
| None => (st', Rerr (Rabort Rtype_error))
)
| res => res
))"
|"
fun_evaluate st env [If e1 e2 e3] = (
(case  fix_clock st (fun_evaluate st env [e1]) of
(st', Rval v2) =>
(case  do_if (List.hd v2) e2 e3 of
Some e => fun_evaluate st' env [e]
| None => (st', Rerr (Rabort Rtype_error))
)
| res => res
))"
|"
fun_evaluate st env [Mat e pes] = (
(case  fix_clock st (fun_evaluate st env [e]) of
(st', Rval v2) =>
fun_evaluate_match st' env (List.hd v2) pes Bindv
| res => res
))"
|"
fun_evaluate st env [Let xo e1 e2] = (
(case  fix_clock st (fun_evaluate st env [e1]) of
(st', Rval v2) => fun_evaluate st' ( env (| v := (nsOptBind xo (List.hd v2)(v   env)) |)) [e2]
| res => res
))"
|"
fun_evaluate st env [Letrec funs e] = (
if allDistinct (List.map ( λx .
(case  x of (x,y,z) => x )) funs) then
fun_evaluate st ( env (| v := (build_rec_env funs env(v   env)) |)) [e]
else
(st, Rerr (Rabort Rtype_error)))"
|"
fun_evaluate st env [Tannot e t1] = (
fun_evaluate st env [e])"
|"
fun_evaluate st env [Lannot e l] = (
fun_evaluate st env [e])"
|"
fun_evaluate_match st env v2 [] err_v = ( (st, Rerr (Rraise err_v)))"
|"
fun_evaluate_match st env v2 ((p,e)# pes) err_v  = (
if allDistinct (pat_bindings p []) then
(case  pmatch(c   env)(refs   st) p v2 [] of
Match env_v' => fun_evaluate st ( env (| v := (nsAppend (alist_to_ns env_v')(v   env)) |)) [e]
| No_match => fun_evaluate_match st env v2 pes err_v
| Match_type_error => (st, Rerr (Rabort Rtype_error))
)
else (st, Rerr (Rabort Rtype_error)))"
by pat_completeness auto

― ‹‹val evaluate_decs :
forall 'ffi. list modN -> state 'ffi -> sem_env v -> list dec -> state 'ffi * result (sem_env v) v››
fun
fun_evaluate_decs  :: "(string)list ⇒ 'ffi state ⇒(v)sem_env ⇒(dec)list ⇒ 'ffi state*(((v)sem_env),(v))result "  where
"
fun_evaluate_decs mn st env [] = ( (st, Rval (| v = nsEmpty, c = nsEmpty |)))"
|"
fun_evaluate_decs mn st env (d1 # d2 # ds) = (
(case  fun_evaluate_decs mn st env [d1] of
(st1, Rval env1) =>
(case  fun_evaluate_decs mn st1 (extend_dec_env env1 env) (d2 # ds) of
(st2,r) => (st2, combine_dec_result env1 r)
)
| res => res
))"
|"
fun_evaluate_decs mn st env [Dlet locs p e] = (
if allDistinct (pat_bindings p []) then
(case  fun_evaluate st env [e] of
(st', Rval v2) =>
(st',
(case  pmatch(c   env)(refs   st') p (List.hd v2) [] of
Match new_vals => Rval (| v = (alist_to_ns new_vals), c = nsEmpty |)
| No_match => Rerr (Rraise Bindv)
| Match_type_error => Rerr (Rabort Rtype_error)
))
| (st', Rerr err) => (st', Rerr err)
)
else
(st, Rerr (Rabort Rtype_error)))"
|"
fun_evaluate_decs mn st env [Dletrec locs funs] = (
(st,
(if allDistinct (List.map ( λx .
(case  x of (x,y,z) => x )) funs) then
Rval (| v = (build_rec_env funs env nsEmpty), c = nsEmpty |)
else
Rerr (Rabort Rtype_error))))"
|"
fun_evaluate_decs mn st env [Dtype locs tds] = (
(let new_tdecs = (type_defs_to_new_tdecs mn tds) in
if check_dup_ctors tds ∧
(disjnt new_tdecs(defined_types   st) ∧
allDistinct (List.map ( λx .
(case  x of (tvs,tn,ctors) => tn )) tds))
then
(( st (| defined_types := (new_tdecs ∪(defined_types   st)) |)),
Rval (| v = nsEmpty, c = (build_tdefs mn tds) |))
else
(st, Rerr (Rabort Rtype_error))))"
|"
fun_evaluate_decs mn st env [Dtabbrev locs tvs tn t1] = (
(st, Rval (| v = nsEmpty, c = nsEmpty |)))"
|"
fun_evaluate_decs mn st env [Dexn locs cn ts] = (
if TypeExn (mk_id mn cn) ∈(defined_types   st) then
(st, Rerr (Rabort Rtype_error))
else
(( st (| defined_types := ({TypeExn (mk_id mn cn)} ∪(defined_types   st)) |)),
Rval (| v = nsEmpty, c = (nsSing cn (List.length ts, TypeExn (mk_id mn cn))) |)))"

definition envLift  :: " string ⇒ 'a sem_env ⇒ 'a sem_env "  where
" envLift mn env = (
(| v = (nsLift mn(v   env)), c = (nsLift mn(c   env)) |) )"

― ‹‹val evaluate_tops :
forall 'ffi. state 'ffi -> sem_env v -> list top -> state 'ffi *  result (sem_env v) v››
fun
evaluate_tops  :: " 'ffi state ⇒(v)sem_env ⇒(top0)list ⇒ 'ffi state*(((v)sem_env),(v))result "  where
"
evaluate_tops st env [] = ( (st, Rval (| v = nsEmpty, c = nsEmpty |)))"
|"
evaluate_tops st env (top1 # top2 # tops) = (
(case  evaluate_tops st env [top1] of
(st1, Rval env1) =>
(case  evaluate_tops st1 (extend_dec_env env1 env) (top2 # tops) of
(st2, r) => (st2, combine_dec_result env1 r)
)
| res => res
))"
|"
evaluate_tops st env [Tdec d] = ( fun_evaluate_decs [] st env [d])"
|"
evaluate_tops st env [Tmod mn specs ds] = (
if ¬ ([mn] ∈(defined_mods   st)) ∧ no_dup_types ds
then
(case  fun_evaluate_decs [mn] st env ds of
(st', r) =>
(( st' (| defined_mods := ({[mn]} ∪(defined_mods   st')) |)),
(case  r of
Rval env' => Rval (| v = (nsLift mn(v   env')), c = (nsLift mn(c   env')) |)
| Rerr err => Rerr err
))
)
else
(st, Rerr (Rabort Rtype_error)))"

― ‹‹val evaluate_prog : forall 'ffi. state 'ffi -> sem_env v -> prog -> state 'ffi * result (sem_env v) v››
definition
fun_evaluate_prog  :: " 'ffi state ⇒(v)sem_env ⇒(top0)list ⇒ 'ffi state*(((v)sem_env),(v))result "  where
"
fun_evaluate_prog st env prog = (
if no_dup_mods prog(defined_mods   st) ∧ no_dup_top_types prog(defined_types   st) then
evaluate_tops st env prog
else
(st, Rerr (Rabort Rtype_error)))"

end
```