;;;; Chained comparisons, and the property no checker test can assert: how
;;;; many times each operand runs.
;;;;
;;;; (< a b c) means a < b and b < c. The reading a compiler could otherwise
;;;; have picked, the left fold ((a < b) < c), compares a bool against a
;;;; number and nothing means it. The interesting half is the middle operand:
;;;; two links mention b, and the spelling a reader would write by hand,
;;;; (and (< a b) (< b c)), evaluates it twice. So every operand here comes
;;;; through [mark], which prints its tag, and the printed tags are what say
;;;; each operand ran once and in source order.
;;;;
;;;; The folding operators are marked the same way, because "left to right,
;;;; exactly once" is one claim and it is made about both families.

(defonce calls i32)

;; Prints its tag and answers its value. Every operand below is one of these,
;; so the tag line is a transcript of the evaluation.
(defn mark [tag string v i32] i32
  (set calls (+ calls 1))
  (print tag)
  v)

(defn markf [tag string v f64] f64
  (print tag)
  v)

;; A generic chain, admitted by the predicate its signature carries. The same
;; three-link body as everything above, over a type the function does not know.
(defn between [a $t b $t c $t] bool {:where (ordered? $t)}
  (< a b c))

;; Three unannotated parameters are three dyn ones, so this is the chain the
;; runtime compares rather than the machine.
(defn dyn-rising [a b c] bool
  (< a b c))

;; And the all-pairs reading over dyn operands, which asks the runtime the
;; same question three times rather than twice.
(defn dyn-distinct [a b c] bool
  (!= a b c))

;; Prints y when its two arguments agree and N when they do not. Two bools
;; cannot be compared with = — bool is not an ordered or an equatable type —
;; so the agreement between a chain and the spelling it stands for is said
;; with the operators bool does have.
(defn agree [a bool b bool] ()
  (if (and (or a b) (not (and a b))) (print "N") (print "y")))

(defn line [b bool] ()
  (print " -> ")
  (print b)
  (println ""))

(defn main [] i32
  ;; ── the chain itself ──────────────────────────────────────────────
  (print (< 1 2 3)) (print " ")            ; true
  (print (< 1 5 3)) (print " ")            ; false: the second link
  (print (< 5 1 3)) (print " ")            ; false: the first link
  (print (< 1 2 3 4)) (print " ")          ; true, four operands
  (print (< 1 2 4 3)) (println "")         ; false, four operands

  ;; Every member of the family, chained. The middle link is the false one in
  ;; each of the second column.
  (print (<= 1 1 2)) (print " ") (print (<= 1 2 1)) (print " ")
  (print (> 3 2 1))  (print " ") (print (> 3 1 2))  (print " ")
  (print (>= 3 3 1)) (print " ") (print (>= 3 1 2)) (print " ")
  (print (= 2 2 2))  (print " ") (print (= 2 3 2))
  (println "")

  ;; != is the one that does not chain: it asks whether the operands are all
  ;; different, so the pair it looks at is every pair and not only the
  ;; neighbouring ones. (!= 1 2 1) has no two neighbours alike and is still
  ;; false, which is the whole of the difference.
  (print (!= 1 2 3)) (print " ")           ; true
  (print (!= 1 1 2)) (print " ")           ; false, the adjacent pair
  (print (!= 1 2 1)) (print " ")           ; false, the pair chaining misses
  (print (!= 1 2 3 4)) (print " ")         ; true, six pairs
  (print (!= 1 2 3 1)) (print " ")         ; false, first against last
  (print (!= 1 2 3 2)) (println "")        ; false, a pair in the middle

  ;; The chain and the spelling it stands for agree, everywhere both are
  ;; legal. Written out rather than trusted, because it is the whole claim.
  (agree (< 1 2 3) (and (< 1 2) (< 2 3)))
  (agree (< 1 5 3) (and (< 1 5) (< 5 3)))
  (agree (< 5 1 3) (and (< 5 1) (< 1 3)))
  (agree (<= 1 1 2) (and (<= 1 1) (<= 1 2)))
  (agree (> 3 1 2) (and (> 3 1) (> 1 2)))
  (agree (= 2 3 2) (and (= 2 3) (= 3 2)))
  (agree (< 1 2 3 4) (and (< 1 2) (and (< 2 3) (< 3 4))))
  ;; != stands for the all-pairs spelling, not the adjacent one.
  (agree (!= 1 2 1) (and (!= 1 2) (and (!= 2 1) (!= 1 1))))
  (agree (!= 1 2 3) (and (!= 1 2) (and (!= 1 3) (!= 2 3))))
  (println "")

  ;; ── one evaluation of each operand, in order ──────────────────────
  ;; The first link is true here, so the chain goes on. Three tags.
  (set calls 0)
  (line (< (mark "a" 1) (mark "b" 2) (mark "c" 3)))
  ;; abc -> true

  ;; The first link is *false* here, and the tags still say abc: stopping
  ;; early stops comparing, not running. b appears once although two links
  ;; name it, which is the bug the slots exist to prevent.
  (line (< (mark "a" 9) (mark "b" 1) (mark "c" 5)))
  ;; abc -> false

  ;; Four operands, false in the middle, and every one of them runs.
  (line (< (mark "a" 1) (mark "b" 2) (mark "c" 0) (mark "d" 9)))
  ;; abcd -> false

  ;; Ten marks across three chains is the count, and a middle operand
  ;; evaluated twice would make it eleven.
  (print calls) (println "")               ; 10

  ;; != makes the same promise over its larger set of pairs. All different,
  ;; six comparisons over four operands, four tags.
  (set calls 0)
  (line (!= (mark "a" 1) (mark "b" 2) (mark "c" 3) (mark "d" 4)))
  ;; abcd -> true

  ;; The *first* pair it looks at already says no, and the other three
  ;; operands run anyway: every operand is in its slot before any pair is
  ;; compared, so stopping early stops comparing and nothing else.
  (line (!= (mark "a" 1) (mark "b" 1) (mark "c" 3) (mark "d" 4)))
  ;; abcd -> false

  ;; The pair chaining would never have looked at — first against last.
  (line (!= (mark "a" 1) (mark "b" 2) (mark "c" 3) (mark "d" 1)))
  ;; abcd -> false

  ;; Twelve, and each of the three lines above contributed four. An operand
  ;; named by three pairs evaluated once per pair would say twenty-four.
  (print calls) (println "")               ; 12

  ;; The folding operators make the same promise.
  (set calls 0)
  (print (+ (mark "p" 1) (mark "q" 2) (mark "r" 3))) (println "")   ; pqr6
  (print (- (mark "p" 10) (mark "q" 3) (mark "r" 2))) (println "")  ; pqr5
  (print (* (mark "p" 2) (mark "q" 3) (mark "r" 4))) (println "")   ; pqr24
  (print (min (mark "p" 5) (mark "q" 2) (mark "r" 8))) (println "") ; pqr2
  (print (max (mark "p" 5) (mark "q" 2) (mark "r" 8))) (println "") ; pqr8
  (print calls) (println "")               ; 15

  ;; ── the types a chain admits ──────────────────────────────────────
  ;; One width throughout: the first pair decides, the rest are checked
  ;; against it, and nothing widens implicitly at three operands any more
  ;; than it does at two.
  (let [x (u8 1) y (u8 2) z (u8 3)]
    (print (< x y z)) (print " "))         ; true
  (let [x (i64 -5) y (i64 0) z (i64 5)]
    (print (< x y z)) (print " "))         ; true
  (print (< (markf "f" 1.0) (markf "g" 2.0) (markf "h" 3.0))) (println "")
  ;; true, and fgh printed first

  ;; Strings, which = and != admit and the orderings do not. They are the one
  ;; operand type here that is not a machine word, so they are what says the
  ;; slots a chain binds are slots of whatever type the operands have.
  (print (= "a" "a" "a")) (print " ")      ; true
  (print (= "a" "b" "a")) (print " ")      ; false
  (print (!= "a" "b" "c")) (print " ")     ; true
  (print (!= "a" "b" "a")) (println "")    ; false, the non-adjacent pair

  ;; The generic chain, at two types.
  (print (between (i32 1) (i32 2) (i32 3))) (print " ")   ; true
  (print (between (f64 3.0) (f64 2.0) (f64 1.0))) (println "") ; false

  ;; And the dyn chain, where the runtime does the comparing.
  (print (dyn-rising 1 2 3)) (print " ")   ; true
  (print (dyn-rising 1 5 3)) (print " ")   ; false
  (print (dyn-distinct 1 2 3)) (print " ") ; true
  (print (dyn-distinct 1 2 1)) (println "") ; false, the non-adjacent pair
  0)