Changeset 2797 for extracted/iOMonad.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/iOMonad.ml

    r2775 r2797  
    5252    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
    5353let rec iO_rect_Type4 h_Interact h_Value h_Wrong = function
    54 | Interact (o, x_4542) ->
    55   h_Interact o x_4542 (fun x_4541 ->
    56     iO_rect_Type4 h_Interact h_Value h_Wrong (x_4542 x_4541))
    57 | Value x_4543 -> h_Value x_4543
    58 | Wrong x_4544 -> h_Wrong x_4544
     54| Interact (o, x_4555) ->
     55  h_Interact o x_4555 (fun x_4554 ->
     56    iO_rect_Type4 h_Interact h_Value h_Wrong (x_4555 x_4554))
     57| Value x_4556 -> h_Value x_4556
     58| Wrong x_4557 -> h_Wrong x_4557
    5959
    6060(** val iO_rect_Type3 :
     
    6262    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
    6363let rec iO_rect_Type3 h_Interact h_Value h_Wrong = function
    64 | Interact (o, x_4558) ->
    65   h_Interact o x_4558 (fun x_4557 ->
    66     iO_rect_Type3 h_Interact h_Value h_Wrong (x_4558 x_4557))
    67 | Value x_4559 -> h_Value x_4559
    68 | Wrong x_4560 -> h_Wrong x_4560
     64| Interact (o, x_4571) ->
     65  h_Interact o x_4571 (fun x_4570 ->
     66    iO_rect_Type3 h_Interact h_Value h_Wrong (x_4571 x_4570))
     67| Value x_4572 -> h_Value x_4572
     68| Wrong x_4573 -> h_Wrong x_4573
    6969
    7070(** val iO_rect_Type2 :
     
    7272    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
    7373let rec iO_rect_Type2 h_Interact h_Value h_Wrong = function
    74 | Interact (o, x_4566) ->
    75   h_Interact o x_4566 (fun x_4565 ->
    76     iO_rect_Type2 h_Interact h_Value h_Wrong (x_4566 x_4565))
    77 | Value x_4567 -> h_Value x_4567
    78 | Wrong x_4568 -> h_Wrong x_4568
     74| Interact (o, x_4579) ->
     75  h_Interact o x_4579 (fun x_4578 ->
     76    iO_rect_Type2 h_Interact h_Value h_Wrong (x_4579 x_4578))
     77| Value x_4580 -> h_Value x_4580
     78| Wrong x_4581 -> h_Wrong x_4581
    7979
    8080(** val iO_rect_Type1 :
     
    8282    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
    8383let rec iO_rect_Type1 h_Interact h_Value h_Wrong = function
    84 | Interact (o, x_4574) ->
    85   h_Interact o x_4574 (fun x_4573 ->
    86     iO_rect_Type1 h_Interact h_Value h_Wrong (x_4574 x_4573))
    87 | Value x_4575 -> h_Value x_4575
    88 | Wrong x_4576 -> h_Wrong x_4576
     84| Interact (o, x_4587) ->
     85  h_Interact o x_4587 (fun x_4586 ->
     86    iO_rect_Type1 h_Interact h_Value h_Wrong (x_4587 x_4586))
     87| Value x_4588 -> h_Value x_4588
     88| Wrong x_4589 -> h_Wrong x_4589
    8989
    9090(** val iO_rect_Type0 :
     
    9292    'a4) -> (Errors.errmsg -> 'a4) -> ('a1, 'a2, 'a3) iO -> 'a4 **)
    9393let rec iO_rect_Type0 h_Interact h_Value h_Wrong = function
    94 | Interact (o, x_4582) ->
    95   h_Interact o x_4582 (fun x_4581 ->
    96     iO_rect_Type0 h_Interact h_Value h_Wrong (x_4582 x_4581))
    97 | Value x_4583 -> h_Value x_4583
    98 | Wrong x_4584 -> h_Wrong x_4584
     94| Interact (o, x_4595) ->
     95  h_Interact o x_4595 (fun x_4594 ->
     96    iO_rect_Type0 h_Interact h_Value h_Wrong (x_4595 x_4594))
     97| Value x_4596 -> h_Value x_4596
     98| Wrong x_4597 -> h_Wrong x_4597
    9999
    100100(** val iO_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.