Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/bitVectorTrie.ml

    r2649 r2717  
    4343    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    4444    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    45 let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_14569 = function
    46 | Leaf x_14571 -> h_Leaf x_14571
    47 | Node (n, x_14573, x_14572) ->
    48   h_Node n x_14573 x_14572
    49     (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14573)
    50     (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14572)
     45let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_4046 = function
     46| Leaf x_4048 -> h_Leaf x_4048
     47| Node (n, x_4050, x_4049) ->
     48  h_Node n x_4050 x_4049
     49    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_4050)
     50    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_4049)
    5151| Stub n -> h_Stub n
    5252
     
    5454    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    5555    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    56 let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_14585 = function
    57 | Leaf x_14587 -> h_Leaf x_14587
    58 | Node (n, x_14589, x_14588) ->
    59   h_Node n x_14589 x_14588
    60     (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14589)
    61     (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14588)
     56let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_4062 = function
     57| Leaf x_4064 -> h_Leaf x_4064
     58| Node (n, x_4066, x_4065) ->
     59  h_Node n x_4066 x_4065
     60    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_4066)
     61    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_4065)
    6262| Stub n -> h_Stub n
    6363
     
    6565    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    6666    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    67 let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_14593 = function
    68 | Leaf x_14595 -> h_Leaf x_14595
    69 | Node (n, x_14597, x_14596) ->
    70   h_Node n x_14597 x_14596
    71     (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14597)
    72     (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14596)
     67let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_4070 = function
     68| Leaf x_4072 -> h_Leaf x_4072
     69| Node (n, x_4074, x_4073) ->
     70  h_Node n x_4074 x_4073
     71    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_4074)
     72    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_4073)
    7373| Stub n -> h_Stub n
    7474
     
    7676    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    7777    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    78 let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_14601 = function
    79 | Leaf x_14603 -> h_Leaf x_14603
    80 | Node (n, x_14605, x_14604) ->
    81   h_Node n x_14605 x_14604
    82     (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14605)
    83     (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14604)
     78let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_4078 = function
     79| Leaf x_4080 -> h_Leaf x_4080
     80| Node (n, x_4082, x_4081) ->
     81  h_Node n x_4082 x_4081
     82    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_4082)
     83    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_4081)
    8484| Stub n -> h_Stub n
    8585
     
    8787    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
    8888    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
    89 let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_14609 = function
    90 | Leaf x_14611 -> h_Leaf x_14611
    91 | Node (n, x_14613, x_14612) ->
    92   h_Node n x_14613 x_14612
    93     (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14613)
    94     (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14612)
     89let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_4086 = function
     90| Leaf x_4088 -> h_Leaf x_4088
     91| Node (n, x_4090, x_4089) ->
     92  h_Node n x_4090 x_4089
     93    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_4090)
     94    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_4089)
    9595| Stub n -> h_Stub n
    9696
Note: See TracChangeset for help on using the changeset viewer.