evaluate.lem

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

(* 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
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)) -> evaluate_match st' env v pes v
  | 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
        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) ->
      evaluate_match st' env (head v) pes Bindv
  | 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))

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

val evaluate_decs :
  forall 'ffi. list modN -> state 'ffi -> sem_env v -> list dec -> state 'ffi * result (sem_env v) v
let rec
evaluate_decs mn st env [] = (st, Rval <| v = nsEmpty; c = nsEmpty |>)
and
evaluate_decs mn st env (d1::d2::ds) =
  match evaluate_decs mn st env [d1] with
  | (st1, Rval env1) ->
    match evaluate_decs mn st1 (extend_dec_env env1 env) (d2::ds) with
    | (st2,r) -> (st2, combine_dec_result env1 r)
    end
  | res -> res
  end
and
evaluate_decs mn 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 Bindv)
         | Match_type_error -> Rerr (Rabort Rtype_error)
         end)
    | (st', Rerr err) -> (st', Rerr err)
    end
  else
    (st, Rerr (Rabort Rtype_error))
and
evaluate_decs mn 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 mn st env [Dtype locs tds] =
  let new_tdecs = type_defs_to_new_tdecs mn tds in
    if check_dup_ctors tds &&
       disjoint new_tdecs st.defined_types &&
       allDistinct (map (fun (tvs,tn,ctors) -> tn) tds)
    then
      (<| st with defined_types = new_tdecs union st.defined_types |>,
       Rval <| v = nsEmpty; c = build_tdefs mn tds |>)
    else
      (st, Rerr (Rabort Rtype_error))
and
evaluate_decs mn st env [Dtabbrev locs tvs tn t] =
  (st, Rval <| v = nsEmpty; c = nsEmpty |>)
and
evaluate_decs mn st env [Dexn locs cn ts] =
  if TypeExn (mk_id mn cn) IN st.defined_types then
    (st, Rerr (Rabort Rtype_error))
  else
    (<| st with defined_types = {TypeExn (mk_id mn cn)} union st.defined_types |>,
     Rval <| v = nsEmpty; c = nsSing cn (length ts, TypeExn (mk_id mn cn)) |>)
declare termination_argument evaluate_decs = automatic

declare {isabelle} rename function evaluate_decs = fun_evaluate_decs

let envLift mn env =
  <| v = nsLift mn env.v; c = nsLift mn env.c |>

val evaluate_tops :
  forall 'ffi. state 'ffi -> sem_env v -> list top -> state 'ffi *  result (sem_env v) v
let rec
evaluate_tops st env [] = (st, Rval <| v = nsEmpty; c = nsEmpty |>)
and
evaluate_tops st env (top1::top2::tops) =
  match evaluate_tops st env [top1] with
  | (st1, Rval env1) ->
      match evaluate_tops st1 (extend_dec_env env1 env) (top2::tops) with
      | (st2, r) -> (st2, combine_dec_result env1 r)
      end
  | res -> res
  end
and
evaluate_tops st env [Tdec d] = evaluate_decs [] st env [d]
and
evaluate_tops st env [Tmod mn specs ds] =
  if not ([mn] IN st.defined_mods) && no_dup_types ds
  then
    match evaluate_decs [mn] st env ds with
    | (st', r) ->
        (<| st' with defined_mods = {[mn]} union st'.defined_mods |>,
         match r with
         | Rval env' -> Rval <| v = nsLift mn env'.v; c = nsLift mn env'.c |>
         | Rerr err -> Rerr err
         end)
    end
  else
    (st, Rerr (Rabort Rtype_error))
declare termination_argument evaluate_tops = automatic

val evaluate_prog : forall 'ffi. state 'ffi -> sem_env v -> prog -> state 'ffi * result (sem_env v) v
let
evaluate_prog st env prog =
  if no_dup_mods prog st.defined_mods && no_dup_top_types prog st.defined_types then
    evaluate_tops st env prog
  else
    (st, Rerr (Rabort Rtype_error))

declare {isabelle} rename function evaluate_prog = fun_evaluate_prog