extracted/toRTLabs.mli

   1 open Preamble
   2
   3 open Setoids
   4
   5 open Monad
   6
   7 open Option
   8
   9 open Div_and_mod
  10
  11 open Jmeq
  12
  13 open Russell
  14
  15 open Util
  16
  17 open Bool
  18
  19 open Relations
  20
  21 open Nat
  22
  23 open Hints_declaration
  24
  25 open Core_notation
  26
  27 open Pts
  28
  29 open Logic
  30
  31 open Types
  32
  33 open List
  34
  35 open Lists
  36
  37 open Extra_bool
  38
  39 open Coqlib
  40
  41 open Values
  42
  43 open FrontEndVal
  44
  45 open Hide
  46
  47 open ByteValues
  48
  49 open Division
  50
  51 open Z
  52
  53 open BitVectorZ
  54
  55 open Pointers
  56
  57 open GenMem
  58
  59 open FrontEndMem
  60
  61 open Proper
  62
  63 open PositiveMap
  64
  65 open Deqsets
  66
  67 open Extralib
  68
  69 open Identifiers
  70
  71 open Exp
  72
  73 open Arithmetic
  74
  75 open Vector
  76
  77 open FoldStuff
  78
  79 open BitVector
  80
  81 open Extranat
  82
  83 open Integers
  84
  85 open AST
  86
  87 open ErrorMessages
  88
  89 open Positive
  90
  91 open PreIdentifiers
  92
  93 open Errors
  94
  95 open Globalenvs
  96
  97 open CostLabel
  98
  99 open FrontEndOps
 100
 101 open Cminor_syntax
 102
 103 open BitVectorTrie
 104
 105 open Graphs
 106
 107 open Order
 108
 109 open Registers
 110
 111 open RTLabs_syntax
 112
 113 type env =
 114   (Registers.register, AST.typ) Types.prod Identifiers.identifier_map
 115
 116 val populate_env :
 117   env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list ->
 118   (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
 119   Identifiers.universe) Types.prod
 120
 121 val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register
 122
 123 type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
 124                fx_rettyp : AST.typ Types.option }
 125
 126 val fixed_rect_Type4 :
 127   (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
 128   -> 'a1
 129
 130 val fixed_rect_Type5 :
 131   (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
 132   -> 'a1
 133
 134 val fixed_rect_Type3 :
 135   (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
 136   -> 'a1
 137
 138 val fixed_rect_Type2 :
 139   (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
 140   -> 'a1
 141
 142 val fixed_rect_Type1 :
 143   (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
 144   -> 'a1
 145
 146 val fixed_rect_Type0 :
 147   (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
 148   -> 'a1
 149
 150 val fx_gotos : fixed -> Identifiers.identifier_set
 151
 152 val fx_env : fixed -> env
 153
 154 val fx_rettyp : fixed -> AST.typ Types.option
 155
 156 val fixed_inv_rect_Type4 :
 157   fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 158   -> 'a1) -> 'a1
 159
 160 val fixed_inv_rect_Type3 :
 161   fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 162   -> 'a1) -> 'a1
 163
 164 val fixed_inv_rect_Type2 :
 165   fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 166   -> 'a1) -> 'a1
 167
 168 val fixed_inv_rect_Type1 :
 169   fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 170   -> 'a1) -> 'a1
 171
 172 val fixed_inv_rect_Type0 :
 173   fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
 174   -> 'a1) -> 'a1
 175
 176 val fixed_discr : fixed -> fixed -> __
 177
 178 val fixed_jmdiscr : fixed -> fixed -> __
 179
 180 type resultok = __
 181
 182 type goto_map =
 183   PreIdentifiers.identifier Identifiers.identifier_map
 184   (* singleton inductive, whose constructor was mk_goto_map *)
 185
 186 val goto_map_rect_Type4 :
 187   fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
 188   Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
 189
 190 val goto_map_rect_Type5 :
 191   fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
 192   Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
 193
 194 val goto_map_rect_Type3 :
 195   fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
 196   Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
 197
 198 val goto_map_rect_Type2 :
 199   fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
 200   Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
 201
 202 val goto_map_rect_Type1 :
 203   fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
 204   Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
 205
 206 val goto_map_rect_Type0 :
 207   fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
 208   Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1
 209
 210 val gm_map :
 211   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 212   PreIdentifiers.identifier Identifiers.identifier_map
 213
 214 val goto_map_inv_rect_Type4 :
 215   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 216   (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
 217   'a1) -> 'a1
 218
 219 val goto_map_inv_rect_Type3 :
 220   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 221   (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
 222   'a1) -> 'a1
 223
 224 val goto_map_inv_rect_Type2 :
 225   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 226   (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
 227   'a1) -> 'a1
 228
 229 val goto_map_inv_rect_Type1 :
 230   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 231   (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
 232   'a1) -> 'a1
 233
 234 val goto_map_inv_rect_Type0 :
 235   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 236   (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
 237   'a1) -> 'a1
 238
 239 val goto_map_discr :
 240   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __
 241
 242 val goto_map_jmdiscr :
 243   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __
 244
 245 val dpi1__o__gm_map__o__inject :
 246   fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
 247   Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
 248   Types.sig0
 249
 250 val eject__o__gm_map__o__inject :
 251   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
 252   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0
 253
 254 val gm_map__o__inject :
 255   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
 256   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0
 257
 258 val dpi1__o__gm_map :
 259   fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
 260   Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
 261
 262 val eject__o__gm_map :
 263   fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
 264   PreIdentifiers.identifier Identifiers.identifier_map
 265
 266 type partial_fn = { pf_labgen : Identifiers.universe;
 267                     pf_reggen : Identifiers.universe;
 268                     pf_params : (Registers.register, AST.typ) Types.prod
 269                                 List.list;
 270                     pf_locals : (Registers.register, AST.typ) Types.prod
 271                                 List.list; pf_result : resultok;
 272                     pf_stacksize : Nat.nat;
 273                     pf_graph : RTLabs_syntax.statement Graphs.graph;
 274                     pf_gotos : goto_map;
 275                     pf_labels : PreIdentifiers.identifier
 276                                 Identifiers.identifier_map Types.sig0;
 277                     pf_entry : Graphs.label Types.sig0;
 278                     pf_exit : Graphs.label Types.sig0 }
 279
 280 val partial_fn_rect_Type4 :
 281   fixed -> (Identifiers.universe -> Identifiers.universe ->
 282   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 283   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 284   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 285   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 286   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 287   partial_fn -> 'a1
 288
 289 val partial_fn_rect_Type5 :
 290   fixed -> (Identifiers.universe -> Identifiers.universe ->
 291   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 292   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 293   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 294   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 295   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 296   partial_fn -> 'a1
 297
 298 val partial_fn_rect_Type3 :
 299   fixed -> (Identifiers.universe -> Identifiers.universe ->
 300   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 301   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 302   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 303   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 304   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 305   partial_fn -> 'a1
 306
 307 val partial_fn_rect_Type2 :
 308   fixed -> (Identifiers.universe -> Identifiers.universe ->
 309   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 310   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 311   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 312   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 313   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 314   partial_fn -> 'a1
 315
 316 val partial_fn_rect_Type1 :
 317   fixed -> (Identifiers.universe -> Identifiers.universe ->
 318   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 319   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 320   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 321   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 322   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 323   partial_fn -> 'a1
 324
 325 val partial_fn_rect_Type0 :
 326   fixed -> (Identifiers.universe -> Identifiers.universe ->
 327   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 328   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 329   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 330   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 331   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
 332   partial_fn -> 'a1
 333
 334 val pf_labgen : fixed -> partial_fn -> Identifiers.universe
 335
 336 val pf_reggen : fixed -> partial_fn -> Identifiers.universe
 337
 338 val pf_params :
 339   fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list
 340
 341 val pf_locals :
 342   fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list
 343
 344 val pf_result : fixed -> partial_fn -> resultok
 345
 346 val pf_stacksize : fixed -> partial_fn -> Nat.nat
 347
 348 val pf_graph : fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph
 349
 350 val pf_gotos : fixed -> partial_fn -> goto_map
 351
 352 val pf_labels :
 353   fixed -> partial_fn -> PreIdentifiers.identifier Identifiers.identifier_map
 354   Types.sig0
 355
 356 val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0
 357
 358 val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0
 359
 360 val partial_fn_inv_rect_Type4 :
 361   fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 362   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 363   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 364   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 365   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 366   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 367   'a1
 368
 369 val partial_fn_inv_rect_Type3 :
 370   fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 371   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 372   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 373   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 374   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 375   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 376   'a1
 377
 378 val partial_fn_inv_rect_Type2 :
 379   fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 380   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 381   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 382   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 383   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 384   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 385   'a1
 386
 387 val partial_fn_inv_rect_Type1 :
 388   fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 389   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 390   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 391   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 392   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 393   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 394   'a1
 395
 396 val partial_fn_inv_rect_Type0 :
 397   fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
 398   (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
 399   AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
 400   RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
 401   PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
 402   Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
 403   'a1
 404
 405 val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __
 406
 407 val fn_contains_rect_Type4 :
 408   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
 409
 410 val fn_contains_rect_Type5 :
 411   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
 412
 413 val fn_contains_rect_Type3 :
 414   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
 415
 416 val fn_contains_rect_Type2 :
 417   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
 418
 419 val fn_contains_rect_Type1 :
 420   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
 421
 422 val fn_contains_rect_Type0 :
 423   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1
 424
 425 val fn_contains_inv_rect_Type4 :
 426   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 427
 428 val fn_contains_inv_rect_Type3 :
 429   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 430
 431 val fn_contains_inv_rect_Type2 :
 432   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 433
 434 val fn_contains_inv_rect_Type1 :
 435   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 436
 437 val fn_contains_inv_rect_Type0 :
 438   fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 439
 440 val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __
 441
 442 val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __
 443
 444 val fill_in_statement :
 445   fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
 446   partial_fn Types.sig0
 447
 448 val add_to_graph :
 449   fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
 450   partial_fn Types.sig0
 451
 452 val change_entry :
 453   fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
 454
 455 val add_fresh_to_graph :
 456   fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
 457   partial_fn Types.sig0
 458
 459 val fresh_reg :
 460   fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
 461   Registers.register Types.sig0) Types.dPair
 462
 463 val choose_reg :
 464   fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
 465   Types.sig0, Registers.register Types.sig0) Types.dPair
 466
 467 val foldr_all : ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
 468
 469 val foldr_all' :
 470   ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2
 471
 472 val eject' : ('a1, 'a2) Types.dPair -> 'a1
 473
 474 val choose_regs :
 475   fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list -> partial_fn
 476   -> (partial_fn Types.sig0, Registers.register List.list Types.sig0)
 477   Types.dPair
 478
 479 val add_stmt_inv_rect_Type4 :
 480   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 481   'a1) -> 'a1
 482
 483 val add_stmt_inv_rect_Type5 :
 484   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 485   'a1) -> 'a1
 486
 487 val add_stmt_inv_rect_Type3 :
 488   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 489   'a1) -> 'a1
 490
 491 val add_stmt_inv_rect_Type2 :
 492   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 493   'a1) -> 'a1
 494
 495 val add_stmt_inv_rect_Type1 :
 496   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 497   'a1) -> 'a1
 498
 499 val add_stmt_inv_rect_Type0 :
 500   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
 501   'a1) -> 'a1
 502
 503 val add_stmt_inv_inv_rect_Type4 :
 504   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
 505   -> 'a1) -> 'a1
 506
 507 val add_stmt_inv_inv_rect_Type3 :
 508   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
 509   -> 'a1) -> 'a1
 510
 511 val add_stmt_inv_inv_rect_Type2 :
 512   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
 513   -> 'a1) -> 'a1
 514
 515 val add_stmt_inv_inv_rect_Type1 :
 516   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
 517   -> 'a1) -> 'a1
 518
 519 val add_stmt_inv_inv_rect_Type0 :
 520   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
 521   -> 'a1) -> 'a1
 522
 523 val add_stmt_inv_discr :
 524   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
 525
 526 val add_stmt_inv_jmdiscr :
 527   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __
 528
 529 type fn_con_because =
 530 | Fn_con_eq of partial_fn
 531 | Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
 532 | Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
 533    * partial_fn Types.sig0
 534
 535 val fn_con_because_rect_Type4 :
 536   fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 537   partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 538   Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 539   fn_con_because -> 'a1
 540
 541 val fn_con_because_rect_Type5 :
 542   fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 543   partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 544   Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 545   fn_con_because -> 'a1
 546
 547 val fn_con_because_rect_Type3 :
 548   fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 549   partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 550   Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 551   fn_con_because -> 'a1
 552
 553 val fn_con_because_rect_Type2 :
 554   fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 555   partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 556   Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 557   fn_con_because -> 'a1
 558
 559 val fn_con_because_rect_Type1 :
 560   fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 561   partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 562   Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 563   fn_con_because -> 'a1
 564
 565 val fn_con_because_rect_Type0 :
 566   fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 567   partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
 568   Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
 569   fn_con_because -> 'a1
 570
 571 val fn_con_because_inv_rect_Type4 :
 572   fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
 573   (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
 574   'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
 575   Types.sig0 -> __ -> __ -> 'a1) -> 'a1
 576
 577 val fn_con_because_inv_rect_Type3 :
 578   fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
 579   (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
 580   'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
 581   Types.sig0 -> __ -> __ -> 'a1) -> 'a1
 582
 583 val fn_con_because_inv_rect_Type2 :
 584   fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
 585   (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
 586   'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
 587   Types.sig0 -> __ -> __ -> 'a1) -> 'a1
 588
 589 val fn_con_because_inv_rect_Type1 :
 590   fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
 591   (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
 592   'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
 593   Types.sig0 -> __ -> __ -> 'a1) -> 'a1
 594
 595 val fn_con_because_inv_rect_Type0 :
 596   fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
 597   (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
 598   'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
 599   Types.sig0 -> __ -> __ -> 'a1) -> 'a1
 600
 601 val fn_con_because_discr :
 602   fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
 603
 604 val fn_con_because_jmdiscr :
 605   fixed -> partial_fn -> fn_con_because -> fn_con_because -> __
 606
 607 val fn_con_because_left : fixed -> partial_fn -> fn_con_because -> partial_fn
 608
 609 val add_expr :
 610   fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> Registers.register
 611   Types.sig0 -> partial_fn Types.sig0
 612
 613 val add_exprs :
 614   fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
 615   Registers.register List.list -> partial_fn -> partial_fn Types.sig0
 616
 617 val stmt_inv_rect_Type4 :
 618   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 619
 620 val stmt_inv_rect_Type5 :
 621   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 622
 623 val stmt_inv_rect_Type3 :
 624   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 625
 626 val stmt_inv_rect_Type2 :
 627   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 628
 629 val stmt_inv_rect_Type1 :
 630   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 631
 632 val stmt_inv_rect_Type0 :
 633   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1
 634
 635 val stmt_inv_inv_rect_Type4 :
 636   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 637
 638 val stmt_inv_inv_rect_Type3 :
 639   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 640
 641 val stmt_inv_inv_rect_Type2 :
 642   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 643
 644 val stmt_inv_inv_rect_Type1 :
 645   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 646
 647 val stmt_inv_inv_rect_Type0 :
 648   fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 649
 650 val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __
 651
 652 val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __
 653
 654 val expr_is_cst_ident :
 655   AST.typ -> Cminor_syntax.expr -> AST.ident Types.option
 656
 657 val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
 658
 659 val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __
 660
 661 val add_return :
 662   fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
 663   partial_fn -> partial_fn Types.sig0
 664
 665 val record_goto_label :
 666   fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn
 667
 668 val add_goto_dummy :
 669   fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0
 670
 671 val add_stmt :
 672   fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0
 673
 674 val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0
 675
 676 val c2ra_function :
 677   Cminor_syntax.internal_function -> RTLabs_syntax.internal_function
 678
 679 val cminor_to_rtlabs :
 680   Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program
 681