Changeset 2773 for extracted/csem.mli


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 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/csem.mli

    r2730 r2773  
    9494
    9595open Globalenvs
    96 
    97 open BitVectorTrie
    9896
    9997open CostLabel
     
    153151val sem_cmp :
    154152  Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
    155   Csyntax.type0 -> GenMem.mem1 -> Values.val0 Types.option
     153  Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option
    156154
    157155val cast_bool_to_target :
     
    164162val sem_binary_operation :
    165163  Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
    166   Csyntax.type0 -> GenMem.mem1 -> Csyntax.type0 -> Values.val0 Types.option
     164  Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0 Types.option
    167165
    168166val cast_int_int :
     
    170168  BitVector.bitVector
    171169
    172 type genv0 = Csyntax.clight_fundef Globalenvs.genv_t
     170type genv = Csyntax.clight_fundef Globalenvs.genv_t
    173171
    174172type env = Pointers.block Identifiers.identifier_map
     
    177175
    178176val load_value_of_type :
    179   Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
     177  Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
    180178  Values.val0 Types.option
    181179
    182180val store_value_of_type :
    183   Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
    184   Values.val0 -> GenMem.mem1 Types.option
     181  Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
     182  Values.val0 -> GenMem.mem Types.option
    185183
    186184val blocks_of_env : env -> Pointers.block List.list
     
    315313val call_cont : cont -> cont
    316314
    317 type state0 =
    318 | State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
     315type state =
     316| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
    319317| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
    320    * cont * GenMem.mem1
    321 | Returnstate of Values.val0 * cont * GenMem.mem1
     318   * cont * GenMem.mem
     319| Returnstate of Values.val0 * cont * GenMem.mem
    322320| Finalstate of Integers.int
    323321
    324322val state_rect_Type4 :
    325   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    326   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    327   cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    328   -> (Integers.int -> 'a1) -> state0 -> 'a1
     323  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
     324  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
     325  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
     326  (Integers.int -> 'a1) -> state -> 'a1
    329327
    330328val state_rect_Type5 :
    331   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    332   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    333   cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    334   -> (Integers.int -> 'a1) -> state0 -> 'a1
     329  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
     330  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
     331  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
     332  (Integers.int -> 'a1) -> state -> 'a1
    335333
    336334val state_rect_Type3 :
    337   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    338   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    339   cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    340   -> (Integers.int -> 'a1) -> state0 -> 'a1
     335  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
     336  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
     337  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
     338  (Integers.int -> 'a1) -> state -> 'a1
    341339
    342340val state_rect_Type2 :
    343   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    344   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    345   cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    346   -> (Integers.int -> 'a1) -> state0 -> 'a1
     341  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
     342  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
     343  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
     344  (Integers.int -> 'a1) -> state -> 'a1
    347345
    348346val state_rect_Type1 :
    349   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    350   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    351   cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    352   -> (Integers.int -> 'a1) -> state0 -> 'a1
     347  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
     348  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
     349  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
     350  (Integers.int -> 'a1) -> state -> 'a1
    353351
    354352val state_rect_Type0 :
    355   (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    356   'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    357   cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    358   -> (Integers.int -> 'a1) -> state0 -> 'a1
     353  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
     354  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
     355  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
     356  (Integers.int -> 'a1) -> state -> 'a1
    359357
    360358val state_inv_rect_Type4 :
    361   state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    362   GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    363   Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    364   -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     359  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     360  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     361  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     362  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    365363
    366364val state_inv_rect_Type3 :
    367   state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    368   GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    369   Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    370   -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     365  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     366  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     367  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     368  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    371369
    372370val state_inv_rect_Type2 :
    373   state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    374   GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    375   Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    376   -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     371  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     372  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     373  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     374  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    377375
    378376val state_inv_rect_Type1 :
    379   state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    380   GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    381   Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    382   -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     377  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     378  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     379  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     380  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    383381
    384382val state_inv_rect_Type0 :
    385   state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    386   GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    387   Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    388   -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    389 
    390 val state_discr : state0 -> state0 -> __
    391 
    392 val state_jmdiscr : state0 -> state0 -> __
     383  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
     384  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
     385  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
     386  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     387
     388val state_discr : state -> state -> __
     389
     390val state_jmdiscr : state -> state -> __
    393391
    394392val find_label_ls :
Note: See TracChangeset for help on using the changeset viewer.