Changeset 3043 for extracted/iOMonad.ml


Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/iOMonad.ml

    r2997 r3043  
    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_4775) ->
    55   h_Interact o x_4775 (fun x_4774 ->
    56     iO_rect_Type4 h_Interact h_Value h_Wrong (x_4775 x_4774))
    57 | Value x_4776 -> h_Value x_4776
    58 | Wrong x_4777 -> h_Wrong x_4777
     54| Interact (o, x_4685) ->
     55  h_Interact o x_4685 (fun x_4684 ->
     56    iO_rect_Type4 h_Interact h_Value h_Wrong (x_4685 x_4684))
     57| Value x_4686 -> h_Value x_4686
     58| Wrong x_4687 -> h_Wrong x_4687
    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_4791) ->
    65   h_Interact o x_4791 (fun x_4790 ->
    66     iO_rect_Type3 h_Interact h_Value h_Wrong (x_4791 x_4790))
    67 | Value x_4792 -> h_Value x_4792
    68 | Wrong x_4793 -> h_Wrong x_4793
     64| Interact (o, x_4701) ->
     65  h_Interact o x_4701 (fun x_4700 ->
     66    iO_rect_Type3 h_Interact h_Value h_Wrong (x_4701 x_4700))
     67| Value x_4702 -> h_Value x_4702
     68| Wrong x_4703 -> h_Wrong x_4703
    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_4799) ->
    75   h_Interact o x_4799 (fun x_4798 ->
    76     iO_rect_Type2 h_Interact h_Value h_Wrong (x_4799 x_4798))
    77 | Value x_4800 -> h_Value x_4800
    78 | Wrong x_4801 -> h_Wrong x_4801
     74| Interact (o, x_4709) ->
     75  h_Interact o x_4709 (fun x_4708 ->
     76    iO_rect_Type2 h_Interact h_Value h_Wrong (x_4709 x_4708))
     77| Value x_4710 -> h_Value x_4710
     78| Wrong x_4711 -> h_Wrong x_4711
    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_4807) ->
    85   h_Interact o x_4807 (fun x_4806 ->
    86     iO_rect_Type1 h_Interact h_Value h_Wrong (x_4807 x_4806))
    87 | Value x_4808 -> h_Value x_4808
    88 | Wrong x_4809 -> h_Wrong x_4809
     84| Interact (o, x_4717) ->
     85  h_Interact o x_4717 (fun x_4716 ->
     86    iO_rect_Type1 h_Interact h_Value h_Wrong (x_4717 x_4716))
     87| Value x_4718 -> h_Value x_4718
     88| Wrong x_4719 -> h_Wrong x_4719
    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_4815) ->
    95   h_Interact o x_4815 (fun x_4814 ->
    96     iO_rect_Type0 h_Interact h_Value h_Wrong (x_4815 x_4814))
    97 | Value x_4816 -> h_Value x_4816
    98 | Wrong x_4817 -> h_Wrong x_4817
     94| Interact (o, x_4725) ->
     95  h_Interact o x_4725 (fun x_4724 ->
     96    iO_rect_Type0 h_Interact h_Value h_Wrong (x_4725 x_4724))
     97| Value x_4726 -> h_Value x_4726
     98| Wrong x_4727 -> h_Wrong x_4727
    9999
    100100(** val iO_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.