Skip to content

Commit

Permalink
fixing bugs introduced by merge
Browse files Browse the repository at this point in the history
  • Loading branch information
@tomaz1502
tomaz1502 committed Apr 28, 2024
1 parent 23254b2 commit c6fbcaf
Showing 1 changed file with 39 additions and 55 deletions.
94 changes: 39 additions & 55 deletions src/lib/Templates.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,31 +8,50 @@ type synt_vars_data = (variable_name * synt_var_kind * int) list

type var_map = (variable_name, parsed_template_arg) Hashtbl.t

let rec get_const_disc_arith_expr = function
| Parsed_sum_diff (lhs, rhs, Parsed_plus) -> NumConst.add (get_const_disc_arith_expr lhs) (get_const_disc_term rhs)
| Parsed_sum_diff (lhs, rhs, Parsed_minus) -> NumConst.sub (get_const_disc_arith_expr lhs) (get_const_disc_term rhs)
| Parsed_term term -> get_const_disc_term term

and get_const_disc_term = function
| Parsed_product_quotient (lhs, rhs, Parsed_mul) -> NumConst.mul (get_const_disc_term lhs) (get_const_disc_factor rhs)
| Parsed_product_quotient (lhs, rhs, Parsed_div) -> NumConst.div (get_const_disc_term lhs) (get_const_disc_factor rhs)
| Parsed_factor factor -> get_const_disc_factor factor

and get_const_disc_factor = function
| Parsed_constant (ParsedValue.Weak_number_value value) -> value
| Parsed_unary_min factor -> NumConst.neg (get_const_disc_factor factor)
| Parsed_nested_expr expr -> get_const_disc_arith_expr expr
| _ -> failwith "[get_const_disc_factor]: argument is not an integer constant"
let eval_expr_err_msg = "[eval_boolean_expression]: Trying to evaluate an expression whose value is not known at compile time."

let rec eval_parsed_boolean_expression g_decls = function
| Parsed_discrete_bool_expr e -> eval_parsed_discrete_bool_expr g_decls e
| Parsed_conj_dis _ -> failwith eval_expr_err_msg

and eval_parsed_discrete_bool_expr g_decls = function
| Parsed_arithmetic_expr e -> eval_parsed_arithmetic_expr g_decls e
| _ -> failwith eval_expr_err_msg

and eval_parsed_arithmetic_expr g_decls = function
| Parsed_sum_diff (arith_expr, term, Parsed_plus) -> (eval_parsed_arithmetic_expr g_decls arith_expr) + (eval_parsed_term g_decls term)
| Parsed_sum_diff (arith_expr, term, Parsed_minus) -> (eval_parsed_arithmetic_expr g_decls arith_expr) - (eval_parsed_term g_decls term)
| Parsed_term t -> eval_parsed_term g_decls t

and eval_parsed_term g_decls = function
| Parsed_product_quotient (term, factor, Parsed_mul) -> eval_parsed_term g_decls term * eval_parsed_factor g_decls factor
| Parsed_product_quotient (term, factor, Parsed_div) -> eval_parsed_term g_decls term / eval_parsed_factor g_decls factor
| Parsed_factor factor -> eval_parsed_factor g_decls factor

and eval_parsed_factor g_decls = function
| Parsed_constant v -> NumConst.to_bounded_int (ParsedValue.to_numconst_value v)
| Parsed_variable (name, _) -> expand_const_var g_decls name
| _ -> failwith eval_expr_err_msg

and expand_const_var g_decls name =
let inspect_decl (name', expr_opt) = if name = name' then expr_opt else None in
let inspect_decls_of_type (_, decls_of_type) = List.find_map inspect_decl decls_of_type in
let inspect_all_decls decls =
List.find_map Fun.id (List.map inspect_decls_of_type decls)
in
match inspect_all_decls g_decls with
| None -> failwith "[expand_model]: Size of syntatic array is a non-constant variable."
| Some expr -> eval_parsed_boolean_expression g_decls expr

let find_arr_len_opt arr_name =
List.find_map (fun (name, _, len) -> if arr_name = name then Some len else None)

let gen_var_from_access def gen_var_from_name arr_name index synt_arrays =
let gen_var_from_access g_decls def gen_var_from_name arr_name index synt_arrays =
let arr_len_opt = find_arr_len_opt arr_name synt_arrays in
match arr_len_opt with
| None -> def
| Some len ->
let index_c = NumConst.to_bounded_int (get_const_disc_arith_expr index) in
let index_c = eval_parsed_arithmetic_expr g_decls index in
if index_c < len then
let var_name = gen_access_id arr_name index_c in
gen_var_from_name var_name
Expand Down Expand Up @@ -62,41 +81,6 @@ let instantiate_discrete_arithmetic_expression (param_map : var_map) : parsed_di
let instantiate_convex_predicate (param_map : var_map) (inv : convex_predicate) : convex_predicate =
List.map (instantiate_discrete_boolean_expression param_map) inv

let eval_expr_err_msg = "[eval_boolean_expression]: Trying to evaluate an expression whose value is not known at compile time."

let rec eval_parsed_boolean_expression g_decls = function
| Parsed_discrete_bool_expr e -> eval_parsed_discrete_bool_expr g_decls e
| Parsed_conj_dis _ -> failwith eval_expr_err_msg

and eval_parsed_discrete_bool_expr g_decls = function
| Parsed_arithmetic_expr e -> eval_parsed_arithmetic_expr g_decls e
| _ -> failwith eval_expr_err_msg

and eval_parsed_arithmetic_expr g_decls = function
| Parsed_sum_diff (arith_expr, term, Parsed_plus) -> (eval_parsed_arithmetic_expr g_decls arith_expr) + (eval_parsed_term g_decls term)
| Parsed_sum_diff (arith_expr, term, Parsed_minus) -> (eval_parsed_arithmetic_expr g_decls arith_expr) - (eval_parsed_term g_decls term)
| Parsed_term t -> eval_parsed_term g_decls t

and eval_parsed_term g_decls = function
| Parsed_product_quotient (term, factor, Parsed_mul) -> eval_parsed_term g_decls term * eval_parsed_factor g_decls factor
| Parsed_product_quotient (term, factor, Parsed_div) -> eval_parsed_term g_decls term / eval_parsed_factor g_decls factor
| Parsed_factor factor -> eval_parsed_factor g_decls factor

and eval_parsed_factor g_decls = function
| Parsed_constant v -> NumConst.to_bounded_int (ParsedValue.to_numconst_value v)
| Parsed_variable (name, _) -> expand_const_var g_decls name
| _ -> failwith eval_expr_err_msg

and expand_const_var g_decls name =
let inspect_decl (name', expr_opt) = if name = name' then expr_opt else None in
let inspect_decls_of_type (_, decls_of_type) = List.find_map inspect_decl decls_of_type in
let inspect_all_decls decls =
List.find_map Fun.id (List.map inspect_decls_of_type decls)
in
match inspect_all_decls g_decls with
| None -> failwith "[expand_model]: Size of syntatic array is a non-constant variable."
| Some expr -> eval_parsed_boolean_expression g_decls expr

(*****************************************************************************)
(* Instantiation of templates *)
(*****************************************************************************)
Expand Down Expand Up @@ -321,19 +305,19 @@ and expand_parsed_discrete_factor g_decls synt_arrays = fun factor ->
| Parsed_access (factor', index) ->
let arr_name = get_name_of_factor factor' in
let gen_var_from_name name = Parsed_variable (name, 0) in
gen_var_from_access factor gen_var_from_name arr_name index synt_arrays
gen_var_from_access g_decls factor gen_var_from_name arr_name index synt_arrays
| _ -> factor

let expand_sync (g_decls : variable_declarations) : unexpanded_sync -> sync = function
| UnexpandedSync action -> Sync (expand_name_or_access g_decls action)
| UnexpandedNoSync -> NoSync

let expand_indexed_update (synt_arrays : synt_vars_data) : parsed_scalar_or_index_update_type -> parsed_scalar_or_index_update_type =
let expand_indexed_update (g_decls : variable_declarations) (synt_arrays : synt_vars_data) : parsed_scalar_or_index_update_type -> parsed_scalar_or_index_update_type =
fun e ->
match e with
| Parsed_indexed_update (Parsed_scalar_update (name, _), index) -> begin
let gen_var_from_name name = Parsed_scalar_update (name, 0) in
gen_var_from_access e gen_var_from_name name index synt_arrays
gen_var_from_access g_decls e gen_var_from_name name index synt_arrays
end
| _ -> e

Expand Down

0 comments on commit c6fbcaf

Please sign in to comment.