path: root/src/lem_interp/interp.lem

open import Pervasives
import Map
import Map_extra
import List_extra
open import String_extra

open import Interp_ast

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

val pure : effect
let pure = Effect_aux(Effect_set []) 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

(* type nat = num *)

(* 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
 | V_vector of integer * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
 | V_record of t * list (id * value)
 | V_ctor of id * t * value
 | 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_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')
  | (_, _) -> false
  end

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

(* Store for local memory of ref cells *)
type lmem = LMem of nat * map nat value
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 outcome =  (* these should be related to the Sail effect language, obviously...*)
  | Read_mem of read_kind * value (*the address*) * (value -> instruction_state)      (* the continuation parameterised just on a value or on a write? *)
  | Write_mem of write_kind * value (*the address*) * value (*the value*) * (bool (*ss wcond success*) -> instruction state)    
  | Barrier of barrier_kind * instruction_state
  | Read_reg of reg_name * (value -> instruction_state)
  | Write_reg of reg_name * value * instruction_state
  | Write_next_instruction_address of value * instruction_state  (* separate out NIA and _PC from the real Write_reg? *)
  | Internal of instruction_state   (* normally we'll want the system to eagerly do these, either within the interpreter or outside.  But not always: sometimes we'll want to single-step through them - or at the block-level or somesuch *)
  | Nondet_choice of list instruction_state    (* for (1) explicit nondet choices of single bits in the ISA, (2) interpreting conditionals that hit a "don't know" value in register/memory footprint calculation, and perhaps (3) interpreting intra-instruction parallelism, eg for load-multiple *)
  | Done
  | Error of ...   (* for internal errors that should all be prevented by Sail typechecking and careful writing of the ISA semantics *)
  | Undefined_instruction of ...   (* for dynamically detected occurrences of UNPREDICTABLE *)
*)

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
 | Nondet of list (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
 | Frame of id * exp tannot * env * lmem * stack

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 

(* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *)
val interp : defs tannot -> exp tannot -> 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 has_memory_effect : list base_effect -> bool
let rec has_memory_effect efcts =
  match efcts with
  | [] -> false
  | (BE_aux e _)::efcts ->
    match e with
    | BE_wreg -> true
    | BE_wmem -> true
    | _ -> has_memory_effect efcts
    end 
  end

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,Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown) 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

val litV_to_vec : lit -> value
let litV_to_vec (L_aux lit l) =
  match lit with
  | L_hex s ->
    let hexes = String.toCharList s in
    (* XXX unimplemented *)
    V_vector 0 true []
  | L_bin s -> 
    let bits = String.toCharList s in
    let exploded_bits = bits in (*List.map (fun c -> String.toString [c]) bits in*)
    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) exploded_bits in
    (* XXX assume binary constants are written in big-endian,
     * we might need syntax to change this assumption. *)
    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)
  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_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)
  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) ->
    List.foldr (fun vbox mem -> match vbox with
                                    | V_boxref n t -> update_mem mem n v end)
      mem vs
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)
  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 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)))
  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
  | Frame id e env mem stack -> Frame id (e_builder e) env mem stack
  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 "enum" (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
	 (T_app "enum" (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 "enum" (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 "enum" (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_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
  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)))
	else 
          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
      | 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 -> E_app id [to_exp vals]
      | V_register (Reg id tan) -> E_id id
     end)
    (Unknown,(val_annot (val_typ v)))

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

val match_pattern : pat tannot -> value -> 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', [])
          else (false,[])
        else (false,[])
      | V_vector n' inc' bits' -> 
        if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l=r) && rest) true bits bits',[])
        else (false,[])
      | _ -> (false,[]) end
    else
    match value with
    | V_lit(litv) -> (lit = litv, [])
    | _ -> (false,[])
    end
 | P_wild -> (true,[])
 | P_as pat id ->  let (matched_p,bounds) = match_pattern pat value in
		     if matched_p then
		       (matched_p,(id,value)::bounds)
		     else (false,[])
 | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information *)
 | P_id id -> (true, [(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,bounds) ->
            if matched_p then
              let (matched_p,new_bounds) = match_pattern pat value in
              (matched_p, (new_bounds ++ bounds))
            else (false,[])) (true,[]) pats vals
     else (false,[])
   | _ -> (false,[]) end
 | P_record fpats _ ->
   match value with
   | V_record t fvals ->
     List.foldr
       (fun (FP_aux (FP_Fpat id pat) _) (matched_p,bounds) ->
         if matched_p then
           let (matched_p,new_bounds) = match in_env fvals id with
                                       | Nothing -> (false,[])
                                       | Just v -> match_pattern pat v end in
           (matched_p, (new_bounds ++ bounds))
         else (false,[])) (true,[]) fpats
   | _ -> (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,bounds) -> 
	 if matched_p then
	   let (matched_p,new_bounds) = match_pattern pat value in
	   (matched_p, (new_bounds ++ bounds)) 
	 else (false,[]))
       (true,[]) (if inc then pats else List.reverse pats) vals
     else (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,bounds) -> if matched_p && i < v_len then
	   let (matched_p,new_bounds) = match_pattern pat (list_nth vals (if inc then i+n else i-n)) in
	   (matched_p,new_bounds++bounds)
         else (false,[]))
       (true,[]) ipats
   | _ -> (false, [])
   end 
 | P_vector_concat pats ->
   match value with
   | V_vector n inc vals ->
     let (matched_p,bounds,remaining_vals) =
       List.foldl 
         (fun (matched_p,bounds,r_vals) (P_aux pat (l,Just(t,_,_,_))) ->
	   let (matched_p,bounds',matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
	   (matched_p,bounds' ++ bounds,r_vals)) (true,[],vals) pats in
     if matched_p && ([] = remaining_vals) then (matched_p,bounds) else (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,bounds) -> if matched_p then
	   let (matched_p,new_bounds) = match_pattern pat v in
	   (matched_p,bounds++new_bounds)
	 else (false,[]))
       (true,[]) pats vals
     else (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,bounds) -> if matched_p then
	   let (matched_p,new_bounds) = match_pattern pat v in
	   (matched_p,bounds++new_bounds)
	 else (false,[]))
       (true,[]) pats vals
     else (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,bounds,matcheds,r_vals) = vec_concat_match wilds r_vals in
	    if matched_p 
	    then (matched_p, (id,(V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds))::bounds,matcheds,r_vals)
	    else (false,[],[],[])
	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
	    (false,[],[],[]) (*TODO see if can have some constraint bounds here*)
	  | _ -> (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,[],[],[]) (*TODO see if can have some constraint bounds here*)
	  | _ -> (false,[],[],[]) end)
      | P_as (P_aux pat (l',Just(t,_,_,_))) id -> 
	let (matched_p, bounds,matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
	if matched_p 
	then (matched_p, ((id,V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds)::bounds),matcheds,r_vals)
	else (false,[],[],[])	  
      | P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals inc l t
      | _ -> (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,[],[],r_vals)
    | pat::pats -> match r_vals with
      | [] -> (false,[],[],[])
      | r::r_vals -> 
	let (matched_p,new_bounds) = match_pattern pat r in
        if matched_p then 
          let (matched_p,bounds,matcheds,r_vals) = vec_concat_match pats r_vals in
          (matched_p, new_bounds++bounds,matcheds++[r],r_vals)
        else (false,[],[],[]) end
    end


val find_funcl : list (funcl tannot) -> value -> maybe (env * (exp tannot))
let rec find_funcl funcls value =
  match funcls with
  | [] -> Nothing
  | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
    let (is_matching,env) = match_pattern pat value in
    if is_matching then Just (env,exp) else find_funcl funcls value
  end

val find_case : list (pexp tannot) -> value -> maybe (env * (exp tannot))
let rec find_case pexps value =
  match pexps with
  | [] -> Nothing
  | (Pat_aux (Pat_exp p e) _)::pexps -> 
    let (is_matching,env) = match_pattern p value in
    if is_matching then Just(env,e) else find_case pexps value
  end

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

val interp_main : top_level -> env -> lmem -> (exp tannot) -> (outcome * lmem * env)
val exp_list : top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * env)
val interp_lbind : top_level -> env -> lmem -> (letbind tannot) -> ((outcome * lmem * env) * (maybe ((exp tannot) -> (letbind tannot))))

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)  

(*Interpret a list of expressions, tracking local state but evaluating in the same scope (i.e. not tracking env) *)
let rec exp_list 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 t_level l_env l_mem e)
                    (fun value lm le -> exp_list 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 t_level l_env l_mem (E_aux exp (l,annot)) =
  let (Env defs lets regs ctors subregs) = 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 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) 
	                     (Frame (id_of_string "0")
		                (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) 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) 
                        | _ -> (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 -> 
              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_none " name), l_mem,l_env)
          end 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)
	          (Frame (Id_aux (Id "0") Unknown)
		         (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),
           l_mem,l_env)
        | _ -> (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 t_level l_env l_mem cond)
	              (fun value lm le -> 
			match value with
                          | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn
                          | _ -> interp_main t_level l_env lm els 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 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 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 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
                                                      interp_main t_level le lm 
                                                        (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))
                                                  | _ -> (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 t_level l_env l_mem exp)
                      (fun v lm le ->
                        match find_case pats v with
                        | Nothing -> (Error l "No matching patterns in case",lm,le)
                        | Just (env,exp) -> interp_main t_level (env++l_env) lm exp
		        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 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 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 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)
                        | _ -> (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 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 t_level l_env l_mem hd)
                      (fun hdv lm le -> resolve_outcome
                                        (interp_main 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)
                                                   | _ -> (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 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
                        | _ -> (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 ->
      (*Need to update to read one position of a register*)
      resolve_outcome (interp_main 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 t_level l_env lm vec)
                                          (fun vvec lm le ->
                                            match vvec with
                                            | V_vector base inc vals -> (Value (access_vector vvec n) Tag_empty,lm,le)
                                            | _ -> (Error l "Vector access of non-vector",lm,le)end)
                                          (fun a -> 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)))))
                        | _ -> (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 ->
      (*Need to update to read a slice of a register*)
      resolve_outcome (interp_main 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 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 t_level l_env lm vec)
                                                              (fun vvec lm le ->
                                                                match vvec with
                                                                | V_vector base inc vals -> (Value (slice_vector vvec n1 n2) Tag_empty,lm,le)
                                                                | _ -> (Error l "Vector slice of non-vector",lm,le)end)
                                                              (fun a -> 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)))))
                                            | _ -> (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)))))
                        | _ -> (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 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 t_level le lm exp)
                                          (fun vup lm le ->
                                            resolve_outcome (interp_main t_level le lm vec)
                                                            (fun vec lm le ->
                                                              match vec with
                                                              | V_vector base inc vals -> (Value (fupdate_vec vec n1 vup) 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))))
                        | _ -> (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 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 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 t_level l_env lm exp)
                                  (fun v_rep lm le ->
                                    (resolve_outcome 
                                       (interp_main t_level l_env lm vec)
                                       (fun vvec lm le ->
                                         match vvec with
                                         | V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2) 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))))
                              | _ -> (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))))
                        | _ -> (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_tuple(exps) -> 
      exp_list t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
    | E_vector(exps) ->
      exp_list 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) ->
      let (indexes,exps) = List.unzip iexps in
      let is_inc = match typ with
        | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
        | _ -> false end in
      exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot))) 
                       (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
    | E_block(exps) -> interp_block t_level l_env l_env l_mem exps
    | E_app f args ->
      (match (exp_list 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_empty -> 
	  (match find_function defs f with
	  | Just(funcls) -> 
            (match find_funcl funcls v with
	    | Nothing -> 
              (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
	    | Just(env,exp) -> 
              resolve_outcome (interp_main t_level env l_mem exp)
	                      (fun ret lm le -> (Value ret Tag_empty, lm,l_env))
                              (fun a -> update_stack a 
				(fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) 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
	    | Nothing -> 
              (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
	    | Just(env,exp) -> 
              resolve_outcome (interp_main t_level env l_mem exp)
	                      (fun ret lm le -> (Value ret Tag_empty, lm,l_env))
                              (fun a -> update_stack a 
				(fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) 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_memory_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) 
          then
            (Action (Read_mem (id_of_string name_ext) v Nothing) 
	            (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top), lm, le)
          else
            (Action (Call_extern name_ext v) 
	            (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) 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 t_level l_env l_mem lft)
                      (fun lv lm le -> 
                         resolve_outcome (interp_main t_level l_env lm r)
                                         (fun rv lm le -> 
                                           match tag with
                                           | 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 
				               | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
				               | Just(env,exp) ->
				                 resolve_outcome (interp_main t_level env emem exp)
				                   (fun ret lm le -> (Value ret Tag_empty,l_mem,l_env))
                                                   (fun a -> update_stack a 
						     (fun stack -> (Frame (Id_aux (Id "0") l)
								          (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) 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 
				               | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
				               | Just(env,exp) ->
				                 resolve_outcome (interp_main t_level env emem exp)
				                   (fun ret lm le -> (Value ret Tag_empty,l_mem,l_env))
                                                   (fun a -> update_stack a 
						     (fun stack -> (Frame (Id_aux (Id "0") l)
								          (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) 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])) 
						     (Frame (Id_aux (Id "0") l) 
							    (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) 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_let (lbind : letbind tannot) exp -> 
    match (interp_letbind t_level l_env l_mem lbind) with
    | ((Value v tag_l,lm,le),_) -> interp_main t_level le lm exp                                             
    | (((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 t_level l_env l_mem exp)
                    (fun v lm le -> 
                      (match create_write_message_or_update 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

 and interp_block t_level init_env local_env local_mem exps =
   match exps with
    | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)) Tag_empty, local_mem, init_env)
    | [ exp ] -> interp_main t_level local_env local_mem exp
    | exp:: exps ->
      resolve_outcome (interp_main t_level local_env local_mem exp)
                      (fun _ lm le -> interp_block t_level init_env le lm exps)
                      (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_block(e::exps)) (Unknown,Nothing)))))
    end

and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
   let (Env defs lets regs ctors subregs) = 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 -> 
	      (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 ->
		  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)
          end 
        | Tag_extern _ ->
	  let regf = Reg id annot in
	  let request = (Action (Write_reg regf Nothing value) 
			        (Frame (Id_aux (Id "0") l) 
				       (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) 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 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) 
                                (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) 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) 
			        (Frame (Id_aux (Id "0") l) 
				       (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) 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 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 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)
		         (Frame (Id_aux (Id "0") l)
			        (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env),Nothing)
	      | (V_register regform,false,Just lexp_builder) ->
		((Action (Write_reg regform Nothing value)
		         (Frame (Id_aux (Id "0") l)
			        (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) 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 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 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 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 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 t_level l_env l_mem (LB_aux lbind (l,annot)) =
  match lbind with
  | LB_val_explicit t pat exp ->
    match (interp_main t_level l_env l_mem exp) with
    | (Value v Tag_empty,lm,le) ->
      (match match_pattern pat v with
      | (true,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 t_level l_env l_mem exp) with
    | (Value v Tag_empty,lm,le) ->
      (match match_pattern pat v with
      | (true,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	

(*Beef up to pick up enums as well*)
let rec to_global_letbinds (Defs defs) t_level =
  let  (Env defs' lets regs ctors subregs) = 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 t_level [] emem lbind with
      | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs)
      | ((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
    | _ -> to_global_letbinds (Defs defs) t_level
    end
  end


let interp defs exp =
  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) in 
  let (o,t_level) = to_global_letbinds defs t_level in
  match o with
  | (Value _ _,_,_) -> 
     match interp_main t_level [] emem exp with
     | (o,_,_) -> o
     end 
  | (o,_,_) -> o 
  end

let rec resume_main t_level stack value =
  match stack with
  | Top -> Error Unknown "Top hit without place to put value"
  | Frame id exp env mem Top -> 
    match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end 
  | Frame id exp env mem stack ->
    match resume_main t_level stack value with
    | Value v tag -> 
      match interp_main t_level ((id,v)::env) mem exp with | (o,_,_) -> o end 
    | Action action stack -> Action action (Frame id exp env mem stack)
    | Error l s -> Error l s
    end  
  end

let resume defs stack value =
  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) in 
  let (o,t_level) = to_global_letbinds defs t_level in
  match o with
  | (Value _ _,_,_) -> 
     resume_main t_level stack value
  | (o,_,_) -> o 
  end