(* 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".

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 (max_id_of_env (fn_params f)) (max_id_of_env (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_for_program : clight_program → universe SymbolTag ≝
λp. match max_id_of_program p with [ an_identifier i ⇒
      let next ≝ succ i in
      mk_universe SymbolTag next
    ].