From bb99a5882b4fd9f1499d47eedb53f691829e19d1 Mon Sep 17 00:00:00 2001 From: dsac Date: Sat, 17 Dec 2022 16:30:10 +0100 Subject: [PATCH] [ast2C] store old values of variables used in the pre construct --- src/ast_to_c.ml | 16 +++++++++++++++- src/c_utils.ml | 6 +++++- src/cprint.ml | 30 +++++++++++++++++++++++++++--- 3 files changed, 47 insertions(+), 5 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 014007e..4bfdd9b 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -71,6 +71,17 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = let nb_int_vars, h_int = one_node node pv TInt in let nb_bool_vars, h_bool = one_node node pv TBool in let nb_real_vars, h_real = one_node node pv TReal in + + (** h_map gathers information from h_* maps above *) + let h_map = + Hashtbl.create (nb_int_vars + nb_bool_vars + nb_real_vars) in + let () = + Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("ivars", v)) h_int in + let () = + Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("bvars", v)) h_bool in + let () = + Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("rvars", v)) h_real in + let node_out_vars = snd node.n_outputs in let h_out = Hashtbl.create (List.length node_out_vars) in let () = List.iteri @@ -95,7 +106,9 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = nt_map_int = h_int; nt_map_bool = h_bool; nt_map_real = h_real; + nt_map = h_map; nt_output_map = h_out; + nt_prevars = pv; } in h end @@ -110,8 +123,9 @@ let make_state_types nodes: (ident, node_state) Hashtbl.t = let ast_to_c prog = let prog_st_types = make_state_types prog in - Format.printf "%s\n\n%a\n\n/* Node Prototypes: */\n%a" + Format.printf "%s\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" Config.c_includes cp_state_types prog_st_types cp_prototypes (prog, prog_st_types) + cp_nodes (prog, prog_st_types) diff --git a/src/c_utils.ml b/src/c_utils.ml index fe33c09..83a354a 100644 --- a/src/c_utils.ml +++ b/src/c_utils.ml @@ -7,7 +7,9 @@ open Ast * [(variable, is_pre)] to an index of the corresponding array (see below) * where [variable] is of type [t_var], and [is_pre] indicated whether we * deal with pre (x) or x. - * 6. A mapping mapping the output number i to its location (name of the + * 6. A mapping mapping any variable to the name of the C table containing it + * and the index at which it is stored (= union of the tables [nt_map_*]) + * 7. A mapping mapping the output number i to its location (name of the * table that contains it and index. * * Important Note: if a variable x appears behind a pre, it will count as two @@ -29,6 +31,8 @@ type node_state = nt_map_int: (t_var * bool, int) Hashtbl.t; nt_map_bool: (t_var * bool, int) Hashtbl.t; nt_map_real: (t_var * bool, int) Hashtbl.t; + nt_map: (t_var * bool, string * int) Hashtbl.t; nt_output_map: (int, string * int) Hashtbl.t; + nt_prevars: t_var list } diff --git a/src/cprint.ml b/src/cprint.ml index 3881257..ab2db08 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -41,7 +41,7 @@ let cp_prototype fmt (node, h): unit = | None -> failwith "This should not happend!" | Some nst -> begin - Format.fprintf fmt "void %s (%s *state, %a);\n" + Format.fprintf fmt "void %s (%s *state, %a)" node.n_name nst.nt_name cp_varlist (snd node.n_inputs) @@ -49,9 +49,33 @@ let cp_prototype fmt (node, h): unit = let rec cp_prototypes fmt (nodes, h) = match nodes with - | [] -> Format.fprintf fmt "\n\n" + | [] -> () | node :: nodes -> - Format.fprintf fmt "%a%a" + Format.fprintf fmt "%a;\n%a" cp_prototype (node, h) cp_prototypes (nodes, h) +(** The ollowing function prints the code to remember previous values of + * variables used with the pre construct. *) +let cp_prevars fmt (node, h) = + let node_st = Hashtbl.find h node.n_name in + List.iter + (fun v -> (** Note that «dst_array = src_array» should hold. *) + let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in + let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in + Format.fprintf fmt "\t%s[%d] = %s[%d];\n" + dst_array dst_idx src_array src_idx) + node_st.nt_prevars + +let rec cp_node fmt (node, h) = + Format.fprintf fmt "%a\n{\nTODO...\n%a}\n" + cp_prototype (node, h) + cp_prevars (node, h) + +let rec cp_nodes fmt (nodes, h) = + match nodes with + | [] -> () + | node :: nodes -> + Format.fprintf fmt "%a\n%a" + cp_node (node, h) + cp_nodes (nodes, h)