Changeset 2773 for extracted/eRTLptr.ml


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/eRTLptr.ml

    r2743 r2773  
    99open LabelledObjects
    1010
     11open BitVectorTrie
     12
    1113open Graphs
    1214
     
    1719open Registers
    1820
    19 open BitVectorTrie
    20 
    2121open CostLabel
    2222
     
    3737open Extralib
    3838
     39open Lists
     40
     41open Identifiers
     42
     43open Integers
     44
     45open AST
     46
     47open Division
     48
     49open Exp
     50
     51open Arithmetic
     52
    3953open Setoids
    4054
     
    4256
    4357open Option
    44 
    45 open Lists
    46 
    47 open Identifiers
    48 
    49 open Integers
    50 
    51 open AST
    52 
    53 open Division
    54 
    55 open Exp
    56 
    57 open Arithmetic
    5858
    5959open Extranat
     
    116116    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    117117let rec ertlptr_seq_rect_Type4 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    118 | Ertlptr_ertl x_21035 -> h_ertlptr_ertl x_21035
    119 | LOW_ADDRESS (x_21037, x_21036) -> h_LOW_ADDRESS x_21037 x_21036
    120 | HIGH_ADDRESS (x_21039, x_21038) -> h_HIGH_ADDRESS x_21039 x_21038
     118| Ertlptr_ertl x_16345 -> h_ertlptr_ertl x_16345
     119| LOW_ADDRESS (x_16347, x_16346) -> h_LOW_ADDRESS x_16347 x_16346
     120| HIGH_ADDRESS (x_16349, x_16348) -> h_HIGH_ADDRESS x_16349 x_16348
    121121
    122122(** val ertlptr_seq_rect_Type5 :
     
    124124    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    125125let rec ertlptr_seq_rect_Type5 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    126 | Ertlptr_ertl x_21044 -> h_ertlptr_ertl x_21044
    127 | LOW_ADDRESS (x_21046, x_21045) -> h_LOW_ADDRESS x_21046 x_21045
    128 | HIGH_ADDRESS (x_21048, x_21047) -> h_HIGH_ADDRESS x_21048 x_21047
     126| Ertlptr_ertl x_16354 -> h_ertlptr_ertl x_16354
     127| LOW_ADDRESS (x_16356, x_16355) -> h_LOW_ADDRESS x_16356 x_16355
     128| HIGH_ADDRESS (x_16358, x_16357) -> h_HIGH_ADDRESS x_16358 x_16357
    129129
    130130(** val ertlptr_seq_rect_Type3 :
     
    132132    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    133133let rec ertlptr_seq_rect_Type3 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    134 | Ertlptr_ertl x_21053 -> h_ertlptr_ertl x_21053
    135 | LOW_ADDRESS (x_21055, x_21054) -> h_LOW_ADDRESS x_21055 x_21054
    136 | HIGH_ADDRESS (x_21057, x_21056) -> h_HIGH_ADDRESS x_21057 x_21056
     134| Ertlptr_ertl x_16363 -> h_ertlptr_ertl x_16363
     135| LOW_ADDRESS (x_16365, x_16364) -> h_LOW_ADDRESS x_16365 x_16364
     136| HIGH_ADDRESS (x_16367, x_16366) -> h_HIGH_ADDRESS x_16367 x_16366
    137137
    138138(** val ertlptr_seq_rect_Type2 :
     
    140140    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    141141let rec ertlptr_seq_rect_Type2 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    142 | Ertlptr_ertl x_21062 -> h_ertlptr_ertl x_21062
    143 | LOW_ADDRESS (x_21064, x_21063) -> h_LOW_ADDRESS x_21064 x_21063
    144 | HIGH_ADDRESS (x_21066, x_21065) -> h_HIGH_ADDRESS x_21066 x_21065
     142| Ertlptr_ertl x_16372 -> h_ertlptr_ertl x_16372
     143| LOW_ADDRESS (x_16374, x_16373) -> h_LOW_ADDRESS x_16374 x_16373
     144| HIGH_ADDRESS (x_16376, x_16375) -> h_HIGH_ADDRESS x_16376 x_16375
    145145
    146146(** val ertlptr_seq_rect_Type1 :
     
    148148    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    149149let rec ertlptr_seq_rect_Type1 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    150 | Ertlptr_ertl x_21071 -> h_ertlptr_ertl x_21071
    151 | LOW_ADDRESS (x_21073, x_21072) -> h_LOW_ADDRESS x_21073 x_21072
    152 | HIGH_ADDRESS (x_21075, x_21074) -> h_HIGH_ADDRESS x_21075 x_21074
     150| Ertlptr_ertl x_16381 -> h_ertlptr_ertl x_16381
     151| LOW_ADDRESS (x_16383, x_16382) -> h_LOW_ADDRESS x_16383 x_16382
     152| HIGH_ADDRESS (x_16385, x_16384) -> h_HIGH_ADDRESS x_16385 x_16384
    153153
    154154(** val ertlptr_seq_rect_Type0 :
     
    156156    (Registers.register -> Graphs.label -> 'a1) -> ertlptr_seq -> 'a1 **)
    157157let rec ertlptr_seq_rect_Type0 h_ertlptr_ertl h_LOW_ADDRESS h_HIGH_ADDRESS = function
    158 | Ertlptr_ertl x_21080 -> h_ertlptr_ertl x_21080
    159 | LOW_ADDRESS (x_21082, x_21081) -> h_LOW_ADDRESS x_21082 x_21081
    160 | HIGH_ADDRESS (x_21084, x_21083) -> h_HIGH_ADDRESS x_21084 x_21083
     158| Ertlptr_ertl x_16390 -> h_ertlptr_ertl x_16390
     159| LOW_ADDRESS (x_16392, x_16391) -> h_LOW_ADDRESS x_16392 x_16391
     160| HIGH_ADDRESS (x_16394, x_16393) -> h_HIGH_ADDRESS x_16394 x_16393
    161161
    162162(** val ertlptr_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.