diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 55 |
1 files changed, 44 insertions, 11 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index b6f16d4f..aeb846d9 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -28,6 +28,7 @@ type action = | 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 + | 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 = @@ -83,6 +84,7 @@ let rec 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 @@ -97,6 +99,20 @@ let rec to_memory_ops (Defs defs) = | _ -> 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 @@ -274,6 +290,12 @@ let rec find_memory mems id = | (id',t)::mems -> if id'=id then Some t else find_memory mems id end +let rec find_extern externs id = + match externs with + | [] -> None + | (id',s)::externs -> if id'=id then Some s else find_extern externs id + end + val match_pattern : pat -> value -> bool * list (id * value) let rec match_pattern p value = match p with @@ -406,8 +428,8 @@ let rec find_case pexps value = if is_matching then Some(env,e) else find_case pexps value end -(*top_level is a three tuple of (all definitions, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *) -type top_level = defs * list (id*reg_form) * list (id * typ) * list (id * typ) +(*top_level is a three tuple of (all definitions, external funcitons, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *) +type top_level = defs * list (id * string) * 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) @@ -441,7 +463,7 @@ and interp_main t_level l_env l_mem exp = | 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,ctors) -> + | (defs,externs,regs,mems,ctors) -> 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) @@ -614,7 +636,7 @@ and interp_main t_level l_env l_mem exp = | 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,ctors)) -> + | (E_id(id),(defs,externs,regs,mems,ctors)) -> (match find_function defs id with | Some(funcls) -> resolve_outcome (interp_main t_level l_env l_mem (List.hd args)) @@ -641,8 +663,14 @@ and interp_main t_level l_env l_mem exp = 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) - end) end) + | None -> + (match find_extern externs id with + | Some(str) -> + resolve_outcome (interp_main t_level l_env l_mem (List.hd args)) + (fun argv lm le -> (Action (Call_extern str argv) (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) + end) end) end) | _ -> (Error "Application with expression other than identifier",l_mem,l_env) end | E_app_infix l op r -> @@ -651,9 +679,13 @@ and interp_main t_level l_env l_mem exp = resolve_outcome (interp_main t_level l_env lm r) (fun rv lm le -> (match t_level with - | (defs,regs,mems,ctors) -> + | (defs,externs,regs,mems,ctors) -> (match find_function defs op with - | None -> (Error "No matching pattern for function",lm,l_env) + | None -> + (match find_extern externs op with + | Some(str) -> + (Action (Call_extern str (V_tuple [lv;rv])) (Frame (Id "0") (E_id (Id "0")) le lm Top),lm,le) + | None -> (Error "No matching function",lm,l_env) end) | Some (funcls) -> (match find_funcl funcls (V_tuple [lv;rv]) with | None -> (Error "No matching pattern for function",lm,l_env) @@ -694,7 +726,7 @@ and interp_main t_level l_env l_mem exp = end and create_write_message_or_update t_level value l_env l_mem is_top_level lexp = - let (defs,regs,mems,ctors) = t_level in + let (defs,externs,regs,mems,ctors) = t_level in match lexp with | LEXP_id id -> match in_env l_env id with @@ -798,6 +830,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp = match a with | Read_reg _ _ -> ((Action a s,lm,le), Some (fun e -> LEXP_field (lexp_builder e) id)) | Read_mem _ _ _ -> ((Action a s,lm,le), Some (fun e -> LEXP_field (lexp_builder e) id)) + | Call_extern _ _ -> ((Action a s,lm,le), Some (fun e -> LEXP_field (lexp_builder e) id)) | _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),None) end | e -> e end) @@ -825,7 +858,7 @@ end let interp defs exp = - let t_level = (defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in + let t_level = (defs, to_externs defs,to_registers defs,to_memory_ops defs,to_data_constructors defs) in match interp_main t_level [] emem exp with | (o,_,_) -> o end @@ -845,5 +878,5 @@ let rec resume_main t_level stack value = end let resume defs stack value = - let t_level = (defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in + let t_level = (defs, to_externs defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in resume_main t_level stack value |