extracted/preIdentifiers.ml

   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 type identifierTag =
  22 | Label
  23 | CostTag
  24 | RegisterTag
  25 | LabelTag
  26 | SymbolTag
  27 | ASMTag
  28
  29 (** val identifierTag_rect_Type4 :
  30     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
  31 let rec identifierTag_rect_Type4 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
  32 | Label -> h_Label
  33 | CostTag -> h_CostTag
  34 | RegisterTag -> h_RegisterTag
  35 | LabelTag -> h_LabelTag
  36 | SymbolTag -> h_SymbolTag
  37 | ASMTag -> h_ASMTag
  38
  39 (** val identifierTag_rect_Type5 :
  40     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
  41 let rec identifierTag_rect_Type5 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
  42 | Label -> h_Label
  43 | CostTag -> h_CostTag
  44 | RegisterTag -> h_RegisterTag
  45 | LabelTag -> h_LabelTag
  46 | SymbolTag -> h_SymbolTag
  47 | ASMTag -> h_ASMTag
  48
  49 (** val identifierTag_rect_Type3 :
  50     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
  51 let rec identifierTag_rect_Type3 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
  52 | Label -> h_Label
  53 | CostTag -> h_CostTag
  54 | RegisterTag -> h_RegisterTag
  55 | LabelTag -> h_LabelTag
  56 | SymbolTag -> h_SymbolTag
  57 | ASMTag -> h_ASMTag
  58
  59 (** val identifierTag_rect_Type2 :
  60     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
  61 let rec identifierTag_rect_Type2 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
  62 | Label -> h_Label
  63 | CostTag -> h_CostTag
  64 | RegisterTag -> h_RegisterTag
  65 | LabelTag -> h_LabelTag
  66 | SymbolTag -> h_SymbolTag
  67 | ASMTag -> h_ASMTag
  68
  69 (** val identifierTag_rect_Type1 :
  70     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
  71 let rec identifierTag_rect_Type1 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
  72 | Label -> h_Label
  73 | CostTag -> h_CostTag
  74 | RegisterTag -> h_RegisterTag
  75 | LabelTag -> h_LabelTag
  76 | SymbolTag -> h_SymbolTag
  77 | ASMTag -> h_ASMTag
  78
  79 (** val identifierTag_rect_Type0 :
  80     'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> identifierTag -> 'a1 **)
  81 let rec identifierTag_rect_Type0 h_Label h_CostTag h_RegisterTag h_LabelTag h_SymbolTag h_ASMTag = function
  82 | Label -> h_Label
  83 | CostTag -> h_CostTag
  84 | RegisterTag -> h_RegisterTag
  85 | LabelTag -> h_LabelTag
  86 | SymbolTag -> h_SymbolTag
  87 | ASMTag -> h_ASMTag
  88
  89 (** val identifierTag_inv_rect_Type4 :
  90     identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  91     -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  92 let identifierTag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 =
  93   let hcut = identifierTag_rect_Type4 h1 h2 h3 h4 h5 h6 hterm in hcut __
  94
  95 (** val identifierTag_inv_rect_Type3 :
  96     identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
  97     -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
  98 let identifierTag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 =
  99   let hcut = identifierTag_rect_Type3 h1 h2 h3 h4 h5 h6 hterm in hcut __
 100
 101 (** val identifierTag_inv_rect_Type2 :
 102     identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 103     -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 104 let identifierTag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 =
 105   let hcut = identifierTag_rect_Type2 h1 h2 h3 h4 h5 h6 hterm in hcut __
 106
 107 (** val identifierTag_inv_rect_Type1 :
 108     identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 109     -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 110 let identifierTag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 =
 111   let hcut = identifierTag_rect_Type1 h1 h2 h3 h4 h5 h6 hterm in hcut __
 112
 113 (** val identifierTag_inv_rect_Type0 :
 114     identifierTag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1)
 115     -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 116 let identifierTag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 =
 117   let hcut = identifierTag_rect_Type0 h1 h2 h3 h4 h5 h6 hterm in hcut __
 118
 119 (** val identifierTag_discr : identifierTag -> identifierTag -> __ **)
 120 let identifierTag_discr x y =
 121   Logic.eq_rect_Type2 x
 122     (match x with
 123      | Label -> Obj.magic (fun _ dH -> dH)
 124      | CostTag -> Obj.magic (fun _ dH -> dH)
 125      | RegisterTag -> Obj.magic (fun _ dH -> dH)
 126      | LabelTag -> Obj.magic (fun _ dH -> dH)
 127      | SymbolTag -> Obj.magic (fun _ dH -> dH)
 128      | ASMTag -> Obj.magic (fun _ dH -> dH)) y
 129
 130 type identifier =
 131   Positive.pos
 132   (* singleton inductive, whose constructor was an_identifier *)
 133
 134 (** val identifier_rect_Type4 :
 135     identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
 136 let rec identifier_rect_Type4 tag h_an_identifier x_2070 =
 137   let x_2071 = x_2070 in h_an_identifier x_2071
 138
 139 (** val identifier_rect_Type5 :
 140     identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
 141 let rec identifier_rect_Type5 tag h_an_identifier x_2073 =
 142   let x_2074 = x_2073 in h_an_identifier x_2074
 143
 144 (** val identifier_rect_Type3 :
 145     identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
 146 let rec identifier_rect_Type3 tag h_an_identifier x_2076 =
 147   let x_2077 = x_2076 in h_an_identifier x_2077
 148
 149 (** val identifier_rect_Type2 :
 150     identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
 151 let rec identifier_rect_Type2 tag h_an_identifier x_2079 =
 152   let x_2080 = x_2079 in h_an_identifier x_2080
 153
 154 (** val identifier_rect_Type1 :
 155     identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
 156 let rec identifier_rect_Type1 tag h_an_identifier x_2082 =
 157   let x_2083 = x_2082 in h_an_identifier x_2083
 158
 159 (** val identifier_rect_Type0 :
 160     identifierTag -> (Positive.pos -> 'a1) -> identifier -> 'a1 **)
 161 let rec identifier_rect_Type0 tag h_an_identifier x_2085 =
 162   let x_2086 = x_2085 in h_an_identifier x_2086
 163
 164 (** val identifier_inv_rect_Type4 :
 165     identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
 166 let identifier_inv_rect_Type4 x1 hterm h1 =
 167   let hcut = identifier_rect_Type4 x1 h1 hterm in hcut __
 168
 169 (** val identifier_inv_rect_Type3 :
 170     identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
 171 let identifier_inv_rect_Type3 x1 hterm h1 =
 172   let hcut = identifier_rect_Type3 x1 h1 hterm in hcut __
 173
 174 (** val identifier_inv_rect_Type2 :
 175     identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
 176 let identifier_inv_rect_Type2 x1 hterm h1 =
 177   let hcut = identifier_rect_Type2 x1 h1 hterm in hcut __
 178
 179 (** val identifier_inv_rect_Type1 :
 180     identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
 181 let identifier_inv_rect_Type1 x1 hterm h1 =
 182   let hcut = identifier_rect_Type1 x1 h1 hterm in hcut __
 183
 184 (** val identifier_inv_rect_Type0 :
 185     identifierTag -> identifier -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
 186 let identifier_inv_rect_Type0 x1 hterm h1 =
 187   let hcut = identifier_rect_Type0 x1 h1 hterm in hcut __
 188
 189 (** val identifier_discr :
 190     identifierTag -> identifier -> identifier -> __ **)
 191 let identifier_discr a1 x y =
 192   Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
 193