Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/switchRemoval.mli

    r2717 r2773  
    5757open Identifiers
    5858
    59 open BitVectorTrie
    60 
    6159open CostLabel
    6260
     
    134132
    135133open MemoryInjections
    136 
    137 type switch_free = __
    138 
    139 type branches_switch_free = __
    140134
    141135val convert_break_to_goto :
     
    192186val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program
    193187
    194 type substatement_ls = __
    195 
    196 type substatement_P = __
    197 
    198188val nonempty_block_rect_Type4 :
    199   GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
     189  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
    200190
    201191val nonempty_block_rect_Type5 :
    202   GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
     192  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
    203193
    204194val nonempty_block_rect_Type3 :
    205   GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
     195  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
    206196
    207197val nonempty_block_rect_Type2 :
    208   GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
     198  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
    209199
    210200val nonempty_block_rect_Type1 :
    211   GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
     201  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
    212202
    213203val nonempty_block_rect_Type0 :
    214   GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
     204  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1
    215205
    216206val nonempty_block_inv_rect_Type4 :
    217   GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
     207  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
    218208
    219209val nonempty_block_inv_rect_Type3 :
    220   GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
     210  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
    221211
    222212val nonempty_block_inv_rect_Type2 :
    223   GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
     213  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
    224214
    225215val nonempty_block_inv_rect_Type1 :
    226   GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
     216  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
    227217
    228218val nonempty_block_inv_rect_Type0 :
    229   GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
    230 
    231 val nonempty_block_discr : GenMem.mem1 -> Pointers.block -> __
    232 
    233 val nonempty_block_jmdiscr : GenMem.mem1 -> Pointers.block -> __
     219  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1
     220
     221val nonempty_block_discr : GenMem.mem -> Pointers.block -> __
     222
     223val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __
    234224
    235225val sr_memext_rect_Type4 :
    236   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    237   -> 'a1) -> 'a1
     226  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     227  'a1) -> 'a1
    238228
    239229val sr_memext_rect_Type5 :
    240   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    241   -> 'a1) -> 'a1
     230  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     231  'a1) -> 'a1
    242232
    243233val sr_memext_rect_Type3 :
    244   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    245   -> 'a1) -> 'a1
     234  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     235  'a1) -> 'a1
    246236
    247237val sr_memext_rect_Type2 :
    248   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    249   -> 'a1) -> 'a1
     238  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     239  'a1) -> 'a1
    250240
    251241val sr_memext_rect_Type1 :
    252   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    253   -> 'a1) -> 'a1
     242  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     243  'a1) -> 'a1
    254244
    255245val sr_memext_rect_Type0 :
    256   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    257   -> 'a1) -> 'a1
     246  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     247  'a1) -> 'a1
    258248
    259249val sr_memext_inv_rect_Type4 :
    260   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    261   -> __ -> 'a1) -> 'a1
     250  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     251  __ -> 'a1) -> 'a1
    262252
    263253val sr_memext_inv_rect_Type3 :
    264   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    265   -> __ -> 'a1) -> 'a1
     254  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     255  __ -> 'a1) -> 'a1
    266256
    267257val sr_memext_inv_rect_Type2 :
    268   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    269   -> __ -> 'a1) -> 'a1
     258  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     259  __ -> 'a1) -> 'a1
    270260
    271261val sr_memext_inv_rect_Type1 :
    272   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    273   -> __ -> 'a1) -> 'a1
     262  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     263  __ -> 'a1) -> 'a1
    274264
    275265val sr_memext_inv_rect_Type0 :
    276   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
    277   -> __ -> 'a1) -> 'a1
     266  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
     267  __ -> 'a1) -> 'a1
    278268
    279269val sr_memext_discr :
    280   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
     270  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __
    281271
    282272val sr_memext_jmdiscr :
    283   GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __
     273  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __
    284274
    285275val env_codomain :
Note: See TracChangeset for help on using the changeset viewer.