extracted/rTLabs_syntax.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 Proper
  12
  13 open PositiveMap
  14
  15 open Deqsets
  16
  17 open ErrorMessages
  18
  19 open PreIdentifiers
  20
  21 open Errors
  22
  23 open Extralib
  24
  25 open Lists
  26
  27 open Positive
  28
  29 open Identifiers
  30
  31 open Exp
  32
  33 open Arithmetic
  34
  35 open Vector
  36
  37 open Div_and_mod
  38
  39 open Util
  40
  41 open FoldStuff
  42
  43 open BitVector
  44
  45 open Jmeq
  46
  47 open Russell
  48
  49 open List
  50
  51 open Setoids
  52
  53 open Monad
  54
  55 open Option
  56
  57 open Extranat
  58
  59 open Bool
  60
  61 open Relations
  62
  63 open Nat
  64
  65 open Integers
  66
  67 open Types
  68
  69 open AST
  70
  71 open CostLabel
  72
  73 open FrontEndVal
  74
  75 open Hide
  76
  77 open ByteValues
  78
  79 open GenMem
  80
  81 open FrontEndMem
  82
  83 open Division
  84
  85 open Z
  86
  87 open BitVectorZ
  88
  89 open Pointers
  90
  91 open Coqlib
  92
  93 open Values
  94
  95 open FrontEndOps
  96
  97 open Order
  98
  99 open Registers
 100
 101 open BitVectorTrie
 102
 103 open Graphs
 104
 105 type statement =
 106 | St_skip of Graphs.label
 107 | St_cost of CostLabel.costlabel * Graphs.label
 108 | St_const of AST.typ * Registers.register * FrontEndOps.constant
 109    * Graphs.label
 110 | St_op1 of AST.typ * AST.typ * FrontEndOps.unary_operation
 111    * Registers.register * Registers.register * Graphs.label
 112 | St_op2 of AST.typ * AST.typ * AST.typ * FrontEndOps.binary_operation
 113    * Registers.register * Registers.register * Registers.register
 114    * Graphs.label
 115 | St_load of AST.typ * Registers.register * Registers.register * Graphs.label
 116 | St_store of AST.typ * Registers.register * Registers.register
 117    * Graphs.label
 118 | St_call_id of AST.ident * Registers.register List.list
 119    * Registers.register Types.option * Graphs.label
 120 | St_call_ptr of Registers.register * Registers.register List.list
 121    * Registers.register Types.option * Graphs.label
 122 | St_cond of Registers.register * Graphs.label * Graphs.label
 123 | St_return
 124
 125 (** val statement_rect_Type4 :
 126     (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 127     (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 128     'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 129     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 130     (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 131     Registers.register -> Registers.register -> Registers.register ->
 132     Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 133     Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 134     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 135     (AST.ident -> Registers.register List.list -> Registers.register
 136     Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 137     Registers.register List.list -> Registers.register Types.option ->
 138     Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
 139     Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
 140 let rec statement_rect_Type4 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
 141 | St_skip x_14903 -> h_St_skip x_14903
 142 | St_cost (x_14905, x_14904) -> h_St_cost x_14905 x_14904
 143 | St_const (t, x_14908, x_14907, x_14906) ->
 144   h_St_const t x_14908 x_14907 x_14906
 145 | St_op1 (t', t, x_14912, x_14911, x_14910, x_14909) ->
 146   h_St_op1 t' t x_14912 x_14911 x_14910 x_14909
 147 | St_op2 (t', t1, t2, x_14917, x_14916, x_14915, x_14914, x_14913) ->
 148   h_St_op2 t' t1 t2 x_14917 x_14916 x_14915 x_14914 x_14913
 149 | St_load (x_14921, x_14920, x_14919, x_14918) ->
 150   h_St_load x_14921 x_14920 x_14919 x_14918
 151 | St_store (x_14925, x_14924, x_14923, x_14922) ->
 152   h_St_store x_14925 x_14924 x_14923 x_14922
 153 | St_call_id (x_14929, x_14928, x_14927, x_14926) ->
 154   h_St_call_id x_14929 x_14928 x_14927 x_14926
 155 | St_call_ptr (x_14933, x_14932, x_14931, x_14930) ->
 156   h_St_call_ptr x_14933 x_14932 x_14931 x_14930
 157 | St_cond (x_14936, x_14935, x_14934) -> h_St_cond x_14936 x_14935 x_14934
 158 | St_return -> h_St_return
 159
 160 (** val statement_rect_Type5 :
 161     (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 162     (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 163     'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 164     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 165     (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 166     Registers.register -> Registers.register -> Registers.register ->
 167     Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 168     Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 169     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 170     (AST.ident -> Registers.register List.list -> Registers.register
 171     Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 172     Registers.register List.list -> Registers.register Types.option ->
 173     Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
 174     Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
 175 let rec statement_rect_Type5 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
 176 | St_skip x_14949 -> h_St_skip x_14949
 177 | St_cost (x_14951, x_14950) -> h_St_cost x_14951 x_14950
 178 | St_const (t, x_14954, x_14953, x_14952) ->
 179   h_St_const t x_14954 x_14953 x_14952
 180 | St_op1 (t', t, x_14958, x_14957, x_14956, x_14955) ->
 181   h_St_op1 t' t x_14958 x_14957 x_14956 x_14955
 182 | St_op2 (t', t1, t2, x_14963, x_14962, x_14961, x_14960, x_14959) ->
 183   h_St_op2 t' t1 t2 x_14963 x_14962 x_14961 x_14960 x_14959
 184 | St_load (x_14967, x_14966, x_14965, x_14964) ->
 185   h_St_load x_14967 x_14966 x_14965 x_14964
 186 | St_store (x_14971, x_14970, x_14969, x_14968) ->
 187   h_St_store x_14971 x_14970 x_14969 x_14968
 188 | St_call_id (x_14975, x_14974, x_14973, x_14972) ->
 189   h_St_call_id x_14975 x_14974 x_14973 x_14972
 190 | St_call_ptr (x_14979, x_14978, x_14977, x_14976) ->
 191   h_St_call_ptr x_14979 x_14978 x_14977 x_14976
 192 | St_cond (x_14982, x_14981, x_14980) -> h_St_cond x_14982 x_14981 x_14980
 193 | St_return -> h_St_return
 194
 195 (** val statement_rect_Type3 :
 196     (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 197     (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 198     'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 199     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 200     (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 201     Registers.register -> Registers.register -> Registers.register ->
 202     Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 203     Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 204     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 205     (AST.ident -> Registers.register List.list -> Registers.register
 206     Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 207     Registers.register List.list -> Registers.register Types.option ->
 208     Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
 209     Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
 210 let rec statement_rect_Type3 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
 211 | St_skip x_14995 -> h_St_skip x_14995
 212 | St_cost (x_14997, x_14996) -> h_St_cost x_14997 x_14996
 213 | St_const (t, x_15000, x_14999, x_14998) ->
 214   h_St_const t x_15000 x_14999 x_14998
 215 | St_op1 (t', t, x_15004, x_15003, x_15002, x_15001) ->
 216   h_St_op1 t' t x_15004 x_15003 x_15002 x_15001
 217 | St_op2 (t', t1, t2, x_15009, x_15008, x_15007, x_15006, x_15005) ->
 218   h_St_op2 t' t1 t2 x_15009 x_15008 x_15007 x_15006 x_15005
 219 | St_load (x_15013, x_15012, x_15011, x_15010) ->
 220   h_St_load x_15013 x_15012 x_15011 x_15010
 221 | St_store (x_15017, x_15016, x_15015, x_15014) ->
 222   h_St_store x_15017 x_15016 x_15015 x_15014
 223 | St_call_id (x_15021, x_15020, x_15019, x_15018) ->
 224   h_St_call_id x_15021 x_15020 x_15019 x_15018
 225 | St_call_ptr (x_15025, x_15024, x_15023, x_15022) ->
 226   h_St_call_ptr x_15025 x_15024 x_15023 x_15022
 227 | St_cond (x_15028, x_15027, x_15026) -> h_St_cond x_15028 x_15027 x_15026
 228 | St_return -> h_St_return
 229
 230 (** val statement_rect_Type2 :
 231     (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 232     (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 233     'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 234     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 235     (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 236     Registers.register -> Registers.register -> Registers.register ->
 237     Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 238     Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 239     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 240     (AST.ident -> Registers.register List.list -> Registers.register
 241     Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 242     Registers.register List.list -> Registers.register Types.option ->
 243     Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
 244     Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
 245 let rec statement_rect_Type2 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
 246 | St_skip x_15041 -> h_St_skip x_15041
 247 | St_cost (x_15043, x_15042) -> h_St_cost x_15043 x_15042
 248 | St_const (t, x_15046, x_15045, x_15044) ->
 249   h_St_const t x_15046 x_15045 x_15044
 250 | St_op1 (t', t, x_15050, x_15049, x_15048, x_15047) ->
 251   h_St_op1 t' t x_15050 x_15049 x_15048 x_15047
 252 | St_op2 (t', t1, t2, x_15055, x_15054, x_15053, x_15052, x_15051) ->
 253   h_St_op2 t' t1 t2 x_15055 x_15054 x_15053 x_15052 x_15051
 254 | St_load (x_15059, x_15058, x_15057, x_15056) ->
 255   h_St_load x_15059 x_15058 x_15057 x_15056
 256 | St_store (x_15063, x_15062, x_15061, x_15060) ->
 257   h_St_store x_15063 x_15062 x_15061 x_15060
 258 | St_call_id (x_15067, x_15066, x_15065, x_15064) ->
 259   h_St_call_id x_15067 x_15066 x_15065 x_15064
 260 | St_call_ptr (x_15071, x_15070, x_15069, x_15068) ->
 261   h_St_call_ptr x_15071 x_15070 x_15069 x_15068
 262 | St_cond (x_15074, x_15073, x_15072) -> h_St_cond x_15074 x_15073 x_15072
 263 | St_return -> h_St_return
 264
 265 (** val statement_rect_Type1 :
 266     (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 267     (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 268     'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 269     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 270     (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 271     Registers.register -> Registers.register -> Registers.register ->
 272     Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 273     Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 274     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 275     (AST.ident -> Registers.register List.list -> Registers.register
 276     Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 277     Registers.register List.list -> Registers.register Types.option ->
 278     Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
 279     Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
 280 let rec statement_rect_Type1 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
 281 | St_skip x_15087 -> h_St_skip x_15087
 282 | St_cost (x_15089, x_15088) -> h_St_cost x_15089 x_15088
 283 | St_const (t, x_15092, x_15091, x_15090) ->
 284   h_St_const t x_15092 x_15091 x_15090
 285 | St_op1 (t', t, x_15096, x_15095, x_15094, x_15093) ->
 286   h_St_op1 t' t x_15096 x_15095 x_15094 x_15093
 287 | St_op2 (t', t1, t2, x_15101, x_15100, x_15099, x_15098, x_15097) ->
 288   h_St_op2 t' t1 t2 x_15101 x_15100 x_15099 x_15098 x_15097
 289 | St_load (x_15105, x_15104, x_15103, x_15102) ->
 290   h_St_load x_15105 x_15104 x_15103 x_15102
 291 | St_store (x_15109, x_15108, x_15107, x_15106) ->
 292   h_St_store x_15109 x_15108 x_15107 x_15106
 293 | St_call_id (x_15113, x_15112, x_15111, x_15110) ->
 294   h_St_call_id x_15113 x_15112 x_15111 x_15110
 295 | St_call_ptr (x_15117, x_15116, x_15115, x_15114) ->
 296   h_St_call_ptr x_15117 x_15116 x_15115 x_15114
 297 | St_cond (x_15120, x_15119, x_15118) -> h_St_cond x_15120 x_15119 x_15118
 298 | St_return -> h_St_return
 299
 300 (** val statement_rect_Type0 :
 301     (Graphs.label -> 'a1) -> (CostLabel.costlabel -> Graphs.label -> 'a1) ->
 302     (AST.typ -> Registers.register -> FrontEndOps.constant -> Graphs.label ->
 303     'a1) -> (AST.typ -> AST.typ -> FrontEndOps.unary_operation ->
 304     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 305     (AST.typ -> AST.typ -> AST.typ -> FrontEndOps.binary_operation ->
 306     Registers.register -> Registers.register -> Registers.register ->
 307     Graphs.label -> 'a1) -> (AST.typ -> Registers.register ->
 308     Registers.register -> Graphs.label -> 'a1) -> (AST.typ ->
 309     Registers.register -> Registers.register -> Graphs.label -> 'a1) ->
 310     (AST.ident -> Registers.register List.list -> Registers.register
 311     Types.option -> Graphs.label -> 'a1) -> (Registers.register ->
 312     Registers.register List.list -> Registers.register Types.option ->
 313     Graphs.label -> 'a1) -> (Registers.register -> Graphs.label ->
 314     Graphs.label -> 'a1) -> 'a1 -> statement -> 'a1 **)
 315 let rec statement_rect_Type0 h_St_skip h_St_cost h_St_const h_St_op1 h_St_op2 h_St_load h_St_store h_St_call_id h_St_call_ptr h_St_cond h_St_return = function
 316 | St_skip x_15133 -> h_St_skip x_15133
 317 | St_cost (x_15135, x_15134) -> h_St_cost x_15135 x_15134
 318 | St_const (t, x_15138, x_15137, x_15136) ->
 319   h_St_const t x_15138 x_15137 x_15136
 320 | St_op1 (t', t, x_15142, x_15141, x_15140, x_15139) ->
 321   h_St_op1 t' t x_15142 x_15141 x_15140 x_15139
 322 | St_op2 (t', t1, t2, x_15147, x_15146, x_15145, x_15144, x_15143) ->
 323   h_St_op2 t' t1 t2 x_15147 x_15146 x_15145 x_15144 x_15143
 324 | St_load (x_15151, x_15150, x_15149, x_15148) ->
 325   h_St_load x_15151 x_15150 x_15149 x_15148
 326 | St_store (x_15155, x_15154, x_15153, x_15152) ->
 327   h_St_store x_15155 x_15154 x_15153 x_15152
 328 | St_call_id (x_15159, x_15158, x_15157, x_15156) ->
 329   h_St_call_id x_15159 x_15158 x_15157 x_15156
 330 | St_call_ptr (x_15163, x_15162, x_15161, x_15160) ->
 331   h_St_call_ptr x_15163 x_15162 x_15161 x_15160
 332 | St_cond (x_15166, x_15165, x_15164) -> h_St_cond x_15166 x_15165 x_15164
 333 | St_return -> h_St_return
 334
 335 (** val statement_inv_rect_Type4 :
 336     statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 337     Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 338     FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 339     -> FrontEndOps.unary_operation -> Registers.register ->
 340     Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 341     -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
 342     Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 343     (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
 344     __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
 345     Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
 346     -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
 347     (Registers.register -> Registers.register List.list -> Registers.register
 348     Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 349     Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 350 let statement_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
 351   let hcut = statement_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
 352   hcut __
 353
 354 (** val statement_inv_rect_Type3 :
 355     statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 356     Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 357     FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 358     -> FrontEndOps.unary_operation -> Registers.register ->
 359     Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 360     -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
 361     Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 362     (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
 363     __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
 364     Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
 365     -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
 366     (Registers.register -> Registers.register List.list -> Registers.register
 367     Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 368     Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 369 let statement_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
 370   let hcut = statement_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
 371   hcut __
 372
 373 (** val statement_inv_rect_Type2 :
 374     statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 375     Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 376     FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 377     -> FrontEndOps.unary_operation -> Registers.register ->
 378     Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 379     -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
 380     Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 381     (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
 382     __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
 383     Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
 384     -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
 385     (Registers.register -> Registers.register List.list -> Registers.register
 386     Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 387     Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 388 let statement_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
 389   let hcut = statement_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
 390   hcut __
 391
 392 (** val statement_inv_rect_Type1 :
 393     statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 394     Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 395     FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 396     -> FrontEndOps.unary_operation -> Registers.register ->
 397     Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 398     -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
 399     Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 400     (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
 401     __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
 402     Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
 403     -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
 404     (Registers.register -> Registers.register List.list -> Registers.register
 405     Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 406     Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 407 let statement_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
 408   let hcut = statement_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
 409   hcut __
 410
 411 (** val statement_inv_rect_Type0 :
 412     statement -> (Graphs.label -> __ -> 'a1) -> (CostLabel.costlabel ->
 413     Graphs.label -> __ -> 'a1) -> (AST.typ -> Registers.register ->
 414     FrontEndOps.constant -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 415     -> FrontEndOps.unary_operation -> Registers.register ->
 416     Registers.register -> Graphs.label -> __ -> 'a1) -> (AST.typ -> AST.typ
 417     -> AST.typ -> FrontEndOps.binary_operation -> Registers.register ->
 418     Registers.register -> Registers.register -> Graphs.label -> __ -> 'a1) ->
 419     (AST.typ -> Registers.register -> Registers.register -> Graphs.label ->
 420     __ -> 'a1) -> (AST.typ -> Registers.register -> Registers.register ->
 421     Graphs.label -> __ -> 'a1) -> (AST.ident -> Registers.register List.list
 422     -> Registers.register Types.option -> Graphs.label -> __ -> 'a1) ->
 423     (Registers.register -> Registers.register List.list -> Registers.register
 424     Types.option -> Graphs.label -> __ -> 'a1) -> (Registers.register ->
 425     Graphs.label -> Graphs.label -> __ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 426 let statement_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 =
 427   let hcut = statement_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 hterm in
 428   hcut __
 429
 430 (** val statement_jmdiscr : statement -> statement -> __ **)
 431 let statement_jmdiscr x y =
 432   Logic.eq_rect_Type2 x
 433     (match x with
 434      | St_skip a0 -> Obj.magic (fun _ dH -> dH __)
 435      | St_cost (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 436      | St_const (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 437      | St_op1 (a0, a1, a2, a3, a4, a5) ->
 438        Obj.magic (fun _ dH -> dH __ __ __ __ __ __)
 439      | St_op2 (a0, a1, a2, a3, a4, a5, a6, a7) ->
 440        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __)
 441      | St_load (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 442      | St_store (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 443      | St_call_id (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 444      | St_call_ptr (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
 445      | St_cond (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 446      | St_return -> Obj.magic (fun _ dH -> dH)) y
 447
 448 type internal_function = { f_labgen : Identifiers.universe;
 449                            f_reggen : Identifiers.universe;
 450                            f_result : (Registers.register, AST.typ)
 451                                       Types.prod Types.option;
 452                            f_params : (Registers.register, AST.typ)
 453                                       Types.prod List.list;
 454                            f_locals : (Registers.register, AST.typ)
 455                                       Types.prod List.list;
 456                            f_stacksize : Nat.nat;
 457                            f_graph : statement Graphs.graph;
 458                            f_entry : Graphs.label Types.sig0;
 459                            f_exit : Graphs.label Types.sig0 }
 460
 461 (** val internal_function_rect_Type4 :
 462     (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 463     AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 464     Types.prod List.list -> (Registers.register, AST.typ) Types.prod
 465     List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
 466     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 467     internal_function -> 'a1 **)
 468 let rec internal_function_rect_Type4 h_mk_internal_function x_15456 =
 469   let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
 470     f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
 471     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15456
 472   in
 473   h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
 474     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
 475
 476 (** val internal_function_rect_Type5 :
 477     (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 478     AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 479     Types.prod List.list -> (Registers.register, AST.typ) Types.prod
 480     List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
 481     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 482     internal_function -> 'a1 **)
 483 let rec internal_function_rect_Type5 h_mk_internal_function x_15458 =
 484   let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
 485     f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
 486     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15458
 487   in
 488   h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
 489     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
 490
 491 (** val internal_function_rect_Type3 :
 492     (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 493     AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 494     Types.prod List.list -> (Registers.register, AST.typ) Types.prod
 495     List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
 496     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 497     internal_function -> 'a1 **)
 498 let rec internal_function_rect_Type3 h_mk_internal_function x_15460 =
 499   let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
 500     f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
 501     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15460
 502   in
 503   h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
 504     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
 505
 506 (** val internal_function_rect_Type2 :
 507     (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 508     AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 509     Types.prod List.list -> (Registers.register, AST.typ) Types.prod
 510     List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
 511     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 512     internal_function -> 'a1 **)
 513 let rec internal_function_rect_Type2 h_mk_internal_function x_15462 =
 514   let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
 515     f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
 516     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15462
 517   in
 518   h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
 519     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
 520
 521 (** val internal_function_rect_Type1 :
 522     (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 523     AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 524     Types.prod List.list -> (Registers.register, AST.typ) Types.prod
 525     List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
 526     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 527     internal_function -> 'a1 **)
 528 let rec internal_function_rect_Type1 h_mk_internal_function x_15464 =
 529   let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
 530     f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
 531     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15464
 532   in
 533   h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
 534     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
 535
 536 (** val internal_function_rect_Type0 :
 537     (Identifiers.universe -> Identifiers.universe -> (Registers.register,
 538     AST.typ) Types.prod Types.option -> (Registers.register, AST.typ)
 539     Types.prod List.list -> (Registers.register, AST.typ) Types.prod
 540     List.list -> Nat.nat -> statement Graphs.graph -> __ -> __ ->
 541     Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 542     internal_function -> 'a1 **)
 543 let rec internal_function_rect_Type0 h_mk_internal_function x_15466 =
 544   let { f_labgen = f_labgen0; f_reggen = f_reggen0; f_result = f_result0;
 545     f_params = f_params0; f_locals = f_locals0; f_stacksize = f_stacksize0;
 546     f_graph = f_graph0; f_entry = f_entry0; f_exit = f_exit0 } = x_15466
 547   in
 548   h_mk_internal_function f_labgen0 f_reggen0 f_result0 f_params0 f_locals0
 549     f_stacksize0 f_graph0 __ __ f_entry0 f_exit0 __
 550
 551 (** val f_labgen : internal_function -> Identifiers.universe **)
 552 let rec f_labgen xxx =
 553   xxx.f_labgen
 554
 555 (** val f_reggen : internal_function -> Identifiers.universe **)
 556 let rec f_reggen xxx =
 557   xxx.f_reggen
 558
 559 (** val f_result :
 560     internal_function -> (Registers.register, AST.typ) Types.prod
 561     Types.option **)
 562 let rec f_result xxx =
 563   xxx.f_result
 564
 565 (** val f_params :
 566     internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
 567 let rec f_params xxx =
 568   xxx.f_params
 569
 570 (** val f_locals :
 571     internal_function -> (Registers.register, AST.typ) Types.prod List.list **)
 572 let rec f_locals xxx =
 573   xxx.f_locals
 574
 575 (** val f_stacksize : internal_function -> Nat.nat **)
 576 let rec f_stacksize xxx =
 577   xxx.f_stacksize
 578
 579 (** val f_graph : internal_function -> statement Graphs.graph **)
 580 let rec f_graph xxx =
 581   xxx.f_graph
 582
 583 (** val f_entry : internal_function -> Graphs.label Types.sig0 **)
 584 let rec f_entry xxx =
 585   xxx.f_entry
 586
 587 (** val f_exit : internal_function -> Graphs.label Types.sig0 **)
 588 let rec f_exit xxx =
 589   xxx.f_exit
 590
 591 (** val internal_function_inv_rect_Type4 :
 592     internal_function -> (Identifiers.universe -> Identifiers.universe ->
 593     (Registers.register, AST.typ) Types.prod Types.option ->
 594     (Registers.register, AST.typ) Types.prod List.list ->
 595     (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
 596     statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
 597     Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 598 let internal_function_inv_rect_Type4 hterm h1 =
 599   let hcut = internal_function_rect_Type4 h1 hterm in hcut __
 600
 601 (** val internal_function_inv_rect_Type3 :
 602     internal_function -> (Identifiers.universe -> Identifiers.universe ->
 603     (Registers.register, AST.typ) Types.prod Types.option ->
 604     (Registers.register, AST.typ) Types.prod List.list ->
 605     (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
 606     statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
 607     Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 608 let internal_function_inv_rect_Type3 hterm h1 =
 609   let hcut = internal_function_rect_Type3 h1 hterm in hcut __
 610
 611 (** val internal_function_inv_rect_Type2 :
 612     internal_function -> (Identifiers.universe -> Identifiers.universe ->
 613     (Registers.register, AST.typ) Types.prod Types.option ->
 614     (Registers.register, AST.typ) Types.prod List.list ->
 615     (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
 616     statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
 617     Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 618 let internal_function_inv_rect_Type2 hterm h1 =
 619   let hcut = internal_function_rect_Type2 h1 hterm in hcut __
 620
 621 (** val internal_function_inv_rect_Type1 :
 622     internal_function -> (Identifiers.universe -> Identifiers.universe ->
 623     (Registers.register, AST.typ) Types.prod Types.option ->
 624     (Registers.register, AST.typ) Types.prod List.list ->
 625     (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
 626     statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
 627     Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 628 let internal_function_inv_rect_Type1 hterm h1 =
 629   let hcut = internal_function_rect_Type1 h1 hterm in hcut __
 630
 631 (** val internal_function_inv_rect_Type0 :
 632     internal_function -> (Identifiers.universe -> Identifiers.universe ->
 633     (Registers.register, AST.typ) Types.prod Types.option ->
 634     (Registers.register, AST.typ) Types.prod List.list ->
 635     (Registers.register, AST.typ) Types.prod List.list -> Nat.nat ->
 636     statement Graphs.graph -> __ -> __ -> Graphs.label Types.sig0 ->
 637     Graphs.label Types.sig0 -> __ -> __ -> 'a1) -> 'a1 **)
 638 let internal_function_inv_rect_Type0 hterm h1 =
 639   let hcut = internal_function_rect_Type0 h1 hterm in hcut __
 640
 641 (** val internal_function_jmdiscr :
 642     internal_function -> internal_function -> __ **)
 643 let internal_function_jmdiscr x y =
 644   Logic.eq_rect_Type2 x
 645     (let { f_labgen = a0; f_reggen = a1; f_result = a2; f_params = a3;
 646        f_locals = a4; f_stacksize = a5; f_graph = a6; f_entry = a9; f_exit =
 647        a10 } = x
 648      in
 649     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __)) y
 650
 651 type rTLabs_program =
 652   (internal_function AST.fundef, AST.init_data List.list) AST.program
 653