source: extracted/fresh.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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