extracted/fixpoints.ml

   1 open Preamble
   2
   3 open Exp
   4
   5 open Arithmetic
   6
   7 open Integers
   8
   9 open AST
  10
  11 open Proper
  12
  13 open PositiveMap
  14
  15 open ErrorMessages
  16
  17 open PreIdentifiers
  18
  19 open Errors
  20
  21 open Extralib
  22
  23 open Lists
  24
  25 open Positive
  26
  27 open Identifiers
  28
  29 open Deqsets
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 open Extranat
  38
  39 open Vector
  40
  41 open Div_and_mod
  42
  43 open Jmeq
  44
  45 open Russell
  46
  47 open List
  48
  49 open Util
  50
  51 open FoldStuff
  52
  53 open Bool
  54
  55 open Relations
  56
  57 open Nat
  58
  59 open BitVector
  60
  61 open BitVectorTrie
  62
  63 open Hints_declaration
  64
  65 open Core_notation
  66
  67 open Pts
  68
  69 open Logic
  70
  71 open Types
  72
  73 open Graphs
  74
  75 type property_lattice = { l_bottom : __; l_equal : (__ -> __ -> Bool.bool);
  76                           l_included : (__ -> __ -> Bool.bool);
  77                           l_is_maximal : (__ -> Bool.bool) }
  78
  79 (** val property_lattice_rect_Type4 :
  80     (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  81     Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
  82 let rec property_lattice_rect_Type4 h_mk_property_lattice x_18885 =
  83   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
  84     l_is_maximal = l_is_maximal0 } = x_18885
  85   in
  86   h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
  87
  88 (** val property_lattice_rect_Type5 :
  89     (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  90     Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
  91 let rec property_lattice_rect_Type5 h_mk_property_lattice x_18887 =
  92   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
  93     l_is_maximal = l_is_maximal0 } = x_18887
  94   in
  95   h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
  96
  97 (** val property_lattice_rect_Type3 :
  98     (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  99     Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
 100 let rec property_lattice_rect_Type3 h_mk_property_lattice x_18889 =
 101   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
 102     l_is_maximal = l_is_maximal0 } = x_18889
 103   in
 104   h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
 105
 106 (** val property_lattice_rect_Type2 :
 107     (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
 108     Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
 109 let rec property_lattice_rect_Type2 h_mk_property_lattice x_18891 =
 110   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
 111     l_is_maximal = l_is_maximal0 } = x_18891
 112   in
 113   h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
 114
 115 (** val property_lattice_rect_Type1 :
 116     (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
 117     Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
 118 let rec property_lattice_rect_Type1 h_mk_property_lattice x_18893 =
 119   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
 120     l_is_maximal = l_is_maximal0 } = x_18893
 121   in
 122   h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
 123
 124 (** val property_lattice_rect_Type0 :
 125     (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
 126     Bool.bool) -> 'a1) -> property_lattice -> 'a1 **)
 127 let rec property_lattice_rect_Type0 h_mk_property_lattice x_18895 =
 128   let { l_bottom = l_bottom0; l_equal = l_equal0; l_included = l_included0;
 129     l_is_maximal = l_is_maximal0 } = x_18895
 130   in
 131   h_mk_property_lattice __ l_bottom0 l_equal0 l_included0 l_is_maximal0
 132
 133 type l_property = __
 134
 135 (** val l_bottom : property_lattice -> __ **)
 136 let rec l_bottom xxx =
 137   xxx.l_bottom
 138
 139 (** val l_equal : property_lattice -> __ -> __ -> Bool.bool **)
 140 let rec l_equal xxx =
 141   xxx.l_equal
 142
 143 (** val l_included : property_lattice -> __ -> __ -> Bool.bool **)
 144 let rec l_included xxx =
 145   xxx.l_included
 146
 147 (** val l_is_maximal : property_lattice -> __ -> Bool.bool **)
 148 let rec l_is_maximal xxx =
 149   xxx.l_is_maximal
 150
 151 (** val property_lattice_inv_rect_Type4 :
 152     property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 153     Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
 154 let property_lattice_inv_rect_Type4 hterm h1 =
 155   let hcut = property_lattice_rect_Type4 h1 hterm in hcut __
 156
 157 (** val property_lattice_inv_rect_Type3 :
 158     property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 159     Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
 160 let property_lattice_inv_rect_Type3 hterm h1 =
 161   let hcut = property_lattice_rect_Type3 h1 hterm in hcut __
 162
 163 (** val property_lattice_inv_rect_Type2 :
 164     property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 165     Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
 166 let property_lattice_inv_rect_Type2 hterm h1 =
 167   let hcut = property_lattice_rect_Type2 h1 hterm in hcut __
 168
 169 (** val property_lattice_inv_rect_Type1 :
 170     property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 171     Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
 172 let property_lattice_inv_rect_Type1 hterm h1 =
 173   let hcut = property_lattice_rect_Type1 h1 hterm in hcut __
 174
 175 (** val property_lattice_inv_rect_Type0 :
 176     property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 177     Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1 **)
 178 let property_lattice_inv_rect_Type0 hterm h1 =
 179   let hcut = property_lattice_rect_Type0 h1 hterm in hcut __
 180
 181 (** val property_lattice_jmdiscr :
 182     property_lattice -> property_lattice -> __ **)
 183 let property_lattice_jmdiscr x y =
 184   Logic.eq_rect_Type2 x
 185     (let { l_bottom = a1; l_equal = a2; l_included = a3; l_is_maximal =
 186        a4 } = x
 187      in
 188     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
 189
 190 type valuation = Graphs.label -> __
 191
 192 type rhs = valuation -> __
 193
 194 type equations = Graphs.label -> rhs
 195
 196 type fixpoint =
 197   valuation
 198   (* singleton inductive, whose constructor was mk_fixpoint *)
 199
 200 (** val fixpoint_rect_Type4 :
 201     property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 202     'a1 **)
 203 let rec fixpoint_rect_Type4 latt eqs h_mk_fixpoint x_18916 =
 204   let fix_lfp = x_18916 in h_mk_fixpoint fix_lfp __
 205
 206 (** val fixpoint_rect_Type5 :
 207     property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 208     'a1 **)
 209 let rec fixpoint_rect_Type5 latt eqs h_mk_fixpoint x_18918 =
 210   let fix_lfp = x_18918 in h_mk_fixpoint fix_lfp __
 211
 212 (** val fixpoint_rect_Type3 :
 213     property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 214     'a1 **)
 215 let rec fixpoint_rect_Type3 latt eqs h_mk_fixpoint x_18920 =
 216   let fix_lfp = x_18920 in h_mk_fixpoint fix_lfp __
 217
 218 (** val fixpoint_rect_Type2 :
 219     property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 220     'a1 **)
 221 let rec fixpoint_rect_Type2 latt eqs h_mk_fixpoint x_18922 =
 222   let fix_lfp = x_18922 in h_mk_fixpoint fix_lfp __
 223
 224 (** val fixpoint_rect_Type1 :
 225     property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 226     'a1 **)
 227 let rec fixpoint_rect_Type1 latt eqs h_mk_fixpoint x_18924 =
 228   let fix_lfp = x_18924 in h_mk_fixpoint fix_lfp __
 229
 230 (** val fixpoint_rect_Type0 :
 231     property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 232     'a1 **)
 233 let rec fixpoint_rect_Type0 latt eqs h_mk_fixpoint x_18926 =
 234   let fix_lfp = x_18926 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   let yyy = xxx in yyy
 239
 240 (** val fixpoint_inv_rect_Type4 :
 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
 246 (** val fixpoint_inv_rect_Type3 :
 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
 252 (** val fixpoint_inv_rect_Type2 :
 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
 258 (** val fixpoint_inv_rect_Type1 :
 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
 264 (** val fixpoint_inv_rect_Type0 :
 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 =
 273   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
 274
 275 (** val fixpoint_jmdiscr :
 276     property_lattice -> equations -> fixpoint -> fixpoint -> __ **)
 277 let fixpoint_jmdiscr a1 a2 x y =
 278   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
 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
 297 (** val dpi1__o__fix_lfp :
 298     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
 301
 302 (** val eject__o__fix_lfp :
 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