Changeset 2773 for extracted/iO.ml


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

    r2743 r2773  
    4646
    4747open IOMonad
    48 
    49 open BitVectorTrie
    5048
    5149open CostLabel
     
    152150    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    153151    'a1 **)
    154 let rec io_out_rect_Type4 h_mk_io_out x_5847 =
    155   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    156     io_in_typ0 } = x_5847
     152let rec io_out_rect_Type4 h_mk_io_out x_1355 =
     153  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     154    io_in_typ0 } = x_1355
    157155  in
    158156  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    161159    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    162160    'a1 **)
    163 let rec io_out_rect_Type5 h_mk_io_out x_5849 =
    164   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    165     io_in_typ0 } = x_5849
     161let rec io_out_rect_Type5 h_mk_io_out x_1357 =
     162  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     163    io_in_typ0 } = x_1357
    166164  in
    167165  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    170168    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    171169    'a1 **)
    172 let rec io_out_rect_Type3 h_mk_io_out x_5851 =
    173   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    174     io_in_typ0 } = x_5851
     170let rec io_out_rect_Type3 h_mk_io_out x_1359 =
     171  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     172    io_in_typ0 } = x_1359
    175173  in
    176174  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    179177    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    180178    'a1 **)
    181 let rec io_out_rect_Type2 h_mk_io_out x_5853 =
    182   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    183     io_in_typ0 } = x_5853
     179let rec io_out_rect_Type2 h_mk_io_out x_1361 =
     180  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     181    io_in_typ0 } = x_1361
    184182  in
    185183  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    188186    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    189187    'a1 **)
    190 let rec io_out_rect_Type1 h_mk_io_out x_5855 =
    191   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    192     io_in_typ0 } = x_5855
     188let rec io_out_rect_Type1 h_mk_io_out x_1363 =
     189  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     190    io_in_typ0 } = x_1363
    193191  in
    194192  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    197195    (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
    198196    'a1 **)
    199 let rec io_out_rect_Type0 h_mk_io_out x_5857 =
    200   let { io_function = io_function0; io_args = io_args0; io_in_typ =
    201     io_in_typ0 } = x_5857
     197let rec io_out_rect_Type0 h_mk_io_out x_1365 =
     198  let { io_function = io_function0; io_args = io_args0; io_in_typ =
     199    io_in_typ0 } = x_1365
    202200  in
    203201  h_mk_io_out io_function0 io_args0 io_in_typ0
     
    264262let do_io fn args t =
    265263  IOMonad.Interact ({ io_function = fn; io_args = args; io_in_typ = t },
    266     (fun res1 -> IOMonad.Value res1))
     264    (fun res -> IOMonad.Value res))
    267265
    268266(** val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO **)
Note: See TracChangeset for help on using the changeset viewer.