Changeset 2775 for extracted/monad.ml


Ignore:
Timestamp:
Mar 5, 2013, 9:52:39 PM (7 years ago)
Author:
sacerdot
Message:

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/monad.ml

    r2773 r2775  
    2525    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    2626    -> monad -> 'a1 **)
    27 let rec monad_rect_Type4 h_mk_Monad x_1474 =
    28   let { m_return = m_return0; m_bind = m_bind0 } = x_1474 in
     27let rec monad_rect_Type4 h_mk_Monad x_744 =
     28  let { m_return = m_return0; m_bind = m_bind0 } = x_744 in
    2929  h_mk_Monad __ m_return0 m_bind0
    3030
     
    3232    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    3333    -> monad -> 'a1 **)
    34 let rec monad_rect_Type5 h_mk_Monad x_1476 =
    35   let { m_return = m_return0; m_bind = m_bind0 } = x_1476 in
     34let rec monad_rect_Type5 h_mk_Monad x_746 =
     35  let { m_return = m_return0; m_bind = m_bind0 } = x_746 in
    3636  h_mk_Monad __ m_return0 m_bind0
    3737
     
    3939    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    4040    -> monad -> 'a1 **)
    41 let rec monad_rect_Type3 h_mk_Monad x_1478 =
    42   let { m_return = m_return0; m_bind = m_bind0 } = x_1478 in
     41let rec monad_rect_Type3 h_mk_Monad x_748 =
     42  let { m_return = m_return0; m_bind = m_bind0 } = x_748 in
    4343  h_mk_Monad __ m_return0 m_bind0
    4444
     
    4646    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    4747    -> monad -> 'a1 **)
    48 let rec monad_rect_Type2 h_mk_Monad x_1480 =
    49   let { m_return = m_return0; m_bind = m_bind0 } = x_1480 in
     48let rec monad_rect_Type2 h_mk_Monad x_750 =
     49  let { m_return = m_return0; m_bind = m_bind0 } = x_750 in
    5050  h_mk_Monad __ m_return0 m_bind0
    5151
     
    5353    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    5454    -> monad -> 'a1 **)
    55 let rec monad_rect_Type1 h_mk_Monad x_1482 =
    56   let { m_return = m_return0; m_bind = m_bind0 } = x_1482 in
     55let rec monad_rect_Type1 h_mk_Monad x_752 =
     56  let { m_return = m_return0; m_bind = m_bind0 } = x_752 in
    5757  h_mk_Monad __ m_return0 m_bind0
    5858
     
    6060    (__ -> (__ -> __ -> __) -> (__ -> __ -> __ -> (__ -> __) -> __) -> 'a1)
    6161    -> monad -> 'a1 **)
    62 let rec monad_rect_Type0 h_mk_Monad x_1484 =
    63   let { m_return = m_return0; m_bind = m_bind0 } = x_1484 in
     62let rec monad_rect_Type0 h_mk_Monad x_754 =
     63  let { m_return = m_return0; m_bind = m_bind0 } = x_754 in
    6464  h_mk_Monad __ m_return0 m_bind0
    6565
     
    6767
    6868(** val m_return0 : monad -> 'a1 -> __ **)
    69 let rec m_return0 xxx x_1501 =
    70   (let { m_return = yyy; m_bind = x0 } = xxx in Obj.magic yyy) __ x_1501
     69let rec m_return0 xxx x_771 =
     70  (let { m_return = yyy; m_bind = x0 } = xxx in Obj.magic yyy) __ x_771
    7171
    7272(** val m_bind0 : monad -> __ -> ('a1 -> __) -> __ **)
    73 let rec m_bind0 xxx x_1498 x_1499 =
    74   (let { m_return = x0; m_bind = yyy } = xxx in Obj.magic yyy) __ __ x_1498
    75     x_1499
     73let rec m_bind0 xxx x_768 x_769 =
     74  (let { m_return = x0; m_bind = yyy } = xxx in Obj.magic yyy) __ __ x_768
     75    x_769
    7676
    7777(** val monad_inv_rect_Type4 :
     
    111111(** val monadProps_rect_Type4 :
    112112    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
    113 let rec monadProps_rect_Type4 h_mk_MonadProps x_1505 =
    114   let max_def = x_1505 in h_mk_MonadProps max_def __ __ __ __
     113let rec monadProps_rect_Type4 h_mk_MonadProps x_775 =
     114  let max_def = x_775 in h_mk_MonadProps max_def __ __ __ __
    115115
    116116(** val monadProps_rect_Type5 :
    117117    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
    118 let rec monadProps_rect_Type5 h_mk_MonadProps x_1507 =
    119   let max_def = x_1507 in h_mk_MonadProps max_def __ __ __ __
     118let rec monadProps_rect_Type5 h_mk_MonadProps x_777 =
     119  let max_def = x_777 in h_mk_MonadProps max_def __ __ __ __
    120120
    121121(** val monadProps_rect_Type3 :
    122122    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
    123 let rec monadProps_rect_Type3 h_mk_MonadProps x_1509 =
    124   let max_def = x_1509 in h_mk_MonadProps max_def __ __ __ __
     123let rec monadProps_rect_Type3 h_mk_MonadProps x_779 =
     124  let max_def = x_779 in h_mk_MonadProps max_def __ __ __ __
    125125
    126126(** val monadProps_rect_Type2 :
    127127    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
    128 let rec monadProps_rect_Type2 h_mk_MonadProps x_1511 =
    129   let max_def = x_1511 in h_mk_MonadProps max_def __ __ __ __
     128let rec monadProps_rect_Type2 h_mk_MonadProps x_781 =
     129  let max_def = x_781 in h_mk_MonadProps max_def __ __ __ __
    130130
    131131(** val monadProps_rect_Type1 :
    132132    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
    133 let rec monadProps_rect_Type1 h_mk_MonadProps x_1513 =
    134   let max_def = x_1513 in h_mk_MonadProps max_def __ __ __ __
     133let rec monadProps_rect_Type1 h_mk_MonadProps x_783 =
     134  let max_def = x_783 in h_mk_MonadProps max_def __ __ __ __
    135135
    136136(** val monadProps_rect_Type0 :
    137137    (monad -> __ -> __ -> __ -> __ -> 'a1) -> monadProps -> 'a1 **)
    138 let rec monadProps_rect_Type0 h_mk_MonadProps x_1515 =
    139   let max_def = x_1515 in h_mk_MonadProps max_def __ __ __ __
     138let rec monadProps_rect_Type0 h_mk_MonadProps x_785 =
     139  let max_def = x_785 in h_mk_MonadProps max_def __ __ __ __
    140140
    141141(** val max_def : monadProps -> monad **)
     
    168168  let hcut = monadProps_rect_Type0 h1 hterm in hcut __
    169169
    170 type 'x_1502 max_def__o__monad = __
     170type 'x_772 max_def__o__monad = __
    171171
    172172type setoidMonadProps =
     
    177177    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    178178    setoidMonadProps -> 'a1 **)
    179 let rec setoidMonadProps_rect_Type4 h_mk_SetoidMonadProps x_1537 =
    180   let smax_def = x_1537 in
     179let rec setoidMonadProps_rect_Type4 h_mk_SetoidMonadProps x_807 =
     180  let smax_def = x_807 in
    181181  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
    182182
     
    184184    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    185185    setoidMonadProps -> 'a1 **)
    186 let rec setoidMonadProps_rect_Type5 h_mk_SetoidMonadProps x_1539 =
    187   let smax_def = x_1539 in
     186let rec setoidMonadProps_rect_Type5 h_mk_SetoidMonadProps x_809 =
     187  let smax_def = x_809 in
    188188  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
    189189
     
    191191    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    192192    setoidMonadProps -> 'a1 **)
    193 let rec setoidMonadProps_rect_Type3 h_mk_SetoidMonadProps x_1541 =
    194   let smax_def = x_1541 in
     193let rec setoidMonadProps_rect_Type3 h_mk_SetoidMonadProps x_811 =
     194  let smax_def = x_811 in
    195195  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
    196196
     
    198198    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    199199    setoidMonadProps -> 'a1 **)
    200 let rec setoidMonadProps_rect_Type2 h_mk_SetoidMonadProps x_1543 =
    201   let smax_def = x_1543 in
     200let rec setoidMonadProps_rect_Type2 h_mk_SetoidMonadProps x_813 =
     201  let smax_def = x_813 in
    202202  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
    203203
     
    205205    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    206206    setoidMonadProps -> 'a1 **)
    207 let rec setoidMonadProps_rect_Type1 h_mk_SetoidMonadProps x_1545 =
    208   let smax_def = x_1545 in
     207let rec setoidMonadProps_rect_Type1 h_mk_SetoidMonadProps x_815 =
     208  let smax_def = x_815 in
    209209  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
    210210
     
    212212    (monad -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> __ -> 'a1) ->
    213213    setoidMonadProps -> 'a1 **)
    214 let rec setoidMonadProps_rect_Type0 h_mk_SetoidMonadProps x_1547 =
    215   let smax_def = x_1547 in
     214let rec setoidMonadProps_rect_Type0 h_mk_SetoidMonadProps x_817 =
     215  let smax_def = x_817 in
    216216  h_mk_SetoidMonadProps smax_def __ __ __ __ __ __ __ __ __
    217217
     
    250250  let hcut = setoidMonadProps_rect_Type0 h1 hterm in hcut __
    251251
    252 type 'x_1502 smax_def__o__monad = __
     252type 'x_772 smax_def__o__monad = __
    253253
    254254(** val setoid_of_monad : setoidMonadProps -> Setoids.setoid **)
     
    299299let m_list_map_sigma m f l =
    300300  List.foldr (fun el macc ->
    301     m_bind0 m (f el) (fun eta367 ->
    302       let r = eta367 in
    303       m_bind0 m macc (fun eta366 ->
    304         let acc = eta366 in m_return0 m (List.Cons (r, acc)))))
     301    m_bind0 m (f el) (fun eta285 ->
     302      let r = eta285 in
     303      m_bind0 m macc (fun eta284 ->
     304        let acc = eta284 in m_return0 m (List.Cons (r, acc)))))
    305305    (m_return0 m List.Nil) l
    306306
     
    401401    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    402402    injMonadPred -> 'a1 **)
    403 let rec injMonadPred_rect_Type4 m h_mk_InjMonadPred x_1607 =
    404   let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1607 in
     403let rec injMonadPred_rect_Type4 m h_mk_InjMonadPred x_1048 =
     404  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1048 in
    405405  h_mk_InjMonadPred im_pred0 mp_inject0 __
    406406
     
    408408    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    409409    injMonadPred -> 'a1 **)
    410 let rec injMonadPred_rect_Type5 m h_mk_InjMonadPred x_1609 =
    411   let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1609 in
     410let rec injMonadPred_rect_Type5 m h_mk_InjMonadPred x_1050 =
     411  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1050 in
    412412  h_mk_InjMonadPred im_pred0 mp_inject0 __
    413413
     
    415415    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    416416    injMonadPred -> 'a1 **)
    417 let rec injMonadPred_rect_Type3 m h_mk_InjMonadPred x_1611 =
    418   let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1611 in
     417let rec injMonadPred_rect_Type3 m h_mk_InjMonadPred x_1052 =
     418  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1052 in
    419419  h_mk_InjMonadPred im_pred0 mp_inject0 __
    420420
     
    422422    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    423423    injMonadPred -> 'a1 **)
    424 let rec injMonadPred_rect_Type2 m h_mk_InjMonadPred x_1613 =
    425   let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1613 in
     424let rec injMonadPred_rect_Type2 m h_mk_InjMonadPred x_1054 =
     425  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1054 in
    426426  h_mk_InjMonadPred im_pred0 mp_inject0 __
    427427
     
    429429    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    430430    injMonadPred -> 'a1 **)
    431 let rec injMonadPred_rect_Type1 m h_mk_InjMonadPred x_1615 =
    432   let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1615 in
     431let rec injMonadPred_rect_Type1 m h_mk_InjMonadPred x_1056 =
     432  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1056 in
    433433  h_mk_InjMonadPred im_pred0 mp_inject0 __
    434434
     
    436436    monad -> (monadPred -> (__ -> __ -> __ Types.sig0 -> __) -> __ -> 'a1) ->
    437437    injMonadPred -> 'a1 **)
    438 let rec injMonadPred_rect_Type0 m h_mk_InjMonadPred x_1617 =
    439   let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1617 in
     438let rec injMonadPred_rect_Type0 m h_mk_InjMonadPred x_1058 =
     439  let { im_pred = im_pred0; mp_inject = mp_inject0 } = x_1058 in
    440440  h_mk_InjMonadPred im_pred0 mp_inject0 __
    441441
     
    445445
    446446(** val mp_inject0 : monad -> injMonadPred -> __ Types.sig0 -> __ **)
    447 let rec mp_inject0 m xxx x_1632 =
    448   (xxx.mp_inject) __ __ x_1632
     447let rec mp_inject0 m xxx x_1073 =
     448  (xxx.mp_inject) __ __ x_1073
    449449
    450450(** val injMonadPred_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.