path: root/src/lem_interp/interp.lem

open import Pervasives
import Map
import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
open import Show_extra (* for 'show' to convert nat to string) *)
open import String_extra (* for chr *)
import Assert_extra (*For failwith when partiality is known to be unreachable*)

open import Interp_ast
open import Interp_utilities
open import Instruction_extractor

type tannot = Interp_utilities.tannot

val intern_annot : tannot -> tannot
let intern_annot annot =
  match annot with
    | Just (t,_,ncs,effect) ->
      Just (t,Tag_empty,ncs,pure)
    | Nothing -> Nothing
  end

let val_annot typ = Just(typ,Tag_empty,[],pure)

let ctor_annot typ = Just(typ,Tag_ctor,[],pure)

(* This is different from OCaml: it will drop elements from the longest list. *)
let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')

type reg_form =
 | Reg of id * tannot
 | SubReg of id * reg_form * index_range

type value =
 | V_boxref of nat * t  
 | V_lit of lit
 | V_tuple of list value
 | V_list of list value
 (* A full vector: integer is the first index, bool says if that's most or least significant *)
 | V_vector of integer * bool * list value 
 (* A vector with default values, second integer stores length; as above otherwise *)
 | V_vector_sparse of integer * integer * bool * list (integer * value) * value 
 | V_record of t * list (id * value)
 | V_ctor of id * t * value
 | V_unknown (* Distinct from undefined, used by memory system *)
 | V_register of reg_form (* Value to store register access, when not actively reading or writing *)
 | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
 | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)

let rec integerToString n acc =
  if n = 0 then
    acc
  else
    integerToString (n / 10) (chr (natFromInteger (n mod 10 + 48)) :: acc)

let string_of_integer i = if i = 0 then "0" else toString(integerToString i [])

let rec string_of_value v = match v with
  | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
  | V_lit (L_aux lit _) -> 
    (match lit with
    | L_unit -> "()"
    | L_zero -> "0"
    | L_one  -> "1"
    | L_true -> "true"
    | L_false -> "false"
    | L_num num -> string_of_integer num
    | L_hex hex -> "0x" ^ hex
    | L_bin bin -> "0b" ^ bin
    | L_undef -> "undefined"
    | L_string str-> "\"" ^ str ^ "\"" end)
  | V_tuple vals -> "(" ^ (list_to_string string_of_value "," vals) ^ ")"
  | V_list vals -> "[||" ^ (list_to_string string_of_value "," vals) ^ "||]"
  | V_vector i inc vals -> 
    let default_format _ = "[" ^ (list_to_string string_of_value "," vals) ^ "]" in
    let to_bin () = "0b" ^ 
      (List.foldr (fun v rst -> (match v with | V_lit (L_aux l _) -> (match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" end)
	                                      | V_unknown -> "?" end) ^rst) "" vals) in
    match vals with
      | [] -> default_format ()
      | v::vs ->
	match v with 
	  | V_lit (L_aux L_zero _) -> to_bin()
	  | V_lit (L_aux L_one _) -> to_bin()
	  | _ -> default_format() end end
  | V_vector_sparse start stop inc vals default -> 
    "[" ^ (list_to_string (fun (i,v) -> (string_of_integer i) ^ " = " ^ (string_of_value v)) "," vals) ^ "]:" ^
      string_of_integer start ^ "-" ^string_of_integer  stop ^ "(default of " ^ (string_of_value default) ^ ")"
  | V_record t vals ->
    "{" ^ (list_to_string (fun (id,v) -> (get_id id) ^ "=" ^ (string_of_value v)) ";" vals) ^ "}"
  | V_ctor id t value -> (get_id id) ^ " " ^ string_of_value value     
  | V_unknown -> "Unknown"
  | V_register _ -> "register_as_value"
  | V_register_alias _ _ -> "register_as_alias"
  | V_track v _ -> "tainted " ^ (string_of_value v)
end

let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
and value_eq left right =
  (* XXX it is not clear whether t = t' will work in all cases *)
  match (left, right) with
  | (V_lit l, V_lit l') -> lit_eq l l'
  | (V_boxref n t, V_boxref m t') -> n = m && t = t'
  | (V_tuple l, V_tuple l') -> listEqualBy value_eq l l'
  | (V_list l, V_list l') -> listEqualBy value_eq l l'
  | (V_vector n b l, V_vector m b' l') ->
      n = m && b = b' && listEqualBy value_eq l l'
  | (V_vector_sparse n o b l v, V_vector_sparse m p b' l' v') ->
    n=m && o=p && b=b' && listEqualBy (fun (i,v) (i',v') -> i=i' && (value_eq v v')) l l' && value_eq v v'
  | (V_record t l, V_record t' l') ->
      t = t' &&
      listEqualBy id_value_eq l l'
  | (V_ctor i t v, V_ctor i' t' v') -> t = t' && id_value_eq (i, v) (i', v')
  | (V_unknown,_) -> true
  | (_,V_unknown) -> true
  | (V_track v _, v2) -> value_eq v v2
  | (v,V_track v2 _)  -> value_eq v v2
  | (_, _) -> false
  end

instance (Eq value)
  let (=) = value_eq
  let (<>) n1 n2 = not (value_eq n1 n2)
end

let reg_start_pos reg = 
  match reg with
    | Reg _ (Just(typ,_,_,_)) -> 
      let start_from_vec targs = match targs with
	| T_args [T_arg_nexp (Ne_const s);_;_;_] -> s
      end in
      let start_from_reg targs = match targs with
	| T_args [T_arg_typ (T_app "vector" targs)] -> start_from_vec targs
      end in
      let start_from_abbrev t = match t with
	| T_app "vector" targs -> start_from_vec targs
	| T_app "register" targs -> start_from_reg targs
      end in
      match typ with 
	| T_app "vector" targs -> start_from_vec targs
	| T_app "register" targs -> start_from_reg targs
	| T_abbrev _ t -> start_from_abbrev t
      end 
end 

let reg_size reg = 
  match reg with
    | Reg _ (Just(typ,_,_,_)) -> 
      let end_from_vec targs = match targs with
	| T_args [_;T_arg_nexp (Ne_const s);_;_] -> s
      end in
      let end_from_reg targs = match targs with
	| T_args [T_arg_typ (T_app "vector" targs)] -> end_from_vec targs
      end in
      let end_from_abbrev t = match t with
	| T_app "vector" targs -> end_from_vec targs
	| T_app "register" targs -> end_from_reg targs
      end in
      match typ with 
	| T_app "vector" targs -> end_from_vec targs
	| T_app "register" targs -> end_from_reg targs
	| T_abbrev _ t -> end_from_abbrev t
      end 
end 

let vector_length v = match v with
  | V_vector n inc vals -> integerFromNat(List.length vals)
  | V_vector_sparse n m inc vals def -> m
  | V_lit _ -> 1
  | _ -> 0
end

(*Constant unit value, for use in interpreter *)
let unitv = V_lit (L_aux L_unit Unknown)

(* Store for local memory of ref cells *)
type lmem = LMem of nat * map nat value

(* Environment for bindings *)
type env = list (id * value)
(* Environment for lexical bindings, nat is a counter to build new unique variables when necessary *)
type lenv = LEnv of nat * env

let emem = LMem 1 Map.empty
let eenv = LEnv 1 []

type sub_reg_map = list (id * index_range)

(*top_level is a tuple of 
  (all definitions,
   all extracted instructions (where possible),
   letbound and enum values, 
   register values, 
   Typedef union constructors, 
   sub register mappings, and register aliases) *)
type top_level = 
  | Env of (defs tannot) * list instruction_form * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))

type action = 
 | Read_reg of reg_form * maybe (integer * integer)
 | Write_reg of reg_form * maybe (integer* integer) * value
 | Read_mem of id * value * maybe (integer * integer)
 | Write_mem of id * value * maybe (integer * integer) * value
 | Barrier of id * value
 | Write_next_IA of value (* Perhaps not needed? *)
 | Nondet of list (exp tannot)
 | Call_extern of string * value
 | Exit of (exp tannot)
 (* For stepper, no action needed. String is function called, value is parameter, on next state is a new function body *)
 | Step of l * maybe string * maybe value 

(* Inverted call stack, where top item on the stack is waiting for an action to resolve and all other frames for the right stack *)
type stack = 
 | Top
 | Hole_frame of id * exp tannot * top_level * lenv * lmem * stack (* Stack frame waiting to fill a hole with a value *)
 | Thunk_frame of exp tannot * top_level * lenv * lmem * stack     (* Paused stack frame *)

(*Internal representation of outcomes from running the interpreter. Actions request an external party to resolve a request or pause*)
type outcome =
 | Value of value
 | Action of action * stack
 | Error of l * string 

type interp_mode = <| eager_eval : bool; track_values : bool |>

(* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
val to_top_env : (outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)

(* interprets the exp sequentially in the presence of a set of top level definitions and returns a value, a memory request, or other external action *)
val interp :interp_mode -> (outcome -> maybe value) -> defs tannot -> exp tannot -> outcome

(* Takes a paused partially evaluated expression, puts the value into the environment, and runs again *)
val resume : interp_mode -> stack -> maybe value -> outcome

(* Internal definitions to setup top_level *)
val to_register_fields : defs tannot -> list (id * list (id * index_range))
let rec to_register_fields (Defs defs) = 
  match defs with
  | [ ] -> [ ]
  | def::defs -> 
    match def with 
    | DEF_type (TD_aux (TD_register id n1 n2 indexes) l') ->
      (id,List.map (fun (a,b) -> (b,a)) indexes)::(to_register_fields (Defs defs))
    | _ -> to_register_fields (Defs defs)
    end 
  end

val to_registers : defs tannot -> env
let rec to_registers (Defs defs) = 
  match defs with
  | [ ] -> [ ]
  | def::defs -> 
    match def with 
    | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
    | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> (id, V_register_alias aspec tannot) :: (to_registers (Defs defs))
    | _ -> to_registers (Defs defs)
    end 
  end 

val to_aliases : defs tannot -> list (id * (alias_spec tannot))
let rec to_aliases (Defs defs) =
  match defs with
    | [] -> []
    | def::defs ->
      match def with
	| DEF_reg_dec (DEC_aux (DEC_alias id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
	| DEF_reg_dec (DEC_aux (DEC_typ_alias typ id aspec) _) -> (id, aspec) :: (to_aliases (Defs defs))
	| _ -> to_aliases (Defs defs)
      end 
    end

val to_data_constructors : defs tannot -> list (id * typ)
let rec to_data_constructors (Defs defs) =
  match defs with
  | [] -> []
  | def :: defs ->
    match def with
    | DEF_type (TD_aux t _)->
      match t with 
      | TD_variant id _ tq tid_list _ ->
        (List.map 
	   (fun (Tu_aux t _) ->
	     match t with
	    | (Tu_ty_id x y) -> (y,x)
	    | Tu_id x -> (x,unit_t) end) tid_list)++(to_data_constructors (Defs defs))
      | _ -> to_data_constructors (Defs defs) end
    | _ -> to_data_constructors (Defs defs) end
   end

(*Memory and environment helper functions*)
val in_env :forall 'a. (list (id * 'a)) -> id -> maybe 'a
let rec in_env env id =
 match env with
 | [] -> Nothing
 | (eid,value)::env -> if (get_id eid) = (get_id id) then Just value else in_env env id
 end 

val in_lenv : lenv -> id -> value
let in_lenv (LEnv _ env) id =
  match in_env env id with
  | Nothing -> V_unknown
  | Just v  -> v 
end

(*Prefer entries in the first when conflict*)
let rec list_union first second =
  match first with
    | [] -> second
    | (id,v)::frst ->
      match in_env second id with
	| Nothing -> (id,v)::(list_union frst second)
	| Just _ -> (id,v)::(list_union frst 
			       (List.deleteBy (fun (id,v) (id2,v2) -> (get_id id) = (get_id id2))
				  (id,v) second)) end
end

val union_env : lenv -> lenv -> lenv
let union_env (LEnv i1 env1) (LEnv i2 env2) = 
  let l = if i1 < i2 then i2 else i1 in
  LEnv l (list_union env1 env2)

val fresh_var : lenv -> (id * lenv)
let fresh_var (LEnv i env) =
  let lenv = (LEnv (i+1) env) in
  ((Id_aux (Id ((show i) ^ "var")) Interp_ast.Unknown), lenv)

val add_to_env : (id * value) -> lenv -> lenv
let add_to_env entry (LEnv i env) = (LEnv i (entry::env))

val in_mem : lmem -> nat -> value
let in_mem (LMem _ m) n = 
  Map_extra.find n m
  (* Map.lookup n m *)

val update_mem : lmem -> nat -> value -> lmem
let update_mem (LMem c m) loc value =
  let m' = Map.delete loc m in
  let m' = Map.insert loc value m' in
  LMem c m'

(*Value helper functions*)

val is_lit_vector : lit -> bool
let is_lit_vector (L_aux l _) = 
  match l with
  | L_bin _ -> true 
  | L_hex _ -> true
  | _ -> false
end

val litV_to_vec : lit -> bool -> value
let litV_to_vec (L_aux lit l) is_inc =
  match lit with
  | L_hex s ->
    let to_v b = V_lit (L_aux b l) in
    let hexes = List.map to_v 
                 (List.concat 
		    (List.map 
		       (fun s -> match s with
			 | #'0' -> [L_zero;L_zero;L_zero;L_zero]
			 | #'1' -> [L_zero;L_zero;L_zero;L_one ]
			 | #'2' -> [L_zero;L_zero;L_one ;L_zero]
			 | #'3' -> [L_zero;L_zero;L_one ;L_one ]
			 | #'4' -> [L_zero;L_one ;L_zero;L_zero]
			 | #'5' -> [L_zero;L_one ;L_zero;L_one ]
			 | #'6' -> [L_zero;L_one ;L_one ;L_zero]
			 | #'7' -> [L_zero;L_one ;L_one ;L_one ]
			 | #'8' -> [L_one ;L_zero;L_zero;L_zero]
			 | #'9' -> [L_one ;L_zero;L_zero;L_one ]
			 | #'A' -> [L_one ;L_zero;L_one ;L_zero]
			 | #'B' -> [L_one ;L_zero;L_one ;L_one ]
			 | #'C' -> [L_one ;L_one ;L_zero;L_zero]
			 | #'D' -> [L_one ;L_one ;L_zero;L_one ]
			 | #'E' -> [L_one ;L_one ;L_one ;L_zero]
			 | #'F' -> [L_one ;L_one ;L_one ;L_one ]
			 | #'a' -> [L_one ;L_zero;L_one ;L_zero]
			 | #'b' -> [L_one ;L_zero;L_one ;L_one ]
			 | #'c' -> [L_one ;L_one ;L_zero;L_zero]
			 | #'d' -> [L_one ;L_one ;L_zero;L_one ]
			 | #'e' -> [L_one ;L_one ;L_one ;L_zero]
			 | #'f' -> [L_one ;L_one ;L_one ;L_one ] end)
		       (String.toCharList s))) in
    if is_inc 
    then V_vector 0 true hexes
    else V_vector (integerFromNat ((List.length hexes) -1)) false hexes
  | L_bin s -> 
    let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) (String.toCharList s) in
    if is_inc
    then V_vector 0 true bits
    else V_vector (integerFromNat ((List.length bits) -1)) false bits
  end

(* Like List_extra.nth with a integer instead of nat index -
 * using an unsafe coercion. *)
val list_nth : forall 'a . list 'a -> integer -> 'a
let list_nth l n = List_extra.nth l (natFromInteger n)

val list_length : forall 'a . list 'a -> integer
let list_length l = integerFromNat (List.length l)

val taint: value -> list reg_form -> value
let rec taint value regs = 
  match regs with
    | [] -> value
    | _ ->
      match value with 
	| V_track value rs -> taint value (regs ++ rs)
	| V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
	| _ -> V_track value regs
end end

val retaint: value -> value -> value
let retaint orig updated =
  match orig with 
    | V_track _ rs -> taint updated rs
    | _ -> updated
end

val detaint: value -> value 
let rec detaint value = 
  match value with
    | V_track value _ -> detaint value
    | v -> v
end

let rec binary_taint thunk vall valr =
 match (vall,valr) with
   | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl++rr)
   | (V_track vl rl,vr) -> taint (binary_taint thunk vl vr) rl
   | (vl,V_track vr rr) -> taint (binary_taint thunk vl vr) rr
   | (vl,vr) -> thunk vl vr
end 

val access_vector : value -> integer -> value
let access_vector v n =
  retaint v (match (detaint v) with
    | V_unknown -> V_unknown 
    | V_vector m inc vs -> 
      if inc then
	list_nth vs (n - m)
      else list_nth vs (m - n)
    | V_vector_sparse _ _ _ vs d ->
      match (List.lookup n vs) with
	| Nothing -> d
	| Just v  -> v end 
  end )

val from_n_to_n :forall 'a. integer -> integer  -> list 'a -> list 'a
let from_n_to_n from to_ ls =
  let from = natFromInteger from in
  let to_ = natFromInteger to_ in
  take (to_ - from + 1) (drop from ls)

val slice_sparse_list : (integer -> integer -> bool) -> (integer -> integer) -> 
                        list (integer * value) -> integer -> integer -> ((list (integer * value)) * bool)
let rec slice_sparse_list compare update_n vals n1 n2 = 
  let sl = slice_sparse_list compare update_n in
  if (n1 = n2) && (vals = []) 
  then ([],true)
  else if (n1=n2)
  then ([],false)
  else match vals with
    | [] -> ([],true)
    | (i,v)::vals -> 
      if n1 = i 
      then let (rest,still_sparse) = (sl vals (update_n n1) n2) in ((i,v)::rest,still_sparse)
      else if (compare n1 i)
      then  (sl vals (update_n n1) n2)
      else let (rest,_) = (sl vals (update_n i) n2) in ((i,v)::rest,true)
  end

val slice_vector : value -> integer -> integer -> value
let slice_vector v n1 n2 =
  retaint v (match detaint v with
    | V_vector m inc vs ->
      if inc 
      then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) vs)
      else V_vector (n1 - n2 + 1) inc (from_n_to_n (m - n1) (m - n2) vs)
    | V_vector_sparse m n inc vs d -> 
      let (slice, still_sparse) = 
	if inc 
	then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
	else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
      if still_sparse && inc
      then V_vector_sparse n1 (n2 - n1) inc slice d
      else if inc then V_vector 0 inc (List.map snd slice)
      else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) inc slice d
      else V_vector (n1 - n2 +1) inc (List.map snd slice)
 end )

val update_field_list : list (id * value) -> list (id * value) -> list (id * value)
let rec update_field_list base updates =
  match base with
  | [] -> []
  | (id,v)::bs -> match in_env updates id with
    | Just v -> (id,v)::(update_field_list bs updates)
    | Nothing -> (id,v)::(update_field_list bs updates) end
end

val fupdate_record : value -> value -> value
let fupdate_record base updates = 
  let fupdate_record_helper base updates =
      (match (base,updates) with
	| (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us) 
       end) in
  binary_taint fupdate_record_helper base updates

val fupdate_sparse : (integer -> integer -> bool) -> list (integer*value) -> integer -> value -> list (integer*value)
let rec fupdate_sparse comes_after vs n vexp =
  match vs with
    | [] -> [(n,vexp)]
    | (i,v)::vs ->
      if i = n then (i,vexp)::vs
      else if (comes_after i n) then (n,vexp)::(i,v)::vs
      else (i,v)::(fupdate_sparse comes_after vs n vexp)
end

val fupdate_vec : value -> integer -> value -> value
let fupdate_vec v n vexp =
  let tainted = binary_taint (fun v _ -> v) v vexp in
  retaint tainted
    (match detaint v with
      | V_vector m inc vals -> 
	V_vector m inc (List.update vals (natFromInteger (if inc then (n-m) else (m-n))) vexp)
      | V_vector_sparse m o inc vals d ->
	V_vector_sparse m o inc (fupdate_sparse (if inc then (>) else (<)) vals n vexp) d
     end)

val replace_is : forall 'a. list 'a -> list 'a -> integer -> integer -> integer -> list 'a
let rec replace_is ls vs base start stop =
  match (ls,vs) with
  | ([],_) -> []
  | (ls,[]) -> ls
  | (l::ls,v::vs) -> 
    if base >= start then
      if start >= stop then v::ls
      else v::(replace_is ls vs (base + 1) (start + 1) stop)
    else l::(replace_is ls (v::vs) (base+1) start stop)
  end

val replace_sparse : (integer -> integer -> bool) -> list (integer * value) -> list (integer * value) -> list (integer * value)
let rec replace_sparse compare vals reps =
  match (vals,reps) with
    | ([],rs) -> rs
    | (vs,[]) -> vs
    | ((i1,v)::vs,(i2,r)::rs) ->
      if i1 = i2 then (i2,r)::(replace_sparse compare vs rs)
      else if (compare i1 i2) 
      then (i1,v)::(replace_sparse compare vs ((i2,r)::rs))
      else (i2,r)::(replace_sparse compare ((i1,v)::vs) rs)
end

val fupdate_vector_slice : value -> value -> integer -> integer -> value
let fupdate_vector_slice vec replace start stop =
  let fupdate_vec_help vec replace = 
    (match (vec,replace) with
    | (V_vector m inc vals,V_vector _ inc' reps) ->
      V_vector m inc 
	(replace_is vals 
	   (if inc=inc' then reps else (List.reverse reps))
	   0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
    | (V_vector m inc vals, V_unknown) ->
      V_vector m inc
	(replace_is vals 
	   (List.replicate (natFromInteger(if inc then (stop-start) else (start-stop))) V_unknown)
	   0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
    | (V_vector_sparse m n inc vals d,V_vector _ _ reps) ->
      let (_,repsi) = List.foldl (fun (i,rs) r -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
      (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals (List.reverse repsi)) d)
    | (V_vector_sparse m n inc vals d, V_unknown) ->
      let (_,repsi) = List.foldl (fun (i,rs) r -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) 
	(List.replicate (natFromInteger (if inc then (stop-start) else (start-stop))) V_unknown) in
      (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals (List.reverse repsi)) d)
    | (V_unknown,_) -> V_unknown
     end) in
  binary_taint fupdate_vec_help vec replace

val update_vector_slice : value -> value -> integer -> integer -> lmem -> lmem
let update_vector_slice vector value start stop mem = 
  match (detaint vector,detaint value) with
  | ((V_boxref n t), v) ->
    update_mem mem n (fupdate_vector_slice (in_mem mem n) (retaint value v) start stop)    
  | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
    let (V_vector m' _ vs') = slice_vector vector start stop in
    foldr2 (fun vbox v mem -> match vbox with
      | V_boxref n t -> update_mem mem n v end)
      mem vs' vals
  | ((V_vector m inc vs),(V_vector_sparse n o inc2 vals d)) -> 
    let (V_vector m' _ vs') = slice_vector vector start stop in
    let (_,mem) = foldr (fun vbox (i,mem) ->
                          match vbox with
			    | V_boxref n t -> 
			      (if inc then i+1 else i-1,
				update_mem mem n (match List.lookup i vals with
				  | Nothing -> d
				  | Just v  -> v end))
                          end) (m,mem) vs' in 
    mem
  | ((V_vector m inc vs),v) ->
    let (V_vector m' _ vs') = slice_vector vector start stop in
    List.foldr (fun vbox mem -> match vbox with
                                    | V_boxref n t -> update_mem mem n v end)
      mem vs'
end

let update_vector_start new_start expected_size v = 
  retaint v
    (match detaint v with
      | V_lit (L_aux L_zero _) ->
	V_vector new_start true (*TODO: Check for default endianness here*) [v]
      | V_lit (L_aux L_one _) ->
	V_vector new_start true [v]
      | V_vector m inc vs -> V_vector new_start inc vs
  (*Note, may need to shrink and check if still sparse *)
      | V_vector_sparse m n inc vals d -> V_vector_sparse new_start n inc vals d 
      | V_unknown -> 
	V_vector new_start true (List.replicate (natFromInteger expected_size) V_unknown)
      | V_lit (L_aux L_undef _) -> 
	V_vector new_start true (List.replicate (natFromInteger expected_size) v)
     end)

val in_ctors : list (id * typ) -> id -> maybe typ
let rec in_ctors ctors id =
  match ctors with
  | [] -> Nothing
  | (cid,typ)::ctors -> if (get_id cid) = (get_id id) then Just typ else in_ctors ctors id
end

(*Stack manipulation functions *)
(*Extends expression and context of 'top' stack frame *)
let add_to_top_frame e_builder stack =
  match stack with
  | Top -> Top
  | Hole_frame id e t_level env mem stack -> 
    let (e',env') = (e_builder e env) in Hole_frame id e' t_level env' mem stack
  | Thunk_frame e t_level env mem stack -> 
    let (e',env') = (e_builder e env) in Thunk_frame e' t_level env' mem stack
  end

(*Is this the innermost hole*)
let top_hole stack : bool =
  match stack with
  | Hole_frame _ (E_aux (E_id (Id_aux (Id "0") _)) _) _ _ _ Top -> true
  | _ -> false
end

(*Converts a Hole_frame into a Thunk_frame, pushing to the top of the stack to insert the value at the innermost context *)
val add_answer_to_stack : stack -> value -> stack
let rec add_answer_to_stack stack v = 
  match stack with
  | Top -> Top
  | Hole_frame id e t_level (LEnv i env) mem Top -> Thunk_frame e t_level (LEnv i ((id,v)::env)) mem Top
  | Thunk_frame e t_level env mem Top -> Thunk_frame e t_level env mem Top
  | Hole_frame id e t_level env mem stack -> Hole_frame id e t_level env mem (add_answer_to_stack stack v)
  | Thunk_frame e t_level env mem stack -> Thunk_frame e t_level env mem (add_answer_to_stack stack v)
end

(*Throws away all but the environment and local memory of the top stack frame, putting given expression in this context *)
val set_in_context : stack -> exp tannot -> stack
let rec set_in_context stack e =
  match stack with
    | Top -> Top
    | Hole_frame id oe t_level env mem Top -> Thunk_frame e t_level env mem Top
    | Thunk_frame oe t_level env mem Top -> Thunk_frame e t_level env mem Top
    | Hole_frame _ _ _ _ _ s -> set_in_context s e
    | Thunk_frame _ _ _ _ s -> set_in_context s e
end

let get_stack_state stack = 
  match stack with
    | Top -> Assert_extra.failwith "Top reached in extracting stack state"
    | Hole_frame id exp top_level lenv lmem stack -> (lenv,lmem)
    | Thunk_frame exp top_level lenv lmem stack -> (lenv,lmem)
end

let id_of_string s = (Id_aux (Id s) Unknown)

let redex_id = id_of_string "0"

(*functions for converting in progress evaluation back into expression for building current continuation*)
let rec combine_typs ts =
  match ts with
  | [] -> T_var "fresh"
  | [t] -> t
  | t::ts ->
    let t' = combine_typs ts in
    match (t,t') with 
      | (_,T_var _) -> t
      | ((T_app "range" (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
	 (T_app "range" (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
	let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
	let r = (larger + larger_r) - smaller in
	T_app "range" (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
      | ((T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); 
				   T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
	 (T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); 
				  T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
	let t = combine_typs [t1;t2] in
	match (o1,o2) with
	  | (Ord_inc,Ord_inc) ->
	    let larger_start = if b1 < b2 then b2 else b1 in
	    let smaller_rise = if r1 < r2 then r1 else r2 in
	    (T_app "vector" (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
				     (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
	  | (Ord_dec,Ord_dec) ->
	    let smaller_start = if b1 < b2 then b1 else b2 in
	    let smaller_fall = if r1 < r2 then r2 else r2 in
	    (T_app "vector" (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
				     (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
	  | _ -> T_var "fresh"
	 end 
      | _ -> t'
     end 
   end

let reg_to_t r =
  match r with
    | Reg id (Just (t,_,_,_)) -> t
    | _ -> T_var "fresh"
 end

let rec val_typ v =
  match v with
    | V_boxref n t -> T_app "reg" (T_args [T_arg_typ t])
    | V_lit (L_aux lit _) ->
      match lit with
	| L_unit -> T_id "unit"
	| L_true -> T_id "bool"
	| L_false -> T_id "bool"
	| L_one -> T_id "bit"
	| L_zero -> T_id "bit"
	| L_string _ -> T_id "string"
	| L_num n -> T_app "range" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
	| L_undef -> T_var "fresh"
      end 
    | V_tuple vals -> T_tup (List.map val_typ vals)
    | V_vector n inc vals -> 
      let ts = List.map val_typ vals in
      let t = combine_typs ts in
      T_app "vector" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const (list_length vals));
			      T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
			      T_arg_typ t])
    | V_vector_sparse n m inc vals d ->
      let ts = List.map val_typ (d::(List.map snd vals)) in
      let t = combine_typs ts in
      T_app "vector" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const m);
			      T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
			      T_arg_typ t])
    | V_record t ivals -> t
    | V_list vals -> 
      let ts = List.map val_typ vals in
      let t = combine_typs ts in
      T_app "list" (T_args [T_arg_typ t])
    | V_ctor id t vals -> t
    | V_register reg -> reg_to_t reg
    | V_track v _ -> val_typ v
    | V_unknown -> T_var "fresh" (*consider carrying the type along*)
  end

(* When mode.track_values keeps tracking on registers by extending environment *)
let rec to_exp mode env v : (exp tannot * lenv) =
  let mk_annot is_ctor = (Interp_ast.Unknown, if is_ctor then (ctor_annot (val_typ v)) else (val_annot (val_typ v))) in
  let annot = mk_annot false in
  let mapf vs ((LEnv l env) as lenv) : (list (exp tannot) * lenv) =
    let (es, env) = 
      List.foldr (fun v (es,env) -> let (e,ev) = (to_exp mode env v) in
                                    if mode.track_values 
                                    then ((e::es), union_env ev env)
                                    else ((e::es), env))
                  ([],(LEnv l [])) vs in
    (es, union_env env lenv)
  in
  match v with
  | V_boxref n t -> (E_aux (E_id (Id_aux (Id (show n)) Unknown)) annot, env)
  | V_lit lit -> (E_aux (E_lit lit) annot, env)
  | V_tuple(vals) -> 
    let (es,env') = mapf vals env in (E_aux (E_tuple es) annot, env')
  | V_vector n inc vals -> 
    let (es,env') = mapf vals env in
    if (inc && n=0) 
    then (E_aux (E_vector es) annot, env') 
    else if inc 
    then (E_aux (E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n,e)::acc)) (n,[]) es)))
	                          (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
    else 
      (E_aux (E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n,e)::acc)) (n-(list_length es),[]) es)) 
	                       (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
  | V_vector_sparse n m inc vals d ->
    let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in
    let ((d : (exp tannot)),env')  = to_exp mode env' d in
    (E_aux (E_vector_indexed 
	      ((if inc then List.reverse else (fun i -> i)) (List.map (fun ((i,v), e) -> (i, e)) (List.zip vals es)))
	      (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env')
  | V_record t ivals -> 
    let (es,env') = mapf (List.map (fun (i,v) -> v) ivals) env in
    (E_aux (E_record(FES_aux (FES_Fexps
			        (List.map (fun ((id,value), e) -> (FE_aux (FE_Fexp id e) (Unknown,Nothing)))
                                   (List.zip ivals es)) false) 
	               (Unknown,Nothing))) annot, env')
  | V_list(vals) -> let (es,env') = mapf vals env in (E_aux (E_list es) annot, env')
  | V_ctor id t vals -> 
    (match vals with
    | V_lit (L_aux L_unit _) -> (E_aux (E_id id) (mk_annot true), env)
    | V_track (V_lit (L_aux L_unit _)) _ -> (E_aux (E_id id) (mk_annot true), env)
    | V_tuple vals -> let (es,env') = mapf vals env in (E_aux (E_app id es) (mk_annot true), env')
    | V_track (V_tuple vals) _ -> let (es,env') = mapf vals env in (E_aux (E_app id es) (mk_annot true), env')
    | V_track _ _ -> 
      if mode.track_values 
      then begin let (fid,env') = fresh_var env in
                 let env' = add_to_env (fid,vals) env' in
                 (E_aux 
		    (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))])
		    (mk_annot true), env')
      end 
      else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) (mk_annot true), env') 
    | _ -> 
      let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) (mk_annot true),env') end)
  | V_register (Reg id tan) -> (E_aux (E_id id) annot, env)
  | V_track v' _ -> 
    if mode.track_values
    then begin let (fid,env') = fresh_var env in
               let env' = add_to_env (fid,v) env' in
               (E_aux (E_id fid) annot, env') end
    else to_exp mode env v'
  | V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env)
end

val env_to_let : interp_mode -> lenv -> (exp tannot) -> (exp tannot)
let rec env_to_let_help mode env = match env with
  | [] -> []
  | (i,v)::env -> 
    let t = (val_typ v) in
    let tan = (val_annot t) in
    let (e,_) = to_exp <| mode with track_values = false |> eenv v in
    (((P_aux (P_id i) (Unknown,tan)),e),t)::(env_to_let_help mode env)
end 

let env_to_let mode (LEnv _ env) (E_aux e annot) = 
  match env_to_let_help mode env with
    | [] -> E_aux e annot
    | [((p,e),t)] -> E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot
    | pts -> let ts = List.map snd pts in
	     let pes = List.map fst pts in
	     let ps = List.map fst pes in
	     let es = List.map snd pes in
	     let t = T_tup ts in
	     let tan = val_annot t in
	     E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan))
				                   (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
		           (E_aux e annot))
	           annot
end

(* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
val match_pattern : pat tannot -> value -> bool * bool * lenv
let rec match_pattern (P_aux p _) value_whole =
  let value = detaint value_whole in
  let taint_pat v = binary_taint (fun v _ -> v) v value_whole in
  match p with 
  | P_lit(lit) -> 
    if is_lit_vector lit then
      let (V_vector n inc bits) = litV_to_vec lit true in (*TODO use type annotation to select between increasing and decreasing*)
      match value with
      | V_lit litv -> 
        if is_lit_vector litv then 
          let (V_vector n' inc' bits') = litV_to_vec litv true in (*TODO use type annotation to select between increasing and decreasing *)
          if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, eenv)
          else (false,false,eenv)
        else (false,false,eenv)
      | V_vector n' inc' bits' -> 
        if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l=r) && rest) true bits bits',false,eenv)
        else (false,false,eenv)
      | V_unknown -> (true,true,eenv)
      | _ -> (false,false,eenv) end
    else
    match value with
    | V_lit(litv) -> (lit = litv, false,eenv)
    | V_vector _ _ [V_lit(litv)] -> (lit = litv,false,eenv)
    | V_unknown -> (true,true,eenv)
    | _ -> (false,false,eenv)
    end
 | P_wild -> (true,false,eenv)
 | P_as pat id ->  
   let (matched_p,used_unknown,(LEnv bi bounds)) = match_pattern pat value in
   if matched_p then
     (matched_p,used_unknown,(LEnv bi ((id,value_whole)::bounds)))
   else (false,false,eenv)
 | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information, but that's looking less useful *)
 | P_id id -> (true, false, (LEnv 0 [(id,value_whole)]))
 | P_app (Id_aux id _) pats -> 
   match value with
   | V_ctor (Id_aux cid _) t (V_tuple vals) -> 
     if (id = cid && ((List.length pats) = (List.length vals)))
     then foldr2
          (fun pat value (matched_p,used_unknown,bounds) ->
            if matched_p then
              let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in
              (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
            else (false,false,eenv)) (true,false,eenv) pats vals
     else (false,false,eenv)
   | V_ctor (Id_aux cid _) t (V_track (V_tuple vals) r) -> 
     if (id = cid && ((List.length pats) = (List.length vals)))
     then foldr2
          (fun pat value (matched_p,used_unknown,bounds) ->
            if matched_p then
              let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value r) in
              (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
            else (false,false,eenv)) (true,false,eenv) pats vals
     else (false,false,eenv)
   | V_ctor (Id_aux cid _) t v ->
     if id = cid
     then (match (pats,detaint v) with
     | ([],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
     | ([p],_) -> match_pattern p v
     | _ -> (false,false,eenv) end)
     else (false,false,eenv)
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false,eenv) end
 | P_record fpats _ ->
   match value with
   | V_record t fvals ->
     List.foldr
       (fun (FP_aux (FP_Fpat id pat) _) (matched_p,used_unknown,bounds) ->
         if matched_p then
           let (matched_p,used_unknown',new_bounds) = match in_env fvals id with
                                       | Nothing -> (false,false,eenv)
                                       | Just v -> match_pattern pat v end in
           (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
         else (false,false,eenv)) (true,false,eenv) fpats
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false,eenv)
   end           
 | P_vector pats ->
   match value with
   | V_vector n inc vals ->
     if ((List.length vals) = (List.length pats))
     then foldr2
       (fun pat value (matched_p,used_unknown,bounds) -> 
	 if matched_p then
	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in
	   (matched_p, (used_unknown||used_unknown'), (union_env new_bounds bounds))
	 else (false,false,eenv))
       (true,false,eenv) (if inc then pats else List.reverse pats) vals
     else (false,false,eenv)
   | V_vector_sparse n m inc vals d ->
     if ((natFromInteger m) = (List.length pats))
     then let (_,matched_p,used_unknown,bounds) =
	    foldr
	      (fun pat (i,matched_p,used_unknown,bounds) ->
		if matched_p 
		then let (matched_p,used_unknown',new_bounds) = 
		       match_pattern pat (match List.lookup i vals with
			 | Nothing -> d
			 | Just v  -> (taint_pat v) end) in
		     ((if inc then i+1 else i-1),matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
                else (i,false,false,eenv)) (n,true,false,eenv) pats in
	  (matched_p,used_unknown,bounds)
     else (false,false,eenv)
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false,eenv)
     end
 | P_vector_indexed ipats ->
   match value with
   | V_vector n inc vals ->
     let v_len = if inc then list_length vals + n else n - list_length vals in
     List.foldr
       (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < v_len then
	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat (list_nth vals (if inc then i+n else i-n))) in
	   (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
         else (false,false,eenv))
       (true,false,eenv) ipats
   | V_vector_sparse n m inc vals d ->
     List.foldr
       (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < m then
	   let (matched_p,used_unknown',new_bounds) = 
             match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint_pat v) end) in
	   (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
	 else (false,false,eenv))
       (true,false,eenv) ipats
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false, eenv)
   end 
 | P_vector_concat pats ->
   match value with
   | V_vector n inc vals ->
     let (matched_p,used_unknown,bounds,remaining_vals) =
       List.foldl 
         (fun (matched_p,used_unknown,bounds,r_vals) (P_aux pat (l,Just(t,_,_,_))) ->
	   let (matched_p,used_unknown',bounds',matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
	   (matched_p,(used_unknown || used_unknown'),(union_env bounds' bounds),r_vals)) (true,false,eenv,vals) pats in
     if matched_p && ([] = remaining_vals) then (matched_p,used_unknown,bounds) else (false,false,eenv) 
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false, eenv) 
   end
 | P_tup(pats) ->
   match value with 
   | V_tuple(vals) ->
     if ((List.length pats)= (List.length vals))
     then foldr2 
       (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat v) in
	   (matched_p,used_unknown ||used_unknown', (union_env new_bounds bounds))
	 else (false,false,eenv))
       (true,false,eenv) pats vals
     else (false,false,eenv)
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false,eenv)
     end 
 | P_list(pats) ->
   match value with 
   | V_list(vals) ->
     if ((List.length pats)= (List.length vals))
     then foldr2 
       (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat v) in
	   (matched_p,used_unknown|| used_unknown', (union_env new_bounds bounds))
	 else (false,false,eenv))
       (true,false,eenv) pats vals
     else (false,false,eenv)
   | V_unknown -> (true,true,eenv)
   | _ -> (false,false,eenv) end
 end 

and vec_concat_match_plev pat r_vals inc l t =
    match pat with
      | P_lit (L_aux (L_bin bin_string) l') ->
	let bin_chars = toCharList bin_string in
	let binpats = List.map 
          (fun b -> P_aux (match b with | #'0' -> P_lit (L_aux L_zero l') | #'1' -> P_lit (L_aux L_one l')end) (l',Nothing)) bin_chars in
	vec_concat_match binpats r_vals
      | P_vector pats -> vec_concat_match pats r_vals
      | P_id id -> (match t with
	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
	    let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
	    let (matched_p,used_unknown,(LEnv bi bounds),matcheds,r_vals) = vec_concat_match wilds r_vals in
	    if matched_p 
	    then (matched_p, used_unknown, 
                  (LEnv bi ((id,(V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds))::bounds)),
                  matcheds,r_vals)
	    else (false,false,eenv,[],[])
	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
	    (false,false,eenv,[],[]) (*TODO see if can have some constraint bounds here*)
	  | _ -> (false,false,eenv,[],[]) end)
      | P_wild -> (match t with
	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
	    let wilds = List.genlist (fun _ -> P_aux P_wild (l,Nothing)) (natFromInteger i) in
	    vec_concat_match wilds r_vals 
	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
	    (false,false,eenv,[],[]) (*TODO see if can have some constraint bounds here*)
	  | _ -> (false,false,eenv,[],[]) end)
      | P_as (P_aux pat (l',Just(t,_,_,_))) id -> 
	let (matched_p, used_unknown, (LEnv bi bounds),matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
	if matched_p 
	then (matched_p, used_unknown,
              (LEnv bi ((id,V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds)::bounds)),
              matcheds,r_vals)
	else (false,false,eenv,[],[])	  
      | P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals inc l t
      | _ -> (false,false,eenv,[],[]) end 
      (*TODO Need to support indexed here, skipping intermediate numbers but consumming r_vals, and as *)

and vec_concat_match pats r_vals =
    match pats with
    | [] -> (true,false,eenv,[],r_vals)
    | pat::pats -> match r_vals with
      | [] -> (false,false,eenv,[],[])
      | r::r_vals -> 
	let (matched_p,used_unknown,new_bounds) = match_pattern pat r in
        if matched_p then 
          let (matched_p,used_unknown',bounds,matcheds,r_vals) = vec_concat_match pats r_vals in
          (matched_p, used_unknown||used_unknown',(union_env new_bounds bounds),r :: matcheds,r_vals)
        else (false,false,eenv,[],[]) end
    end


(* Returns all matches using Unknown until either there are no more matches or a pattern matches with no Unknowns used *)
val find_funcl : list (funcl tannot) -> value -> list (lenv * bool * (exp tannot))
let rec find_funcl funcls value =
  match funcls with
  | [] -> []
  | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
    let (is_matching,used_unknown,env) = match_pattern pat value in
    if (is_matching && used_unknown)
    then (env,used_unknown,exp)::(find_funcl funcls value)
    else if is_matching then [(env,used_unknown,exp)]
    else find_funcl funcls value
  end

(*see above comment*)
val find_case : list (pexp tannot) -> value -> list (lenv * bool * (exp tannot))
let rec find_case pexps value =
  match pexps with
  | [] -> []
  | (Pat_aux (Pat_exp p e) _)::pexps -> 
    let (is_matching,used_unknown,env) = match_pattern p value in
    if (is_matching && used_unknown)
    then (env,used_unknown,e)::find_case pexps value
    else if is_matching then [(env,used_unknown,e)]
    else find_case pexps value
  end

val interp_main : interp_mode -> top_level -> lenv -> lmem -> (exp tannot) -> (outcome * lmem * lenv)
val exp_list : interp_mode -> top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> lenv -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * lenv)
val interp_lbind : interp_mode -> top_level -> lenv -> lmem -> (letbind tannot) -> ((outcome * lmem * lenv) * (maybe ((exp tannot) -> (letbind tannot))))
val interp_alias_read : interp_mode -> top_level -> lenv -> lmem -> (alias_spec tannot) -> (outcome * lmem * lenv)

let resolve_outcome to_match value_thunk action_thunk =
  match to_match with
    | (Value v,lm,le) -> value_thunk v lm le
    | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
    | (Error l s,lm,le) -> (Error l s,lm,le)
  end

let update_stack (Action act stack) fn = Action act (fn stack)  

let debug_out fn value e tl lm le = 
  (Action (Step (get_exp_l e) fn value) (Thunk_frame e tl le lm Top),lm,le)

let to_exps mode env vals = 
  List.foldr (fun v (es,env) -> let (e,env') = to_exp mode env v in (e::es, union_env env' env)) ([],env) vals

let get_num v = match v with
  | V_lit (L_aux (L_num n) _) -> n
  | _ -> 0 end

(*Interpret a list of expressions, tracking local state but evaluating in the same scope (i.e. not tracking env) *)
let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
  match exps with
  | [ ] -> (Value (build_v vals), l_mem, l_env)
  | e::exps -> 
    resolve_outcome (interp_main mode t_level l_env l_mem e)
                    (fun value lm le -> exp_list mode t_level build_e build_v l_env lm (vals++[value]) exps)
                    (fun a -> update_stack a (add_to_top_frame 
                                                (fun e env -> 
                                                  let (es,env') = to_exps mode env vals in (build_e (es++(e::exps)),env'))))
  end

and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
  let (typ,tag,ncs,effect) = match annot with 
    | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
    | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
  match exp with
    | E_lit lit -> 
      if is_lit_vector lit 
      then let is_inc = (match typ with 
	| T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> true | _ -> false end) in
           (Value (litV_to_vec lit is_inc),l_mem,l_env) 
      else (Value (V_lit lit), l_mem,l_env)
    | E_cast ((Typ_aux typ _) as ctyp) exp -> 
      (*Cast is either a no-op, a signal to read a register, or a signal to change the start of a vector *)
      resolve_outcome 
	(interp_main mode t_level l_env l_mem exp)
	(fun v lm le -> 
	  (* Potentially use cast to change vector start position *)
	  let conditional_update_vstart () =
	    match typ with
	      | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
		match (detaint v) with 
		  | V_vector start inc vs ->
		    if start = i then (Value v,lm,le) else (Value (update_vector_start i 1 v),lm,le)
		  | _ -> (Value v,lm,le) end
	      | _ -> (Value v,lm,le) end in
          (match (tag,detaint v) with 
	    (*Cast is telling us to read a register*)
	    | (Tag_extern _, V_register regform) ->
	      (Action (Read_reg regform Nothing) 
	         (Hole_frame redex_id
		    (E_aux (E_id redex_id) (Unknown, (val_annot (reg_to_t regform)))) t_level le lm Top), lm,le)
	    (*Cast is changing vector start position, potentially*)
	    | (_,v) -> conditional_update_vstart () end))
	(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env))))
    | E_id id -> 
      let name = get_id id in
      match tag with
	| Tag_empty -> 
	  match in_lenv l_env id with
	  | V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
	  | value -> (Value value,l_mem,l_env) end
        | Tag_global ->
	  match in_env lets id with
	    | Just(value) -> (Value value, l_mem,l_env)
	    | Nothing -> 
	      (match in_env regs id with
		| Just(value) -> (Value value, l_mem,l_env)
		| Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_global"),l_mem,l_env) end) end
        | Tag_enum ->
          match in_env lets id with
            | Just(value) -> (Value value,l_mem,l_env)
	    | Nothing -> (Error l ("Internal error: " ^ name ^ " unbound on Tag_enum "), l_mem,l_env)
	    end 
        | Tag_extern _ -> (* update with id here when it's never just "register" *)
	  let regf = match in_lenv l_env id with (* Check for local treatment of a register as a value *)
	    | V_register regform -> regform
	    | _ -> 
	      match in_env regs id with (* Register isn't a local value, so pull from global environment *)
		| Just(V_register regform) -> regform
		| _ -> Reg id annot end end in
	  (Action (Read_reg regf Nothing)
	          (Hole_frame redex_id
		         (E_aux (E_id redex_id) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env)
        | Tag_alias -> 
	  match in_env aliases id with
	    | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
	    | _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
        | _ -> (Error l ("Internal error: tag other than empty,enum,or extern for " ^ name),l_mem,l_env)
        end
    | E_if cond thn els ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem cond)
	(fun value_whole lm le -> 
	  let value = detaint value_whole in
	  match (value,mode.eager_eval) with
	    (*TODO remove booleans here when fully removed elsewhere *)
	    | (V_lit(L_aux L_one _),true) -> interp_main mode t_level l_env lm thn
	    | (V_lit(L_aux L_one _),false) -> debug_out Nothing Nothing thn t_level lm l_env
	    | (V_vector _ _ [(V_lit(L_aux L_one _))],true) -> interp_main mode t_level l_env lm thn
	    | (V_vector _ _ [(V_lit(L_aux L_one _))],false) -> debug_out Nothing Nothing thn t_level lm l_env
	    | (V_unknown,_) -> interp_main mode t_level l_env lm (E_aux (E_block [thn;els]) (l,annot))
            | (_,true) -> interp_main mode t_level l_env lm els 
	    | (_,false) -> debug_out Nothing Nothing els t_level lm l_env end)
        (fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_if c thn els) (l,annot), env))))
    | E_for id from to_ by ((Ord_aux o _) as order) exp ->
      let is_inc = match o with | Ord_inc -> true | _ -> false end in
      resolve_outcome 
	(interp_main mode t_level l_env l_mem from)
        (fun from_val_whole lm le ->
	  let from_val = detaint from_val_whole in
          let (from_e,env) = to_exp mode le from_val_whole in
          match from_val with
            | V_lit(L_aux(L_num from_num) fl) -> 
              resolve_outcome 
		(interp_main mode t_level env lm to_)
                (fun to_val_whole lm le ->
		  let to_val = detaint to_val_whole in
		  let (to_e,env) = to_exp mode le to_val_whole in
                  match to_val with
                    | V_lit(L_aux (L_num to_num) tl) ->
                      resolve_outcome 
                        (interp_main mode t_level env lm by)
                        (fun by_val_whole lm le ->
			  let by_val = detaint by_val_whole in
			  let (by_e,env) = to_exp mode le by_val_whole in
                          match by_val with 
                            | V_lit (L_aux (L_num by_num) bl) ->
                              if ((is_inc && (from_num > to_num)) || (not(is_inc) && (from_num < to_num)))  
                              then (Value(V_lit (L_aux L_unit l)),lm,le)
                              else
				let (ftyp,ttyp,btyp) = (val_typ from_val,val_typ to_val,val_typ by_val) in
				let augment_annot = (fl, val_annot (combine_typs [ftyp;ttyp])) in
				let diff = L_aux (L_num (if is_inc then from_num+by_num else from_num - by_num)) fl in
				let (augment_e,env) = match (from_val_whole,by_val_whole) with
				  | (V_lit _, V_lit _) -> ((E_aux (E_lit diff) augment_annot), env)
				  | (V_track _ rs, V_lit _) -> to_exp mode env (taint (V_lit diff) rs)
				  | (V_lit _, V_track _ rs) -> to_exp mode env (taint (V_lit diff) rs)
				  | (V_track _ r1, V_track _ r2) -> 
				    (to_exp mode env (taint (V_lit diff) (r1 ++ r2))) end in
				let  e = 
				  (E_aux (E_block 
					    [(E_aux 
						(E_let 
						   (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
						      (Unknown,val_annot ftyp))
						   exp) (l,annot));
					     (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
					    (l,annot)) in
				if mode.eager_eval
				then interp_main mode t_level env lm e 
				else debug_out Nothing Nothing e t_level lm env
                            | V_unknown -> 
			      let e = 
				(E_aux (E_let 
					  (LB_aux 
					     (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
					     (fl, val_annot (val_typ from_val)))
					  exp) (l,annot)) in
			      interp_main mode t_level env lm e
                            | _ -> (Error l "internal error: by must be a number",lm,le) end)
                        (fun a -> update_stack a 
			  (add_to_top_frame (fun b env -> (E_aux (E_for id from_e to_e b order exp) (l,annot), env))))
		    | V_unknown -> 
		      let e =
			(E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
					      (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
		      interp_main mode t_level env lm e
                    | _ -> (Error l "internal error: to must be a number",lm,env) end)
                (fun a -> update_stack a 
		  (add_to_top_frame (fun t env -> 
		    (E_aux (E_for id from_e t by order exp) (l,annot), env))))
	    | V_unknown ->
	      let e =
		(E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
				      (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
	      interp_main mode t_level env lm e
            | _ -> (Error l "internal error: from must be a number",lm,le) end)
        (fun a -> update_stack a (add_to_top_frame (fun f env -> (E_aux (E_for id f to_ by order exp) (l,annot), env))))
    | E_case exp pats ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem exp)
        (fun v lm le ->
          match find_case pats v with
            | [] -> (Error l ("No matching patterns in case for value " ^ (string_of_value v)),lm,le)
            | [(env,used_unknown,exp)] -> 
	      if mode.eager_eval
	      then interp_main mode t_level (union_env env l_env) lm exp
	      else debug_out Nothing Nothing exp t_level lm (union_env env l_env)
	    | multi_matches ->
	      let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
	      interp_main mode t_level l_env lm (E_aux (E_block lets) (l,annot))
	 end)
        (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env))))
    | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> 
      let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
      exp_list mode t_level 
	(fun es -> 
	  (E_aux 
	     (E_record 
		(FES_aux (FES_Fexps 
			    (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es) false) fes_annot))
	          (l,annot)))
	(fun vs -> (V_record typ (List.zip fields vs))) l_env l_mem [] exps
    | E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem exp)
        (fun rv lm le -> match rv with
          | V_record t fvs ->
            let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
            resolve_outcome 
	      (exp_list mode t_level 
		        (fun es -> 
                          let (e,_) = (to_exp <|mode with track_values = false|> eenv rv) in
			  (E_aux (E_record_update e 
				    (FES_aux (FES_Fexps 
						(map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
						   fields es) false) fes_annot))
			     (l,annot)))
                        (fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
              (fun vs lm le -> (Value (fupdate_record rv vs), lm, le))
              (fun a -> a) (*Due to exp_list this won't happen, but we want to functionaly update on Value *)
	  | V_unknown -> (Value V_unknown, lm, le)
          | _ -> (Error l "internal error: record update requires record",lm,le) end)
        (fun a -> update_stack a 
	  (add_to_top_frame 
	     (fun e env -> (E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot), env))))
    | E_list(exps) ->
      exp_list mode t_level (fun exps -> E_aux (E_list exps) (l,annot)) V_list l_env l_mem [] exps
    | E_cons hd tl ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem hd)
        (fun hdv lm le -> 
	  resolve_outcome
            (interp_main mode t_level l_env lm tl)
            (fun tlv lm le -> match detaint tlv with 
              | V_list t -> (Value (retaint tlv (V_list (hdv::t))),lm,le)
	      | V_unknown -> (Value (retaint tlv V_unknown),lm,le)
              | _ -> (Error l "Internal error '::' of non-list value",lm,le) end)
            (fun a -> update_stack a 
              (add_to_top_frame 
		 (fun t env -> let (hde,env') = to_exp mode env hdv in (E_aux (E_cons hde t) (l,annot),env')))))
        (fun a -> update_stack a (add_to_top_frame (fun h env -> (E_aux (E_cons h tl) (l,annot), env))))
    | E_field exp id -> 
      resolve_outcome 
	(interp_main mode t_level l_env l_mem exp)
        (fun value_whole lm le -> 
          match detaint value_whole with 
            | V_record t fexps -> 
	      (match in_env fexps id with
                | Just v -> (Value (retaint value_whole v),lm,l_env)
                | Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end)
	    | V_unknown -> (Value (retaint value_whole V_unknown),lm,l_env)
            | _ -> (Error l "Internal error, neither register nor record at field access",lm,le) end)
        (fun a -> 
	  match (exp,a) with
	    | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
	       (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_))) as regf) Nothing) s)) ->
	      match in_env subregs (Id_aux (Id id') Unknown) with
		| Just(indexes) ->
		  (match in_env indexes id with
		    | Just ir -> 
		      (Action (Read_reg (SubReg id regf ir) Nothing) s)
		    | _ -> Error l "Internal error, unrecognized read, no id"
	           end) 
		| Nothing -> Error l "Internal error, unrecognized read, no reg" end
            | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
               (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_))) as regf) Nothing) s))->
	      match in_env subregs (Id_aux (Id id') Unknown) with
		| Just(indexes) ->
		  match in_env indexes id with
		    | Just ir -> 
		      (Action (Read_reg (SubReg id regf ir) Nothing) s)
		    | _ -> Error l "Internal error, unrecognized read, no id"
		                end 
                | Nothing -> Error l "Internal error, unrecognized read, no reg" end
             | _ -> update_stack a (add_to_top_frame (fun e env -> (E_aux(E_field e id) (l,annot),env))) end)
    | E_vector_access vec i ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem i)
        (fun iv lm le -> 
	  match detaint iv with
	    | V_unknown -> (Value iv,lm,le)
	    | V_lit (L_aux (L_num n) ln) ->
              resolve_outcome
		(interp_main mode t_level l_env lm vec)
		(fun vvec lm le ->
		  let v_access vvec num = (match (vvec,num) with
		    | (V_vector _ _ _,V_lit _) -> access_vector vvec n
		    | (V_vector_sparse _ _ _ _ _,V_lit _) -> access_vector vvec n
		    | (V_vector _ _ _,V_unknown) -> V_unknown
		    | (V_vector_sparse _ _ _ _ _,V_unknown) -> V_unknown
		    | (V_unknown,_) -> V_unknown 
		    | _ -> Assert_extra.failwith 
		      ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]") end) in
		  (Value (binary_taint v_access vvec iv),lm,le))
		(fun a ->
		  match a with
		    | Action (Read_reg reg Nothing) stack -> 
		      (match vec with
			| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
			| _ -> Action (Read_reg reg Nothing) 
			  (add_to_top_frame 
			     (fun v env -> 
			       let (iv_e, env) = to_exp mode env iv in
			       (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
		    | Action (Read_reg reg (Just (o,p))) stack ->
		      (match vec with
			| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
			| _ -> Action (Read_reg reg (Just (o,p))) 
			  (add_to_top_frame 
			     (fun v env -> 
			       let (iv_e, env) = to_exp mode env iv in
			       (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
		    | _ -> 
		      update_stack a 
			(add_to_top_frame 
			   (fun v env -> 
			     let (iv_e, env) = to_exp mode env iv in
			     (E_aux (E_vector_access v iv_e) (l,annot), env))) end)
            | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
        (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_access vec i) (l,annot), env))))
    | E_vector_subrange vec i1 i2 ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem i1)
        (fun i1v lm le ->
	  match detaint i1v with
	    | V_unknown -> (Value i1v,lm,le)
	    | V_lit (L_aux (L_num n1) nl1) -> 
              resolve_outcome 
		(interp_main mode t_level l_env lm i2)
		(fun i2v lm le ->
		  match detaint i2v with
		    | V_unknown -> (Value i2v,lm,le)
		    | _ ->
		      resolve_outcome 
			(interp_main mode t_level l_env lm vec)
			(fun vvec lm le ->
			  let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
			  let take_slice vtup vvec =
			    (match vtup with
			      | V_tuple [v1;v2] ->
				(match (detaint v1, detaint v2) with 
				  | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) ->
				    (match vvec with
				      | V_vector _ _ _ -> slice_vector vvec n1 n2
				      | V_vector_sparse _ _ _ _ _ -> slice_vector vvec n1 n2
				      | V_unknown -> 
					let inc = n1 < n2 in
					V_vector n1 inc 
					  (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown)
				      | _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end)
			      | _ -> Assert_extra.failwith("slice not a tuple of nums " ^ (string_of_value vtup)) end) in
			  (Value (binary_taint take_slice slice vvec), lm,le))
			(fun a -> 
			  let rebuild v env = let (ie1,env) = to_exp mode env i1v in
					      let (ie2,env) = to_exp mode env i2v in
					      (E_aux (E_vector_subrange v ie1 ie2) (l,annot), env) in
			  match a with 
			    | Action (Read_reg reg Nothing) stack ->
			      match vec with
				| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> 
				  Action (Read_reg reg (Just((get_num i1v),(get_num i2v)))) stack
				| _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end
		            | Action (Read_reg reg (Just (o,p))) stack ->
			      match vec with
				| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> 
				  Action (Read_reg reg (Just((get_num i1v),(get_num i2v)))) stack
				| _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end
                            | _ -> update_stack a (add_to_top_frame rebuild) end)
		 end)
                (fun a -> update_stack a 
		  (add_to_top_frame 
		     (fun i2 env -> 
		       let (ie1,env) = to_exp mode env i1v in
		       (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env))))
	 end) 
        (fun a -> 
	  update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env))))
    | E_vector_update vec i exp ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem i)
        (fun vi lm le ->
          (match (detaint vi) with
            | V_lit (L_aux (L_num n1) ln1) ->
              (resolve_outcome 
		 (interp_main mode t_level le lm exp)
                 (fun vup lm le ->
                   resolve_outcome 
		     (interp_main mode t_level le lm vec)
                     (fun vec lm le ->
		       let fvup vi vec = (match vec with
			 | V_vector _ _ _ -> fupdate_vec vec n1 vup
			 | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec n1 vup
			 | V_unknown -> V_unknown
                         | _ -> Assert_extra.failwith "Update of vector given non-vector" end) in
		       (Value (binary_taint fvup vi vec),lm,le))
                     (fun a -> update_stack a 
		       (add_to_top_frame 
			  (fun v env ->
                            let (eup,env') = (to_exp mode env vup) in 
			    let (ei, env') = (to_exp mode env' vi) in
                            (E_aux (E_vector_update v ei eup) (l,annot), env')))))
                 (fun a -> update_stack a 
		   (add_to_top_frame 
		      (fun e env -> 
			let (ei, env) = to_exp mode env vi in
			(E_aux (E_vector_update vec ei e) (l,annot), env)))))
	    | V_unknown -> (Value vi,lm,l_env)
            | _ -> Assert_extra.failwith "Update of vector requires number for access" end))
        (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_update vec i exp) (l,annot), env))))
    | E_vector_update_subrange vec i1 i2 exp ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem i1)
        (fun vi1 lm le ->
	  match detaint vi1 with
	    | V_unknown -> (Value vi1,lm,le)
            | V_lit (L_aux (L_num n1) ln1) ->
              resolve_outcome 
                (interp_main mode t_level l_env lm i2) 
                (fun vi2 lm le ->
		  match detaint vi2 with
		    | V_unknown -> (Value vi2,lm,le)
                    | V_lit (L_aux (L_num n2) ln2) ->
                      resolve_outcome 
			(interp_main mode t_level l_env lm exp)
                        (fun v_rep lm le ->
                          (resolve_outcome 
                             (interp_main mode t_level l_env lm vec)
                             (fun vvec lm le ->
			       let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in
			       let fup_v_slice v1 vvec = (match vvec with
                                 | V_vector _ _ _ -> fupdate_vector_slice vvec v_rep n1 n2
				 | V_vector_sparse _ _ _ _ _ -> fupdate_vector_slice vvec v_rep n1 n2
				 | V_unknown -> V_unknown
				 | _ -> Assert_extra.failwith "Vector update requires vector" end) in
			       (Value (binary_taint fup_v_slice slice vvec),lm,le))
                             (fun a -> update_stack a 
                               (add_to_top_frame 
				  (fun v env -> 
                                    let (e_rep,env') = to_exp mode env v_rep in
                                    let (ei1, env') = to_exp mode env' vi1 in
                                    let (ei2, env') = to_exp mode env' vi2 in
                                    (E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env'))))))
                        (fun a -> update_stack a 
                          (add_to_top_frame 
			     (fun e env -> 
                               let (ei1,env') = to_exp mode env vi1 in
                               let (ei2,env') = to_exp mode env' vi2 in
                               (E_aux (E_vector_update_subrange vec ei1 ei2 e) (l,annot),env'))))
                    | _ -> Assert_extra.failwith "vector update requires number" end)
                (fun a -> 
		  update_stack a (add_to_top_frame 
                                    (fun i2 env -> 
                                      let (ei1, env') = to_exp mode env vi1 in
                                      (E_aux (E_vector_update_subrange vec ei1 i2 exp) (l,annot), env'))))
            | _ -> Assert_extra.failwith "vector update requires number" end)
        (fun a -> 
	  update_stack a 
	    (add_to_top_frame (fun i1 env -> (E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot), env))))
    | E_vector_append e1 e2 ->
      resolve_outcome 
	(interp_main mode t_level l_env l_mem e1)
        (fun v1 lm le ->
         match detaint v1 with
	    | V_unknown -> (Value v1,lm,l_env)
            | _ ->
              (resolve_outcome 
		 (interp_main mode t_level l_env lm e2)
                 (fun v2 lm le ->
		   let append v1 v2 = (match (v1,v2) with
                     | (V_vector m inc vals1, V_vector _ _ vals2) -> V_vector m inc (vals1++vals2)
		     | (V_vector m inc vals1, V_vector_sparse _ len _ vals2 d) ->
		       let original_len = integerFromNat (List.length vals1) in
		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
		       let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
		       V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d
		     | (V_vector_sparse m len inc vals1 d, V_vector _ _ vals2) ->
		       let new_len = integerFromNat (List.length vals2) in
		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
		       V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d
		     | (V_vector_sparse m len inc vals1 d, V_vector_sparse _ new_len _ vals2 _) ->
		       let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
		       V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d
		     | (V_unknown,_) -> V_unknown (*update to get length from type*)
		     | (_,V_unknown) -> V_unknown (*see above*)
                     | _ -> Assert_extra.failwith "vector concat requires vector" end) in
		   (Value (binary_taint append v1 v2),lm,le))
                 (fun a -> update_stack a (add_to_top_frame 
                                             (fun e env -> 
                                               let (e1,env') = to_exp mode env v1 in
                                               (E_aux (E_vector_append e1 e) (l,annot),env'))))) end)
        (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_vector_append e e2) (l,annot),env))))
    | E_tuple(exps) -> 
      exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
    | E_vector(exps) ->
      let is_inc = (match typ with
        | T_app "vector" (T_args [ _; _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
        | _ -> false end) in
      let base = integerFromNat (if is_inc then 0 else (List.length exps) - 1) in
      exp_list mode t_level 
        (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector base is_inc vals) l_env l_mem [] exps
    | E_vector_indexed iexps (Def_val_aux default dannot) ->
      let (indexes,exps) = List.unzip iexps in
      let (is_inc,base,len) = (match typ with
        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux Ord_inc _); _]) -> 
	  (true,base,len)
        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux _ _); _]) -> 
	  (false,base,len) end) in
      (match default with
	| Def_val_empty ->
	  exp_list mode t_level 
	    (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) 
				                (Def_val_aux default dannot)) (l,annot)))
            (fun vals -> V_vector (if indexes=[] then 0 else (List_extra.head indexes)) is_inc vals)
	    l_env l_mem [] exps
	| Def_val_dec default_exp ->
	  let (b,len) = match (base,len) with
	    | (Ne_const b,Ne_const l) -> (b,l) end in
	  resolve_outcome 
	    (interp_main mode t_level l_env l_mem default_exp)
	    (fun v lm le -> 
	      exp_list mode t_level 
                (fun es -> 
                  let (ev,_) = to_exp <|mode with track_values = false |> eenv v in
                  (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
			    (Def_val_aux (Def_val_dec ev) dannot))
		     (l,annot)))
		(fun vs -> (V_vector_sparse b len is_inc (map2 (fun i v -> (i,v)) indexes vs) v)) l_env l_mem [] exps)
	    (fun a -> 
	      update_stack a 
		(add_to_top_frame (fun e env -> 
		  (E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot), env)))) end)	  
    | E_block exps -> interp_block mode t_level l_env l_env l_mem l annot exps
    | E_nondet exps ->
      (Action (Nondet exps) 
	      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,(intern_annot annot))) t_level l_env l_mem Top),
       l_mem, l_env)
    | E_app f args ->
      (match (exp_list mode t_level 
                (fun es -> E_aux (E_app f es) (l,annot)) 
		(fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) 
		l_env l_mem [] args) with
      | (Value v,lm,le) -> 
        let name = get_id f in 
        (match tag with
        | Tag_global ->
	  (match find_function defs f with
	    | Just(funcls) -> 
              (match find_funcl funcls v with
		| [] -> 
		  (Error l ("No matching pattern for function " ^ name ^
			       " on value " ^ (string_of_value v)),l_mem,l_env)
		| [(env,used_unknown,exp)] -> 
		  resolve_outcome 
                    (if mode.eager_eval 
		     then (interp_main mode t_level env emem exp)
		     else (debug_out (Just name) (Just v) exp t_level emem env))  
	            (fun ret lm le -> (Value ret, l_mem,l_env))
                    (fun a -> update_stack a 
		      (fun stack -> (Hole_frame (id_of_string "0") 
				       (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
				       t_level l_env l_mem stack)))
                | multi_matches ->
                  let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
                  interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot))
               end)
            | Nothing -> 
	      (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
	| Tag_empty -> 
	  (match find_function defs f with
	  | Just(funcls) -> 
            (match find_funcl funcls v with
	    | [] -> 
              (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
	    | [(env,used_unknown,exp)] -> 
	      resolve_outcome 
                (if mode.eager_eval 
		 then (interp_main mode t_level env emem exp)
		 else (debug_out (Just name) (Just v) exp t_level emem env))  
	        (fun ret lm le -> (Value ret, l_mem,l_env))
                (fun a -> update_stack a 
		  (fun stack -> (Hole_frame (id_of_string "0") 
				   (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
				   t_level l_env l_mem stack)))
             end)
          | Nothing -> 
	    (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
	| Tag_spec ->  
          (match find_function defs f with
	  | Just(funcls) -> 
            (match find_funcl funcls v with
	    | [] -> 
              (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
	    | [(env,used_unknown,exp)] -> 
              resolve_outcome 
		(if mode.eager_eval 
		 then (interp_main mode t_level env emem exp)
                 else (debug_out (Just name) (Just v) exp t_level emem env))
	        (fun ret lm le -> (Value ret, l_mem,l_env))
                (fun a -> update_stack a 
		  (fun stack -> 
                    (Hole_frame (id_of_string "0") 
                       (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack)))
             end)
          | Nothing -> 
	    (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
        | Tag_ctor ->
          (match in_ctors ctors f with
          | Just(_) -> (Value (V_ctor f typ v), lm, le)
          | Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
           end)
        | Tag_extern opt_name ->
	  let effects = (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) in
          let name_ext = match opt_name with | Just s -> s | Nothing -> name end in
          if has_rmem_effect effects 
          then
            (Action (Read_mem (id_of_string name_ext) v Nothing) 
	            (Hole_frame (Id_aux (Id "0") l) 
                                (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
          else if has_barr_effect effects
          then 
            (Action (Barrier (id_of_string name_ext) v)
                    (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
	  else if has_wmem_effect effects
	  then 
	    (*TODO This is wrong, need to split up value or unsplit generally*)
	    (Action (Write_mem (id_of_string name_ext) v Nothing v) 
	       (Hole_frame (Id_aux (Id "0") l)
		  (E_aux (E_id (Id_aux (Id "0") l)) (l, intern_annot annot)) t_level le lm Top),lm,le)
          else 
            (Action (Call_extern name_ext v) 
	            (Hole_frame (Id_aux (Id "0") l) 
                                (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
        | _ ->
	  (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end)
      | out -> out end)
    | E_app_infix lft op r -> 
       let op = match op with
       | Id_aux (Id x) il -> Id_aux (DeIid x) il
       | _ -> op
       end in
      let name = get_id op in
      resolve_outcome 
	(interp_main mode t_level l_env l_mem lft)
        (fun lv lm le -> 
          resolve_outcome 
	    (interp_main mode t_level l_env lm r)
            (fun rv lm le -> 
              match tag with
                | Tag_global ->
		  (match find_function defs op with
		    | Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
                    | Just (funcls) ->
		      (match find_funcl funcls (V_tuple [lv;rv]) with 
			| [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
			| [(env,used_unknown,exp)] ->
			  resolve_outcome 
			    (if mode.eager_eval
			     then (interp_main mode t_level env emem exp)
			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env)) 
			    (fun ret lm le -> (Value ret,l_mem,l_env))
                            (fun a -> update_stack a 
			      (fun stack -> 
				(Hole_frame (Id_aux (Id "0") l)
				   (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
				   t_level l_env l_mem stack)))
				                end)end)
		| Tag_empty -> 
		  (match find_function defs op with
		    | Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
                    | Just (funcls) ->
		      (match find_funcl funcls (V_tuple [lv;rv]) with 
			| [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
			| [(env,used_unknown,exp)] ->
			  resolve_outcome 
			    (if mode.eager_eval
			     then (interp_main mode t_level env emem exp)
			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env)) 
			    (fun ret lm le -> (Value ret,l_mem,l_env))
                            (fun a -> update_stack a 
			      (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,annot))
					       t_level l_env l_mem stack)))
		       end)end)
                | Tag_spec ->
                  (match find_function defs op with
		    | Nothing -> (Error l ("No function definition found for " ^ name),lm,le)
                    | Just (funcls) ->
		      (match find_funcl funcls (V_tuple [lv;rv]) with 
			| [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
			| [(env,used_unknown,exp)] ->
			  resolve_outcome 
			    (if mode.eager_eval 
			     then (interp_main mode t_level env emem exp)
			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env))
			    (fun ret lm le -> (Value ret,l_mem,l_env))
                            (fun a -> update_stack a 
			      (fun stack -> (Hole_frame (Id_aux (Id "0") l)
					       (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
					       t_level l_env l_mem stack)))
		       end)end)
                | Tag_extern ext_name ->
                  let ext_name = match ext_name with Just s -> s | Nothing -> name end in
        (Action (Call_extern ext_name (V_tuple [lv;rv])) 
	   (Hole_frame redex_id 
	      (E_aux (E_id redex_id) (l,intern_annot annot)) t_level le lm Top),lm,le) end)
            (fun a -> update_stack a 
              (add_to_top_frame 
                 (fun r env -> let (el,env') = to_exp mode env lv in (E_aux (E_app_infix el op r) (l,annot), env')))))
        (fun a -> update_stack a (add_to_top_frame (fun lft env -> (E_aux (E_app_infix lft op r) (l,annot), env))))
  | E_exit exp ->
    (Action (Exit exp) 
            (Thunk_frame (E_aux (E_lit (L_aux L_unit Unknown)) (l, intern_annot annot)) 
	       t_level l_env l_mem Top),l_mem, l_env)
  | E_let (lbind : letbind tannot) exp -> 
    match (interp_letbind mode t_level l_env l_mem lbind) with
    | ((Value v,lm,le),_) ->
      if mode.eager_eval
      then interp_main mode t_level le lm exp
      else debug_out Nothing Nothing exp t_level lm le                                           
    | (((Action a s as o),lm,le),Just lbuild) ->  
      ((update_stack o (add_to_top_frame (fun e env -> (E_aux (E_let (lbuild e) exp) (l,annot), env)))),lm,le)
    | (e,_) -> e end
  | E_assign lexp exp ->
    resolve_outcome 
      (interp_main mode t_level l_env l_mem exp)
      (fun v lm le -> 
        (match create_write_message_or_update mode t_level v l_env lm true lexp with
          | (outcome,Nothing) -> outcome
          | (outcome,Just lexp_builder) ->
            resolve_outcome outcome
              (fun v lm le -> (Value v,lm,le))
              (fun a -> 
		(match a with
		  | (Action (Write_reg regf range value) stack) -> (Action (Write_reg regf range value) stack)
		  | (Action (Write_mem id a range value) stack) -> (Action (Write_mem id a range value) stack)
		  | _ -> update_stack a (add_to_top_frame 
					   (fun e env -> 
                                             let (ev,env') = (to_exp mode env v) in
                                             let (lexp,env') = (lexp_builder e env') in
                                             (E_aux (E_assign lexp ev) (l,annot),env'))) end))
	 end))
      (fun a -> update_stack a (add_to_top_frame (fun v env -> (E_aux (E_assign lexp v) (l,annot), env))))
  end

(*TODO shrink location information on recursive calls *)
 and interp_block mode t_level init_env local_env local_mem l tannot exps =
   match exps with
    | [] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
    | [exp] -> 
      if mode.eager_eval
      then interp_main mode t_level local_env local_mem exp
      else debug_out Nothing Nothing exp t_level local_mem local_env
    | exp:: exps ->
      resolve_outcome (interp_main mode t_level local_env local_mem exp)
                      (fun _ lm le -> 
			if mode.eager_eval
			then interp_block mode t_level init_env le lm l tannot exps
			else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
                      (fun a -> update_stack a 
			(add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
    end

and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
   let (Env defs instrs lets regs ctors subregs aliases) = t_level in
  let (typ,tag,ncs,ef) = match annot with 
    | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
    | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
   match lexp with
    | LEXP_id id -> 
      match tag with
	| Tag_empty ->
	  match detaint (in_lenv l_env id) with
	    | ((V_boxref n t) as v) -> 
	      if is_top_level 
	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
	      else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
	    | V_unknown ->
	      if is_top_level then
		let (LMem c m) = l_mem in
		let l_mem = (LMem (c+1) m) in
		((Value (V_lit (L_aux L_unit l)), 
		  update_mem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
	      else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
            | v -> 
	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
	      else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
	     end 
        | Tag_global -> 
	  (match in_env lets id with
	    | Just v -> 
	      if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing)
	      else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
	    | Nothing -> ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
	   end)
        | Tag_extern _ ->
	  let regf = 
	    match in_env regs id with (*pull the regform with the most specific type annotation from env *)
	      | Just(V_register regform) -> regform
	      | _ -> Assert_extra.failwith "Register not known in regenv" end in
          let start_pos = reg_start_pos regf in
	  let reg_size = reg_size regf in
	  let request = 
            (Action (Write_reg regf Nothing (update_vector_start start_pos reg_size value))
	       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
	     l_mem,l_env) in
          if is_top_level then (request,Nothing) 
	  else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
	| Tag_alias -> 
	  let request = 
	    (match in_env aliases id with
	      | Just (AL_aux aspec (l,_)) -> 
		(match aspec with
		  | AL_subreg (RI_aux (RI_id reg)  (li, ((Just((T_id id),_,_,_)) as annot'))) subreg ->
		    (match in_env subregs (Id_aux (Id id) Unknown) with
		      | Just indexes -> 
			(match in_env indexes subreg with
			  | Just ir -> 
			    (Action 
			       (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
				  (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) 
			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
				  t_level l_env l_mem Top), l_mem, l_env)
			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
		      | _ -> 
			(Error l ("Internal error: alias spec has unknown register type " ^ id), l_mem, l_env) end)
		  | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_)) as annot'))) subreg ->
		    (match in_env subregs (Id_aux (Id id) Unknown) with
		      | Just indexes -> 
			(match in_env indexes subreg with
			  | Just ir -> 
			    (Action 
			       (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
				  (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value))
			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
				  t_level l_env l_mem Top), l_mem, l_env)
			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
		      | _ -> (Error l ("Internal error: alias spec has unknown register type "^id), l_mem, l_env) end)
		  | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
		    resolve_outcome (interp_main mode t_level l_env l_mem e) 
		      (fun v le lm -> match v with 
			| V_lit (L_aux (L_num i) _) -> 
			  (Action (Write_reg (Reg reg annot') (Just (i,i)) (update_vector_start i 1 value)) 
			          (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
				     t_level l_env l_mem Top), l_mem, l_env) end)
		      (fun a -> a)
		  | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
		    resolve_outcome (interp_main mode t_level l_env l_mem start)
		      (fun v lm le -> 
			match detaint v with 
			  | V_lit (L_aux (L_num start) _) ->
			    (resolve_outcome (interp_main mode t_level l_env lm stop)
			       (fun v le lm ->
				 (match detaint v with
				   | V_lit (L_aux (L_num stop) _) ->
				     (Action (Write_reg (Reg reg annot') (Just (start,stop)) 
						(update_vector_start start ((abs (start - stop)) +1) value)) 
					(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
					   t_level l_env l_mem Top),
				      l_mem, l_env) end))
			       (fun a -> a)) end)
		      (fun a -> a)
		  | AL_concat (RI_aux (RI_id reg1) (l1,annot1)) (RI_aux (RI_id reg2) annot2) -> 
		    let val_typ t = match t with
			  | T_app "register" (T_args [T_arg_typ t]) -> t
			  | T_abbrev _ (T_app "register" (T_args [T_arg_typ t])) -> t end in
		    let (t1,t2) = match (annot1,annot2) with
		      | (Just (t1,_,_,_), (_,(Just (t2,_,_,_)))) -> (val_typ t1,val_typ t2) end in
                   (match (t1,t2) with
		      | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]),
			 T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) ->
			(Action (Write_reg (Reg reg1 annot1) Nothing (slice_vector value b1 r1))
			        (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
						              (fst (to_exp <| mode with track_values =false|> eenv 
                                                                           (slice_vector value (r1+1) r2)))) annot2)
				              t_level l_env l_mem Top), l_mem,l_env) end) end)
	    | _ -> (Error l ("Internal error: alias not found for id " ^(get_id id)),l_mem,l_env) end) in
	  (request,Nothing)
        | _ -> 
	  ((Error l ("Internal error: writing to id with tag other than extern, empty, or alias " ^ (get_id id)),
	    l_mem,l_env),Nothing)
      end 
    | LEXP_memory id exps -> 
      match (exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing)) 
	              (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
		      l_env l_mem [] exps) with
      | (Value v,lm,le) ->
        (match tag with
        | Tag_extern ->
          let request = (Action (Write_mem id v Nothing value) 
                           (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top),
			 lm,l_env) in
          if is_top_level then (request,Nothing) 
	  else 
            (request,
             Just (fun e env->
               let (parms,env) = (to_exps mode env (match v with | V_tuple vs -> vs | v -> [v] end)) in
	       (LEXP_aux (LEXP_memory id parms) (l,annot), env)))
         end)
      | (Action a s,lm, le) -> 
	((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) env -> (LEXP_aux (LEXP_memory id es) (l,annot), env)))
      | e -> (e,Nothing) end
    | LEXP_cast typc id -> 
      match tag with
	| Tag_empty ->
	  match detaint (in_lenv l_env id) with
	    | ((V_boxref n t) as v) -> 
	      if is_top_level 
	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
	      else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
	    | V_unknown -> 	  
	      if is_top_level 
              then begin
		let (LMem c m) = l_mem in
		let l_mem = (LMem (c+1) m) in
		((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, 
		  (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
              end
              else ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
            | v -> 
	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
	      else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
          end 
        | Tag_extern _ ->
	   let regf = 
	    match in_env regs id with (*pull the regform with the most specific type annotation from env *)
	      | Just(V_register regform) -> regform
	      | _ -> Assert_extra.failwith "Register not known in regenv" end in
          let start_pos = reg_start_pos regf in
	  let reg_size = reg_size regf in
	  let request = 
            (Action (Write_reg regf Nothing (update_vector_start start_pos reg_size value)) 
	       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
	     l_mem,l_env) in
          if is_top_level then (request,Nothing)
	  else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
        | _ -> 
	  ((Error l ("Internal error: writing to id not extern or empty " ^(get_id id)),l_mem,l_env),Nothing)
      end 
    | LEXP_vector lexp exp -> 
      match (interp_main mode t_level l_env l_mem exp) with
      | (Value i,lm,le) ->
        (match detaint i with 
	| V_unknown -> ((Value i,lm,le),Nothing)
        | V_lit (L_aux (L_num n) ln) -> 
          let next_builder le_builder = 
            (fun e env -> 
              let (lexp,env) = le_builder e env in
              let (ie,env) = to_exp mode env i in
	      (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in
          (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
          | ((Value v_whole,lm,le),maybe_builder) ->
            let v = detaint v_whole in
            let nth _ = detaint (access_vector v n) in
            (match v with 
	      | V_unknown -> ((Value v_whole,lm,le),Nothing)
	      | V_boxref i _ -> 
		(match (in_mem lm i,is_top_level,maybe_builder) with
		  | ((V_vector _ _ _ as vec),true,_) ->
		    let new_vec = fupdate_vector_slice vec (V_vector 1 true [value]) n n in
		    ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm i new_vec, l_env), Nothing)
		  | ((V_track (V_vector _ _ _ as vec) r), true,_) ->
		    let new_vec = fupdate_vector_slice vec (V_vector 1 true [value])  n n in
		    ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm i (taint new_vec r),l_env),Nothing)
		  | ((V_vector _ _ _ as vec),false, Just lexp_builder) ->
		    ((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder))
		  | (v,_,_) -> Assert_extra.failwith("no vector findable in set bit, found " ^ (string_of_value v))
		 end )
              | V_vector inc m vs -> 
		(match (nth(),is_top_level,maybe_builder) with
		  | (V_register regform,true,_) ->
		    let start_pos = reg_start_pos regform in
		    let reg_size = reg_size regform in
		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
		        (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
		      l_mem,l_env),
		     Nothing)
		  | (V_register regform,false,Just lexp_builder) ->
		    let start_pos = reg_start_pos regform in
		    let reg_size = reg_size regform in
		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
		        (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
		      l_mem,l_env),
                     Just (next_builder lexp_builder))
		  | (V_boxref n t,true,_) -> 
		    ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
		  | (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing)
		  | (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
		  | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
		  | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
	      | V_vector_sparse n m inc vs d ->
              (match (nth(),is_top_level,maybe_builder) with
		| (V_register regform,true,_) ->
		    let start_pos = reg_start_pos regform in 
		    let reg_size = reg_size regform in
		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
		      l_mem,l_env),Nothing)
		| (V_register regform,false,Just lexp_builder) ->
		    let start_pos = reg_start_pos regform in
		    let reg_size = reg_size regform in
		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
		      l_mem,l_env),
                     Just (next_builder lexp_builder))				
		| (V_boxref n t,true,_) -> 
		  ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
		| (v,true,_) -> 
		  ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),lm,l_env),
		   Nothing)
		| ((V_boxref n t),false, Just lexp_builder) -> 
		  ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
		| (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
            | v -> 
	      ((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing)
	     end)
         | ((Action a s,lm,le),Just lexp_builder) ->
           (match (a,is_top_level) with
           | ((Write_reg regf Nothing value),true) -> 
	     ((Action (Write_reg regf (Just (n,n)) 
			 (if (vector_length value) = 1 
			  then (update_vector_start n 1 value)
			  else (access_vector value n))) s, lm,le), Nothing)
           | ((Write_reg regf Nothing value),false) -> 
	     ((Action (Write_reg regf (Just (n,n)) 
			 (if (vector_length value) = 1 
			  then (update_vector_start n 1 value)
			  else (access_vector value n))) s,lm,le),
	      Just  (next_builder lexp_builder))
           | ((Write_mem id a Nothing value),true) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
           | ((Write_mem id a Nothing value),false) -> 
	     ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
           | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
         | e -> e end)
        | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end)
      | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
      | e -> (e,Nothing) end
    | LEXP_vector_range lexp exp1 exp2  ->
      match (interp_main mode t_level l_env l_mem exp1) with
      | (Value i1, lm, le) ->
        (match detaint i1 with
	| V_unknown -> ((Value i1,lm,le),Nothing)
        | V_lit (L_aux (L_num n1) ln1) ->
          (match (interp_main mode t_level l_env l_mem exp2) with
          | (Value i2,lm,le) ->
            (match detaint i2 with
	    | V_unknown -> ((Value i2,lm,le),Nothing)
            | V_lit (L_aux (L_num n2) ln2) ->
              let next_builder le_builder = 
		(fun e env -> 
                  let (e1,env) = to_exp mode env i1 in
                  let (e2,env) = to_exp mode env i2 in
                  let (lexp,env) = le_builder e env in
                  (LEXP_aux (LEXP_vector_range lexp e1 e2) (l,annot), env)) in
              (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
              | ((Value v,lm,le), Just lexp_builder) ->
		(match (detaint v,is_top_level) with
                | (V_vector m inc vs,true) -> 
                  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
		| (V_boxref _ _, true) -> 
		  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
                | (V_vector m inc vs,false) ->
                  ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
		| (V_unknown,_) -> 
		  let inc =  n1 < n2 in
		  let start = if inc then n1 else (n2-1) in
		  let size = natFromInteger ((abs (n1-n2)) + 1) in      
		  ((Value (V_vector start inc (List.replicate size V_unknown)),lm,l_env),Nothing)
                | _ -> ((Error l "Vector required",lm,le),Nothing) end)
              | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
		let len = ((abs (n1-n2)) +1) in
                ((Action 
		    (Write_reg regf (Just (n1,n2)) 
		       (if (vector_length value) <= len 
			then (update_vector_start n1 len value)
			else (slice_vector value n1 n2))) s,lm,le),
		 Just (next_builder lexp_builder))
              | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
                ((Action (Write_mem id a (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
              | ((Action a s,lm,le), Just lexp_builder) ->
                ((Action a s,lm,le), Just (next_builder lexp_builder))
              | e -> e end)
            | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
          | (Action a s,lm,le) ->
            ((Action a s,lm, le), 
             Just (fun e env -> 
               let (e1,env) = to_exp mode env i1 in
               (LEXP_aux (LEXP_vector_range lexp e1 e) (l,annot), env)))
          | e -> (e,Nothing) end)
        | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
      | (Action a s,lm,le) ->
        ((Action a s, lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot), env)))
      | e -> (e,Nothing) end
   | LEXP_field lexp id ->
     (match (create_write_message_or_update mode t_level value l_env l_mem false lexp) with
     | ((Value (V_record t fexps),lm,le),Just lexp_builder) ->
       let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in 
                                             (LEXP_aux (LEXP_field lexp id) (l,annot), env)) in
       match (in_env fexps id,is_top_level) with
       | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)), update_mem lm n value, l_env),Nothing)
       | (Just (V_boxref n t),false) -> ((Value (in_mem lm n),lm,l_env),next_builder)
       | (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing)
       | (Just v,false) -> ((Value v,lm,l_env),next_builder)
       | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
     | ((Action a s,lm,le), Just lexp_builder) ->  
       let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in 
                                             (LEXP_aux (LEXP_field lexp id) (l,annot), env)) in
       match a with
       | Read_reg _ _ -> ((Action a s,lm,le), next_builder)
       | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder)
       | Call_extern _ _ -> ((Action a s,lm,le), next_builder)
       | Write_reg ((Reg _ (Just(T_id id',_,_,_))) as regf) Nothing value -> 
	 match in_env subregs (Id_aux (Id id') Unknown) with
	   | Just(indexes) ->
	     match in_env indexes id with
	       | Just ir -> 
		 ((Action (Write_reg (SubReg id regf ir) Nothing 
			     (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
		   lm,le), 
		  (if is_top_level then Nothing else next_builder))
	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
		 end 
            | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
       | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_))) as regf) Nothing value -> 
	 match in_env subregs (Id_aux (Id id') Unknown) with
	   | Just(indexes) ->
	     match in_env indexes id with
	       | Just ir -> 
		 ((Action (Write_reg (SubReg id regf ir) Nothing 
			     (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
		   lm,le), 
		  (if is_top_level then Nothing else next_builder))
	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
		 end 
            | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
       | _ -> ((Error l "Internal error, unrecognized write, no matching action",lm,le),Nothing)
       end 
     | e -> e end)
     end	

and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
  match lbind with
  | LB_val_explicit t pat exp ->
    match (interp_main mode t_level l_env l_mem exp) with
    | (Value v,lm,le) ->
      (match match_pattern pat v with
      | (true,used_unknown,env) -> ((Value (V_lit (L_aux L_unit l)), lm, (union_env env l_env)),Nothing)
      | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
    | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e ->(LB_aux (LB_val_explicit t pat e) (l,annot)))))
    | e -> (e,Nothing) end
  | LB_val_implicit pat exp ->
    match (interp_main mode t_level l_env l_mem exp) with
    | (Value v,lm,le) ->
      (match match_pattern pat v with
      | (true,used_unknown,env) -> ((Value (V_lit (L_aux L_unit l)), lm, (union_env env l_env)),Nothing)
      | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
    | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
    | e -> (e,Nothing) end
end	

and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
  let stack = Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem Top in
  let get_reg_typ_name typ =
    match typ with
      | T_id i -> i
      | T_abbrev (T_id i) _ -> i
    end in
  match alspec with
    | AL_subreg (RI_aux (RI_id reg) (li,((Just (t,_,_,_)) as annot'))) subreg ->
      let reg_ti = get_reg_typ_name t in
      (match in_env subregs (Id_aux (Id reg_ti) Unknown) with
	| Just indexes -> 
	  (match in_env indexes subreg with
	    | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot') ir) Nothing) stack, l_mem, l_env)
	    | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
	| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti), l_mem, l_env) end)
    | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
      resolve_outcome (interp_main mode t_level l_env l_mem e) 
        (fun v le lm -> match v with 
	  | V_lit (L_aux (L_num i) _) -> 
	    (Action (Read_reg (Reg reg annot') (Just (i,i))) stack, l_mem, l_env) end)
        (fun a -> a) (*Should not currently happen as type system enforces constants*)
    | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
      resolve_outcome (interp_main mode t_level l_env l_mem start)
        (fun v lm le -> 
	  match v with 
	    | V_lit (L_aux (L_num start) _) ->
	      (resolve_outcome 
		 (interp_main mode t_level l_env lm stop)
		 (fun v le lm ->
		   (match v with
		     | V_lit (L_aux (L_num stop) _) ->
		       (Action (Read_reg (Reg reg annot') (Just (start,stop))) stack, l_mem, l_env) end))
		 (fun a -> a)) end)
        (fun a -> a) (*Neither action function should occur, due to above*)
    | AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) -> 
      (Action (Read_reg (Reg reg1 annot1) Nothing)
	      (Hole_frame (Id_aux (Id "0") Unknown)
		          (E_aux (E_vector_append (E_aux (E_id (Id_aux (Id "0") l1)) (l1, (intern_annot annot1)))
    				                  (E_aux (E_id reg2) annot2)) 
			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end

let rec eval_toplevel_let handle_action tlevel env mem lbind = 
  match interp_letbind <|eager_eval=true; track_values=false;|> tlevel env mem lbind with
    | ((Value v, lm, (LEnv _ le)),_) -> Just le
    | ((Action a s,lm,le), Just le_builder) -> 
      (match handle_action (Action a s) with
	| Just value ->
	  (match s with
	    | Hole_frame id exp tl lenv lmem s ->
	      eval_toplevel_let handle_action tl (add_to_env (id,value) lenv) lmem (le_builder exp) end)
	| Nothing -> Nothing end)
    | _ -> Nothing end

let rec to_global_letbinds handle_action (Defs defs) t_level =
  let  (Env defs' instrs lets regs ctors subregs aliases) = t_level in
  match defs with
  | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
  | def::defs ->
    match def with
    | DEF_val lbind ->
      match eval_toplevel_let handle_action t_level eenv emem lbind with
	| Just le -> 
	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
	| Nothing -> 
	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs lets regs ctors subregs aliases) end
    | DEF_type (TD_aux tdef _) ->
      match tdef with
      | TD_enum id ns ids _ -> 
        let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
        to_global_letbinds handle_action (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
      | _ -> to_global_letbinds handle_action (Defs defs) t_level end
    | _ -> to_global_letbinds handle_action (Defs defs) t_level
    end
  end

(*TODO Contemplate making decode and execute environment variables instead of these constants*)
let to_top_env external_functions defs = 
  let t_level = Env defs (extract_instructions "decode" "execute" defs) 
                    [] (* empty letbind and enum values, call below will fill in any *) 
		    (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
  let (o,t_level) = to_global_letbinds external_functions defs t_level in
  match o with
    | (Value _,_,_) -> (Nothing,t_level)
    | (o,_,_) -> (Just o,t_level)
  end

let interp mode external_functions defs exp =
  match (to_top_env external_functions defs) with
    | (Nothing,t_level) -> 
      match interp_main mode t_level eenv emem exp with
	| (o,_,_) -> o
      end 
    | (Just o,_) -> o (* Should do something different for action to allow global lets to call external functions *)
  end

let rec resume_with_env mode stack value =
  match (stack,value) with
  | (Top,_) -> (Error Unknown "Top hit without expression to evaluate",eenv)
  | (Hole_frame id exp t_level env mem Top,Just value) -> 
    match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,e) -> (o,e) end 
  | (Hole_frame id exp t_level env mem stack,Just value) ->
    match resume_with_env mode stack (Just value) with
    | (Value v,e) -> 
      match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,e) -> (o,e) end 
    | (Action action stack,e) -> (Action action (Hole_frame id exp t_level env mem stack),e)
    | (Error l s,e) -> (Error l s,e)
    end  
  | (Hole_frame id exp t_level env mem stack, Nothing) ->
    match resume_with_env mode stack Nothing with
      | (Value v,e) ->
	match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,e) -> (o,e) end
      | (Action action stack,e) -> (Action action (Hole_frame id exp t_level env mem stack),e)
      | (Error l s,e) -> (Error l s,e)
    end
  | (Thunk_frame exp t_level env mem Top,_) ->
    match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end
  | (Thunk_frame exp t_level env mem stack,value) ->
    match resume_with_env mode stack value with
    | (Value v,e) -> 
      match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end 
    | (Action action stack,e) -> (Action action (Thunk_frame exp t_level env mem stack),e)
    | (Error l s,e) -> (Error l s,e)
    end  
  end

let rec resume mode stack value =
  match (stack,value) with
  | (Top,_) -> Error Unknown "Top hit without expression to evaluate"
  | (Hole_frame id exp t_level env mem Top,Just value) -> 
    match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,_) -> o end 
  | (Hole_frame id exp t_level env mem stack,Just value) ->
    match resume mode stack (Just value) with
    | Value v -> 
      match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,_) -> o end 
    | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
    | Error l s -> Error l s
    end  
  | (Hole_frame id exp t_level env mem stack, Nothing) ->
    match resume mode stack Nothing with
      | Value v ->
	match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,_) -> o end
      | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
      | Error l s -> Error l s
    end
  | (Thunk_frame exp t_level env mem Top,_) ->
    match interp_main mode t_level env mem exp with | (o,_,_) -> o end
  | (Thunk_frame exp t_level env mem stack,value) ->
    match resume mode stack value with
    | Value v -> 
      match interp_main mode t_level env mem exp with | (o,_,_) -> o end 
    | Action action stack -> Action action (Thunk_frame exp t_level env mem stack)
    | Error l s -> Error l s
    end  
  end