Changeset 2775 for extracted/vector.ml


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

The compiler now computes also the stack cost model.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/vector.ml

    r2773 r2775  
    4242    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    4343    vector -> 'a2 **)
    44 let rec vector_rect_Type4 h_VEmpty h_VCons x_1761 = function
     44let rec vector_rect_Type4 h_VEmpty h_VCons x_1293 = function
    4545| VEmpty -> h_VEmpty
    46 | VCons (n, x_1764, x_1763) ->
    47   h_VCons n x_1764 x_1763 (vector_rect_Type4 h_VEmpty h_VCons n x_1763)
     46| VCons (n, x_1296, x_1295) ->
     47  h_VCons n x_1296 x_1295 (vector_rect_Type4 h_VEmpty h_VCons n x_1295)
    4848
    4949(** val vector_rect_Type3 :
    5050    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    5151    vector -> 'a2 **)
    52 let rec vector_rect_Type3 h_VEmpty h_VCons x_1773 = function
     52let rec vector_rect_Type3 h_VEmpty h_VCons x_1305 = function
    5353| VEmpty -> h_VEmpty
    54 | VCons (n, x_1776, x_1775) ->
    55   h_VCons n x_1776 x_1775 (vector_rect_Type3 h_VEmpty h_VCons n x_1775)
     54| VCons (n, x_1308, x_1307) ->
     55  h_VCons n x_1308 x_1307 (vector_rect_Type3 h_VEmpty h_VCons n x_1307)
    5656
    5757(** val vector_rect_Type2 :
    5858    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    5959    vector -> 'a2 **)
    60 let rec vector_rect_Type2 h_VEmpty h_VCons x_1779 = function
     60let rec vector_rect_Type2 h_VEmpty h_VCons x_1311 = function
    6161| VEmpty -> h_VEmpty
    62 | VCons (n, x_1782, x_1781) ->
    63   h_VCons n x_1782 x_1781 (vector_rect_Type2 h_VEmpty h_VCons n x_1781)
     62| VCons (n, x_1314, x_1313) ->
     63  h_VCons n x_1314 x_1313 (vector_rect_Type2 h_VEmpty h_VCons n x_1313)
    6464
    6565(** val vector_rect_Type1 :
    6666    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    6767    vector -> 'a2 **)
    68 let rec vector_rect_Type1 h_VEmpty h_VCons x_1785 = function
     68let rec vector_rect_Type1 h_VEmpty h_VCons x_1317 = function
    6969| VEmpty -> h_VEmpty
    70 | VCons (n, x_1788, x_1787) ->
    71   h_VCons n x_1788 x_1787 (vector_rect_Type1 h_VEmpty h_VCons n x_1787)
     70| VCons (n, x_1320, x_1319) ->
     71  h_VCons n x_1320 x_1319 (vector_rect_Type1 h_VEmpty h_VCons n x_1319)
    7272
    7373(** val vector_rect_Type0 :
    7474    'a2 -> (Nat.nat -> 'a1 -> 'a1 vector -> 'a2 -> 'a2) -> Nat.nat -> 'a1
    7575    vector -> 'a2 **)
    76 let rec vector_rect_Type0 h_VEmpty h_VCons x_1791 = function
     76let rec vector_rect_Type0 h_VEmpty h_VCons x_1323 = function
    7777| VEmpty -> h_VEmpty
    78 | VCons (n, x_1794, x_1793) ->
    79   h_VCons n x_1794 x_1793 (vector_rect_Type0 h_VEmpty h_VCons n x_1793)
     78| VCons (n, x_1326, x_1325) ->
     79  h_VCons n x_1326 x_1325 (vector_rect_Type0 h_VEmpty h_VCons n x_1325)
    8080
    8181(** val vector_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.