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 String_extra (* for 'show' to convert nat to string) *)

open import Interp_ast

type tannot = maybe (t * tag * list nec * effect)

let get_exp_l (E_aux e (l,annot)) = l

val pure : effect
let pure = Effect_aux(Effect_set []) Unknown
let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown

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)

(* Workaround Lem's inability to scrap my (type classes) boilerplate.
 * Implementing only Eq, and only for literals - hopefully this will
 * be enough, but we should in principle implement ordering for everything in
 * Interp_ast *)

val lit_eq: lit -> lit -> bool
let lit_eq (L_aux left _) (L_aux right _) =
   match (left, right) with
   | (L_unit, L_unit) -> true
   | (L_zero, L_zero) -> true
   | (L_one, L_one) -> true
   | (L_true, L_true) -> true
   | (L_false, L_false) -> true
   | (L_num n, L_num m) -> n = m
   | (L_hex h, L_hex h') -> h = h'
   | (L_bin b, L_bin b') -> b = b'
   | (L_undef, L_undef) -> true
   | (L_string s, L_string s') -> s = s'
   | (_, _) -> false
end

instance (Eq lit)
  let (=) = lit_eq
  let (<>) n1 n2 = not (lit_eq n1 n2)
end

(* 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')

let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end

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

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
  | (_, _) -> false
  end

instance (Eq value)
  let (=) = value_eq
  let (<>) n1 n2 = not (value_eq n1 n2)
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 lexical variables *)
type env = list (id * value)

let emem = LMem 1 Map.empty

type read_kind = Read_plain | Read_reserve | Read_acquire
type write_kind = Write_plain | Write_conditional | Write_release
type barrier_kind = | Barrier_plain  (* ?? *) 

(*top_level is a tuple of 
  (all definitions, letbound and enum values, register values, Typedef union constructors, and sub register mappings) *)
type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range)) * 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)
 | Exit of (exp tannot)
 | Debug of l
 | Call_extern of string * 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 * env * lmem * stack (* Stack frame waiting to fill a hole with a value *)
 | Thunk_frame of exp tannot * top_level * env * lmem * stack (* Paused stack frame *)

(*Internal representation of outcomes from running the interpreter. Actions request an external party to resolve a request *)
type outcome =
 | Value of value * tag (* If tag is external and value is register, then register value should be read *)
 | Action of action * stack
 | Error of l * string 

type interp_mode = <| eager_eval : bool |>

(* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
val to_top_env : 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 -> 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

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))
    | _ -> 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 has_rmem_effect : list base_effect -> bool
val has_barr_effect : list base_effect -> bool

(*General has_effect function that selects which effect searched for based on a numeric selector *)
let rec has_effect which efcts =
  match efcts with
  | [] -> false
  | (BE_aux e _)::efcts ->
    match (which,e) with
    | (BE_rreg,BE_rreg)    -> true 
    | (BE_wreg,BE_wreg)    -> true 
    | (BE_rmem,BE_rmem)    -> true 
    | (BE_wmem,BE_wmem)    -> true 
    | (BE_barr,BE_barr)    -> true 
    | (BE_undef,BE_undef)  -> true 
    | (BE_unspec,BE_unspec) -> true 
    | (BE_nondet,BE_nondet) -> true 
    | _ -> has_effect which efcts
    end 
  end
let has_rmem_effect = has_effect BE_rmem
let has_barr_effect = has_effect BE_barr

let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
let get_effects (Typ_aux t _) =
  match t with
    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
    | _ -> []
  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 -> (id,unit_t) end) tid_list)++(to_data_constructors (Defs defs))
      | _ -> to_data_constructors (Defs defs) end
    | _ -> to_data_constructors (Defs defs) end
   end

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

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

(* XXX Both make an endian assumption, and should use a flag to switch*)
val litV_to_vec : lit -> value
let litV_to_vec (L_aux lit l) =
  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
    V_vector 0 true 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
    V_vector 0 true 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 access_vector : value -> integer -> value
let access_vector v n =
  match v with
  | 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 
  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 =
  match v with
  | V_vector m inc vs ->
    if inc 
    then V_vector 0 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 0 (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 = 
  match (base,updates) with
  | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us) end

val update_vector_slice : value -> value -> lmem -> lmem
let rec update_vector_slice vector value mem = 
  match (vector,value) with
  | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
    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 (_,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) ->
    List.foldr (fun vbox mem -> match vbox with
                                    | V_boxref n t -> update_mem mem n v end)
      mem vs
end

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

val fupdate_vec : value -> integer -> value -> value
let fupdate_vec v n vexp =
  match 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 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 =
  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_sparse m n inc vals d,V_vector _ _ reps) ->
    let (_,repsi) = List.foldr (fun r (i,rs) -> ((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 repsi) d)
  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

let add_to_top_frame e_builder stack =
  match stack with
  | Top -> Top
  | Hole_frame id e t_level env mem stack -> Hole_frame id (e_builder e) t_level env mem stack
  | Thunk_frame e t_level env mem stack -> Thunk_frame (e_builder e) t_level env mem stack
  end

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 almost 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 env mem Top -> Thunk_frame e t_level ((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

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 id_of_string s = (Id_aux (Id s) Unknown)

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_unknown -> T_var "fresh" (*consider carrying the type along*)
  end

let rec to_exp v =
  E_aux
    (match v with
      | V_boxref n t -> E_id (Id_aux (Id (show n)) Unknown)
      | V_lit lit -> E_lit lit
      | V_tuple(vals) -> E_tuple (List.map to_exp vals)
      | V_vector n inc vals -> 
	if (inc && n=0) 
	then E_vector (List.map to_exp vals) 
	else if inc then
          E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
	                   (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
	else 
          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals)) 
	                   (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))
      | V_vector_sparse n m inc vals d ->
	E_vector_indexed ((if inc then List.reverse else (fun i -> i)) 
			     (List.map (fun (i,v) -> (i, to_exp v)) vals))
	                 (Def_val_aux (Def_val_dec (to_exp d)) (Interp_ast.Unknown,Nothing)) (*Can possibly do better*)
      | V_record t ivals -> 
	E_record(FES_aux (FES_Fexps
			    (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false) 
		   (Unknown,Nothing))
      | V_list(vals) -> E_list (List.map to_exp vals)
      | V_ctor id t vals -> 
        match vals with
        | V_lit (L_aux L_unit _) -> E_id id
        | V_tuple vals -> E_app id (map to_exp vals)
        | _ -> E_app id [to_exp vals] end
      | V_register (Reg id tan) -> E_id id
      | V_unknown -> E_id (id_of_string "-100")
     end)
    (Unknown,(val_annot (val_typ v)))

val env_to_let : env -> (exp tannot) -> (exp tannot)
let rec env_to_let_help env = match env with
  | [] -> []
  | (i,v)::env -> 
    let t = (val_typ v) in
    let tan = (val_annot t) in
    (((P_aux (P_id i) (Unknown,tan)),(to_exp v)),t)::(env_to_let_help env)
end 

let env_to_let env (E_aux e annot) = 
  match env_to_let_help 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


val find_type_def : defs tannot -> id -> maybe (type_def tannot)
val find_function : defs tannot -> id -> maybe (list (funcl tannot))

let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls

let rec find_function (Defs defs) id =
  match defs with 
  | [] -> Nothing
  | def::defs -> 
    match def with
    | DEF_fundef f -> match get_funcls id f with
      | [] -> find_function (Defs defs) id
      | funcs -> Just funcs end
    | _ -> find_function (Defs defs) id
    end 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 * list (id * value)
let rec match_pattern (P_aux p _) value =
  match p with 
  | P_lit(lit) -> 
    if is_lit_vector lit then
      let (V_vector n inc bits) = litV_to_vec lit in
      match value with
      | V_lit litv -> 
        if is_lit_vector litv then 
          let (V_vector n' inc' bits') = litV_to_vec litv in
          if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, [])
          else (false,false,[])
        else (false,false,[])
      | V_vector n' inc' bits' -> 
        if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l=r) && rest) true bits bits',false,[])
        else (false,false,[])
      | V_unknown -> (true,true,[])
      | _ -> (false,false,[]) end
    else
    match value with
    | V_lit(litv) -> (lit = litv, false,[])
    | V_unknown -> (true,true,[])
    | _ -> (false,false,[])
    end
 | P_wild -> (true,false,[])
 | P_as pat id ->  let (matched_p,used_unknown,bounds) = match_pattern pat value in
		     if matched_p then
		       (matched_p,used_unknown,(id,value)::bounds)
		     else (false,false,[])
 | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information *)
 | P_id id -> (true, false, [(id,value)])
 | 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 value in
              (matched_p, (used_unknown || used_unknown'), (new_bounds ++ bounds))
            else (false,false,[])) (true,false,[]) pats vals
     else (false,false,[])
   | V_ctor (Id_aux cid _) t v ->
     if id = cid
     then (match (pats,v) with
     | ([],(V_lit (L_aux L_unit _))) -> (true,true,[])
     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,true,[])
     | ([p],v) -> match_pattern p v
     | _ -> (false,false,[]) end)
     else (false,false,[])
   | V_unknown -> (true,true,[])
   | _ -> (false,false,[]) 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,[])
                                       | Just v -> match_pattern pat v end in
           (matched_p, (used_unknown || used_unknown'), (new_bounds ++ bounds))
         else (false,false,[])) (true,false,[]) fpats
   | V_unknown -> (true,true,[])
   | _ -> (false,false,[])
   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 value in
	   (matched_p, (used_unknown||used_unknown'), (new_bounds ++ bounds)) 
	 else (false,false,[]))
       (true,false,[]) (if inc then pats else List.reverse pats) vals
     else (false,false,[])
   | 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  -> v end) in
		     ((if inc then i+1 else i-1),matched_p,used_unknown||used_unknown',(new_bounds ++ bounds))
                else (i,false,false,[])) (n,true,false,[]) pats in
	  (matched_p,used_unknown,bounds)
     else (false,false,[])
   | V_unknown -> (true,true,[])
   | _ -> (false,false,[])
     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 (list_nth vals (if inc then i+n else i-n)) in
	   (matched_p,used_unknown||used_unknown',new_bounds++bounds)
         else (false,false,[]))
       (true,false,[]) 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 -> v end) in
	   (matched_p,used_unknown||used_unknown',new_bounds++bounds)
	 else (false,false,[]))
       (true,false,[]) ipats
   | V_unknown -> (true,true,[])
   | _ -> (false,false, [])
   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'),bounds' ++ bounds,r_vals)) (true,false,[],vals) pats in
     if matched_p && ([] = remaining_vals) then (matched_p,used_unknown,bounds) else (false,false,[]) 
   | V_unknown -> (true,true,[])
   | _ -> (false,false, []) 
   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 v in
	   (matched_p,used_unknown ||used_unknown', bounds++new_bounds)
	 else (false,false,[]))
       (true,false,[]) pats vals
     else (false,false,[])
   | V_unknown -> (true,true,[])
   | _ -> (false,false,[])
     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 v in
	   (matched_p,used_unknown|| used_unknown', bounds++new_bounds)
	 else (false,false,[]))
       (true,false,[]) pats vals
     else (false,false,[])
   | V_unknown -> (true,true,[])
   | _ -> (false,false,[]) 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,bounds,matcheds,r_vals) = vec_concat_match wilds r_vals in
	    if matched_p 
	    then (matched_p, used_unknown, (id,(V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds))::bounds,matcheds,r_vals)
	    else (false,false,[],[],[])
	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
	    (false,false,[],[],[]) (*TODO see if can have some constraint bounds here*)
	  | _ -> (false,false,[],[],[]) 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,[],[],[]) (*TODO see if can have some constraint bounds here*)
	  | _ -> (false,false,[],[],[]) end)
      | P_as (P_aux pat (l',Just(t,_,_,_))) id -> 
	let (matched_p, used_unknown, bounds,matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
	if matched_p 
	then (matched_p, used_unknown,((id,V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds)::bounds),matcheds,r_vals)
	else (false,false,[],[],[])	  
      | P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals inc l t
      | _ -> (false,false,[],[],[]) 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,[],[],r_vals)
    | pat::pats -> match r_vals with
      | [] -> (false,false,[],[],[])
      | 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',new_bounds++bounds,r :: matcheds,r_vals)
        else (false,false,[],[],[]) 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 (env * 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 (env * 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 -> env -> lmem -> (exp tannot) -> (outcome * lmem * env)
val exp_list : interp_mode -> top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * env)
val interp_lbind : interp_mode -> top_level -> env -> lmem -> (letbind tannot) -> ((outcome * lmem * env) * (maybe ((exp tannot) -> (letbind tannot))))
val interp_alias_read : interp_mode -> top_level -> env -> lmem -> (alias_spec tannot) -> (outcome * lmem * env)

let resolve_outcome to_match value_thunk action_thunk =
  match to_match with
    | (Value v tag,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 e tl lm le = (Action (Debug (get_exp_l e)) (Thunk_frame e tl le lm Top),lm,le)

(*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) Tag_empty, 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 -> (build_e ((List.map to_exp vals)++(e::exps))))))
  end

and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
  let (Env defs 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 (Value (litV_to_vec lit) Tag_empty,l_mem,l_env) 
      else (Value (V_lit lit) Tag_empty, l_mem,l_env)
    | E_cast ((Typ_aux typ _) as ctyp) exp -> 
      resolve_outcome (interp_main mode t_level l_env l_mem exp)
	              (fun v lm le -> 
                        match (tag,v) with 
	                | (Tag_extern _, V_register regform) ->
	                  (Action (Read_reg regform Nothing) 
	                     (Hole_frame (id_of_string "0")
		                (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) t_level le lm Top), lm,le)
			| (_,V_vector start inc items) -> 
			  (match typ with
			    | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
			      if start = i 
			      then (Value v tag,lm,le)
			      else (Value (V_vector i inc items) tag,lm,le)
			    | _ -> (Value v tag,lm,le) end)
			| (_,V_vector_sparse start inc len items def) ->
			  (match typ with
			    | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
			      if start = i
			      then (Value v tag,lm,le)
			      else (Value (V_vector_sparse i inc len items def) tag,lm,le) (*Shoud I trim any actual items*)
			    | _ -> (Value v tag,lm,le) end)
                        | _ -> (Value v Tag_empty,lm,le) end)
	              (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_cast ctyp e) (l,annot)))))
    | E_id id -> 
      let name = get_id id in
      match tag with
	| Tag_empty -> 
	  match in_env l_env id with
	    | Just(value) -> match value with
		             | V_boxref n t -> (Value (in_mem l_mem n) Tag_empty,l_mem,l_env)
			     | _ -> (Value value Tag_empty,l_mem,l_env) end
            | Nothing ->  (Value V_unknown Tag_empty,l_mem,l_env) end
        | Tag_global ->
	  match in_env lets id with
	    | Just(value) -> (Value value Tag_empty, l_mem,l_env)
	    | Nothing -> 
	      (match in_env regs id with
		| Just(value) -> (Value value Tag_empty, l_mem,l_env)
		| Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_global " name),l_mem,l_env) end) end
        | Tag_enum ->
          match in_env lets id with
            | Just(value) -> (Value value Tag_empty,l_mem,l_env)
	    | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_enum " name), l_mem,l_env)
	    end 
        | Tag_extern _ -> (* update with id here when it's never just "register" *)
	  let regf = match in_env l_env id with
	    | Just(V_register regform) -> regform
	    | _ -> 
	      match in_env regs id with
		| Just(V_register regform) -> regform
		| _ -> Reg id annot end end in
	  (Action (Read_reg regf Nothing)
	          (Hole_frame (Id_aux (Id "0") Unknown)
		         (E_aux (E_id (Id_aux (Id "0") l)) (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 (String.stringAppend "Internal error: tag other than empty,enum,or extern " 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 lm le -> 
			match (value,mode.eager_eval) with
                          | (V_lit(L_aux L_true _),true) -> interp_main mode t_level l_env lm thn
			  | (V_lit(L_aux L_true _),false) -> debug_out 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 els t_level lm l_env end)
                      (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) (l,annot)))))
    | 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 lm le ->
                        match from_val with
                        | (V_lit(L_aux(L_num from_num) fl) as fval) -> 
                          resolve_outcome (interp_main mode t_level le lm to_)
                                          (fun to_val lm le ->
                                            match to_val with
                                            | (V_lit(L_aux (L_num to_num) tl) as tval) ->
                                              resolve_outcome 
                                                (interp_main mode t_level le lm by)
                                                (fun by_val lm le ->
                                                  match by_val with 
                                                  | (V_lit (L_aux (L_num by_num) bl) as bval) ->
                                                    if (from_num = to_num) 
                                                    then (Value(V_lit (L_aux L_unit l)) Tag_empty,lm,le)
                                                    else
						      let (ftyp,ttyp,btyp) = (val_typ fval,val_typ tval,val_typ bval) 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))
											   (E_aux (E_lit(L_aux(L_num from_num) fl)) (fl,val_annot ftyp)))
										   (Unknown,val_annot ftyp))
										exp) (l,annot));
								      (E_aux (E_for id 
										(if is_inc 
										 then (E_aux (E_lit (L_aux (L_num (from_num + by_num)) fl)) (fl,val_annot (combine_typs [ftyp;ttyp])))
										 else (E_aux (E_lit (L_aux (L_num (from_num - by_num)) fl)) (fl,val_annot (combine_typs [ttyp;ftyp]))))
										(E_aux (E_lit (L_aux (L_num to_num) tl)) (tl,val_annot ttyp))
										(E_aux (E_lit (L_aux (L_num by_num) bl)) (bl,val_annot btyp))
										order exp) (l,annot))])
								  (l,annot)) in
						      if mode.eager_eval
						      then interp_main mode t_level le lm e 
						      else debug_out e t_level lm le
                                                  | V_unknown -> let e = (E_aux (E_let 
										   (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ fval)))
											      (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl, val_annot (val_typ fval))))
										   (fl, val_annot (val_typ fval)))
										   exp) (l,annot)) in
								 interp_main mode t_level le 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 -> 
						    (E_aux (E_for id 
							      (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl,(val_annot (val_typ fval))))
							      (E_aux (E_lit (L_aux (L_num to_num) tl)) (tl,(val_annot (val_typ tval))))
							      b order exp) (l,annot)))))
                                            | _ -> (Error l "internal error: to must be a number",lm,le) end)
                                           (fun a -> update_stack a 
					     (add_to_top_frame (fun t -> 
					       (E_aux (E_for id (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl,val_annot (val_typ fval)))
							 t by order exp) (l,annot)))))
                        | _ -> (Error l "internal error: from must be a number",lm,le) end)
                       (fun a -> update_stack a (add_to_top_frame (fun f -> (E_aux (E_for id f to_ by order exp) (l,annot)))))
    | 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",lm,le)
                        | [(env,used_unknown,exp)] -> 
			  if mode.eager_eval
			  then interp_main mode t_level (env++l_env) lm exp
			  else debug_out exp t_level lm (env++l_env)
			| multi_matches ->
			  let lets = List.map (fun (env,_,exp) -> env_to_let 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 -> (E_aux (E_case e pats) (l,annot)))))
    | 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 -> 
					       (E_aux (E_record_update (to_exp rv) 
							 (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) Tag_empty, lm, le))
                                          (fun a -> a)
			| V_unknown -> (Value V_unknown Tag_empty, lm, le)
                        | _ -> (Error l "record upate requires record",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame 
						  (fun e -> E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot))))
    | 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 tlv with 
                                                   | V_list t -> (Value(V_list (hdv::t)) Tag_empty,lm,le)
						   | V_unknwon -> (Value V_unknown Tag_empty,lm,le)
                                                   | _ -> (Error l ":: of non-list value",lm,le) end)
                                        (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) (l,annot)))))
                      (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) (l,annot))))
    | E_field exp id -> 
      resolve_outcome (interp_main mode t_level l_env l_mem exp)
                      (fun value lm le -> 
                        match value with 
                        | V_record t fexps -> match in_env fexps id with
                                            | Just v -> (Value v Tag_empty,lm,l_env)
                                            | Nothing -> (Error l "Field not found in record",lm,le) end
                        | V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                        | _ -> (Error l "Field access of vectors not implemented",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 -> E_aux(E_field e id) (l,annot))) end)
    | E_vector_access vec i ->
      resolve_outcome (interp_main mode t_level l_env l_mem i)
                      (fun iv lm le -> 
                        match iv with
                        | V_lit (L_aux (L_num n) ln) -> 
                          resolve_outcome (interp_main mode t_level l_env lm vec)
                                          (fun vvec lm le ->
                                            match vvec with
                                            | V_vector _ _ _ -> (Value (access_vector vvec n) Tag_empty,lm,le)
					    | V_vector_sparse _ _ _ _ _ -> (Value (access_vector vvec n) Tag_empty,lm,le)
					    | V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                            | _ -> (Error l "Vector access of non-vector",lm,le)end)
                                          (fun a ->
                                            match a with
                                            | Action (Read_reg reg Nothing) stack -> 
                                              if (top_hole stack) 
                                              then Action (Read_reg reg (Just(n,n))) stack 
                                              else Action (Read_reg reg Nothing) (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot))) stack)
                                            | _ -> 
                                              update_stack a 
					        (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))) end)
			| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                        | _ -> (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 -> E_aux (E_vector_access vec i) (l,annot))))
    | E_vector_subrange vec i1 i2 ->
      resolve_outcome (interp_main mode t_level l_env l_mem i1)
                      (fun i1v lm le ->
                        match i1v with
                        | V_lit (L_aux (L_num n1) ln1) ->
                          resolve_outcome (interp_main mode t_level l_env lm i2)
                                          (fun i2v lm le ->
                                            match i2v with
                                            | V_lit (L_aux (L_num n2) ln2) ->
                                              resolve_outcome (interp_main mode t_level l_env lm vec)
                                                              (fun vvec lm le ->
                                                                match vvec with
                                                                | V_vector _ _ _ -> (Value (slice_vector vvec n1 n2) Tag_empty,lm,le)
								| V_vector_sparse _ _ _ _ _ -> (Value (slice_vector vvec n1 n2) Tag_empty, lm,le)
								| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                                                | _ -> (Error l "Vector slice of non-vector",lm,le)end)
                                                              (fun a -> 
                                                                match a with 
                                                                | Action (Read_reg reg Nothing) stack ->
                                                                  if (top_hole stack)
                                                                  then Action (Read_reg reg (Just(n1,n2))) stack
                                                                  else Action (Read_reg reg Nothing) (add_to_top_frame (fun v -> (E_aux (E_vector_subrange v
                                                                                                                                           (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
                                                                                                                                           (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
                                                                                                                                        (l,annot))) stack)
                                                                | _ -> update_stack a 
                                                                  (add_to_top_frame 
								     (fun v -> (E_aux (E_vector_subrange v 
										         (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
										         (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
										  (l,annot)))) end)
					    | V_unknown -> (Value V_unknown Tag_empty, lm,le)
                                            | _ -> (Error l "vector slice given non number for last index",lm,le) end)
                                          (fun a -> update_stack a 
					    (add_to_top_frame 
					       (fun i2 -> (E_aux (E_vector_subrange vec 
								    (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
								    i2) (l,annot)))))
			| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                        | _ -> (Error l "Vector slice given non-number for first index",lm,le) end)
                       (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_aux (E_vector_subrange vec i1 i2) (l,annot)))))
    | E_vector_update vec i exp ->
      resolve_outcome (interp_main mode t_level l_env l_mem i)
                      (fun vi lm le ->
                        match 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 ->
                                                              match vec with
                                                              | V_vector _ _ _ -> (Value (fupdate_vec vec n1 vup) Tag_empty, lm,le)
							      | V_vector_sparse _ _ _ _ _ -> (Value (fupdate_vec vec n1 vup) Tag_empty,lm,le)
							      | V_unknown -> (Value V_unknown Tag_empty, lm, le)
                                                              | _ -> (Error l "Update of vector given non-vector",lm,le) end)
                                                            (fun a -> update_stack a 
							      (add_to_top_frame 
								 (fun v -> E_aux (E_vector_update v 
										    (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) 
										    (to_exp vup)) (l,annot)))))
                                          (fun a -> update_stack a 
					    (add_to_top_frame (fun e -> E_aux (E_vector_update vec 
										 (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
										 e) (l,annot))))
			| V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                        | _ -> (Error l "Update of vector requires number for access",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_update vec i exp) (l,annot))))
    | 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 vi1 with
                        | V_lit (L_aux (L_num n1) ln1) ->
                          resolve_outcome 
                            (interp_main mode t_level l_env lm i2) 
                            (fun vi2 lm le ->
                              match vi2 with
                              | 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 ->
                                         match vvec with
                                         | V_vector _ _ _ -> (Value (fupdate_vector_slice vvec v_rep n1 n2) Tag_empty,lm,le)
					 | V_vector_sparse _ _ _ _ _ -> (Value (fupdate_vector_slice vvec v_rep n1 n2) Tag_empty,lm,le)
					 | V_unknown -> (Value V_unknown Tag_empty,lm,le)
                                         | _ -> (Error l "Vector update requires vector",lm,le) end)
                                       (fun a -> update_stack a 
                                         (add_to_top_frame 
					    (fun v -> E_aux (E_vector_update_subrange v 
							       (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
							       (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)) 
							       (to_exp v_rep)) (l,annot))))))
                                  (fun a -> update_stack a 
                                    (add_to_top_frame 
				       (fun e -> E_aux (E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e) (l,annot))))
			      | V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                              | _ -> (Error l "vector update requires number",lm,le) end)
                            (fun a -> 
			      update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) (l,annot))))
			| V_unknown -> (Value V_unknown Tag_empty,lm,le)
                        | _ -> (Error l "vector update requires number",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot))))
    | E_vector_append e1 e2 ->
      resolve_outcome (interp_main mode t_level l_env l_mem e1)
                      (fun v1 lm le ->
                        match v1 with
                        | V_vector m inc vals1 ->
                          (resolve_outcome (interp_main mode t_level l_env lm e2)
                                            (fun v2 lm le ->
                                              match v2 with
                                              | V_vector _ _ vals2 -> (Value (V_vector m inc (vals1++vals2)) Tag_empty,lm,l_env)
					      | 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
						(Value (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d) Tag_empty, lm,l_env)
					      | V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                                              | _ -> (Error l "vector concat requires vector",lm,le) end)
                                            (fun a -> update_stack a (add_to_top_frame 
                                                                        (fun e -> E_aux (E_vector_append (to_exp v1) e) (l,annot)))))
			| V_vector_sparse m len inc vals1 d ->
			  (resolve_outcome (interp_main mode t_level l_env lm e2)
                                            (fun v2 lm le ->
                                              match v2 with
                                              | 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
						(Value (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d) Tag_empty, lm,l_env)
					      | V_vector_sparse _ new_len _ vals2 _ ->
						let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
						(Value (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d) Tag_empty, lm,l_env)
					      | V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                                              | _ -> (Error l "vector concat requires vector",lm,le) end)
                                            (fun a -> update_stack a (add_to_top_frame 
                                                                        (fun e -> E_aux (E_vector_append (to_exp v1) e) (l,annot)))))
			| V_unknown -> (Value V_unknown Tag_empty,lm,l_env)
                        | _ -> (Error l "vector concat requires vector",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux (E_vector_append e e2) (l,annot))))
    | 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) ->
      exp_list mode t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true 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 (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 -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
								                      (Def_val_aux (Def_val_dec (to_exp v)) 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 -> E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot)))) 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 tag_e,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 (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 exp t_level emem env))  
	            (fun ret lm le -> (Value ret Tag_empty, 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 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 exp t_level emem env))  
	                      (fun ret lm le -> (Value ret Tag_empty, 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 exp t_level emem env))
	                      (fun ret lm le -> (Value ret Tag_empty, 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) Tag_empty, lm, le)
          | Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
           end)
        | Tag_extern opt_name ->
          let name_ext = match opt_name with | Just s -> s | Nothing -> name end in
          if has_rmem_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) 
          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 (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end)
          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
            (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 other than 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 (String.stringAppend "Internal error, no function def for " name),lm,le)
                                               | Just (funcls) ->
						 (match find_funcl funcls (V_tuple [lv;rv]) with 
						   | [] -> (Error l (String.stringAppend "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 exp t_level emem env)) 
				                       (fun ret lm le -> (Value ret Tag_empty,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 (String.stringAppend "Internal error, no function def for " name),lm,le)
                                             | Just (funcls) ->
				               (match find_funcl funcls (V_tuple [lv;rv]) with 
				               | [] -> (Error l (String.stringAppend "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 exp t_level emem env)) 
				                   (fun ret lm le -> (Value ret Tag_empty,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,annot)) t_level l_env l_mem stack)))
				                end)end)
                                           | Tag_spec ->
                                             (match find_function defs op with
				             | Nothing -> (Error l (String.stringAppend "No function definition found for " name),lm,le)
                                             | Just (funcls) ->
				               (match find_funcl funcls (V_tuple [lv;rv]) with 
				               | [] -> (Error l (String.stringAppend "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 exp t_level emem env))
				                   (fun ret lm le -> (Value ret Tag_empty,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 (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) end)
                                         (fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) (l,annot)))))
                       (fun a -> update_stack a (add_to_top_frame (fun lft -> (E_aux (E_app_infix lft op r) (l,annot)))))
  | 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 tag_l,lm,le),_) ->
      if mode.eager_eval
      then interp_main mode t_level le lm exp
      else debug_out exp t_level lm le                                           
    | (((Action a s as o),lm,le),Just lbuild) ->  
      ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) (l,annot))))),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 Tag_empty,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 -> (E_aux (E_assign (lexp_builder e) (to_exp v)) (l,annot)) )) end))
		       end))
                    (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_assign lexp v) (l,annot)))))
  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)) Tag_empty, local_mem, init_env)
    | [ exp ] -> 
      if mode.eager_eval
      then interp_main mode t_level local_env local_mem exp
      else debug_out 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 (E_aux (E_block exps) (l,tannot)) t_level lm le)
                      (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_block(e::exps)) (l,tannot)))))
    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) =
   let (Env defs 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 in_env l_env id with
	    | Just (V_boxref n t) -> 
	      if is_top_level 
	      then ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem l_mem n value, l_env),Nothing)
	      else ((Value (in_mem l_mem n) Tag_empty, l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
	    | Just v -> 
	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
	      else ((Value v Tag_empty,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
	    | Nothing ->
	      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)) Tag_empty, update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
	      else ((Error l (String.stringAppend "Undefined id1 " (get_id id)),l_mem,l_env),Nothing)
             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 Tag_empty,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
	    | Nothing -> ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
	   end)
        | Tag_extern _ ->
	  let regf = Reg id annot in
	  let request = (Action (Write_reg regf Nothing 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 -> LEXP_aux (LEXP_id id) (l,annot)))
        | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (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 tag',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 -> 
	                       (LEXP_aux (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end)) (l,annot))))
         end)
      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot))))
      | e -> (e,Nothing) end
    | LEXP_cast typc id -> 
      match tag with
	| Tag_empty ->
	  match in_env l_env id with
	    | Just (V_boxref n t) -> 
	      if is_top_level 
	      then ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem l_mem n value, l_env),Nothing)
	      else ((Value (in_mem l_mem n) Tag_empty, l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
	    | Just v -> 
	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
	      else ((Value v Tag_empty,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_cast typc id) (l,annot)))
	    | Nothing -> 	  
	      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)) Tag_empty, update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
              end
              else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
          end 
        | Tag_extern _ ->
	  let regf = Reg id annot in
	  let request = (Action (Write_reg regf Nothing 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 -> LEXP_aux (LEXP_cast typc id) (l,annot)))
        | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than 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 tag',lm,le) ->
        (match i with 
        | V_lit (L_aux (L_num n) ln) -> 
          let next_builder le_builder = (fun e -> 
	                                  LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in
          (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
          | ((Value v tag3,lm,le),maybe_builder) ->
            (match v with 
            | V_vector inc m vs -> 
              let nth = access_vector v n in
              (match (nth,is_top_level,maybe_builder) with
	      | (V_register regform,true,_) ->
		((Action (Write_reg regform Nothing 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) ->
		((Action (Write_reg regform Nothing 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)) Tag_empty, update_mem lm n value, 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) Tag_empty,lm, l_env),Just (next_builder lexp_builder))
              | (v,false, Just lexp_builder) -> ((Value v Tag_empty,lm,le), Just (next_builder lexp_builder)) end)
	    | V_vector_sparse n m inc vs d ->
              let nth = access_vector v n in
              (match (nth,is_top_level,maybe_builder) with
		| (V_register regform,true,_) ->
		  ((Action (Write_reg regform Nothing 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) ->
		  ((Action (Write_reg regform Nothing 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)) Tag_empty, update_mem lm n value, 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) Tag_empty,lm, l_env),Just (next_builder lexp_builder))
		| (v,false, Just lexp_builder) -> ((Value v Tag_empty,lm,le), Just (next_builder lexp_builder)) end)
            | _ -> ((Error l "Vector access of non-vector",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)) value) s, lm,le), Nothing)
           | ((Write_reg regf Nothing value),false) -> 
	     ((Action (Write_reg regf (Just (n,n)) value) 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 -> (LEXP_aux (LEXP_vector lexp e) (l,annot))))
      | e -> (e,Nothing) end
    | LEXP_vector_range lexp exp1 exp2  ->
      match (interp_main mode t_level l_env l_mem exp1) with
      | (Value i1 tag_e, lm, le) ->
        (match i1 with
        | V_lit (L_aux (L_num n1) ln1) ->
          (match (interp_main mode t_level l_env l_mem exp2) with
          | (Value i2 tag_e2,lm,le) ->
            (match i2 with
            | V_lit (L_aux (L_num n2) ln2) ->
              let next_builder le_builder = 
		(fun e -> LEXP_aux (LEXP_vector_range (le_builder e) 
				                      (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
						      (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in
              (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
              | ((Value v tag_le,lm,le), Just lexp_builder) ->
                (match (v,is_top_level) with
                | (V_vector m inc vs,true) -> 
                  ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
                | (V_vector m inc vs,false) ->
                  ((Value (slice_vector v n1 n2) Tag_empty,lm,l_env), Just (next_builder lexp_builder))
                | _ -> ((Error l "Vector required",lm,le),Nothing) end)
              | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
                ((Action (Write_reg regf (Just (n1,n2)) value) 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 -> LEXP_aux (LEXP_vector_range lexp 
							                     (E_aux (E_lit (L_aux (L_num  n1) ln1)) (ln1,Nothing))
									     e) (l,annot)))
          | 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 -> LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot)))
      | 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) tag_le,lm,le),Just lexp_builder) ->
       match (in_env fexps id,is_top_level) with
       | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, update_mem lm n value, l_env),Nothing)
       | (Just (V_boxref n t),false) -> 
	 ((Value (in_mem lm n) Tag_empty,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
       | (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing)
       | (Just v,false) -> ((Value v Tag_empty,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
       | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
     | ((Action a s,lm,le), Just lexp_builder) ->  
       match a with
       | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
       | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
       | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
       | 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 value) s,lm,le), 
		  (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))))
	       | _ -> ((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 value) s,lm,le), 
		  (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))))
	       | _ -> ((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 Tag_empty,lm,le) ->
      (match match_pattern pat v with
      | (true,used_unknown,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, 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 Tag_empty,lm,le) ->
      (match match_pattern pat v with
      | (true,used_unknown,env) -> ((Value (V_lit (L_aux L_unit l)) Tag_empty, lm, 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 lets regs ctors subregs aliases) = t_level in 
  let stack = Hole_frame (Id_aux (Id "0") Unknown)
		          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
			  t_level l_env l_mem Top in
  match alspec with
    | AL_subreg reg subreg ->
      (match in_env regs reg with
	| Just (V_register (Reg _ (Just((T_id id),_,_,_)))) ->
	  (match in_env subregs (Id_aux (Id id) 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 " id), l_mem, l_env) end)
	| Just (V_register ((Reg _ (Just((T_abbrev (T_id id) _),_,_,_))) as rf)) ->
	  (match in_env subregs (Id_aux (Id id) Unknown) with
	    | Just indexes -> 
	      (match in_env indexes subreg with
		| Just ir -> (Action (Read_reg (SubReg subreg rf 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 " id), l_mem, l_env) end)
	| _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register " (get_id reg)),l_mem,l_env) end)
 | AL_bit reg 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)
 | AL_slice reg 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)
 | AL_concat reg1 reg2 -> (Error l "Unimplemented yet, alias spec concat", l_mem, l_env)
end

let rec to_global_letbinds (Defs defs) t_level =
  let  (Env defs' lets regs ctors subregs aliases) = t_level in
  match defs with
  | [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
  | def::defs ->
    match def with
    | DEF_val lbind ->
      match interp_letbind <|eager_eval=true|> t_level [] emem lbind with
      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs aliases)
      | ((Action a s,lm,le),_) -> 
	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
      | (e,_) -> (e,t_level) 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 (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs aliases)
      | _ -> to_global_letbinds (Defs defs) t_level end
    | _ -> to_global_letbinds (Defs defs) t_level
    end
  end

let to_top_env defs = 
  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
  let (o,t_level) = to_global_letbinds defs t_level in
  match o with
    | (Value _ _,_,_) -> (Nothing,t_level)
    | (o,_,_) -> (Just o,t_level)
  end

let interp mode defs exp =
  match (to_top_env defs) with
    | (Nothing,t_level) -> 
      match interp_main mode t_level [] 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 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 ((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 tag -> 
      match interp_main mode t_level ((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 tag -> 
      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