(* In order to generate fresh names for Clight programs we find the largest
   identifier used in the program, then set up a universe based on that.
   
   NB: This only considers variables and function names.  Goto labels and
       field idents are ignored.
 *)

include "Clight/Csyntax.ma".
include "utilities/lists.ma".

definition max_id : ident → ident → ident ≝
λa,b. match a with [ an_identifier a ⇒
      match b with [ an_identifier b ⇒
        an_identifier ? (max a b)
      ]].

definition max_id_of_env : list (ident × type) → ident ≝
foldr ?? (λit,id. max_id (\fst it) id) (an_identifier ? one).

definition max_id_of_fn : function → ident ≝
λf. max_id_of_env (fn_params f @ fn_vars f).

definition max_id_of_fundef : clight_fundef → ident ≝
λf. match f with
  [ CL_Internal f ⇒ max_id_of_fn f
  | CL_External id _ _ ⇒ id
  ].

definition max_id_of_functs : list (ident × clight_fundef) → ident ≝
foldr ?? (λidf,id. max_id (max_id (\fst idf) (max_id_of_fundef (\snd idf))) id) (an_identifier ? one).

definition max_id_of_globvars : list (ident × region × (list init_data × type)) → ident ≝
foldr ?? (λit,id. max_id (\fst (\fst it)) id) (an_identifier ? one).

definition max_id_of_program : clight_program → ident ≝
λp. max_id (max_id (max_id_of_functs (prog_funct ?? p))
                   (prog_main ?? p))
           (max_id_of_globvars (prog_vars ?? p)).

definition universe_of_max : ident → universe SymbolTag ≝
λmx. match mx with [ an_identifier i ⇒
      let next ≝ succ i in
      mk_universe SymbolTag next
    ].

definition universe_for_program : clight_program → universe SymbolTag ≝
λp. universe_of_max (max_id_of_program p).


(* A specification for the result *)

definition fn_fresh_for_univ : function → universe SymbolTag → Prop ≝
λf,u. All ? (λit. fresh_for_univ ? (\fst it) u) (fn_params f @ fn_vars f).

definition fd_fresh_for_univ : clight_fundef → universe SymbolTag → Prop ≝
λfd,u.
  match fd with
  [ CL_Internal f ⇒ fn_fresh_for_univ f u
  | CL_External id _ _ ⇒ fresh_for_univ ? id u
  ].

definition globals_fresh_for_univ : ∀V:Type[0]. list (ident × region × V) → universe SymbolTag → Prop ≝
λV,gl,u.  All ? (λv. fresh_for_univ ? (\fst (\fst v)) u) gl.

definition prog_fresh_for_univ : clight_program → universe SymbolTag → Prop ≝
λp,u.
  All ? (λifd. fresh_for_univ ? (\fst ifd) u ∧ fd_fresh_for_univ (\snd ifd) u) (prog_funct ?? p) ∧
  fresh_for_univ ? (prog_main ?? p) u ∧
  globals_fresh_for_univ ? (prog_vars ?? p) u.

(* And they match up. *)

lemma uni_of_max_of : ∀i. fresh_for_univ ? i (universe_of_max i).
* #i normalize //
qed.

lemma uni_max_l : ∀i,j,k. fresh_for_univ ? i (universe_of_max j) → fresh_for_univ ? i (universe_of_max (max_id j k)).
* #i * #j * #k normalize @leb_elim normalize
[ #H #H' @(transitive_le … (succ j)) /2/
| /2/
] qed.

lemma uni_max_r : ∀i,j,k. fresh_for_univ ? i (universe_of_max k) → fresh_for_univ ? i (universe_of_max (max_id j k)).
* #i * #j * #k whd in ⊢ (? → ???(?%)); >commutative_max @(uni_max_l ? (an_identifier ? k) (an_identifier ? j))
qed.


theorem prog_fresh : ∀p. prog_fresh_for_univ p (universe_for_program p).
* #vars #fns #main
%
[ %
  [ @All_alt * #id #fd #pre #post #Efns %
    [ @uni_max_l @uni_max_l >Efns elim pre
      [ @uni_max_l @uni_max_l //
      | #x #y #H @uni_max_r @H
      ]
    | cases fd in Efns ⊢ %;
      [ #fn #Efns @All_alt >Efns * #id' #ty #envpre #envpost #Eenv
        @uni_max_l @uni_max_l elim pre
        [ @uni_max_l @uni_max_r
          whd in ⊢ (???(?%)); >Eenv elim envpre
          [ @uni_max_l //
          | #x #y #H @uni_max_r //
          ]
        | #x #y #H @uni_max_r @H
        ]
      | #id' #tys #ty #Efn >Efn
        @uni_max_l @uni_max_l elim pre
        [ @uni_max_l @uni_max_r //
        | #x #y #H @uni_max_r @H
        ]
      ]
    ]
  | @uni_max_l @uni_max_r //
  ]
| @All_alt * * #id #r #init #pre #post #E @uni_max_r >E elim pre
  [ @uni_max_l //
  | #x #y #H @uni_max_r @H
  ]
] qed.