optimize_machine.ml

(********************************************************************)
(*                                                                  *)
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
(*                                                                  *)
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
(*  under the terms of the GNU Lesser General Public License        *)
(*  version 2.1.                                                    *)
(*                                                                  *)
(********************************************************************)

open Utils
open Lustre_types
open Spec_types
open Machine_code_types
open Corelang
open Causality
open Machine_code_common
module Mpfr = Lustrec_mpfr

let pp_no_effect fmt = Format.fprintf fmt ".. no effect.@ "

let pp_elim m fmt elim =
  IMap.pp ~comment:"/* elim table: */" (pp_val m) fmt elim

let rec fixpoint f x =
  let y, c = f x in
  if c then fixpoint f y else y

let eliminate_var_decl elim m v a =
  if is_memory m v then a else try IMap.find v.var_id elim with Not_found -> a

let rec eliminate_val m elim expr =
  let eliminate_val = eliminate_val m in
  match expr.value_desc with
  | Var v ->
    eliminate_var_decl elim m v expr
  | Fun (id, vl) ->
    { expr with value_desc = Fun (id, List.map (eliminate_val elim) vl) }
  | Array vl ->
    { expr with value_desc = Array (List.map (eliminate_val elim) vl) }
  | Access (v1, v2) ->
    {
      expr with
      value_desc = Access (eliminate_val elim v1, eliminate_val elim v2);
    }
  | Power (v1, v2) ->
    {
      expr with
      value_desc = Power (eliminate_val elim v1, eliminate_val elim v2);
    }
  | Cst _ | ResetFlag ->
    expr

let rec value_eq v1 v2 =
  let values_eq = List.for_all2 value_eq in
  match v1.value_desc, v2.value_desc with
  | Var v1, Var v2 ->
    v1.var_id = v2.var_id
  | Fun (f1, vs1), Fun (f2, vs2) ->
    f1 = f2 && values_eq vs1 vs2
  | Array vs1, Array vs2 ->
    values_eq vs1 vs2
  | Access (v1, v2), Access (w1, w2) | Power (v1, v2), Power (w1, w2) ->
    value_eq v1 w1 && value_eq v2 w2
  | v1, v2 ->
    v1 = v2

let eliminate_val m elim expr =
  let f expr =