extracted/positiveMap.mli

   1 open Preamble
   2
   3 open Hints_declaration
   4
   5 open Core_notation
   6
   7 open Pts
   8
   9 open Logic
  10
  11 open Types
  12
  13 open Bool
  14
  15 open Relations
  16
  17 open Nat
  18
  19 open Positive
  20
  21 open Div_and_mod
  22
  23 open Jmeq
  24
  25 open Russell
  26
  27 open List
  28
  29 open Util
  30
  31 open Setoids
  32
  33 open Monad
  34
  35 open Option
  36
  37 type 'a positive_map =
  38 | Pm_leaf
  39 | Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
  40
  41 val positive_map_rect_Type4 :
  42   'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  43   'a2 -> 'a2) -> 'a1 positive_map -> 'a2
  44
  45 val positive_map_rect_Type3 :
  46   'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  47   'a2 -> 'a2) -> 'a1 positive_map -> 'a2
  48
  49 val positive_map_rect_Type2 :
  50   'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  51   'a2 -> 'a2) -> 'a1 positive_map -> 'a2
  52
  53 val positive_map_rect_Type1 :
  54   'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  55   'a2 -> 'a2) -> 'a1 positive_map -> 'a2
  56
  57 val positive_map_rect_Type0 :
  58   'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2 ->
  59   'a2 -> 'a2) -> 'a1 positive_map -> 'a2
  60
  61 val positive_map_inv_rect_Type4 :
  62   'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  63   'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
  64
  65 val positive_map_inv_rect_Type3 :
  66   'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  67   'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
  68
  69 val positive_map_inv_rect_Type2 :
  70   'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  71   'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
  72
  73 val positive_map_inv_rect_Type1 :
  74   'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  75   'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
  76
  77 val positive_map_inv_rect_Type0 :
  78   'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map ->
  79   'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2
  80
  81 val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __
  82
  83 val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __
  84
  85 val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option
  86
  87 val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1
  88
  89 val pm_set :
  90   Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map
  91
  92 val insert : Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map
  93
  94 val update :
  95   Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option
  96
  97 val fold :
  98   (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2
  99
 100 val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map
 101
 102 val is_none : 'a1 Types.option -> Bool.bool
 103
 104 val is_pm_leaf : 'a1 positive_map -> Bool.bool
 105
 106 val map_opt :
 107   ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map
 108
 109 val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map
 110
 111 val merge :
 112   ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
 113   positive_map -> 'a2 positive_map -> 'a3 positive_map
 114
 115 val domain_size : 'a1 positive_map -> Nat.nat
 116
 117 val pm_all_aux :
 118   'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
 119   (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool
 120
 121 val pm_all :
 122   'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool
 123
 124 val pm_choose :
 125   'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
 126   Types.prod Types.option
 127
 128 val pm_try_remove :
 129   Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
 130   Types.option
 131
 132 val pm_fold_inf_aux :
 133   'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
 134   positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2
 135
 136 val pm_fold_inf :
 137   'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2
 138
 139 val pm_find_aux :
 140   (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos -> 'a1
 141   -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option
 142
 143 val pm_find :
 144   'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
 145   'a1) Types.prod Types.option
 146