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