Merge ast2C_proposition branch with the master one

As Antoine Grimod said that it was already done.

src/ast_to_c.ml

@@ -1,280 +1,324 @@
 open Ast
+open Intermediate_ast
+open Intermediate_utils
+open Cprint
+open Cast
+open Utils
+open Ctranslation
 
-type var_list_delim =
-  | Base
-  | Arg
-  | Dec
 
-let rec pp_varlist var_list_delim fmt : t_varlist -> unit = function
-  | ([], []) -> ()
-  | ([TInt] , IVar h :: []) -> Format.fprintf fmt (
-      match var_list_delim with
-          | Base -> "%s"
-          | Arg -> "int %s"
-          | Dec -> "int %s;") h
-  | ([TReal], RVar h :: []) -> Format.fprintf fmt (
-      match var_list_delim with
-          | Base -> "%s"
-          | Arg -> "float %s"
-          | Dec -> "float %s;") h
-  | ([TBool], BVar h :: []) -> Format.fprintf fmt (
-      match var_list_delim with
-          | Base -> "%s"
-          | Arg -> "bool %s"
-          | Dec -> "bool %s;") h
-  | (TInt :: tl,  IVar h :: h' :: l) ->
-      Format.fprintf fmt (
-          match var_list_delim with
-              | Base -> "%s, %a"
-              | Arg -> "int %s, %a"
-              | Dec -> "int %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l)
-  | (TBool :: tl, BVar h :: h' :: l) ->
-      Format.fprintf fmt (
-          match var_list_delim with
-              | Base -> "%s, %a"
-              | Arg -> "bool %s, %a"
-              | Dec -> "bool %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l)
-  | (TReal :: tl, RVar h :: h' :: l) ->
-      Format.fprintf fmt (
-          match var_list_delim with
-              | Base -> "%s, %a"
-              | Arg -> "float %s, %a"
-              | Dec -> "float %s;\n\t%a") h (pp_varlist var_list_delim) (tl, h' :: l)
-  | _ -> raise (MyTypeError "This exception should not have beed be raised.")
 
-let rec pp_retvarlist fmt : t_varlist -> unit = function
-  | ([], []) -> ()
-  | ([TInt] , IVar h :: []) -> Format.fprintf fmt "int"
-  | ([TReal], RVar h :: []) -> Format.fprintf fmt "float"
-  | ([TBool], BVar h :: []) -> Format.fprintf fmt "bool"
-  | (TInt :: tl,  IVar h :: h' :: l) ->
-      Format.fprintf fmt "int, %a" pp_retvarlist (tl, h' :: l)
-  | (TBool :: tl, BVar h :: h' :: l) ->
-      Format.fprintf fmt "float, %a" pp_retvarlist (tl, h' :: l)
-  | (TReal :: tl, RVar h :: h' :: l) ->
-      Format.fprintf fmt "bool, %a" pp_retvarlist (tl, h' :: l)
-  | _ -> raise (MyTypeError "This exception should not have beed be raised.")
+(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *)
+let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist =
+  let c = ref 1 in
+  let ast_to_intermediate_ast_varlist vl = snd vl in
+  let rec ast_to_intermediate_ast_expr hloc = function
+    | EVar   (_, v) ->
+      begin
+        match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with
+        | None -> IEVar (CVInput (name_of_var v))
+        | Some (s, i) -> IEVar (CVStored (s, i))
+      end
+    | EMonOp (_, MOp_pre, EVar (_, v)) ->
+        let s, i = Hashtbl.find hloc (Utils.name_of_var v, true) in
+        IEVar (CVStored (s, i))
+    | EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e)
+    | EBinOp (_, op, e, e') ->
+       IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
+    | ETriOp (_, op, e, e', e'') ->
+        IETriOp
+          (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e', ast_to_intermediate_ast_expr hloc e'')
+    | EComp  (_, op, e, e') ->
+        IEComp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
+    | EWhen  (_, e, e') ->
+        IEWhen (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
+    | EReset  (_, e, e') ->
+        IEReset (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
+    | EConst (_, c) -> IEConst c
+    | ETuple (_, l) -> IETuple (List.map (ast_to_intermediate_ast_expr hloc) l)
+    | EApp   (_, n, e) ->
+      begin
+        let e = ast_to_intermediate_ast_expr hloc e in
+        let res = IEApp (!c, n, e) in
+        let () = incr c in
+        res
+      end
+  in
+  let ast_to_intermediate_ast_eq hloc (patt, expr) : i_equation =
+    (ast_to_intermediate_ast_varlist patt, ast_to_intermediate_ast_expr hloc expr) in
+  List.map
+    begin
+    fun node ->
+      let () = c := 1 in
+      let hloc = (Hashtbl.find h node.n_name).nt_map in
+      {
+        in_name = node.n_name;
+        in_inputs = ast_to_intermediate_ast_varlist node.n_inputs;
+        in_outputs = ast_to_intermediate_ast_varlist node.n_outputs;
+        in_local_vars = ast_to_intermediate_ast_varlist node.n_local_vars;
+        in_equations = List.map (ast_to_intermediate_ast_eq hloc) node.n_equations;
+      }
+    end
+    nodes
 
-let rec pp_prevarlist node_name fmt : t_varlist -> unit = function
-  | ([], []) -> ()
-  | ([TInt] , IVar h :: []) -> Format.fprintf fmt "int pre_%s_%s;" node_name h
-  | ([TReal], RVar h :: []) -> Format.fprintf fmt "float pre_%s_%s;" node_name h
-  | ([TBool], BVar h :: []) -> Format.fprintf fmt "bool pre_%s_%s;" node_name h
-  | (TInt :: tl,  IVar h :: h' :: l) ->
-      Format.fprintf fmt "int pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l)
-  | (TBool :: tl, BVar h :: h' :: l) ->
-      Format.fprintf fmt "float pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l)
-  | (TReal :: tl, RVar h :: h' :: l) ->
-      Format.fprintf fmt "bool pre_%s_%s;\n%a" node_name h (pp_prevarlist node_name) (tl, h' :: l)
-  | _ -> raise (MyTypeError "This exception should not have beed be raised.")
+(** The following function defines the [node_states] for the nodes of a program,
+  * and puts them in a hash table. *)
+let make_state_types nodes: node_states =
+  (* Hash table to fill *)
+  let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in
 
-let rec pp_asnprevarlist node_name fmt : t_varlist -> unit = function
-  | ([], []) -> ()
-  | ([TInt] , IVar h :: []) | ([TReal], RVar h :: []) | ([TBool], BVar h :: []) -> Format.fprintf fmt "\tpre_%s_%s = %s;" node_name h h
-  | (TInt :: tl,  IVar h :: h' :: l) | (TBool :: tl, BVar h :: h' :: l) | (TReal :: tl, RVar h :: h' :: l) ->
-      Format.fprintf fmt "\tpre_%s_%s = %s;\n%a" node_name h h (pp_asnprevarlist node_name) (tl, h' :: l)
-  | _ -> raise (MyTypeError "This exception should not have beed be raised.")
+  (** [one_node node pv ty] computes the number of variables of type [ty] in
+    * [node] and a mapping from the variables of type ([ty] * bool) to int,
+    *   where [pv] is a list of variables used in the pre construct in the
+    *   program. *)
+  let one_node node pv ty =
+    (* variables of type [ty] among output and local variables *)
+    let vars =
+      List.filter (fun v -> type_var v = [ty])
+        (snd (varlist_concat node.n_outputs node.n_local_vars)) in
+    let all_vars =
+      List.filter (fun v -> type_var v = [ty])
+        (snd (varlist_concat (varlist_concat node.n_inputs node.n_outputs) node.n_local_vars)) in
+    let pre_vars =
+      List.filter (fun v -> List.mem v pv) all_vars in
+    let vars = List.map Utils.name_of_var vars in
+    let pre_vars = List.map Utils.name_of_var pre_vars in
+    let nb = (List.length vars) + (List.length pre_vars) in
+    let tyh: (ident * bool, int) Hashtbl.t = Hashtbl.create nb in
+    let i =
+      List.fold_left
+        (fun i v -> let () = Hashtbl.add tyh (v, false) i in i + 1) 0 vars in
+    let _ = 
+      List.fold_left
+        (fun i v -> let () = Hashtbl.add tyh (v, true) i in i + 1) i pre_vars in
+    (nb, tyh)
+  in
 
-let reset_expressions_counter = ref 0;;
-
-let outputs = ref [];;
-
-let pp_expression node_name =
-  let rec pp_expression_aux fmt expression =
-    let rec pp_expression_list fmt exprs =
-      match exprs with
-      | ETuple([], []) -> ()
-      | ETuple (_ :: tt, expr :: exprs) ->
-          Format.fprintf fmt "%a%s%a"
-            pp_expression_aux expr
-            (if (List.length tt > 0) then ", " else "")
-            pp_expression_list (ETuple (tt, exprs))
-      | _ -> raise (MyTypeError "This exception should not have been raised.")
+  (** [find_prevars n] returns the list of variables appearing after a pre in
+    * the node [n].
+    * Note that the only occurrence of pre are of the form pre (var), due to
+    * the linearization pass.
+    *)
+  let find_prevars node =
+    let rec find_prevars_expr = function
+      | EConst _ | EVar _ -> []
+      | EMonOp (_, MOp_pre, EVar (_, v)) -> [v]
+      | EMonOp (_, _, e) -> find_prevars_expr e
+      | ETriOp (_, _, e, e', e'') ->
+          (find_prevars_expr e) @ (find_prevars_expr e') @ (find_prevars_expr e'')
+      | EComp  (_, _, e, e')
+      | EBinOp (_, _, e, e')
+      | EWhen  (_, e, e')
+      | EReset (_, e, e') -> (find_prevars_expr e) @ (find_prevars_expr e')
+      | ETuple (_, l) -> List.flatten (List.map (find_prevars_expr) l)
+      | EApp   (_, _, e) -> find_prevars_expr e
     in
-    match expression with
-    | EWhen (_, e1, e2) ->
-        begin
-          Format.fprintf fmt "%a ? %a : 0"
-            pp_expression_aux e2
-            pp_expression_aux e1
-        end
-    | EReset (_, e1, e2) ->
-        begin
-            incr reset_expressions_counter;
-            (* Use following trick as we can't use `;`:
-               if(((var = val) && false) || condition)
-               is equivalent to an incorrect statement like
-               if({var = val; condition})
-               We also use this trick with the fact that `0` can be interpreted as a `bool`, an `int` and a `float` *)
-            (* could use C macros to simplify the C code *)
-            Format.fprintf fmt "(((tmp_reset[%i] = %a) && false) || init_%s) ? (((init[%i] = tmp_reset[%i]) || true) ? tmp_reset[%i] : 0) : (%a ? init[%i] : tmp_reset[%i])"
-            (!reset_expressions_counter - 1)
-            pp_expression_aux e1
-            node_name
-            (!reset_expressions_counter - 1)
-            (!reset_expressions_counter - 1)
-            (!reset_expressions_counter - 1)
-            pp_expression_aux e2
-            (!reset_expressions_counter - 1)
-            (!reset_expressions_counter - 1)
-        end
-    | EConst (_, c) ->
-        begin match c with
-        | CBool b -> Format.fprintf fmt "%s" (Bool.to_string b)
-        | CInt i ->  Format.fprintf fmt "%i" i
-        | CReal r -> Format.fprintf fmt "%f" r
-        end
-    | EVar (_, IVar v) | EVar (_, BVar v) | EVar (_, RVar v) -> Format.fprintf fmt "%s" v
-    | EMonOp (_, mop, arg) ->
-        begin match mop with
-        | MOp_not ->
-            Format.fprintf fmt "!%a"
-              pp_expression_aux arg
-        | MOp_minus ->
-            Format.fprintf fmt "-%a"
-              pp_expression_aux arg
-        | MOp_pre ->
-            Format.fprintf fmt "pre_%s_%a" node_name
-              pp_expression_aux arg
-        end
-    | EBinOp (_, BOp_arrow, arg, arg') ->
-        Format.fprintf fmt "init_%s ? %a : %a"
-          node_name
-          pp_expression_aux arg
-          pp_expression_aux arg'
-    | EBinOp (_, bop, arg, arg') ->
-        begin
-        let s = match bop with
-        | BOp_add -> " + " | BOp_sub -> " - "
-        | BOp_mul -> " * " | BOp_div -> " / " | BOp_mod -> " % "
-        | BOp_and -> " && " | BOp_or  -> " || " | _ -> "" (* `ocamlc` doesn't detect that `BOp_arrow` can't match here *) in
-        Format.fprintf fmt "%a%s%a"
-          pp_expression_aux arg
-          s
-          pp_expression_aux arg'
-        end
-    | EComp (_, cop, arg, arg') ->
-        begin
-        let s = match cop with
-        | COp_eq  -> " == "
-        | COp_neq -> " != "
-        | COp_le  -> " <= " | COp_lt  -> " < "
-        | COp_ge  -> " >= " | COp_gt  -> " > " in
-        Format.fprintf fmt "%a%s%a"
-          pp_expression_aux arg
-          s
-          pp_expression_aux arg'
-        end
-    | ETriOp (_, top, arg, arg', arg'') ->
-        begin
-            Format.fprintf fmt "%a ? %a : %a"
-              pp_expression_aux arg
-              pp_expression_aux arg'
-              pp_expression_aux arg''
-        end
-    | EApp (_, f, args)  ->
-        Format.fprintf fmt "%s(%a)"
-          f.n_name
-          pp_expression_list args
-    | ETuple _ ->
-        Format.fprintf fmt "%a"
-          pp_expression_list expression;
+    list_remove_duplicates
+      (List.fold_left
+        (fun acc (_, expr) -> (find_prevars_expr expr) @ acc)
+        [] node.n_equations)
+  in
+
+  (** [count_app n] count the number of auxiliary nodes calls in [n] *)
+  let count_app n =
+    let rec count_app_expr = function
+      | EConst _ | EVar _ -> 0
+      | EMonOp (_, _, e) -> count_app_expr e
+      | ETriOp (_, _, e, e', e'') ->
+          (count_app_expr e) + (count_app_expr e') + (count_app_expr e'')
+      | EComp  (_, _, e, e')
+      | EBinOp (_, _, e, e')
+      | EWhen  (_, e, e')
+      | EReset (_, e, e') -> (count_app_expr e) + (count_app_expr e')
+      | ETuple (_, l) ->
+          List.fold_left (fun acc e -> acc + count_app_expr e) 0 l
+      | EApp   (_, _, e) -> 1 + count_app_expr e
     in
-  pp_expression_aux
+    List.fold_left
+      (fun i (_, expr) -> i + count_app_expr expr)
+      0 n.n_equations
+  in
 
-(* deterministic *)
-let nodes_outputs = Hashtbl.create Config.maxvar;;
+  (** [aux] iterates over all nodes of the program to build the required hash
+    * table *)
+  let rec aux nodes =
+    match nodes with
+    | [] -> h
+    | node :: nodes ->
+        begin
+        let h = aux nodes in
+        let node_name = node.n_name in
+        let pv = find_prevars node in
+        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
 
-let prepend_output_aux node_name name =
-    "output_" ^ node_name ^ "_" ^ name
+        (** 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 prepend_output output node_name =
-    match output with
-    | BVar name -> BVar (prepend_output_aux node_name name)
-    | IVar name -> IVar (prepend_output_aux node_name name)
-    | RVar name -> RVar (prepend_output_aux node_name name)
+        let node_out_vars = snd node.n_outputs in
+        let h_out = Hashtbl.create (List.length node_out_vars) in
+        let () = List.iteri
+          (fun n (v: t_var) ->
+            match v with
+            | IVar s ->
+                let i = Hashtbl.find h_int (s, false) in
+                Hashtbl.add h_out n ("ivars", i)
+            | BVar s ->
+                let i = Hashtbl.find h_bool (s, false) in
+                Hashtbl.add h_out n ("bvars", i)
+            | RVar s ->
+                let i = Hashtbl.find h_real (s, false) in
+                Hashtbl.add h_out n ("rvars", i))
+          (snd node.n_outputs) in
+        let () = Hashtbl.add h node_name
+          {
+            nt_name = Format.asprintf "t_state_%s" node.n_name;
+            nt_nb_int = nb_int_vars;
+            nt_nb_bool = nb_bool_vars;
+            nt_nb_real = nb_real_vars;
+            nt_map = h_map;
+            nt_output_map = h_out;
+            nt_prevars = pv;
+            nt_count_app = count_app node;
+          } in
+        h
+        end
+    in
+  aux nodes
 
-let rec pp_equations node_name fmt: t_eqlist -> unit = function
+
+
+(** The following C-printer functions are in this file, as they need to work on
+  * the AST and are not simple printers. *)
+
+
+
+(** The following 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.in_name in
+  match (Hashtbl.find h node.in_name).nt_prevars with
   | [] -> ()
-  | ((l_types, vars), (EApp (r_types, node, exprs))) :: eqs when l_types <> [] -> Format.fprintf fmt "%a" (pp_equations node_name) ((([], []), (EApp (r_types, node, exprs))) :: ((l_types, vars), (ETuple (fst node.n_outputs, List.map (fun output -> EVar (fst node.n_outputs, prepend_output output node.n_name)) (snd node.n_outputs)))) :: eqs)
-  | (([], []), (ETuple ([], []))) :: eqs -> Format.fprintf fmt "%a" (pp_equations node_name) eqs
-  | ((l_type :: l_types, var :: vars), (ETuple (r_type :: r_types, expr :: exprs))) :: eqs -> Format.fprintf fmt "%a" (pp_equations node_name) ((([l_type], [var]), expr) :: ((l_types, vars), (ETuple (r_types, exprs))) :: eqs)
-  | (([], []), expr) :: eqs ->
-      Format.fprintf fmt "\t%a;\n%a"
-        (pp_expression node_name) expr
-        (pp_equations node_name) eqs
-  | (patt, expr) :: eqs ->
-      Format.fprintf fmt "\t%a = %a;\n%a"
-        (pp_varlist Base) patt
-        (pp_expression node_name) expr
-        (pp_equations node_name) eqs
+  | l ->
+      Format.fprintf fmt
+        "\n\t/* Remember the values used in the [pre] construct */\n";
+      List.iter
+        (fun v -> (** Note that «dst_array = src_array» should hold. *)
+          match Hashtbl.find_opt node_st.nt_map (v, false) with
+          | Some (src_array, src_idx) ->
+            let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
+            Format.fprintf fmt "\tstate->%s[%d] = state->%s[%d];\n"
+              dst_array dst_idx src_array src_idx
+          | None -> 
+            let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
+            Format.fprintf fmt "\tstate->%s[%d] = %s;\n"
+              dst_array dst_idx v
+          )
+        (List.map Utils.name_of_var l)
 
-(* By prepending to the `Format.formatter` `fmt` we could just declare these arrays once with a size of the maximum `reset_expressions_counter` *)
-let pp_resvars reset_expressions_counter =
-    (* use the fact that any boolean and any integer can be encoded as a float, concerning integers [-2^(23+1) + 1; 2^(23+1) + 1] are correctly encoded (cf https://stackoverflow.com/a/53254438) *)
-    Format.sprintf "float tmp_reset[%i], init[%i];" reset_expressions_counter reset_expressions_counter
 
-let pp_return node_name fmt outputs =
-    if node_name = "main" then
-    (Format.fprintf fmt "return %a;"
-    (pp_varlist Base) outputs)
-    else
-        Format.fprintf fmt "%s" (String.concat "\n\t" (List.map (fun output -> match output with | BVar name | IVar name | RVar name -> "output_" ^ node_name ^ "_" ^ name ^ " = " ^ name ^ ";") (snd outputs)))
 
-let pp_node fmt node =
-    (* undefined behavior if the initial code uses a variable with name:
-        - `init_{NODE_NAME}`
-        - `tmp_reset_{int}`
-        - `init_{int}`
-        - `pre_{NODE_NAME}_{VARIABLE}`
-        - `output_{NODE_NAME}_{VARIABLE}` *)
-  reset_expressions_counter := 0;
-  let _ = (pp_equations node.n_name) Format.str_formatter node.n_equations in
-  reset_expressions_counter := 0;
-  Format.fprintf fmt "bool init_%s = true;\n\n%a\n\n%a\n\n%a\n\n%s\n\n%s %s(%a)\n{\n\t%a\n\n\t%a\n\n%a\n\n\tinit_%s = false;\n\n%a\n\n%a\n\n%a\n\n\t%a\n}\n"
-    node.n_name
-    (* could avoid declaring unused variables *)
-    (pp_prevarlist node.n_name) node.n_inputs
-    (pp_prevarlist node.n_name) node.n_local_vars
-    (pp_prevarlist node.n_name) node.n_outputs
-    (pp_resvars !reset_expressions_counter)
-    (if node.n_name = "main" then "int" else "void")
-    node.n_name
-    (* could avoid newlines if they aren't used to seperate statements *)
-    (pp_varlist Arg) node.n_inputs
-    (pp_varlist Dec) node.n_local_vars
-    (pp_varlist Dec) node.n_outputs
-    (pp_equations node.n_name) node.n_equations
-    node.n_name
-    (pp_asnprevarlist node.n_name) node.n_inputs
-    (pp_asnprevarlist node.n_name) node.n_local_vars
-    (pp_asnprevarlist node.n_name) node.n_outputs
-    (pp_return node.n_name) node.n_outputs
+(** The following function defines the behaviour to have at the first
+  * execution of a node, namely:
+  *   - initialize the states of auxiliary nodes
+  *)
+let cp_init_aux_nodes fmt (node, h) =
+  let rec aux fmt (node, nst, i) =
+    match find_app_opt node.in_equations i with
+    | None -> () (** All auxiliary nodes have been initialized *)
+    | Some n ->
+      begin
+      Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\
+          \t\t\tstate->aux_states[%d] = calloc (1, sizeof (%s));\n\
+          \t\t}\n\
+          \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n\
+          \t\t((%s*)(state->aux_states[%d]))->is_reset = state->is_reset;\n"
+        aux (node, nst, i-1)
+        (i-1) (Format.asprintf "t_state_%s" n.n_name)
+        (Format.asprintf "t_state_%s" n.n_name) (i-1)
+        (Format.asprintf "t_state_%s" n.n_name) (i-1)
+      end
+  in
+  let nst = Hashtbl.find h node.in_name in
+  if nst.nt_count_app = 0
+    then ()
+    else begin
+      Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\
+          \tif (state->is_init) {\n%a\t}\n\n\n"
+        aux (node, nst, nst.nt_count_app)
+    end
 
-let rec pp_nodes fmt nodes =
+
+
+(** [cp_equations] prints the node equations. *)
+let cp_equations fmt (eqs, hloc, h) =
+  (** [main_block] is modified through some optimization passes, eg:
+    * - merge two CIf blocks using the same condition
+    * - replace [if (! c) { b1 } else { b2 }] by [if(c) { b2 } else { b1 }]
+    *
+    *  These passes are defined in [ctranslation.ml]
+      *)
+  let main_block: c_block =
+    List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in
+  let main_block = remove_ifnot main_block in
+  let main_block = merge_neighbour_ifs main_block in
+  Format.fprintf fmt "\t/*Main code :*/\n%a"
+    cp_block (main_block, hloc.nt_map)
+
+(** [cp_node] prints a single node *)
+let cp_node fmt (node, h) =
+  Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n"
+    cp_prototype (node, h)
+    cp_init_aux_nodes (node, h)
+    cp_equations (node.in_equations, Hashtbl.find h node.in_name, h)
+    cp_prevars (node, h)
+
+(** [cp_nodes] recursively prints all the nodes of a program. *)
+let rec cp_nodes fmt (nodes, h) =
   match nodes with
   | [] -> ()
   | node :: nodes ->
-    Format.fprintf fmt "%a\n%a" pp_node node pp_nodes nodes
+      Format.fprintf fmt "%a\n%a"
+        cp_node (node, h)
+        cp_nodes (nodes, h)
 
-let rec load_outputs_from_vars node_name n_outputs =
-  match n_outputs with
-  | [] -> ()
-  | BVar n_output :: n_outputs
-  | IVar n_output :: n_outputs
-  | RVar n_output :: n_outputs ->
-    (if (not (List.mem n_output !outputs)) then outputs := (node_name ^ "_" ^ n_output) :: !outputs;); load_outputs_from_vars node_name n_outputs
 
-let rec load_outputs_from_nodes nodes =
-  match nodes with
-  | [] -> ()
-  | node :: nodes ->
-          (if node.n_name <> "main" then (load_outputs_from_vars node.n_name (snd node.n_outputs)); Hashtbl.add nodes_outputs node.n_name (snd node.n_outputs)); load_outputs_from_nodes nodes
 
-let ast_to_c fmt prog =
-  load_outputs_from_nodes prog;
-  Format.fprintf fmt
-    (* could verify that uses, possibly indirectly (cf `->` implementation), a boolean in the ast before including `<stdbool.h>` *)
-    "#include <stdbool.h>\n\n%s\n\n%a"
-    ("float " ^ (String.concat ", " (List.map (fun output -> "output_" ^ output) !outputs)) ^ ";") pp_nodes prog
+(** [dump_var_locations] dumps the internal tables to map the program variable
+  * (after all the passes) to their location in the final C program. *)
+let dump_var_locations fmt (st: node_states) =
+  Format.fprintf fmt "Tables mapping the AST variables to the C variables:\n";
+  Hashtbl.iter
+    (fun n st ->
+      Format.fprintf fmt "  ∗ NODE: %s\n" n;
+    Hashtbl.iter
+    (fun (s, (ispre: bool)) ((arr: string), (idx: int)) ->
+      match ispre with
+      | true -> Format.fprintf fmt "    PRE Variable %s stored as %s[%d]\n" s arr idx
+      | false -> Format.fprintf fmt "        Variable %s stored as %s[%d]\n" s arr idx)
+    st.nt_map)
+    st
+
+
+
+(** main function that prints a C-code from a term of type [t_nodelist]. *)
+let ast_to_c fmt verbose debug prog =
+  verbose "Computation of the node_states";
+  let prog_st_types = make_state_types prog in
+  debug (Format.asprintf "%a" dump_var_locations prog_st_types);
+  let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
+  Format.fprintf fmt "%a\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
+    cp_includes (Config.c_includes)
+    cp_state_types prog_st_types
+    cp_state_frees (iprog, prog_st_types)
+    cp_nodes (iprog, prog_st_types)
+    cp_main_fn (prog, prog_st_types)
 

src/cast.ml

@@ -0,0 +1,27 @@
+open Intermediate_ast
+open Ast
+
+(** This file contains a small subset of the syntax of C required for the
+  * translation. *)
+
+(** A [c_block] represents a block in C. *)
+type c_block = c_expression list
+
+(** A [c_expresion] represents a C expression, which can need sequences and
+  * function calls. *)
+and c_expression =
+  | CAssign of c_var * c_value
+  | CSeq of c_expression * c_expression
+  | CIf of c_value * c_block * c_block
+  | CApplication of ident * int * c_var list * c_var list * node_states
+  | CReset of ident * int * c_value * c_block
+
+(** A value here is anything that can be inlined into a single C expression
+  * containing no function call, condition, ... *)
+and c_value =
+  | CVariable of c_var
+  | CMonOp of monop * c_value
+  | CBinOp of binop * c_value * c_value
+  | CComp of compop * c_value * c_value
+  | CConst of const
+

src/config.ml

@@ -3,3 +3,4 @@
     * variables. *)
 let maxvar = 100
 
+let c_includes = ["stdbool"; "stdlib"; "stdio"; "string"]

src/cprint.ml

@@ -0,0 +1,446 @@
+open Intermediate_utils
+open Intermediate_ast
+open Ast
+open Cast
+
+(** This file contains extremely simple functions printing C code. *)
+
+let rec cp_includes fmt = function
+  | [] -> ()
+  | h :: t ->
+      Format.fprintf fmt "#include <%s.h>\n%a" h cp_includes t
+
+let cp_node_state fmt (st: node_state) =
+  let print_if_any fmt (ty, nb, name): unit =
+    if nb = 0
+      then ()
+      else Format.fprintf fmt "\n\t%s %s[%d];" ty name nb
+  in
+  if st.nt_count_app = 0
+    then
+      Format.fprintf fmt "typedef struct {%a%a%a\n\
+            \tbool is_init, is_reset;\n\
+            } %s;\n\n"
+        print_if_any ("int", st.nt_nb_int, "ivars")
+        print_if_any ("bool", st.nt_nb_bool, "bvars")
+        print_if_any ("double", st.nt_nb_real, "rvars")
+        st.nt_name
+    else
+      Format.fprintf fmt "typedef struct {%a%a%a\n\
+            \tbool is_init, is_reset;\n\
+            \tvoid* aux_states[%d]; /* stores the states of auxiliary nodes */\n\
+            } %s;\n\n"
+        print_if_any ("int", st.nt_nb_int, "ivars")
+        print_if_any ("bool", st.nt_nb_bool, "bvars")
+        print_if_any ("double", st.nt_nb_real, "rvars")
+        st.nt_count_app st.nt_name
+
+let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit =
+  Hashtbl.iter (fun n nst ->
+    Format.fprintf fmt "/* Struct holding states of the node %s: */\n%a" n
+      cp_node_state nst) h
+
+
+
+(** [cp_state_frees] prints the required code to recursively free the node
+  * states. *)
+let cp_state_frees fmt (iprog, sts) =
+  let rec find_callee (i: int) (f: i_node) =
+    let rec aux_expr = function
+      | IETuple [] | IEVar   _ | IEConst _ -> None
+      | IEMonOp (_, e) -> aux_expr e
+      | IEWhen  (e, e')
+      | IEReset (e, e')
+      | IEComp  (_, e, e')
+      | IEBinOp (_, e, e') ->
+        begin
+          match aux_expr e with
+          | None -> aux_expr e'
+          | Some res -> Some res
+        end
+      | IETriOp (_, e, e', e'') ->
+        begin
+          match aux_expr e with
+          | None ->
+            (match aux_expr e' with
+            | None -> aux_expr e''
+            | Some res -> Some res)
+          | Some res -> Some res
+        end
+      | IETuple (h :: t) ->
+        begin
+          match aux_expr h with
+          | None -> aux_expr (IETuple t)
+          | Some res -> Some res
+        end
+      | IEApp   (j, n, e) ->
+          if i = j
+            then Some n.n_name
+            else aux_expr e
+    in
+    List.fold_right
+      (fun (_, expr) acc ->
+        match acc with
+        | Some _ -> acc
+        | None -> aux_expr expr)
+      f.in_equations None
+  in
+  let rec cp_free_aux fmt (i, caller_name) =
+    let idx = i - 1 in
+    match find_callee i (List.find (fun n -> n.in_name = caller_name) iprog)with
+    | None -> ()
+    | Some callee_name ->
+      let callee_st = Hashtbl.find sts callee_name in
+      if callee_st.nt_count_app > 0
+        then
+          Format.fprintf fmt "\tif (st->aux_states[%d]) {\n\
+            \t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n\
+            \t\tfree (st->aux_state[%d]);\n\t}\n%a"
+            idx callee_name callee_name idx
+            idx cp_free_aux (i+1, caller_name)
+        else Format.fprintf fmt "\tif (st->aux_states[%d])\n\
+            \t\tfree(st->aux_states[%d]);\n%a"
+            idx idx cp_free_aux (i+1, caller_name)
+  in
+  Hashtbl.iter
+    (fun node_name node_st ->
+      if node_st.nt_count_app = 0
+        then () (** Nothing to free for the node [node_name]. *)
+        else
+          Format.fprintf fmt "void free_state_%s(t_state_%s *);\n"
+            node_name node_name) sts;
+  Hashtbl.iter
+    (fun node_name node_st ->
+      if node_st.nt_count_app = 0
+        then () (** Nothing to free for the node [node_name]. *)
+        else
+          Format.fprintf fmt "void free_state_%s(t_state_%s *st)\n\
+            {\n\
+              %a\
+            }\n"
+            node_name node_name
+            cp_free_aux (1, node_name)) sts
+
+
+
+let cp_var' fmt = function
+  | CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx
+  | CVInput s -> Format.fprintf fmt "%s" s
+
+let cp_var fmt = function
+  | IVar s -> Format.fprintf fmt "int %s" s
+  | BVar s -> Format.fprintf fmt "bool %s" s
+  | RVar s -> Format.fprintf fmt "double %s" s
+
+let rec cp_varlist' fmt vl =
+  let print_if_any fmt = function
+    | [] -> ()
+    | _ :: _ -> Format.fprintf fmt ", "
+  in
+  match vl with
+  | [] -> ()
+  | v :: vl ->
+    Format.fprintf fmt "%a%a%a"
+    cp_var' v
+    print_if_any vl
+    cp_varlist' vl
+
+let rec cp_varlist fmt vl =
+  let print_if_any fmt = function
+    | [] -> ()
+    | _ :: _ -> Format.fprintf fmt ", "
+  in
+  match vl with
+  | [] -> ()
+  | v :: vl ->
+    Format.fprintf fmt "%a%a%a"
+    cp_var v
+    print_if_any vl
+    cp_varlist vl
+
+
+
+(** [cp_prototype] prints functions prototypes (without the «;»). It is only
+  * used to write the beginning of functions right now. If we later allow to
+  * use auxiliary nodes before their definition, it might be useful to declare
+  * all the prototypes at the beginning of the file (Cf. [cp_prototypes] below.
+  *)
+let cp_prototype fmt (node, h): unit =
+  match Hashtbl.find_opt h node.in_name with
+  | None -> failwith "This should not happened!"
+  | Some nst ->
+      begin
+        Format.fprintf fmt "void fn_%s (%s *state, %a)"
+          node.in_name
+          nst.nt_name
+          cp_varlist node.in_inputs
+      end
+
+let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) =
+  match nodes with
+  | [] -> ()
+  | node :: nodes ->
+      Format.fprintf fmt "%a;\n%a"
+        cp_prototype (node, h)
+        cp_prototypes (nodes, h)
+
+
+
+(** [cp_value] prints values, that is unary or binary operations which can be
+  * inlined in the final code without requiring many manipulations.
+  * It uses a lot of parenthesis at the moment. An improvement would be to
+  * remove useless ones at some point. *)
+let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) =
+  let string_of_binop = function
+    | BOp_add -> "+"
+    | BOp_sub -> "-"
+    | BOp_mul -> "*"
+    | BOp_div -> "/"
+    | BOp_mod -> "%"
+    | BOp_and -> "&&"
+    | BOp_or  -> "||"
+    | BOp_arrow -> failwith "string_of_binop undefined on (->)"
+  in
+  let string_of_compop = function
+    | COp_eq -> "=="
+    | COp_neq -> "!="
+    | COp_le -> "<="
+    | COp_lt -> "<"
+    | COp_ge -> ">="
+    | COp_gt -> ">"
+  in
+  match value with
+  | CVariable (CVInput s) -> Format.fprintf fmt "%s" s
+  | CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "state->%s[%d]" arr idx
+  | CConst (CInt i) -> Format.fprintf fmt "%d" i
+  | CConst (CBool b) -> Format.fprintf fmt "%s" (Bool.to_string b)
+  | CConst (CReal r) -> Format.fprintf fmt "%f" r
+  | CMonOp (MOp_not, v) -> Format.fprintf fmt "! (%a)" cp_value (v, hloc)
+  | CMonOp (MOp_minus, v) -> Format.fprintf fmt "- (%a)" cp_value (v, hloc)
+  | CMonOp (MOp_pre, (CVariable v)) ->
+      let varname = (match v with
+                    | CVStored (arr, idx) ->
+                      begin
+                        match find_varname hloc (arr, idx) with
+                        | None -> failwith "This varname should be defined."
+                        | Some (n, _) -> n
+                      end
+                    | CVInput n -> n) in
+      let (arr, idx) = Hashtbl.find hloc (varname, true) in
+      Format.fprintf fmt "state->%s[%d]" arr idx
+  | CBinOp (BOp_arrow, v, v') ->
+      Format.fprintf fmt "(state->is_init ? (%a) : (%a))"
+        cp_value (v, hloc) cp_value (v', hloc)
+  | CBinOp (op, v, v') ->
+      Format.fprintf fmt "(%a) %s (%a)"
+        cp_value (v, hloc) (string_of_binop op) cp_value (v', hloc)
+  | CComp (op, v, v') ->
+      Format.fprintf fmt "(%a) %s (%a)"
+        cp_value (v, hloc) (string_of_compop op) cp_value (v', hloc)
+  | CMonOp (MOp_pre, _) ->
+      failwith "The linearization should have removed this case."
+
+
+
+let prefix_ = ref "\t"
+
+(** The following function prints one transformed equation of the program into a
+  * set of instruction ending in assignments. *)
+let rec cp_block fmt (b, hloc) =
+  match b with
+  | [] -> ()
+  | e :: b ->
+    Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block (b, hloc)
+and cp_expression fmt (expr, hloc) =
+  let prefix = !prefix_ in
+  match expr with
+  | CAssign (CVStored (arr, idx), value) ->
+    begin
+      Format.fprintf fmt "%sstate->%s[%d] = %a;\n"
+        prefix arr idx cp_value (value, hloc)
+    end
+  | CAssign (CVInput _, _) -> failwith "never assign an input."
+  | CSeq (e, e') ->
+      Format.fprintf fmt "%a%a"
+        cp_expression (e, hloc)
+        cp_expression (e', hloc)
+  | CApplication (fn, nb, argl, destl, h) ->
+    begin
+      let aux_node_st = Hashtbl.find h fn in
+      let h_out = aux_node_st.nt_output_map in
+      Format.fprintf fmt "%sfn_%s(%s, %a);\n"
+        prefix fn
+        (Format.asprintf "state->aux_states[%d]" (nb-1))
+        cp_varlist' argl;
+      let _ = List.fold_left
+        (fun i var ->
+          match var with
+          | CVStored (arr, idx) ->
+            let (arr', idx') = Hashtbl.find h_out i in
+            Format.fprintf fmt "%sstate->%s[%d] = ((%s*)(state->aux_states[%d]))->%s[%d];\n"
+              prefix arr idx
+              aux_node_st.nt_name (nb-1)
+              arr' idx';
+            i+1
+          | CVInput _ -> failwith "Impossible!")
+        0 destl in ()
+    end
+  | CReset (node_name, i, v, b) ->
+    begin
+      Format.fprintf fmt "\tif (%a) {\n\
+        \t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\
+        \t\t((t_state_%s*)(state->aux_states[%d]))->is_reset = true;\n\
+        \t}\n\
+        %a\n"
+        cp_value (v, hloc)
+        node_name
+        (i - 1)
+        node_name
+        (i - 1)
+        cp_block (b, hloc)
+    end
+  | CIf (v, b1, []) ->
+      let p = prefix in
+      prefix_ := prefix^"\t";
+      Format.fprintf fmt "%sif (%a) {\n%a%s}\n"
+        p
+        cp_value (v, hloc)
+        cp_block (b1, hloc)
+        p;
+        prefix_ := p
+  | CIf (v, b1, b2) ->
+      let p = prefix in
+      prefix_ := prefix^"\t";
+      Format.fprintf fmt "%sif (%a) {\n%a%s} else {\n%a%s}\n"
+        p
+        cp_value (v, hloc)
+        cp_block (b1, hloc)
+        p
+        cp_block (b2, hloc)
+        p;
+      prefix_  := p
+
+
+
+(** [cp_main] prints  a main function to the C code if necessary:
+  * if there is a function [main] in the lustre program, it will generate a main
+  * function in the C code, otherwise it does not do anything.
+  *)
+let cp_main_fn fmt (prog, sts) =
+  let rec cp_array fmt (vl: t_var list): unit =
+    match vl with
+    | [] -> ()
+    | v :: vl ->
+      let typ, name =
+        match v with
+        | IVar s -> ("int", s)
+        | RVar s -> ("double", s)
+        | BVar s ->
+            Format.fprintf fmt "\tchar _char_of_%s;\n" s;
+            ("bool", s)
+        in
+      Format.fprintf fmt "\t%s %s;\n%a" typ name
+      cp_array vl
+  in
+  let rec cp_inputs fmt (f, l) =
+    match l with
+    | [] -> ()
+    | h :: t ->
+      (if f
+        then Format.fprintf fmt ", %s%a"
+        else Format.fprintf fmt "%s%a")
+        (Utils.name_of_var h)
+        cp_inputs (true, t)
+  in
+  let cp_scanf fmt vl =
+    let rec cp_scanf_str fmt (b, vl) =
+      match vl with
+      | [] -> ()
+      | h :: t ->
+        (if b
+          then Format.fprintf fmt " %s%a"
+          else Format.fprintf fmt "%s%a")
+        (match h with
+        | IVar _ -> "%d"
+        | BVar _ -> "%c"
+        | RVar _ -> "%lf")
+        cp_scanf_str (true, t)
+    in
+    let rec cp_scanf_args fmt vl =
+      match vl with
+      | [] -> ()
+      | RVar s :: vl | IVar s :: vl ->
+        Format.fprintf fmt ", &%s%a" s cp_scanf_args vl
+      | BVar s :: vl ->
+        Format.fprintf fmt ", &%s%a" (Format.sprintf "_char_of_%s" s)
+          cp_scanf_args  vl
+    in
+    Format.fprintf fmt "\"%a\"%a"
+      cp_scanf_str (false, vl)
+      cp_scanf_args vl
+  in
+  let cp_printf fmt vl =
+    let rec cp_printf_str fmt (b, vl) =
+      match vl with
+      | [] -> ()
+      | h :: t ->
+        (if b
+          then Format.fprintf fmt " %s%a"
+          else Format.fprintf fmt "%s%a")
+        (match h with
+        | IVar _ -> "%d"
+        | BVar _ -> "%c"
+        | RVar _ -> "%f")
+        cp_printf_str (true, t)
+    in
+    let rec cp_printf_arg fmt (h, i) =
+      match Hashtbl.find_opt h i with
+      | None -> ()
+      | Some (s, i) ->
+        Format.fprintf fmt ", state.%s[%d]%a"
+          s i cp_printf_arg (h, i+1)
+    in
+    Format.fprintf fmt "\"%a\\n\"%a"
+      cp_printf_str (false, vl)
+      cp_printf_arg ((Hashtbl.find sts "main").nt_output_map, 0)
+  in
+  let rec cp_char_to_bool fmt vl =
+    match vl with
+    | [] -> ()
+    | RVar _ :: vl | IVar _ :: vl -> Format.fprintf fmt "%a" cp_char_to_bool vl
+    | BVar s :: vl ->
+      Format.fprintf fmt "\t\t%s = (%s == 't') ? true : false;\n%a"
+        s (Format.sprintf "_char_of_%s" s)
+        cp_char_to_bool vl
+  in
+  let cp_free fmt () =
+    let main_st = Hashtbl.find  sts "main" in
+    if main_st.nt_count_app = 0
+      then ()
+      else Format.fprintf fmt "\tfree_state_main(&state);\n"
+  in
+  match List.find_opt (fun n -> n.n_name = "main") prog with
+  | None -> ()
+  | Some node ->
+    Format.fprintf fmt "int main (int argc, char **argv)\n\
+      {\n%a\n\
+        \tchar _buffer[1024];\n\
+        \tt_state_main state;\n\
+        \tstate.is_init = true;\n\
+        \tstate.is_reset = false;\n\
+        \twhile(true) {\n\
+          \t\tscanf(\"%%s\", _buffer);\n\
+          \t\tif(!strcmp(_buffer, \"exit\")) { break; }\n\
+          \t\tsscanf(_buffer, %a);\n%a\
+          \t\tfn_main(&state, %a);\n\
+          \t\tprintf(%a);\n\
+        \t}\n\
+        %a\treturn EXIT_SUCCESS;\n\
+      }\n"
+      cp_array (snd node.n_inputs)
+      cp_scanf (snd node.n_inputs)
+      cp_char_to_bool (snd node.n_inputs)
+      cp_inputs (false, snd node.n_inputs)
+      cp_printf (snd node.n_outputs)
+      cp_free ()
+

src/ctranslation.ml

@@ -0,0 +1,120 @@
+open Ast
+open Intermediate_ast
+open Cast
+
+let rec iexpression_to_cvalue e =
+  match e with
+  | IEVar   v -> CVariable v
+  | IEMonOp (op, e) -> CMonOp (op, iexpression_to_cvalue e)
+  | IEBinOp (op, e, e') ->
+      CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')
+  | IEComp  (op, e, e') ->
+      CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')
+  | IEConst c -> CConst c
+  | IEWhen  _
+  | IEReset _
+  | IETuple _
+  | IEApp   _
+  | IETriOp _ -> failwith "Should not happened."
+
+let rec equation_to_expression (node_st, node_sts, (vl, expr)) =
+  let hloc = node_st.nt_map in
+  let fetch_unique_var () =
+    match vl with
+    | [v] ->
+      begin
+        match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with
+        | None -> CVInput (Utils.name_of_var v)
+        | Some (arr, idx) -> CVStored (arr, idx)
+      end
+    | _ -> failwith "This should not happened."
+  in
+  match expr with
+  | IEVar   vsrc ->
+      CAssign (fetch_unique_var (), CVariable vsrc)
+  | IEMonOp (MOp_pre, IEVar v) ->
+      CAssign (fetch_unique_var (), CVariable v)
+  | IEConst c ->
+      CAssign (fetch_unique_var (), CConst c)
+  | IEMonOp (op, e) ->
+      CAssign (fetch_unique_var (),
+                CMonOp (op, iexpression_to_cvalue e))
+  | IEBinOp (op, e, e') ->
+      CAssign (fetch_unique_var (),
+                CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e'))
+  | IEComp  (op, e, e') ->
+      CAssign (fetch_unique_var (),
+                CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e'))
+      (** [CApp] below represents the i-th call to an aux node *)
+  | IEApp   (i, node, e) ->
+      (** e is a tuple of variables due to the linearization pass *)
+      let al: c_var list =
+        match e with
+        | IETuple l ->
+            List.map
+              (function
+                | IEVar v -> v
+                | _ -> failwith "should not happened due to the linearization pass."
+                ) l
+        | _ -> failwith "should not happened due to the linearization pass."
+        in
+      let vl =
+        List.map
+          (fun v ->
+            match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with
+            | Some (arr, idx) -> CVStored (arr, idx)
+            | None -> CVInput (Utils.name_of_var v))
+          vl
+        in
+      CApplication (node.n_name,i , al, vl, node_sts)
+  | IETuple _ -> failwith "linearization should have \
+                            transformed the tuples of the right members."
+  | IEWhen  (expr, cond) ->
+    begin
+      CIf (iexpression_to_cvalue cond,
+            [equation_to_expression (node_st, node_sts, (vl, expr))],
+            [])
+    end
+  | IETriOp (TOp_if, _, _, _) ->
+      failwith "A pass should have turned conditionnals into merges."
+  | IETriOp (TOp_merge, c, e, e') ->
+      CIf (iexpression_to_cvalue c,
+        [equation_to_expression (node_st, node_sts, (vl, e))],
+        [equation_to_expression (node_st, node_sts, (vl, e'))])
+  | IEReset (IEApp (i, node, b), c) -> CReset (node.n_name, i, iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, IEApp (i, node, b)))])
+  | IEReset _ -> failwith "A pass should have turned not function resets into function resets"
+
+
+
+let rec remove_ifnot = function
+  | [] -> []
+  | CIf (CMonOp (MOp_not, c), bh :: bt, b'h :: b't) :: block ->
+      (CIf (c, b'h :: b't, bh :: bt)) :: (remove_ifnot block )
+  | stmt :: block ->
+      stmt :: (remove_ifnot block)
+
+let rec merge_neighbour_ifs = function
+  | [] -> []
+  | [stmt] -> [stmt]
+  | CIf (c, e1, e2) :: CIf (c', e'1, e'2) :: b ->
+    begin
+      if c = c' then
+        merge_neighbour_ifs
+          (CIf (c,
+            merge_neighbour_ifs (e1 @ e'1),
+            merge_neighbour_ifs (e2 @ e'2)) :: b)
+      else if c = CMonOp (MOp_not, c') then
+        merge_neighbour_ifs
+          (CIf (c',
+            merge_neighbour_ifs (e2 @ e'1),
+            merge_neighbour_ifs (e1 @ e'2)) :: b)
+      else if c' = CMonOp (MOp_not, c) then
+        merge_neighbour_ifs
+          (CIf (c,
+            merge_neighbour_ifs (e1 @ e'2),
+            merge_neighbour_ifs (e2 @ e'1)) :: b)
+      else CIf (c, e1, e2) :: merge_neighbour_ifs (CIf (c', e'1, e'2) :: b)
+    end
+  | stmt :: stmt' :: b ->
+      stmt :: merge_neighbour_ifs (stmt' :: b)
+

src/intermediate_ast.ml

@@ -0,0 +1,75 @@
+open Ast
+
+(** A node state is translated into a struct. This struct has:
+  *   1. A name (t_state_<name of the node>)
+  *   2. A number of local and output variables of each type (int, real, bool)
+  *   3-5. mappings that maps
+  *     [(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 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
+  * variables in the point 2. above..
+  *
+  * It should be translated as follow in C:
+      typedef struct {
+          int ivars[nt_nb_int];  (or nothing if nt_nb_int = 0)
+          int bvars[nt_nb_bool]; (or nothing if nt_nb_bool = 0)
+          int rvars[nt_nb_real]; (or nothing if nt_nb_real = 0)
+          bool is_init;
+      } t_state_<node name>;
+  *)
+type node_state =
+  {
+    nt_name: string;
+    nt_nb_int : int;
+    nt_nb_real: int;
+    nt_nb_bool: int;
+    nt_map: (ident * bool, string * int) Hashtbl.t;
+    nt_output_map: (int, string * int) Hashtbl.t;
+    nt_prevars: t_var list;
+    nt_count_app: int;
+  }
+
+
+
+type c_var =
+  | CVStored of string * int
+  | CVInput of ident
+
+type i_expression =
+  | IEVar   of c_var
+  | IEMonOp of monop * i_expression
+  | IEBinOp of binop * i_expression * i_expression
+  | IETriOp of triop * i_expression * i_expression * i_expression
+  | IEComp  of compop * i_expression * i_expression
+  | IEWhen  of i_expression * i_expression
+  | IEReset of i_expression * i_expression
+  | IEConst of const
+  | IETuple of (i_expression list)
+      (** [CApp] below represents the n-th call to an aux node *)
+  | IEApp   of int * t_node * i_expression
+
+and i_varlist = t_var list
+
+and i_equation = i_varlist * i_expression
+
+and i_eqlist = i_equation list
+
+and i_node =
+  {
+    in_name : ident;
+    in_inputs: i_varlist;
+    in_outputs: i_varlist;
+    in_local_vars: i_varlist;
+    in_equations: i_eqlist;
+  }
+
+type i_nodelist = i_node list
+
+type node_states = (ident, node_state) Hashtbl.t
+

src/intermediate_utils.ml

@@ -0,0 +1,50 @@
+open Intermediate_ast
+
+let rec find_app_opt eqs i =
+  let rec find_app_expr_opt i = function
+    | IEVar _ | IEConst _ -> None
+    | IEMonOp (_, e) -> find_app_expr_opt i e
+    | IEReset (e, e') | IEWhen (e, e') | IEComp (_, e, e') | IEBinOp (_, e, e') ->
+        begin
+        match find_app_expr_opt i e with
+        | None -> find_app_expr_opt i e'
+        | Some n -> Some n
+        end
+    | IETriOp (_, e, e', e'') ->
+        begin
+        match find_app_expr_opt i e with
+        | None ->
+          begin
+          match find_app_expr_opt i e' with
+          | None -> find_app_expr_opt i e''
+          | Some n -> Some n
+          end
+        | Some n -> Some n
+        end
+    | IETuple l ->
+        List.fold_left
+          (fun acc e ->
+            match acc, find_app_expr_opt i e with
+            | Some n, _ -> Some n
+            | None, v -> v)
+          None l
+        (** [IEApp] below represents the n-th call to an aux node *)
+    | IEApp (j, n, e) ->
+        if i = j
+          then Some n
+          else find_app_expr_opt i e
+  in
+  match eqs with
+  | [] -> None
+  | (_, expr) :: eqs ->
+    match find_app_expr_opt i expr with
+    | None -> find_app_opt eqs i
+    | Some n -> Some n
+
+let find_varname h v =
+  Hashtbl.fold
+    (fun s e acc ->
+      match acc with
+      | None -> if e = v then Some s else None
+      | Some _ -> acc)
+    h None

src/lexer.mll

@@ -26,6 +26,7 @@
       ("merge", TO_merge);
       ("when", WHEN);
       ("reset", RESET);
+      ("every", EVERY);
       ("pre", MO_pre);
       ("true", CONST_BOOL(true));
       ("false", CONST_BOOL(false));

src/lustre_pp.ml

@@ -37,7 +37,7 @@ let rec pp_varlist fmt : t_varlist -> unit = function
       Format.fprintf fmt "%s: bool, %a" h pp_varlist (tl, h' :: l)
   | (TReal :: tl, RVar h :: h' :: l) ->
       Format.fprintf fmt "%s: real, %a" h pp_varlist (tl, h' :: l)
-  | _ -> raise (MyTypeError "This exception should not have beed be raised.")
+  | _ -> raise (MyTypeError "(1) This exception should not have beed be raised.")
 
 let pp_expression =
   let upd_prefix s = s ^ " |  " in
@@ -45,11 +45,14 @@ let pp_expression =
     let rec pp_expression_list prefix fmt exprs =
       match exprs with
       | ETuple([], []) -> ()
-      | ETuple (_ :: tt, expr :: exprs) ->
+      | ETuple (typs, expr :: exprs) ->
+          let typ_h, typ_t =
+            Utils.list_select (List.length (Utils.type_exp expr)) typs in
           Format.fprintf fmt "%a%a"
             (pp_expression_aux (prefix^" |> ")) expr
-            (pp_expression_list prefix) (ETuple (tt, exprs))
-      | _ -> raise (MyTypeError "This exception should not have been raised.")
+            (pp_expression_list prefix) (ETuple (typ_t, exprs))
+      | ETuple (_, []) -> failwith "An empty tuple has a type!"
+      | _ -> failwith "This exception should never occur."
     in
     match expression with
     | EWhen (_, e1, e2) ->
@@ -70,7 +73,7 @@ let pp_expression =
         begin match c with
         | CBool b -> Format.fprintf fmt "\t\t\t%s<%s : bool>\n" prefix (Bool.to_string b)
         | CInt i ->  Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i
-        | CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r
+        | CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: real>\n" prefix r
         end
     | EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v
     | EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v

src/main.ml

@@ -9,24 +9,46 @@ let print_debug d s =
 let print_verbose v s =
   if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else ()
 
-let exec_passes ast main_fn verbose debug passes f =
+
+
+(** [exec_passes] executes the passes on the parsed typed-AST.
+  * A pass should return [Some program] in case of a success, and [None]
+  * otherwise.
+  *
+  * The function [exec_passes] returns the optionnal program returned by the
+  * last pass.
+  *
+  * A pass should never be interrupted by an exception. Nevertheless, we make
+  * sure that no pass raise one. *)
+let exec_passes ast verbose debug passes f =
   let rec aux ast = function
     | [] ->  f ast
     | (n, p) :: passes ->
         verbose (Format.asprintf "Executing pass %s:\n" n);
-        match p verbose debug main_fn ast with
-        | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
-        | Some ast -> (
-        debug (Format.asprintf "Current AST (after %s):\n%a\n" n Pp.pp_ast ast);
-        aux ast passes)
+        try
+        begin
+          match p verbose debug ast with
+          | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
+          | Some ast -> (
+            debug
+              (Format.asprintf
+                "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
+            aux ast passes)
+        end with
+        | _ -> failwith ("The pass "^n^" should have caught me!")
   in
   aux ast passes
 
 
+
 let _ =
   (** Usage and argument parsing. *)
-  let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"; "clock_unification"] in
-  let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
+  let default_passes =
+    ["linearization_reset"; "remove_if";
+      "linearization_pre"; "linearization_tuples"; "linearization_app";
+      "ensure_assign_val";
+      "equations_ordering"] in
+  let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in
   let usage_msg =
     "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
       [-o output_file] [-m main_function] source_file\n" in
@@ -34,7 +56,6 @@ let _ =
   let debug = ref false in
   let ppast = ref false in
   let nopopt = ref false in
-  let simopt = ref false in
   let passes = ref [] in
   let source_file = ref "" in
   let testopt = ref false in
@@ -51,7 +72,6 @@ let _ =
       ("-debug", Arg.Set debug, "Output a lot of debug information");
       ("-p", Arg.String (fun s -> passes := s :: !passes),
             "Add a pass to the compilation process");
-      ("-sim", Arg.Set simopt, "Simulate the main node");
       ("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])");
     ] in
   Arg.parse speclist anon_fun usage_msg ;
@@ -59,17 +79,20 @@ let _ =
   if !passes = [] then passes := default_passes;
   let print_verbose = print_verbose !verbose in
   let print_debug = print_debug !debug in
-  let main_fn = "main" in
 
   (** Definition of the passes table *)
   let passes_table  = Hashtbl.create 100 in
   List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
     [
-      ("pre2vars", Passes.pre2vars);
-      ("chkvar_init_unicity", Passes.chkvar_init_unicity);
+      ("remove_if", Passes.pass_if_removal);
+      ("linearization_tuples", Passes.pass_linearization_tuples);
+      ("linearization_app", Passes.pass_linearization_app);
+      ("linearization_pre", Passes.pass_linearization_pre);
+      ("ensure_assign_val", Passes.pass_ensure_assignment_value);
+      ("linearization_reset", Passes.pass_linearization_reset);
+      ("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity);
       ("automata_translation", Passes.automata_translation_pass);
       ("automata_validity", Passes.check_automata_validity);
-      ("linearization", Passes.pass_linearization);
       ("equations_ordering", Passes.pass_eq_reordering);
       ("check_typing", Passes.pass_typing);
       ("clock_unification", Passes.clock_unification_pass);
@@ -93,7 +116,7 @@ let _ =
       begin
         close_in_noerr inchan;
         Format.printf "Syntax error at %a: %s\n\n"
-          Pp.pp_loc (l, !source_file) s;
+          Lustre_pp.pp_loc (l, !source_file) s;
         exit 0
       end
     | Parsing.Parse_error ->
@@ -101,11 +124,16 @@ let _ =
         close_in_noerr inchan;
         Parsing.(
         Format.printf "Syntax error at %a\n\n"
-          Pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
+          Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
         exit 0
       end
     in
 
+  (** Computes the list of passes to execute. If the [-test] flag is set, all
+    * sanity passes (ie. passes which do not modify the AST, but ensure its
+    * validity) are re-run after any other pass.
+    *
+    * Note: the sanity passes are always executed before any other. *)
   let passes =
     List.map
       (fun (pass: string) -> (pass,
@@ -121,26 +149,21 @@ let _ =
     in
 
   print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a"
-                Pp.pp_ast ast) ;
-  exec_passes ast main_fn print_verbose print_debug passes
-    begin
-    if !simopt
-      then Simulation.simulate main_fn
-      else
-        begin
-        if !ppast
-          then (Format.printf "%a" Pp.pp_ast)
-          else (
-            if !nopopt
-              then (fun _ -> ())
-              else
-              (
-                  let oc = open_out !output_file in
-                  let fmt = Format.make_formatter
-                        (Stdlib.output_substring oc)
-                        (fun () -> Stdlib.flush oc) in
-                  Format.fprintf fmt "%a" Ast_to_c.ast_to_c);
-              )
-        end
-    end
+                Lustre_pp.pp_ast ast) ;
+  exec_passes ast print_verbose print_debug passes
+  begin
+  if !ppast
+    then (Format.printf "%a" Lustre_pp.pp_ast)
+    else (
+      if !nopopt
+        then (fun _ -> ())
+        else
+        (
+            let oc = open_out !output_file in
+            let fmt = Format.make_formatter
+                  (Stdlib.output_substring oc)
+                  (fun () -> Stdlib.flush oc) in
+            Ast_to_c.ast_to_c fmt print_verbose print_debug);
+        )
+  end
 

src/parser.mly

@@ -63,7 +63,7 @@
 
   let make_binop_nonbool e1 e2 op error_msg =
     let t1 = type_exp e1 in let t2 = type_exp e2 in
-    (** e1 and e2 should be nunmbers here.*)
+    (** e1 and e2 should be numbers here.*)
     if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
       then
         begin
@@ -88,7 +88,7 @@
 
   let make_comp_nonbool e1 e2 op error_msg =
     let t1 = type_exp e1 in let t2 = type_exp e2 in
-    (** e1 and e2 should be nunmbers here.*)
+    (** e1 and e2 should be numbers here.*)
     if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
       then
         begin
@@ -144,6 +144,7 @@
 
 %token WHEN
 %token RESET
+%token EVERY 
 
 %token IF
 %token THEN
@@ -215,8 +216,8 @@ node_content:
               if vars_distinct e_in e_out (snd $10)
                 then (Hashtbl.add defined_nodes node_name n; n)
                 else raise (MyParsingError
-                            ("There is a conflict between the names of local, input \
-                            or output variables.",
+                            ("There is a conflict between the names of local,\
+                             input or output variables.",
                             current_location()))
           end};
 
@@ -312,33 +313,33 @@ expr:
   | MO_pre expr                        { EMonOp (type_exp $2, MOp_pre, $2) }
   | MINUS expr
       { monop_neg_condition $2 [TBool]
-          "You cannot take the opposite of a boolean expression."
+          "You cannot take the opposite of an expression that is not a number."
           (EMonOp (type_exp $2, MOp_minus, $2)) }
   | PLUS expr
       { monop_neg_condition $2 [TBool]
-          "You cannot take the plus of a boolean expression." $2 }
+          "(+) expects its argument to be a number." $2 }
   /* Binary operators */
   | expr PLUS expr
       { make_binop_nonbool $1 $3 BOp_add
-          "You should know better; addition hates booleans" }
+          "Addition expects both arguments to be (the same kind of) numbers." }
   | expr MINUS expr
       { make_binop_nonbool $1 $3 BOp_sub
-          "You should know better; subtraction hates booleans" }
+          "Substraction expects both arguments to be (the same kind of) numbers." }
   | expr BO_mul expr
       { make_binop_nonbool $1 $3 BOp_mul
-          "You should know better; multiplication hates booleans" }
+          "Multiplication expects both arguments to be (the same kind of) numbers." }
   | expr BO_div expr
       { make_binop_nonbool $1 $3 BOp_div
-          "You should know better; division hates booleans" }
+          "Division expects both arguments to be (the same kind of) numbers." }
   | expr BO_mod expr
       { make_binop_nonbool $1 $3 BOp_mod
-          "You should know better; modulo hates booleans" }
+          "Modulo expects both arguments to be numbers." }
   | expr BO_and expr
       { make_binop_bool $1 $3 BOp_and
-          "You should know better; conjunction hates numbers" }
+          "Conjunction expects both arguments to be booleans." }
   | expr BO_or expr
       { make_binop_bool $1 $3 BOp_or
-          "You should know better; disjunction hates numbers" }
+          "Disjunction expects both arguments to be booleans." }
   | expr BO_arrow expr
       { let e1 = $1 in let t1 = type_exp e1 in
         let e2 = $3 in let t2 = type_exp e2 in
@@ -381,9 +382,9 @@ expr:
          then EWhen (t1, e1, e2)
          else raise (MyParsingError ("The when does not type-check!",
                     current_location())) }
-  | expr RESET expr
-      { let e1 = $1 in let t1 = type_exp e1 in
-        let e2 = $3 in let t2 = type_exp e2 in
+  | RESET expr EVERY expr
+      { let e1 = $2 in let t1 = type_exp e1 in
+        let e2 = $4 in let t2 = type_exp e2 in
         if t2 = [TBool]
          then EReset (t1, e1, e2)
          else raise (MyParsingError ("The reset does not type-check!",

src/passes.ml

@@ -4,92 +4,544 @@ open Ast
 open Passes_utils
 open Utils
 
-let pre2vars verbose debug main_fn =
-  let rec all_pre expr =
-    match expr with
-    | EMonOp (ty, MOp_pre, expr) -> all_pre expr
-    | EMonOp _ -> false
-    | EVar _ -> true
-    | _ -> false
-  in
-  let rec pre_push expr : t_expression =
-    match expr with
-    | EVar _ -> EMonOp (type_exp expr, MOp_pre, expr)
-    | EConst _ -> expr (** pre(c) = c for any constant c *)
-    | EMonOp (ty, mop, expr) ->
-      begin
-        match mop with
-      | MOp_pre ->
-        if all_pre expr
-          then EMonOp (ty, mop, EMonOp (ty, mop, expr))
-          else pre_push (pre_push expr)
-      | _ -> EMonOp (ty, mop, pre_push expr)
-      end
-    | EBinOp (ty, bop, expr, expr') ->
-        let expr = pre_push expr in let expr' = pre_push expr' in
-        EBinOp (ty, bop, expr, expr')
-    | ETriOp (ty, top, expr, expr', expr'') ->
-        let expr = pre_push expr in let expr' = pre_push expr' in
-        let expr'' = pre_push expr'' in
-        ETriOp (ty, top, expr, expr', expr'')
-    | EComp  (ty, cop, expr, expr') ->
-        let expr = pre_push expr in let expr' = pre_push expr' in
-        EComp (ty, cop, expr, expr')
-    | EWhen  (ty, expr, expr') ->
-        let expr = pre_push expr in let expr' = pre_push expr' in
-        EWhen (ty, expr, expr')
-    | EReset (ty, expr, expr') ->
-        let expr = pre_push expr in let expr' = pre_push expr' in
-        EReset (ty, expr, expr')
-    | ETuple (ty, elist) ->
-        let elist =
-          List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in
-        ETuple (ty, elist)
-    | EApp   (ty, node, arg) ->
-        let arg = pre_push arg in
-        EApp (ty, node, arg)
-  in
-  let rec aux (expr: t_expression) =
-    match expr with
-    | EVar   _ -> expr
-    | EMonOp (ty, mop, expr) ->
-      begin
-        match mop with
-        | MOp_pre -> pre_push expr
-        | _ -> let expr = aux expr in EMonOp (ty, mop, expr)
-      end
-    | EBinOp (ty, bop, expr, expr') ->
-        let expr = aux expr in let expr' = aux expr' in
-        EBinOp (ty, bop, expr, expr')
-    | ETriOp (ty, top, expr, expr', expr'') ->
-        let expr = aux expr in let expr' = aux expr' in
-        let expr'' = aux expr'' in
-        ETriOp (ty, top, expr, expr', expr'')
-    | EComp  (ty, cop, expr, expr') ->
-        let expr = aux expr in let expr' = aux expr' in
-        EComp (ty, cop, expr, expr')
-    | EWhen  (ty, expr, expr') ->
-        let expr = aux expr in let expr' = aux expr' in
-        EWhen (ty, expr, expr')
-    | EReset (ty, expr, expr') ->
-        let expr = aux expr in let expr' = aux expr' in
-        EReset (ty, expr, expr')
-    | EConst (ty, c) -> EConst (ty, c)
-    | ETuple (ty, elist) ->
-        let elist =
-          List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in
-        ETuple (ty, elist)
-    | EApp   (ty, node, arg) ->
-        let arg = aux arg in
-        EApp (ty, node, arg)
-  in
-  expression_pass (somify aux)
 
-let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option =
+
+(** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones.
+  *
+  *     [x1, ..., xn = if c then e_l else e_r;]
+  * is replaced by:
+  *     (t1, ..., tn) = e_l;
+  *     (u1, ..., un) = e_r;
+  *     (v1, ..., vn) = (t1, ..., tn) when c;
+  *     (w1, ..., wn) = (u1, ..., un) when (not c);
+  *     (x1, ..., xn) = merge c (v1, ..., vn) (w1, ..., wn);
+  *
+  * Note that the first two equations (before the use of when) is required in
+  * order to have the expressions active at each step.
+  *)
+let pass_if_removal verbose debug =
+  let varcount = ref 0 in (** new variables are called «_ifrem[varcount]» *)
+  (** Makes a pattern (t_varlist) of fresh variables matching the type t *)
+  let make_patt t: t_varlist =
+    (t, List.fold_right
+      (fun ty acc ->
+        let nvar: ident = Format.sprintf "_ifrem%d" !varcount in
+        let nvar =
+          match ty with
+          | TInt -> IVar nvar
+          | TReal -> RVar nvar
+          | TBool -> BVar nvar
+          in
+        incr varcount;
+        nvar :: acc)
+      t [])
+  in
+  (** If a tuple contains a single element, it should not be. *)
+  let simplify_tuple t =
+    match t with
+    | ETuple (t, [elt]) -> elt
+    | _ -> t
+  in
+  (** For each equation, build a list of equations and a new list of local
+    * variables as well as an updated version of the original equation. *)
+  let rec aux_eq vars eq: t_eqlist * t_varlist * t_equation =
+    let patt, expr = eq in
+    match expr with
+    | EConst _ | EVar   _ -> [], vars, eq
+    | EMonOp (t, op, e) ->
+        let eqs, vars, (patt, e) = aux_eq vars (patt, e) in
+        eqs, vars, (patt, EMonOp (t, op, e))
+    | EBinOp (t, op, e, e') ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        let eqs', vars, (_, e') = aux_eq vars (patt, e') in
+        eqs @ eqs', vars, (patt, EBinOp (t, op, e, e'))
+    | ETriOp (t, TOp_if, e, e', e'') ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        let eqs', vars, (_, e') = aux_eq vars (patt, e') in
+        let eqs'', vars, (_, e'') = aux_eq vars (patt, e'') in
+        let patt_l: t_varlist = make_patt t in
+        let patt_r: t_varlist = make_patt t in
+        let patt_l_when: t_varlist = make_patt t in
+        let patt_r_when: t_varlist = make_patt t in
+        let expr_l: t_expression =
+          simplify_tuple
+          (ETuple
+            (fst patt_l, List.map (fun v -> EVar (type_var v, v)) (snd patt_l)))
+          in
+        let expr_r: t_expression =
+          simplify_tuple
+          (ETuple
+            (fst patt_r, List.map (fun v -> EVar (type_var v, v)) (snd patt_r)))
+          in
+        let expr_l_when: t_expression =
+          simplify_tuple
+          (ETuple
+            (fst patt_l_when, List.map (fun v -> EVar (type_var v, v))
+              (snd patt_l_when)))
+          in
+        let expr_r_when: t_expression =
+          simplify_tuple
+          (ETuple
+            (fst patt_r_when, List.map (fun v -> EVar (type_var v, v))
+              (snd patt_r_when)))
+          in
+        let equations: t_eqlist =
+          [(patt_l, e');
+            (patt_r, e'');
+            (patt_l_when,
+              EWhen (t, expr_l, e));
+            (patt_r_when,
+                EWhen (t,
+                  expr_r,
+                  (EMonOp (type_exp e, MOp_not, e))))]
+            @ eqs @ eqs' @eqs'' in
+        let vars: t_varlist =
+          varlist_concat
+            vars
+            (varlist_concat patt_l_when (varlist_concat patt_r_when
+            (varlist_concat patt_r patt_l))) in
+        let expr =
+          ETriOp (t, TOp_merge, e, expr_l_when, expr_r_when) in
+        equations, vars, (patt, expr)
+    | ETriOp (t, op, e, e', e'') ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        let eqs', vars, (_, e') = aux_eq vars (patt, e') in
+        let eqs'', vars, (_, e'') = aux_eq vars (patt, e'') in
+        eqs @ eqs' @ eqs'', vars, (patt, ETriOp (t, op, e, e', e''))
+    | EComp  (t, op, e, e') ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        let eqs', vars, (_, e') = aux_eq vars (patt, e') in
+        eqs @ eqs', vars, (patt, EComp (t, op, e, e'))
+    | EWhen  (t, e, e') ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        let eqs', vars, (_, e') = aux_eq vars (patt, e') in
+        eqs @ eqs', vars, (patt, EWhen (t, e, e'))
+    | EReset (t, e, e') ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        let eqs', vars, (_, e') = aux_eq vars (patt, e') in
+        eqs @ eqs', vars, (patt, EReset (t, e, e'))
+    | ETuple (t, l) ->
+        let eqs, vars, l, _ =
+          List.fold_right
+            (fun e (eqs, vars, l, remaining_patt) ->
+              let patt_l, patt_r = split_patt remaining_patt e in
+              let eqs', vars, (_, e) = aux_eq vars (patt_l, e) in
+              eqs' @ eqs, vars, (e :: l), patt_r)
+            l ([], vars, [], patt) in
+          eqs, vars, (patt, ETuple (t, l))
+    | EApp   (t, n, e) ->
+        let eqs, vars, (_, e) = aux_eq vars (patt, e) in
+        eqs, vars, (patt, EApp (t, n, e))
+  in
+  (** For each node, apply the previous function to all equations. *)
+  let aux_if_removal node =
+    let new_equations, new_locvars =
+      List.fold_left
+        (fun (eqs, vars) eq ->
+          let eqs', vars, eq = aux_eq vars eq in
+          eq :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_equations = new_equations; n_local_vars = new_locvars }
+  in
+  node_pass aux_if_removal
+
+
+(** [pass_linearization_reset] makes sure that all reset constructs in the program
+  * are applied to functions.
+  * This is required, since the reset construct is translated into resetting the
+  * function state in the final C code. *)
+let pass_linearization_reset verbose debug =
+  (** [node_lin] linearizes a single node. *)
+  let node_lin (node: t_node): t_node option =
+    (** [reset_aux_expression] takes an expression and returns:
+      *   - a list of additional equations
+      *   - the new list of local variables
+      *   - an updated version of the original expression *)
+    let rec reset_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
+      match expr with
+      | EVar _ -> [], vars, expr
+      | EMonOp (t, op, e) ->
+          let eqs, vars, e = reset_aux_expression vars e in
+          eqs, vars, EMonOp (t, op, e)
+      | EBinOp (t, op, e, e') ->
+          let eqs, vars, e = reset_aux_expression vars e in
+          let eqs', vars, e' = reset_aux_expression vars e' in
+          eqs @ eqs', vars, EBinOp (t, op, e, e')
+      | ETriOp (t, op, e, e', e'') ->
+          let eqs, vars, e = reset_aux_expression vars e in
+          let eqs', vars, e' = reset_aux_expression vars e' in
+          let eqs'', vars, e'' = reset_aux_expression vars e'' in
+          eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
+      | EComp  (t, op, e, e') ->
+          let eqs, vars, e = reset_aux_expression vars e in
+          let eqs', vars, e' = reset_aux_expression vars e' in
+          eqs @ eqs', vars, EComp (t, op, e, e')
+      | EWhen  (t, e, e') ->
+          let eqs, vars, e = reset_aux_expression vars e in
+          let eqs', vars, e' = reset_aux_expression vars e' in
+          eqs @ eqs', vars, EWhen (t, e, e')
+      | EReset (t, e, e') ->
+          (
+            match e with
+              | EApp (t_app, n_app, e_app) ->
+                let eqs, vars, e = reset_aux_expression vars e in
+                eqs, vars, EReset (t, e, e')
+              | e -> reset_aux_expression vars e
+          )
+      | EConst _ -> [], vars, expr
+      | ETuple (t, l) ->
+          let eqs, vars, l = List.fold_right
+            (fun e (eqs, vars, l) ->
+              let eqs', vars, e = reset_aux_expression vars e in
+              eqs' @ eqs, vars, (e :: l))
+            l ([], vars, []) in
+          eqs, vars, ETuple (t, l)
+      | EApp (t, n, e) ->
+          let eqs, vars, e = reset_aux_expression vars e in
+          eqs, vars, EApp (t, n, e)
+      in
+    (** Applies the previous function to the expressions of every equation. *)
+    let new_equations, new_locvars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = reset_aux_expression vars expr in
+          (patt, expr)::eqs' @ eqs, vars)
+        ([], node.n_local_vars)
+        node.n_equations
+      in
+    Some { node with n_local_vars = new_locvars; n_equations = new_equations }
+  in
+  node_pass node_lin
+
+
+(** [pass_linearization_pre] makes sure that all pre constructs in the program
+  * are applied to variables.
+  * This is required, since the pre construct is translated into a variable in
+  * the final C code. *)
+let pass_linearization_pre verbose debug =
+  (** [node_lin] linearizes a single node. *)
+  let node_lin (node: t_node): t_node option =
+    (** [pre_aux_expression] takes an expression and returns:
+      *   - a list of additional equations
+      *   - the new list of local variables
+      *   - an updated version of the original expression *)
+    let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
+      match expr with
+      | EVar _ -> [], vars, expr
+      | EMonOp (t, op, e) ->
+          begin
+          match op, e with
+          | MOp_pre, EVar _ ->
+              let eqs, vars, e = pre_aux_expression vars e in
+              eqs, vars, EMonOp (t, op, e)
+          | MOp_pre, _ ->
+              let eqs, vars, e = pre_aux_expression vars e in
+              let nvar: string = fresh_var_name vars 6 in
+              let nvar = match t with
+                          | [TInt]  -> IVar nvar
+                          | [TBool] -> BVar nvar
+                          | [TReal] -> RVar nvar
+                          | _ -> failwith "Should not happened." in
+              let neq_patt: t_varlist = (t, [nvar]) in
+              let neq_expr: t_expression = e in
+              let vars = varlist_concat (t, [nvar]) vars in
+              (neq_patt, neq_expr) :: eqs, vars, EMonOp (t, MOp_pre, EVar (t, nvar))
+          | _, _ ->
+              let eqs, vars, e = pre_aux_expression vars e in
+              eqs, vars, EMonOp (t, op, e)
+          end
+      | EBinOp (t, op, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EBinOp (t, op, e, e')
+      | ETriOp (t, op, e, e', e'') -> (** Do we always want a new var here? *)
+          let eqs, vars, e = pre_aux_expression vars e in
+          let nvar: string = fresh_var_name vars 6 in
+          let nvar: t_var = BVar nvar in
+          let neq_patt: t_varlist = ([TBool], [nvar]) in
+          let neq_expr: t_expression = e in
+          let vars = varlist_concat vars (neq_patt) in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          let eqs'', vars, e'' = pre_aux_expression vars e'' in
+          (neq_patt, neq_expr) :: eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
+      | EComp  (t, op, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EComp (t, op, e, e')
+      | EWhen  (t, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EWhen (t, e, e')
+      | EReset (t, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EReset (t, e, e')
+      | EConst _ -> [], vars, expr
+      | ETuple (t, l) ->
+          let eqs, vars, l = List.fold_right
+            (fun e (eqs, vars, l) ->
+              let eqs', vars, e = pre_aux_expression vars e in
+              eqs' @ eqs, vars, (e :: l))
+            l ([], vars, []) in
+          eqs, vars, ETuple (t, l)
+      | EApp   (t, n, e) ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          eqs, vars, EApp (t, n, e)
+      in
+    (** Applies the previous function to the expressions of every equation. *)
+    let new_equations, new_locvars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = pre_aux_expression vars expr in
+          (patt, expr)::eqs' @ eqs, vars)
+        ([], node.n_local_vars)
+        node.n_equations
+      in
+    Some { node with n_local_vars = new_locvars; n_equations = new_equations }
+  in
+  node_pass node_lin
+
+
+
+(** [pass_linearization_tuples] transforms expressions of the form
+  *     (x1, ..., xn) = (e1, ..., em);
+  * into:
+  *     p1 = e1;
+  *       ...
+  *     pm = em;
+  * where flatten (p1, ..., pm) = x1, ..., xn
+  *
+  * Idem for tuples hidden behind merges and when:
+  *     patt = (...) when c;
+  *     patt = merge c (...) (...);
+  *)
+let pass_linearization_tuples verbose debug ast =
+  (** [split_tuple] takes an equation and produces an equation list
+    * corresponding to the [pi = ei;] above. *)
+  let rec split_tuple (eq: t_equation): t_eqlist =
+    let patt, expr = eq in
+    match expr with
+    | ETuple (_, expr_h :: expr_t) ->
+      begin
+        let t_l = type_exp expr_h in
+        let patt_l, patt_r = list_select (List.length t_l) (snd patt) in
+        let t_r = List.flatten (List.map type_var patt_r) in
+        ((t_l, patt_l), expr_h) ::
+          split_tuple ((t_r, patt_r), ETuple (t_r, expr_t))
+      end
+    | ETuple (_, []) -> []
+    | _ -> [eq]
+  in
+  (** For each node, apply the previous function to all equations.
+    * It builds fake equations in order to take care of tuples behind
+    *  merge/when. *)
+  let aux_linearization_tuples node =
+    let new_equations = List.flatten
+     (List.map
+        (fun eq ->
+          match snd eq with
+          | ETuple _ -> split_tuple eq
+          | EWhen (t, ETuple (_, l), e') ->
+              List.map
+                (fun (patt, expr) -> (patt, EWhen (type_exp expr, expr, e')))
+                (split_tuple (fst eq, ETuple (t, l)))
+          | ETriOp (t, TOp_merge, c, ETuple (_, l), ETuple (_, l')) ->
+            begin
+              if List.length l <> List.length l'
+                || List.length t <> List.length (snd (fst eq))
+                then raise (PassExn "Error while merging tuples.")
+                else
+                  fst
+                    (List.fold_left2
+                    (fun (eqs, remaining_patt) el er ->
+                      let patt, remaining_patt = split_patt remaining_patt el in
+                      let t = type_exp el in
+                      (patt, ETriOp (t, TOp_merge, c, el, er))
+                        :: eqs, remaining_patt)
+                    ([], fst eq) l l')
+            end
+          | _ -> [eq])
+        node.n_equations) in
+    Some { node with n_equations = new_equations }
+  in
+  try node_pass aux_linearization_tuples ast with
+  | PassExn err -> (debug err; None)
+
+
+
+(** [pass_linearization_app] makes sure that any argument to a function is
+  * either a variable, or of the form [pre _] (which will be translated as a
+  * variable in the final C code. *)
+let pass_linearization_app verbose debug =
+  let applin_count = ref 0 in (* new variables are called «_applin[varcount]» *)
+  (** [aux_expr] recursively explores the AST in order to find applications, and
+    * adds the requires variables and equations. *)
+  let rec aux_expr vars expr: t_eqlist * t_varlist * t_expression =
+    match expr with
+    | EConst _ | EVar   _ -> [], vars, expr
+    | EMonOp (t, op, expr) ->
+        let eqs, vars, expr = aux_expr vars expr in
+        eqs, vars, EMonOp (t, op, expr)
+    | EBinOp (t, op, e, e') ->
+        let eqs, vars, e = aux_expr vars e in
+        let eqs', vars, e' = aux_expr vars e' in
+        eqs @ eqs', vars, EBinOp (t, op, e, e')
+    | ETriOp (t, op, e, e', e'') ->
+        let eqs, vars, e = aux_expr vars e in
+        let eqs', vars, e' = aux_expr vars e' in
+        let eqs'', vars, e'' = aux_expr vars e'' in
+        eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
+    | EComp  (t, op, e, e') ->
+        let eqs, vars, e = aux_expr vars e in
+        let eqs', vars, e' = aux_expr vars e' in
+        eqs @ eqs', vars, EComp (t, op, e, e')
+    | EWhen  (t, e, e') ->
+        let eqs, vars, e = aux_expr vars e in
+        let eqs', vars, e' = aux_expr vars e' in
+        eqs @ eqs', vars, EWhen (t, e, e')
+    | EReset (t, e, e') ->
+        let eqs, vars, e = aux_expr vars e in
+        let eqs', vars, e' = aux_expr vars e' in
+        eqs @ eqs', vars, EReset (t, e, e')
+    | ETuple (t, l) ->
+        let eqs, vars, l =
+          List.fold_right
+            (fun e (eqs, vars, l) ->
+              let eqs', vars, e = aux_expr vars e in
+              eqs' @ eqs, vars, (e :: l))
+            l ([], vars, []) in
+        eqs, vars, ETuple (t, l)
+    | EApp   (tout, n, ETuple (tin, l)) ->
+        let eqs, vars, l =
+          List.fold_right
+            (fun e (eqs, vars, l) ->
+              let eqs', vars, e = aux_expr vars e in
+              match e with
+              | EVar _ | EMonOp (_, MOp_pre, _) -> (** No need for a new var. *)
+                  eqs' @ eqs, vars, (e :: l)
+              | _ -> (** Need for a new var. *)
+                  let ty = match type_exp e with
+                           | [ty] -> ty
+                           | _ -> failwith "One should not provide
+                           tuples as arguments to an auxiliary node."
+                           in
+                  let nvar: string = Format.sprintf "_applin%d" !applin_count in
+                  incr applin_count;
+                  let nvar: t_var =
+                    match ty with
+                    | TBool -> BVar nvar
+                    | TInt -> IVar nvar
+                    | TReal -> RVar nvar
+                    in
+                  let neq_patt: t_varlist = ([ty], [nvar]) in
+                  let neq_expr: t_expression = e in
+                  let vars = varlist_concat neq_patt vars in
+                  (neq_patt, neq_expr)::eqs'@eqs, vars, EVar([ty], nvar) :: l)
+            l ([], vars, []) in
+        eqs, vars, EApp (tout, n, ETuple (tin, l))
+    | EApp _ -> failwith "Should not happened (parser)"
+  in
+  (** [aux_linearization_app] applies the previous function to every equation *)
+  let aux_linearization_app node =
+    let new_equations, new_locvars =
+      List.fold_left
+        (fun (eqs, vars) eq ->
+          let eqs', vars, expr = aux_expr vars (snd eq) in
+          (fst eq, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars)
+        node.n_equations
+      in
+    Some { node with n_local_vars = new_locvars; n_equations = new_equations }
+  in
+  node_pass aux_linearization_app
+
+
+
+let pass_ensure_assignment_value verbose debug =
+  let varcount = ref 0 in
+  let rec aux_expr should_be_value vars expr =
+    match expr with
+    | EConst _ | EVar   _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+        let eqs, vars, e = aux_expr true vars e in
+        eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+        let eqs, vars, e = aux_expr true vars e in
+        let eqs', vars, e' = aux_expr true vars e' in
+        eqs @ eqs', vars, EBinOp (t, op, e, e')
+    | ETriOp (t, op, e, e', e'') ->
+        let eqs, vars, e = aux_expr should_be_value vars e in
+        let eqs', vars, e' = aux_expr should_be_value vars e' in
+        let eqs'', vars, e'' = aux_expr should_be_value vars e'' in
+        eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
+    | EComp  (t, op, e, e') ->
+        let eqs, vars, e = aux_expr true vars e in
+        let eqs', vars, e' = aux_expr true vars e' in
+        eqs @ eqs', vars, EComp (t, op, e, e')
+    | EWhen  (t, e, e') ->
+        let eqs, vars, e = aux_expr should_be_value vars e in
+        let eqs', vars, e' = aux_expr should_be_value vars e' in
+        eqs @ eqs', vars, EWhen (t, e, e')
+    | EReset (t, e, e') ->
+        let eqs, vars, e = aux_expr should_be_value vars e in
+        let eqs', vars, e' = aux_expr should_be_value vars e' in
+        eqs @ eqs', vars, EReset (t, e, e')
+    | ETuple (t, l) ->
+        let eqs, vars, l =
+          List.fold_right
+            (fun e (eqs, vars, l) ->
+              let eqs', vars, e = aux_expr true vars e in
+              eqs' @ eqs, vars, e :: l)
+            l ([], vars, []) in
+        eqs, vars, ETuple (t, l)
+    | EApp   (t, n, e) ->
+        let eqs, vars, e = aux_expr true vars e in
+        if should_be_value
+          then
+            let nvar = Format.sprintf "_assignval%d" !varcount in
+            incr varcount;
+            let nvar: t_var =
+              match t with
+              | [TBool] -> BVar nvar
+              | [TReal] -> RVar nvar
+              | [TInt]  -> IVar nvar
+              | _ ->
+                failwith "An application occurring here should return a single element."
+              in
+            let neq_patt: t_varlist = (t, [nvar]) in
+            let neq_expr: t_expression = EApp (t, n, e) in
+            let vars = varlist_concat neq_patt vars in
+            (neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar)
+          else
+            eqs, vars, EApp (t, n, e)
+  in
+  let aux_ensure_assign_val node =
+    let new_equations, vars =
+      List.fold_left
+        (fun (eqs, vars) eq ->
+          let eqs', vars, expr = aux_expr false vars (snd eq) in
+          (fst eq, expr) :: eqs' @ eqs, vars
+          )
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_equations = new_equations; n_local_vars = vars }
+  in
+  node_pass aux_ensure_assign_val
+
+
+
+(** [sanity_pass_assignment_unicity] makes sure that there is at most one
+  * equation defining each variable (and that no equation tries to redefine an
+  * input).
+  *
+  * This is required, since the equations are not ordered in Lustre. *)
+let sanity_pass_assignment_unicity verbose debug : t_nodelist -> t_nodelist option =
+  (** For each node, test the node. *)
   let aux (node: t_node) : t_node option =
     let incr_aux h n =
       match Hashtbl.find_opt h n with
-      | None -> raise (PassExn "todo, should not happened.")
+      | None -> raise (PassExn "should not happened.")
       | Some num -> Hashtbl.replace h n (num + 1)
       in
     let incr_eq h (((_, patt), _): t_equation) =
@@ -171,114 +623,7 @@ let rec tpl debug ((pat, exp): t_equation) =
   | ETuple (_, []) -> []
   | _ -> [(pat, exp)]
 
-let pass_linearization verbose debug main_fn =
-  let node_lin (node: t_node): t_node option =
-    let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
-      match expr with
-      | EVar _ -> [], vars, expr
-      | EMonOp (t, op, e) ->
-          begin
-          match op with
-          | MOp_pre ->
-              let eqs, vars, e = pre_aux_expression vars e in
-              let nvar: string = fresh_var_name vars 6 in
-              let nvar = match t with
-                          | [TInt]  -> IVar nvar
-                          | [TBool] -> BVar nvar
-                          | [TReal] -> RVar nvar
-                          | _ -> failwith "Should not happened." in
-              let neq_patt: t_varlist = (t, [nvar]) in
-              let neq_expr: t_expression = e in
-              let vars = varlist_concat (t, [nvar]) vars in
-              (neq_patt, neq_expr) :: eqs, vars, EMonOp (t, MOp_pre, EVar (t, nvar))
-          | _ ->
-              let eqs, vars, e = pre_aux_expression vars e in
-              eqs, vars, EMonOp (t, op, e)
-          end
-      | EBinOp (t, op, e, e') ->
-          let eqs, vars, e = pre_aux_expression vars e in
-          let eqs', vars, e' = pre_aux_expression vars e' in
-          eqs @ eqs', vars, EBinOp (t, op, e, e')
-      | ETriOp (t, op, e, e', e'') ->
-          let eqs, vars, e = pre_aux_expression vars e in
-          let nvar: string = fresh_var_name vars 6 in
-          let nvar: t_var = BVar nvar in
-          let neq_patt: t_varlist = ([TBool], [nvar]) in
-          let neq_expr: t_expression = e in
-          let vars = varlist_concat vars (neq_patt) in
-          let eqs', vars, e' = pre_aux_expression vars e' in
-          let eqs'', vars, e'' = pre_aux_expression vars e'' in
-          (neq_patt, neq_expr) :: eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
-      | EComp  (t, op, e, e') ->
-          let eqs, vars, e = pre_aux_expression vars e in
-          let eqs', vars, e' = pre_aux_expression vars e' in
-          eqs @ eqs', vars, EComp (t, op, e, e')
-      | EWhen  (t, e, e') ->
-          let eqs, vars, e = pre_aux_expression vars e in
-          let eqs', vars, e' = pre_aux_expression vars e' in
-          eqs @ eqs', vars, EWhen (t, e, e')
-      | EReset (t, e, e') ->
-          let eqs, vars, e = pre_aux_expression vars e in
-          let eqs', vars, e' = pre_aux_expression vars e' in
-          eqs @ eqs', vars, EReset (t, e, e')
-      | EConst _ -> [], vars, expr
-      | ETuple (t, l) ->
-          let eqs, vars, l = List.fold_right
-            (fun e (eqs, vars, l) ->
-              let eqs', vars, e = pre_aux_expression vars e in
-              eqs' @ eqs, vars, (e :: l))
-            l ([], vars, []) in
-          eqs, vars, ETuple (t, l)
-      | EApp   (t, n, e) ->
-          let eqs, vars, e = pre_aux_expression vars e in
-          eqs, vars, EApp (t, n, e)
-      in
-    let rec pre_aux_equation (vars: t_varlist) ((patt, expr): t_equation) =
-      let eqs, vars, expr = pre_aux_expression vars expr in
-      (patt, expr)::eqs, vars
-      in
-    let rec tpl ((pat, exp): t_equation) =
-      match exp with
-      | ETuple (_, hexps :: texps) ->
-          debug "An ETuple has been recognized, inlining...";
-          let p1, p2 =
-            list_select
-              (List.length (type_exp hexps))
-              (snd pat) in
-          let t1 = List.flatten (List.map type_var p1) in
-          let t2 = List.flatten (List.map type_var p2) in
-          ((t1, p1), hexps)
-            :: (tpl ((t2, p2),
-                ETuple (List.flatten (List.map type_exp texps), texps)))
-      | ETuple (_, []) -> []
-      | _ -> [(pat, exp)]
-    in
-    let new_equations = List.flatten
-      (List.map
-        tpl
-        node.n_equations)
-      in
-    let new_equations, new_locvars =
-      List.fold_left
-        (fun (eqs, vars) eq ->
-          let es, vs = pre_aux_equation vars eq in
-          es @ eqs, vs)
-        ([], node.n_local_vars)
-        new_equations
-      in
-    Some
-      {
-        n_name = node.n_name;
-        n_inputs = node.n_inputs;
-        n_outputs = node.n_outputs;
-        n_local_vars = new_locvars;
-        n_equations = new_equations;
-        n_automata = node.n_automata;
-      }
-  in
-  node_pass node_lin
-
-let pass_eq_reordering verbose debug main_fn ast =
+let pass_eq_reordering verbose debug ast =
   let rec pick_equations init_vars eqs remaining_equations =
     match remaining_equations with
     | [] -> Some eqs
@@ -312,7 +657,7 @@ let pass_eq_reordering verbose debug main_fn ast =
   in
   node_pass node_eq_reorganising ast
 
-let pass_typing verbose debug main_fn ast =
+let pass_typing verbose debug ast =
   let htbl = Hashtbl.create (List.length ast) in
   let () = debug "[typing verification]" in
   let () = List.iter
@@ -382,7 +727,7 @@ let pass_typing verbose debug main_fn ast =
           else None
   in aux ast
 
-let check_automata_validity verbos debug main_fn = 
+let check_automata_validity verbos debug = 
   let check_automaton_branch_vars automaton = 
     let (init, states) = automaton in
     let left_side = Hashtbl.create 10 in
@@ -493,7 +838,7 @@ let automaton_translation debug automaton =
   in
 
   let rec translate_var s v explist ty = match explist with
-  | [] -> default_constant ty (* TODO *)
+  | [] -> default_constant ty
   | (state, exp)::q -> 
       ETriOp(Utils.type_exp exp, TOp_if,
         EComp([TBool], COp_eq, 
@@ -539,10 +884,10 @@ let automata_trans_pass debug (node:t_node) : t_node option=
       n_automata = []; (* not needed anymore *)
     }
 
-let automata_translation_pass verbose debug main_fn = 
+let automata_translation_pass verbose debug = 
   node_pass (automata_trans_pass debug)
 
-let clock_unification_pass verbose debug main_fn ast = 
+let clock_unification_pass verbose debug ast = 
 
   let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
     
@@ -601,8 +946,8 @@ let clock_unification_pass verbose debug main_fn ast =
       | _ -> failure ("Merge format")
     end
   | ETriOp(_, TOp_if, e1, e2, e3) ->
-      let c1 = compute_clock_exp e1
-      and c2 = compute_clock_exp e2
+      let (* Unused: c1 = compute_clock_exp e1
+      and*) c2 = compute_clock_exp e2
       and c3 = compute_clock_exp e3 in
       if c2 <> c3 then
         failure "If clocks"

src/simulation.ml

@@ -1,92 +0,0 @@
-open Ast
-
-type sim_var =
-  | SIVar of ident * (int option)
-  | SBVar of ident * (bool option)
-  | SRVar of ident * (real option)
-
-type sim_node_st =
-  {
-    node_outputs: sim_var list;
-    node_loc_vars: sim_var list;
-    node_inner_nodes: sim_node list;
-  }
-and sim_node_step_fn =
-  sim_node_st -> sim_var list -> (sim_var list * sim_node_st)
-and sim_node = sim_node_st * sim_node_step_fn
-
-let pp_sim fmt ((sn, _): sim_node) =
-  let rec aux fmt vars =
-    match vars with
-    | [] -> ()
-    | SIVar (s, None) :: t ->
-        Format.fprintf fmt "\t<%s : int> uninitialized yet.\n%a" s aux t
-    | SBVar (s, None) :: t ->
-        Format.fprintf fmt "\t<%s : bool> uninitialized yet.\n%a" s aux t
-    | SRVar (s, None) :: t ->
-        Format.fprintf fmt "\t<%s : real> uninitialized yet.\n%a" s aux t
-    | SIVar (s, Some i) :: t ->
-        Format.fprintf fmt "\t<%s : int> = %d\n%a" s i aux t
-    | SBVar (s, Some b) :: t ->
-        Format.fprintf fmt "\t<%s : bool> = %s\n%a" s (Bool.to_string b) aux t
-    | SRVar (s, Some r) :: t ->
-        Format.fprintf fmt "\t<%s : real> = %f\n%a" s r aux t
-  in
-  if sn.node_loc_vars <> []
-    then
-      Format.fprintf fmt "State of the simulated node:\n\
-                          \tOutput variables:\n%a
-                          \tLocal variables:\n%a"
-        aux sn.node_outputs
-        aux sn.node_loc_vars
-    else
-      Format.fprintf fmt "State of the simulated node:\n\
-                          \tOutput variables:\n%a
-                          \tThere are no local variables:\n"
-        aux sn.node_outputs
-
-
-exception MySimulationException of string
-
-let fetch_node (p: t_nodelist) (s: ident) : t_node =
-  match List.filter (fun n -> n.n_name = s) p with
-  | [e] -> e
-  | _ -> raise (MySimulationException (Format.asprintf "Node %s undefined." s))
-
-let fetch_var (l: sim_var list) (s: ident) =
-  match List.filter
-    (function
-      | SBVar (v, _) | SRVar (v, _) | SIVar (v, _) -> v = s) l with
-  | [v] -> v
-  | _ -> raise (MySimulationException
-                (Format.asprintf "Variable %s undefined." s))
-
-(** TODO! *)
-let make_sim (main_fn: ident) (p: t_nodelist): sim_node =
-  let main_n = fetch_node p main_fn in
-  let node_outputs =
-    List.map
-      (function
-        | IVar s -> SIVar (s, None)
-        | BVar s -> SBVar (s, None)
-        | RVar s -> SRVar (s, None))
-      (snd main_n.n_outputs) in
-  let node_loc_vars: sim_var list =
-    List.map
-      (function
-        | IVar s -> SIVar (s, None)
-        | BVar s -> SBVar (s, None)
-        | RVar s -> SRVar (s, None))
-      (snd main_n.n_local_vars) in
-  let node_inner_nodes = (* TODO! *) [] in
-  ({node_outputs = node_outputs;
-    node_loc_vars = node_loc_vars;
-    node_inner_nodes = node_inner_nodes; },
-    (fun s l -> (s.node_outputs, s)))
-
-
-
-let simulate main_fn ast =
-  let sim_ast = make_sim main_fn ast in
-  Format.printf "Initial state:\n%a" pp_sim sim_ast
-

src/test.node

@@ -1,21 +1,18 @@
-node diagonal_int (i: int) returns (o1, o2 : int);
+node id_int (i: int) returns (o: int);
 let
-	(o1, o2) = (i, i);
+  o = i -> i;
 tel
 
-node undiag_test (i: int) returns (o : bool);
-var l1, l2: int; l3: int;
+node aux (i, j: int) returns (o: int);
 let
-	l3 = (pre (1)) -> 0;
-	(l1, l2) = diagonal_int(i);
-	o = (not (not (l1 = l2))) and (l1 = l2) and true;
+  o = id_int(i) + id_int(j);
 tel
 
-node auto (i: int) returns (o : int);
-var x, y:int;
+node main (i: int) returns (a, b: int);
+var tmp: int;
 let
-	automaton
-	| Incr -> do (o,x) = (0 fby o + 1, 2); done
-	| Decr -> do (o,x) = diagonal_int(0 fby o); done
+  a = 1;
+  b = aux (i, a);
+  tmp = aux (a+b, i);
 tel
 

src/test2.node

@@ -1,13 +1,15 @@
-node main (i: int) returns (o1: int);
+node aux (i: int) returns (a, b: int);
 let
-    o1 = 10 -> pre (20 -> 30);
+  a = 1 -> pre i;
+  b = 2 * i -> (3 * pre i);
 tel
 
-node flipflop(i: int) returns (z: int);
-var x, y: int; c: bool;
+node n (i: int) returns (o1, o2: int);
+var u1, u2, t1, t2: int; c: bool;
 let
-	c = true fby (not c);
-	x = 1 on c;
-	y = 2 on (not c);
-	z = merge c x y;
+  c = true -> not pre c;
+  (t1, t2) = aux (i) when c;
+  (u1, u2) = aux (i) when (not c);
+  o1 = merge c t1 u1;
+  o2 = merge c t2 u2;
 tel

src/utils.ml

@@ -9,6 +9,13 @@ let rec list_select n = function
           let p1, p2 = list_select (n-1) t in
           h :: p1, p2
 
+let rec list_remove_duplicates l =
+  match l with
+  | [] -> []
+  | h :: t ->
+      let t = list_remove_duplicates t in
+      if List.mem h t then t else h :: t
+
 let rec list_map_option (f: 'a -> 'b option) (l: 'a list) : 'b list option =
   List.fold_right (fun elt acc ->
     match acc, f elt with
@@ -97,3 +104,9 @@ let rec vars_of_expr (expr: t_expression) : ident list =
 let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist =
   (fst l1 @ fst l2, snd l1 @ snd l2)
 
+let split_patt (patt: t_varlist) (e: t_expression): t_varlist * t_varlist =
+  let pl, pr = list_select (List.length (type_exp e)) (snd patt) in
+  let tl = List.flatten (List.map type_var pl) in
+  let tr = List.flatten (List.map type_var pr) in
+  (tl, pl), (tr, pr)
+

tests/test.node

@@ -0,0 +1,21 @@
+node diagonal_int (i: int) returns (o1, o2 : int);
+let
+	(o1, o2) = (i, i);
+tel
+
+node undiag_test (i: int) returns (o : bool);
+var l1, l2: int; l3: int;
+let
+	l3 = (pre (1)) -> 0;
+	(l1, l2) = diagonal_int(i);
+	o = (not (not (l1 = l2))) and (l1 = l2) and true;
+tel
+
+node auto (i: int) returns (o : int);
+var x, y:int;
+let
+	automaton
+	| Incr -> do (o,x) = (0 fby o + 1, 2); done
+	| Decr -> do (o,x) = diagonal_int(0 fby o); done
+tel
+

tests/test2.node

@@ -0,0 +1,11 @@
+node diagonal_int (i: int) returns (o1, o2 : int);
+let
+	(o1, o2) = (i, i);
+tel
+
+node main (i: int) returns (o1, o2, o3, o4: int);
+let
+    (o1, o2) = diagonal_int(i);
+    (o3, o4) = diagonal_int(o1);
+tel
+