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/rTLabs_abstract.mli

    r2730 r2773  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open Graphs
    46
     
    1315open SmallstepExec
    1416
    15 open BitVectorTrie
    16 
    1717open CostLabel
    1818
     
    119119open RTLabs_semantics
    120120
    121 type rTLabs_state = RTLabs_semantics.state0
     121type rTLabs_state = RTLabs_semantics.state
    122122
    123123type rTLabs_genv = RTLabs_semantics.genv
     
    133133open Deqsets_extra
    134134
    135 val status_class_jmdiscr0 :
     135val status_class_jmdiscr :
    136136  StructuredTraces.status_class -> StructuredTraces.status_class -> __
    137137
    138 type rTLabs_ext_state = { ras_state : RTLabs_semantics.state0;
     138type rTLabs_ext_state = { ras_state : RTLabs_semantics.state;
    139139                          ras_fn_stack : Pointers.block List.list }
    140140
    141141val rTLabs_ext_state_rect_Type4 :
    142   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
     142  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    143143  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
    144144
    145145val rTLabs_ext_state_rect_Type5 :
    146   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
     146  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    147147  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
    148148
    149149val rTLabs_ext_state_rect_Type3 :
    150   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
     150  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    151151  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
    152152
    153153val rTLabs_ext_state_rect_Type2 :
    154   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
     154  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    155155  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
    156156
    157157val rTLabs_ext_state_rect_Type1 :
    158   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
     158  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    159159  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
    160160
    161161val rTLabs_ext_state_rect_Type0 :
    162   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Pointers.block
     162  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Pointers.block
    163163  List.list -> __ -> 'a1) -> rTLabs_ext_state -> 'a1
    164164
    165165val ras_state :
    166   RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state0
     166  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
    167167
    168168val ras_fn_stack :
     
    170170
    171171val rTLabs_ext_state_inv_rect_Type4 :
    172   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
     172  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    173173  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
    174174
    175175val rTLabs_ext_state_inv_rect_Type3 :
    176   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
     176  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    177177  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
    178178
    179179val rTLabs_ext_state_inv_rect_Type2 :
    180   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
     180  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    181181  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
    182182
    183183val rTLabs_ext_state_inv_rect_Type1 :
    184   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
     184  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    185185  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
    186186
    187187val rTLabs_ext_state_inv_rect_Type0 :
    188   RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state0 ->
     188  RTLabs_semantics.genv -> rTLabs_ext_state -> (RTLabs_semantics.state ->
    189189  Pointers.block List.list -> __ -> __ -> 'a1) -> 'a1
    190190
     
    197197val dpi1__o__Ras_state__o__inject :
    198198  RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
    199   RTLabs_semantics.state0 Types.sig0
     199  RTLabs_semantics.state Types.sig0
    200200
    201201val eject__o__Ras_state__o__inject :
    202202  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
    203   RTLabs_semantics.state0 Types.sig0
     203  RTLabs_semantics.state Types.sig0
    204204
    205205val ras_state__o__inject :
    206   RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state0
     206  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state
    207207  Types.sig0
    208208
    209209val dpi1__o__Ras_state :
    210210  RTLabs_semantics.genv -> (rTLabs_ext_state, 'a1) Types.dPair ->
    211   RTLabs_semantics.state0
     211  RTLabs_semantics.state
    212212
    213213val eject__o__Ras_state :
    214214  RTLabs_semantics.genv -> rTLabs_ext_state Types.sig0 ->
    215   RTLabs_semantics.state0
     215  RTLabs_semantics.state
    216216
    217217val next_state :
    218   RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state0 ->
     218  RTLabs_semantics.genv -> rTLabs_ext_state -> RTLabs_semantics.state ->
    219219  Events.trace -> rTLabs_ext_state
    220220
    221 val rTLabs_classify :
    222   RTLabs_semantics.state0 -> StructuredTraces.status_class
    223 
    224 val rTLabs_cost : RTLabs_semantics.state0 -> Bool.bool
     221val rTLabs_classify : RTLabs_semantics.state -> StructuredTraces.status_class
     222
     223val rTLabs_cost : RTLabs_semantics.state -> Bool.bool
    225224
    226225val rTLabs_cost_label :
    227   RTLabs_semantics.state0 -> CostLabel.costlabel Types.option
     226  RTLabs_semantics.state -> CostLabel.costlabel Types.option
    228227
    229228type rTLabs_pc =
Note: See TracChangeset for help on using the changeset viewer.