Skip to content

Commit

Permalink
remove duplicate definitions
Browse files Browse the repository at this point in the history
  • Loading branch information
tomaz1502 committed Apr 24, 2024
1 parent b64c0af commit cced754
Showing 1 changed file with 0 additions and 35 deletions.
35 changes: 0 additions & 35 deletions src/lib/Templates.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,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_g_decls_of_type (_, g_decls) = List.find_map inspect_decl g_decls in
let inspect_all_g_decls g_decls =
List.find_map Fun.id (List.map inspect_g_decls_of_type g_decls)
in
match inspect_all_g_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

0 comments on commit cced754

Please sign in to comment.