Changeset 2717 for extracted/events.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/events.ml

    r2649 r2717  
    1919open Division
    2020
     21open Exp
     22
    2123open Arithmetic
    2224
     
    7880
    7981open Values
     82
     83open BitVectorTrie
    8084
    8185open CostLabel
     
    8791    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    8892let rec eventval_rect_Type4 h_EVint = function
    89 | EVint (sz, x_2897) -> h_EVint sz x_2897
     93| EVint (sz, x_5459) -> h_EVint sz x_5459
    9094
    9195(** val eventval_rect_Type5 :
    9296    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9397let rec eventval_rect_Type5 h_EVint = function
    94 | EVint (sz, x_2900) -> h_EVint sz x_2900
     98| EVint (sz, x_5462) -> h_EVint sz x_5462
    9599
    96100(** val eventval_rect_Type3 :
    97101    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    98102let rec eventval_rect_Type3 h_EVint = function
    99 | EVint (sz, x_2903) -> h_EVint sz x_2903
     103| EVint (sz, x_5465) -> h_EVint sz x_5465
    100104
    101105(** val eventval_rect_Type2 :
    102106    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    103107let rec eventval_rect_Type2 h_EVint = function
    104 | EVint (sz, x_2906) -> h_EVint sz x_2906
     108| EVint (sz, x_5468) -> h_EVint sz x_5468
    105109
    106110(** val eventval_rect_Type1 :
    107111    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    108112let rec eventval_rect_Type1 h_EVint = function
    109 | EVint (sz, x_2909) -> h_EVint sz x_2909
     113| EVint (sz, x_5471) -> h_EVint sz x_5471
    110114
    111115(** val eventval_rect_Type0 :
    112116    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    113117let rec eventval_rect_Type0 h_EVint = function
    114 | EVint (sz, x_2912) -> h_EVint sz x_2912
     118| EVint (sz, x_5474) -> h_EVint sz x_5474
    115119
    116120(** val eventval_inv_rect_Type4 :
     
    157161    eventval -> 'a1) -> event -> 'a1 **)
    158162let rec event_rect_Type4 h_EVcost h_EVextcall = function
    159 | EVcost x_2937 -> h_EVcost x_2937
     163| EVcost x_5499 -> h_EVcost x_5499
    160164| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    161165
     
    164168    eventval -> 'a1) -> event -> 'a1 **)
    165169let rec event_rect_Type5 h_EVcost h_EVextcall = function
    166 | EVcost x_2941 -> h_EVcost x_2941
     170| EVcost x_5503 -> h_EVcost x_5503
    167171| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    168172
     
    171175    eventval -> 'a1) -> event -> 'a1 **)
    172176let rec event_rect_Type3 h_EVcost h_EVextcall = function
    173 | EVcost x_2945 -> h_EVcost x_2945
     177| EVcost x_5507 -> h_EVcost x_5507
    174178| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    175179
     
    178182    eventval -> 'a1) -> event -> 'a1 **)
    179183let rec event_rect_Type2 h_EVcost h_EVextcall = function
    180 | EVcost x_2949 -> h_EVcost x_2949
     184| EVcost x_5511 -> h_EVcost x_5511
    181185| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    182186
     
    185189    eventval -> 'a1) -> event -> 'a1 **)
    186190let rec event_rect_Type1 h_EVcost h_EVextcall = function
    187 | EVcost x_2953 -> h_EVcost x_2953
     191| EVcost x_5515 -> h_EVcost x_5515
    188192| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    189193
     
    192196    eventval -> 'a1) -> event -> 'a1 **)
    193197let rec event_rect_Type0 h_EVcost h_EVextcall = function
    194 | EVcost x_2957 -> h_EVcost x_2957
     198| EVcost x_5519 -> h_EVcost x_5519
    195199| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    196200
Note: See TracChangeset for help on using the changeset viewer.