63 open Hints_declaration
77 (** val max_id : AST.ident -> AST.ident -> AST.ident **)
79 let a0 = a in let b0 = b in Positive.max a0 b0
81 (** val max_id_of_env :
82 (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident **)
84 List.foldr (fun it id -> max_id it.Types.fst id) Positive.One
86 (** val max_id_of_fn : Csyntax.function0 -> AST.ident **)
88 max_id_of_env (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
90 (** val max_id_of_fundef : Csyntax.clight_fundef -> AST.ident **)
91 let max_id_of_fundef = function
92 | Csyntax.CL_Internal f0 -> max_id_of_fn f0
93 | Csyntax.CL_External (id, x, x0) -> id
95 (** val max_id_of_functs :
96 (AST.ident, Csyntax.clight_fundef) Types.prod List.list -> AST.ident **)
97 let max_id_of_functs =
98 List.foldr (fun idf id ->
99 max_id (max_id idf.Types.fst (max_id_of_fundef idf.Types.snd)) id)
102 (** val max_id_of_globvars :
103 ((AST.ident, AST.region) Types.prod, (AST.init_data List.list,
104 Csyntax.type0) Types.prod) Types.prod List.list -> AST.ident **)
105 let max_id_of_globvars =
106 List.foldr (fun it id -> max_id it.Types.fst.Types.fst id) Positive.One
108 (** val max_id_of_program : Csyntax.clight_program -> AST.ident **)
109 let max_id_of_program p =
110 max_id (max_id (max_id_of_functs p.AST.prog_funct) p.AST.prog_main)
111 (max_id_of_globvars p.AST.prog_vars)
113 (** val universe_of_max : AST.ident -> Identifiers.universe **)
114 let universe_of_max mx =
115 let i = mx in let next = Positive.succ i in next
117 (** val universe_for_program :
118 Csyntax.clight_program -> Identifiers.universe **)
119 let universe_for_program p =
120 universe_of_max (max_id_of_program p)