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