Representation.Partition

1module Representation.Partition
2
3import Std.Foundation
4import Std.List
5import Std.Natural
6
7-- Coordinates name logical items, not addresses, ranks, or tensor layouts.
8-- A caller may use a stable ordinal enumeration of keys or population IDs.
9-- Half-open intervals allow empty assignments without inventing padding work.
10family LogicalInterval : Type 0
11constructor LogicalIntervalOf
12field unrestricted logicalIntervalBegin : Nat
13field unrestricted logicalIntervalEnd : Nat
14
15end-family
16
17family PartitionFailure : Type 0
18constructor PartitionNoParticipants
19constructor PartitionParticipantOutside
20constructor PartitionExtentOutsideWord
21
22end-family
23
24def intervalBegin =
25  (lambda unrestricted interval : (family LogicalInterval) .
26    (eliminate
27      LogicalInterval
28      (lambda unrestricted current : (family LogicalInterval) . Nat)
29      interval
30      (branch LogicalIntervalOf begin end . begin)))
31
32def intervalEnd =
33  (lambda unrestricted interval : (family LogicalInterval) .
34    (eliminate
35      LogicalInterval
36      (lambda unrestricted current : (family LogicalInterval) . Nat)
37      interval
38      (branch LogicalIntervalOf begin end . end)))
39
40def intervalExtent =
41  (lambda unrestricted interval : (family LogicalInterval) .
42    (naturalSaturatingSubtract (intervalEnd interval) (intervalBegin interval)))
43
44-- A disjoint intersection is an empty interval at the larger begin. Preserve
45-- begin <= end so downstream consumers can reuse the ordinary interval laws.
46def intervalIntersection =
47  (lambda unrestricted left : (family LogicalInterval) .
48    (lambda unrestricted right : (family LogicalInterval) .
49      (let unrestricted begin =
50        (naturalSelect
51          (naturalLess (intervalBegin left) (intervalBegin right))
52          (intervalBegin right)
53          (intervalBegin left))
54        in
55        (let unrestricted end =
56          (naturalMinimum (intervalEnd left) (intervalEnd right))
57          in
58          (constructor
59            LogicalInterval
60            LogicalIntervalOf
61            begin
62            (naturalSelect (naturalLess end begin) begin end))))))
63
64def intervalWithin =
65  (lambda unrestricted extent : Nat .
66    (lambda unrestricted interval : (family LogicalInterval) .
67      (naturalAnd
68        (naturalLessOrEqual (intervalBegin interval) (intervalEnd interval))
69        (naturalLessOrEqual (intervalEnd interval) extent))))
70
71-- Validate ordered coverage in one pass over fragments, not over coordinates.
72-- Checking only summed lengths would accept an overlap paired with a hole.
73-- Requiring the next begin to equal the previous end detects both, including
74-- at the boundaries. Unordered input must be canonicalized by its owner first.
75def intervalPartitionValid :
76  (pi unrestricted extent : Nat .
77    (pi unrestricted intervals : (family StdList (family LogicalInterval)) . Nat)) =
78  (lambda unrestricted extent : Nat .
79    (lambda unrestricted intervals : (family StdList (family LogicalInterval)) .
80      (app
81        (eliminate
82          StdList
83          (lambda unrestricted current : (family StdList (family LogicalInterval)) .
84            (pi unrestricted cursor : Nat . Nat))
85          intervals
86          (branch StdListEmpty . (lambda unrestricted cursor : Nat . (naturalEqual cursor extent)))
87          (branch
88            StdListCons
89            head
90            tail
91            induction
92            .
93            (lambda unrestricted cursor : Nat .
94              (naturalAnd
95                (naturalEqual cursor (intervalBegin head))
96                (naturalAnd (intervalWithin extent head) (induction (intervalEnd head)))))))
97        0)))
98
99-- Project one role from a regular partition in constant arithmetic work.
100-- The quotient/remainder law keeps every endpoint <= extent; intermediate
101-- multiplication cannot overflow for an admitted role and U64 extent.
102-- No list of 200,000 ranks and no recursion on an integer magnitude is built.
103def balancedIntervalUnchecked =
104  (lambda unrestricted extent : Nat .
105    (lambda unrestricted participants : Nat .
106      (lambda unrestricted role : Nat .
107        (app
108          (lambda unrestricted quotient : Nat .
109            (app
110              (lambda unrestricted remainder : Nat .
111                (app
112                  (lambda unrestricted begin : Nat .
113                    (constructor
114                      LogicalInterval
115                      LogicalIntervalOf
116                      begin
117                      (naturalAdd begin (naturalAdd quotient (naturalLess role remainder)))))
118                  (naturalAdd (naturalMultiply quotient role) (naturalMinimum role remainder))))
119              (naturalModuloUnchecked extent participants)))
120          (naturalDivideUnchecked extent participants)))))
121
122def balancedInterval =
123  (lambda unrestricted extent : Nat .
124    (lambda unrestricted participants : Nat .
125      (lambda unrestricted role : Nat .
126        (nat-eliminate
127          (lambda unrestricted flag : Nat .
128            (family StdResult (family PartitionFailure) (family LogicalInterval)))
129          (constructor
130            StdResult
131            StdFailure
132            (family PartitionFailure)
133            (family LogicalInterval)
134            (constructor PartitionFailure PartitionExtentOutsideWord))
135          (lambda unrestricted predecessor : Nat .
136            (lambda unrestricted induction : (family StdResult (family PartitionFailure) (family LogicalInterval)) .
137              (nat-eliminate
138                (lambda unrestricted flag : Nat .
139                  (family StdResult (family PartitionFailure) (family LogicalInterval)))
140                (constructor
141                  StdResult
142                  StdFailure
143                  (family PartitionFailure)
144                  (family LogicalInterval)
145                  (constructor PartitionFailure PartitionNoParticipants))
146                (lambda unrestricted previous : Nat .
147                  (lambda unrestricted rest : (family StdResult (family PartitionFailure) (family LogicalInterval)) .
148                    (nat-eliminate
149                      (lambda unrestricted flag : Nat .
150                        (family StdResult (family PartitionFailure) (family LogicalInterval)))
151                      (constructor
152                        StdResult
153                        StdFailure
154                        (family PartitionFailure)
155                        (family LogicalInterval)
156                        (constructor PartitionFailure PartitionParticipantOutside))
157                      (lambda unrestricted before : Nat .
158                        (lambda unrestricted ignored : (family StdResult (family PartitionFailure) (family LogicalInterval)) .
159                          (constructor
160                            StdResult
161                            StdSuccess
162                            (family PartitionFailure)
163                            (family LogicalInterval)
164                            (balancedIntervalUnchecked extent participants role))))
165                      (naturalLess role participants))))
166                (naturalNonzero participants))))
167          (naturalLessOrEqual extent 18446744073709551615)))))