source: extracted/fixpoints.mli @ 2746

Last change on this file since 2746 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: 4.7 KB
Line 
1open Preamble
2
3open Exp
4
5open Arithmetic
6
7open Integers
8
9open AST
10
11open Proper
12
13open PositiveMap
14
15open Deqsets
16
17open ErrorMessages
18
19open PreIdentifiers
20
21open Errors
22
23open Extralib
24
25open Setoids
26
27open Monad
28
29open Option
30
31open Lists
32
33open Positive
34
35open Identifiers
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  equations -> 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 -> fixpoint -> equations -> valuation
170
171val fixpoint_inv_rect_Type4 :
172  property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
173  'a1) -> 'a1
174
175val fixpoint_inv_rect_Type3 :
176  property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
177  'a1) -> 'a1
178
179val fixpoint_inv_rect_Type2 :
180  property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
181  'a1) -> 'a1
182
183val fixpoint_inv_rect_Type1 :
184  property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
185  'a1) -> 'a1
186
187val fixpoint_inv_rect_Type0 :
188  property_lattice -> fixpoint -> ((equations -> valuation) -> __ -> __ ->
189  'a1) -> 'a1
190
191val fixpoint_discr : property_lattice -> fixpoint -> fixpoint -> __
192
193val fixpoint_jmdiscr : property_lattice -> fixpoint -> fixpoint -> __
194
195val dpi1__o__fix_lfp :
196  property_lattice -> (fixpoint, 'a1) Types.dPair -> equations -> valuation
197
198val eject__o__fix_lfp :
199  property_lattice -> fixpoint Types.sig0 -> equations -> valuation
200
201type fixpoint_computer = property_lattice -> fixpoint
202
Note: See TracBrowser for help on using the repository browser.