diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 214 | ||||
| -rw-r--r-- | src/pretty_print.ml | 4 |
2 files changed, 193 insertions, 25 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 98cf658e..9fd9f1e1 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -98,6 +98,20 @@ let rec to_memory_ops (Defs defs) = | _ -> to_memory_ops (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 (x,y) -> (y,x)) 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 -> option value let rec in_env env id = match env with @@ -173,12 +187,48 @@ let rec update_vector_slice vector value mem = vs mem end +let rec replace_ith ls v base i = + match ls with + | [] -> [] + | l::ls -> if base = i then v::ls else l::(replace_ith ls v (1+base) i) 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 (replace_ith vals vexp 0 (if inc then (n-m) else (m-n))) + end + +let rec replace_is ls vs base start stop = + match (ls,vs) with + | ([],_) -> [] + | (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.rev 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 -> 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 +val in_ctors : list (id * typ) -> id -> option typ +let rec in_ctors ctors id = + match ctors with + | [] -> None + | (cid,typ)::ctors -> if cid = id then Some 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 @@ -237,8 +287,31 @@ let rec match_pattern p value = 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_app id pats -> + match value with + | V_ctor cid (V_tuple vals) -> + if (id = cid && ((List.length pats) = (List.length vals))) + 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,[])) pats vals (true,[]) + else (false,[]) + | _ -> (false,[]) end + | P_record fpats _ -> + match value with + | V_record fvals -> + List.fold_right + (fun (FP_Fpat id pat) (matched_p,bounds) -> + if matched_p then + let (matched_p,new_bounds) = match in_env fvals id with + | None -> (false,[]) + | Some v -> match_pattern pat v end in + (matched_p, (new_bounds @ bounds)) + else (false,[])) fpats (true,[]) + | _ -> (false,[]) + end | P_vector pats -> match value with | V_vector n inc vals -> @@ -302,8 +375,17 @@ let rec find_funcl funcls value = 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 find_case : list pexp -> value -> option (env * exp) +let rec find_case pexps value = + match pexps with + | [] -> None + | (Pat_exp p e)::pexps -> + let (is_matching,env) = match_pattern p value in + 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) 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) @@ -337,7 +419,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) -> + | (defs,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) @@ -354,6 +436,38 @@ and interp_main t_level l_env l_mem exp = | 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 + | None -> (Error "No matching patterns in case",lm,le) + | Some (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.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))) @@ -419,11 +533,54 @@ and interp_main t_level l_env l_mem exp = 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)))))) + (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) -> @@ -435,7 +592,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)) -> + | (E_id(id),(defs,regs,mems,ctors)) -> (match find_function defs id with | Some(funcls) -> resolve_outcome (interp_main t_level l_env l_mem (List.hd args)) @@ -449,14 +606,19 @@ and interp_main t_level l_env l_mem exp = end)) (fun a -> update_stack a (add_to_top_frame (fun a -> (E_app f [a])))) | None -> - (match find_memory mems id with + (match in_ctors ctors 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 argv lm le -> (Value (V_ctor id argv), 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) + | 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) + end) end) | _ -> (Error "Application with expression other than identifier",l_mem,l_env) end | E_app_infix l op r -> @@ -465,7 +627,7 @@ 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) -> + | (defs,regs,mems,ctors) -> (match find_function defs op with | None -> (Error "No matching pattern for function",lm,l_env) | Some (funcls) -> @@ -507,7 +669,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) = t_level in + let (defs,regs,mems,ctors) = t_level in match lexp with | LEXP_id id -> match in_env l_env id with @@ -542,6 +704,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp = | (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 @@ -550,14 +713,16 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp = (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) + | ((V_boxref n),false, Some lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Some (next_builder lexp_builder)) + | (v,false, Some lexp_builder) -> ((Value v,lm,le), Some (next_builder lexp_builder)) 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) + | ((Write_reg regf None value),false) -> ((Action (Write_reg regf (Some (n,n)) value) s,lm,le), Some (next_builder lexp_builder)) + | ((Write_mem id a None value),true) -> ((Action (Write_mem id a (Some (n,n)) value) s,lm,le), None) + | ((Write_mem id a None value),false) -> ((Action (Write_mem id a (Some (n,n)) value) s,lm,le), Some (next_builder lexp_builder)) + | _ -> ((Action a s,lm,le), Some (next_builder lexp_builder)) 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))) @@ -571,18 +736,21 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp = | (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), 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)))) + ((Value (slice_vector v n1 n2),lm,l_env), Some (next_builder lexp_builder)) | _ -> ((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 (Write_reg regf (Some (n1,n2)) value) s,lm,le), Some (next_builder lexp_builder)) + | ((Action (Write_mem id a None value) s,lm,le), Some lexp_builder) -> + ((Action (Write_mem id a (Some (n1,n2)) value) s,lm,le), Some (next_builder lexp_builder)) | ((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))))) + ((Action a s,lm,le), Some (next_builder lexp_builder)) | e -> e end) | _ -> ((Error "Vector slice requires a number", lm, le),None) end) | (Action a s,lm,le) -> @@ -616,7 +784,7 @@ end let interp defs exp = - let t_level = (defs, to_registers defs,to_memory_ops defs) in + let t_level = (defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in match interp_main t_level [] emem exp with | (o,_,_) -> o end @@ -636,5 +804,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) in + let t_level = (defs, to_registers defs,to_memory_ops defs,to_data_constructors defs) in resume_main t_level stack value diff --git a/src/pretty_print.ml b/src/pretty_print.ml index b8e936b3..917a469f 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -612,8 +612,8 @@ let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) = - let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd ";" pp_lem_funcl funcl in - fprintf ppf "@[<0>(%a %a %a %a [%a]@]" + let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in + fprintf ppf "@[<0>(%a %a %a %a [%a])@]" kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls let pp_lem_def ppf (DEF_aux(d,(l,_))) = |