Changeset 2773 for extracted/genMem.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/genMem.mli

    r2717 r2773  
    4141open Errors
    4242
     43open Lists
     44
     45open Identifiers
     46
     47open Integers
     48
     49open AST
     50
     51open Division
     52
     53open Exp
     54
     55open Arithmetic
     56
    4357open Setoids
    4458
     
    4761open Option
    4862
    49 open Lists
    50 
    51 open Identifiers
    52 
    53 open Integers
    54 
    55 open AST
    56 
    57 open Division
    58 
    59 open Exp
    60 
    61 open Arithmetic
    62 
    6363open Extranat
    6464
     
    8181open ByteValues
    8282
    83 val update1 : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1
     83val update : Z.z -> 'a1 -> (Z.z -> 'a1) -> Z.z -> 'a1
    8484
    8585val update_block :
     
    133133val block_contents_jmdiscr : block_contents -> block_contents -> __
    134134
    135 type mem1 = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
     135type mem = { blocks : (Pointers.block -> block_contents); nextblock : Z.z }
    136136
    137137val mem_rect_Type4 :
    138   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
     138  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
    139139
    140140val mem_rect_Type5 :
    141   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
     141  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
    142142
    143143val mem_rect_Type3 :
    144   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
     144  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
    145145
    146146val mem_rect_Type2 :
    147   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
     147  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
    148148
    149149val mem_rect_Type1 :
    150   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
     150  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
    151151
    152152val mem_rect_Type0 :
    153   ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem1 -> 'a1
    154 
    155 val blocks : mem1 -> Pointers.block -> block_contents
    156 
    157 val nextblock : mem1 -> Z.z
     153  ((Pointers.block -> block_contents) -> Z.z -> __ -> 'a1) -> mem -> 'a1
     154
     155val blocks : mem -> Pointers.block -> block_contents
     156
     157val nextblock : mem -> Z.z
    158158
    159159val mem_inv_rect_Type4 :
    160   mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     160  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    161161  'a1
    162162
    163163val mem_inv_rect_Type3 :
    164   mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     164  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    165165  'a1
    166166
    167167val mem_inv_rect_Type2 :
    168   mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     168  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    169169  'a1
    170170
    171171val mem_inv_rect_Type1 :
    172   mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     172  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    173173  'a1
    174174
    175175val mem_inv_rect_Type0 :
    176   mem1 -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
    177   'a1
    178 
    179 val mem_discr : mem1 -> mem1 -> __
    180 
    181 val mem_jmdiscr : mem1 -> mem1 -> __
     176  mem -> ((Pointers.block -> block_contents) -> Z.z -> __ -> __ -> 'a1) ->
     177  'a1
     178
     179val mem_discr : mem -> mem -> __
     180
     181val mem_jmdiscr : mem -> mem -> __
    182182
    183183val oneZ : Z.z
     
    185185val empty_block : Z.z -> Z.z -> block_contents
    186186
    187 val empty : mem1
    188 
    189 val alloc : mem1 -> Z.z -> Z.z -> (mem1, Pointers.block) Types.prod
    190 
    191 val free : mem1 -> Pointers.block -> mem1
    192 
    193 val free_list : mem1 -> Pointers.block List.list -> mem1
    194 
    195 val low_bound : mem1 -> Pointers.block -> Z.z
    196 
    197 val high_bound : mem1 -> Pointers.block -> Z.z
    198 
    199 val block_region0 : mem1 -> Pointers.block -> AST.region
     187val empty : mem
     188
     189val alloc : mem -> Z.z -> Z.z -> (mem, Pointers.block) Types.prod
     190
     191val free : mem -> Pointers.block -> mem
     192
     193val free_list : mem -> Pointers.block List.list -> mem
     194
     195val low_bound : mem -> Pointers.block -> Z.z
     196
     197val high_bound : mem -> Pointers.block -> Z.z
     198
     199val block_region : mem -> Pointers.block -> AST.region
    200200
    201201val do_if_in_bounds :
    202   mem1 -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z ->
    203   'a1) -> 'a1 Types.option
    204 
    205 val beloadv : mem1 -> Pointers.pointer -> ByteValues.beval Types.option
     202  mem -> Pointers.pointer -> (Pointers.block -> block_contents -> Z.z -> 'a1)
     203  -> 'a1 Types.option
     204
     205val beloadv : mem -> Pointers.pointer -> ByteValues.beval Types.option
    206206
    207207val bestorev :
    208   mem1 -> Pointers.pointer -> ByteValues.beval -> mem1 Types.option
    209 
     208  mem -> Pointers.pointer -> ByteValues.beval -> mem Types.option
     209
Note: See TracChangeset for help on using the changeset viewer.