Merge remote-tracking branch 'origin/master' into wip

src/passes.ml

@@ -137,9 +137,9 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option
     in
     let add_var_in = add_var 1 in
     let add_var_loc = add_var 0 in
-    List.iter add_var_in (snd node.n_inputs);
     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
@@ -173,12 +173,95 @@ let rec tpl debug ((pat, exp): t_equation) =
 
 let pass_linearization verbose debug main_fn =
   let node_lin (node: t_node): t_node option =
+    let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
+      match expr with
+      | EVar _ -> [], vars, expr
+      | EMonOp (t, op, e) ->
+          begin
+          match op with
+          | MOp_pre ->
+              let eqs, vars, e = pre_aux_expression vars e in
+              let nvar: string = fresh_var_name vars 6 in
+              let nvar = match t with
+                          | [TInt]  -> IVar nvar
+                          | [TBool] -> BVar nvar
+                          | [TReal] -> RVar nvar
+                          | _ -> failwith "Should not happened." in
+              let neq_patt: t_varlist = (t, [nvar]) in
+              let neq_expr: t_expression = EMonOp (t, MOp_pre, e) in
+              let vars = varlist_concat (t, [nvar]) vars in
+              (neq_patt, neq_expr) :: eqs, vars, EVar (t, nvar)
+          | _ ->
+              let eqs, vars, e = pre_aux_expression vars e in
+              eqs, vars, EMonOp (t, op, e)
+          end
+      | EBinOp (t, op, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EBinOp (t, op, e, e')
+      | ETriOp (t, op, e, e', e'') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          let eqs'', vars, e'' = pre_aux_expression vars e'' in
+          eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'')
+      | EComp  (t, op, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EComp (t, op, e, e')
+      | EWhen  (t, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EWhen (t, e, e')
+      | EReset (t, e, e') ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          let eqs', vars, e' = pre_aux_expression vars e' in
+          eqs @ eqs', vars, EReset (t, e, e')
+      | EConst _ -> [], vars, expr
+      | ETuple (t, l) ->
+          let eqs, vars, l = List.fold_right
+            (fun e (eqs, vars, l) ->
+              let eqs', vars, e = pre_aux_expression vars e in
+              eqs' @ eqs, vars, (e :: l))
+            l ([], vars, []) in
+          eqs, vars, ETuple (t, l)
+      | EApp   (t, n, e) ->
+          let eqs, vars, e = pre_aux_expression vars e in
+          eqs, vars, EApp (t, n, e)
+      in
+    let rec pre_aux_equation (vars: t_varlist) (eq: t_equation) =
+      let (patt, expr) = eq in
+      let eqs, vars, expr = pre_aux_expression vars expr in
+      (patt, expr)::eqs, vars
+      in
+    let rec tpl ((pat, exp): t_equation) =
+      match exp with
+      | ETuple (_, hexps :: texps) ->
+          debug "An ETuple has been recognized, inlining...";
+          let p1, p2 =
+            list_select
+              (List.length (type_exp hexps))
+              (snd pat) in
+          let t1 = List.flatten (List.map type_var p1) in
+          let t2 = List.flatten (List.map type_var p2) in
+          ((t1, p1), hexps)
+            :: (tpl ((t2, p2),
+                ETuple (List.flatten (List.map type_exp texps), texps)))
+      | ETuple (_, []) -> []
+      | _ -> [(pat, exp)]
+    in
     let new_equations = List.flatten
-      begin
+      (List.map
-      List.map
+        tpl
-        (tpl debug)
+        node.n_equations)
-        node.n_equations
+      in
-      end in
+    let new_equations, new_locvars =
+      List.fold_left
+        (fun (eqs, vars) eq ->
+          let es, vs = pre_aux_equation vars eq in
+          es @ eqs, ((fst vs) @ (fst vars), (snd vs) @ (snd vars)))
+        (new_equations, node.n_local_vars)
+        new_equations
+      in
     Some
       {
         n_name = node.n_name;