Theory SmallStep
chapter ‹Generated by Lem from ‹semantics/alt_semantics/smallStep.lem›.›
theory "SmallStep"
imports
Main
"HOL-Library.Datatype_Records"
"LEM.Lem_pervasives_extra"
"Lib"
"Namespace"
"Ast"
"SemanticPrimitives"
"Ffi"
begin
datatype ctxt_frame =
Craise " unit "
| Chandle " unit " " (pat * exp0) list "
| Capp " op0 " " v list " " unit " " exp0 list "
| Clog " lop " " unit " " exp0 "
| Cif " unit " " exp0 " " exp0 "
| Cmat " unit " " (pat * exp0) list " " v "
| Clet " varN option " " unit " " exp0 "
| Ccon " ( (modN, conN)id0)option " " v list " " unit " " exp0 list "
| Ctannot " unit " " t "
| Clannot " unit " " locs "
type_synonym ctxt =" ctxt_frame * v sem_env "
type_synonym 'ffi small_state =" v sem_env * ('ffi, v) store_ffi * exp_or_val * ctxt list "
datatype 'ffi e_step_result =
Estep " 'ffi small_state "
| Eabort " abort "
| Estuck
definition push :: "(v)sem_env ⇒(v)store*'ffi ffi_state ⇒ exp0 ⇒ ctxt_frame ⇒(ctxt_frame*(v)sem_env)list ⇒ 'ffi e_step_result " where
" push env s e c' cs = ( Estep (env, s, Exp e, ((c',env)# cs)))"
definition return :: "(v)sem_env ⇒(v)store*'ffi ffi_state ⇒ v ⇒(ctxt)list ⇒ 'ffi e_step_result " where
" return env s v2 c2 = ( Estep (env, s, Val v2, c2))"
definition application :: " op0 ⇒(v)sem_env ⇒(v)store*'ffi ffi_state ⇒(v)list ⇒(ctxt)list ⇒ 'ffi e_step_result " where
" application op1 env s vs c2 = (
(case op1 of
Opapp =>
(case do_opapp vs of
Some (env,e) => Estep (env, s, Exp e, c2)
| None => Eabort Rtype_error
)
| _ =>
(case do_app s op1 vs of
Some (s',r) =>
(case r of
Rerr (Rraise v2) => Estep (env,s',Val v2,((Craise () ,env)# c2))
| Rerr (Rabort a) => Eabort a
| Rval v2 => return env s' v2 c2
)
| None => Eabort Rtype_error
)
))"
fun continue :: "(v)store*'ffi ffi_state ⇒ v ⇒(ctxt_frame*(v)sem_env)list ⇒ 'ffi e_step_result " where
" continue s v2 ([]) = ( Estuck )"
|" continue s v2 ((Craise _, env) # c2) = (
(case c2 of
[] => Estuck
| ((Chandle _ pes,env') # c2) =>
Estep (env,s,Val v2,((Cmat () pes v2, env')# c2))
| _ # c2 => Estep (env,s,Val v2,((Craise () ,env)# c2))
))"
|" continue s v2 ((Chandle _ pes, env) # c2) = (
return env s v2 c2 )"
|" continue s v2 ((Capp op1 vs _ [], env) # c2) = (
application op1 env s (v2 # vs) c2 )"
|" continue s v2 ((Capp op1 vs _ (e # es), env) # c2) = (
push env s e (Capp op1 (v2 # vs) () es) c2 )"
|" continue s v2 ((Clog l _ e, env) # c2) = (
(case do_log l v2 e of
Some (Exp e) => Estep (env, s, Exp e, c2)
| Some (Val v2) => return env s v2 c2
| None => Eabort Rtype_error
))"
|" continue s v2 ((Cif _ e1 e2, env) # c2) = (
(case do_if v2 e1 e2 of
Some e => Estep (env, s, Exp e, c2)
| None => Eabort Rtype_error
))"
|" continue s v2 ((Cmat _ [] err_v, env) # c2) = (
Estep (env, s, Val err_v, ((Craise () , env) # c2)))"
|" continue s v2 ((Cmat _ ((p,e)# pes) err_v, env) # c2) = (
if Lem_list.allDistinct (pat_bindings p []) then
(case pmatch(c env) (fst s) p v2 [] of
Match_type_error => Eabort Rtype_error
| No_match => Estep (env, s, Val v2, ((Cmat () pes err_v,env)# c2))
| Match env' => Estep (( env (| v := (nsAppend (alist_to_ns env')(v env)) |)), s, Exp e, c2)
)
else
Eabort Rtype_error )"
|" continue s v2 ((Clet n _ e, env) # c2) = (
Estep (( env (| v := (nsOptBind n v2(v env)) |)), s, Exp e, c2))"
|" continue s v2 ((Ccon n vs _ [], env) # c2) = (
if do_con_check(c env) n (List.length vs +( 1 :: nat)) then
(case build_conv(c env) n (v2 # vs) of
None => Eabort Rtype_error
| Some v2 => return env s v2 c2
)
else
Eabort Rtype_error )"
|" continue s v2 ((Ccon n vs _ (e # es), env) # c2) = (
if do_con_check(c env) n (((List.length vs +( 1 :: nat)) +( 1 :: nat)) + List.length es) then
push env s e (Ccon n (v2 # vs) () es) c2
else
Eabort Rtype_error )"
|" continue s v2 ((Ctannot _ t1, env) # c2) = (
return env s v2 c2 )"
|" continue s v2 ((Clannot _ l, env) # c2) = (
return env s v2 c2 )"
fun e_step :: "(v)sem_env*((v)store*'ffi ffi_state)*exp_or_val*(ctxt)list ⇒ 'ffi e_step_result " where
" e_step (env, s,(Val v2), c2) = (
continue s v2 c2 )"
|" e_step (env, s,(Exp e), c2) = (
(case e of
Lit l => return env s (Litv l) c2
| Raise e =>
push env s e (Craise () ) c2
| Handle e pes =>
push env s e (Chandle () pes) c2
| Con n es =>
if do_con_check(c env) n (List.length es) then
(case List.rev es of
[] =>
(case build_conv(c env) n [] of
None => Eabort Rtype_error
| Some v2 => return env s v2 c2
)
| e # es =>
push env s e (Ccon n [] () es) c2
)
else
Eabort Rtype_error
| Var n =>
(case nsLookup(v env) n of
None => Eabort Rtype_error
| Some v2 =>
return env s v2 c2
)
| Fun n e => return env s (Closure env n e) c2
| App op1 es =>
(case List.rev es of
[] => application op1 env s [] c2
| (e # es) => push env s e (Capp op1 [] () es) c2
)
| Log l e1 e2 => push env s e1 (Clog l () e2) c2
| If e1 e2 e3 => push env s e1 (Cif () e2 e3) c2
| Mat e pes => push env s e (Cmat () pes (Conv (Some ((''Bind''), TypeExn (Short (''Bind'')))) [])) c2
| Let n e1 e2 => push env s e1 (Clet n () e2) c2
| Letrec funs e =>
if ¬ (allDistinct (List.map ( λx .
(case x of (x,y,z) => x )) funs)) then
Eabort Rtype_error
else
Estep (( env (| v := (build_rec_env funs env(v env)) |)),
s, Exp e, c2)
| Tannot e t1 => push env s e (Ctannot () t1) c2
| Lannot e l => push env s e (Clannot () l) c2
))"
definition e_step_reln :: "(v)sem_env*('ffi,(v))store_ffi*exp_or_val*(ctxt)list ⇒(v)sem_env*('ffi,(v))store_ffi*exp_or_val*(ctxt)list ⇒ bool " where
" e_step_reln st1 st2 = (
(e_step st1 = Estep st2))"
fun
small_eval :: "(v)sem_env ⇒(v)store*'ffi ffi_state ⇒ exp0 ⇒(ctxt)list ⇒((v)store*'ffi ffi_state)*((v),(v))result ⇒ bool " where
"
small_eval env s e c2 (s', Rval v2) = ((
∃ env'. (rtranclp (e_step_reln)) (env,s,Exp e,c2) (env',s',Val v2,[])))"
|"
small_eval env s e c2 (s', Rerr (Rraise v2)) = ((
∃ env'.
∃ env''. (rtranclp (e_step_reln)) (env,s,Exp e,c2) (env',s',Val v2,[(Craise () , env'')])))"
|"
small_eval env s e c2 (s', Rerr (Rabort a)) = ((
∃ env'.
∃ e'.
∃ c'.
(rtranclp (e_step_reln)) (env,s,Exp e,c2) (env',s',e',c') ∧
(e_step (env',s',e',c') = Eabort a)))"
definition e_diverges :: "(v)sem_env ⇒(v)store*'ffi ffi_state ⇒ exp0 ⇒ bool " where
" e_diverges env s e = ((
∀ env'.
∀ s'.
∀ e'.
∀ c'.
(rtranclp (e_step_reln)) (env,s,Exp e,[]) (env',s',e',c')
⟶
((∃ env''. ∃ s''. ∃ e''. ∃ c''.
e_step_reln (env',s',e',c') (env'',s'',e'',c'')))))"
end