extracted/fixpoints.mli

   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
  83 val property_lattice_rect_Type5 :
  84   (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  85   Bool.bool) -> 'a1) -> property_lattice -> 'a1
  86
  87 val property_lattice_rect_Type3 :
  88   (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  89   Bool.bool) -> 'a1) -> property_lattice -> 'a1
  90
  91 val property_lattice_rect_Type2 :
  92   (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  93   Bool.bool) -> 'a1) -> property_lattice -> 'a1
  94
  95 val property_lattice_rect_Type1 :
  96   (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
  97   Bool.bool) -> 'a1) -> property_lattice -> 'a1
  98
  99 val property_lattice_rect_Type0 :
 100   (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ -> Bool.bool) -> (__ ->
 101   Bool.bool) -> 'a1) -> property_lattice -> 'a1
 102
 103 type l_property
 104
 105 val l_bottom : property_lattice -> __
 106
 107 val l_equal : property_lattice -> __ -> __ -> Bool.bool
 108
 109 val l_included : property_lattice -> __ -> __ -> Bool.bool
 110
 111 val l_is_maximal : property_lattice -> __ -> Bool.bool
 112
 113 val property_lattice_inv_rect_Type4 :
 114   property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 115   Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
 116
 117 val property_lattice_inv_rect_Type3 :
 118   property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 119   Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
 120
 121 val property_lattice_inv_rect_Type2 :
 122   property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 123   Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
 124
 125 val property_lattice_inv_rect_Type1 :
 126   property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 127   Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
 128
 129 val property_lattice_inv_rect_Type0 :
 130   property_lattice -> (__ -> __ -> (__ -> __ -> Bool.bool) -> (__ -> __ ->
 131   Bool.bool) -> (__ -> Bool.bool) -> __ -> 'a1) -> 'a1
 132
 133 val property_lattice_jmdiscr : property_lattice -> property_lattice -> __
 134
 135 type valuation = Graphs.label -> __
 136
 137 type rhs = valuation -> __
 138
 139 type equations = Graphs.label -> rhs
 140
 141 type fixpoint =
 142   valuation
 143   (* singleton inductive, whose constructor was mk_fixpoint *)
 144
 145 val fixpoint_rect_Type4 :
 146   property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 147   'a1
 148
 149 val fixpoint_rect_Type5 :
 150   property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 151   'a1
 152
 153 val fixpoint_rect_Type3 :
 154   property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 155   'a1
 156
 157 val fixpoint_rect_Type2 :
 158   property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 159   'a1
 160
 161 val fixpoint_rect_Type1 :
 162   property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 163   'a1
 164
 165 val fixpoint_rect_Type0 :
 166   property_lattice -> equations -> (valuation -> __ -> 'a1) -> fixpoint ->
 167   'a1
 168
 169 val fix_lfp : property_lattice -> equations -> fixpoint -> valuation
 170
 171 val fixpoint_inv_rect_Type4 :
 172   property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
 173   -> 'a1
 174
 175 val fixpoint_inv_rect_Type3 :
 176   property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
 177   -> 'a1
 178
 179 val fixpoint_inv_rect_Type2 :
 180   property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
 181   -> 'a1
 182
 183 val fixpoint_inv_rect_Type1 :
 184   property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
 185   -> 'a1
 186
 187 val fixpoint_inv_rect_Type0 :
 188   property_lattice -> equations -> fixpoint -> (valuation -> __ -> __ -> 'a1)
 189   -> 'a1
 190
 191 val fixpoint_discr :
 192   property_lattice -> equations -> fixpoint -> fixpoint -> __
 193
 194 val fixpoint_jmdiscr :
 195   property_lattice -> equations -> fixpoint -> fixpoint -> __
 196
 197 val dpi1__o__fix_lfp__o__inject :
 198   property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
 199   Types.sig0
 200
 201 val eject__o__fix_lfp__o__inject :
 202   property_lattice -> equations -> fixpoint Types.sig0 -> valuation
 203   Types.sig0
 204
 205 val fix_lfp__o__inject :
 206   property_lattice -> equations -> fixpoint -> valuation Types.sig0
 207
 208 val dpi1__o__fix_lfp :
 209   property_lattice -> equations -> (fixpoint, 'a1) Types.dPair -> valuation
 210
 211 val eject__o__fix_lfp :
 212   property_lattice -> equations -> fixpoint Types.sig0 -> valuation
 213
 214 type fixpoint_computer = property_lattice -> equations -> fixpoint
 215
 216 val dpi1__o__apply_fixpoint :
 217   property_lattice -> equations -> (fixpoint, 'a1) Types.dPair ->
 218   Graphs.label -> __
 219
 220 val eject__o__apply_fixpoint :
 221   property_lattice -> equations -> fixpoint Types.sig0 -> Graphs.label -> __
 222