source: extracted/initialisation.mli @ 2716

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

...

File size: 1.8 KB
Line 
1open Preamble
2
3open CostLabel
4
5open FrontEndVal
6
7open Hide
8
9open ByteValues
10
11open GenMem
12
13open FrontEndMem
14
15open Proper
16
17open PositiveMap
18
19open Deqsets
20
21open Extralib
22
23open Lists
24
25open Identifiers
26
27open Integers
28
29open AST
30
31open Division
32
33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open FoldStuff
40
41open BitVector
42
43open Z
44
45open BitVectorZ
46
47open Pointers
48
49open ErrorMessages
50
51open Option
52
53open Setoids
54
55open Monad
56
57open Positive
58
59open PreIdentifiers
60
61open Errors
62
63open Div_and_mod
64
65open Jmeq
66
67open Russell
68
69open Util
70
71open Bool
72
73open Relations
74
75open Nat
76
77open List
78
79open Hints_declaration
80
81open Core_notation
82
83open Pts
84
85open Logic
86
87open Types
88
89open Coqlib
90
91open Values
92
93open FrontEndOps
94
95open Cminor_syntax
96
97open Extra_bool
98
99open Globalenvs
100
101val init_expr :
102  AST.init_data -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option
103
104val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
105
106val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __
107
108val init_datum :
109  AST.ident -> AST.region -> AST.init_data -> Nat.nat -> Cminor_syntax.stmt
110  Types.sig0
111
112val init_var :
113  AST.ident -> AST.region -> AST.init_data List.list -> Cminor_syntax.stmt
114  Types.sig0
115
116val init_vars :
117  ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
118  List.list -> Cminor_syntax.stmt Types.sig0
119
120val add_statement :
121  CostLabel.costlabel -> AST.ident -> Cminor_syntax.stmt Types.sig0 ->
122  (AST.ident, Cminor_syntax.internal_function AST.fundef) Types.prod
123  List.list -> (AST.ident, Cminor_syntax.internal_function AST.fundef)
124  Types.prod List.list
125
126val empty_vars :
127  ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod
128  List.list -> ((AST.ident, AST.region) Types.prod, Nat.nat) Types.prod
129  List.list
130
131val replace_init :
132  CostLabel.costlabel -> Cminor_syntax.cminor_program ->
133  Cminor_syntax.cminor_noinit_program
134
Note: See TracBrowser for help on using the repository browser.