source: driver/extracted/fixpoints.mli @ 3106

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

New extraction. Novely: a pre-main is used in the back-end. Initialization
of global data is performed in LINToASM.

Note: the cost-emission of the initialization costlabel in the front-end is
virtual, but not performed in the traces I generate and print. To be fixed
(how?)

File size: 5.2 KB
Line 
1open Preamble
2
3open Exp
4
5open Arithmetic
6
7open Integers
8
9open AST
10
11open Proper
12
13open PositiveMap
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Deqsets
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Extranat
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 Bool
54
55open Relations
56
57open Nat
58
59open BitVector
60
61open BitVectorTrie
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open Graphs
74
75type property_lattice = { l_bottom : __; l_equal : (__ -> __ -> Bool.bool);
76                          l_included : (__ -> __ -> Bool.bool);
77                          l_is_maximal : (__ -> Bool.bool) }
78
79val property_lattice_rect_Type4 :
80  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
81  Bool.bool) -> 'a1) -> property_lattice -> 'a1
82
83val property_lattice_rect_Type5 :
84  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
85  Bool.bool) -> 'a1) -> property_lattice -> 'a1
86
87val property_lattice_rect_Type3 :
88  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
89  Bool.bool) -> 'a1) -> property_lattice -> 'a1
90
91val property_lattice_rect_Type2 :
92  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
93  Bool.bool) -> 'a1) -> property_lattice -> 'a1
94
95val property_lattice_rect_Type1 :
96  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
97  Bool.bool) -> 'a1) -> property_lattice -> 'a1
98
99val property_lattice_rect_Type0 :
100  (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
101  Bool.bool) -> 'a1) -> property_lattice -> 'a1
102
103type l_property
104
105val l_bottom : property_lattice -> __
106
107val l_equal : property_lattice -> __ -> __ -> Bool.bool
108
109val l_included : property_lattice -> __ -> __ -> Bool.bool
110
111val l_is_maximal : property_lattice -> __ -> Bool.bool
112
113val property_lattice_inv_rect_Type4 :
114  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
115  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
116
117val property_lattice_inv_rect_Type3 :
118  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
119  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
120
121val property_lattice_inv_rect_Type2 :
122  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
123  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
124
125val property_lattice_inv_rect_Type1 :
126  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
127  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
128
129val property_lattice_inv_rect_Type0 :
130  property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
131  Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
132
133val property_lattice_jmdiscr : property_lattice -> property_lattice -> __
134
135type valuation = Graphs.label -> __
136
137type rhs = valuation -> __
138
139type equations = Graphs.label -> rhs
140
141type fixpoint =
142  valuation
143  (* singleton inductive, whose constructor was mk_fixpoint *)
144
145val fixpoint_rect_Type4 :
146  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
147  'a1
148
149val fixpoint_rect_Type5 :
150  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
151  'a1
152
153val fixpoint_rect_Type3 :
154  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
155  'a1
156
157val fixpoint_rect_Type2 :
158  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
159  'a1
160
161val fixpoint_rect_Type1 :
162  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
163  'a1
164
165val fixpoint_rect_Type0 :
166  property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
167  'a1
168
169val fix_lfp : property_lattice -> equations -> fixpoint -> valuation
170
171val fixpoint_inv_rect_Type4 :
172  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
173  -> 'a1
174
175val fixpoint_inv_rect_Type3 :
176  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
177  -> 'a1
178
179val fixpoint_inv_rect_Type2 :
180  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
181  -> 'a1
182
183val fixpoint_inv_rect_Type1 :
184  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
185  -> 'a1
186
187val fixpoint_inv_rect_Type0 :
188  property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
189  -> 'a1
190
191val fixpoint_discr :
192  property_lattice -> equations -> fixpoint -> fixpoint -> __
193
194val fixpoint_jmdiscr :
195  property_lattice -> equations -> fixpoint -> fixpoint -> __
196
197val dpi1__o__fix_lfp__o__inject :
198  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
199  Types.sig0
200
201val eject__o__fix_lfp__o__inject :
202  property_lattice -> equations -> fixpoint Types.sig0 -> valuation
203  Types.sig0
204
205val fix_lfp__o__inject :
206  property_lattice -> equations -> fixpoint -> valuation Types.sig0
207
208val dpi1__o__fix_lfp :
209  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
210
211val eject__o__fix_lfp :
212  property_lattice -> equations -> fixpoint Types.sig0 -> valuation
213
214type fixpoint_computer = property_lattice -> equations -> fixpoint
215
216val dpi1__o__apply_fixpoint :
217  property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
218  Graphs.label -> __
219
220val eject__o__apply_fixpoint :
221  property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label -> __
222
Note: See TracBrowser for help on using the repository browser.