Module Normalization

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 Lustre.LSyntax Lustre.LCausality.
From Velus Require Import Lustre.Normalization.Fresh.
From Velus Require Import Lustre.Normalization.Unnesting Lustre.Normalization.NormFby.

Complete Normalization


Module Type NORMALIZATION
       (Import Ids : IDS)
       (Import Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (Import Syn : LSYNTAX Ids Op)
       (Import Caus : LCAUSALITY Ids Op Syn).

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

  Definition normalize_global G :
    wl_global G ->
    Forall (fun n => n_prefixes n = elab_prefs) G ->
    res global.
Proof.

  Lemma normalize_global_prefixes : forall G Hwl Hprefs G',
      normalize_global G Hwl Hprefs = OK G' ->
      Forall (fun n => PS.Equal (n_prefixes n) (PSP.of_list gensym_prefs)) G'.
Proof.

  Lemma normalize_global_iface_eq : forall G Hwl Hprefs G',
      normalize_global G Hwl Hprefs = OK G' ->
      global_iface_eq G G'.
Proof.

  Theorem normalize_global_normalized_global : forall G G' Hwl Hprefs,
      normalize_global G Hwl Hprefs = OK G' ->
      normalized_global G'.
Proof.

Helper for the l_to_nl function
  Program Definition normalize_global' (G : {G | wl_global G /\ Forall (fun n => n_prefixes n = elab_prefs) G}) :
    {G | match G with OK G => Forall (fun n => PS.Equal (n_prefixes n) (PSP.of_list gensym_prefs)) G | _ => True end } :=
    exist _ (normalize_global G _ _) _.
Next Obligation.
End NORMALIZATION.

Module NormalizationFun
       (Ids : IDS)
       (Op : OPERATORS)
       (OpAux : OPERATORS_AUX Op)
       (Syn : LSYNTAX Ids Op)
       (Caus : LCAUSALITY Ids Op Syn)
       <: NORMALIZATION Ids Op OpAux Syn Caus.
  Include NORMALIZATION Ids Op OpAux Syn Caus.
End NormalizationFun.