;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; An implementation of social choice functions as positional scoring
;; rules
;;
;; players range from 0 to ...
;; consequences range from 0 to ...
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; NOTE:
;; We assume a formula is accepted by the following BNF:
;;
;; F ::= (x) | (i (x x)) | (neg F) | (and F F ...) | (or F F ...) |
;;       (diamond i F) | (box i F) | (pospref i F) | (necpref i F)
;;
;; where x is a consequence, i is a player.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;; STRUCTURES
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; structure of social choice function
(defstruct scf
  players
  consequences
  scorerule)

;; structure of a model of social choice function
(defstruct model-scf
  scfunc
  prefprofile)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;; OUTCOME SCORING RULES 
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun outcome (scfunc profile)
  "Returns the outcome of the social choice function *scfunc* 
for the preference profile *profile*."
  (let (
	(scores (make-array (scf-consequences scfunc)
			    :initial-element 0))
	(best-score 0)
	(best-consequence NIL))
    (dolist (pref profile)
      (do* (
	    (i 0 (+ i 1))
	    (conseq (nth i pref)
		    (nth i pref)))
	   ((= i (scf-consequences scfunc)))
	   (let ((temp (+ (elt scores conseq)
			  (nth i (scf-scorerule scfunc)))))
	     (when (> temp best-score)
	       (setf best-score temp)
	       (setf best-consequence conseq))
	     (setf (elt scores conseq) temp))))
    best-consequence
    )
  )

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; AUXILIARY FUNCTIONS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun permutations (l)
  "Returns the list of permutations of the list *l* in parameter."
  (if (null l) '(())
    (mapcan #'(lambda (x)
		(mapcar #'(lambda (y) (cons x y))
			(permutations (remove x l :count 1)))) l)))


(defun list-of-preferences (consequences)
  "Returns the list of all the preferences over a number of
consequences *consequences*"
  (let ((pref '()))
    ;; we find one admissible preference
    (do ((i 0 (+ i 1)))
  	((= i consequences))
  	(setf pref (cons i pref)))
    ;; we return its permutations
    (permutations pref)))


(defun combine-preferences (preferences-list players)
  "Returns the list of all preference profiles for *players* and
*preferences-list*"
  (if (or (null preferences-list) (= players 0)) '(())
    (mapcan #'(lambda (x)
		(mapcar #'(lambda (y) (cons x y))
			(combine-preferences 
			 preferences-list (1- players))))
	    preferences-list)))


(defun list-of-profiles (players consequences)
  "Returns the list of all preference profiles over a number of
players *players* and consequences *consequences*"
  (combine-preferences (list-of-preferences consequences) players))
    

(defun substitute-pref (player pref profile)
  "Replaces *player*'s preference in the *profile* with *pref*."
  (cond ((and (< player (length profile))
	      (>= player 0))
	 (let ((new-profile '()))
	   (do ((j 0 (+ j 1)))
	       ((= j (length profile)) (nreverse new-profile))
	       (if (= j player)
		   (push pref new-profile) 
		 (push (nth j profile) new-profile)))))
	(t (error "Error substitute-pref: bad arguments."))))


(defun local-effectivity (player profile)
  "Returns the list of profiles for which the player is locally
effective at *profile*"
  (cond ((and (< player (length profile))
	      (>= player 0))
	 (let ((new-list '()))
	   (dolist (x (list-of-preferences (length (car profile))))
	     (push (substitute-pref player x profile) new-list))
	   new-list))
	(t (error "Error local-effectivity: bad arguments."))))


(defun in-profile-prefers (player profile x y)
  "In *profile*, *player* prefers *x* over *y*."
  (when (member y (member x (nth player profile)))
    t))


(defun truly-prefers (player mscf x y)
  "In the model *mscf*, *player* truly prefers *x* over *y*."
  (in-profile-prefers player (model-scf-prefprofile mscf) x y))


(defun preferred-profiles (player profile mscf)
  "Returns the list of profiles that *player* weakly truly prefers to
*profile* in *mscf*"
  (let ((current-outcome
	 (outcome (model-scf-scfunc mscf) profile)) (new-list '()))
    ;; for all possible profiles
    (dolist (x (list-of-profiles (length profile) (length (car profile)))) 
      (when (truly-prefers player mscf (outcome (model-scf-scfunc mscf) x)
			   current-outcome)
	(push x new-list))) 
    new-list))


(defun is-a-controlled-atom (formula)
  "*formula* is of the form: `(i (x y))', `i', `x' and `y' integers."
  (and (listp formula)
       (= (length formula) 2)
       (numberp (car formula))
       (listp (cadr formula))
       (= (length (cadr formula)) 2)
       (numberp (caadr formula))
       (numberp (cadr (cadr formula)))))


(defun is-a-consequence-atom (formula)
  "*formula* is of the form (x), *x* being an integer"
  (and (listp formula)
       (= (length formula) 1)
       (numberp (car formula))))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;; MODEL CHECKING
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun mc-exist-quant (formula mscfunc list-of-profiles)
  "*list-of-profiles*: a list of profiles against which to model check
the *formula*. Returns t only if *formula* holds in some profile"
  (if (eq list-of-profiles '())
      nil
    (or (model-check formula mscfunc (car list-of-profiles))
	(mc-exist-quant formula mscfunc (cdr list-of-profiles)))))


(defun mc-forall-quant (formula mscfunc list-of-profiles)
  "*list-of-profiles*: a list of profiles against which to model check
the *formula*. Returns t only if *formula* holds in every profile"
  (if (eq list-of-profiles '())
      t
    (and (model-check formula mscfunc (car list-of-profiles))
	 (mc-forall-quant formula mscfunc (cdr list-of-profiles)))))


(defun model-check (formula mscfunc profile)
  "Checks whether *formula* is true at *profile* of *mscfunc*."
  (cond
   ;; *formula* is a controlled atom [e.g. (0 (1 2))]
   ((is-a-controlled-atom formula)
    (in-profile-prefers (car formula) profile (caadr formula) 
			(cadr (cadr formula))))
   ;; *formula* is a consequence atom [e.g.: (3)]
   ((is-a-consequence-atom formula)
    (eq (car formula) (outcome (model-scf-scfunc mscfunc) profile)))
   ;; *formula* main operator is a negation [e.g.: (neg F)]
   ((eq (car formula) 'neg)
    (not (model-check (cadr formula) mscfunc profile)))
   ;; *formula* main operator is a conjunction 
   ;; [e.g.: (and (0) (2 (0 1)) (1 (2 1)))]
   ((eq (car formula) 'and)
    (and (model-check (cadr formula) mscfunc profile)
	 (if (not (eq (cddr formula) nil))
	     (model-check (cons 'and (cddr formula)) mscfunc profile)
	   t)))
   ;; *formula* main operator is a disjunction [e.g.: (or F1 F2 F3 F4)]
   ((eq (car formula) 'or)
    (or (model-check (cadr formula) mscfunc profile)
	(if (not (eq (cddr formula) nil))
	    (model-check (cons 'or (cddr formula)) mscfunc profile)
	  nil)))
   ;; *formula* main modality is a diamond [e.g.: (diamond 2 F)]
   ((eq (car formula) 'diamond)
    (mc-exist-quant (caddr formula) mscfunc
		    (local-effectivity (cadr formula) profile)))
   ;; *formula* main modality is a box [e.g.: (box 3 F)]
   ((eq (car formula) 'box)
    (mc-forall-quant (caddr formula) 
		     mscfunc 
		     (local-effectivity (cadr formula) profile)))
   ;; *formula* main modality is preference diamond [e.g.: (pospref 2 F)]
   ((eq (car formula) 'pospref)
    (mc-exist-quant (caddr formula) 
		    mscfunc 
		    (preferred-profiles (cadr formula) profile
					mscfunc)))
   ;; *formula* main modality is preference box [e.g.: (box 1 (2 (a b)))]
   ((eq (car formula) 'necpref)
    (mc-forall-quant (caddr formula) 
		     mscfunc 
		     (preferred-profiles (cadr formula) profile
					 mscfunc)))
   (t (error "Error model-check: formula ~S possibly malformed."
	     formula))))


(defun solve (formula mscfunc &optional verbose)
  "Returns all the preference profiles of *msfunc* that satisfy
*formula*. If the optional parameter *verbose* is set to *t*, the
function will print every state verifying *formula* on the fly."
  (let ((ok-states '()))
    (dolist (x (list-of-profiles 
		(scf-players (model-scf-scfunc mscfunc))
		(scf-consequences (model-scf-scfunc mscfunc))))
      (when (model-check formula mscfunc x)
	(when (eq verbose t)
	    (print x))
	(push x ok-states)))
    ok-states))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; GAME THEORY
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun construct-ne (conseq player)
  `(and (,conseq) 
	(box ,player (pospref ,player (,conseq)))))


(defun construct-player-ne (player consequences)
  (let ((my-list '())) 
    (do ((i 0 (+ i 1)))
	((= i consequences))
	(setf my-list (cons (construct-ne i player) my-list)))
    (setf my-list (cons 'or my-list))
    my-list))


(defun construct-player-dom (player players consequences)
  (let ((my-list (construct-player-ne player consequences)))
    (do ((i 0 (+ i 1)))
	((= i players))
	(unless (= i player) 
	  (setf my-list `(box ,i ,my-list))))
    my-list))
				    

(defun construct-equilibrium-ne (players consequences)
  (let ((my-list '()))
    (do ((i 0 (+ i 1)))
	((= i players))
	(setf my-list (cons (construct-player-ne i consequences)
			    my-list)))
    (setf my-list (cons 'and my-list)) my-list))


(defun construct-equilibrium-dom (players consequences)
  (let ((my-list '()))
    (do ((i 0 (+ i 1)))
	((= i players))
	(setf my-list (cons (construct-player-dom i players
			    consequences) my-list)))
    (setf my-list (cons 'and my-list)) my-list))


(defun init-gt (players consequences)
  "Instantiates solution concepts with *players* and *consequences*"
  (progn
    (defparameter ne (construct-equilibrium-ne players consequences))
    (defparameter dom (construct-equilibrium-dom players consequences)) 
    t))


(defun is-strategy-proof-rec (scf list-of-profiles)
  "Checks whether the models of scf made of *scf* and the first
  profile in *list-of-profiles* admits a dominance equilibrium at this
  very profile. Then it lauches the recursion on the list of other
  profiles in *list-of-profiles*."
  (if (eq list-of-profiles nil)
      t
    (and (model-check dom 
		      (make-model-scf :scfunc scf 
				      :prefprofile (car
						    list-of-profiles))
		      (car list-of-profiles))
	 (is-strategy-proof-rec scf (cdr list-of-profiles)))))


(defun is-strategy-proof (scf)
  "Check whether *scf* is strategy proof. It merely checks that for
every preference profile p, playing p is a dominance equilibirum."
  (init-gt (scf-players scf) (scf-consequences scf))
  (is-strategy-proof-rec scf (list-of-profiles (scf-players scf) 
					       (scf-consequences scf))))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;; TESTS
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; clisp
;; (load 'scf.lisp)
;; sbcl
;; (load "scf.lisp")

;; (init-gt 3 2)
;; (defvar scf32 (make-scf :players 3 :consequences 2 :scorerule '(1 0)))
;; (defvar profile32 '((0 1) (1 0) (0 1)))
;; (defvar mscf32 (make-model-scf :scfunc scf32 :prefprofile profile32))
;; (solve dom mscf32)
;; (is-strategy-proof scf32)

;; (init-gt 3 3)
;; (defvar scf33 (make-scf :players 3 :consequences 3 :scorerule '(2 1 0)))
;; (defvar profile33 '((2 0 1) (2 1 0) (0 1 2)))
;; (defvar mscf33 (make-model-scf :scfunc scf33 :prefprofile profile33))
;; (model-check ne mscf33 profile33)
;; (model-check dom mscf33 profile33)
;; (solve ne mscf33)
;; (solve `(and ,ne (1 (2 1))) mscf33)
;; (is-strategy-proof scf33)

;; (init-gt 3 4)
;; (defvar scf34 (make-scf :players 3 :consequences 4 :scorerule '(2 2 1 0)))
;; (defvar profile34 '((2 0 1 3) (2 3 1 0) (3 0 1 2)))
;; (defvar mscf34 (make-model-scf :scfunc scf34 :prefprofile profile34))
;; (model-check ne mscf34 profile34)
;; (model-check dom mscf34 profile34)
;; (solve ne mscf34)
;; (is-strategy-proof scf34)

;; (defvar scf44 (make-scf :players 4 :consequences 4 :scorerule '(2 2 1 0)))
;; (defvar profile44 '((3 2 0 1) (2 0 1 3) (2 3 1 0) (3 0 1 2)))
;; (defvar mscf44 (make-model-scf :scfunc scf44 :prefprofile profile44))
;; (init-gt 4 4)
;; (model-check ne mscf44 profile44)
;; (model-check dom mscf44 profile44)
;; (solve ne mscf44)
;; (is-strategy-proof scf44)