Changeset 2951 for extracted/fixpoints.ml
 Timestamp:
 Mar 25, 2013, 11:30:01 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/fixpoints.ml
r2873 r2951 80 80 (__ > __ > (__ > __ > Bool.bool) > (__ > __ > Bool.bool) > (__ > 81 81 Bool.bool) > 'a1) > property_lattice > 'a1 **) 82 let rec property_lattice_rect_Type4 h_mk_property_lattice x_ 21945=83 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 84 l_is_maximal = l_is_maximal0 } = x_ 2194582 let rec property_lattice_rect_Type4 h_mk_property_lattice x_19049 = 83 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 84 l_is_maximal = l_is_maximal0 } = x_19049 85 85 in 86 86 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0 … … 89 89 (__ > __ > (__ > __ > Bool.bool) > (__ > __ > Bool.bool) > (__ > 90 90 Bool.bool) > 'a1) > property_lattice > 'a1 **) 91 let rec property_lattice_rect_Type5 h_mk_property_lattice x_ 21947=92 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 93 l_is_maximal = l_is_maximal0 } = x_ 2194791 let rec property_lattice_rect_Type5 h_mk_property_lattice x_19051 = 92 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 93 l_is_maximal = l_is_maximal0 } = x_19051 94 94 in 95 95 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0 … … 98 98 (__ > __ > (__ > __ > Bool.bool) > (__ > __ > Bool.bool) > (__ > 99 99 Bool.bool) > 'a1) > property_lattice > 'a1 **) 100 let rec property_lattice_rect_Type3 h_mk_property_lattice x_ 21949=101 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 102 l_is_maximal = l_is_maximal0 } = x_ 21949100 let rec property_lattice_rect_Type3 h_mk_property_lattice x_19053 = 101 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 102 l_is_maximal = l_is_maximal0 } = x_19053 103 103 in 104 104 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0 … … 107 107 (__ > __ > (__ > __ > Bool.bool) > (__ > __ > Bool.bool) > (__ > 108 108 Bool.bool) > 'a1) > property_lattice > 'a1 **) 109 let rec property_lattice_rect_Type2 h_mk_property_lattice x_ 21951=110 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 111 l_is_maximal = l_is_maximal0 } = x_ 21951109 let rec property_lattice_rect_Type2 h_mk_property_lattice x_19055 = 110 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 111 l_is_maximal = l_is_maximal0 } = x_19055 112 112 in 113 113 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0 … … 116 116 (__ > __ > (__ > __ > Bool.bool) > (__ > __ > Bool.bool) > (__ > 117 117 Bool.bool) > 'a1) > property_lattice > 'a1 **) 118 let rec property_lattice_rect_Type1 h_mk_property_lattice x_ 21953=119 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 120 l_is_maximal = l_is_maximal0 } = x_ 21953118 let rec property_lattice_rect_Type1 h_mk_property_lattice x_19057 = 119 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 120 l_is_maximal = l_is_maximal0 } = x_19057 121 121 in 122 122 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0 … … 125 125 (__ > __ > (__ > __ > Bool.bool) > (__ > __ > Bool.bool) > (__ > 126 126 Bool.bool) > 'a1) > property_lattice > 'a1 **) 127 let rec property_lattice_rect_Type0 h_mk_property_lattice x_ 21955=128 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 129 l_is_maximal = l_is_maximal0 } = x_ 21955127 let rec property_lattice_rect_Type0 h_mk_property_lattice x_19059 = 128 let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0; 129 l_is_maximal = l_is_maximal0 } = x_19059 130 130 in 131 131 h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0 … … 195 195 196 196 type fixpoint = 197 equations >valuation197 valuation 198 198 (* singleton inductive, whose constructor was mk_fixpoint *) 199 199 200 200 (** val fixpoint_rect_Type4 : 201 property_lattice > ((equations > valuation) > __ > 'a1) > fixpoint202 >'a1 **)203 let rec fixpoint_rect_Type4 latt h_mk_fixpoint x_21976=204 let fix_lfp = x_ 21976in h_mk_fixpoint fix_lfp __201 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 202 'a1 **) 203 let rec fixpoint_rect_Type4 latt eqs h_mk_fixpoint x_19080 = 204 let fix_lfp = x_19080 in h_mk_fixpoint fix_lfp __ 205 205 206 206 (** val fixpoint_rect_Type5 : 207 property_lattice > ((equations > valuation) > __ > 'a1) > fixpoint208 >'a1 **)209 let rec fixpoint_rect_Type5 latt h_mk_fixpoint x_21978=210 let fix_lfp = x_ 21978in h_mk_fixpoint fix_lfp __207 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 208 'a1 **) 209 let rec fixpoint_rect_Type5 latt eqs h_mk_fixpoint x_19082 = 210 let fix_lfp = x_19082 in h_mk_fixpoint fix_lfp __ 211 211 212 212 (** val fixpoint_rect_Type3 : 213 property_lattice > ((equations > valuation) > __ > 'a1) > fixpoint214 >'a1 **)215 let rec fixpoint_rect_Type3 latt h_mk_fixpoint x_21980=216 let fix_lfp = x_ 21980in h_mk_fixpoint fix_lfp __213 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 214 'a1 **) 215 let rec fixpoint_rect_Type3 latt eqs h_mk_fixpoint x_19084 = 216 let fix_lfp = x_19084 in h_mk_fixpoint fix_lfp __ 217 217 218 218 (** val fixpoint_rect_Type2 : 219 property_lattice > ((equations > valuation) > __ > 'a1) > fixpoint220 >'a1 **)221 let rec fixpoint_rect_Type2 latt h_mk_fixpoint x_21982=222 let fix_lfp = x_ 21982in h_mk_fixpoint fix_lfp __219 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 220 'a1 **) 221 let rec fixpoint_rect_Type2 latt eqs h_mk_fixpoint x_19086 = 222 let fix_lfp = x_19086 in h_mk_fixpoint fix_lfp __ 223 223 224 224 (** val fixpoint_rect_Type1 : 225 property_lattice > ((equations > valuation) > __ > 'a1) > fixpoint226 >'a1 **)227 let rec fixpoint_rect_Type1 latt h_mk_fixpoint x_21984=228 let fix_lfp = x_ 21984in h_mk_fixpoint fix_lfp __225 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 226 'a1 **) 227 let rec fixpoint_rect_Type1 latt eqs h_mk_fixpoint x_19088 = 228 let fix_lfp = x_19088 in h_mk_fixpoint fix_lfp __ 229 229 230 230 (** val fixpoint_rect_Type0 : 231 property_lattice > ((equations > valuation) > __ > 'a1) > fixpoint232 >'a1 **)233 let rec fixpoint_rect_Type0 latt h_mk_fixpoint x_21986=234 let fix_lfp = x_ 21986in h_mk_fixpoint fix_lfp __235 236 (** val fix_lfp : property_lattice > fixpoint > equations> valuation **)237 let rec fix_lfp latt xxx =231 property_lattice > equations > (valuation > __ > 'a1) > fixpoint > 232 'a1 **) 233 let rec fixpoint_rect_Type0 latt eqs h_mk_fixpoint x_19090 = 234 let fix_lfp = x_19090 in h_mk_fixpoint fix_lfp __ 235 236 (** val fix_lfp : property_lattice > equations > fixpoint > valuation **) 237 let rec fix_lfp latt eqs xxx = 238 238 let yyy = xxx in yyy 239 239 240 240 (** val fixpoint_inv_rect_Type4 : 241 property_lattice > fixpoint > ((equations > valuation)> __ > __ >242 'a1) > 'a1 **) 243 let fixpoint_inv_rect_Type4 x1 hterm h1 =244 let hcut = fixpoint_rect_Type4 x1 h1 hterm in hcut __241 property_lattice > equations > fixpoint > (valuation > __ > __ > 242 'a1) > 'a1 **) 243 let fixpoint_inv_rect_Type4 x1 x2 hterm h1 = 244 let hcut = fixpoint_rect_Type4 x1 x2 h1 hterm in hcut __ 245 245 246 246 (** val fixpoint_inv_rect_Type3 : 247 property_lattice > fixpoint > ((equations > valuation)> __ > __ >248 'a1) > 'a1 **) 249 let fixpoint_inv_rect_Type3 x1 hterm h1 =250 let hcut = fixpoint_rect_Type3 x1 h1 hterm in hcut __247 property_lattice > equations > fixpoint > (valuation > __ > __ > 248 'a1) > 'a1 **) 249 let fixpoint_inv_rect_Type3 x1 x2 hterm h1 = 250 let hcut = fixpoint_rect_Type3 x1 x2 h1 hterm in hcut __ 251 251 252 252 (** val fixpoint_inv_rect_Type2 : 253 property_lattice > fixpoint > ((equations > valuation)> __ > __ >254 'a1) > 'a1 **) 255 let fixpoint_inv_rect_Type2 x1 hterm h1 =256 let hcut = fixpoint_rect_Type2 x1 h1 hterm in hcut __253 property_lattice > equations > fixpoint > (valuation > __ > __ > 254 'a1) > 'a1 **) 255 let fixpoint_inv_rect_Type2 x1 x2 hterm h1 = 256 let hcut = fixpoint_rect_Type2 x1 x2 h1 hterm in hcut __ 257 257 258 258 (** val fixpoint_inv_rect_Type1 : 259 property_lattice > fixpoint > ((equations > valuation)> __ > __ >260 'a1) > 'a1 **) 261 let fixpoint_inv_rect_Type1 x1 hterm h1 =262 let hcut = fixpoint_rect_Type1 x1 h1 hterm in hcut __259 property_lattice > equations > fixpoint > (valuation > __ > __ > 260 'a1) > 'a1 **) 261 let fixpoint_inv_rect_Type1 x1 x2 hterm h1 = 262 let hcut = fixpoint_rect_Type1 x1 x2 h1 hterm in hcut __ 263 263 264 264 (** val fixpoint_inv_rect_Type0 : 265 property_lattice > fixpoint > ((equations > valuation) > __ > __ > 266 'a1) > 'a1 **) 267 let fixpoint_inv_rect_Type0 x1 hterm h1 = 268 let hcut = fixpoint_rect_Type0 x1 h1 hterm in hcut __ 269 270 (** val fixpoint_discr : property_lattice > fixpoint > fixpoint > __ **) 271 let fixpoint_discr a1 x y = 265 property_lattice > equations > fixpoint > (valuation > __ > __ > 266 'a1) > 'a1 **) 267 let fixpoint_inv_rect_Type0 x1 x2 hterm h1 = 268 let hcut = fixpoint_rect_Type0 x1 x2 h1 hterm in hcut __ 269 270 (** val fixpoint_discr : 271 property_lattice > equations > fixpoint > fixpoint > __ **) 272 let fixpoint_discr a1 a2 x y = 272 273 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH > dH __ __)) y 273 274 274 (** val fixpoint_jmdiscr : property_lattice > fixpoint > fixpoint > __ **) 275 let fixpoint_jmdiscr a1 x y = 275 (** val fixpoint_jmdiscr : 276 property_lattice > equations > fixpoint > fixpoint > __ **) 277 let fixpoint_jmdiscr a1 a2 x y = 276 278 Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH > dH __ __)) y 277 279 280 (** val dpi1__o__fix_lfp__o__inject : 281 property_lattice > equations > (fixpoint, 'a1) Types.dPair > valuation 282 Types.sig0 **) 283 let dpi1__o__fix_lfp__o__inject x0 x2 x4 = 284 fix_lfp x0 x2 x4.Types.dpi1 285 286 (** val eject__o__fix_lfp__o__inject : 287 property_lattice > equations > fixpoint Types.sig0 > valuation 288 Types.sig0 **) 289 let eject__o__fix_lfp__o__inject x0 x2 x4 = 290 fix_lfp x0 x2 (Types.pi1 x4) 291 292 (** val fix_lfp__o__inject : 293 property_lattice > equations > fixpoint > valuation Types.sig0 **) 294 let fix_lfp__o__inject x0 x2 x3 = 295 fix_lfp x0 x2 x3 296 278 297 (** val dpi1__o__fix_lfp : 279 property_lattice > (fixpoint, 'a1) Types.dPair > equations> valuation **)280 let dpi1__o__fix_lfp x0 x 2=281 fix_lfp x0 x 2.Types.dpi1298 property_lattice > equations > (fixpoint, 'a1) Types.dPair > valuation **) 299 let dpi1__o__fix_lfp x0 x1 x3 = 300 fix_lfp x0 x1 x3.Types.dpi1 282 301 283 302 (** val eject__o__fix_lfp : 284 property_lattice > fixpoint Types.sig0 > equations > valuation **) 285 let eject__o__fix_lfp x0 x2 = 286 fix_lfp x0 (Types.pi1 x2) 287 288 type fixpoint_computer = property_lattice > fixpoint 289 303 property_lattice > equations > fixpoint Types.sig0 > valuation **) 304 let eject__o__fix_lfp x0 x1 x3 = 305 fix_lfp x0 x1 (Types.pi1 x3) 306 307 type fixpoint_computer = property_lattice > equations > fixpoint 308 309 (** val dpi1__o__apply_fixpoint : 310 property_lattice > equations > (fixpoint, 'a1) Types.dPair > 311 Graphs.label > __ **) 312 let dpi1__o__apply_fixpoint x0 x1 x3 = 313 let latt = x0 in 314 let eqs = x1 in let f = x3.Types.dpi1 in (fun l > fix_lfp latt eqs f l) 315 316 (** val eject__o__apply_fixpoint : 317 property_lattice > equations > fixpoint Types.sig0 > Graphs.label > 318 __ **) 319 let eject__o__apply_fixpoint x0 x1 x3 = 320 let latt = x0 in 321 let eqs = x1 in let f = Types.pi1 x3 in (fun l > fix_lfp latt eqs f l) 322
Note: See TracChangeset
for help on using the changeset viewer.