extracted/fresh.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Coqlib
   6
   7 open Proper
   8
   9 open PositiveMap
  10
  11 open Deqsets
  12
  13 open ErrorMessages
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Extralib
  20
  21 open Lists
  22
  23 open Positive
  24
  25 open Identifiers
  26
  27 open Exp
  28
  29 open Arithmetic
  30
  31 open Vector
  32
  33 open Div_and_mod
  34
  35 open Util
  36
  37 open FoldStuff
  38
  39 open BitVector
  40
  41 open Jmeq
  42
  43 open Russell
  44
  45 open List
  46
  47 open Setoids
  48
  49 open Monad
  50
  51 open Option
  52
  53 open Extranat
  54
  55 open Bool
  56
  57 open Relations
  58
  59 open Nat
  60
  61 open Integers
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open AST
  74
  75 open Csyntax
  76
  77 (** val max_id : AST.ident -> AST.ident -> AST.ident **)
  78 let max_id a b =
  79   let a0 = a in let b0 = b in Positive.max a0 b0
  80
  81 (** val max_id_of_env :
  82     (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident **)
  83 let max_id_of_env =
  84   List.foldr (fun it id -> max_id it.Types.fst id) Positive.One
  85
  86 (** val max_id_of_fn : Csyntax.function0 -> AST.ident **)
  87 let max_id_of_fn f =
  88   max_id_of_env (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
  89
  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
  94
  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)
 100     Positive.One
 101
 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
 107
 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)
 112
 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
 116
 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)
 121