Changeset 2717 for extracted/iO.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 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/iO.ml

    r2649 r2717  
    4747open IOMonad
    4848
     49open BitVectorTrie
     50
    4951open CostLabel
    5052
     
    6264
    6365open Division
     66
     67open Exp
    6468
    6569open Arithmetic
     
    148152    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    149153    'a1 **)
    150 let rec io_out_rect_Type4 h_mk_io_out x_3363 =
    151   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    152     io_in_typ0 } = x_3363
     154let rec io_out_rect_Type4 h_mk_io_out x_5821 =
     155  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     156    io_in_typ0 } = x_5821
    153157  in
    154158  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    157161    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    158162    'a1 **)
    159 let rec io_out_rect_Type5 h_mk_io_out x_3365 =
    160   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    161     io_in_typ0 } = x_3365
     163let rec io_out_rect_Type5 h_mk_io_out x_5823 =
     164  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     165    io_in_typ0 } = x_5823
    162166  in
    163167  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    166170    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    167171    'a1 **)
    168 let rec io_out_rect_Type3 h_mk_io_out x_3367 =
    169   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    170     io_in_typ0 } = x_3367
     172let rec io_out_rect_Type3 h_mk_io_out x_5825 =
     173  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     174    io_in_typ0 } = x_5825
    171175  in
    172176  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    175179    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    176180    'a1 **)
    177 let rec io_out_rect_Type2 h_mk_io_out x_3369 =
    178   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    179     io_in_typ0 } = x_3369
     181let rec io_out_rect_Type2 h_mk_io_out x_5827 =
     182  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     183    io_in_typ0 } = x_5827
    180184  in
    181185  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    184188    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    185189    'a1 **)
    186 let rec io_out_rect_Type1 h_mk_io_out x_3371 =
    187   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    188     io_in_typ0 } = x_3371
     190let rec io_out_rect_Type1 h_mk_io_out x_5829 =
     191  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     192    io_in_typ0 } = x_5829
    189193  in
    190194  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    193197    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    194198    'a1 **)
    195 let rec io_out_rect_Type0 h_mk_io_out x_3373 =
    196   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    197     io_in_typ0 } = x_3373
     199let rec io_out_rect_Type0 h_mk_io_out x_5831 =
     200  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     201    io_in_typ0 } = x_5831
    198202  in
    199203  h_mk_io_out io_function0 io_args0 io_in_typ0
Note: See TracChangeset for help on using the changeset viewer.