path: root/src/lem_interp/interp.lem

open import Pervasives
import Map
import Map_extra
import Maybe
import List_extra
import String

open import Interp_ast

(* 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 s -> s | DeIid s -> s end

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 Map.empty

type reg_form =
 | Reg of id * 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 * maybe (nat * nat)
 | Write_reg of reg_form * maybe (nat* nat) * value
 | Read_mem of id * value * maybe (nat * nat)
 | Write_mem of id * value * maybe (nat * nat) * value
 | Call_extern of string * 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_spec valsp -> 
      match valsp with
      | VS_val_spec (TypSchm_ts tq ((Typ_app (Id "reg") _) as t)) id -> (id, Reg id t):: (to_registers (Defs defs))
      | _ -> to_registers (Defs defs)
      end
    | DEF_reg_dec typ id -> (id, Reg id typ) :: (to_registers (Defs defs))
    | DEF_type tdef ->
      match tdef with 
      | TD_register id n1 n2 ranges -> 
	(id,Reg id (Typ_app (Id "vector")[]))::
	((to_reg_ranges id (Reg id (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 base_effect -> bool
let rec has_memory_effect efcts =
  match efcts with
  | [] -> false
  | e::efcts ->
    match e with
    | BE_wreg -> true
    | BE_wmem -> true
    | _ -> has_memory_effect efcts
    end 
  end

(*Look for externs as well*)
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 (Effect_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 to_externs : defs -> list (id * string)
let rec to_externs (Defs defs) =
  match defs with
  | [] -> []
  | def ::defs ->
    match def with
    | DEF_spec valsp ->
      match valsp with
      | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r e) as t)) id s ->
        (id,s)::(to_externs (Defs defs))
      | _ -> to_externs (Defs defs) end
    | _ -> to_externs (Defs defs) end
  end

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

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

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

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

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

val litV_to_vec : lit -> value
let litV_to_vec l =
  match l with
  | L_hex s ->
    let hexes = String.toCharList s in
    V_vector 0 true []
  | L_bin s -> 
    let bits = String.toCharList s in
    let exploded_bits = List.map (fun c -> String.toString [c]) bits in
    let bits = List.map (fun s -> match s with | "0" -> (V_lit L_zero) | "1" -> (V_lit L_one) end) exploded_bits in
    V_vector 0 true bits
  end

val access_vector : value -> nat -> value
let access_vector v n =
  match v with
  | V_vector m inc vs -> 
    if inc then
    List_extra.nth vs (n - m)
    else List_extra.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
    | 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 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)) ->
    foldr2 (fun vbox v mem -> match vbox with
                                       | V_boxref n -> 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 -> update_mem mem n v end)
      mem vs
end

val fupdate_vec : value -> nat -> value -> value
let fupdate_vec v n vexp =
  match v with
  | V_vector m inc vals -> 
    V_vector m inc (List.update vals (if inc then (n-m) else (m-n)) vexp)
  end

val replace_is : forall 'a. list 'a -> list 'a -> nat -> nat -> nat -> 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 -> nat -> nat -> 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_reg : list (id * reg_form) -> id -> maybe reg_form
let rec in_reg regs id =
  match regs with
  | [] -> Nothing
  | (eid,regf)::regs -> if eid = id then Just regf else in_reg regs id
end
val in_ctors : list (id * typ) -> id -> maybe typ
let rec in_ctors ctors id =
  match ctors with
  | [] -> Nothing
  | (cid,typ)::ctors -> if cid = 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 rec to_exp v =
    match v with
    | V_boxref n -> E_id (Id ("XXX 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.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(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
    | V_list(vals) -> E_list (List.map to_exp vals)
    | V_ctor id vals -> E_app id [to_exp vals]
    end

val find_type_def : defs -> id -> maybe type_def
val find_function : defs -> id -> maybe (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 
  | [] -> 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 find_memory : list ( id * typ ) -> id -> maybe typ
let find_memory mems id = List.lookup id mems

val find_extern : list ( id * string ) -> id -> maybe string
let find_extern externs id = List.lookup id externs

val match_pattern : pat -> value -> bool * list (id * value)
let rec match_pattern 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 pats -> 
   match value with
   | V_ctor cid (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 fvals ->
     List.foldr
       (fun (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_extra.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) pat ->
           match pat with
           | P_vector pats -> vec_concat_match pats r_vals
           | P_id id -> (false,[],[]) (*Need to have at least a guess of how many to consume*)
           | _ -> (false,[],[]) end) (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 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,r_vals) = vec_concat_match pats r_vals in
                       (matched_p, new_bounds++bounds,r_vals)
                     else (false,[],[]) end
    end


val find_funcl : list funcl -> value -> maybe (env * exp)
let rec find_funcl funcls value =
  match funcls with
  | [] -> Nothing
  | (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 -> value -> maybe (env * exp)
let rec find_case pexps value =
  match pexps with
  | [] -> Nothing
  | (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, external functions, letbound values, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
type top_level = Env of defs * list (id * string) * env * list (id*reg_form) * list (id * typ) * 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) * (maybe (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 -> if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (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
                 | Just(value) -> match value with
		                  | V_boxref n ->(Value (in_mem l_mem n),l_mem,l_env)
		                  | _ -> (Value value,l_mem,l_env) end
		 | Nothing -> match t_level with
		           | (Env defs externs lets regs mems ctors) ->
                             match in_env lets id with
                             | Just(value) -> (Value value,l_mem,l_env) 
                             | Nothing -> 
			       match in_reg regs id with
			       | Just(regf) -> 
			         (Action (Read_reg regf Nothing) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top), l_mem, l_env) 
			       | Nothing ->                                  
                                 let name = get_id id in
			         (Error (String.stringAppend "unbound identifier " name ),l_mem,l_env)
			        end 
                              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_for id from to_ by exp ->
      resolve_outcome (interp_main t_level l_env l_mem from)
                      (fun from_val lm le ->
                        match from_val with
                        | V_lit(L_num from_num) -> 
                          resolve_outcome (interp_main t_level le lm to_)
                                          (fun to_val lm le ->
                                            match to_val with
                                            | V_lit(L_num to_num) ->
                                              resolve_outcome 
                                                (interp_main t_level le lm by)
                                                (fun by_val lm le ->
                                                  match by_val with 
                                                  | V_lit (L_num by_num) ->
                                                    if (from_num = to_num) 
                                                    then (Value(V_lit L_unit),lm,le)
                                                    else interp_main t_level le lm 
                                                      (E_block [(E_let (LB_val_implicit (P_id id) (E_lit (L_num from_num))) exp);
                                                                (E_for id (E_lit (L_num (from_num + by_num))) (E_lit (L_num to_num)) (E_lit (L_num by_num)) exp)])
                                                  | _ -> (Error "by must be a number",lm,le) end)
                                                (fun a -> update_stack a (add_to_top_frame (fun b -> (E_for id (E_lit (L_num from_num)) (E_lit (L_num to_num)) b exp))))
                                            | _ -> (Error "to must be a number",lm,le) end)
                                           (fun a -> update_stack a (add_to_top_frame (fun t -> (E_for id (E_lit (L_num from_num)) t by exp))))
                        | _ -> (Error "from must be a number",lm,le) end)
                       (fun a -> update_stack a (add_to_top_frame (fun f -> (E_for id f to_ by exp))))
    | 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 "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_case e pats)))
    | E_record(FES_Fexps fexps _) -> 
      let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
      exp_list t_level (fun es -> (E_record(FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
	               (fun vs -> (V_record (List.zip 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.unzip (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 (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
                                                            (fun vs -> (V_record (List.zip 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
                                            | Just v -> (Value v,lm,l_env)
                                            | Nothing -> (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_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_num n1) ->
                          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), lm,le)
                                                              | _ -> (Error "Update of vector given non-vector",lm,le) end)
                                                            (fun a -> update_stack a (add_to_top_frame (fun v -> E_vector_update v (E_lit (L_num n1)) (to_exp vup)))))
                                          (fun a -> update_stack a (add_to_top_frame (fun e -> E_vector_update vec (E_lit (L_num n1)) e)))
                        | _ -> (Error "Update of vector requires number for access",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_update vec i exp)))                            
    | 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_num n1) ->
                          resolve_outcome 
                            (interp_main t_level l_env lm i2) 
                            (fun vi2 lm le ->
                              match vi2 with
                              | V_lit (L_num n2) ->
                                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),lm,le)
                                         | _ -> (Error "Vector update requires vector",lm,le) end)
                                       (fun a -> update_stack a 
                                         (add_to_top_frame (fun v -> E_vector_update_subrange v (E_lit (L_num n1)) (E_lit (L_num n2)) (to_exp v_rep))))))
                                  (fun a -> update_stack a 
                                    (add_to_top_frame (fun e -> E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e)))
                              | _ -> (Error "vector update requires number",lm,le) end)
                            (fun a -> update_stack a (add_to_top_frame (fun i2 -> E_vector_update_subrange vec (to_exp vi1) i2 exp)))
                        | _ -> (Error "vector update requires number",lm,le) end)
                      (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_vector_update_subrange vec i1 i2 exp)))
    | 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.unzip iexps in
      exp_list t_level (fun es -> (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es))) 
                       (fun vals -> V_vector (List_extra.head 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 (exp_list t_level (fun es -> E_app f es) (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] args) with
      | (Value v,lm,le) -> 
         (match (f,t_level) with
      	 | (id,(Env defs externs lets regs mems ctors)) -> 
	   (match find_function defs id with
	   | Just(funcls) -> 
             (match find_funcl funcls v with
	     | Nothing -> 
               let name = get_id id in
               (Error (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, lm,l_env))
                               (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
             end)
          | Nothing -> 
            (match in_ctors ctors id with
            | Just(typ) -> (Value (V_ctor id v), lm, le)
            | Nothing -> 
              (match find_memory mems id with
              | Just(typ) -> 
                (Action (Read_mem id v Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
              | Nothing -> 
                (match find_extern externs id with
                | Just(str) -> 
                  (Action (Call_extern str v) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
                | Nothing -> (Error "Unknown function call",lm,le) end)
	       end) end) end) end)
         | out -> out end)
    | E_app_infix l op r -> 
       let op = match op with
       | Id x -> DeIid x
       | DeIid _ -> op
       end in
      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
			                   | (Env defs externs lets regs mems ctors) ->
				             (match find_function defs op with
				             | Nothing -> 
                                               (match find_extern externs op with
                                               | Just(str) ->
                                                 (Action (Call_extern str (V_tuple [lv;rv])) (Frame (Id "0") (E_id (Id "0")) le lm Top),lm,le)
                                               | Nothing ->
                                                   (Error (String.stringAppend
                                                   "No matching function "
                                                   (get_id op)),lm,l_env) end)
				             | Just (funcls) ->
				               (match find_funcl funcls (V_tuple [lv;rv]) with 
				               | Nothing -> (Error "No matching pattern for function",lm,l_env)
				               | Just(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),Just 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,Nothing) -> outcome
                      | (outcome,Just 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 ] -> 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_block(e::exps))))
    end

and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
   let (Env defs externs lets regs mems ctors) = t_level in
   match lexp with
    | LEXP_id id -> 
      match in_env l_env id with
      | Just (V_boxref n) -> 
	if is_top_level 
	then ((Value (V_lit L_unit), update_mem l_mem n value, l_env),Nothing)
	else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_id id))
      | Just v -> if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e -> LEXP_id id))
      | Nothing -> 
	match in_reg regs id with
	| Just regf -> let request = (Action (Write_reg regf Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env) in
                       if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_id id))
	| Nothing -> 
	  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),Nothing)
          end
          else ((Error "Undefined id",l_mem,l_env),Nothing)
        end
      end 
    | LEXP_memory id exps -> 
      match (exp_list t_level E_tuple (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] exps) with
      | (Value v,lm,le) ->
        let request = (Action (Write_mem id v Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
        if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end))))
      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_tuple es) -> (LEXP_memory id es)))
      | e -> (e,Nothing) 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) -> 
          let next_builder le_builder = (fun e -> LEXP_vector (le_builder e) (E_lit (L_num n))) in
          (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),Nothing)
              | (v,true,_) -> ((Error "Vector does not contain reg values",lm,l_env),Nothing)
              | ((V_boxref n),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
              | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
            | _ -> ((Error "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 "Vector access must be a number",lm,le),Nothing) end)
      | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_vector lexp e)))
      | e -> (e,Nothing) 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) ->
              let next_builder le_builder = (fun e -> LEXP_vector_range (le_builder e) (E_lit (L_num n1)) (E_lit (L_num n2))) in
              (match (create_write_message_or_update t_level value l_env lm false lexp) with
              | ((Value v,lm,le), Just 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), Nothing)
                | (V_vector m inc vs,false) ->
                  ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
                | _ -> ((Error "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 "Vector slice requires a number", lm, le),Nothing) end)
          | (Action a s,lm,le) ->
            ((Action a s,lm, le), Just (fun e -> LEXP_vector_range lexp (E_lit (L_num  n1)) e))
          | e -> (e,Nothing) end)
        | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
      | (Action a s,lm,le) ->
        ((Action a s, lm,le), Just (fun e -> LEXP_vector_range lexp e exp2))
      | 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 fexps),lm,le),Just lexp_builder) ->
       match (in_env fexps id,is_top_level) with
       | (Just (V_boxref n),true) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
       | (Just (V_boxref n),false) -> ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
       | (Just v, true) -> ((Error "Field access requires record",lm,le),Nothing)
       | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
       | (Nothing,_) -> ((Error "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_field (lexp_builder e) id))
       | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
       | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
       | _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
       end 
     | e -> e 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),Nothing)
      | _ -> ((Error "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_val_explicit t pat e)))
    | e -> (e,Nothing) 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),Nothing)
      | _ -> ((Error "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_val_implicit pat e)))
    | e -> (e,Nothing) end
end	

let rec to_global_letbinds (Defs defs) t_level =
  let  (Env defs' externs lets regs mems ctors) = t_level in
  match defs with
  | [] -> ((Value (V_lit L_unit), emem, []),t_level)
  | def ::defs ->
    match def with
    | DEF_val lbind ->
      match interp_letbind t_level [] emem lbind with
      | ((Value v,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' externs (lets++le) regs mems ctors)
      | ((Action a s,lm,le),_) -> ((Error "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_externs defs) [] (to_registers defs) (to_memory_ops defs) (to_data_constructors 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 "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,v)::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 = Env defs (to_externs defs) [] (to_registers defs) (to_memory_ops defs) (to_data_constructors 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