63 open Hints_declaration
75 type property_lattice = { l_bottom : __; l_equal : (__ -> __ -> Bool.bool);
76 l_included : (__ -> __ -> Bool.bool);
77 l_is_maximal : (__ -> Bool.bool) }
79 val property_lattice_rect_Type4 :
80 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
81 Bool.bool) -> 'a1) -> property_lattice -> 'a1
83 val property_lattice_rect_Type5 :
84 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
85 Bool.bool) -> 'a1) -> property_lattice -> 'a1
87 val property_lattice_rect_Type3 :
88 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
89 Bool.bool) -> 'a1) -> property_lattice -> 'a1
91 val property_lattice_rect_Type2 :
92 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
93 Bool.bool) -> 'a1) -> property_lattice -> 'a1
95 val property_lattice_rect_Type1 :
96 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
97 Bool.bool) -> 'a1) -> property_lattice -> 'a1
99 val property_lattice_rect_Type0 :
100 (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
101 Bool.bool) -> 'a1) -> property_lattice -> 'a1
105 val l_bottom : property_lattice -> __
107 val l_equal : property_lattice -> __ -> __ -> Bool.bool
109 val l_included : property_lattice -> __ -> __ -> Bool.bool
111 val l_is_maximal : property_lattice -> __ -> Bool.bool
113 val property_lattice_inv_rect_Type4 :
114 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
115 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
117 val property_lattice_inv_rect_Type3 :
118 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
119 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
121 val property_lattice_inv_rect_Type2 :
122 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
123 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
125 val property_lattice_inv_rect_Type1 :
126 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
127 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
129 val property_lattice_inv_rect_Type0 :
130 property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
131 Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
133 val property_lattice_jmdiscr : property_lattice -> property_lattice -> __
135 type valuation = Graphs.label -> __
137 type rhs = valuation -> __
139 type equations = Graphs.label -> rhs
143 (* singleton inductive, whose constructor was mk_fixpoint *)
145 val fixpoint_rect_Type4 :
146 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
149 val fixpoint_rect_Type5 :
150 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
153 val fixpoint_rect_Type3 :
154 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
157 val fixpoint_rect_Type2 :
158 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
161 val fixpoint_rect_Type1 :
162 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
165 val fixpoint_rect_Type0 :
166 property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
169 val fix_lfp : property_lattice -> equations -> fixpoint -> valuation
171 val fixpoint_inv_rect_Type4 :
172 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
175 val fixpoint_inv_rect_Type3 :
176 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
179 val fixpoint_inv_rect_Type2 :
180 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
183 val fixpoint_inv_rect_Type1 :
184 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
187 val fixpoint_inv_rect_Type0 :
188 property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
192 property_lattice -> equations -> fixpoint -> fixpoint -> __
194 val fixpoint_jmdiscr :
195 property_lattice -> equations -> fixpoint -> fixpoint -> __
197 val dpi1__o__fix_lfp__o__inject :
198 property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
201 val eject__o__fix_lfp__o__inject :
202 property_lattice -> equations -> fixpoint Types.sig0 -> valuation
205 val fix_lfp__o__inject :
206 property_lattice -> equations -> fixpoint -> valuation Types.sig0
208 val dpi1__o__fix_lfp :
209 property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
211 val eject__o__fix_lfp :
212 property_lattice -> equations -> fixpoint Types.sig0 -> valuation
214 type fixpoint_computer = property_lattice -> equations -> fixpoint
216 val dpi1__o__apply_fixpoint :
217 property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
220 val eject__o__apply_fixpoint :
221 property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label -> __