From Coq Require Import String.
From Coq Require Import List Sorting.Permutation.
Import List.ListNotations.
Open Scope list_scope.

From compcert Require Import common.Errors.
From Velus Require Import Common.
From Velus Require Import Operators.
From Velus Require Import Clocks.
From Velus Require Import StaticEnv.
From Velus Require Import Lustre.LSyntax.
From Velus Require Import Lustre.Normalization.Unnesting Lustre.Normalization.NormFby.

Complete Normalization

Module Type NORMALIZATION
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Import Cks : CLOCKS Ids Op OpAux)
       (Import Senv : STATICENV Ids Op OpAux Cks)
       (Import Syn : LSYNTAX Ids Op OpAux Cks Senv).

  Module Export Unnesting := UnnestingFun Ids Op OpAux Cks Senv Syn.
  Module Export NormFby := NormFbyFun Ids Op OpAux Cks Senv Syn Unnesting.

  Definition normalize_global G :=
    normfby_global (unnest_global G).

  Lemma normalize_global_iface_eq : forall G,
      global_iface_eq G (normalize_global G).

  Theorem normalize_global_normalized_global : forall G,
      wl_global G ->
      wx_global G ->
      normalized_global (normalize_global G).

End NORMALIZATION.

Module NormalizationFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Ids Op)
       (Cks : CLOCKS Ids Op OpAux)
       (Senv : STATICENV Ids Op OpAux Cks)
       (Syn : LSYNTAX Ids Op OpAux Cks Senv)
       <: NORMALIZATION Ids Op OpAux Cks Senv Syn.
  Include NORMALIZATION Ids Op OpAux Cks Senv Syn.
End NormalizationFun.