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

    r2775 r2797  
    4949    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    5050    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    51 let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_14634 = function
    52 | Leaf x_14636 -> h_Leaf x_14636
    53 | Node (n, x_14638, x_14637) ->
    54   h_Node n x_14638 x_14637
    55     (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14638)
    56     (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14637)
     51let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_14647 = function
     52| Leaf x_14649 -> h_Leaf x_14649
     53| Node (n, x_14651, x_14650) ->
     54  h_Node n x_14651 x_14650
     55    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14651)
     56    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14650)
    5757| Stub n -> h_Stub n
    5858
     
    6060    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    6161    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    62 let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_14650 = function
    63 | Leaf x_14652 -> h_Leaf x_14652
    64 | Node (n, x_14654, x_14653) ->
    65   h_Node n x_14654 x_14653
    66     (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14654)
    67     (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14653)
     62let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_14663 = function
     63| Leaf x_14665 -> h_Leaf x_14665
     64| Node (n, x_14667, x_14666) ->
     65  h_Node n x_14667 x_14666
     66    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14667)
     67    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14666)
    6868| Stub n -> h_Stub n
    6969
     
    7171    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    7272    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    73 let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_14658 = function
    74 | Leaf x_14660 -> h_Leaf x_14660
    75 | Node (n, x_14662, x_14661) ->
    76   h_Node n x_14662 x_14661
    77     (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14662)
    78     (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14661)
     73let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_14671 = function
     74| Leaf x_14673 -> h_Leaf x_14673
     75| Node (n, x_14675, x_14674) ->
     76  h_Node n x_14675 x_14674
     77    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14675)
     78    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14674)
    7979| Stub n -> h_Stub n
    8080
     
    8282    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    8383    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    84 let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_14666 = function
    85 | Leaf x_14668 -> h_Leaf x_14668
    86 | Node (n, x_14670, x_14669) ->
    87   h_Node n x_14670 x_14669
    88     (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14670)
    89     (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14669)
     84let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_14679 = function
     85| Leaf x_14681 -> h_Leaf x_14681
     86| Node (n, x_14683, x_14682) ->
     87  h_Node n x_14683 x_14682
     88    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14683)
     89    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14682)
    9090| Stub n -> h_Stub n
    9191
     
    9393    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    9494    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    95 let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_14674 = function
    96 | Leaf x_14676 -> h_Leaf x_14676
    97 | Node (n, x_14678, x_14677) ->
    98   h_Node n x_14678 x_14677
    99     (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14678)
    100     (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14677)
     95let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_14687 = function
     96| Leaf x_14689 -> h_Leaf x_14689
     97| Node (n, x_14691, x_14690) ->
     98  h_Node n x_14691 x_14690
     99    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14691)
     100    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14690)
    101101| Stub n -> h_Stub n
    102102
Note: See TracChangeset for help on using the changeset viewer.