semanticPrimitives.lem

(*
  Definitions of semantic primitives (e.g., values, and functions for doing
  primitive operations) used in the semantics.
*)
open import Pervasives
open import Lib
import List_extra
import List
import String
import String_extra
open import Ast
open import Namespace
open import Ffi
open import FpSem FpOpt
open import FpValTree
open import RealOps

(* Constructors and exceptions need unique identities, which we represent by stamps. *)
type stamp =
  (* Each type gets a unique number, and the constructor name must be unique
     inside of the type *)
  | TypeStamp of conN * nat
  | ExnStamp of nat

(*
val type_defs_to_new_tdecs : list modN -> type_def -> set tid_or_exn
let type_defs_to_new_tdecs mn tdefs =
  Set.fromList (List.map (fun (tvs,tn,ctors) -> TypeId (mk_id mn tn)) tdefs)
*)

type sem_env 'v =
  <| v : namespace modN varN 'v
   (* Lexical mapping of constructor idents to arity, stamp pairs *)
   ; c : namespace modN conN (nat * stamp)
   |>

(* Value forms *)
type v =
  | Litv of lit
  (* Constructor application. Can be a tuple or a given constructor of a given type *)
  | Conv of maybe stamp * list v
  (* Function closures
     The environment is used for the free variables in the function *)
  | Closure of sem_env v * varN * exp
  (* Function closure for recursive functions
   * See Closure and Letrec above
   * The last variable name indicates which function from the mutually
   * recursive bundle this closure value represents *)
  | Recclosure of sem_env v * list (varN * varN * exp) * varN
  | Loc of nat
  | Vectorv of list v
  | FP_WordTree of fp_word_val
  | FP_BoolTree of fp_bool_val
  | Real of real
  (* Environment value for Eval, and its numeric identifier *)
  | Env of (sem_env v) * (nat * nat)

(* The runtime semantics should be able to deal with constants too, thus we add
   a translation function from word constants to value trees *)
val fp_translate: v -> maybe v
let rec fp_translate (Litv (Word64 w)) = Just (FP_WordTree (Fp_const w))
    and fp_translate (FP_WordTree v) = Just (FP_WordTree v)
    and fp_translate (FP_BoolTree v) = Just (FP_BoolTree v)
    and fp_translate _ = Nothing

type env_ctor = namespace modN conN (nat * stamp)
type env_val = namespace modN varN v

let bind_stamp = ExnStamp 0
let chr_stamp = ExnStamp 1
let div_stamp = ExnStamp 2
let subscript_stamp = ExnStamp 3

let bind_exn_v = Conv (Just bind_stamp) []
let chr_exn_v = Conv (Just chr_stamp) []
let div_exn_v = Conv (Just div_stamp) []
let sub_exn_v = Conv (Just subscript_stamp) []

let bool_type_num      : nat = 0
let list_type_num      : nat = 1
let option_type_num    : nat = 2
let lit_type_num       : nat = 3
let id_type_num        : nat = 4
let ast_t_type_num     : nat = 5
let pat_type_num       : nat = 6
let lop_type_num       : nat = 7
let opn_type_num       : nat = 8
let opb_type_num       : nat = 9
let opw_type_num       : nat = 10
let shift_type_num     : nat = 11
let word_size_type_num : nat = 12
let fp_uop_type_num    : nat = 13
let fp_bop_type_num    : nat = 14
let fp_top_type_num    : nat = 15
let fp_cmp_type_num    : nat = 16
let real_uop_type_num  : nat = 17
let real_bop_type_num  : nat = 18
let real_cmp_type_num  : nat = 19
let op_type_num        : nat = 20
let locn_type_num      : nat = 21
let locs_type_num      : nat = 22
let fp_opt_num         : nat = 23
let exp_type_num       : nat = 24
let dec_type_num       : nat = 25

(* The result of evaluation *)
type abort =
  | Rtype_error
  | Rtimeout_error
  | Rffi_error of final_event

type error_result 'a =
  | Rraise of 'a (* Should only be a value of type exn *)
  | Rabort of abort

type result 'a 'b =
  | Rval of 'a
  | Rerr of error_result 'b

(* Stores *)
type store_v 'a =
  (* A ref cell *)
    Refv of 'a
  (* A byte array *)
  | W8array of list word8
  (* An array of values *)
  | Varray of list 'a

val store_v_same_type : forall 'a. store_v 'a -> store_v 'a -> bool
let store_v_same_type v1 v2 =
  match (v1,v2) with
  | (Refv _, Refv _) -> true
  | (W8array _,W8array _) -> true
  | (Varray _,Varray _) -> true
  | _ -> false
  end

(* The nth item in the list is the value at location n *)
type store 'a = list (store_v 'a)

val empty_store : forall 'a. store 'a
let empty_store = []

val store_lookup : forall 'a. nat -> store 'a -> maybe (store_v 'a)
let store_lookup l st =
  if l < List.length st then
    Just (List_extra.nth st l)
  else
    Nothing

val store_alloc : forall 'a. store_v 'a -> store 'a -> store 'a * nat
let store_alloc v st =
  ((st ++ [v]), List.length st)

val store_assign : forall 'a. nat -> store_v 'a -> store 'a -> maybe (store 'a)
let store_assign n v st =
  if n < List.length st &&
     store_v_same_type (List_extra.nth st n) v
  then
    Just (List.update st n v)
  else
    Nothing

(*
   State component encapsulating Icing optimizations and rewriter oracle.
   rws := list of rewrites allowed to be applied by the semantics
   opts := oracle that decides which rewrites are applied next
   choices := global counter how many rewriting steps have been done
   canOpt := flag indicating whether evaluation has stepped below an "opt" scope
*)
type optChoice =
  | Strict (* strict 64-bit floating-point semantics, ignores annotations *)
  | FPScope of fp_opt (* currently under scope *)

(* TODO: do we need to `list exp` to assert? *)
type fpState =
  <| rws: list fp_rw
   ; opts: nat -> list rewrite_app
   ; choices: nat
   ; canOpt : optChoice
   ; assertions : nat -> store v -> sem_env v -> bool
   ; real_sem : bool
   |>

(* Compiler checker for Eval. The current design requires the compiler
   to be run (as regular code within the semantics) before Eval is called,
   and these config parameters specify how to interpret the declarations to
   be evaluated and check that the compiler was run correctly. *)
type compiler_args = ((nat * nat) * v * list dec)
type compiler_fun = compiler_args -> maybe (v * list word8 * list word64)

type eval_decs_state =
  <|
    compiler : compiler_fun ;
    (* state must be encoded as v somehow *)
    compiler_state : v ;
    env_id_counter : (nat * nat * nat) ;
    (* decs must also be encoded as v *)
    decode_decs : v -> maybe (list dec)
  |>

(* Alternative mode for Eval including an oracle.
   This is only for use in the compiler proof. *)
type eval_oracle_fun = nat -> compiler_args

type eval_oracle_state =
  <|
    oracle : eval_oracle_fun ;
    custom_do_eval : list v -> eval_oracle_fun ->
        maybe ((nat * nat) * eval_oracle_fun * list dec) ;
    envs : list (list (sem_env v)) ;
    generation : nat
  |>

type eval_state =
    EvalDecs of eval_decs_state
  | EvalOracle of eval_oracle_state

type state 'ffi =
  <| clock : nat
   ; refs  : store v
   ; ffi : ffi_state 'ffi
   ; next_type_stamp : nat
   ; next_exn_stamp : nat
   ; fp_state : fpState
   ; eval_state : maybe eval_state
   |>

(* Other primitives *)
(* Check that a constructor is properly applied *)
val do_con_check : env_ctor -> maybe (id modN conN) -> nat -> bool
let do_con_check cenv n_opt l =
  match n_opt with
    | Nothing -> true
    | Just n ->
        match nsLookup cenv n with
          | Nothing -> false
          | Just (l',_) -> l = l'
        end
  end

val build_conv : env_ctor -> maybe (id modN conN) -> list v -> maybe v
let build_conv envC cn vs =
  match cn with
    | Nothing ->
        Just (Conv Nothing vs)
    | Just id ->
        match nsLookup envC id with
          | Nothing -> Nothing
          | Just (len,stamp) -> Just (Conv (Just stamp) vs)
        end
  end

val lit_same_type : lit -> lit -> bool
let lit_same_type l1 l2 =
  match (l1,l2) with
    | (IntLit _, IntLit _) -> true
    | (Char _, Char _) -> true
    | (StrLit _, StrLit _) -> true
    | (Word8 _, Word8 _) -> true
    | (Word64 _, Word64 _) -> true
    | _ -> false
  end

type match_result 'a =
  | No_match
  | Match_type_error
  | Match of 'a

val same_type : stamp -> stamp -> bool
let rec same_type (TypeStamp _ n1) (TypeStamp _ n2) = n1 = n2
and same_type (ExnStamp _) (ExnStamp _) = true
and same_type _ _ = false

val same_ctor : stamp -> stamp -> bool
let same_ctor stamp1 stamp2 = stamp1 = stamp2

val ctor_same_type : maybe stamp -> maybe stamp -> bool
let ctor_same_type c1 c2 =
  match (c1,c2) with
    | (Nothing, Nothing) -> true
    | (Just stamp1, Just stamp2) -> same_type stamp1 stamp2
    | _ -> false
  end

val Boolv : bool -> v
let Boolv b = if b
  then Conv (Just (TypeStamp "True" bool_type_num)) []
  else Conv (Just (TypeStamp "False" bool_type_num)) []

val compress: v -> v
val compress_list : list v -> list v
let rec compress (FP_WordTree fp) = (Litv (Word64 (compress_word fp)))
    and compress (FP_BoolTree fp) = (Boolv (compress_bool fp))
    and compress (Real r) = Real r
    and compress (Litv l) = (Litv l)
    and compress (Conv ts vs) = Conv ts (compress_list vs)
    and compress (Closure env x e) = Closure env x e
    and compress (Env env n) = Env env n
    and compress (Recclosure env es x) = Recclosure env es x
    and compress (Loc n) = Loc n
    and compress (Vectorv vs) = Vectorv (compress_list vs)
    and compress_list ([]) = []
    and compress_list (v::vs) = (compress v)::(compress_list vs)

(* A big-step pattern matcher.  If the value matches the pattern, return an
 * environment with the pattern variables bound to the corresponding sub-terms
 * of the value; this environment extends the environment given as an argument.
 * No_match is returned when there is no match, but any constructors
 * encountered in determining the match failure are applied to the correct
 * number of arguments, and constructors in corresponding positions in the
 * pattern and value come from the same type.  Match_type_error is returned
 * when one of these conditions is violated *)
val pmatch : env_ctor -> store v -> pat -> v -> alist varN v -> match_result (alist varN v)
let rec
pmatch envC s Pany v' env = Match env
and
pmatch envC s (Pvar x) v' env = Match ((x,v')::env)
and
pmatch envC s (Plit l) (Litv l') env =
  if l = l' then
    Match env
  else if lit_same_type l l' then
    No_match
  else
    Match_type_error
and
pmatch envC s (Pcon (Just n) ps) (Conv (Just stamp') vs) env =
  match nsLookup envC n with
    | Just (l,stamp) ->
        if same_type stamp stamp' && List.length ps = l then
          if same_ctor stamp stamp' then
            if List.length vs = l then
              pmatch_list envC s ps vs env
            else
              Match_type_error
          else
            No_match
        else
          Match_type_error
    | _ -> Match_type_error
  end
and
pmatch envC s (Pcon Nothing ps) (Conv Nothing vs) env =
  if List.length ps = List.length vs then
    pmatch_list envC s ps vs env
  else
    Match_type_error
and
pmatch envC s (Pref p) (Loc lnum) env =
  match store_lookup lnum s with
    | Just (Refv v) -> pmatch envC s p v env
    | Just _ -> Match_type_error
    | Nothing -> Match_type_error
  end
and
pmatch envC s (Pas p i) v env =
  pmatch envC s p v ((i,v)::env)
and
pmatch envC s (Ptannot p t) v env =
  pmatch envC s p v env
and
pmatch envC _ _ _ env = Match_type_error
and
pmatch_list envC s [] [] env = Match env
and
pmatch_list envC s (p::ps) (v::vs) env =
  match pmatch envC s p v env with
    | Match_type_error -> Match_type_error
    | Match env' -> pmatch_list envC s ps vs env'
    | No_match ->
        match pmatch_list envC s ps vs env with
          | Match_type_error -> Match_type_error
          | _ -> No_match
        end
  end
and
pmatch_list envC s _ _ env = Match_type_error

val can_pmatch_all : env_ctor -> store v -> list pat -> v -> bool
let rec
can_pmatch_all envC refs [] v = true
and
can_pmatch_all envC refs (p::ps) v =
  if pmatch envC refs p v [] = Match_type_error
  then false else can_pmatch_all envC refs ps v

(* Bind each function of a mutually recursive set of functions to its closure *)
val build_rec_env : list (varN * varN * exp) -> sem_env v -> env_val -> env_val
let build_rec_env funs cl_env add_to_env =
  foldr
    (fun (f,x,e) env' -> nsBind f (Recclosure cl_env funs f) env')
    add_to_env
    funs

(* Lookup in the list of mutually recursive functions *)
val find_recfun : forall 'a 'b. varN -> list (varN * 'a * 'b) -> maybe ('a * 'b)
let rec find_recfun n funs =
  match funs with
    | [] -> Nothing
    | (f,x,e) :: funs ->
        if f = n then
          Just (x,e)
        else
          find_recfun n funs
  end

declare termination_argument find_recfun = automatic

type eq_result =
  | Eq_val of bool
  | Eq_type_error

val do_eq : v -> v -> eq_result
let rec
do_eq (Litv l1) (Litv l2) =
  if lit_same_type l1 l2 then Eq_val (l1 = l2)
  else Eq_type_error
and
do_eq (Loc l1) (Loc l2) = Eq_val (l1 = l2)
and
do_eq (Conv cn1 vs1) (Conv cn2 vs2) =
  if cn1 = cn2 && (List.length vs1 = List.length vs2) then
    do_eq_list vs1 vs2
  else if ctor_same_type cn1 cn2 then
    Eq_val false
  else
    Eq_type_error
and
do_eq (Vectorv vs1) (Vectorv vs2) =
  if List.length vs1 = List.length vs2 then
    do_eq_list vs1 vs2
  else
    Eq_val false
and
do_eq (Closure _ _ _) (Closure _ _ _) = Eq_val true
and
do_eq (Closure _ _ _) (Recclosure _ _ _) = Eq_val true
and
do_eq (Recclosure _ _ _) (Closure _ _ _) = Eq_val true
and
do_eq (Recclosure _ _ _) (Recclosure _ _ _) = Eq_val true
and
do_eq (FP_BoolTree v1) (FP_BoolTree v2) = Eq_val (compress_bool v1 = compress_bool v2)
and
do_eq (FP_BoolTree v1) (Conv cn2 vs2) =
  match Boolv (compress_bool v1) with
  | Conv cn1 vs1 ->
    if cn1 = cn2 && (List.length vs1 = List.length vs2) then
      do_eq_list vs1 vs2
      else if ctor_same_type cn1 cn2 then
         Eq_val false
      else
        Eq_type_error
  | _ -> Eq_type_error
  end
and
do_eq (Conv cn1 vs1) (FP_BoolTree v2) =
  match Boolv (compress_bool v2) with
  | Conv cn2 vs2 ->
    if cn1 = cn2 && (List.length vs1 = List.length vs2) then
      do_eq_list vs1 vs2
      else if ctor_same_type cn1 cn2 then
         Eq_val false
      else
        Eq_type_error
  | _ -> Eq_type_error
  end
and
do_eq (FP_WordTree v1) (FP_WordTree v2) = Eq_val (compress_word v1 = compress_word v2)
and
do_eq (Litv (Word64 w1)) (FP_WordTree v2) = Eq_val (w1 = compress_word v2)
and
do_eq (FP_WordTree v1) (Litv (Word64 w2)) = Eq_val (compress_word v1 = w2)
and
do_eq (Real r1) (Real r2) = Eq_val (r1 = r2)
and
do_eq (Env _ (gen1, id1)) (Env _ (gen2, id2)) = Eq_val (gen1 = gen2 && id1 = id2)
and
do_eq _ _ = Eq_type_error
and
do_eq_list [] [] = Eq_val true
and
do_eq_list (v1::vs1) (v2::vs2) =
  match do_eq v1 v2 with
    | Eq_type_error -> Eq_type_error
    | Eq_val r ->
        if not r then
          Eq_val false
        else
          do_eq_list vs1 vs2
  end
and
do_eq_list _ _ = Eq_val false

(* Do an application *)
val do_opapp : list v -> maybe (sem_env v * exp)
let do_opapp vs =
  match vs with
  | [Closure env n e; v] ->
      Just (<| env with v = nsBind n v env.v |>, e)
  | [Recclosure env funs n; v] ->
      if allDistinct (List.map (fun (f,x,e) -> f) funs) then
        match find_recfun n funs with
          | Just (n,e) -> Just (<| env with v = nsBind n v (build_rec_env funs env env.v) |>, e)
          | Nothing -> Nothing
        end
      else
        Nothing
  | _ -> Nothing
  end

(* If a value represents a list, get that list. Otherwise return Nothing *)
val v_to_list : v -> maybe (list v)
let rec v_to_list (Conv (Just stamp) []) =
  if stamp = TypeStamp "[]" list_type_num then
    Just []
  else
    Nothing
and v_to_list (Conv (Just stamp) [v1;v2]) =
  if stamp = TypeStamp "::" list_type_num then
    match v_to_list v2 with
      | Just vs -> Just (v1::vs)
      | Nothing -> Nothing
    end
  else
    Nothing
and v_to_list _ = Nothing

val list_to_v : list v -> v
let rec list_to_v [] = Conv (Just (TypeStamp "[]" list_type_num)) []
and list_to_v (x::xs) = Conv (Just (TypeStamp "::" list_type_num)) [x; list_to_v xs]

val v_to_char_list : v -> maybe (list char)
let rec v_to_char_list (Conv (Just stamp) []) =
  if stamp = TypeStamp "[]" list_type_num then
    Just []
  else
    Nothing
and v_to_char_list (Conv (Just stamp) [Litv (Char c);v]) =
  if stamp = TypeStamp "::" list_type_num then
    match v_to_char_list v with
      | Just cs -> Just (c::cs)
      | Nothing -> Nothing
    end
  else
    Nothing
and v_to_char_list _ = Nothing

val vs_to_string : list v -> maybe string
let rec vs_to_string [] = Just ""
and vs_to_string (Litv(StrLit s1)::vs) =
  match vs_to_string vs with
  | Just s2 -> Just (s1 ^ s2)
  | _ -> Nothing
  end
and vs_to_string _ = Nothing

val maybe_to_v : maybe v -> v
let rec maybe_to_v Nothing =
  Conv (Just (TypeStamp "None" option_type_num)) []
and maybe_to_v (Just v) =
  Conv (Just (TypeStamp "Some" option_type_num)) [v]

val v_to_id : v -> maybe (id modN varN)
let rec v_to_id (Conv (Just stamp) [Litv (StrLit s)]) =
  if stamp = TypeStamp "Short" id_type_num then
    Just (Short s)
  else
    Nothing
and v_to_id (Conv (Just stamp) [Litv (StrLit s); v]) =
  if stamp = TypeStamp "Long" id_type_num then
    match v_to_id v with
      | Just id -> Just (Long s id)
      | Nothing -> Nothing
    end
  else
    Nothing
and v_to_id _ = Nothing
declare termination_argument v_to_id = automatic

val enc_pair : v -> v -> v
let enc_pair v1 v2 = Conv Nothing [v1; v2]

val enc_list : list v -> v
let rec
  enc_list [] =
    Conv (Just (TypeStamp "[]" list_type_num)) []
and
  enc_list (x::xs) =
    Conv (Just (TypeStamp "::" list_type_num)) [x; enc_list xs]

val enc_option : maybe v -> v
let rec
  enc_option Nothing =
    Conv (Just (TypeStamp "None" option_type_num)) []
and
  enc_option (Just x) =
    Conv (Just (TypeStamp "Some" option_type_num)) [x]

val enc_lit : lit -> v
let rec
  enc_lit (Word64 w) =
    Conv (Just (TypeStamp "Word64" lit_type_num)) [Litv (Word64 w)]
and
  enc_lit (Word8 b) =
    Conv (Just (TypeStamp "Word8" lit_type_num)) [Litv (Word8 b)]
and
  enc_lit (StrLit s) =
    Conv (Just (TypeStamp "Strlit" lit_type_num)) [Litv (StrLit s)]
and
  enc_lit (Char c) =
    Conv (Just (TypeStamp "Char" lit_type_num)) [Litv (Char c)]
and
  enc_lit (IntLit i) =
    Conv (Just (TypeStamp "Intlit" lit_type_num)) [Litv (IntLit i)]

val enc_id : id modN typeN -> v
let rec
  enc_id (Short s) =
    Conv (Just (TypeStamp "Short" id_type_num)) [Litv (StrLit s)]
and
  enc_id (Long s i) =
    Conv (Just (TypeStamp "Long" id_type_num)) [Litv (StrLit s); enc_id i]

val enc_ast_t : ast_t -> v
let rec
  enc_ast_t (Atapp x y) =
    Conv (Just (TypeStamp "Atapp" ast_t_type_num))
      [enc_list (List.map enc_ast_t x); enc_id y]
and
  enc_ast_t (Attup x) =
    Conv (Just (TypeStamp "Attup" ast_t_type_num))
      [enc_list (List.map enc_ast_t x)]
and
  enc_ast_t (Atfun x_3 x_2) =
    Conv (Just (TypeStamp "Atfun" ast_t_type_num))
      [enc_ast_t x_3; enc_ast_t x_2]
and
  enc_ast_t (Atvar x_1) =
    Conv (Just (TypeStamp "Atvar" ast_t_type_num)) [Litv (StrLit x_1)]

val enc_pat : pat -> v
let rec
  enc_pat (Ptannot x_9 x_8) =
    Conv (Just (TypeStamp "Ptannot" pat_type_num))
      [enc_pat x_9; enc_ast_t x_8]
and
  enc_pat (Pref x_7) =
    Conv (Just (TypeStamp "Pref" pat_type_num))
      [enc_pat x_7]
and
  enc_pat (Pas x_6 x_5) =
    Conv (Just (TypeStamp "Pas" pat_type_num))
      [enc_pat x_6; Litv (StrLit x_5)]
and
  enc_pat (Pcon x_4 x_3) =
    Conv (Just (TypeStamp "Pcon" pat_type_num))
      [enc_option (option_map enc_id x_4); enc_list (List.map enc_pat x_3)]
and
  enc_pat (Plit x_2) =
    Conv (Just (TypeStamp "Plit" pat_type_num))
      [enc_lit x_2]
and
  enc_pat (Pvar x_1) =
    Conv (Just (TypeStamp "Pvar" pat_type_num))
      [Litv (StrLit x_1)]
and
  enc_pat Pany =
    Conv (Just (TypeStamp "Pany" pat_type_num)) []

val enc_lop : lop -> v
let rec
  enc_lop Or = Conv (Just (TypeStamp "Or" lop_type_num)) []
and
  enc_lop And = Conv (Just (TypeStamp "And" lop_type_num)) []

val enc_opn : opn -> v
let rec
  enc_opn Modulo = Conv (Just (TypeStamp "Modulo" opn_type_num)) []
and
  enc_opn Divide = Conv (Just (TypeStamp "Divide" opn_type_num)) []
and
  enc_opn Times = Conv (Just (TypeStamp "Times" opn_type_num)) []
and
  enc_opn Minus = Conv (Just (TypeStamp "Minus" opn_type_num)) []
and
  enc_opn Plus = Conv (Just (TypeStamp "Plus" opn_type_num)) []

val enc_opb : opb -> v
let rec
  enc_opb Geq = Conv (Just (TypeStamp "Geq" opb_type_num)) []
and
  enc_opb Leq = Conv (Just (TypeStamp "Leq" opb_type_num)) []
and
  enc_opb Gt = Conv (Just (TypeStamp "Gt" opb_type_num)) []
and
  enc_opb Lt = Conv (Just (TypeStamp "Lt" opb_type_num)) []

val enc_opw : opw -> v
let rec
  enc_opw Sub = Conv (Just (TypeStamp "Sub" opw_type_num)) []
and
  enc_opw Add = Conv (Just (TypeStamp "Add" opw_type_num)) []
and
  enc_opw Xor = Conv (Just (TypeStamp "Xor" opw_type_num)) []
and
  enc_opw Orw = Conv (Just (TypeStamp "Orw" opw_type_num)) []
and
  enc_opw Andw = Conv (Just (TypeStamp "Andw" opw_type_num)) []

val enc_shift : shift -> v
let rec
  enc_shift Ror = Conv (Just (TypeStamp "Ror" shift_type_num)) []
and
  enc_shift Asr = Conv (Just (TypeStamp "Asr" shift_type_num)) []
and
  enc_shift Lsr = Conv (Just (TypeStamp "Lsr" shift_type_num)) []
and
  enc_shift Lsl = Conv (Just (TypeStamp "Lsl" shift_type_num)) []

val enc_word_size : word_size -> v
let rec
  enc_word_size W64 = Conv (Just (TypeStamp "W64" word_size_type_num)) []
and
  enc_word_size W8 = Conv (Just (TypeStamp "W8" word_size_type_num)) []

val enc_fp_uop : fp_uop -> v
let rec
  enc_fp_uop FP_Sqrt = Conv (Just (TypeStamp "Fp_sqrt" fp_uop_type_num)) []
and
  enc_fp_uop FP_Neg = Conv (Just (TypeStamp "Fp_neg" fp_uop_type_num)) []
and
  enc_fp_uop FP_Abs = Conv (Just (TypeStamp "Fp_abs" fp_uop_type_num)) []

val enc_fp_bop : fp_bop -> v
let rec
  enc_fp_bop FP_Div = Conv (Just (TypeStamp "Fp_div" fp_bop_type_num)) []
and
  enc_fp_bop FP_Mul = Conv (Just (TypeStamp "Fp_mul" fp_bop_type_num)) []
and
  enc_fp_bop FP_Sub = Conv (Just (TypeStamp "Fp_sub" fp_bop_type_num)) []
and
  enc_fp_bop FP_Add = Conv (Just (TypeStamp "Fp_add" fp_bop_type_num)) []

val enc_fp_top : fp_top -> v
let rec
  enc_fp_top FP_Fma = Conv (Just (TypeStamp "Fp_fma" fp_top_type_num)) []

val enc_fp_cmp : fp_cmp -> v
let rec
  enc_fp_cmp FP_Equal =
    Conv (Just (TypeStamp "Fp_equal" fp_cmp_type_num)) []
and
  enc_fp_cmp FP_GreaterEqual =
    Conv (Just (TypeStamp "Fp_greaterequal" fp_cmp_type_num)) []
and
  enc_fp_cmp FP_Greater =
    Conv (Just (TypeStamp "Fp_greater" fp_cmp_type_num)) []
and
  enc_fp_cmp FP_LessEqual =
    Conv (Just (TypeStamp "Fp_lessequal" fp_cmp_type_num)) []
and
  enc_fp_cmp FP_Less =
    Conv (Just (TypeStamp "Fp_less" fp_cmp_type_num)) []

val enc_real_uop : real_uop -> v
let rec
  enc_real_uop Real_Sqrt = Conv (Just (TypeStamp "Real_sqrt" real_uop_type_num)) []
and
  enc_real_uop Real_Neg = Conv (Just (TypeStamp "Real_neg" real_uop_type_num)) []
and
  enc_real_uop Real_Abs = Conv (Just (TypeStamp "Real_abs" real_uop_type_num)) []

val enc_real_bop : real_bop -> v
let rec
  enc_real_bop Real_Div = Conv (Just (TypeStamp "Real_div" real_bop_type_num)) []
and
  enc_real_bop Real_Mul = Conv (Just (TypeStamp "Real_mul" real_bop_type_num)) []
and
  enc_real_bop Real_Sub = Conv (Just (TypeStamp "Real_sub" real_bop_type_num)) []
and
  enc_real_bop Real_Add = Conv (Just (TypeStamp "Real_add" real_bop_type_num)) []

val enc_real_cmp : real_cmp -> v
let rec
  enc_real_cmp Real_Equal =
    Conv (Just (TypeStamp "Real_equal" real_cmp_type_num)) []
and
  enc_real_cmp Real_GreaterEqual =
    Conv (Just (TypeStamp "Real_greaterequal" real_cmp_type_num)) []
and
  enc_real_cmp Real_Greater =
    Conv (Just (TypeStamp "Real_greater" real_cmp_type_num)) []
and
  enc_real_cmp Real_LessEqual =
    Conv (Just (TypeStamp "Real_lessequal" real_cmp_type_num)) []
and
  enc_real_cmp Real_Less =
    Conv (Just (TypeStamp "Real_less" real_cmp_type_num)) []


val nat_to_v : nat -> v
let nat_to_v n = Litv (IntLit (integerFromNat n))

val enc_op : op -> v
let rec
  enc_op Eval = Conv (Just (TypeStamp "Eval" op_type_num)) []
and
  enc_op Env_id = Conv (Just (TypeStamp "Env_id" op_type_num)) []
and
  enc_op (FFI x_15) =
    Conv (Just (TypeStamp "Ffi" op_type_num)) [Litv (StrLit x_15)]
and
  enc_op ConfigGC = Conv (Just (TypeStamp "Configgc" op_type_num)) []
and
  enc_op ListAppend = Conv (Just (TypeStamp "Listappend" op_type_num)) []
and
  enc_op Aupdate = Conv (Just (TypeStamp "Aupdate" op_type_num)) []
and
  enc_op Alength = Conv (Just (TypeStamp "Alength" op_type_num)) []
and
  enc_op Asub = Conv (Just (TypeStamp "Asub" op_type_num)) []
and
  enc_op AallocEmpty = Conv (Just (TypeStamp "Aallocempty" op_type_num)) []
and
  enc_op Aalloc = Conv (Just (TypeStamp "Aalloc" op_type_num)) []
and
  enc_op Aupdate_unsafe =
    Conv (Just (TypeStamp "Aupdate_unsafe" op_type_num)) []
and
  enc_op Asub_unsafe = Conv (Just (TypeStamp "Asub_unsafe" op_type_num)) []
and
  enc_op Vlength = Conv (Just (TypeStamp "Vlength" op_type_num)) []
and
  enc_op Vsub = Conv (Just (TypeStamp "Vsub" op_type_num)) []
and
  enc_op VfromList = Conv (Just (TypeStamp "Vfromlist" op_type_num)) []
and
  enc_op Strcat = Conv (Just (TypeStamp "Strcat" op_type_num)) []
and
  enc_op Strlen = Conv (Just (TypeStamp "Strlen" op_type_num)) []
and
  enc_op Strsub = Conv (Just (TypeStamp "Strsub" op_type_num)) []
and
  enc_op Explode = Conv (Just (TypeStamp "Explode" op_type_num)) []
and
  enc_op Implode = Conv (Just (TypeStamp "Implode" op_type_num)) []
and
  enc_op (Chopb x_14) =
    Conv (Just (TypeStamp "Chopb" op_type_num)) [enc_opb x_14]
and
  enc_op Chr = Conv (Just (TypeStamp "Chr_1" op_type_num)) []
and
  enc_op Ord = Conv (Just (TypeStamp "Ord" op_type_num)) []
and
  enc_op CopyAw8Aw8 = Conv (Just (TypeStamp "Copyaw8aw8" op_type_num)) []
and
  enc_op CopyAw8Str = Conv (Just (TypeStamp "Copyaw8str" op_type_num)) []
and
  enc_op CopyStrAw8 = Conv (Just (TypeStamp "Copystraw8" op_type_num)) []
and
  enc_op CopyStrStr = Conv (Just (TypeStamp "Copystrstr" op_type_num)) []
and
  enc_op (WordToInt x_13) =
    Conv (Just (TypeStamp "Wordtoint" op_type_num)) [enc_word_size x_13]
and
  enc_op (WordFromInt x_12) =
    Conv (Just (TypeStamp "Wordfromint" op_type_num)) [enc_word_size x_12]
and
  enc_op Aw8update = Conv (Just (TypeStamp "Aw8update" op_type_num)) []
and
  enc_op Aw8length = Conv (Just (TypeStamp "Aw8length" op_type_num)) []
and
  enc_op Aw8sub = Conv (Just (TypeStamp "Aw8sub" op_type_num)) []
and
  enc_op Aw8alloc = Conv (Just (TypeStamp "Aw8alloc" op_type_num)) []
and
  enc_op Aw8sub_unsafe = Conv (Just (TypeStamp "Aw8sub_unsafe" op_type_num)) []
and
  enc_op Aw8update_unsafe =
    Conv (Just (TypeStamp "Aw8update_unsafe" op_type_num)) []
and
  enc_op Opderef = Conv (Just (TypeStamp "Opderef" op_type_num)) []
and
  enc_op Opref = Conv (Just (TypeStamp "Opref" op_type_num)) []
and
  enc_op Opassign = Conv (Just (TypeStamp "Opassign" op_type_num)) []
and
  enc_op Opapp = Conv (Just (TypeStamp "Opapp" op_type_num)) []
and
  enc_op (FP_top x_11) =
    Conv (Just (TypeStamp "Fp_top" op_type_num)) [enc_fp_top x_11]
and
  enc_op (FP_bop x_10) =
    Conv (Just (TypeStamp "Fp_bop" op_type_num)) [enc_fp_bop x_10]
and
  enc_op (FP_uop x_9) =
    Conv (Just (TypeStamp "Fp_uop" op_type_num)) [enc_fp_uop x_9]
and
  enc_op (FP_cmp x_8) =
    Conv (Just (TypeStamp "Fp_cmp" op_type_num)) [enc_fp_cmp x_8]
and
  enc_op (FpFromWord) =
    Conv (Just (TypeStamp "Fpfromword" op_type_num)) []
and
  enc_op (FpToWord) =
    Conv (Just (TypeStamp "Fptoword" op_type_num)) []
and
  enc_op (Real_bop x_10) =
    Conv (Just (TypeStamp "Real_bop" op_type_num)) [enc_real_bop x_10]
and
  enc_op (Real_uop x_9) =
    Conv (Just (TypeStamp "Real_uop" op_type_num)) [enc_real_uop x_9]
and
  enc_op (Real_cmp x_8) =
    Conv (Just (TypeStamp "Real_cmp" op_type_num)) [enc_real_cmp x_8]
and
  enc_op (RealFromFP) =
    Conv (Just (TypeStamp "Realfromfp" op_type_num)) []
and
  enc_op Equality = Conv (Just (TypeStamp "Equality" op_type_num)) []
and
  enc_op (Shift x_7 x_6 x_5) =
    Conv (Just (TypeStamp "Shift" op_type_num))
      [enc_word_size x_7; enc_shift x_6; nat_to_v x_5]
and
  enc_op (Opw x_4 x_3) =
    Conv (Just (TypeStamp "Opw" op_type_num)) [enc_word_size x_4; enc_opw x_3]
and
  enc_op (Opb x_2) =
    Conv (Just (TypeStamp "Opb" op_type_num)) [enc_opb x_2]
and
  enc_op (Opn x_1) =
    Conv (Just (TypeStamp "Opn" op_type_num)) [enc_opn x_1]

val maybe_all_list : forall 'a. list (maybe 'a) -> maybe (list 'a)
let rec maybe_all_list v =
  match v with
  | [] -> Just []
  | (Nothing :: _) -> Nothing
  | (Just x :: vs) -> match maybe_all_list vs with
    | Just xs -> Just (x :: xs)
    | Nothing -> Nothing
    end
  end

val v_to_word8 : v -> maybe word8
let v_to_word8 v = match v with
  | Litv (Word8 w) -> Just w
  | _ -> Nothing
  end

val v_to_word8_list : v -> maybe (list word8)
let v_to_word8_list v = match v_to_list v with
  | Just xs -> maybe_all_list (List.map v_to_word8 xs)
  | Nothing -> Nothing
  end

val v_to_word64 : v -> maybe word64
let v_to_word64 v = match v with
  | Litv (Word64 w) -> Just w
  | _ -> Nothing
  end

val v_to_word64_list : v -> maybe (list word64)
let v_to_word64_list v = match v_to_list v with
  | Just xs -> maybe_all_list (List.map v_to_word64 xs)
  | Nothing -> Nothing
  end

val lookup_env : eval_oracle_state -> (nat * nat) -> maybe (sem_env v)
let lookup_env s (i, j) = match List.index s.envs i with
  | Nothing -> Nothing
  | Just gen_envs -> List.index gen_envs j
  end

val add_decs_generation : eval_decs_state -> eval_decs_state
let add_decs_generation s = match s.env_id_counter with
  | (cur_gen, next_id, next_gen) -> <| s with env_id_counter =
        (next_gen, 0, next_gen + 1) |>
  end

val add_env_generation : eval_oracle_state -> eval_oracle_state
let add_env_generation s = <| s with
    generation = List.length s.envs ;
    envs = List.append s.envs [[]] |>

val declare_env : maybe eval_state -> sem_env v -> maybe (v * maybe eval_state)
let declare_env es env = match es with
  | Nothing -> Nothing
  | Just (EvalDecs s) -> match s.env_id_counter with
    | (cur_gen, next_id, next_gen) -> Just (Env env (cur_gen, next_id),
        Just (EvalDecs <| s with env_id_counter =
            (cur_gen, next_id + 1, next_gen) |>))
    end
  | Just (EvalOracle s) -> match (List.index s.envs s.generation) with
    | Just gen_envs -> Just (Conv Nothing
            [nat_to_v s.generation; nat_to_v (List.length gen_envs)],
        Just (EvalOracle <| s with envs = List.update s.envs s.generation
            (List.append gen_envs [env]) |>))
    | Nothing -> Nothing
    end
  end

(* Concrete, or first-order values, which do not contain code closures and
   are unchanged by many compiler phases. *)
val concrete_v : v -> bool
let rec concrete_v v = match v with
  | Litv _ -> true
  | Loc _ -> true
  | Vectorv vs -> concrete_v_list vs
  | Conv _ vs -> concrete_v_list vs
  | _ -> false
  end
and
  concrete_v_list [] = true
and
  concrete_v_list (v :: vs) = (concrete_v v && concrete_v_list vs)

val compiler_agrees : compiler_fun -> compiler_args -> v * v * v -> bool
let compiler_agrees f args (st_v, bs_v, ws_v) = match
    (f args, args, v_to_word8_list bs_v, v_to_word64_list ws_v)
  with
  | (Just (st, c_bs, c_ws), (_, prev_st_v, _), Just bs, Just ws) ->
    st = st_v && c_bs = bs && c_ws = ws && concrete_v st_v &&
        concrete_v prev_st_v
  | _ -> false
  end

(* get the declarations to be evaluated in the various Eval semantics *)
val do_eval : list v -> maybe eval_state ->
        maybe (sem_env v * list dec * maybe eval_state)
let do_eval vs es =
  match (es, vs) with
  | (Just (EvalDecs s), [Env env id; st_v; decs_v; st_v2; bs_v; ws_v]) ->
    match s.decode_decs decs_v with
    | Just decs -> if st_v = s.compiler_state && concrete_v decs_v &&
            compiler_agrees s.compiler (id, st_v, decs) (st_v2, bs_v, ws_v)
        then Just (env, decs, Just (EvalDecs
            (add_decs_generation <| s with compiler_state = st_v2 |>)))
        else Nothing
    | _ -> Nothing
    end
  | (Just (EvalOracle s), vs) -> match s.custom_do_eval vs s.oracle with
    | Just (env_id, oracle, decs) -> match lookup_env s env_id with
      | Just env -> Just (env, decs, Just (EvalOracle
            (add_env_generation <| s with oracle = oracle |>)))
      | _ -> Nothing
      end
    | _ -> Nothing
    end
  | _ -> Nothing
  end

(* conclude an Eval generation *)
val reset_env_generation : maybe eval_state -> maybe eval_state -> maybe eval_state
let reset_env_generation prior_es es = match (prior_es, es) with
  | (Just (EvalOracle prior_s), Just (EvalOracle s)) ->
    Just (EvalOracle <| s with generation = prior_s.generation |>)
  | (Just (EvalDecs prior_s), Just (EvalDecs s)) -> match
        (prior_s.env_id_counter, s.env_id_counter) with
    | ((cur_gen, next_id, _), (_, _, next_gen)) ->
    Just (EvalDecs <| s with env_id_counter = (cur_gen, next_id, next_gen) |>)
    end
  | _ -> es
  end

val copy_array : forall 'a. list 'a * integer -> integer -> maybe (list 'a * integer) -> maybe (list 'a)
let copy_array (src,srcoff) len d =
  if srcoff < 0 || len < 0 || List.length src < natFromInteger(srcoff + len) then Nothing else
    let copied = List.take (natFromInteger len) (List.drop (natFromInteger srcoff) src) in
    match d with
    | Just (dst,dstoff) ->
        if dstoff < 0 || List.length dst < natFromInteger(dstoff + len) then Nothing else
          Just (List.take (natFromInteger dstoff) dst ++
                copied ++
                List.drop (natFromInteger (dstoff + len)) dst)
    | Nothing -> Just copied
    end

val ws_to_chars : list word8 -> list char
let ws_to_chars ws = List.map (fun w -> String_extra.chr(natFromWord8 w)) ws

val chars_to_ws : list char -> list word8
let chars_to_ws cs = List.map (fun c -> word8FromInteger(integerFromNat(String_extra.ord c))) cs

val opn_lookup : opn -> integer -> integer -> integer
let opn_lookup n : integer -> integer -> integer = match n with
  | Plus -> (+)
  | Minus -> (-)
  | Times -> ( * )
  | Divide -> (/)
  | Modulo -> (mod)
end

val opb_lookup : opb -> integer -> integer -> bool
let opb_lookup n : integer -> integer -> bool = match n with
  | Lt -> (<)
  | Gt -> (>)
  | Leq -> (<=)
  | Geq -> (>=)
end

val opw8_lookup : opw -> word8 -> word8 -> word8
let opw8_lookup op = match op with
  | Andw -> W8and
  | Orw -> W8or
  | Xor -> W8xor
  | Add -> W8add
  | Sub -> W8sub
end

val opw64_lookup : opw -> word64 -> word64 -> word64
let opw64_lookup op = match op with
  | Andw -> W64and
  | Orw -> W64or
  | Xor -> W64xor
  | Add -> W64add
  | Sub -> W64sub
end

val shift8_lookup : shift -> word8 -> nat -> word8
let shift8_lookup sh = match sh with
  | Lsl -> W8lsl
  | Lsr -> W8lsr
  | Asr -> W8asr
  | Ror -> W8ror
end

val shift64_lookup : shift -> word64 -> nat -> word64
let shift64_lookup sh = match sh with
  | Lsl -> W64lsl
  | Lsr -> W64lsr
  | Asr -> W64asr
  | Ror -> W64ror
end

type exp_or_val =
  | Exp of exp
  | Val of v

type store_ffi 'ffi 'v = store 'v * ffi_state 'ffi

val do_fprw: result v v -> list rewrite_app -> list fp_rw -> maybe (result v v)
let do_fprw v fp_opt fp_rws =
  match (v, fp_opt) with
  | (Rval (FP_BoolTree fv), rws) ->
    match rwAllBoolTree rws fp_rws fv with
    | Nothing -> Nothing
    | Just fv_opt -> Just (Rval (FP_BoolTree fv_opt))
    end
  | (Rval (FP_WordTree fv), rws) ->
    match rwAllWordTree rws fp_rws fv with
    | Nothing -> Nothing
    | Just fv_opt -> Just (Rval (FP_WordTree fv_opt))
    end
  | (Rval r, [] ) -> Just v
  | (_, _) -> Nothing
  end

val do_fpoptimise : fp_opt -> list v -> list v
let rec do_fpoptimise sc [] = []
    and do_fpoptimise sc [Litv l] =
        [Litv l]
    and do_fpoptimise sc [Conv st vs] =
        [Conv st (do_fpoptimise sc vs)]
    and do_fpoptimise sc [Closure env x e] =
        [Closure env x e]
    and do_fpoptimise sc [Recclosure env ls x] =
        [Recclosure env ls x]
    and do_fpoptimise sc [Loc n] =
        [Loc n]
    and do_fpoptimise sc [Vectorv vs] =
        [Vectorv (do_fpoptimise sc vs)]
    and do_fpoptimise sc [Real r] = [Real r]
    and do_fpoptimise sc [FP_WordTree fp] =
        [FP_WordTree (Fp_wopt sc fp)]
    and do_fpoptimise sc [FP_BoolTree fp] =
        [FP_BoolTree (Fp_bopt sc fp)]
    and do_fpoptimise sc [Env env n] =
        [Env env n]
    and do_fpoptimise sc (v::vs) =
        (do_fpoptimise sc [v]) ++ (do_fpoptimise sc vs)

val do_app : forall 'ffi. store_ffi 'ffi v -> op -> list v -> maybe (store_ffi 'ffi v * result v v)
let do_app ((s:store v),(t:ffi_state 'ffi)) op vs =
  match (op, vs) with
    | (ListAppend, [x1; x2]) ->
      match (v_to_list x1, v_to_list x2) with
        | (Just xs, Just ys) -> Just ((s,t), Rval (list_to_v (xs ++ ys)))
        | _ -> Nothing
      end
    | (Opn op, [Litv (IntLit n1); Litv (IntLit n2)]) ->
        if (op = Divide || (op = Modulo)) && (n2 = 0) then
          Just ((s,t), Rerr (Rraise div_exn_v))
        else
          Just ((s,t), Rval (Litv (IntLit (opn_lookup op n1 n2))))
    | (Opb op, [Litv (IntLit n1); Litv (IntLit n2)]) ->
        Just ((s,t), Rval (Boolv (opb_lookup op n1 n2)))
    | (Opw W8 op, [Litv (Word8 w1); Litv (Word8 w2)]) ->
        Just ((s,t), Rval (Litv (Word8 (opw8_lookup op w1 w2))))
    | (Opw W64 op, [Litv (Word64 w1); Litv (Word64 w2)]) ->
        Just ((s,t), Rval (Litv (Word64 (opw64_lookup op w1 w2))))
    | (Opw W64 op, [FP_WordTree w1; Litv (Word64 w2)]) ->
        let wr1 = compress_word w1 in
          Just ((s,t), Rval (Litv (Word64 (opw64_lookup op wr1 w2))))
    | (Opw W64 op, [Litv (Word64 w1); FP_WordTree w2]) ->
        let wr2 = compress_word w2 in
          Just ((s,t), Rval (Litv (Word64 (opw64_lookup op w1 wr2))))
    | (Opw W64 op, [FP_WordTree w1; FP_WordTree w2]) ->
        let wr1 = compress_word w1 in
        let wr2 = compress_word w2 in
          Just ((s,t), Rval (Litv (Word64 (opw64_lookup op wr1 wr2))))
    | (FP_top t_op, [v1; v2; v3]) ->
        match (fp_translate v1, fp_translate v2, fp_translate v3) with
        | (Just (FP_WordTree w1), Just (FP_WordTree w2), Just (FP_WordTree w3)) ->
          Just ((s,t), Rval (FP_WordTree (fp_top t_op w1 w2 w3)))
        | _ -> Nothing
        end
    | (FP_bop bop, [v1; v2]) ->
        match (fp_translate v1, fp_translate v2) with
        | (Just (FP_WordTree w1), Just (FP_WordTree w2)) ->
          Just ((s,t),Rval (FP_WordTree (fp_bop bop w1 w2)))
        | _ -> Nothing
        end
    | (FP_uop uop, [v1]) ->
        match (fp_translate v1) with
        | (Just (FP_WordTree w1)) ->
          Just ((s,t),Rval (FP_WordTree (fp_uop uop w1)))
        | _ -> Nothing
        end
    | (FP_cmp cmp, [v1; v2]) ->
        match (fp_translate v1, fp_translate v2) with
        | (Just (FP_WordTree w1), Just (FP_WordTree w2)) ->
          Just ((s,t),Rval (FP_BoolTree (fp_cmp cmp w1 w2)))
        | _ -> Nothing
        end
    | (FpToWord, [FP_WordTree v1]) -> Just ((s,t), Rval (Litv (Word64 (compress_word v1))))
    | (FpFromWord, [Litv (Word64 v1)]) -> (Just ((s,t), Rval (FP_WordTree (Fp_const v1))))
    | (Real_cmp cmp, [Real v1; Real v2]) ->
        Just ((s,t), Rval (Boolv (real_cmp cmp v1 v2)))
    | (Real_bop bop, [Real v1; Real v2]) ->
        Just ((s,t), Rval (Real (real_bop bop v1 v2)))
    | (Real_uop uop, [Real v1]) ->
        Just ((s,t), Rval (Real (real_uop uop v1)))
    | (RealFromFP, [Litv (Word64 fp)]) ->
        Just ((s,t), Rval (Real (float2real fp)))
    | (Shift W8 op n, [Litv (Word8 w)]) ->
        Just ((s,t), Rval (Litv (Word8 (shift8_lookup op w n))))
    | (Shift W64 op n, [Litv (Word64 w)]) ->
        Just ((s,t), Rval (Litv (Word64 (shift64_lookup op w n))))
    | (Shift W64 op n, [FP_WordTree w1]) ->
        let wr1 = compress_word w1 in
          (Just ((s,t), Rval (Litv (Word64 (shift64_lookup op wr1 n)))))
    | (Equality, [v1; v2]) ->
        match do_eq v1 v2 with
          | Eq_type_error -> Nothing
          | Eq_val b -> Just ((s,t), Rval (Boolv b))
        end
    | (Opassign, [Loc lnum; v]) ->
        match store_assign lnum (Refv v) s with
          | Just s' -> Just ((s',t), Rval (Conv Nothing []))
          | Nothing -> Nothing
        end
    | (Opref, [v]) ->
        let (s',n) = store_alloc (Refv v) s in
          Just ((s',t), Rval (Loc n))
    | (Opderef, [Loc n]) ->
        match store_lookup n s with
          | Just (Refv v) -> Just ((s,t),Rval v)
          | _ -> Nothing
        end
    | (Aw8alloc, [Litv (IntLit n); Litv (Word8 w)]) ->
        if n < 0 then
          Just ((s,t), Rerr (Rraise sub_exn_v))
        else
          let (s',lnum) =
            store_alloc (W8array (List.replicate (natFromInteger n) w)) s
          in
            Just ((s',t), Rval (Loc lnum))
    | (Aw8sub, [Loc lnum; Litv (IntLit i)]) ->
        match store_lookup lnum s with
          | Just (W8array ws) ->
              if i < 0 then
                Just ((s,t), Rerr (Rraise sub_exn_v))
              else
                let n = natFromInteger i in
                  if n >= List.length ws then
                    Just ((s,t), Rerr (Rraise sub_exn_v))
                  else
                    Just ((s,t), Rval (Litv (Word8 (List_extra.nth ws n))))
          | _ -> Nothing
        end
    | (Aw8sub_unsafe, [Loc lnum; Litv (IntLit i)]) ->
        match store_lookup lnum s with
          | Just (W8array ws) ->
              if i < 0 then
                Nothing
              else
                let n = natFromInteger i in
                  if n >= List.length ws then
                    Nothing
                  else
                    Just ((s,t), Rval (Litv (Word8 (List_extra.nth ws n))))
          | _ -> Nothing
        end
    | (Aw8length, [Loc n]) ->
        match store_lookup n s with
          | Just (W8array ws) ->
              Just ((s,t),Rval (Litv(IntLit(integerFromNat(List.length ws)))))
          | _ -> Nothing
         end
    | (Aw8update, [Loc lnum; Litv(IntLit i); Litv(Word8 w)]) ->
        match store_lookup lnum s with
        | Just (W8array ws) ->
            if i < 0 then
              Just ((s,t), Rerr (Rraise sub_exn_v))
            else
              let n = natFromInteger i in
                if n >= List.length ws then
                  Just ((s,t), Rerr (Rraise sub_exn_v))
                else
                  match store_assign lnum (W8array (List.update ws n w)) s with
                    | Nothing -> Nothing
                    | Just s' -> Just ((s',t), Rval (Conv Nothing []))
                  end
        | _ -> Nothing
      end
    | (Aw8update_unsafe, [Loc lnum; Litv(IntLit i); Litv(Word8 w)]) ->
        match store_lookup lnum s with
        | Just (W8array ws) ->
            if i < 0 then
              Nothing
            else
              let n = natFromInteger i in
                if n >= List.length ws then
                  Nothing
                else
                  match store_assign lnum (W8array (List.update ws n w)) s with
                    | Nothing -> Nothing
                    | Just s' -> Just ((s',t), Rval (Conv Nothing []))
                  end
        | _ -> Nothing
      end
    | (WordFromInt W8, [Litv(IntLit i)]) ->
        Just ((s,t), Rval (Litv (Word8 (word8FromInteger i))))
    | (WordFromInt W64, [Litv(IntLit i)]) ->
        Just ((s,t), Rval (Litv (Word64 (word64FromInteger i))))
    | (WordToInt W8, [Litv (Word8 w)]) ->
        Just ((s,t), Rval (Litv (IntLit (integerFromNat(natFromWord8 w)))))
    | (WordToInt W64, [Litv (Word64 w)]) ->
        Just ((s,t), Rval (Litv (IntLit (integerFromNat(natFromWord64 w)))))
    | (WordToInt W64, [FP_WordTree v]) ->
        let w = compress_word v in
          Just ((s,t), Rval (Litv (IntLit (integerFromNat(natFromWord64 w)))))
    | (CopyStrStr, [Litv(StrLit str);Litv(IntLit off);Litv(IntLit len)]) ->
        Just ((s,t),
        match copy_array (toCharList str,off) len Nothing with
        | Nothing -> Rerr (Rraise sub_exn_v)
        | Just cs -> Rval (Litv(StrLit(toString(cs))))
        end)
    | (CopyStrAw8, [Litv(StrLit str);Litv(IntLit off);Litv(IntLit len);
                    Loc dst;Litv(IntLit dstoff)]) ->
        match store_lookup dst s with
        | Just (W8array ws) ->
            match copy_array (toCharList str,off) len (Just(ws_to_chars ws,dstoff)) with
            | Nothing -> Just ((s,t), Rerr (Rraise sub_exn_v))
            | Just cs ->
              match store_assign dst (W8array (chars_to_ws cs)) s with
              | Just s' ->  Just ((s',t), Rval (Conv Nothing []))
              | _ -> Nothing
              end
            end
        | _ -> Nothing
        end
    | (CopyAw8Str, [Loc src;Litv(IntLit off);Litv(IntLit len)]) ->
      match store_lookup src s with
      | Just (W8array ws) ->
        Just ((s,t),
          match copy_array (ws,off) len Nothing with
          | Nothing -> Rerr (Rraise sub_exn_v)
          | Just ws -> Rval (Litv(StrLit(toString(ws_to_chars ws))))
          end)
      | _ -> Nothing
      end
    | (CopyAw8Aw8, [Loc src;Litv(IntLit off);Litv(IntLit len);
                    Loc dst;Litv(IntLit dstoff)]) ->
      match (store_lookup src s, store_lookup dst s) with
      | (Just (W8array ws), Just (W8array ds)) ->
          match copy_array (ws,off) len (Just(ds,dstoff)) with
          | Nothing -> Just ((s,t), Rerr (Rraise sub_exn_v))
          | Just ws ->
              match store_assign dst (W8array ws) s with
              | Just s' -> Just ((s',t), Rval (Conv Nothing []))
              | _ -> Nothing
              end
          end
      | _ -> Nothing
      end
    | (Ord, [Litv (Char c)]) ->
          Just ((s,t), Rval (Litv(IntLit(integerFromNat(String_extra.ord c)))))
    | (Chr, [Litv (IntLit i)]) ->
        Just ((s,t),
          if i < 0 || i > 255 then
            Rerr (Rraise chr_exn_v)
          else
            Rval (Litv(Char(String_extra.chr(natFromInteger i)))))
    | (Chopb op, [Litv (Char c1); Litv (Char c2)]) ->
        Just ((s,t), Rval (Boolv (opb_lookup op (integerFromNat(String_extra.ord c1)) (integerFromNat(String_extra.ord c2)))))
    | (Implode, [v]) ->
          match v_to_char_list v with
          | Just ls ->
              Just ((s,t), Rval (Litv (StrLit (toString ls))))
          | Nothing -> Nothing
          end
    | (Explode, [v]) ->
          match v with
          | Litv (StrLit str) ->
              Just ((s,t), Rval (list_to_v (List.map (fun c -> Litv (Char c)) (toCharList str))))
          | _ -> Nothing
          end
    | (Strsub, [Litv (StrLit str); Litv (IntLit i)]) ->
        if i < 0 then
          Just ((s,t), Rerr (Rraise sub_exn_v))
        else
          let n = natFromInteger i in
            if n >= stringLength str then
              Just ((s,t), Rerr (Rraise sub_exn_v))
            else
              Just ((s,t), Rval (Litv (Char (List_extra.nth (toCharList str) n))))
    | (Strlen, [Litv (StrLit str)]) ->
        Just ((s,t), Rval (Litv(IntLit(integerFromNat(stringLength str)))))
    | (Strcat, [v]) ->
        match v_to_list v with
        | Just vs ->
            match vs_to_string vs with
            | Just str ->
                Just ((s,t), Rval (Litv(StrLit str)))
            | _ -> Nothing
            end
        | _ -> Nothing
        end
    | (VfromList, [v]) ->
          match v_to_list v with
            | Just vs ->
                Just ((s,t), Rval (Vectorv vs))
            | Nothing -> Nothing
          end
    | (Vsub, [Vectorv vs; Litv (IntLit i)]) ->
        if i < 0 then
          Just ((s,t), Rerr (Rraise sub_exn_v))
        else
          let n = natFromInteger i in
            if n >= List.length vs then
              Just ((s,t), Rerr (Rraise sub_exn_v))
            else
              Just ((s,t), Rval (List_extra.nth vs n))
    | (Vlength, [Vectorv vs]) ->
        Just ((s,t), Rval (Litv (IntLit (integerFromNat (List.length vs)))))
    | (Aalloc, [Litv (IntLit n); v]) ->
        if n < 0 then
          Just ((s,t), Rerr (Rraise sub_exn_v))
        else
          let (s',lnum) =
            store_alloc (Varray (List.replicate (natFromInteger n) v)) s
          in
            Just ((s',t), Rval (Loc lnum))
    | (AallocEmpty, [Conv Nothing []]) ->
        let (s',lnum) = store_alloc (Varray []) s in
          Just ((s',t), Rval (Loc lnum))
    | (Asub, [Loc lnum; Litv (IntLit i)]) ->
        match store_lookup lnum s with
          | Just (Varray vs) ->
              if i < 0 then
                Just ((s,t), Rerr (Rraise sub_exn_v))
              else
                let n = natFromInteger i in
                  if n >= List.length vs then
                    Just ((s,t), Rerr (Rraise sub_exn_v))
                  else
                    Just ((s,t), Rval (List_extra.nth vs n))
          | _ -> Nothing
        end
    | (Asub_unsafe, [Loc lnum; Litv (IntLit i)]) ->
        match store_lookup lnum s with
          | Just (Varray vs) ->
              if i < 0 then
                Nothing
              else
                let n = natFromInteger i in
                  if n >= List.length vs then
                    Nothing
                  else
                    Just ((s,t), Rval (List_extra.nth vs n))
          | _ -> Nothing
        end
    | (Alength, [Loc n]) ->
        match store_lookup n s with
          | Just (Varray ws) ->
              Just ((s,t),Rval (Litv(IntLit(integerFromNat(List.length ws)))))
          | _ -> Nothing
         end
    | (Aupdate, [Loc lnum; Litv (IntLit i); v]) ->
        match store_lookup lnum s with
        | Just (Varray vs) ->
            if i < 0 then
              Just ((s,t), Rerr (Rraise sub_exn_v))
            else
              let n = natFromInteger i in
                if n >= List.length vs then
                  Just ((s,t), Rerr (Rraise sub_exn_v))
                else
                  match store_assign lnum (Varray (List.update vs n v)) s with
                    | Nothing -> Nothing
                    | Just s' -> Just ((s',t), Rval (Conv Nothing []))
                  end
        | _ -> Nothing
      end
    | (Aupdate_unsafe, [Loc lnum; Litv (IntLit i); v]) ->
        match store_lookup lnum s with
        | Just (Varray vs) ->
            if i < 0 then
              Nothing
            else
              let n = natFromInteger i in
                if n >= List.length vs then
                  Nothing
                else
                  match store_assign lnum (Varray (List.update vs n v)) s with
                    | Nothing -> Nothing
                    | Just s' -> Just ((s',t), Rval (Conv Nothing []))
                  end
        | _ -> Nothing
      end
    | (ConfigGC, [Litv (IntLit i); Litv (IntLit j)]) ->
        Just ((s,t), Rval (Conv Nothing []))
    | (FFI n, [Litv(StrLit conf); Loc lnum]) ->
        match store_lookup lnum s with
        | Just (W8array ws) ->
            match call_FFI t n (List.map (fun c -> word8FromNat(String_extra.ord c)) (toCharList conf)) ws with
            | FFI_return t' ws' ->
               match store_assign lnum (W8array ws') s with
               | Just s' -> Just ((s', t'), Rval (Conv Nothing []))
               | Nothing -> Nothing
               end
            | FFI_final outcome ->
               Just ((s, t), Rerr (Rabort (Rffi_error outcome)))
            end
        | _ -> Nothing
        end
    | (Env_id, [Env env (gen, id)]) -> Just ((s, t),
            Rval (Conv Nothing [nat_to_v gen; nat_to_v id]))
    | (Env_id, [Conv Nothing [gen; id]]) -> Just ((s, t),
            Rval (Conv Nothing [gen; id]))
     | _ -> Nothing
  end

(* Do a logical operation *)
val do_log : lop -> v -> exp -> maybe exp_or_val
let do_log l v e =
  if l = And && v = Boolv true || l = Or && v = Boolv false then
    Just (Exp e)
  else if l = And && v = Boolv false || l = Or && v = Boolv true then
    Just (Val v)
  else
    Nothing

(* Do an if-then-else *)
val do_if : v -> exp -> exp -> maybe exp
let do_if v e1 e2 =
  if v = (Boolv true) then
    Just e1
  else if v = (Boolv false) then
    Just e2
  else
    Nothing

(* Semantic helpers for definitions *)

let build_constrs stamp condefs =
  List.map
    (fun (conN, ts) ->
      (conN, (List.length ts, TypeStamp conN stamp)))
    condefs

(* Build a constructor environment for the type definition tds *)
val build_tdefs : nat -> list (list tvarN * typeN * list (conN * list ast_t)) -> env_ctor
let rec build_tdefs next_stamp [] = alist_to_ns []
and build_tdefs next_stamp ((tvs,tn,condefs)::tds) =
  nsAppend
    (build_tdefs (next_stamp + 1) tds)
    (alist_to_ns (List.reverse (build_constrs next_stamp condefs)))
declare termination_argument build_tdefs = automatic

(* Checks that no constructor is defined twice in a type *)
val check_dup_ctors : list tvarN * typeN * list (conN * list ast_t) -> bool
let check_dup_ctors (tvs, tn, condefs) =
  List.allDistinct [ n | forall ((n, ts) MEM condefs) | true ]

val combine_dec_result : forall 'a. sem_env v -> result (sem_env v) 'a -> result (sem_env v) 'a
let combine_dec_result env r =
  match r with
    | Rerr e -> Rerr e
    | Rval env' -> Rval <| v = nsAppend env'.v env.v; c = nsAppend env'.c env.c |>
  end

val extend_dec_env : sem_env v -> sem_env v -> sem_env v
let extend_dec_env new_env env =
  <| c = nsAppend new_env.c env.c; v = nsAppend new_env.v env.v |>

(* Checks that a boolean expression has a floating-point operation *)
val isFpBoolExp: exp -> bool
let isFpBoolExp e =
    match e with
    | App op es -> isFpBool op
    | _ -> false
    end

(*
val decs_to_types : list dec -> list typeN
let decs_to_types ds =
  List.concat (List.map (fun d ->
        match d with
          | Dtype locs tds -> List.map (fun (tvs,tn,ctors) -> tn) tds
          | _ -> [] end)
     ds)

val no_dup_types : list dec -> bool
let no_dup_types ds =
  List.allDistinct (decs_to_types ds)

val prog_to_mods : list top -> list (list modN)
let prog_to_mods tops =
  List.concat (List.map (fun top ->
        match top with
          | Tmod mn _ _ -> [[mn]]
          | _ -> [] end)
     tops)

val no_dup_mods : list top -> set (list modN) -> bool
let no_dup_mods tops defined_mods =
  List.allDistinct (prog_to_mods tops) &&
  disjoint (Set.fromList (prog_to_mods tops)) defined_mods

val prog_to_top_types : list top -> list typeN
let prog_to_top_types tops =
  List.concat (List.map (fun top ->
        match top with
          | Tdec d -> decs_to_types [d]
          | _ -> [] end)
     tops)

val no_dup_top_types : list top -> set tid_or_exn -> bool
let no_dup_top_types tops defined_types =
  List.allDistinct (prog_to_top_types tops) &&
  disjoint (Set.fromList (List.map (fun tn -> TypeId (Short tn)) (prog_to_top_types tops))) defined_types
  *)

let shift_fp_opts s = <| s with fp_state =
                         <| s.fp_state with
                           opts = (fun x -> s.fp_state.opts (x + 1));
                           choices = s.fp_state.choices + 1 |> |>