evaluate.lem

(*
  Functional big-step semantics for evaluation of CakeML programs.
*)
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. *)

let fix_clock s (s',res) =
  (<| s' with clock = if s'.clock <= s.clock
                     then s'.clock else s.clock |>,res)

let dec_clock s = <| s with clock = s.clock - 1 |>

let do_eval_res vs s = match do_eval vs s.eval_state with
  | Nothing -> (s, Rerr (Rabort Rtype_error))
  | Just (env1, decs, es1) -> (<| s with eval_state = es1 |>, Rval (env1, decs))
  end

(* list_result is equivalent to map_result (\v. [v]) I, where map_result is
 * defined in evalPropsTheory *)
let rec
list_result (Rval v) = Rval [v]
and
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
val evaluate_decs : forall 'ffi. state 'ffi -> sem_env v -> list dec -> state 'ffi * result (sem_env v) v
let rec
evaluate st env [] = (st, Rval [])
and
evaluate st env (e1::e2::es) =
  match fix_clock st (evaluate st env [e1]) with
  | (st', Rval v1) ->
      match evaluate st' env (e2::es) with
      | (st'', Rval vs) -> (st'', Rval (head v1::vs))
      | res -> res
      end
  | res -> res
  end
and
evaluate st env [Lit l] = (st, Rval [Litv l])
and
evaluate st env [Raise e] =
  match evaluate st env [e] with
  | (st', Rval v) -> (st', Rerr (Rraise (head v)))
  | res -> res
  end
and
evaluate st env [Handle e pes] =
  match fix_clock st (evaluate st env [e]) with
  | (st', Rerr (Rraise v)) ->
      if can_pmatch_all env.c st'.refs (List.map fst pes) v
      then evaluate_match st' env v pes v
      else (st', Rerr (Rabort Rtype_error))
  | res -> res
  end
and
evaluate st env [Con cn es] =
  if do_con_check env.c cn (length es) then
    match evaluate st env (reverse es) with
    | (st', Rval vs) ->
        match build_conv env.c cn (reverse vs) with
        | Just v -> (st', Rval [v])
        | Nothing -> (st', Rerr (Rabort Rtype_error))
        end
    | res -> res
    end
  else (st, Rerr (Rabort Rtype_error))
and
evaluate st env [Var n] =
  match nsLookup env.v n with
  | Just v -> (st, Rval [v])
  | Nothing -> (st, Rerr (Rabort Rtype_error))
  end
and
evaluate st env [Fun x e] = (st, Rval [Closure env x e])
and
evaluate st env [App op es] =
  match fix_clock st (evaluate st env (reverse es)) with
  | (st', Rval vs) ->
      if op = Opapp then
        match do_opapp (reverse vs) with
        | Just (env',e) ->
            if st'.clock = 0 then
              (st', Rerr (Rabort Rtimeout_error))
            else
              evaluate (dec_clock st') env' [e]
        | Nothing -> (st', Rerr (Rabort Rtype_error))
        end
      else if op = Eval then
        match fix_clock st' (do_eval_res (reverse vs) st') with
        | (st1, Rval (env1, decs)) ->
            if st1.clock = 0 then
              (st1, Rerr (Rabort Rtimeout_error))
            else
              match fix_clock (dec_clock st1)
                      (evaluate_decs (dec_clock st1) env1 decs) with
              | (st2, Rval env2) -> match declare_env st2.eval_state
                  (extend_dec_env env2 env1) with
                | Just (x, es2) -> (<| st2 with eval_state =
                    reset_env_generation st'.eval_state es2 |>, Rval [x])
                | Nothing -> (st2, Rerr (Rabort Rtype_error))
                end
              | (st2, Rerr (Rabort a)) -> (st2, Rerr (Rabort a))
              | (st2, Rerr e) -> (<| st2 with eval_state =
                  reset_env_generation st'.eval_state st2.eval_state |>, Rerr e)
              end
        | (st1, Rerr e) -> (st1, Rerr e)
        end
      else
        match do_app (st'.refs,st'.ffi) op (reverse vs) with
        | Just ((refs,ffi),r) -> (<| st' with refs = refs; ffi = ffi |>, list_result r)
        | Nothing -> (st', Rerr (Rabort Rtype_error))
        end
  | res -> res
  end
and
evaluate st env [Log lop e1 e2] =
  match fix_clock st (evaluate st env [e1]) with
  | (st', Rval v1) ->
      match do_log lop (head v1) e2 with
      | Just (Exp e) -> evaluate st' env [e]
      | Just (Val v) -> (st', Rval [v])
      | Nothing -> (st', Rerr (Rabort Rtype_error))
      end
  | res -> res
  end
and
evaluate st env [If e1 e2 e3] =
  match fix_clock st (evaluate st env [e1]) with
  | (st', Rval v) ->
      match do_if (head v) e2 e3 with
      | Just e -> evaluate st' env [e]
      | Nothing -> (st', Rerr (Rabort Rtype_error))
      end
  | res -> res
  end
and
evaluate st env [Mat e pes] =
  match fix_clock st (evaluate st env [e]) with
  | (st', Rval v) ->
      if can_pmatch_all env.c st'.refs (List.map fst pes) (head v)
      then evaluate_match st' env (head v) pes bind_exn_v
      else (st', Rerr (Rabort Rtype_error))
  | res -> res
  end
and
evaluate st env [Let xo e1 e2] =
  match fix_clock st (evaluate st env [e1]) with
  | (st', Rval v) -> evaluate st' <| env with v = nsOptBind xo (head v) env.v |> [e2]
  | res -> res
  end
and
evaluate st env [Letrec funs e] =
  if allDistinct (map (fun (x,y,z) -> x) funs) then
    evaluate st <| env with v = build_rec_env funs env env.v |> [e]
  else
    (st, Rerr (Rabort Rtype_error))
and
evaluate st env [Tannot e t] =
  evaluate st env [e]
and
evaluate st env [Lannot e l] =
  evaluate st env [e]
and
evaluate_match st env v [] err_v = (st, Rerr (Rraise err_v))
and
evaluate_match st env v ((p,e)::pes) err_v  =
  if allDistinct (pat_bindings p []) then
    match pmatch env.c st.refs p v [] with
    | Match env_v' -> evaluate st <| env with v = nsAppend (alist_to_ns env_v') env.v |> [e]
    | No_match -> evaluate_match st env v pes err_v
    | Match_type_error -> (st, Rerr (Rabort Rtype_error))
    end
  else (st, Rerr (Rabort Rtype_error))
and
evaluate_decs st env [] = (st, Rval <| v = nsEmpty; c = nsEmpty |>)
and
evaluate_decs st env (d1::d2::ds) =
  match fix_clock st (evaluate_decs st env [d1]) with
  | (st1, Rval env1) ->
    match evaluate_decs st1 (extend_dec_env env1 env) (d2::ds) with
    | (st2,r) -> (st2, combine_dec_result env1 r)
    end
  | res -> res
  end
and
evaluate_decs st env [Dlet locs p e] =
  if allDistinct (pat_bindings p []) then
    match evaluate st env [e] with
    | (st', Rval v) ->
        (st',
         match pmatch env.c st'.refs p (head v) [] with
         | Match new_vals -> Rval <| v = alist_to_ns new_vals; c = nsEmpty |>
         | No_match -> Rerr (Rraise bind_exn_v)
         | Match_type_error -> Rerr (Rabort Rtype_error)
         end)
    | (st', Rerr err) -> (st', Rerr err)
    end
  else
    (st, Rerr (Rabort Rtype_error))
and
evaluate_decs st env [Dletrec locs funs] =
  (st,
   if allDistinct (map (fun (x,y,z) -> x) funs) then
     Rval <| v = build_rec_env funs env nsEmpty; c = nsEmpty |>
   else
     Rerr (Rabort Rtype_error))
and
evaluate_decs st env [Dtype locs tds] =
  if List.all check_dup_ctors tds then
    (<| st with next_type_stamp = st.next_type_stamp + List.length tds |>,
     Rval <| v = nsEmpty; c = build_tdefs st.next_type_stamp tds |>)
  else
    (st, Rerr (Rabort Rtype_error))
and
evaluate_decs st env [Dtabbrev locs tvs tn t] =
  (st, Rval <| v = nsEmpty; c = nsEmpty |>)
and
evaluate_decs st env [Denv n] =
  match declare_env st.eval_state env with
  | Just (x, es') -> (<| st with eval_state = es' |>,
        Rval <| v = nsSing n x; c = nsEmpty |>)
  | Nothing -> (st, Rerr (Rabort Rtype_error))
  end
and
evaluate_decs st env [Dexn locs cn ts] =
  (<| st with next_exn_stamp = st.next_exn_stamp + 1 |>,
   Rval <| v = nsEmpty; c = nsSing cn (length ts, ExnStamp st.next_exn_stamp) |>)
and
evaluate_decs st env [Dmod mn ds] =
  match evaluate_decs st env ds with
  | (st', r) ->
      (st',
       match r with
       | Rval env' -> Rval <| v = nsLift mn env'.v; c = nsLift mn env'.c |>
       | Rerr err -> Rerr err
       end)
  end
and
evaluate_decs st env [Dlocal lds ds] =
  match fix_clock st (evaluate_decs st env lds) with
  | (st1, Rval env1) ->
    evaluate_decs st1 (extend_dec_env env1 env) ds
  | res -> res
  end

declare {isabelle} rename function evaluate = fun_evaluate
declare {isabelle} rename function evaluate_match = fun_evaluate_match
declare {isabelle} rename function evaluate_decs = fun_evaluate_decs