Delete TODO to use git Issues instead

TODO

@@ -1,5 +0,0 @@
-# Parseur
-
- - ajustement des automates
-
-# ...

src/lustre_pp.ml

@@ -160,6 +160,7 @@ and pp_nexts fmt: t_expression list * string list -> unit = function
       pp_expression e
       n
       pp_nexts (exprs, nexts)
+  | _, _ -> () (*This should never happen*)
 
 and pp_translist fmt: t_state list -> unit = function
   | [] -> ()

src/passes.ml

@@ -6,13 +6,13 @@ open Utils
 
 
 
-(** [pass_when_lin] linearises the when construct so that it only appears as
+(** [pass_when_lin] linearizes the when construct so that it only appears as
   * main construction of right members of equations. *)
 let pass_when_lin verbose debug =
   (* prefix of the fresh variables to use and counter to make them unique. *)
   let varname_prefix = "_whenlin" in
   let count = ref 0 in
-  (** Auxiliary function that linearises an expression. *)
+  (** Auxiliary function that linearizes an expression. *)
   let rec aux_expr vars expr toplevel conds =
     match expr with
     | EVar _ | EConst _ -> [], vars, expr
@@ -74,7 +74,7 @@ let pass_when_lin verbose debug =
                 ((t, [newvar]), EWhen (t, e, e')) :: eqs'@eqs, vars, EVar (t, newvar)
                 end
               else
-                  raise (PassExn "When should only happened on unary expressions.")
+                  raise (PassExn "When should only happen on unary expressions.")
           end
   in
   (** For each node: *)
@@ -93,14 +93,14 @@ let pass_when_lin verbose debug =
 
 
 
-(** [pass_merge_lin] linearises ther merges so that they only appear as main
+(** [pass_merge_lin] linearizes the merges so that they only appear as main
   * construct of right sides of equations.
   * This simplifies their handling in next passes and in the C printer. *)
 let pass_merge_lin verbose debug =
   (* prefix of the fresh variables to use and counter to make them unique. *)
   let varname_prefix = "_mergelin" in
   let count = ref 0 in
-  (** Auxiliary function that linearises an expression. *)
+  (** Auxiliary function that linearizes an expression. *)
   let rec aux_expr vars expr toplevel =
     match expr with
     | EVar _ | EConst _ -> [], vars, expr
@@ -163,7 +163,7 @@ let pass_merge_lin verbose debug =
                 let eqs'', vars, e' = aux_expr vars e' false in
                 ((t, [newvar]), ETriOp (t, TOp_merge, c, e, e')) :: eqs @ eqs' @ eqs'', vars, EVar (t, newvar)
               else
-                raise (PassExn "Merges should only happened on unary expressions.")
+                raise (PassExn "Merges should only happen on unary expressions.")
             end
       end
   in
@@ -330,7 +330,7 @@ let pass_if_removal verbose debug =
   * 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] linearises a single node. *)
+  (** [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
@@ -399,7 +399,7 @@ let pass_linearization_reset verbose debug =
   * 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] linearises a single node. *)
+  (** [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
@@ -1121,14 +1121,14 @@ let clock_unification_pass verbose debug ast =
     | EVar([TBool], var) -> acc, e
     | EConst([TBool], cons) -> acc, e
     | EMonOp([TBool], MOp_not, e) -> count_not e (acc + 1)
-    | _ -> raise (PassExn "verify_when failure")
+    | _ -> acc, e
   in
 
   let verify_when e1 e2 =
       let n1, var1 = count_not e1 0
       and n2, var2 = count_not e2 0 in
       if n1 mod 2 <> n2 mod 2 || var1 <> var2 then
-          raise (PassExn "clock unification failure")
+          raise (PassExn "verify_when failure")
   in
 
   let get_var_name var = match var with
@@ -1243,14 +1243,9 @@ let clock_unification_pass verbose debug ast =
         snd n.n_local_vars); (* Initializing local variables to Unknown clock *)
       List.iter (fun v -> Hashtbl.replace known_clocks v Base) (
         snd n.n_outputs); (* Initializing outputs to base clock *)
-      try
-        begin
           iter_til_stable n.n_equations;
           (* catch potential errors and test for unification *)
           check_unification n;
           Some n
-        end
-      with
-      | PassExn err -> (verbose err; None)
     end
   in node_pass compute_clock_node ast

tests/automaton.node

@@ -11,7 +11,7 @@ let
     o = (not (not (l1 = l2))) and (l1 = l2) and true;
 tel
 
-node auto (i: int) returns (o : int);
+node main (i: int) returns (o : int);
 var x, y:int;
 let
     automaton

tests/when_merge.node

@@ -1,14 +1,13 @@
-node test (i: int) returns (o: int);
+node test (i: real) returns (o: real);
-var x, y: int;
+var x, y: real;
 let
-    x = (1 / i) when (i <> 0);
+    x = (1.0 / i) when (i <> 0.0);
-    y = 0 when (not (i <> 0));
+    y = 0.0 when (not (i <> 0.0));
-    o = merge (i <> 0) x y;
+    o = merge (i <> 0.0) x y;
 tel
 
-node main (i: int) returns (o: int);
+node main (i: real) returns (o: real);
-var garbage: int;
 let
-    garbage = test(0);
+    -- The idea is to pass `0.0` as the input to acknowledge that the division by zero isn't computed.
-    o = test(1);
+    o = test(i);
 tel