source: extracted/fresh.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 8 years ago

...

File size: 2.1 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75(** val max_id : AST.ident -> AST.ident -> AST.ident **)
76let max_id a b =
77  let a0 = a in let b0 = b in Positive.max0 a0 b0
78
79(** val max_id_of_env :
80    (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident **)
81let max_id_of_env =
82  List.foldr (fun it id -> max_id it.Types.fst id) Positive.One
83
84(** val max_id_of_fn : Csyntax.function0 -> AST.ident **)
85let max_id_of_fn f =
86  max_id_of_env (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
87
88(** val max_id_of_fundef : Csyntax.clight_fundef -> AST.ident **)
89let max_id_of_fundef = function
90| Csyntax.CL_Internal f0 -> max_id_of_fn f0
91| Csyntax.CL_External (id, x, x0) -> id
92
93(** val max_id_of_functs :
94    (AST.ident, Csyntax.clight_fundef) Types.prod List.list -> AST.ident **)
95let max_id_of_functs =
96  List.foldr (fun idf id ->
97    max_id (max_id idf.Types.fst (max_id_of_fundef idf.Types.snd)) id)
98    Positive.One
99
100(** val max_id_of_globvars :
101    ((AST.ident, AST.region) Types.prod, (AST.init_data List.list,
102    Csyntax.type0) Types.prod) Types.prod List.list -> AST.ident **)
103let max_id_of_globvars =
104  List.foldr (fun it id -> max_id it.Types.fst.Types.fst id) Positive.One
105
106(** val max_id_of_program : Csyntax.clight_program -> AST.ident **)
107let max_id_of_program p =
108  max_id (max_id (max_id_of_functs p.AST.prog_funct) p.AST.prog_main)
109    (max_id_of_globvars p.AST.prog_vars)
110
111(** val universe_of_max : AST.ident -> Identifiers.universe **)
112let universe_of_max mx =
113  let i = mx in let next = Positive.succ i in next
114
115(** val universe_for_program :
116    Csyntax.clight_program -> Identifiers.universe **)
117let universe_for_program p =
118  universe_of_max (max_id_of_program p)
119
Note: See TracBrowser for help on using the repository browser.