(in-package "ACL2")

(include-book "std/top" :dir :system)
(include-book "centaur/gl/gl" :dir :system)
(include-book "centaur/gl/def-gl-rule" :dir :system)
(include-book "centaur/gl/bfr-satlink" :dir :system)

(def-gl-clause-processor my-glcp)

(make-event (prog2$ (tshell-ensure)
                    '(value-triple :invisible))
            :check-expansion t)

(defun verbose-glucose-config ()
  (declare (xargs :guard t))
  (satlink::make-config :cmdline "glucose-cert"
                        :verbose t
                        :mintime 1/2
                        :remove-temps t))

(defattach gl::gl-satlink-config verbose-glucose-config)
(gl::gl-satlink-mode)

(std::defenum player-count-p
  (:zero :one :two))

(defconst *baseball* 0)
(defconst *basketball* 1)
(defconst *soccerball* 2)
(defconst *volleyball* 3)

(make-event
 `(std::defenum ball-p
                (,*baseball* ,*basketball* ,*soccerball* ,*volleyball*)))

(std::defaggregate sport
  ((player-count player-count-p
                 "Number of players, denoted with symbols instead of integers.")
   (ball ball-p))
  :legiblep
  :ordered)

(define set-sport-to-basketball
  ((sport sport-p))
  (change-sport sport :ball *basketball*))

(defrule basketball-p-of-set-sport-to-basketball
  (implies (sport-p sport)
           (equal (sport->ball (set-sport-to-basketball sport))
                  *basketball*))
  :enable (set-sport-to-basketball))

(in-theory (enable sport-p ball-p player-count-p))

(def-gl-rule basketball-p-of-set-sport-to-basketball-via-gl
  :hyp (sport-p sport)
  :concl (equal (sport->ball (set-sport-to-basketball sport))
                *basketball*)
; Mimics the following from books/centaur/gl/gobjectp.lisp:
;; `(:g-ite (:g-boolean . ,(qv 0))
;;          (:g-ite (:g-boolean . ,(qv 1))
;;                  ACL2::ABC . COMMON-LISP::ABC)
;;          (:g-ite (:g-boolean . ,(qv 1))
;;                  ACL2::ACD . COMMON-LISP::ACD))
  :g-bindings '((sport ((player-count . (:g-ite (:g-boolean . 0)
                                               :zero
                                               (:g-ite (:g-boolean . 1)
                                                       :one
                                                       .
                                                       :two)))
                        (ball . (:g-number (2 3 4)))))))