[ast2C] store old values of variables used in the pre construct

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)
 

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
   }
 

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)