001    package fj.data.hlist;
002    
003    import fj.F;
004    import fj.pre.Show;
005    
006    /**
007     * A basic prelude of values lifted into the type system.
008     */
009    @SuppressWarnings({"ALL"})
010    public final class HPre {
011      private HPre() {
012        throw new UnsupportedOperationException();
013      }
014    
015      /**
016       * A type-level Boolean
017       */
018      public static class HBool {
019        private HBool() {
020        }
021      }
022    
023      /**
024       * Boolean true
025       */
026      public static class HTrue extends HBool {
027        private HTrue() {
028        }
029      }
030    
031      /**
032       * Boolean false
033       */
034      public static class HFalse extends HBool {
035        private HFalse() {
036        }
037      }
038    
039      private static final HTrue hTrue = new HTrue();
040      private static final HFalse hFalse = new HFalse();
041    
042      /**
043       * Returns a boolean value whose type represents truth.
044       *
045       * @return a boolean value whose type represents truth.
046       */
047      public static HTrue hTrue() {
048        return hTrue;
049      }
050    
051      /**
052       * Returns a boolean value whose type represents falsehood.
053       *
054       * @return a boolean value whose type represents falsehood.
055       */
056      public static HFalse hFalse() {
057        return hFalse;
058      }
059    
060      /**
061       * Type-level boolean conjunction. A value of this type represents evidence that AB -> C
062       *
063       * @param <A> A boolean
064       * @param <B> A boolean
065       * @param <C> The logical implication of A and B
066       */
067      public static final class HAnd<A extends HBool, B extends HBool, C extends HBool> {
068        private final C v;
069    
070        private HAnd(final C v) {
071          this.v = v;
072        }
073    
074        public C v() {
075          return v;
076        }
077    
078        public static HAnd<HFalse, HFalse, HFalse> hAnd(final HFalse a, final HFalse b) {
079          return new HAnd<HFalse, HFalse, HFalse>(hFalse());
080        }
081    
082        public static HAnd<HTrue, HFalse, HFalse> hAnd(final HTrue a, final HFalse b) {
083          return new HAnd<HTrue, HFalse, HFalse>(hFalse());
084        }
085    
086        public static HAnd<HFalse, HTrue, HFalse> hAnd(final HFalse a, final HTrue b) {
087          return new HAnd<HFalse, HTrue, HFalse>(hFalse());
088        }
089    
090        public static HAnd<HTrue, HTrue, HTrue> hAnd(final HTrue a, final HTrue b) {
091          return new HAnd<HTrue, HTrue, HTrue>(hTrue());
092        }
093      }
094    
095      /**
096       * Type-level boolean disjunction. A value of this type represents evidence that A+B -> C
097       *
098       * @param <A> A boolean
099       * @param <B> A boolean
100       * @param <C> The logical implication of A or B
101       */
102      public static final class HOr<A extends HBool, B extends HBool, C extends HBool> {
103        private final C v;
104    
105        private HOr(final C v) {
106          this.v = v;
107        }
108    
109        public C v() {
110          return v;
111        }
112    
113        public static HOr<HFalse, HFalse, HFalse> hOr(final HFalse a, final HFalse b) {
114          return new HOr<HFalse, HFalse, HFalse>(hFalse());
115        }
116    
117        public static HOr<HTrue, HFalse, HTrue> hOr(final HTrue a, final HFalse b) {
118          return new HOr<HTrue, HFalse, HTrue>(hTrue());
119        }
120    
121        public static HOr<HFalse, HTrue, HTrue> hOr(final HFalse a, final HTrue b) {
122          return new HOr<HFalse, HTrue, HTrue>(hTrue());
123        }
124    
125        public static HOr<HTrue, HTrue, HTrue> hOr(final HTrue a, final HTrue b) {
126          return new HOr<HTrue, HTrue, HTrue>(hTrue());
127        }
128      }
129    
130      /**
131       * A type-level conditional. The type of the last parameter is implied by the first three.
132       *
133       * @param <T> A boolean
134       * @param <X> The type of Z if T is true.
135       * @param <Y> The type of Z if T is false.
136       * @param <Z> A type that is either X or Z, depending on T.
137       */
138      public static final class HCond<T, X, Y, Z> {
139        private HCond(final Z z) {
140          this.z = z;
141        }
142    
143        private final Z z;
144    
145        public Z v() {
146          return z;
147        }
148    
149        public static <X, Y> HCond<HFalse, X, Y, Y> hCond(final HFalse t, final X x, final Y y) {
150          return new HCond<HFalse, X, Y, Y>(y);
151        }
152    
153        public static <X, Y> HCond<HTrue, X, Y, X> hCond(final HTrue t, final X x, final Y y) {
154          return new HCond<HTrue, X, Y, X>(x);
155        }
156      }
157    
158      /**
159       * Type-level natural numbers.
160       */
161      public abstract static class HNat<A extends HNat<A>> {
162        public abstract Show<A> show();
163    
164        public abstract Integer toInteger();
165    
166        public static HZero hZero() {
167          return new HZero();
168        }
169    
170        public static <N extends HNat<N>> HSucc<N> hSucc(final N n) {
171          return new HSucc<N>(n);
172        }
173    
174        public static <N extends HNat<N>> N hPred(final HSucc<N> n) {
175          return n.pred;
176        }
177      }
178    
179      /**
180       * Type-level zero
181       */
182      public static final class HZero extends HNat<HZero> {
183        private HZero() {
184        }
185    
186        public Show<HZero> show() {
187          return Show.showS(new F<HZero, String>() {
188            public String f(final HZero hZero) {
189              return "HZero";
190            }
191          });
192        }
193    
194        public Integer toInteger() {
195          return 0;
196        }
197      }
198    
199      /**
200       * A natural number N + 1
201       *
202       * @param <N> The predecessor of this number.
203       */
204      public static final class HSucc<N extends HNat<N>> extends HNat<HSucc<N>> {
205        private HSucc(final N n) {
206          pred = n;
207        }
208    
209        private final N pred;
210    
211        public Show<HSucc<N>> show() {
212          return Show.showS(new F<HSucc<N>, String>() {
213            public String f(final HSucc<N> s) {
214              return "HSucc (" + s.show().showS(s) + ')';
215            }
216          });
217        }
218    
219        public Integer toInteger() {
220          return 1 + pred.toInteger();
221        }
222      }
223    
224      /**
225       * Type-level equality. Represents evidence for X and Y being equal, or counterevidence against.
226       */
227      public static final class HEq<X, Y, B extends HBool> {
228        private final B v;
229    
230        private HEq(final B v) {
231          this.v = v;
232        }
233    
234        public B v() {
235          return v;
236        }
237    
238        /**
239         * Zero is equal to itself.
240         *
241         * @param a Zero
242         * @param b Zero
243         * @return Equality for Zero
244         */
245        public static HEq<HZero, HZero, HTrue> eq(final HZero a, final HZero b) {
246          return new HEq<HZero, HZero, HTrue>(hTrue());
247        }
248    
249        /**
250         * Zero is not equal to anything other than zero.
251         */
252        public static <N extends HNat<N>> HEq<HZero, HSucc<N>, HFalse> eq(final HZero a, final HSucc<N> b) {
253          return new HEq<HZero, HSucc<N>, HFalse>(hFalse());
254        }
255    
256        /**
257         * Zero is not equal to anything other than zero.
258         */
259        public static <N extends HNat<N>> HEq<HSucc<N>, HZero, HFalse> eq(final HSucc<N> a, final HZero b) {
260          return new HEq<HSucc<N>, HZero, HFalse>(hFalse());
261        }
262    
263        /**
264         * A number is equal to another if their predecessors are equal.
265         */
266        public static <N extends HNat<N>, NN extends HNat<NN>, B extends HBool, E extends HEq<N, NN, B>>
267        HEq<HSucc<N>, HSucc<NN>, B> eq(final HSucc<N> a, final HSucc<NN> b, final E e) {
268          return new HEq<HSucc<N>, HSucc<NN>, B>(e.v);
269        }
270    
271      }
272    
273      /**
274       * Type-level integer arithmetic
275       */
276      public static final class HAdd<A extends HNat<A>, B extends HNat<B>, C extends HNat<C>> {
277        private final C sum;
278    
279        private HAdd(final C sum) {
280          this.sum = sum;
281        }
282    
283        /**
284         * The sum of zero and any other number is that number.
285         */
286        public static <N extends HNat<N>> HAdd<HZero, HSucc<N>, HSucc<N>> add(final HZero a, final HSucc<N> b) {
287          return new HAdd<HZero, HSucc<N>, HSucc<N>>(b);
288        }
289    
290        /**
291         * The sum of zero and any other number is that number.
292         */
293        public static <N extends HNat<N>> HAdd<HSucc<N>, HZero, HSucc<N>> add(final HSucc<N> a, final HZero b) {
294          return new HAdd<HSucc<N>, HZero, HSucc<N>>(a);
295        }
296    
297        /**
298         * The sum of numbers a and b is one greater than the sum of b and the predecessor of a.
299         */
300        public static <N extends HNat<N>, M extends HNat<M>, R extends HNat<R>, H extends HAdd<N, HSucc<M>, R>>
301        HAdd<HSucc<N>, HSucc<M>, HSucc<R>> add(final HSucc<N> a, final HSucc<M> b, final H h) {
302          return new HAdd<HSucc<N>, HSucc<M>, HSucc<R>>(HNat.hSucc(h.sum));
303        }
304      }
305    
306    }