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