path: root/src/lem_interp/interp.lem

open Pervasives
open Pmap
open Interp_ast

type nat = num

type value =
 | V_boxref of nat 
 | V_lit of lit
 | V_tuple of list value
 | V_list of list value
 | V_vector of nat * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
 | V_record of list (id * value)
 | V_ctor of id * value

type mem = Mem of nat * map nat value
type env = list (id * value)

let emem = Mem 1 Pmap.empty

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

(* These may need to be refined or expanded based on memory requirement *)
type action = 
 | Read_reg of reg_form * option (nat * nat)
 | Write_reg of reg_form * option (nat* nat) * value
 | Read_mem of id * value * option (nat * nat)
 | Write_mem of id * value * option (nat * nat) * value

(* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *)
type stack = 
 | Top
 | Frame of id * exp * env * mem * stack

(* Either a case must be added for parallel options or action must be tied to a list *)
type outcome =
 | Value of value
 | Action of action * stack
 | Error of string (* When we store location information, it should be added here *)

(* 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 -> exp -> outcome

val to_registers : defs -> list (id * reg_form)
let rec to_registers (Defs defs) =
  match defs with
  | [ ] -> [ ]
  | def::defs -> 
    match def with 
    | DEF_val letb -> to_registers (Defs defs) (* Todo, maybe look through let bindings *)
    | DEF_spec valsp -> 
      match valsp with
      | VS_val_spec (TypSchm_ts tq ((Typ_app (Id "reg") _) as t)) id -> (id, Reg t):: (to_registers (Defs defs))
      | _ -> to_registers (Defs defs)
      end
    | DEF_reg_dec typ id -> (id, Reg typ) :: (to_registers (Defs defs))
    | DEF_type tdef ->
      match tdef with 
      | TD_register id n1 n2 ranges -> 
	(id,Reg (Typ_app (Id "vector")[]))::
	((to_reg_ranges id (Reg (Typ_app (Id "vector")[])) ranges) @ (to_registers (Defs defs)))
      | _ -> to_registers (Defs defs)
      end
    | _ -> to_registers (Defs defs)
    end 
  end
and to_reg_ranges base_id base_reg ranges =
  match ranges with
  | [ ] -> [ ]
  | (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges)
  end

val has_memory_effect : list efct -> bool
let rec has_memory_effect efcts =
  match efcts with
  | [] -> false
  | e::efcts ->
    match e with
    | Effect_wreg -> true
    | Effect_wmem -> true
    | _ -> has_memory_effect efcts
    end 
  end

val to_memory_ops : defs -> list (id * typ)
let rec to_memory_ops (Defs defs) =
  match defs with
  | [] -> []
  | def ::defs ->
    match def with
    | DEF_spec valsp ->
      match valsp with
      | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effects_set eff)) as t)) id ->
        if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
      | _ -> to_memory_ops (Defs defs) end
    | _ -> to_memory_ops (Defs defs) end
  end

val in_env : env -> id -> option value
let rec in_env env id =
 match env with
 | [] -> None
 | (eid,value)::env -> if eid = id then Some value else in_env env id
 end 

val in_mem : mem -> nat -> value
let in_mem (Mem _ m) n = 
  Pmap.find n m
  (* if (Pmap.mem n m) then Some (Pmap.find n m) else None *)

val update_mem : mem -> nat -> value -> mem
let update_mem (Mem c m) loc value =
  let m' = Pmap.remove loc m in
  let m' = Pmap.add loc value m' in
  Mem c m'

val access_vector : value -> nat -> 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. nat -> nat -> nat -> list 'a -> list 'a
let rec from_n_to_n from to_ acc ls =
  match ls with
  | [] -> []
  | l::ls -> 
    if (acc <= from)
    then if (from = to_)
      then [ l ]
      else l::(from_n_to_n (from + 1) to_ acc ls)
    else from_n_to_n from to_ (acc + 1) ls
  end

val slice_vector : value -> nat -> nat -> value
let slice_vector v n1 n2 =
  match v with
  | V_vector m inc vs ->
    if inc 
    then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) 0 vs)
    else V_vector n1 inc (from_n_to_n (m - n1) (m - n2) 0 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
    | Some v -> (id,v)::(update_field_list bs updates)
    | None -> (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 bs,V_record us) -> V_record (update_field_list bs us) end

val update_vector_slice : value -> value -> mem -> mem
let rec update_vector_slice vector value mem = 
  match (vector,value) with
  | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
    List.fold_right2 (fun vbox v mem -> match vbox with
                                       | V_boxref n -> update_mem mem n v end)
      vs vals mem
  | ((V_vector m inc vs),v) ->
    List.fold_right (fun vbox mem -> match vbox with
                                    | V_boxref n -> update_mem mem n v end)
      vs mem
end

val in_reg : list (id * reg_form) -> id -> option reg_form
let rec in_reg regs id =
  match regs with
  | [] -> None
  | (eid,regf)::regs -> if eid = id then Some regf else in_reg regs 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 rec to_exp v =
    match v with
    | V_boxref n -> E_id (Id (string_of_num n))
    | 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.rev (snd (List.fold_left (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
      else 
        E_vector_indexed (snd (List.fold_right (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) vals (n-(List.length vals),[])))
    | V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
    end

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

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

let rec find_function (Defs defs) id =
  match defs with 
  | [] -> None
  | def::defs -> 
    match def with
    | DEF_fundef f -> match get_funcls id f with
      | [] -> find_function (Defs defs) id
      | funcs -> Some funcs end
    | _ -> find_function (Defs defs) id
    end end

let rec find_memory mems id =
  match mems with
  | [] -> None
  | (id',t)::mems -> if id'=id then Some t else find_memory mems id
  end

val match_pattern : pat -> value -> bool * list (id * value)
let rec match_pattern p value =
  match p with 
  | P_lit(lit) -> 
    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, list pat) -> (* union constructor pattern *) need defs for this case, to check that id is a constructor *)
(* | P_record of list fpat * bool (* struct pattern *) todo *)
 | P_vector pats ->
   match value with
   | V_vector n inc vals ->
     if ((List.length vals) = (List.length pats))
     then List.fold_right2
       (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,[]))
       (if inc then pats else List.rev pats) vals (true,[])
     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.fold_right
       (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,[]))
       ipats (true,[])
   | _ -> (false, [])
   end
(* | P_vector_concat of list pat (* concatenated vector pattern *) TODO *)
 | P_tup(pats) ->
   match value with 
   | V_tuple(vals) ->
     if ((List.length pats)= (List.length vals))
     then List.fold_right2 
       (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,[]))
       pats vals (true,[])
     else (false,[])
   | _ -> (false,[])
     end 
 | P_list(pats) ->
   match value with 
   | V_list(vals) ->
     if ((List.length pats)= (List.length vals))
     then List.fold_right2 
       (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,[]))
       pats vals (true,[])
     else (false,[])
   | _ -> (false,[]) end
 end 

val find_funcl : list funcl -> value -> option (env * exp)
let rec find_funcl funcls value =
  match funcls with
  | [] -> None
  | (FCL_Funcl id pat exp)::funcls ->
    let (is_matching,env) = match_pattern pat value in
    if is_matching then Some (env,exp) else find_funcl funcls value
  end

(*top_level is a three tuple of (all definitions, declared registers, memory functions (typ expected to be num -> num -> a)) *)
type top_level = defs * list (id*reg_form) * list (id * typ)

val interp_main : top_level -> env -> mem -> exp -> (outcome * mem * env)
val exp_list : top_level -> (list exp -> exp) -> (list value -> value) -> env -> mem -> list value -> list exp -> (outcome * mem * env)
val interp_lbind : top_level -> env -> mem -> letbind -> ((outcome * mem * env) * (option (exp -> letbind)))

let resolve_outcome to_match value_thunk action_thunk =
  match to_match with
  | (Value v,lm,le) -> value_thunk v lm le
  | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
  | (Error s,lm,le) -> (Error 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), 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 exp =
    match exp with
    | E_lit lit -> (Value (V_lit lit), l_mem,l_env)
    | E_cast typ exp -> interp_main t_level l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *)
    | E_id id -> match in_env l_env id with
                 | Some(value) -> match value with
		                  | V_boxref n ->(Value (in_mem l_mem n),l_mem,l_env)
		                  | _ -> (Value value,l_mem,l_env) end
		 | None -> match t_level with
		           | (defs,regs,mems) ->
			     match in_reg regs id with
			     | Some(regf) -> 
			       (Action (Read_reg regf None) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top), l_mem, l_env) 
			     | None -> 
			       (Error "Unimplemented global memory read or unbound identifier",l_mem,l_env)
			     end 
                            end
		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_true) -> interp_main t_level l_env lm thn
                        | V_lit(L_false) -> interp_main t_level l_env lm els
                        | _ -> (Error "Type error, not provided boolean for if",lm,l_env) end)
                      (fun a -> update_stack a (add_to_top_frame (fun c -> (E_if c thn els))))
    | E_record(FES_Fexps fexps _) -> 
      let (fields,exps) = List.split (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
      exp_list t_level (fun es -> (E_record(FES_Fexps (List.map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
	               (fun vs -> (V_record (List.combine fields vs))) l_env l_mem [] exps
    | E_record_update exp (FES_Fexps fexps _) ->
      resolve_outcome (interp_main t_level l_env l_mem exp)
                      (fun rv lm le -> 
                        match rv with
                        | V_record fvs ->
                          let (fields,exps) = List.split (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
                          resolve_outcome (exp_list t_level (fun es -> (E_record_update (to_exp rv) (FES_Fexps (List.map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
                                                            (fun vs -> (V_record (List.combine fields vs))) l_env l_mem [] exps)
                                          (fun vs lm le ->
                                            (Value (fupdate_record rv vs), lm, le))
                                          (fun a -> a)
                        | _ -> (Error "record upate requires record",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_record_update e (FES_Fexps fexps false))))
    | E_list(exps) ->
      exp_list t_level E_list 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)),lm,le)
                                                   | _ -> (Error ":: of non-list value",lm,le) end)
                                        (fun a -> update_stack a (add_to_top_frame (fun t -> E_cons (to_exp hdv) t))))
                      (fun a -> update_stack a (add_to_top_frame (fun h -> E_cons h tl)))
    | E_field exp id -> 
      resolve_outcome (interp_main t_level l_env l_mem exp)
                      (fun value lm le -> 
                        match value with 
                        | V_record fexps -> match in_env fexps id with
                                            | Some v -> (Value v,lm,l_env)
                                            | None -> (Error "Field not found in record",lm,le) end
                        | _ -> (Error "Field access requires a record",lm,le)
                        end )
                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_field e id)))
    | E_vector_access vec i ->
      resolve_outcome (interp_main t_level l_env l_mem i)
                      (fun iv lm le -> 
                        match iv with
                        | V_lit (L_num n) -> 
                          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),lm,le)
                                            | _ -> (Error "Vector access of non-vector",lm,le)end)
                                          (fun a -> update_stack a (add_to_top_frame (fun v -> (E_vector_access v (E_lit (L_num n))))))
                        | _ -> (Error "Vector access not given a number for index",lm,l_env) end)
                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_access vec i)))
    | E_vector_subrange vec i1 i2 ->
      resolve_outcome (interp_main t_level l_env l_mem i1)
                      (fun i1v lm le ->
                        match i1v with
                        | V_lit (L_num n1) ->
                          resolve_outcome (interp_main t_level l_env lm i2)
                                          (fun i2v lm le ->
                                            match i2v with
                                            | V_lit (L_num n2) ->
                                              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),lm,le)
                                                                | _ -> (Error "Vector slice of non-vector",lm,le)end)
                                                              (fun a -> update_stack a (add_to_top_frame (fun v -> (E_vector_subrange v (E_lit (L_num n1)) (E_lit (L_num n2))))))
                                            | _ -> (Error "vector slice given non number for last index",lm,le) end)
                                          (fun a -> update_stack a (add_to_top_frame (fun i2 -> (E_vector_subrange vec (E_lit (L_num n1)) i2))))
                        | _ -> (Error "Vector slice given non-number for first index",lm,le) end)
                       (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_vector_subrange vec i1 i2))))
    | E_tuple(exps) -> 
      exp_list t_level E_tuple V_tuple l_env l_mem [] exps
    | E_vector(exps) ->
      exp_list t_level E_vector (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
    | E_vector_indexed(iexps) ->
      let (indexes,exps) = List.split iexps in
      exp_list t_level (fun es -> (E_vector_indexed (List.map2 (fun i e -> (i,e)) indexes es))) 
                       (fun vals -> V_vector (List.hd indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps
    | E_block(exps) -> interp_block t_level l_env l_env l_mem exps
    | E_app f args ->
      match (f,t_level) with
      | (E_id(id),(defs,regs,mems)) -> 
	(match find_function defs id with
	| Some(funcls) -> 
          resolve_outcome (interp_main t_level l_env l_mem (List.hd args))
                          (fun argv lm le -> 
                            (match find_funcl funcls argv with
	                    | None -> (Error "No matching pattern for function",lm,l_env) (*TODO add function name*)
	                    | Some(env,exp) -> 
                              resolve_outcome (interp_main t_level env emem exp)
	                                      (fun ret lm le -> (Value ret, l_mem,l_env))
                                              (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
                             end))
                          (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
	| None -> 
          (match find_memory mems id with
          | Some(typ) -> 
            resolve_outcome (interp_main t_level l_env l_mem (List.hd args))
                            (fun argv lm le -> (Action (Read_mem id argv None) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le))
                            (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a]))))
          | None -> (Error "Unknown function call",l_mem,l_env) end)                              
 (*also need to look for data constructors*)
	 end)
      | _ -> (Error "Application with expression other than identifier",l_mem,l_env)
      end 
    | E_app_infix l op r -> 
      resolve_outcome (interp_main t_level l_env l_mem l)
                      (fun lv lm le -> 
                         resolve_outcome (interp_main t_level l_env lm r)
                                         (fun rv lm le -> 
			                   (match t_level with
			                   | (defs,regs,mems) ->
				             (match find_function defs op with
				             | None -> (Error "No matching pattern for function",lm,l_env)
				             | Some (funcls) ->
				               (match find_funcl funcls (V_tuple [lv;rv]) with 
				               | None -> (Error "No matching pattern for function",lm,l_env)
				               | Some(env,exp) ->
				                 resolve_outcome (interp_main t_level env emem exp)
				                 (fun ret lm le -> (Value ret,l_mem,l_env))
                                                 (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
				                end)
				              end)
			                    end))
                                         (fun a -> update_stack a (add_to_top_frame (fun r -> (E_app_infix (to_exp lv) op r)))))
                       (fun a -> update_stack a (add_to_top_frame (fun l -> (E_app_infix l op r))))
  | E_let lbind exp -> 
    match (interp_letbind t_level l_env l_mem lbind) with
    | ((Value v,lm,le),_) -> interp_main t_level le lm exp
    | (((Action a s as o),lm,le),Some lbuild) ->  ((update_stack o (add_to_top_frame (fun e -> (E_let (lbuild e) exp)))),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,None) -> outcome
                      | (outcome,Some lexp_builder) ->
                        resolve_outcome outcome
                                        (fun v lm le -> (Value v,lm,le))
                                        (fun a -> update_stack a (add_to_top_frame (fun e -> (E_assign (lexp_builder e) (to_exp v))))) end))
                    (fun a -> update_stack a (add_to_top_frame (fun v -> (E_assign lexp v))))
  end

 and interp_block t_level init_env local_env local_mem exps =
   match exps with
    | [ ] -> (Value (V_lit(L_unit)), local_mem, init_env)
    | 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_block(e::exps))))
    end

and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
   let (defs,regs,mems) = t_level in
   match lexp with
    | LEXP_id id -> 
      match in_env l_env id with
      | Some (V_boxref n) -> 
	if is_top_level 
	then ((Value (V_lit L_unit), update_mem l_mem n value, l_env),None)
	else ((Value (in_mem l_mem n), l_mem, l_env),Some (fun e -> LEXP_id id))
      | Some v -> if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),None) else ((Value v,l_mem,l_env),Some (fun e -> LEXP_id id))
      | None -> 
	match in_reg regs id with
	| Some regf -> let request = (Action (Write_reg regf None value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env) in
                       if is_top_level then (request,None) else (request,Some (fun e -> LEXP_id id))
	| None -> 
	  if is_top_level 
          then begin
	    let (Mem c m) = l_mem in
	    let l_mem = (Mem (c+1) m) in
	    ((Value (V_lit L_unit), update_mem l_mem c value, (id,(V_boxref c))::l_env),None)
          end
          else ((Error "Undefined id",l_mem,l_env),None)
        end
      end 
    | LEXP_memory id exp -> 
      match (interp_main t_level l_env l_mem exp) with
      | (Value t,lm,le) ->
        let request = (Action (Write_mem id t None value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
        if is_top_level then (request,None) else (request,Some (fun e -> (LEXP_memory id (to_exp t))))
      | (Action a s,lm, le) -> ((Action a s,lm,le), Some (fun e -> (LEXP_memory id e)))
      | e -> (e,None) end
    | LEXP_vector lexp exp -> 
      match (interp_main t_level l_env l_mem exp) with
      | (Value i,lm,le) ->
        (match i with 
        | V_lit (L_num n) -> 
          (match (create_write_message_or_update t_level value l_env lm false lexp) with
          | ((Value v,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_boxref n,true,_) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),None)
              | (v,true,_) -> ((Error "Vector does not contain reg values",lm,l_env),None)
              | ((V_boxref n),false, Some lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Some (fun e -> LEXP_vector (lexp_builder e) (E_lit (L_num n))))
              | (v,false, Some lexp_builder) -> ((Value v,lm,le), Some (fun e -> LEXP_vector (lexp_builder e) (E_lit (L_num n)))) end)
            | _ -> ((Error "Vector access of non-vector",lm,l_env),None) end)
         | ((Action a s,lm,le),Some lexp_builder) ->
           (match (a,is_top_level) with
           | ((Write_reg regf None value),true) -> ((Action (Write_reg regf (Some (n,n)) value) s, lm,le), None)
           | ((Write_reg regf None value),false) -> ((Action (Write_reg regf (Some (n,n)) value) s,lm,le), Some  (fun e -> (LEXP_vector (lexp_builder e) (E_lit (L_num n)))))
           | ((Read_reg regf r),_) -> ((Action a s,lm,le), Some (fun e -> (LEXP_vector (lexp_builder e) (E_lit (L_num n))))) end)
         | e -> e end)
        | _ -> ((Error "Vector access must be a number",lm,le),None) end)
      | (Action a s,lm,le) -> ((Action a s,lm,le), Some (fun e -> (LEXP_vector lexp e)))
      | e -> (e,None) end
    | LEXP_vector_range lexp exp1 exp2  ->
      match (interp_main t_level l_env l_mem exp1) with
      | (Value i1, lm, le) ->
        (match i1 with
        | V_lit (L_num n1) ->
          (match (interp_main t_level l_env l_mem exp2) with
          | (Value i2,lm,le) ->
            (match i2 with
            | V_lit (L_num n2) ->
              (match (create_write_message_or_update t_level value l_env lm false lexp) with
              | ((Value v,lm,le), Some lexp_builder) ->
                (match (v,is_top_level) with
                | (V_vector m inc vs,true) -> 
                  ((Value (V_lit L_unit), update_vector_slice (slice_vector v n1 n2) value lm, l_env), None)
                | (V_vector m inc vs,false) ->
                  ((Value (slice_vector v n1 n2),lm,l_env), Some (fun e -> LEXP_vector_range (lexp_builder e) (E_lit (L_num n1)) (E_lit (L_num n2))))
                | _ -> ((Error "Vector required",lm,le),None) end)
              | ((Action (Write_reg regf None value) s, lm,le), Some lexp_builder) ->
                ((Action (Write_reg regf (Some (n1,n2)) value) s,lm,le), Some (fun e -> LEXP_vector_range (lexp_builder e) (E_lit (L_num n1)) (E_lit (L_num n2))))
              | ((Action a s,lm,le), Some lexp_builder) ->
                ((Action a s,lm,le), Some (fun e -> (LEXP_vector_range (lexp_builder e) (E_lit (L_num n1)) (E_lit (L_num n2)))))
              | e -> e end)
            | _ -> ((Error "Vector slice requires a number", lm, le),None) end)
          | (Action a s,lm,le) ->
            ((Action a s,lm, le), Some (fun e -> LEXP_vector_range lexp (E_lit (L_num  n1)) e))
          | e -> (e,None) end)
        | _ -> ((Error "Vector slice requires a number", lm, le),None) end)
      | (Action a s,lm,le) ->
        ((Action a s, lm,le), Some (fun e -> LEXP_vector_range lexp e exp2))
      | e -> (e,None) end
     end	

and interp_letbind t_level l_env l_mem lbind =
  match lbind with
  | LB_val_explicit t pat exp ->
    match (interp_main t_level l_env l_mem exp) with
    | (Value v,lm,le) ->
      (match match_pattern pat v with
      | (true,env) -> ((Value (V_lit L_unit), lm, env@l_env),None)
      | _ -> ((Error "Pattern in letbind did not match value",lm,le),None) end)
    | (Action a s,lm,le) -> ((Action a s,lm,le),(Some (fun e -> LB_val_explicit t pat e)))
    | e -> (e,None) end
  | LB_val_implicit pat exp ->
    match (interp_main t_level l_env l_mem exp) with
    | (Value v,lm,le) ->
      (match match_pattern pat v with
      | (true,env) -> ((Value (V_lit L_unit), lm, env@l_env),None)
      | _ -> ((Error "Pattern in letbind did not match value",lm,le),None) end)
    | (Action a s,lm,le) -> ((Action a s,lm,le),(Some (fun e -> LB_val_implicit pat e)))
    | e -> (e,None) end
end	


let interp defs exp =
  let t_level = (defs, to_registers defs,to_memory_ops defs) in 
  match interp_main t_level [] emem exp with
  | (o,_,_) -> o
  end

let rec resume_main t_level stack value =
  match stack with
  | Top -> Error "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 -> 
      match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end 
    | Action action stack -> Action action (Frame id exp env mem stack)
    | Error s -> Error s
    end  
  end

let resume defs stack value =
  let t_level = (defs, to_registers defs,to_memory_ops defs) in
  resume_main t_level stack value