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
open import FpValTree FpSem

(* 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 do_real_check : forall 'ffi. bool -> result v v -> maybe (result v v)
let do_real_check b r =
  if b then Just r
  else match r with
  | Rval (Real r) -> Nothing
  | _ -> Just r
  end

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) ->
    match (getOpClass op) with
    | FunApp ->
        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
     |EvalOp ->
        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
    | Simple ->
        match do_app (st'.refs,st'.ffi) op (reverse vs) with
        | Nothing -> (st', Rerr (Rabort Rtype_error))
        | Just ((refs,ffi),r) ->
            (<| st' with refs = refs; ffi = ffi |>, list_result r)
        end
    | Icing ->
      match do_app (st'.refs,st'.ffi) op (reverse vs) with
      | Nothing -> (st', Rerr (Rabort Rtype_error))
      | Just ((refs,ffi),r) ->
        let fp_opt =
          if (st'.fp_state.canOpt = FPScope Opt)
          then
            (match (do_fprw r (st'.fp_state.opts 0) (st'.fp_state.rws)) with
            (* if it fails, just use the old value tree *)
            | Nothing -> r
            | Just r_opt -> r_opt
            end)
            (* If we cannot optimize, we should not allow matching on the structure in the oracle *)
          else r
        in
        let stN = if (st'.fp_state.canOpt = FPScope Opt) then shift_fp_opts st' else st' in
        let fp_res =
          if (isFpBool op)
          then match fp_opt with
            | Rval (FP_BoolTree fv) -> Rval (Boolv (compress_bool fv))
            | v -> v
            end
          else fp_opt
        in ((<| stN with refs = refs; ffi = ffi |>), list_result fp_res)
      end
    | Reals ->
      if (st'.fp_state.real_sem) then
      match do_app (st'.refs,st'.ffi) op (reverse vs) with
      | Nothing -> (st', Rerr (Rabort Rtype_error))
      | Just ((refs,ffi),r) ->
        (<| st' with refs = refs; ffi = ffi |>, list_result r)
      end
      else (shift_fp_opts 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 st env [FpOptimise annot e] =
  let newFpState =
    if (st.fp_state.canOpt = Strict)
    then st.fp_state
    else <| st.fp_state with canOpt = FPScope annot|>
  in
    match fix_clock st (evaluate (<| st with fp_state = newFpState |>) env [e]) with
    | (st', Rval vs) ->
    (<| st' with fp_state = <| st'.fp_state with canOpt = st.fp_state.canOpt |> |>,
        Rval (do_fpoptimise annot vs))
    | (st', Rerr e) ->
    (<| st' with fp_state = <| st'.fp_state with canOpt = st.fp_state.canOpt |> |>, Rerr e)
    end
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