# 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

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

― ‹‹ Small-step semantics for expression only.  Modules and definitions have
* big-step semantics only ››

― ‹‹ Evaluation contexts
* The hole is denoted by the unit type
* The env argument contains bindings for the free variables of expressions in
the context ››
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 "
― ‹‹ The value is raised if none of the patterns match ››
| Cmat " unit " " (pat * exp0) list " " v "
| Clet "  varN option " " unit " " exp0 "
― ‹‹ Evaluating a constructor's arguments
* The v list should be in reverse order. ››
| Ccon "  ( (modN, conN)id0)option " " v list " " unit " " exp0 list "
| Ctannot " unit " " t "
| Clannot " unit " " locs "
type_synonym ctxt =" ctxt_frame * v sem_env "

― ‹‹ State for CEK-style expression evaluation
* - constructor data
* - the store
* - the environment for the free variables of the current expression
* - the current expression to evaluate, or a value if finished
* - the context stack (continuation) of what to do once the current expression
*   is finished.  Each entry has an environment for it's free variables ››

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

― ‹‹ The semantics are deterministic, and presented functionally instead of
* relationally for proof rather that readability; the steps are very small: we
* push individual frames onto the context stack instead of finding a redex in a
* single step ››

― ‹‹val push : forall 'ffi. sem_env v -> store_ffi 'ffi v -> exp -> ctxt_frame -> list ctxt -> e_step_result 'ffi››
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)))"

― ‹‹val return : forall 'ffi. sem_env v -> store_ffi 'ffi v -> v -> list ctxt -> e_step_result 'ffi››
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))"

― ‹‹val application : forall 'ffi. op -> sem_env v -> store_ffi 'ffi v -> list v -> list ctxt -> e_step_result 'ffi››
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
)
))"

― ‹‹ apply a context to a value ››
― ‹‹val continue : forall 'ffi. store_ffi 'ffi v -> v -> list ctxt -> e_step_result 'ffi››
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 )"

― ‹‹ The single step expression evaluator.  Returns None if there is nothing to
* do, but no type error.  Returns Type_error on encountering free variables,
* mis-applied (or non-existent) constructors, and when the wrong kind of value
* if given to a primitive.  Returns Bind_error when no pattern in a match
* matches the value.  Otherwise it returns the next state ››

― ‹‹val e_step : forall 'ffi. small_state 'ffi -> e_step_result 'ffi››
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
))"

― ‹‹ Define a semantic function using the steps ››

― ‹‹val e_step_reln : forall 'ffi. small_state 'ffi -> small_state 'ffi -> bool››
― ‹‹val small_eval : forall 'ffi. sem_env v -> store_ffi 'ffi v -> exp -> list ctxt -> store_ffi 'ffi v * result v v -> bool››

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)))"

― ‹‹val e_diverges : forall 'ffi. sem_env v -> store_ffi 'ffi v -> exp -> bool››
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
```