Delete TODO to use git Issues instead

TODO

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

src/cprint.ml

@@ -95,7 +95,7 @@ let cp_state_frees fmt (iprog, sts) =
         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"
+            \t\tfree (st->aux_states[%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\

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/main.ml

@@ -41,6 +41,7 @@ let _ =
   (** Usage and argument parsing. *)
   let default_passes =
     ["linearization_reset"; "automata_translation"; "remove_if";
+      "linearization_merge"; "linearization_when";
       "linearization_pre"; "linearization_tuples"; "linearization_app";
       "ensure_assign_val";
       "equations_ordering";
@@ -82,6 +83,8 @@ let _ =
   List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
     [
       ("remove_if", Passes.pass_if_removal);
+      ("linearization_merge", Passes.pass_merge_lin);
+      ("linearization_when", Passes.pass_when_lin);
       ("linearization_tuples", Passes.pass_linearization_tuples);
       ("linearization_app", Passes.pass_linearization_app);
       ("linearization_pre", Passes.pass_linearization_pre);

src/passes.ml

@@ -6,6 +6,183 @@ open Utils
 
 
 
+(** [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 linearizes an expression. *)
+  let rec aux_expr vars expr toplevel conds =
+    match expr with
+    | EVar _ | EConst _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EBinOp (t, op, e, e')
+    | EComp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      eqs'@eqs, vars, EComp (t, op, e, e')
+    | EReset (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds 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 false conds in
+          eqs' @ eqs, vars, (e :: l))
+        l ([], vars, []) in
+      eqs, vars, ETuple (t, l)
+    | EApp (t, n, e) ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      eqs, vars, EApp (t, n, e)
+    | ETriOp (t, op, e, e', e'') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false conds in
+      let eqs'', vars, e'' = aux_expr vars e'' false conds in
+      eqs''@eqs'@eqs, vars, ETriOp (t, op, e, e', e'')
+    | EWhen (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false conds in
+      let eqs', vars, e' = aux_expr vars e' false (e :: conds) in
+      let e =
+        List.fold_left
+          (fun e e' -> EBinOp ([TBool], BOp_and, e,e'))
+          e conds
+      in
+      if toplevel
+        then
+          eqs'@eqs, vars, EWhen (t, e, e')
+        else
+          begin
+            if List.length t = 1
+              then
+                begin
+                let newvar = Format.sprintf "%s%d" varname_prefix !count in
+                let newvar =
+                  match List.hd t with
+                  | TInt -> IVar newvar
+                  | TBool -> BVar newvar
+                  | TReal -> RVar newvar
+                  in
+                let () = incr count in
+                let vars = (t @ (fst vars), newvar :: (snd vars)) in
+                ((t, [newvar]), EWhen (t, e, e')) :: eqs'@eqs, vars, EVar (t, newvar)
+                end
+              else
+                  raise (PassExn "When should only happen on unary expressions.")
+          end
+  in
+  (** For each node: *)
+  let aux_when_lin node =
+    (** Loop on equations to get additional equations and variables. *)
+    let eqs, vars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = aux_expr vars expr true [] in
+          (patt, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_local_vars = vars; n_equations = eqs }
+  in
+  node_pass aux_when_lin
+
+
+
+(** [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 linearizes an expression. *)
+  let rec aux_expr vars expr toplevel =
+    match expr with
+    | EVar _ | EConst _ -> [], vars, expr
+    | EMonOp (t, op, e) ->
+      let eqs, vars, e = aux_expr vars e false in
+      eqs, vars, EMonOp (t, op, e)
+    | EBinOp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EBinOp (t, op, e, e')
+    | EComp (t, op, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs'@eqs, vars, EComp (t, op, e, e')
+    | EReset (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false 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 false in
+          eqs' @ eqs, vars, (e :: l))
+        l ([], vars, []) in
+      eqs, vars, ETuple (t, l)
+    | EApp (t, n, e) ->
+      let eqs, vars, e = aux_expr vars e false in
+      eqs, vars, EApp (t, n, e)
+    | ETriOp (_, TOp_if, _, _, _) ->
+        raise (PassExn "There should no longer be any condition.")
+    | EWhen (t, e, e') ->
+      let eqs, vars, e = aux_expr vars e false in
+      let eqs', vars, e' = aux_expr vars e' false in
+      eqs @ eqs', vars, EWhen (t, e, e')
+    | ETriOp (t, TOp_merge, c, e, e') ->
+      begin
+        if toplevel
+          then
+            begin
+            let eqs, vars, c = aux_expr vars c false in
+            let eqs', vars, e = aux_expr vars e false in
+            let eqs'', vars, e' = aux_expr vars e' false in
+            eqs@eqs'@eqs'', vars, ETriOp (t, TOp_merge, c, e, e')
+            end
+          else
+            begin
+            if List.length t = 1
+              then
+                let newvar = Format.sprintf "%s%d" varname_prefix !count in
+                let newvar =
+                  match List.hd t with
+                  | TInt -> IVar newvar
+                  | TBool -> BVar newvar
+                  | TReal -> RVar newvar
+                  in
+                let () = incr count in
+                let vars = (t @ (fst vars), newvar :: (snd vars)) in
+                let eqs, vars, c = aux_expr vars c false in
+                let eqs', vars, e = aux_expr vars e false in
+                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 happen on unary expressions.")
+            end
+      end
+  in
+  (** For each node: *)
+  let aux_merge_lin node =
+    (** Loop on equations to get additional equations and variables. *)
+    let eqs, vars =
+      List.fold_left
+        (fun (eqs, vars) (patt, expr) ->
+          let eqs', vars, expr = aux_expr vars expr true in
+          (patt, expr) :: eqs' @ eqs, vars)
+        ([], node.n_local_vars) node.n_equations
+      in
+    Some { node with n_local_vars = vars; n_equations = eqs }
+  in
+  node_pass aux_merge_lin
+
+
+
 (** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones.
   *
   *     [x1, ..., xn = if c then e_l else e_r;]
@@ -749,7 +926,7 @@ let pass_typing verbose debug ast =
           else None
   in aux ast
 
-let check_automata_validity verbos debug = 
+let check_automata_validity verbose debug = 
   let check_automaton_branch_vars automaton = 
     let (init, states) = automaton in
     let left_side = Hashtbl.create 10 in
@@ -774,8 +951,11 @@ let check_automata_validity verbos debug =
     end
   in
   let aux node = 
+    try
     List.iter check_automaton_branch_vars node.n_automata;
     Some node
+    with
+    | PassExn err -> (verbose err; None)
   in
   node_pass aux
 
@@ -922,9 +1102,12 @@ let automata_translation_pass verbose debug =
                 eqs@eqs_end, (ty@ty_end, vars@vars_end)
     in
     let aux node = 
+        try
             let eqs, (ty, vars) = iter_automata node.n_automata in
             let (ty_old, vars_old) = node.n_local_vars in
             Some { node with n_local_vars = (ty@ty_old, vars@vars_old); n_equations = node.n_equations@eqs; n_automata = []}
+        with
+        |PassExn err -> (verbose err; None)
     in
   node_pass aux
 
@@ -938,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

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