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_semantics.mli

    r2730 r2773  
    9595open Globalenvs
    9696
     97open CostLabel
     98
     99open Events
     100
     101open IOMonad
     102
     103open IO
     104
     105open SmallstepExec
     106
    97107open BitVectorTrie
    98 
    99 open CostLabel
    100 
    101 open Events
    102 
    103 open IOMonad
    104 
    105 open IO
    106 
    107 open SmallstepExec
    108108
    109109open Graphs
     
    193193val adv : Graphs.label -> frame -> frame
    194194
    195 type state0 =
    196 | State of frame * frame List.list * GenMem.mem1
     195type state =
     196| State of frame * frame List.list * GenMem.mem
    197197| Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
    198198   * Values.val0 List.list * Registers.register Types.option
    199    * frame List.list * GenMem.mem1
     199   * frame List.list * GenMem.mem
    200200| Returnstate of Values.val0 Types.option * Registers.register Types.option
    201    * frame List.list * GenMem.mem1
     201   * frame List.list * GenMem.mem
    202202| Finalstate of Integers.int
    203203
    204204val state_rect_Type4 :
    205   (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
    206   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    207   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    208   -> (Values.val0 Types.option -> Registers.register Types.option -> frame
    209   List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
     205  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
     206  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     207  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
     208  (Values.val0 Types.option -> Registers.register Types.option -> frame
     209  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
    210210
    211211val state_rect_Type5 :
    212   (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
    213   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    214   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    215   -> (Values.val0 Types.option -> Registers.register Types.option -> frame
    216   List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
     212  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
     213  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     214  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
     215  (Values.val0 Types.option -> Registers.register Types.option -> frame
     216  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
    217217
    218218val state_rect_Type3 :
    219   (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
    220   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    221   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    222   -> (Values.val0 Types.option -> Registers.register Types.option -> frame
    223   List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
     219  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
     220  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     221  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
     222  (Values.val0 Types.option -> Registers.register Types.option -> frame
     223  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
    224224
    225225val state_rect_Type2 :
    226   (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
    227   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    228   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    229   -> (Values.val0 Types.option -> Registers.register Types.option -> frame
    230   List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
     226  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
     227  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     228  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
     229  (Values.val0 Types.option -> Registers.register Types.option -> frame
     230  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
    231231
    232232val state_rect_Type1 :
    233   (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
    234   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    235   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    236   -> (Values.val0 Types.option -> Registers.register Types.option -> frame
    237   List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
     233  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
     234  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     235  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
     236  (Values.val0 Types.option -> Registers.register Types.option -> frame
     237  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
    238238
    239239val state_rect_Type0 :
    240   (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
    241   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    242   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    243   -> (Values.val0 Types.option -> Registers.register Types.option -> frame
    244   List.list -> GenMem.mem1 -> 'a1) -> (Integers.int -> 'a1) -> state0 -> 'a1
     240  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
     241  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     242  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
     243  (Values.val0 Types.option -> Registers.register Types.option -> frame
     244  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1
    245245
    246246val state_inv_rect_Type4 :
    247   state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    248   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
    249   List.list -> Registers.register Types.option -> frame List.list ->
    250   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
    251   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    252   'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     247  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     248  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     249  List.list -> Registers.register Types.option -> frame List.list ->
     250  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
     251  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     252  (Integers.int -> __ -> 'a1) -> 'a1
    253253
    254254val state_inv_rect_Type3 :
    255   state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    256   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
    257   List.list -> Registers.register Types.option -> frame List.list ->
    258   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
    259   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    260   'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     255  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     256  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     257  List.list -> Registers.register Types.option -> frame List.list ->
     258  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
     259  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     260  (Integers.int -> __ -> 'a1) -> 'a1
    261261
    262262val state_inv_rect_Type2 :
    263   state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    264   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
    265   List.list -> Registers.register Types.option -> frame List.list ->
    266   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
    267   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    268   'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     263  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     264  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     265  List.list -> Registers.register Types.option -> frame List.list ->
     266  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
     267  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     268  (Integers.int -> __ -> 'a1) -> 'a1
    269269
    270270val state_inv_rect_Type1 :
    271   state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    272   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
    273   List.list -> Registers.register Types.option -> frame List.list ->
    274   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
    275   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    276   'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     271  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     272  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     273  List.list -> Registers.register Types.option -> frame List.list ->
     274  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
     275  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     276  (Integers.int -> __ -> 'a1) -> 'a1
    277277
    278278val state_inv_rect_Type0 :
    279   state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    280   (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
    281   List.list -> Registers.register Types.option -> frame List.list ->
    282   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
    283   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    284   'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    285 
    286 val state_jmdiscr : state0 -> state0 -> __
     279  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     280  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     281  List.list -> Registers.register Types.option -> frame List.list ->
     282  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
     283  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
     284  (Integers.int -> __ -> 'a1) -> 'a1
     285
     286val state_jmdiscr : state -> state -> __
    287287
    288288val build_state :
    289   frame -> frame List.list -> GenMem.mem1 -> Graphs.label -> state0
     289  frame -> frame List.list -> GenMem.mem -> Graphs.label -> state
    290290
    291291val next_instruction : frame -> RTLabs_syntax.statement
     
    310310
    311311val eval_statement :
    312   genv -> state0 -> (IO.io_out, IO.io_in, (Events.trace, state0) Types.prod)
     312  genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
    313313  IOMonad.iO
    314314
    315 val rTLabs_is_final : state0 -> Integers.int Types.option
     315val rTLabs_is_final : state -> Integers.int Types.option
    316316
    317317val rTLabs_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system
    318318
    319 val make_global0 : RTLabs_syntax.rTLabs_program -> genv
    320 
    321 val make_initial_state0 : RTLabs_syntax.rTLabs_program -> state0 Errors.res
     319val make_global : RTLabs_syntax.rTLabs_program -> genv
     320
     321val make_initial_state : RTLabs_syntax.rTLabs_program -> state Errors.res
    322322
    323323val rTLabs_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec
     
    330330
    331331val func_block_of_exec :
    332   genv -> state0 -> Events.trace -> AST.ident ->
    333   RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    334   Registers.register Types.option -> frame List.list -> GenMem.mem1 ->
     332  genv -> state -> Events.trace -> AST.ident ->
     333  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     334  Registers.register Types.option -> frame List.list -> GenMem.mem ->
    335335  Pointers.block Types.sig0
    336336
Note: See TracChangeset for help on using the changeset viewer.