[C] malloc->calloc + conditions merged in free_state_*

[messages] better comment and errors
[C] new lines in then output after each step
2022-12-20 16:52:59 +01:00 · 2022-12-20 16:41:21 +01:00 · 2022-12-20 16:38:29 +01:00 · 2022-12-20 16:34:31 +01:00 · 2022-12-20 16:29:35 +01:00 · 2022-12-20 15:46:31 +01:00
25 changed files with 3013 additions and 188 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,10 @@
 _build
 tags
+beamer.aux
+beamer.log
+beamer.nav
+beamer.out
+beamer.pdf
+beamer.snm
+beamer.toc
+texput.log
--- a/beamer/beamer.tex
+++ b/beamer/beamer.tex
@@ -0,0 +1,247 @@
+\documentclass{beamer}
+\usepackage{listings}
+\lstset{
+  basicstyle=\ttfamily,
+  columns=fullflexible,
+  frame=single,
+  breaklines=true,
+}
+\usepackage{tikz}
+
+\usetikzlibrary{positioning}
+\usetheme{Darmstadt}
+
+\begin{document}
+
+\title{Presentation of our Lustre-to-C compiler}
+\subtitle{github.com/Benjamin-Loison/Synchronous-reactive-systems}
+\date{16 December 2022}
+\author{Benjamin Loison, Arnaud Daby-Seesaram, Antoine Grimod}
+
+\frame{\titlepage}
+
+\section{Structure of the compiler}
+\begin{frame}{Main ideas}
+	\begin{figure}
+		\begin{tikzpicture}
+			\node (sf) {Source file};
+			\node[right =2cm of sf] (ast) {Typed AST};
+			\node[right =2cm of ast] (C) {C program};
+			\draw
+				(sf) edge[->] node[above] {parser} (ast)
+				(ast) edge[->] node[above] {compiler} (C);
+		\end{tikzpicture}
+		\caption{Structure of the compiler}
+	\end{figure}
+\end{frame}
+
+\begin{frame}{Testing}
+	\begin{block}{Passes}
+		The passes can be split into:
+		\begin{itemize}
+			\item those checking the program validity
+			\item those modifying the AST of the program
+		\end{itemize}
+	\end{block}
+\end{frame}
+
+\section{Typed AST}
+\subsection{First attempt using GADTs}
+\begin{frame}
+	\begin{block}{Main idea}
+		Using GADTs to represent nodes and expressions allows to ensure the
+		well-typedness of a program.
+	\end{block}
+	\begin{figure}
+		\centering
+		\includegraphics[width=.75\textwidth]{imgs/gadt.png}
+	\end{figure}
+\end{frame}
+\begin{frame}
+	\begin{block}{Pros of using GADTs}
+		\begin{itemize}
+			\item Any term of the GADT represents a well-typed program
+			\item Extending the language to support more types consists of adding
+				constructors to variables and constants
+			\item The types are easy to read and understand
+		\end{itemize}
+	\end {block}
+
+	\begin{block}{Cons of using GADTs}
+		\begin{itemize}
+			\item
+			They cannot be dynamically generated (hence it is impossible to
+			implement a parser that gives back a GADT)
+			\item
+			One should think about the isomorphism between
+			\texttt{a $\ast$ (b $\ast$ c)} and \texttt{(a $\ast$ b) $\ast$ c}.
+		\end{itemize}
+	\end{block}
+\end{frame}
+
+\subsection{Second attempt: using explicit types in the variables, expressions,
+\dots{} constructors}
+\begin{frame}
+	\begin{block}{Idea}
+		Explicitly collect typing information while parsing.
+	\end{block}
+	\begin{figure}
+		\centering
+		\includegraphics[width=.6\textwidth]{imgs/explicit_types.png}
+	\end{figure}
+\end{frame}
+
+\begin{frame}
+	\begin{block}{Pros of using explicit types}
+		\begin{itemize}
+			\item Programs can be built dynamically, hence a parser can be
+			written
+			\item While parsing, the parser has all the required information on
+			the sub-variables/nodes/expressions to check the well-typedness
+		\end{itemize}
+	\end{block}
+	\begin{block}{Cons of these definitions}
+		\begin{itemize}
+			\item The typing information on terms is very redundant.
+			\item The rejection of ill-typed programs depends on the correctness
+			of the parser
+		\end{itemize}
+	\end{block}
+\end{frame}
+
+\section{Passes}
+\begin{frame}{}
+    \begin{block}{Classification}
+        \begin{itemize}
+            \item node-passes: for all nodes, do \texttt{P: t\_node -> t\_node
+            option}
+            \pause
+            \item equation-passes: for all equations of all nodes, do
+            \texttt{P: t\_equation -> t\_equation option}
+            (the definition uses the node-passes constructor)
+            \pause
+            \item expression-passes: for all expression of all equations, do
+            \texttt{P: t\_expression -> t\_expression option}
+            (the definition uses the equation-passes constructor)
+        \end{itemize}
+    \end{block}
+\end{frame}
+\begin{frame}{Implemented Passes}
+	\begin{block}{Sanity checks}
+		\begin{itemize}
+			\item Check the well-typedness of a program
+            \pause
+			\item Check that there are no assignment conflicts in a programs
+            (node-pass)
+            \pause
+		\end{itemize}
+	\end{block}
+	\begin{block}{AST modification}
+		\begin{itemize}
+			\item Rewrite automata into \texttt{if-then-else} constructs
+            (node-pass)
+            \pause
+			\item Linearization of the equations:
+            \begin{itemize}
+                \item for all, \texttt{pre e} add a, intermediate variable
+                \item \texttt{v1, v2, v3 = f(i), e3;} is rewritten into
+                \texttt{v1, v2 = f(i); v3 = e3;}
+            \end{itemize}
+            (node-pass)
+            \pause
+			\item (no longer required) Push the \texttt{pre} to variables
+            (expression-pass)
+		\end{itemize}
+	\end{block}
+\end{frame}
+
+\begin{frame}[fragile]{Translation of automaton}
+	\only<1>{\lstinputlisting[language=ml, firstline=1, lastline=7]{code/example_automaton.lus}}
+	\only<2>{\lstinputlisting[language=ml, firstline=9, lastline=14]{code/example_automaton.lus}}
+\end{frame}
+\begin{frame}{Restriction on automaton}
+	The patterns that appears on the left of equations must be the
+	same in all branches
+
+	\only<2>{\lstinputlisting[language=ml, firstline=16, lastline=22]{code/example_automaton.lus}}
+\end{frame}
+
+\begin{frame}{Clock unification}
+
+	Derived from the rules provided in \emph{Clock-directed Modular Code Generation for Synchronous
+	Data-flow Languages}
+\end{frame}
+
+\section{Translation to C}
+\begin{frame}
+
+	\texttt{ast\_to\_c.ml} architecture similar to Arnaud's AST pretty-printer.
+
+	\pause
+
+	For instance, go from \texttt{counting.lus} to \texttt{counting.c}.
+
+    \pause
+
+	Use of three tricks, as our compiler only manages \texttt{bool}s, \texttt{int}s and \texttt{float}s:
+		\begin{enumerate}
+			\item \texttt{0} can be interpreted as a \texttt{bool}, an \texttt{int} and a \texttt{float}
+			\pause
+			\item A \texttt{float} correctly encode \texttt{bool}s (\texttt{true} and \texttt{false}) and \texttt{int}s (between $[-2^{24} + 1; 2^{24} + 1]$)
+			\pause
+			\item To run an assignment of \texttt{value} to \texttt{variable} within the condition of a \texttt{if} and also make the cases of the \texttt{if} depends on a condition \texttt{condition}, we can do \texttt{if(((variable = value) \&\& false) || condition)}\\
+			\pause
+			We can also use this trick to execute an assignment and \textit{return} a value \texttt{value\_to\_return} without using any \texttt{;}, by using \texttt{((variable = value) || true) ? value\_to\_return : 0} (thanks to the first trick)
+		\end{enumerate}
+\end{frame}
+
+\begin{frame}
+	\begin{itemize}
+		\item
+			\begin{itemize}
+				\item \texttt{pp\_varlist (Base | Arg | Dec)}
+				\item \texttt{pp\_retvarlist}
+				\item \texttt{pp\_prevarlist}
+				\item \texttt{pp\_asnprevarlist}
+			\end{itemize}
+		\pause
+		\item \texttt{when} implementation error: division by zero for instance, so used the first trick (\texttt{when\_merge.node})
+		\pause
+		\item \texttt{->}: use global variable \texttt{init\_\{NODE\_NAME\}}\\
+					\texttt{1 -> 2 -> 3} returns \texttt{0} on first run and only \texttt{3} on the following ones, correct? (\texttt{arrow.node})
+		\pause
+		\item \texttt{pre}
+		\pause
+		\item \texttt{reset}% (\texttt{reset})
+		\pause
+		\item Functions returning tuples thanks to Arnaud's linearization only have to deal with \texttt{(a0, a1, ..., an) = return\_tuple\_a0\_a1\_dots\_an(0)} (\texttt{function\_returning\_tuple.node})
+	\end{itemize}
+\end{frame}
+
+\section{Tests}
+\begin{frame}{Tests}
+    \begin{block}{testing methods}
+        We thought of three testing methods:
+        \begin{itemize}
+            \item manual testing of our functionalities
+            \item run the sanity-checks-passes after any AST-altering pass
+            \item simulation of the nodes (aborted)
+        \end{itemize}
+    \end{block}
+\end{frame}
+
+\section{Possible improvements}
+\begin{frame}{Improvements}
+    \begin{itemize}
+        \item Increase the expressivity of the accepted programs
+        \item Improve the complexity of the different passes
+        \begin{itemize}
+            \item Group neighbour passes of the same type (node-, expression or
+            equation-pass).
+        \end{itemize}
+        \item \dots{}
+    \end{itemize}
+\end{frame}
+
+\end{document}
+
--- a/beamer/code/example_automaton.lus
+++ b/beamer/code/example_automaton.lus
@@ -0,0 +1,22 @@
+node auto (i: int) returns (o : int);
+var x, y:int;
+let
+	automaton
+	| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
+	| Decr -> do (o,x) = diagonal_int(0 fby o); until o > 3 then Incr
+tel
+
+node auto (i: int) returns (o: int);
+var x, y: int;
+let
+	_s1 = 1 -> (if _s = 1 and o < 5 then 2 else if _s = 2 and o > then 1 else 1);
+	o, x = if _s = 1 then (0 fby o + 1, 2) else if _s = 2 then diagonal_int(0 fby 0) else (0, 0);
+tel
+
+node auto (i: int) returns (o : int);
+var x, y:int;
+let
+	automaton
+	| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
+	| Decr -> do (x,o) = diagonal_int(0 fby o); until o > 3 then Incr
+tel
--- a/beamer/imgs/explicit_types.png
+++ b/beamer/imgs/explicit_types.png
--- a/beamer/imgs/gadt.png
+++ b/beamer/imgs/gadt.png
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -35,10 +35,7 @@ type t_var =
  | IVar of ident
  | RVar of ident

-type full_ty =
-  | FTArr of full_ty * full_ty
-  | FTList of full_ty list
-  | FTBase of base_ty
+type full_ty = base_ty list

 type t_expression =
  | EVar   of full_ty * t_var
@@ -47,17 +44,23 @@ type t_expression =
  | ETriOp of full_ty * triop * t_expression * t_expression * t_expression
  | EComp  of full_ty * compop * t_expression * t_expression
  | EWhen  of full_ty * t_expression * t_expression
-  | EFby   of full_ty * t_expression * t_expression
+  | EReset of full_ty * t_expression * t_expression
  | EConst of full_ty * const
  | ETuple of full_ty * (t_expression list)
  | EApp   of full_ty * t_node * t_expression

 and t_varlist = full_ty * (t_var list)

-and t_equation = t_varlist * t_expression
+and t_equation = t_varlist * t_expression 

 and t_eqlist = t_equation list

+and t_state = | State of ident * t_eqlist * t_expression * ident
+
+and t_automaton = t_state * t_state list
+
+and t_autolist = t_automaton list
+
 and t_node =
  {
    n_name : ident;
@@ -65,8 +68,12 @@ and t_node =
    n_outputs: t_varlist;
    n_local_vars: t_varlist;
    n_equations: t_eqlist;
-    n_type : full_ty;
+    n_automata: t_autolist;
  }

 type t_nodelist = t_node list

+type t_ck = base_ck list
+and base_ck = 
+    | Base
+    | On of base_ck * t_expression
--- a/src/ast_to_c.ml
+++ b/src/ast_to_c.ml
@@ -0,0 +1,324 @@
+open Ast
+open Intermediate_ast
+open Intermediate_utils
+open Cprint
+open Cast
+open Utils
+open Ctranslation
+
+
+
+(** [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
+
+(** 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
+
+  (** [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
+
+  (** [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
+    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
+    List.fold_left
+      (fun i (_, expr) -> i + count_app_expr expr)
+      0 n.n_equations
+  in
+
+  (** [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
+
+        (** h_map gathers information from h_* maps above *)
+        let h_map =
+          Hashtbl.create (nb_int_vars + nb_bool_vars + nb_real_vars) in
+        let () =
+          Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("ivars", v)) h_int in
+        let () =
+          Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("bvars", v)) h_bool in
+        let () =
+          Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("rvars", v)) h_real in
+
+        let node_out_vars = snd node.n_outputs in
+        let h_out = Hashtbl.create (List.length node_out_vars) in
+        let () = List.iteri
+          (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
+
+
+
+(** 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 ->
+      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)
+
+
+
+(** 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
+
+
+
+(** [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"
+        cp_node (node, h)
+        cp_nodes (nodes, h)
+
+
+
+(** [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 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.printf "%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)
+
--- a/src/cast.ml
+++ b/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
+
--- a/src/config.ml
+++ b/src/config.ml
@@ -0,0 +1,6 @@
+(** Maximum Number of variables declared in a single node.
+    * This corresponds to the sum of the number of local, input and output
+    * variables. *)
+let maxvar = 100
+
+let c_includes = ["stdbool"; "stdlib"; "stdio"; "string"]
--- a/src/cprint.ml
+++ b/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 ()
+
--- a/src/ctranslation.ml
+++ b/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)
+
--- a/src/intermediate_ast.ml
+++ 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
+
--- a/src/intermediate_utils.ml
+++ b/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
--- a/src/lexer.mll
+++ b/src/lexer.mll
@@ -14,25 +14,29 @@
      ("returns", RETURNS);
      ("var", VAR);
      ("int", TYP(Ast.TInt));
+      ("real", TYP(Ast.TReal));
      ("bool", TYP(Ast.TBool));
-      ("<=", CMP_le);
-      (">=", CMP_ge);
      ("not", MO_not);
      ("mod", BO_mod);
-      ("&&", BO_and);
      ("and", BO_and);
-      ("||", BO_or);
      ("or", BO_or);
-      ("<>", CMP_neq);
      ("if", IF);
      ("then", THEN);
      ("else", ELSE);
      ("merge", TO_merge);
      ("when", WHEN);
-      ("fby", FBY);
+      ("reset", RESET);
+      ("every", EVERY);
      ("pre", MO_pre);
      ("true", CONST_BOOL(true));
      ("false", CONST_BOOL(false));
+      ("fby", BO_fby);
+      ("automaton", AUTOMAT);
+      ("match", MATCH);
+      ("with", WITH);
+      ("until", UNTIL);
+      ("do", DO);
+      ("done", DONE);
      ];
    fun s ->
      try Hashtbl.find h s with Not_found -> IDENT s
@@ -54,13 +58,22 @@ rule token = parse
  | ';'             { SEMICOL }
  | ':'             { COLON }
  | '<'             { CMP_lt }
+  | "<="            { CMP_le }
  | '>'             { CMP_gt }
+  | ">="            { CMP_ge }
+  | "<>"            { CMP_neq }
  | '+'             { PLUS }
  | '-'             { MINUS }
  | '*'             { BO_mul }
  | '/'             { BO_div }
  | '%'             { BO_mod }
  | "->"            { BO_arrow }
+  | '|'             { CASE }
+  | "--"            { read_single_line_comment lexbuf }
  | eof             { EOF }
-  | _               { raise (Lexing_error (Format.sprintf "Erruer à la vue de %s" (lexeme lexbuf)))}
+  | _               { raise (Lexing_error (Format.sprintf "Error when seeing %s" (lexeme lexbuf)))}

+and read_single_line_comment = parse
+  | '\n' { token lexbuf }
+  | eof { EOF }
+  | _ { read_single_line_comment lexbuf }
--- a/src/lustre_pp.ml
+++ b/src/lustre_pp.ml
@@ -1,45 +1,60 @@
 open Ast

-let pp_loc fmt (start, stop) =
-  Lexing.(
-    Format.fprintf fmt "%s: <l: %d, c: %d> -- <l: %d, c: %d>"
-      start.pos_fname
-      start.pos_lnum start.pos_cnum
-      stop.pos_lnum stop.pos_cnum)
+  let rec debug_type_pp fmt = function
+  | [] -> ()
+  | TInt  :: t -> Format.fprintf fmt "int %a" debug_type_pp t
+  | TBool :: t -> Format.fprintf fmt "bool %a" debug_type_pp t
+  | TReal :: t -> Format.fprintf fmt "real %a" debug_type_pp t
+
+let pp_loc fmt ((start, stop), file) =
+  let spos, epos = 
+    Lexing.(start.pos_cnum, stop.pos_cnum) in
+  let f = open_in file in
+  try
+    begin
+      let rec aux linenum curpos =
+        let line = input_line f in
+        let nextpos = curpos + (String.length line) + 1 in
+        if nextpos >= epos then
+          Format.fprintf fmt "<line %d: %s >" linenum line
+        else
+          aux (linenum + 1) nextpos
+        in
+      aux 1 0;
+      close_in f
+    end
+  with e ->
+    (close_in_noerr f; Format.fprintf fmt "???")

 let rec pp_varlist fmt : t_varlist -> unit = function
-  | (FTList [], []) -> ()
-  | (FTList (FTBase TInt :: _),  IVar h :: []) -> Format.fprintf fmt  "%s" h
-  | (FTList (FTBase TReal :: _), RVar h :: []) -> Format.fprintf fmt  "%s" h
-  | (FTList (FTBase TBool :: _), BVar h :: []) -> Format.fprintf fmt  "%s" h
-  | (FTList (FTBase TInt :: tl),  (IVar h) :: h' :: l) ->
-      Format.fprintf fmt  "%s, %a" h pp_varlist (FTList tl, (h' :: l))
-  | (FTList (FTBase TBool :: tl), (BVar h) :: h' :: l) ->
-      Format.fprintf fmt  "%s, %a" h pp_varlist (FTList tl, (h' :: l))
-  | (FTList (FTBase TReal :: tl), (RVar h) :: h' :: l) ->
-      Format.fprintf fmt  "%s, %a" h pp_varlist (FTList tl, (h' :: l))
-  | _ -> raise (MyTypeError "This exception should not have beed be raised.")
+  | ([], []) -> ()
+  | ([TInt] , IVar h :: []) -> Format.fprintf fmt "%s: int" h
+  | ([TReal], RVar h :: []) -> Format.fprintf fmt "%s: real" h
+  | ([TBool], BVar h :: []) -> Format.fprintf fmt "%s: bool" h
+  | (TInt :: tl,  IVar h :: h' :: l) ->
+      Format.fprintf fmt "%s: int, %a"  h pp_varlist (tl, h' :: l)
+  | (TBool :: tl, BVar h :: h' :: l) ->
+      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 "(1) This exception should not have beed be raised.")

 let pp_expression =
  let upd_prefix s = s ^ " |  " in
  let rec pp_expression_aux prefix fmt expression =
    let rec pp_expression_list prefix fmt exprs =
      match exprs with
-      | ETuple(FTList [], []) -> ()
-      | ETuple (FTList (_ :: tt), expr :: exprs) ->
+      | ETuple([], []) -> ()
+      | 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 (FTList 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
-    | EFby (_, e1, e2) ->
-        begin
-          Format.fprintf fmt "\t\t\t%sFBY\n%a\t\t\tFBY\n%a"
-            prefix
-            (pp_expression_aux (upd_prefix prefix)) e1
-            (pp_expression_aux (upd_prefix prefix)) e2
-        end
    | EWhen (_, e1, e2) ->
        begin
          Format.fprintf fmt "\t\t\t%sWHEN\n%a\t\t\tWHEN\n%a"
@@ -47,12 +62,18 @@ let pp_expression =
            (pp_expression_aux (upd_prefix prefix)) e1
            (pp_expression_aux (upd_prefix prefix)) e2
        end
+    | EReset (_, e1, e2) ->
+        begin
+          Format.fprintf fmt "\t\t\t%sRESET\n%a\t\t\tRESET\n%a"
+            prefix
+            (pp_expression_aux (upd_prefix prefix)) e1
+            (pp_expression_aux (upd_prefix prefix)) e2
+        end
    | EConst (_, c) ->
        begin match c with
-        | CBool true ->  Format.fprintf fmt "\t\t\t%s<true : bool>\n" prefix
-        | CBool false ->  Format.fprintf fmt "\t\t\t%s<false : bool>\n" prefix
-        | 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
+        | 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: 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
@@ -111,26 +132,46 @@ let pp_expression =
          (pp_expression_list prefix) args
    | ETuple _ ->
        Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix
-          (pp_expression_list prefix) expression;
+          (pp_expression_list prefix) expression
    in
  pp_expression_aux ""

 let rec pp_equations fmt: t_eqlist -> unit = function
  | [] -> ()
  | (patt, expr) :: eqs ->
-      Format.fprintf fmt "\t\t∗ left side: %a\n\t\t  right side:\n%a\n%a"
+      Format.fprintf fmt "\t\t∗ Equation of type : %a\n\t\t  left side: %a\n\
+                          \t\t  right side:\n%a\n\n%a"
+        debug_type_pp (Utils.type_exp expr)
        pp_varlist patt
        pp_expression expr
        pp_equations eqs

+let rec pp_automata fmt: t_automaton list -> unit = function
+  | [] -> ()
+  | (_, trans)::tail ->
+      Format.fprintf fmt "\t\t* Automaton : \n%a%a"
+      pp_translist trans
+      pp_automata tail
+
+and pp_translist fmt: t_state list -> unit = function
+  | [] -> ()
+  | State(name, eqs, cond, next)::q ->
+      Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \t\t\tthen %s\n%a"
+      name
+      pp_equations eqs
+      pp_expression cond
+      next
+      pp_translist q
+
 let pp_node fmt node =
-  Format.fprintf fmt "\t∗ Nom du nœud : %s\n\t  Inputs:\n%a\n\t  Outputs:\n%a\n\t\
-    \ \ Local variables:\n%a\n\t  Equations:\n%a\n"
+  Format.fprintf fmt "\t∗ Node name : %s\n\t  Inputs:\n%a\n\t  Outputs:\n%a\n\t\
+    \ \ Local variables:\n%a\n\t  Equations:\n%a\n\t  Automata:\n%a\n"
                 node.n_name
    pp_varlist node.n_inputs
    pp_varlist node.n_outputs
    pp_varlist node.n_local_vars
    pp_equations node.n_equations
+    pp_automata node.n_automata

 let rec pp_nodes fmt nodes =
  match nodes with
@@ -140,7 +181,7 @@ let rec pp_nodes fmt nodes =

 let pp_ast fmt prog =
  Format.fprintf fmt
-    "Le programme est composé de %d nœud(s), listés ci-dessous :\n%a"
+    "The program is made of %d node(s), listed below :\n%a"
    (List.length prog)
    pp_nodes prog

--- a/src/main.ml
+++ b/src/main.ml
@@ -9,37 +9,65 @@ 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 ()

-(** The following function should check whether the program is well-formed, by
-  * induction:
-  *  - for any applications of the form (n, arg1, ..., argn)
-  *    + n exists
-  *    + n waits n arguments
-  *    + arg1, ..., argn sont bien formés
-  *  - The expressions are well-typed
-  *  - The equations are well typed
-  *  - The output is set
-  *)
-let check_well_formedness (a: t_nodelist) = Some a
-let check_dependencies (a: t_nodelist) = Some a
-let simplify_prog (a: t_nodelist) = Some a

-let run verbose debug (passes: (t_nodelist -> t_nodelist option) list)
-  = verbose "kjlksjf"
+
+(** [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);
+        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 = ["check_form"; "check_dependencies"; "simplify_prog"] in
-  let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] [-o output_file] source_file" 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
  let verbose = ref false in
  let debug = ref false in
  let ppast = ref false in
+  let nopopt = ref false in
  let passes = ref [] in
  let source_file = ref "" in
+  let testopt = ref false in
  let output_file = ref "out.c" in
  let anon_fun filename = source_file := filename in
  let speclist =
    [
+      ("-test", Arg.Set testopt, "Runs the sanity passes not only at the \
+                                begining of the compilation, but also after \
+                                each pass altering the AST.");
      ("-ast", Arg.Set ppast, "Only print the AST of the input file");
+      ("-nop", Arg.Set nopopt, "Only computes the AST and execute the passes");
      ("-verbose", Arg.Set verbose, "Output some debug information");
      ("-debug", Arg.Set debug, "Output a lot of debug information");
      ("-p", Arg.String (fun s -> passes := s :: !passes),
@@ -50,37 +78,85 @@ let _ =
  if !source_file = "" then exit_error "No source file specified" else
  if !passes = [] then passes := default_passes;
  let print_verbose = print_verbose !verbose in
-  let print_debug = print_debug !verbose in
+  let print_debug = print_debug !debug in

  (** Definition of the passes table *)
-  let passes_table : (string,  t_nodelist -> t_nodelist option) Hashtbl.t = Hashtbl.create 100 in
+  let passes_table  = Hashtbl.create 100 in
  List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
    [
-      ("check_form", check_well_formedness);
-      ("check_dependencies", check_dependencies);
-      ("simplify_prog", simplify_prog);
+      ("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);
+      ("equations_ordering", Passes.pass_eq_reordering);
+      ("check_typing", Passes.pass_typing);
+      ("clock_unification", Passes.clock_unification_pass);
    ];

-  (** Main functionnalyty below *)
+  (** Main functionality below *)
  print_verbose "Parsing the source file...";
  let ast =
+    let inchan = open_in !source_file in
    try
      begin
-      let inchan = open_in !source_file in
+        (**let _ = Parsing.set_trace true in*)
      let res = Parser.main Lexer.token (Lexing.from_channel inchan) in
      close_in inchan; res
      end
-    with Lexer.Lexing_error s ->
-      exit_error (Format.sprintf "Code d'erreur:\n\t%s\n\n" s); exit 0 in
+    with
+    | Lexer.Lexing_error s ->
+        (close_in_noerr inchan;
+          exit_error (Format.sprintf "Error code:\n\t%s\n\n" s); exit 0)
+    | Utils.MyParsingError (s, l) ->
+      begin
+        close_in_noerr inchan;
+        Format.printf "Syntax error at %a: %s\n\n"
+          Lustre_pp.pp_loc (l, !source_file) s;
+        exit 0
+      end
+    | Parsing.Parse_error ->
+      begin
+        close_in_noerr inchan;
+        Parsing.(
+        Format.printf "Syntax error at %a\n\n"
+          Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
+        exit 0
+      end
+    in

-  if !ppast then Format.printf "%a" Pp.pp_ast ast
-  else
-    let passes = List.map (fun (pass: string) ->
-      match Hashtbl.find_opt passes_table pass with
-      | None ->
-        (exit_error (Format.sprintf "The pass %s does not exist." pass); exit 0)
-      | Some f ->
-        (print_debug ("The pass "^pass^" has been selected."); f)) !passes in
-    run print_verbose print_debug passes;
-    print_verbose "End of the program, exiting gracefully."
+  (** 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,
+        match Hashtbl.find_opt passes_table pass with
+        | None ->
+          (exit_error (Format.sprintf "The pass %s does not exist.\n" pass); exit 0)
+        | Some f ->
+          (print_debug ("The pass "^pass^" has been selected.\n"); f)))
+      (sanity_passes @
+        if !testopt
+          then List.flatten (List.map (fun p -> p :: sanity_passes) !passes)
+          else !passes)
+    in
+
+  print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a"
+                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 Ast_to_c.ast_to_c print_verbose print_debug)
+  end

--- a/src/parser.mly
+++ b/src/parser.mly
@@ -1,64 +1,109 @@
 %{
  open Ast
-  exception MyParsingError of string
+  open Utils

+  let bloop () = Format.printf "bloop\n"
  let current_location () = symbol_start_pos (), symbol_end_pos ()

-  let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create 100
+  let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar

-  let defined_vars : (ident, t_var) Hashtbl.t = Hashtbl.create 100
+  let defined_vars : (ident, t_var) Hashtbl.t = Hashtbl.create Config.maxvar

  let fetch_node (n: ident) =
    match Hashtbl.find_opt defined_nodes n with
    | None ->
        raise (MyParsingError
-                ("The node "^n^" does not exist."))
+                ("The node "^n^" does not exist.", current_location()))
    | Some node -> node

  let fetch_var (n: ident) : t_var =
    match Hashtbl.find_opt defined_vars n with
    | None ->
        raise (MyParsingError
-                ("The var "^n^" does not exist."))
+                ("The var "^n^" does not exist.", current_location()))
    | Some var -> var

-  let type_var (v: t_var) =
-      match v with
-      | IVar _ -> FTBase TInt
-      | BVar _ -> FTBase TBool
-      | RVar _ -> FTBase TReal
+  (*
+  let fetch_var_def (n: ident) : t_var =
+    match Hashtbl.find_opt defined_vars n with
+    | None ->
+        raise (MyParsingError
+                ("The var "^n^" does not exist.", current_location()))
+    | Some (var, true) ->
+        raise (MyParsingError
+                ("The variable "^n^" is defined for the second time.",
+                current_location()))
+    | Some (var, false) ->
+        (Hashtbl.replace defined_vars n (var, true) ; var)
+    *)

-  let type_exp : t_expression -> full_ty = function
-    | EVar   (full_ty , _) -> full_ty
-    | EMonOp (full_ty , _ , _) -> full_ty
-    | EBinOp (full_ty , _ , _ , _) -> full_ty
-    | ETriOp (full_ty , _ , _ , _ , _) -> full_ty
-    | EComp  (full_ty , _ , _ , _) -> full_ty
-    | EWhen  (full_ty , _ , _) -> full_ty
-    | EFby   (full_ty , _ , _) -> full_ty
-    | EConst (full_ty , _) -> full_ty
-    | ETuple (full_ty , _) -> full_ty
-    | EApp   (full_ty , _ , _) -> full_ty
-
-  let concat_varlist  (t1, e1) (t2, e2) =
-    (
-    match t1, t2 with
-    | FTList lt1, FTList lt2 -> (FTList (lt1 @ lt2), e1@e2)
-    | _ ->
-      raise (MyParsingError "This exception should not have been raised."))
+  let concat_varlist  (t1, e1) (t2, e2) = (t1 @ t2, e1 @ e2)

  let make_ident (v : t_var) : t_varlist =
    match v with
-    | IVar _ -> (FTList [FTBase TInt ], [v])
-    | BVar _ -> (FTList [FTBase TBool], [v])
-    | RVar _ -> (FTList [FTBase TReal], [v])
+    | IVar _ -> [TInt ], [v]
+    | BVar _ -> [TBool], [v]
+    | RVar _ -> [TReal], [v]

  let add_ident (v : t_var) (l: t_varlist) : t_varlist =
    match v, l with
-    | IVar _, (FTList tl, l) -> (FTList (FTBase TInt  :: tl), v :: l)
-    | BVar _, (FTList tl, l) -> (FTList (FTBase TBool :: tl), v :: l)
-    | RVar _, (FTList tl, l) -> (FTList (FTBase TReal :: tl), v :: l)
-    | _ -> raise (MyParsingError "This exception should not have been raised.")
+    | IVar _, (tl, l) -> ((TInt  :: tl), v :: l)
+    | BVar _, (tl, l) -> ((TBool :: tl), v :: l)
+    | RVar _, (tl, l) -> ((TReal :: tl), v :: l)
+
+  let monop_condition expr typ_constraint error_msg res =
+    if type_exp expr = typ_constraint
+      then res
+      else raise (MyParsingError (error_msg, current_location()))
+
+  let monop_neg_condition expr typ_constraint error_msg res =
+    if type_exp expr <> typ_constraint
+      then res
+      else raise (MyParsingError (error_msg, current_location()))
+
+  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 numbers here.*)
+    if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
+      then
+        begin
+        if t1 = t2
+          then EBinOp (t1, op, e1, e2)
+          else raise (MyParsingError (error_msg, current_location()))
+        end
+      else raise (MyParsingError (error_msg, current_location()))
+
+  let make_binop_bool e1 e2 op error_msg =
+    let t1 = type_exp e1 in let t2 = type_exp e2 in
+    if t1 = t2 && t1 = [TBool]
+      then EBinOp (t1, op, e1, e2)
+      else raise (MyParsingError (error_msg, current_location()))
+
+  let make_comp e1 e2 op error_msg =
+    let t1 = type_exp e1 in let t2 = type_exp e2 in
+    (** e1 and e2 should not be tuples *)
+    if t1 = t2 && List.length t1 = 1
+      then EComp ([TBool], op, e1, e2)
+      else raise (MyParsingError (error_msg, current_location()))
+
+  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 numbers here.*)
+    if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
+      then
+        begin
+        if t1 = t2
+          then EComp ([TBool], op, e1, e2)
+          else raise (MyParsingError (error_msg, current_location()))
+        end
+      else raise (MyParsingError (error_msg, current_location()))
+
+  let make_tertiary e1 e2 e3 op error_msg =
+    let t1 = type_exp e1 in let t2 = type_exp e2 in let t3 = type_exp e3 in
+    if t2 = t3 && t1 = [TBool]
+      then ETriOp (t2, op, e1, e2, e3)
+      else raise (MyParsingError (error_msg, current_location()))
+
 %}

 %token EOF
@@ -70,6 +115,7 @@
 %token COLON
 %token BOOL
 %token INT
+%token REAL
 %token LET
 %token TEL
 %token NODE
@@ -88,6 +134,7 @@
 %token BO_div
 %token BO_mod
 %token BO_arrow
+%token BO_fby
 %token CMP_le
 %token CMP_lt
 %token CMP_ge
@@ -96,16 +143,31 @@
 %token TO_merge

 %token WHEN
-%token FBY
+%token RESET
+%token EVERY 

 %token IF
 %token THEN
 %token ELSE

+%token AUTOMAT
+%token CASE
+%token MATCH
+%token WITH
+%token DO
+%token DONE
+%token UNTIL
+
 %token<int> CONST_INT
 %token<bool> CONST_BOOL
 %token<Ast.real> CONST_REAL

+%left MO_not
+%left MO_pre
+%left PLUS
+%left MINUS
+%left BO_and BO_or BO_mul BO_div BO_mod BO_arrow BO_fby TO_merge
+
 /* The Entry Point */
 %start main
 %type <Ast.t_nodelist> main
@@ -124,10 +186,11 @@ node:

 node_content:
  IDENT LPAREN in_params RPAREN
-  RETURNS LPAREN out_params RPAREN SEMICOL
+  RETURNS LPAREN out_params RPAREN OPTIONAL_SEMICOL
  local_params
-  LET equations TEL
+  LET node_body TEL OPTIONAL_SEMICOL
    { let node_name = $1 in
+      let (eqs, aut) = $12 in
      let (t_in, e_in) = $3 in
      let (t_out, e_out) = $7 in
      let n: t_node = 
@@ -135,19 +198,48 @@ node_content:
          n_inputs     = (t_in, e_in);
          n_outputs    = (t_out, e_out);
          n_local_vars = $10;
-          n_equations  = $12;
-          n_type = FTArr (t_in, t_out); } in
-      Hashtbl.add defined_nodes node_name n; n };
+          n_equations  = eqs;
+          n_automata = aut; } in
+      if List.length t_in = 0
+        then raise (MyParsingError
+                    (Format.asprintf "The node %s should have arguments."
+                      node_name,
+                    current_location()))
+        else
+          begin
+          if Hashtbl.find_opt defined_nodes node_name <> None
+            then raise (MyParsingError
+                        (Format.asprintf "The node %s is already defined."
+                                          node_name,
+                        current_location()))
+            else
+              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.",
+                            current_location()))
+          end};
+
+node_body:
+  | /* empty */ { ([], []) }
+  | equations node_body { let (eq, aut) = $2 in ($1@eq, aut) }
+  | automaton node_body { let (eq, aut) = $2 in (eq, $1::aut) }
+
+OPTIONAL_SEMICOL:
+  | /* empty */ {}
+  | SEMICOL {}
+;

 in_params:
-  | /* empty */ { (FTList [], []) }
+  | /* empty */ { ([], []) }
  | param_list  { $1 }
 ;

 out_params: param_list { $1 } ;

 local_params:
-  | /* empty */        { (FTList [], []) }
+  | /* empty */        { ([], []) }
  | VAR param_list_semicol { $2 }
 ;

@@ -164,17 +256,17 @@ param:
  ident_comma_list COLON TYP
    { let typ = $3 in
      let idents = $1 in
-      (
-      (FTList
-        (List.map
-          (fun t -> FTBase t) (Utils.list_repeat (List.length idents) typ)),
+      (list_repeat (List.length idents) typ,
      match typ with
      | TBool ->
-        List.map (fun s -> Hashtbl.add defined_vars s (BVar s); BVar s) idents
+        List.map (fun s ->
+          Hashtbl.add defined_vars s (BVar s); BVar s) idents
      | TReal ->
-        List.map (fun s -> Hashtbl.add defined_vars s (RVar s); RVar s) idents
+        List.map (fun s ->
+          Hashtbl.add defined_vars s (RVar s); RVar s) idents
      | TInt  ->
-        List.map (fun s -> Hashtbl.add defined_vars s (IVar s); IVar s) idents)) }
+        List.map (fun s ->
+          Hashtbl.add defined_vars s (IVar s); IVar s) idents) }
 ;

 ident_comma_list:
@@ -185,21 +277,24 @@ equations:
  | /* empty */ { [] }
  | equation SEMICOL equations
      {  $1 :: $3 }
+  | equation OPTIONAL_SEMICOL { [$1] }
 ;

 equation:
-  pattern EQUAL expr
+  | pattern EQUAL expr
    { let (t_patt, patt) = $1 in
-      let expr = $3 in
-      if type_exp expr = t_patt
+      let expr = $3 in let texpr = type_exp expr in
+      if t_patt = texpr
        then ((t_patt, patt), expr)
-        else raise (MyParsingError "The equation does not type check!") };
+        else (raise (MyParsingError ("The equation does not type check!",
+                    current_location()))) };
+automaton:
+  | AUTOMAT transition_list { (List.hd $2, $2)}
+;

 pattern:
  | IDENT
-    { let v = fetch_var $1 in
-    (FTList [type_var v], [v])
-    }
+    { let v = fetch_var $1 in (type_var v, [v]) }
  | LPAREN ident_comma_list_patt RPAREN { $2 };

 ident_comma_list_patt:
@@ -211,50 +306,110 @@ expr:
  | LPAREN expr RPAREN                 { $2 }
  | IDENT                              { let v  = fetch_var $1 in EVar (type_var v, v) }
  /* Unary operators */
-  | MO_not expr                        { EMonOp (type_exp $2, MOp_not, $2) }
+  | MO_not expr
+      { monop_condition $2 [TBool]
+          "You cannot negate a non-boolean expression."
+          (EMonOp (type_exp $2, MOp_not, $2)) }
  | MO_pre expr                        { EMonOp (type_exp $2, MOp_pre, $2) }
-  | MINUS expr                         { EMonOp (type_exp $2, MOp_minus, $2) }
-  | PLUS expr                          { $2 }
+  | MINUS expr
+      { monop_neg_condition $2 [TBool]
+          "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]
+          "(+) expects its argument to be a number." $2 }
  /* Binary operators */
-  | expr PLUS expr                     { EBinOp (type_exp $1, BOp_add, $1, $3) }
-  | expr MINUS expr                    { EBinOp (type_exp $1, BOp_sub, $1, $3) }
-  | expr BO_mul expr                   { EBinOp (type_exp $1, BOp_mul, $1, $3) }
-  | expr BO_div expr                   { EBinOp (type_exp $1, BOp_div, $1, $3) }
-  | expr BO_mod expr                   { EBinOp (type_exp $1, BOp_mod, $1, $3) }
-  | expr BO_and expr                   { EBinOp (type_exp $1, BOp_and, $1, $3) }
-  | expr BO_or expr                    { EBinOp (type_exp $1, BOp_or, $1, $3) }
-  | expr BO_arrow expr                 { EBinOp (type_exp $1, BOp_arrow, $1, $3) }
+  | expr PLUS expr
+      { make_binop_nonbool $1 $3 BOp_add
+          "Addition expects both arguments to be (the same kind of) numbers." }
+  | expr MINUS expr
+      { make_binop_nonbool $1 $3 BOp_sub
+          "Substraction expects both arguments to be (the same kind of) numbers." }
+  | expr BO_mul expr
+      { make_binop_nonbool $1 $3 BOp_mul
+          "Multiplication expects both arguments to be (the same kind of) numbers." }
+  | expr BO_div expr
+      { make_binop_nonbool $1 $3 BOp_div
+          "Division expects both arguments to be (the same kind of) numbers." }
+  | expr BO_mod expr
+      { make_binop_nonbool $1 $3 BOp_mod
+          "Modulo expects both arguments to be numbers." }
+  | expr BO_and expr
+      { make_binop_bool $1 $3 BOp_and
+          "Conjunction expects both arguments to be booleans." }
+  | expr BO_or expr
+      { make_binop_bool $1 $3 BOp_or
+          "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
+        if t1 = t2
+          then EBinOp (type_exp $1, BOp_arrow, $1, $3)
+          else raise (MyParsingError ("The -> does not type-check",
+                      current_location())) }
+  /* Binary operators, syntactic sugar */
+  | expr BO_fby expr
+      { (* e fby e' ==> e -> (pre e') *)
+        let e1 = $1 in let t1 = type_exp e1 in
+        let e2 = $3 in let t2 = type_exp e2 in
+        if t1 = t2
+          then EBinOp (t1, BOp_arrow, e1, (EMonOp (t1, MOp_pre, e2)))
+          else raise (MyParsingError ("The fby does not type-check!",
+                      current_location())) }
  /* Comparison operators */
-  | expr EQUAL expr                    { EComp (FTBase TBool, COp_eq, $1, $3) }
-  | expr CMP_neq expr                  { EComp (FTBase TBool, COp_neq, $1, $3) }
-  | expr CMP_le expr                   { EComp (FTBase TBool, COp_le, $1, $3) }
-  | expr CMP_lt expr                   { EComp (FTBase TBool, COp_lt, $1, $3) }
-  | expr CMP_ge expr                   { EComp (FTBase TBool, COp_ge, $1, $3) }
-  | expr CMP_gt expr                   { EComp (FTBase TBool, COp_gt, $1, $3) }
+  | expr EQUAL expr
+      { make_comp $1 $3 COp_eq "The equality does not type-check!" }
+  | expr CMP_neq expr
+      { make_comp $1 $3 COp_neq "The inquality does not type-check!" }
+  | expr CMP_le expr
+      { make_comp_nonbool $1 $3 COp_le "The comparison <= does not type-check!" }
+  | expr CMP_lt expr
+      { make_comp_nonbool $1 $3 COp_lt "The comparison < does not type-check!" }
+  | expr CMP_ge expr
+      { make_comp_nonbool $1 $3 COp_ge "The comparison >= does not type-check!" }
+  | expr CMP_gt expr
+      { make_comp_nonbool $1 $3 COp_gt "The comparison > does not type-check!" }
  /* Tertiary operators */
-  | IF expr THEN expr ELSE expr        { ETriOp (type_exp $4, TOp_if, $2, $4, $6) }
-  | TO_merge expr expr expr            { ETriOp (type_exp $4, TOp_merge, $2, $3, $4) }
+  | IF expr THEN expr ELSE expr
+      { make_tertiary $2 $4 $6 TOp_if "The if-then-else does not type-check!" }
+  | TO_merge expr expr expr
+      { make_tertiary $2 $3 $4 TOp_merge "The merge does not type-check!" }
  /* When is neither a binop (a * 'a -> 'a) or a comp ('a * 'a -> bool) */
-  | expr WHEN expr                     { EWhen (type_exp $1, $1, $3) }
-  | expr FBY expr                      { EFby (type_exp $1, $1, $3) }
+  | expr WHEN expr
+      { let e1 = $1 in let t1 = type_exp e1 in
+        let e2 = $3 in let t2 = type_exp e2 in
+        if t2 = [TBool]
+         then EWhen (t1, e1, e2)
+         else raise (MyParsingError ("The when does not type-check!",
+                    current_location())) }
+  | 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!",
+                    current_location())) }
  /* Constants */
-  | CONST_INT                          { EConst (FTBase TInt, CInt $1) }
-  | CONST_BOOL                         { EConst (FTBase TBool, CBool $1) }
-  | CONST_REAL                         { EConst (FTBase TReal, CReal $1) }
+  | CONST_INT                          { EConst ([TInt], CInt $1) }
+  | CONST_BOOL                         { EConst ([TBool], CBool $1) }
+  | CONST_REAL                         { EConst ([TReal], CReal $1) }
  /* Tuples */
  | LPAREN expr_comma_list RPAREN      { $2 }
  /* Applications */
+  | IDENT LPAREN RPAREN
+      { raise (MyParsingError ("An application should come with arguments!",
+                      current_location())) }
  | IDENT LPAREN expr_comma_list RPAREN
      { let name = $1 in
        let node = fetch_node name in
        let args = $3 in
-        match node.n_type with
-        | FTArr (tin, t) ->
-            if tin = type_exp args
-              then EApp (t, fetch_node name, args)
-              else raise (MyParsingError "The application does not type check!")
-        | _ -> raise (MyParsingError "This exception should not have been raised from the dead.")
+        if type_exp args = fst node.n_inputs
+          then EApp (fst node.n_outputs, fetch_node name, args)
+          else raise (MyParsingError ("The application does not type check!",
+                      current_location()))
         }
+
+  /* Automaton */
 ;

 expr_comma_list:
@@ -262,15 +417,16 @@ expr_comma_list:
      { let e = $1 in
        match e with
        | ETuple _ -> e
-        | _ -> ETuple (FTList [type_exp e],  [e]) }
+        | _ -> ETuple (type_exp e,  [e]) }
  | expr COMMA expr_comma_list
      { let e = $1 in
        let le = $3 in
        match e, le with
-        | ETuple (FTList l1, t), ETuple (FTList l2, t') -> ETuple (FTList (l1@l2), t @ t')
-        | _, ETuple (FTList lt, t') -> ETuple (FTList ((type_exp e)::lt), e :: t')
-        | _, _ -> raise (MyParsingError "This exception should not have been \
-                                          raised.") }
+        | ETuple (l1, t), ETuple (l2, t') -> ETuple (l1 @ l2, t @ t')
+        | _, ETuple (lt, t') -> ETuple (((type_exp e) @ lt), e :: t')
+        | _, _ -> raise (MyParsingError ("This exception should not have been \
+                                          raised.",
+                                          current_location())) }
 ;

 ident_comma_list:
@@ -278,3 +434,15 @@ ident_comma_list:
  | IDENT COMMA ident_comma_list { $1 :: $3 }
 ;

+transition:
+  | CASE IDENT BO_arrow DO equations DONE { 
+      State($2, $5, EConst([TBool], CBool(true)), $2) }
+  | CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
+      State($2, $5, $7, $9)}
+;
+
+transition_list:
+  | transition { [$1] }
+  | transition transition_list { $1 :: $2 }
+  | /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
+;
--- a/src/passes.ml
+++ b/src/passes.ml
@@ -0,0 +1,992 @@
+(** This file contains simplification passes for our Lustre-like AST *)
+
+open Ast
+open Passes_utils
+open Utils
+
+
+
+(** [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 "should not happened.")
+      | Some num -> Hashtbl.replace h n (num + 1)
+      in
+    let incr_eq h (((_, patt), _): t_equation) =
+      List.iter (fun v -> incr_aux h (name_of_var v)) patt
+      in
+    let rec incr_eqlist h = function
+      | [] -> ()
+      | eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs)
+      in
+    let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in
+    let incr_automata h ((_, states): t_automaton) =
+      let acc = Hashtbl.copy h in
+        List.iter
+          (fun st ->
+            let h_st = Hashtbl.copy h in
+            incr_branch h_st st;
+            Hashtbl.iter
+              (fun varname num' ->
+                match Hashtbl.find_opt acc varname with
+                | None -> failwith "no!"
+                | Some num -> Hashtbl.replace acc varname (Int.max num num')
+                ) h_st) states;
+          Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc
+        in
+    let check_now h : bool=
+      Hashtbl.fold
+        (fun varname num old_res ->
+          if num > 1
+            then (verbose (Format.asprintf "%s initialized twice!" varname); false)
+            else old_res) h true
+      in
+    (*let purge_initialized h =
+      Hashtbl.iter
+        (fun varname num ->
+          if num > 0
+            then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname)
+            else ()) h
+      in*)
+    let h = Hashtbl.create Config.maxvar in
+    let add_var n v =
+      match v with
+      | IVar s -> Hashtbl.add h s n
+      | BVar s -> Hashtbl.add h s n
+      | RVar s -> Hashtbl.add h s n
+    in
+    let add_var_in = add_var 1 in
+    let add_var_loc = add_var 0 in
+    List.iter add_var_loc (snd node.n_outputs);
+    List.iter add_var_loc (snd node.n_local_vars);
+    List.iter add_var_in (snd node.n_inputs);
+    (** Usual Equations *)
+    incr_eqlist h node.n_equations;
+    if check_now h = false
+      then None
+      else
+        begin
+          List.iter (* 0. *) (incr_automata h) node.n_automata;
+          if check_now h
+            then Some node
+            else None
+        end
+    (** never purge -> failwith never executed! purge_initialized h; *)
+  in
+  node_pass aux
+
+let rec tpl debug ((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 debug ((t2, p2),
+            ETuple (List.flatten (List.map type_exp texps), texps)))
+  | ETuple (_, []) -> []
+  | _ -> [(pat, exp)]
+
+let pass_eq_reordering verbose debug ast =
+  let rec pick_equations init_vars eqs remaining_equations =
+    match remaining_equations with
+    | [] -> Some eqs
+    | _ ->
+      begin
+        match List.filter
+                (fun (patt, expr) ->
+                  List.for_all
+                    (fun v -> List.mem v init_vars)
+                    (vars_of_expr expr))
+                remaining_equations with
+        | [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.")
+        | h :: t ->
+            let init_vars =
+              List.fold_left
+                (fun acc vs ->
+                  acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in
+            pick_equations init_vars (eqs@(h :: t))
+              (List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
+      end
+    in
+  let node_eq_reorganising  (node: t_node): t_node option =
+    let init_vars = List.map name_of_var (snd node.n_inputs) in
+    try
+      begin
+      match pick_equations init_vars [] node.n_equations with
+      | None -> None
+      | Some eqs -> Some { node with n_equations = eqs }
+      end
+    with PassExn err -> (verbose err; None)
+  in
+  node_pass node_eq_reorganising ast
+
+let pass_typing verbose debug ast =
+  let htbl = Hashtbl.create (List.length ast) in
+  let () = debug "[typing verification]" in
+  let () = List.iter
+    (fun n -> Hashtbl.add htbl n.n_name (fst n.n_inputs, fst n.n_outputs))
+    ast in
+  let rec check_varlist vl =
+    let t = fst vl in
+    let l = snd vl in
+    match t, l with
+    | [], [] -> true
+    | TInt  :: t, IVar _ :: l -> check_varlist (t, l)
+    | TBool :: t, BVar _ :: l -> check_varlist (t, l)
+    | TReal :: t, RVar _ :: l -> check_varlist (t, l)
+    | _, _ -> false
+    in
+  let rec check_expr vl = function
+    | EVar   (t, v) -> t = type_var v
+    | EMonOp (t, _, e) -> check_expr vl e && type_exp e = t
+    | EBinOp (t, _, e, e') -> check_expr vl e && check_expr vl e'
+                              && t = type_exp e && t = type_exp e'
+    | ETriOp (t, _, c, e, e') ->
+        check_expr vl e && check_expr vl e' && check_expr vl c
+        && type_exp c = [TBool] && type_exp e = t && type_exp e' = t
+    | EComp  (t, _, e, e') ->
+        check_expr vl e && check_expr vl e' && t = [TBool]
+    | EWhen  (t, e, e') ->
+        check_expr vl e && check_expr vl e'
+        && t = type_exp e && [TBool] = type_exp e'
+    | EReset (t, e, e') ->
+        check_expr vl e && check_expr vl e' && t = type_exp e && type_exp e' = [TBool]
+    | EConst (t, c) -> type_const c = t
+    | ETuple (t, l) ->
+        List.for_all (check_expr vl) l
+        && t = List.flatten (List.map type_exp l)
+    | EApp   (t, n, e) ->
+        check_expr vl e && t = (fst n.n_outputs) && type_exp e = (fst n.n_inputs)
+  in
+  let check_equation vl ((peq, eeq): t_equation) =
+    if check_varlist peq
+      then
+        if check_expr vl eeq
+          then fst peq = type_exp eeq
+          else false
+      else false
+  in
+  let rec check_equations vl = function
+    | [] -> true
+    | eq :: eqs ->
+        if check_equation vl eq
+          then check_equations vl eqs
+          else false
+  in
+  let check_one_node node =
+    check_varlist (node.n_inputs)
+    && check_varlist (node.n_outputs)
+    && check_varlist (node.n_local_vars)
+    && check_equations
+        (varlist_concat node.n_inputs
+          (varlist_concat node.n_outputs node.n_local_vars))
+        node.n_equations
+    in
+  let rec aux = function
+    | [] -> Some ast
+    | n :: nodes ->
+        if check_one_node n
+          then aux nodes
+          else None
+  in aux ast
+
+let check_automata_validity verbos debug = 
+  let check_automaton_branch_vars automaton = 
+    let (init, states) = automaton in
+    let left_side = Hashtbl.create 10 in
+
+    let rec init_left_side eqlist = match eqlist with
+    | [] -> ()
+    | (varlist, exp)::q -> 
+        begin
+          Hashtbl.add left_side varlist true;
+          init_left_side q;
+        end
+    in
+    let check_state s = match s with
+    | State(name, eqs, cond, next) ->
+        List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs
+    in
+    begin
+    match init with | State(name, eqs, cond, next) -> init_left_side eqs;
+    let validity = List.for_all (fun s -> (check_state s)) states in
+    if not validity then
+      raise (PassExn "Automaton branch has different variables assignment in different branches")
+    end
+  in
+  let aux node = 
+    List.iter check_automaton_branch_vars node.n_automata;
+    Some node
+  in
+  node_pass aux
+
+let automaton_translation debug automaton = 
+  let gathered = Hashtbl.create 10 in
+  let state_to_int = Hashtbl.create 10 in
+  let add_to_table var exp state = 
+    if Hashtbl.mem gathered var then
+      let res = Hashtbl.find gathered var in
+      Hashtbl.replace gathered var ((state, exp)::res);
+    else
+      Hashtbl.replace gathered var ([(state, exp)])
+  in
+  let rec init_state_translation states c = match states with
+  | [] -> ()
+  | State(name, _, _, _)::q -> 
+      Hashtbl.replace state_to_int name c; (init_state_translation q (c+1))
+  in
+
+  let rec find_state name = 
+    match Hashtbl.find_opt state_to_int name with
+    | None -> failwith "Unknown state in automaton"
+    | Some v -> v
+  in
+
+  let rec equation_pass state : t_eqlist -> unit = function
+    | [] -> ()
+    | (vars, exp)::q -> begin
+      add_to_table vars exp state;
+      equation_pass state q
+    end
+  in
+
+  let flatten_state state = match state with
+  | State(name, eq, cond, next) -> 
+    (* Flattening is not possible
+       for example a branch where x,y = 1, 2 will be unpacked
+       when in another branch x, y = f(z) will not be unpacked
+    *)
+    (*
+    let new_equations = List.flatten
+      begin
+      List.map
+        (tpl debug)
+        eq
+      end in
+    *)
+    equation_pass name eq;
+    State(name, eq, cond, next)
+  in
+
+  let rec transition_eq states s = 
+    match states with
+    | [] -> EVar([TInt], IVar(s))
+    | State(name, eqs, cond, next)::q ->
+        let name = find_state name
+        and next = find_state next in
+        ETriOp([TInt], TOp_if, 
+          EBinOp([TBool], BOp_and, 
+            EComp([TBool], COp_eq,
+              EVar([TInt], IVar(s)),
+              EConst([TInt], CInt(name))
+            ),
+            cond
+          ),
+          EConst([TInt], CInt(next)),
+          transition_eq q s
+        )
+    in
+
+  let default_constant ty =
+    let defaults ty = match ty with
+    | TInt  -> EConst([ty], CInt(0))
+    | TBool -> EConst([ty], CBool(false))
+    | TReal -> EConst([ty], CReal(0.0))
+    in
+    match ty with
+    | [TInt]  -> EConst(ty, CInt(0))
+    | [TBool] -> EConst(ty, CBool(false))
+    | [TReal] -> EConst(ty, CReal(0.0))
+    | _ -> ETuple(ty, List.map defaults ty)
+  in
+
+  let rec translate_var s v explist ty = match explist with
+  | [] -> default_constant ty
+  | (state, exp)::q -> 
+      ETriOp(Utils.type_exp exp, TOp_if,
+        EComp([TBool], COp_eq, 
+          EVar([TInt], IVar(s)),
+          EConst([TInt], CInt(Hashtbl.find state_to_int state))
+        ),
+        exp,
+        translate_var s v q ty
+      )
+  in
+
+  let flatten_automaton automaton = 
+    let (init, states) = automaton in
+    (flatten_state init, List.map flatten_state states)
+  in
+  let (init, states) = flatten_automaton automaton in
+  let s = create_automaton_name () in
+  init_state_translation states 1;
+  let exp_transition = EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, transition_eq states s)) in
+  let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in
+  Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist (fst var))::acc) gathered new_equations, IVar(s)
+
+
+let automata_trans_pass debug (node:t_node) : t_node option=
+
+  let rec aux automaton = match automaton with
+  | [] -> [], [], []
+  | a::q -> 
+      let eq, var = automaton_translation debug a
+      and tail_eq, tail_var, tail_type = aux q in
+      eq@tail_eq, var::tail_var, TInt::tail_type
+  in
+
+  let eqs, vars, new_ty = aux node.n_automata in
+  let ty, loc_vars = node.n_local_vars in
+  Some
+    {
+      n_name = node.n_name;
+      n_inputs = node.n_inputs;
+      n_outputs = node.n_outputs;
+      n_local_vars = (new_ty@ty, vars@loc_vars);
+      n_equations = eqs@node.n_equations;
+      n_automata = []; (* not needed anymore *)
+    }
+
+let automata_translation_pass verbose debug = 
+  node_pass (automata_trans_pass debug)
+
+let clock_unification_pass verbose debug ast = 
+
+  let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
+    
+  let known_clocks = Hashtbl.create 100 in
+
+  let find_clock_var var = 
+      match Hashtbl.find_opt known_clocks var with
+      | None -> 
+        begin
+          match var with
+          | BVar(name)
+          | IVar(name)
+          | RVar(name) -> raise (PassExn ("Cannot find clock of variable "^name) )
+        end
+      | Some c -> c
+  in
+
+  let rec compute_clock_exp exp = match exp with
+  | EConst(_, _) -> [Base]
+  | EVar(_, var) -> find_clock_var var
+  | EMonOp(_, MOp_pre, _) -> [Base]
+  | EMonOp(_, _, e) -> compute_clock_exp e
+
+  | EComp(_, _, e1, e2)
+  | EReset(_, e1, e2)
+  | EBinOp(_, _, e1, e2) -> 
+    begin
+      let c1 = compute_clock_exp e1
+      and c2 = compute_clock_exp e2 in
+      if c1 <> c2 then
+        failure "Binop"
+      else
+        c1
+    end
+  | EWhen(_, e1, e2) -> 
+      begin
+        match compute_clock_exp e1 with
+        | [c1] -> [On (c1, e2)]
+        | _ -> failure "When"
+      end
+  | ETriOp(_, TOp_merge, e1, e2, e3) ->
+    begin
+      let c1 = compute_clock_exp e1
+      and c2 = compute_clock_exp e2
+      and c3 = compute_clock_exp e3 in
+      match c1, c2, c3 with
+      | [c1], [On(cl2, e2)], [On(cl3, e3)] ->
+          begin
+            if cl2 <> c1 || cl3 <> c1 then
+              failure "Triop clocks"
+            else match e2, e3 with
+            | EMonOp(_, MOp_not, e), _ when e = e3 -> [c1]
+            | _, EMonOp(_, MOp_not, e) when e = e2 -> [c1]
+            | _ -> failure "Triop condition"
+          end
+      | _ -> failure ("Merge format")
+    end
+  | ETriOp(_, TOp_if, e1, e2, e3) ->
+      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"
+      else c2
+
+  | ETuple(_, explist) -> List.concat_map compute_clock_exp explist
+  | EApp(_, node, e) -> 
+      let rec aux_app clk_list = match clk_list with
+      | [] -> raise (PassExn "Node called with no argument provided")
+      | [cl] -> cl
+      | t::q -> if t = (aux_app q) then t else failure "App diff clocks"
+      and mult_clk cl out_list = match out_list with
+      | [] -> []
+      | t::q -> cl::(mult_clk cl q)
+      in
+      mult_clk (aux_app (compute_clock_exp e)) (snd node.n_outputs)
+      in
+
+  let rec compute_eq_clock eq = 
+    let rec step vars clks = match vars, clks with
+    | [], [] -> ()
+    | [], c::q -> raise (PassExn "Mismatch between clock size")
+    | v::t, c::q -> Hashtbl.replace known_clocks v [c]; step t q
+    | l, [] -> raise (PassExn "Mismatch between clock size")
+    in
+    let (_, vars), exp = eq in
+    let clk = compute_clock_exp exp in
+    step vars clk
+  in
+
+  let compute_clock_node n = 
+    begin
+      Hashtbl.clear known_clocks;
+      List.iter (fun v -> Hashtbl.replace known_clocks v [Base]) (
+        snd n.n_inputs); (* Initializing inputs to base clock *)
+      List.iter compute_eq_clock n.n_equations;
+      if not (List.for_all (fun v -> (Hashtbl.find known_clocks v) = [Base]) (
+        snd n.n_outputs)) then failure "Outputs" (*Checking that the node's output are on base clock *)
+      else
+        Some n
+    end
+  in node_pass compute_clock_node ast
--- a/src/passes_utils.ml
+++ b/src/passes_utils.ml
@@ -0,0 +1,38 @@
+open Ast
+
+(** [node_pass] is an auxiliary function used to write passes: it will iterate
+  * the function passed as argument on all the nodes of the program *)
+let node_pass f ast: t_nodelist option =
+  Utils.list_map_option f ast
+
+(** [equation_pass] is an auxiliary function used to write passes: it will
+  * iterate the function passed as argument on all the equations of the
+  * program *)
+let equation_pass (f: t_equation -> t_equation option) ast: t_nodelist option =
+  let aux (node: t_node): t_node option =
+    match Utils.list_map_option f node.n_equations with
+    | None -> None
+    | Some eqs -> Some {n_name         = node.n_name;
+                        n_inputs       = node.n_inputs;
+                        n_outputs      = node.n_outputs;
+                        n_local_vars   = node.n_local_vars;
+                        n_equations    = eqs;
+                        n_automata     = node.n_automata;
+                       }
+    in
+  node_pass aux ast
+
+let expression_pass f: t_nodelist -> t_nodelist option =
+  let aux (patt, expr) =
+    match f expr with
+    | None -> None
+    | Some expr -> Some (patt, expr)
+  in
+  equation_pass aux
+
+exception PassExn of string
+
+let counter = ref 0
+let create_automaton_name : unit -> string = fun () ->
+    counter := !counter + 1;
+    Format.asprintf "_s%d" (!counter)
--- a/src/test.node
+++ b/src/test.node
@@ -1,14 +1,18 @@
-node diagonal_int (i: int) returns (o1, o2 : int);
+node id_int (i: int) returns (o: int);
 let
-	o1 = if true then i else 0;
-	o2 = i;
-	(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 = 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 main (i: int) returns (a, b: int);
+var tmp: int;
+let
+  a = 1;
+  b = aux (i, a);
+  tmp = aux (a+b, i);
+tel
+
--- a/src/test2.node
+++ b/src/test2.node
@@ -0,0 +1,15 @@
+node aux (i: int) returns (a, b: int);
+let
+  a = 1 -> pre i;
+  b = 2 * i -> (3 * pre i);
+tel
+
+node n (i: int) returns (o1, o2: int);
+var u1, u2, t1, t2: int; c: bool;
+let
+  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
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -1,2 +1,112 @@
+open Ast
+
+let rec list_select n = function
+  | [] -> [], []
+  | h :: t ->
+      if n = 0
+        then ([], h :: t)
+        else
+          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
+    | None, _ | _, None -> None
+    | Some acc, Some elt -> Some (elt :: acc)) l (Some [])
+
 let rec list_repeat n elt =
  if n = 0 then [] else elt :: (list_repeat (n-1) elt)
+
+let rec list_chk v = function
+  | [] -> false
+  | h :: t -> if h = v then true else list_chk v t
+
+let rec vars_distinct lv lv' lv'' =
+  match lv, lv', lv'' with
+  | [], [], _ -> true
+  | [], h :: t , l'' ->
+      if List.mem h l''
+        then false
+        else vars_distinct [] t l''
+  | h :: t, l', l'' ->
+      if List.mem h l' || List.mem h l''
+        then false
+        else vars_distinct t l' l''
+
+exception MyParsingError of (string * location)
+
+let type_const = function
+  | CReal _ -> [TReal]
+  | CInt  _ -> [TInt ]
+  | CBool _ -> [TBool]
+
+let type_var (v: t_var) =
+    match v with
+    | IVar _ -> [TInt]
+    | BVar _ -> [TBool]
+    | RVar _ -> [TReal]
+
+let type_exp : t_expression -> full_ty = function
+  | EVar   (full_ty , _) -> full_ty
+  | EMonOp (full_ty , _ , _) -> full_ty
+  | EBinOp (full_ty , _ , _ , _) -> full_ty
+  | ETriOp (full_ty , _ , _ , _ , _) -> full_ty
+  | EComp  (full_ty , _ , _ , _) -> full_ty
+  | EWhen  (full_ty , _ , _) -> full_ty
+  | EReset (full_ty , _ , _) -> full_ty
+  | EConst (full_ty , _) -> full_ty
+  | ETuple (full_ty , _) -> full_ty
+  | EApp   (full_ty , _ , _) -> full_ty
+
+let somify f = fun e -> Some (f e)
+
+let name_of_var: t_var -> ident = function
+  | IVar s -> s
+  | BVar s -> s
+  | RVar s -> s
+
+let rec fresh_var_name (l: t_varlist) n : ident =
+  let rec aux acc n =
+    let r = Random.int 26 in
+    Format.asprintf "%c%s"
+      (char_of_int (r + (if Random.bool () then 65 else 97)))
+      (if n = 0 then acc else aux acc (n-1))
+  in
+  let name = aux "" n in
+  if List.filter (fun v -> name_of_var v = name) (snd l) = []
+    then name
+    else fresh_var_name l n
+
+let vars_of_patt patt = List.map name_of_var (snd patt)
+
+let rec vars_of_expr (expr: t_expression) : ident list =
+  match expr with
+  | EConst _ -> []
+  | EVar   (_, v) -> [name_of_var v]
+    (** pre (e) does not rely on anything in this round *)
+  | EMonOp (_, MOp_pre, _) -> []
+  | EApp (_, _, e) | EMonOp (_, _, e) -> vars_of_expr e
+  | EComp  (_, _, e, e') | EReset (_, e, e') | EBinOp (_, _, e, e')
+  | EWhen  (_, e, e') ->
+      (vars_of_expr e) @ (vars_of_expr e')
+  | ETriOp (_, _, e, e', e'') ->
+      (vars_of_expr e) @ (vars_of_expr e') @ (vars_of_expr e'')
+  | ETuple (_, l) -> List.flatten (List.map vars_of_expr l)
+
+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)
+
--- a/tests/test.node
+++ b/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
+
--- a/tests/test2.node
+++ b/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
+
--- a/tests/test_pre.node
+++ b/tests/test_pre.node
@@ -0,0 +1,4 @@
+node n2 (i: int) returns (o: bool);
+let
+    o = pre (true and pre( i = pre(pre(i))));
+tel
Author	SHA1	Message	Date
Arnaud DABY-SEESARAM	8c3e3d1eac	[C] malloc->calloc + conditions merged in free_state_*	2022-12-20 16:52:59 +01:00
Arnaud DABY-SEESARAM	a673c447e3	[messages] better comment and errors	2022-12-20 16:41:21 +01:00
Arnaud DABY-SEESARAM	03def2ce1a	[C] new lines in then output after each step	2022-12-20 16:38:29 +01:00
Arnaud DABY-SEESARAM	ffa8918330	[C] a few fixes	2022-12-20 16:34:31 +01:00
Arnaud DABY-SEESARAM	24108925fd	[cprint] free the allocated memory (states).	2022-12-20 16:29:35 +01:00
Benjamin Loison	fd95446636	Modify C `main` to initialize correctly the state with `is_reset = false`	2022-12-20 15:46:31 +01:00
Benjamin Loison	19524ea99c	Merge branch 'ast2C_proposition' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems into ast2C_proposition	2022-12-20 15:42:59 +01:00
Benjamin Loison	88c145a527	Disable `malloc`s when `reset`ing	2022-12-20 15:39:33 +01:00
Arnaud DABY-SEESARAM	52092b1480	[cprint] code reduction	2022-12-20 15:24:55 +01:00
Arnaud DABY-SEESARAM	f121f55432	[cprint] add a main function	2022-12-20 15:11:12 +01:00
Arnaud DABY-SEESARAM	42536df81c	[parser] update of some error messages	2022-12-20 14:10:34 +01:00
Arnaud DABY-SEESARAM	c7edb27fb0	[lustre_pp] fix a typing error	2022-12-20 14:04:50 +01:00
Arnaud DABY-SEESARAM	3ad133344a	[lustre_pp] precise error messages	2022-12-20 14:02:00 +01:00
Benjamin Loison	4303dcd0e4	Correct a typo in `src/main.ml` disabling the compilation	2022-12-20 13:09:09 +01:00
Arnaud DABY-SEESARAM	f5daae824c	[merge]	2022-12-20 09:51:59 +01:00
Benjamin Loison	9fbdb7000f	Merge branch 'ast2C_proposition' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems into ast2C_proposition	2022-12-20 03:51:31 +01:00
Benjamin Loison	e1de3e6829	Add support for `reset`s	2022-12-20 03:51:28 +01:00
Benjamin Loison	657fe7e6fa	Add support for `reset`s	2022-12-20 03:48:37 +01:00
Arnaud DABY-SEESARAM	91ff654fc9	[passes] ensure that apps don't mix with operators	2022-12-19 23:21:11 +01:00
Benjamin Loison	025d25a146	Replace `nunmbers` to `numbers` in two comments of `src/parser.mly`	2022-12-19 19:48:21 +01:00
Benjamin Loison	10838d3f2d	Remove `TODO` in `src/passes.ml:automaton_translation` As Antoine Grimod said that it was already done.	2022-12-19 17:45:33 +01:00
Benjamin Loison	e63123d8f6	Move from the `x reset y` syntax to `reset x every y` one As described on https://www.di.ens.fr/~pouzet/cours/mpri/cours7/coiteration.pdf#page=4	2022-12-19 16:28:03 +01:00
Arnaud DABY-SEESARAM	01d4a08e8a	[c pass] idem	2022-12-19 14:30:39 +01:00
Arnaud DABY-SEESARAM	9483f7df5e	[c pass] merge neighbour conditionals (improved)	2022-12-19 14:22:19 +01:00
Benjamin Loison	9a0bfd468c	Correct some typos	2022-12-19 14:06:18 +01:00
Benjamin Loison	609870755c	Remove debugging symbols in `failwith` As running `OCAMLRUNPARAM=b ./_build/main.native ...` provides in case of `failwith` a better stacktrace. This enables moving `failwith`s from a file to the other without adapting them.	2022-12-19 13:56:48 +01:00
Arnaud DABY-SEESARAM	906a3d948b	[oups] forgot a pattern matching	2022-12-19 12:20:03 +01:00
Arnaud DABY-SEESARAM	249ac37934	[general] renaming, comments and removal of unused function in [pass_linearization_pre]	2022-12-19 12:18:21 +01:00
Arnaud DABY-SEESARAM	1d39173e94	[general] useless fn removed in pass_linearization_app + comments + print_debug in ast_to_c	2022-12-19 12:07:43 +01:00
Arnaud DABY-SEESARAM	4ff193759b	[passes] removal of constructs: seems ok	2022-12-19 11:22:16 +01:00
Arnaud DABY-SEESARAM	c52dce6c02	[passes] linearization: done for app, tuples (lvl 1 behind when) and pre	2022-12-18 22:34:07 +01:00
Arnaud DABY-SEESARAM	c344f125e5	[passes] linearization of tuple-equations + deletion of unused pass	2022-12-18 19:00:24 +01:00
Arnaud DABY-SEESARAM	aa7f7514d3	[Lustre -> intermediate] fix for the [pre] construct	2022-12-18 17:36:10 +01:00
Arnaud DABY-SEESARAM	77c865e360	[intermediate_ast] remove unused fields of i_nodes	2022-12-18 17:25:34 +01:00
Benjamin Loison	02130cf57c	Rename `maybeprint` to `print_if_any` to precise the purpose of this function	2022-12-18 14:50:55 +01:00
Benjamin Loison	273a868162	Simplify `cp_value` for boolean constants in `src/cprint.ml`	2022-12-18 14:45:23 +01:00
Benjamin Loison	37dfcdda35	Remove unneeded node prototypes, as Lustre only allows to call already defined nodes	2022-12-18 14:42:26 +01:00
Benjamin Loison	c3a64a2bae	Correct some typos	2022-12-18 14:31:56 +01:00
dsac	1491e279f7	[ast2C] printer: ok.	2022-12-18 13:38:40 +01:00
dsac	ce686f6c9a	[ast2C] merge ok (needs linearization)	2022-12-18 10:41:36 +01:00
dsac	1d4e1820e4	[ast2C] Applications to values	2022-12-18 09:41:22 +01:00
dsac	007c5b2862	[c printer] Ok.	2022-12-18 00:26:51 +01:00
dsac	243e8f245a	[ast2C] adding the (->) construct	2022-12-18 00:11:02 +01:00
dsac	791af71913	[ast2C] print all basic operators	2022-12-17 23:58:45 +01:00
dsac	233b385608	missing 'state->' added + print +,-,*,...	2022-12-17 23:46:39 +01:00
dsac	7a32d474d4	[ast2C] support for some basic operations (exemple in test.node)	2022-12-17 23:36:07 +01:00
dsac	cbc834b32a	[ast2C] constants, simple assignations, variables (+ one fix about pre storage)	2022-12-17 22:36:42 +01:00
dsac	a877501cca	[general] renaming: done.	2022-12-17 21:37:37 +01:00
dsac	3cbfaeb2a8	[general] renaming (pp -> lustre_pp ; c_* -> intermediate_*)	2022-12-17 21:26:32 +01:00
dsac	916c7f544b	[ast2C] initialize states of auxiliary nodes.	2022-12-17 18:34:11 +01:00
dsac	6291957be5	[ast2C] init or not init (field added to the state of the node)	2022-12-17 16:35:49 +01:00
dsac	bb99a5882b	[ast2C] store old values of variables used in the pre construct	2022-12-17 16:30:10 +01:00
dsac	0da0f58b22	[ast2C] proposition initiale	2022-12-17 16:01:48 +01:00
Arnaud DABY-SEESARAM	fa052f70e2	[beamer] pause added	2022-12-16 17:00:24 +01:00
Benjamin Loison	0175749296	Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems	2022-12-16 15:53:14 +01:00
Arnaud DABY-SEESARAM	4054da7d47	[beamer]	2022-12-16 16:51:49 +01:00
Antoine Grimod	fc0a12fa12	beamer automaton pass	2022-12-16 16:40:34 +01:00
Benjamin Loison	edfec42738	Add Git link to title slide of beamer	2022-12-16 16:03:47 +01:00
Benjamin Loison	d06fccf36b	Add second slide concerning AST to C	2022-12-16 16:02:03 +01:00
Benjamin Loison	b616bad07a	Modify second slide concerning AST to C	2022-12-16 15:53:04 +01:00
Benjamin Loison	7a0f54f291	Remove unused `pp_loc` from `src/ast_to_c.ml` which was copied from `src/pp.ml` but never used	2022-12-16 15:40:24 +01:00
Benjamin Loison	dbf1583ffd	Complete first slide of AST to C	2022-12-16 15:33:39 +01:00
Benjamin Loison	9e96697991	First slide of AST to C	2022-12-16 15:07:46 +01:00
Antoine Grimod	aa84a07902	testing clock unification	2022-12-16 14:51:41 +01:00
Antoine Grimod	ed54fd0114	clock unification added	2022-12-16 14:51:41 +01:00
Arnaud DABY-SEESARAM	b69b6998ec	[passes] linearisation: update the local variables + lienarisation of tri ops	2022-12-16 14:41:37 +01:00
Benjamin Loison	73b753bec2	Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems	2022-12-16 05:57:55 +01:00
Benjamin Loison	a0383dbf13	Make last equation of a node potentially not ending with a semi column be correctly parsed Otherwise the following code: ``` -- count the number of top between two tick node counting (tick:bool; top:bool) returns (o: bool); var v: int; let o = if tick then v else 0 -> pre o + v; v = if top then 1 else 0 tel; ``` was involving the following error: ``` Syntax error at <line 1: -- count the number of top between two tick > ```	2022-12-16 05:57:25 +01:00
Benjamin Loison	530f6ddf51	Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems	2022-12-16 05:55:15 +01:00
Arnaud DABY-SEESARAM	57dd9c1aa4	[passes] linearozation: avoir duplication of variables	2022-12-16 14:16:13 +01:00
Benjamin Loison	21414e6461	Make last equation of a node potentially not ending with a semi column Otherwise the following code: ``` -- count the number of top between two tick node counting (tick:bool; top:bool) returns (o: bool); var v: int; let o = if tick then v else 0 -> pre o + v; v = if top then 1 else 0 tel; ``` was involving the following error: ``` Syntax error at <line 1: -- count the number of top between two tick > ```	2022-12-16 05:54:41 +01:00
Benjamin Loison	c37e819f1a	Add a title frame to the beamer	2022-12-16 05:06:27 +01:00
Benjamin Loison	ea94bb84dd	Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems	2022-12-16 04:47:05 +01:00
Arnaud DABY-SEESARAM	3fa0f92233	[beamer] A few straight forward slides added	2022-12-16 10:45:20 +01:00
Arnaud DABY-SEESARAM	3417d75620	[passes] linearisation: correction (10 -> pre (20 -> 30)) works	2022-12-16 09:44:50 +01:00
Benjamin Loison	f55cd56fde	Clean other tries	2022-12-16 04:46:48 +01:00
Benjamin Loison	012131e035	Solve C warnings and support renaming outputs of functions	2022-12-16 04:45:30 +01:00
Benjamin Loison	b58b250532	WIP to remove C warnings	2022-12-16 03:18:21 +01:00
Benjamin Loison	78e096d2f4	Add support for returning multiple variables but generate C errors, as we keep returning variables for void functions	2022-12-16 03:03:12 +01:00
Benjamin Loison	621658e177	Removing first try to implement generalized function results	2022-12-16 01:55:53 +01:00
Benjamin Loison	85ecea0b9e	First try to implement generalized function results	2022-12-16 01:55:21 +01:00
Benjamin Loison	7c2c43fe24	Precise to what extent considering integers work fine with working with floats instead	2022-12-16 01:20:42 +01:00
Arnaud DABY-SEESARAM	c7a97f3305	[passes] linearization: merge fix	2022-12-16 09:00:03 +01:00
Arnaud DABY-SEESARAM	8d6349dd3f	Merge remote-tracking branch 'origin/master' into wip	2022-12-16 08:53:55 +01:00
Arnaud DABY-SEESARAM	d7f0f148e9	[pre linearization] done, not tested	2022-12-16 08:52:48 +01:00
dsac	9987922e0f	[passes] linearization of pre (wip)	2022-12-16 07:47:20 +01:00
Antoine Grimod	6af9ddf394	added pass to check validity of automata and disable flattening of automaton branch because of incorrect code resulting from it	2022-12-16 01:04:09 +01:00
Antoine Grimod	1b3af051b3	adding automaton translation pass to list of executed passes	2022-12-16 00:06:51 +01:00
Benjamin Loison	b4ae058bf6	Remove unused variable `new_locvars` in `src/passes.ml`	2022-12-16 00:04:57 +01:00
Benjamin Loison	0c8da12afe	Correct typo in verification that nodes always have arguments and make the `main` having such a verification too, as in Lustre	2022-12-16 00:00:11 +01:00
Antoine Grimod	21d2d0c9bb	fix type error in code	2022-12-15 23:48:02 +01:00
Antoine Grimod	de294df84a	Translation of automaton to lustre almost finished	2022-12-15 23:39:01 +01:00
Benjamin Loison	bfca80bb8b	Avoid crashes that can occur `when` using when with a statement that may crash if the `when` condition doesn't hold For instance ``` node main () returns (o: int); var i: int; let i = 0; o = (1 / i) when false; tel ``` used to crash with for instance: ``` Floating point exception 136 ``` now returns `0` but in fact this value wouldn't be used in theory as the `when` condition doesn't hold.	2022-12-15 23:22:15 +01:00
dsac	74f8a3c3e1	[parser] functions other that main → args required	2022-12-15 22:14:59 +01:00
dsac	0d5e045671	[parser] foirbid calling auxiliary nodes with no arguments	2022-12-15 22:07:16 +01:00
dsac	97c6020414	[parser] avoid conflicts between local, input and output variables	2022-12-15 21:42:21 +01:00
Benjamin Loison	bc8c752649	Add a comment concerning `pp_resvars` to avoid declaring multiple times two arrays while two would be enough	2022-12-15 21:05:20 +01:00
dsac	eceeb3c157	[fix] identation error	2022-12-15 20:37:05 +01:00
Benjamin Loison	ca271eaf66	Correct typos in `src/passes.ml` and `src/test.node`	2022-12-15 20:13:18 +01:00
Benjamin Loison	72ba196142	Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems	2022-12-15 19:52:02 +01:00
Benjamin Loison	1a06fc9a6a	Add `reset` support in C	2022-12-15 19:51:46 +01:00
Arnaud DABY-SEESARAM	8582337774	[passes] pass to check the typing tags of the program / expressions	2022-12-15 18:33:04 +01:00
Arnaud DABY-SEESARAM	db5c584435	[passes] fix for the equation ordering pass	2022-12-15 17:40:15 +01:00
Arnaud DABY-SEESARAM	6459c54159	[passes] ordering equations	2022-12-15 17:11:19 +01:00
Arnaud DABY-SEESARAM	9151a6e29a	[tests] adding the -test option to duplicate sanity checks	2022-12-15 17:11:19 +01:00
Arnaud DABY-SEESARAM	19fd3bc1b9	Merge remote-tracking branch 'origin/master'	2022-12-15 16:18:17 +01:00
Arnaud DABY-SEESARAM	38a7325097	[beamer] slide 7	2022-12-15 16:17:47 +01:00
Benjamin Loison	342aba4426	Correct copy-pasted `int` and `bool` cases	2022-12-15 16:08:22 +01:00
dsac	e84a6e387d	[beamer] proto 0	2022-12-15 11:40:29 +01:00
dsac	ed5f94f821	[simu] wip	2022-12-15 09:13:59 +01:00
dsac	e75d525a6d	[passes] linearisation des équations	2022-12-15 09:13:28 +01:00
dsac	73d5ed7726	[parser] avoid redefinition of nodes	2022-12-14 18:41:59 +01:00
Arnaud DABY-SEESARAM	79f0c7d223	[passes] never redefine an input	2022-12-13 18:15:48 +01:00
Arnaud DABY-SEESARAM	f3416582be	[passes] correction of the check not re-init of variables	2022-12-13 18:08:11 +01:00
Benjamin Loison	c441f8b1a6	Correct typo in comment in `src/config.ml`	2022-12-13 16:03:05 +01:00
Antoine Grimod	b4cc3ae756	"pretty" print for automaton	2022-12-13 15:57:27 +01:00
Arnaud DABY-SEESARAM	e5ac9a719d	[passes] check unicity of the assignations for each var	2022-12-13 15:55:21 +01:00
Arnaud DABY-SEESARAM	69b963c305	[gitfix] rebase fix	2022-12-13 15:04:53 +01:00
Antoine Grimod	bb017afe39	added automaton to ast	2022-12-13 15:03:41 +01:00
Arnaud DABY-SEESARAM	ad1f529863	[typo] adding newline	2022-12-13 14:57:55 +01:00
Arnaud DABY-SEESARAM	51ed84504f	[pre propagation] done.	2022-12-13 14:25:48 +01:00
Antoine Grimod	e9d586dfe7	adding automaton	2022-12-13 11:51:46 +01:00
Arnaud DABY-SEESARAM	c4ad75e4cb	[passes] auxiliary functions	2022-12-13 11:46:04 +01:00
Arnaud DABY-SEESARAM	19be2200f3	Catch syntax errors	2022-12-13 11:43:23 +01:00
Arnaud DABY-SEESARAM	8ef4d035a3	Reject programs with var initialized twice	2022-12-13 10:26:55 +01:00
Arnaud DABY-SEESARAM	ef0effeb1f	improvement over error messages (with code ;) )	2022-12-13 10:26:55 +01:00
Benjamin Loison	298e88f1a5	Simplify `ETriOp` case in `src/ast_to_c.ml`	2022-12-11 22:25:11 +01:00
Benjamin Loison	014110791d	Remove useless `prefix` from `pp_expression_aux` and `pp_expression_list` functions in `src/ast_to_c.ml`	2022-12-11 20:07:28 +01:00
Benjamin Loison	cbddd63927	Format the code to make it shorter and more readable	2022-12-11 19:53:23 +01:00
Benjamin Loison	241f3dcbc0	Add `pre` support in C	2022-12-11 19:28:41 +01:00
Benjamin Loison	c0c29e1df7	Add assignement support for tuples	2022-12-11 18:45:30 +01:00
Benjamin Loison	da823ac3c8	Add `->` support in C	2022-12-10 21:17:32 +01:00
Benjamin Loison	38f58f7558	Unitfy `pp_varlist`, `pp_argvarlist` and `pp_decvarlist`	2022-12-10 20:51:52 +01:00
Benjamin Loison	eac8c6893c	Add support to multiple local variables in C	2022-12-10 20:30:32 +01:00
Benjamin Loison	363f5043a0	Add node call support in C	2022-12-10 20:22:11 +01:00
Benjamin Loison	5a54f897b1	Add indentation to `pp_equations` in `src/ast_to_c.ml`	2022-12-10 19:27:18 +01:00
Benjamin Loison	ac1eea42e9	Make `<=`, `>=` and `<>` work	2022-12-10 19:24:34 +01:00
Benjamin Loison	a44c9288f5	Translate two expressions of the AST from French to English	2022-12-10 19:12:16 +01:00
Benjamin Loison	b2e3ec4dd8	Modify `src/ast_to_c.ml` as a first iteration	2022-12-10 19:07:18 +01:00
Benjamin Loison	a8e89854a4	Copy `src/pp.ml` to `src/ast_to_c` and modify `src/main.ml` accordingly Just `pp_ast` was renamed to `ast_to_c`.	2022-12-10 18:58:06 +01:00
Arnaud DABY-SEESARAM	54d806f149	[pp] add typing information	2022-12-10 17:20:02 +01:00
Arnaud DABY-SEESARAM	5551237414	[parser] types of both side of equations are lists	2022-12-10 17:14:54 +01:00
Benjamin Loison	45d64f6960	Add `reset` keyword	2022-12-10 02:18:04 +01:00
Benjamin Loison	dcf7320c0d	Add one-line comment support and make some semi-column optional Make possible the parsing of the counting example of Clock-directed Modular Code Generation for Synchronous Data-flow Languages (https://www.di.ens.fr/~pouzet/bib/lctes08a.pdf). ``` -- count the number of top between two tick node counting (tick:bool; top:bool) returns (o: int) var v: int; let o = if tick then v else 0 -> pre o + v; v = if top then 1 else 0; tel; ``` The one-line comment rule was inspired from https://mukulrathi.com/create-your-own-programming-language/parsing-ocamllex-menhir/. Note their typo using `single_line_comment` instead of `read_single_line_comment`.	2022-12-10 01:58:09 +01:00
Benjamin Loison	97930ba85c	Correcting typos and using only English	2022-12-10 00:53:20 +01:00
Arnaud DABY-SEESARAM	8775edc6fc	[parser] working equation type-checker	2022-12-10 00:33:14 +01:00
Benjamin Loison	a17b3c6fdd	Make `real` type works Otherwise for the following code: ``` node test (i: real) returns (o: real); let o = 0.0; tel ``` was experiencing: ``` Fatal error: exception Stdlib.Parsing.Parse_error Raised at Stdlib__Parsing.yyparse.loop in file "parsing.ml", line 139, characters 8-25 Called from Stdlib__Parsing.yyparse in file "parsing.ml", line 165, characters 4-28 Re-raised at Stdlib__Parsing.yyparse in file "parsing.ml", line 184, characters 8-17 Called from Parser.main in file "parser.ml" (inlined), line 1110, characters 4-44 Called from Main in file "main.ml", line 70, characters 16-68 ``` Note that `%token REAL` doesn't help to solve this error, but it doesn't seem to be any reason for not having it.	2022-12-10 00:05:07 +01:00
dsac	3c811c6128	Merge remote-tracking branch 'origin/master'	2022-12-10 00:00:28 +01:00
dsac	eb469bc960	Cleanning after last merge + parser factorisation	2022-12-10 00:00:17 +01:00
Benjamin Loison	da1406fbcc	Precise `varlist` types in the AST	2022-12-09 23:43:56 +01:00
Arnaud DABY-SEESARAM	53e356ff55	merge: fby: transformation -> pre dans le parseur	2022-12-09 23:22:05 +01:00
Arnaud DABY-SEESARAM	347cb3a11d	[parser] ajout de fby (proposition alternative) + type checker (sera factorisé)	2022-12-09 23:18:13 +01:00