diff options
Diffstat (limited to 'src/rewriter.ml')
| -rw-r--r-- | src/rewriter.ml | 35 |
1 files changed, 32 insertions, 3 deletions
diff --git a/src/rewriter.ml b/src/rewriter.ml index c7477e93..f0e2a811 100644 --- a/src/rewriter.ml +++ b/src/rewriter.ml @@ -1080,8 +1080,10 @@ let rewrite_sizeof (Defs defs) = (* Retrieve instantiation of the type variables of the called function for the given parameters in the original environment *) let inst = instantiation_of orig_exp in + Bindings.bindings param_map |> List.iter (fun (id, kids) -> print_endline (string_of_id id ^ " => " ^ Util.string_of_list ", " string_of_kid (KidSet.elements kids))); + KBindings.bindings inst |> List.iter (fun (kid, uvar) -> print_endline (string_of_kid kid ^ " => " ^ string_of_uvar uvar)); let kid_exp kid = begin - match KBindings.find kid inst with + match (try KBindings.find kid inst with e -> print_endline (string_of_kid kid ^ " " ^ string_of_exp full_exp); raise e) with | U_nexp nexp -> E_aux (E_sizeof nexp, simple_annot l (atom_typ nexp)) | _ -> raise (Reporting_basic.err_unreachable l @@ -2281,12 +2283,39 @@ let rewrite_defs_early_return = rewrite_defs_base { rewriters_base with rewrite_fun = rewrite_fun_early_return } +let rewrite_constraint = + let rec rewrite_nc (NC_aux (nc_aux, l)) = mk_exp (rewrite_nc_aux nc_aux) + and rewrite_nc_aux = function + | NC_bounded_ge (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2)) + | NC_bounded_le (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id ">=", mk_exp (E_sizeof n2)) + | NC_fixed (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "==", mk_exp (E_sizeof n2)) + | NC_not_equal (n1, n2) -> E_app_infix (mk_exp (E_sizeof n1), mk_id "!=", mk_exp (E_sizeof n2)) + | NC_and (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "&", rewrite_nc nc2) + | NC_or (nc1, nc2) -> E_app_infix (rewrite_nc nc1, mk_id "|", rewrite_nc nc2) + | NC_false -> E_lit (mk_lit L_true) + | NC_true -> E_lit (mk_lit L_false) + | NC_nat_set_bounded (kid, ints) -> + unaux_exp (rewrite_nc (List.fold_left (fun nc int -> nc_or nc (nc_eq (nvar kid) (nconstant int))) nc_true ints)) + in + let rewrite_e_aux (E_aux (e_aux, _) as exp) = + match e_aux with + | E_constraint nc -> + check_exp (env_of exp) (rewrite_nc nc) bool_typ + | _ -> exp + in + + let rewrite_e_constraint = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in + + rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_e_constraint) } + let rewrite_defs_ocaml = [ top_sort_defs; rewrite_defs_remove_vector_concat; + rewrite_constraint; rewrite_sizeof; - rewrite_defs_exp_lift_assign (* ; - rewrite_defs_separate_numbs *) + (* + (* rewrite_defs_exp_lift_assign (* ; + rewrite_defs_separate_numbs *) *) *) ] let rewrite_defs_remove_blocks = |