Changeset 2773 for extracted/eRTL.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/eRTL.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
     
    112112    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    113113let rec move_dst_rect_Type4 h_PSD h_HDW = function
    114 | PSD x_20901 -> h_PSD x_20901
    115 | HDW x_20902 -> h_HDW x_20902
     114| PSD x_16211 -> h_PSD x_16211
     115| HDW x_16212 -> h_HDW x_16212
    116116
    117117(** val move_dst_rect_Type5 :
    118118    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    119119let rec move_dst_rect_Type5 h_PSD h_HDW = function
    120 | PSD x_20906 -> h_PSD x_20906
    121 | HDW x_20907 -> h_HDW x_20907
     120| PSD x_16216 -> h_PSD x_16216
     121| HDW x_16217 -> h_HDW x_16217
    122122
    123123(** val move_dst_rect_Type3 :
    124124    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    125125let rec move_dst_rect_Type3 h_PSD h_HDW = function
    126 | PSD x_20911 -> h_PSD x_20911
    127 | HDW x_20912 -> h_HDW x_20912
     126| PSD x_16221 -> h_PSD x_16221
     127| HDW x_16222 -> h_HDW x_16222
    128128
    129129(** val move_dst_rect_Type2 :
    130130    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    131131let rec move_dst_rect_Type2 h_PSD h_HDW = function
    132 | PSD x_20916 -> h_PSD x_20916
    133 | HDW x_20917 -> h_HDW x_20917
     132| PSD x_16226 -> h_PSD x_16226
     133| HDW x_16227 -> h_HDW x_16227
    134134
    135135(** val move_dst_rect_Type1 :
    136136    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    137137let rec move_dst_rect_Type1 h_PSD h_HDW = function
    138 | PSD x_20921 -> h_PSD x_20921
    139 | HDW x_20922 -> h_HDW x_20922
     138| PSD x_16231 -> h_PSD x_16231
     139| HDW x_16232 -> h_HDW x_16232
    140140
    141141(** val move_dst_rect_Type0 :
    142142    (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1 **)
    143143let rec move_dst_rect_Type0 h_PSD h_HDW = function
    144 | PSD x_20926 -> h_PSD x_20926
    145 | HDW x_20927 -> h_HDW x_20927
     144| PSD x_16236 -> h_PSD x_16236
     145| HDW x_16237 -> h_HDW x_16237
    146146
    147147(** val move_dst_inv_rect_Type4 :
     
    338338| Ertl_new_frame -> h_ertl_new_frame
    339339| Ertl_del_frame -> h_ertl_del_frame
    340 | Ertl_frame_size x_20966 -> h_ertl_frame_size x_20966
     340| Ertl_frame_size x_16276 -> h_ertl_frame_size x_16276
    341341
    342342(** val ertl_seq_rect_Type5 :
     
    345345| Ertl_new_frame -> h_ertl_new_frame
    346346| Ertl_del_frame -> h_ertl_del_frame
    347 | Ertl_frame_size x_20971 -> h_ertl_frame_size x_20971
     347| Ertl_frame_size x_16281 -> h_ertl_frame_size x_16281
    348348
    349349(** val ertl_seq_rect_Type3 :
     
    352352| Ertl_new_frame -> h_ertl_new_frame
    353353| Ertl_del_frame -> h_ertl_del_frame
    354 | Ertl_frame_size x_20976 -> h_ertl_frame_size x_20976
     354| Ertl_frame_size x_16286 -> h_ertl_frame_size x_16286
    355355
    356356(** val ertl_seq_rect_Type2 :
     
    359359| Ertl_new_frame -> h_ertl_new_frame
    360360| Ertl_del_frame -> h_ertl_del_frame
    361 | Ertl_frame_size x_20981 -> h_ertl_frame_size x_20981
     361| Ertl_frame_size x_16291 -> h_ertl_frame_size x_16291
    362362
    363363(** val ertl_seq_rect_Type1 :
     
    366366| Ertl_new_frame -> h_ertl_new_frame
    367367| Ertl_del_frame -> h_ertl_del_frame
    368 | Ertl_frame_size x_20986 -> h_ertl_frame_size x_20986
     368| Ertl_frame_size x_16296 -> h_ertl_frame_size x_16296
    369369
    370370(** val ertl_seq_rect_Type0 :
     
    373373| Ertl_new_frame -> h_ertl_new_frame
    374374| Ertl_del_frame -> h_ertl_del_frame
    375 | Ertl_frame_size x_20991 -> h_ertl_frame_size x_20991
     375| Ertl_frame_size x_16301 -> h_ertl_frame_size x_16301
    376376
    377377(** val ertl_seq_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.