#lang scheme

;;; SILOGÍSTICA
;;; Notación
(define conceptos '(#\A #\B #\C #\D #\E #\F #\G #\H #\I #\J #\K #\L #\M #\N #\O #\P #\Q #\R #\S #\T #\U #\V #\W #\X #\Y #\Z))

(define ids '(#\a #\e #\i #\o))

(define es-falso #\¬)
;;Gramática de expresiones mediante Predicados de tipo
;;Extractores y convertidores
(define es-falso!
  (lambda (s)
    (string-append
     (string es-falso #\()
     s
     (string #\)) ) ))
(define afirmativa!
  (lambda (s)
    (substring s 2 5) ))
(define suj
  (lambda (expr)
    (if (> (string-length expr) 3)
        (string-ref expr 3)
        (string-ref expr 1)) ))
(define pred
  (lambda (expr)
    (if (> (string-length expr) 3)
        (string-ref expr 4)
        (string-ref expr 2)) ))
;;Un enunciado categórico ha de escribirse así: identificador_subtipo Sujeto Predicado
;;Una expresión del tipo es falso que:
(define es-falso?
  (lambda (prop)
    (if (= (string-length prop) 6)
        (if (char=? (string-ref prop 0) es-falso)
            #t
            #f)
        #f) ))
;;Predicado del tipo proposición categórica
(define categorica?
  (lambda (string)
    (if (es-falso? string)
        (categorica? (afirmativa! string))
        (if (= (string-length string) 3)
            (let ((id (string-ref string 0))
                  (sujeto (suj string))
                  (predicado (pred string))
                  )
              (if
               (and
                (member id ids)
                (member sujeto conceptos)
                (member predicado conceptos))
               #t
               #f))
            #f)
        ) ))
;;Subtipos según cantidad y cualidad
(define universal?
  (lambda (string)
    (let ((id (string-ref string 0)) )
      (or (char=? id #\a) (char=? id #\e))
      ) ))
(define particular?
  (lambda (string)
    (let ((id (string-ref string 0)) )
      (or (char=? id #\i) (char=? id #\o))
      ) ))
(define afirmativa?
  (lambda (string)
    (let ((id (string-ref string 0)) )
      (or (char=? id #\a) (char=? id #\i))
      ) ))
(define negativa?
  (lambda (string)
    (let ((id (string-ref string 0)) )
      (or (char=? id #\e) (char=? id #\o))
      ) ))
;;;Reglas de transformación
;;Básicas: leyes del silogismo. Argumento un par de dos categóricas
(define regla-barbara
  (lambda (par)
    (let ((p1 (car par))
          (p2 (cdr par))
          )
    (string #\a (suj p2) (pred p1)) )))
(define regla-celarent
  (lambda (par)
    (let ((p1 (car par))
          (p2 (cdr par))
          )
    (string #\e (suj p2) (pred p1)) )))
(define regla-darii
  (lambda (par)
    (let ((p1 (car par))
          (p2 (cdr par))
          )
    (string #\i (suj p2) (pred p1)) )))
(define regla-ferio
  (lambda (par)
    (let ((p1 (car par))
          (p2 (cdr par))
          )
    (string #\o (suj p2) (pred p1)) )))
;;predicados de reconocimiento para aplicación de leyes del silogismo
(define es-posible-barbara?
  (lambda (prop1 prop2)
    (let ((universal-afirmativa? (lambda (s) (and (universal? s) (afirmativa? s))))
          (suj1 (suj prop1))
          (pred1 (pred prop1))
          (suj2 (suj prop2))
          (pred2 (pred prop2))
          )
      (if (and (universal-afirmativa? prop1) (universal-afirmativa? prop2))
          (if (char=? suj1 pred2)
              #t
              #f)
          #f)
      ) ))
(define es-posible-celarent?
  (lambda (prop1 prop2)
    (let ((universal-afirmativa? (lambda (s) (and (universal? s) (afirmativa? s))))
          (universal-negativa? (lambda (s) (and (universal? s) (negativa? s))))
          (suj1 (suj prop1))
          (pred1 (pred prop1))
          (suj2 (suj prop2))
          (pred2 (pred prop2))
          )
      (if (or
           (and (universal-negativa? prop1) (universal-afirmativa? prop2))
           (and (universal-negativa? prop2) (universal-afirmativa? prop1))
           )
          (if (char=? suj1 pred2)
              #t
              #f)
          #f)
      ) ))
(define es-posible-darii?
  (lambda (prop1 prop2)
    (let ((universal-afirmativa? (lambda (s) (and (universal? s) (afirmativa? s))))
          (particular-afirmativa? (lambda (s) (and (particular? s) (afirmativa? s))))
          (suj1 (suj prop1))
          (pred1 (pred prop1))
          (suj2 (suj prop2))
          (pred2 (pred prop2))
          )
      (if (or
           (and (universal-afirmativa? prop1) (particular-afirmativa? prop2))
           (and (particular-afirmativa? prop1) (universal-afirmativa? prop2))
           )
          (if (char=? suj1 pred2)
              #t
              #f)
          #f)
      ) ))
(define es-posible-ferio?
  (lambda (prop1 prop2)
    (let ((universal-negativa? (lambda (s) (and (universal? s) (negativa? s))))
          (particular-afirmativa? (lambda (s) (and (particular? s) (afirmativa? s))))
          (suj1 (suj prop1))
          (pred1 (pred prop1))
          (suj2 (suj prop2))
          (pred2 (pred prop2))
          )
      (if (or
           (and (universal-negativa? prop1) (particular-afirmativa? prop2))
           (and (particular-afirmativa? prop1) (universal-negativa? prop2))
           )
          (if (char=? suj1 pred2)
              #t
              #f)
          #f)
      ) ))
;;De las contradictorias
;;Las que se aplican a hipótesis de reducción al absurdo
(define es-falso-a->o
  (lambda (expr)
    (string-append (string #\o) (substring (afirmativa! expr) 1)) ))
(define es-falso-e->i
  (lambda (expr)
    (string-append (string #\i) (substring (afirmativa! expr) 1)) ))
(define es-falso-o->a
  (lambda (expr)
    (string-append (string #\a) (substring (afirmativa! expr) 1)) ))
(define es-falso-i->e
  (lambda (expr)
    (string-append (string #\e) (substring (afirmativa! expr) 1)) ))
;;Predicados de reconocimiento de las expresiones es-falso que...
(define es-falso-a?
  (lambda (s)
    (and
     (es-falso? s)
     (universal? (afirmativa! s))
     (afirmativa? (afirmativa! s))
     ) ))
(define es-falso-e?
  (lambda (s)
    (and
     (es-falso? s)
     (universal? (afirmativa! s))
     (negativa? (afirmativa! s))
     ) ))
(define es-falso-i?
  (lambda (s)
    (and
     (es-falso? s)
     (particular? (afirmativa! s))
     (afirmativa? (afirmativa! s))
     ) ))
(define es-falso-o?
  (lambda (s)
    (and
     (es-falso? s)
     (particular? (afirmativa! s))
     (negativa? (afirmativa! s))
     ) ))
;;Subalternancia
(define a->i
  (lambda (expr)
    (string-append (string #\i) (substring expr 1)) ))
(define e->o
  (lambda (expr)
    (string-append (string #\o) (substring expr 1)) ))
;;Predicados de reconocimiento de la subalternancia
(define a?
  (lambda (s)
    (and (universal? s) (afirmativa? s))
    ))
(define e?
  (lambda (s)
    (and (universal? s) (negativa? s))
    ))
;;Conversión simple en general
(define X->Y
  (lambda (expr)
    (let ((id (string-ref expr 0))
          (suj (string-ref expr 1))
          (pred (string-ref expr 2))
          )
      (string id pred suj) )))
;;Predicado de reconocimiento de conversión
(define conversion?
  (lambda (s)
    (or
     (and (universal? s) (negativa? s))
     (and (particular? s) (afirmativa? s)))
    ))
;;Reglas aplicables a una proposición
(define reglas-aplicables-una-proposicion
  (lambda (s)
    (let ((respuesta '()) )
      (when (es-falso-a? s) 
        (set! respuesta
              (cons 
               (proc-sobre-prop es-falso-a->o s) respuesta)))
      (when (es-falso-e? s) 
        (set! respuesta
              (cons 
               (proc-sobre-prop es-falso-e->i s) respuesta)))
      (when (es-falso-i? s)
        (set! respuesta
              (cons 
               (proc-sobre-prop es-falso-i->e s) respuesta)))
      (when (es-falso-o? s)
        (set! respuesta 
              (cons 
               (proc-sobre-prop es-falso-o->a s) respuesta)))
      (when (a? s)
        (set! respuesta
              (cons 
               (proc-sobre-prop a->i s) respuesta)))
      (when (e? s)
        (set! respuesta
              (cons 
               (proc-sobre-prop e->o s) respuesta)))
      (when (conversion? s)
        (set! respuesta
              (cons 
               (proc-sobre-prop X->Y s) respuesta)))
      (reverse respuesta)
      ) ))
;;Reglas aplicables a dos proposiciones
;;Procedimiento auxiliar que construye un par con proc y proposicion(es)
(define proc-sobre-prop
  (lambda (proc p1 . p2)
    (if (null? p2)
        (cons proc p1)
        (cons proc (cons p1 (car p2)))
        ) ))
(define reglas-aplicables-dos-proposiciones
  (lambda (s1 s2)
    (let ((respuesta '()))
      (when (es-posible-barbara? s1 s2)
        (set! respuesta
              (cons 
               (proc-sobre-prop regla-barbara s1 s2) respuesta)))
      (when (es-posible-celarent? s1 s2)
        (set! respuesta
              (cons 
               (proc-sobre-prop regla-celarent s1 s2) respuesta)))
      (when (es-posible-darii? s1 s2)
        (set! respuesta
              (cons 
               (proc-sobre-prop regla-darii s1 s2) respuesta)))
      (when (es-posible-ferio? s1 s2)
        (set! respuesta
              (cons 
               (proc-sobre-prop regla-ferio s1 s2) respuesta)))
      (reverse respuesta)
      ) ))
;;Dada una deduccion, se pueden aplicar las reglas
;;Sobre una proposición
(define reglas-de-una-aplicables-deduccion
  (lambda (lista-prop)
    (if (null? lista-prop)
        '()
        (append
         (reglas-aplicables-una-proposicion (car lista-prop))
         (reglas-de-una-aplicables-deduccion (cdr lista-prop)))
        ) ))
;;Sobre dos proposiciones
(define reglas-de-dos-aplicables-deduccion
  (lambda (lista-prop)
    (letrec
        ((una-todas
          (lambda (primera resto)
            (if (null? resto)
                '()
                (append
                 (reglas-aplicables-dos-proposiciones primera (car resto))
                 (una-todas primera (cdr resto)))
                ) ))
         (todas-con-todas
          (lambda (lst)
            (if (null? lst)
                '()
                (append
                 (una-todas (car lst) (remove (car lst) lista-prop))
                 (todas-con-todas (cdr lst)))
                ) ))
         )
      (todas-con-todas lista-prop)
      ) ))
;;Reglas aplicables
(define reglas-aplicables-deduccion
  (lambda (deduccion)
    (append
     (reglas-de-dos-aplicables-deduccion deduccion)
     (reglas-de-una-aplicables-deduccion deduccion))
    ))
;;Son contradictorias
(define contradictorias?
  (lambda (s1 s2)
    (let ((universal-afirmativa? (lambda (s) (and (universal? s) (afirmativa? s))))
          (universal-negativa? (lambda (s) (and (universal? s) (negativa? s))))
          (particular-afirmativa? (lambda (s) (and (particular? s) (afirmativa? s))))
          (particular-negativa? (lambda (s) (and (particular? s) (negativa? s))))
          (suj_s1 (suj s1))
          (pred_s1 (pred s1))
          (suj_s2 (suj s2))
          (pred_s2 (pred s2))
          )
      (cond
        ((and (universal-afirmativa? s1) (particular-negativa? s2))
         (and (char=? suj_s1 suj_s2) (char=? pred_s1 pred_s2)) )
        ((and (universal-afirmativa? s2) (particular-negativa? s1))
         (and (char=? suj_s1 suj_s2) (char=? pred_s1 pred_s2)) )
        ((and (universal-negativa? s1) (particular-afirmativa? s2))
         (and (char=? suj_s1 suj_s2) (char=? pred_s1 pred_s2)) )
        ((and (universal-negativa? s2) (particular-afirmativa? s1))
         (and (char=? suj_s1 suj_s2) (char=? pred_s1 pred_s2)) )
        ((es-falso? s1) 
         (string=? (afirmativa! s1) s2))
        ((es-falso? s2)
         (string=? s1 (afirmativa! s2)))
        (else #f)
        )
      ) ))
;;Para comprobar si existe una contradiccion en la deduccion
(define hay-contradiccion?
  (lambda (deduccion)
    (letrec ((una-todas
              (lambda (primera resto)
                (if (null? resto)
                    '()
                    (if (contradictorias? primera (car resto))
                        (append
                         (list (cons primera (car resto)))
                         (una-todas primera (cdr resto)))
                        (una-todas primera (cdr resto)))
                    ) ))
             (todas-con-todas
              (lambda (lst)
                (if (null? lst)
                    '()
                    (append
                     (una-todas (car lst) (remove (car lst) deduccion))
                     (todas-con-todas (cdr lst)))
                    ) ))
             (r (todas-con-todas deduccion))
             )
;      (printf "~a~n" r)
      (if (null? r)
          #f
          r)
;      (todas-con-todas deduccion)
      ) ))
;;;
(define print-deduccion
  (lambda (id d r)
    (printf "~a::~n" id)
    (printf "~a premisa 1~n" (first d))
    (printf "~a premisa 2~n" (second d))
    (printf "~a hipótesis reducción al absurdo~n" (third d))
    (let go ((ded (cdddr d))
             (reg r)
             )
      (if (null? reg)
          (let go ((rest-ded ded))
            (if (null? rest-ded)
                (newline)
                (begin
                  (printf "~a~n" (first rest-ded))
                  (go (rest rest-ded)))
                ))
          (begin
            (printf "~a por ~a~n" (first ded) (first reg))
            (go (rest ded) (rest reg)))
          )
      )
    ))
;;;
(define inicia-deduccion
  (lambda (modo)
    (reverse
     (list (first modo) (second modo) (es-falso! (third modo)))) ))

(define deducir
  (lambda (modo id)
    (let go ((deduccion (inicia-deduccion modo))
             )
      (if (hay-contradiccion? deduccion)
          (let*-values ([(d1 r1) 
                         (values
                          (cons
                           (third modo)
                           (cons 
                            (car (hay-contradiccion? deduccion)) deduccion))
                          reglas-aplicadas)]
                        [(d) (reverse d1)]
                        [(r) (reverse r1)]
                        )
          (print-deduccion id d r)
           )
          (begin
            ;(printf "~a ~n" deduccion)
            ;(read-line)
            (go (deduce deduccion)))
          )
      )
    ))

(define paso-deductivo
  (lambda (regla-expr)
    ((car regla-expr) (cdr regla-expr)) ))

(define reglas-aplicadas '())

(define deduce
  (lambda (deduccion)
    (let* ((reglas-aplicables 
            (remove-aplicadas 
             (reglas-aplicables-deduccion deduccion) 
             reglas-aplicadas))
           (regla-expr (car reglas-aplicables))
           (un-paso (paso-deductivo regla-expr))
           )
      (set! reglas-aplicadas (cons regla-expr reglas-aplicadas))
      (cons un-paso deduccion))
    ))
(define remove-aplicadas
  (lambda (aplicables aplicadas)
    (let go ((remover (filter-map 
                       (lambda (x) 
                         (if (assoc (car x) aplicables)
                             x
                             #f))
                       aplicadas))
             (aplicable aplicables)
             )
      (if (null? remover)
          aplicable
          (go (rest remover) (remove (first remover) aplicable))
          )
      )
    ))

;;;
(provide reglas-aplicables-deduccion inicia-deduccion contradictorias? hay-contradiccion?)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 1ª Figura, modos válidos
(define barbara '("aMP" "aSM" "aSP"))
(define celarent '("eMP" "aSM" "eSP"))
(define darii '("aMP" "iSM" "iSP"))
(define ferio '("eMP" "iSM" "oSP"))
(define subalterna-1-AAI '("aMP" "aSM" "iSP"))
(define subalterna-1-EAO '("eMP" "aSM" "oSP"))
; 2ª Figura, modos válidos
(define cesare '("ePM" "aSM" "eSP"))
(define camestre '("aPM" "eSM" "eSP"))
(define festino '("ePM" "iSM" "oSP"))
(define baroco '("aPM" "oSM" "oSP"))
(define subalterna-2-AEO '("aPM" "eSM" "oSP"))
(define subalterna-2-EAO '("ePM" "aSM" "oSP"))
;; 3ª Figura, modos válidos
(define darapti '("aMP" "aMS" "iSP"))
(define disamis '("iMP" "aMS" "iSP"))
(define datisi '("aMP" "iMS" "iSP"))
(define bocardo '("oMP" "aMS" "oSP"))
(define ferison '("eMP" "iMS" "oSP"))
(define felapton '("eMP" "aMS" "oSP"))
;; 4ª Figura, galénica, modos válidos
(define bramantip '("aPM" "aMS" "iSP"))
(define camenes '("aPM" "eMS" "eSP"))
(define dimaris '("iPM" "aMS" "iSP"))
(define fesapo '("ePM" "aMS" "oSP"))
(define fresison '("ePM" "iMS" "oSP"));
(define subalterna-4-AEO '("aPM" "eMS" "oSP"))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(printf "Primera Figura: ~n")
(deducir barbara 'barbara)
(set! reglas-aplicadas '())
(deducir celarent 'celarent)
(set! reglas-aplicadas '())
(deducir darii 'darii)
(set! reglas-aplicadas '())
(deducir ferio 'ferio)
(set! reglas-aplicadas '())
(deducir subalterna-1-AAI 'subalterna-1-AAI)
(set! reglas-aplicadas '())
(deducir subalterna-1-EAO 'subalterna-1-EAO)
(set! reglas-aplicadas '())
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(printf "Segunda Figura: ~n")
(deducir cesare 'cesare)
(set! reglas-aplicadas '())
(deducir camestre 'camestre)
(set! reglas-aplicadas '())
(deducir festino 'festino)
(set! reglas-aplicadas '())
(deducir baroco 'baroco)
(set! reglas-aplicadas '())
(deducir subalterna-2-AEO 'subalterna-2-AEO)
(set! reglas-aplicadas '())
(deducir subalterna-2-EAO 'subalterna-2-EAO)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(printf "Tercera Figura: ~n")
(set! reglas-aplicadas '())
(deducir darapti 'darapti)
(set! reglas-aplicadas '())
(deducir disamis 'disamis)
(set! reglas-aplicadas '())
(deducir datisi 'datisi)
(set! reglas-aplicadas '())
(deducir bocardo 'bocardo)
(set! reglas-aplicadas '())
(deducir ferison 'ferison)
(set! reglas-aplicadas '())
(deducir felapton 'felapton)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(printf "Cuarta Figura: ~n")
(set! reglas-aplicadas '())
(deducir bramantip 'bramantip)
(set! reglas-aplicadas '())
(deducir camenes 'camenes)
(set! reglas-aplicadas '())
(deducir dimaris 'dimaris)
(set! reglas-aplicadas '())
(deducir fesapo 'fesapo)
(set! reglas-aplicadas '())
(deducir fresison 'fresison)
(set! reglas-aplicadas '())
(deducir subalterna-4-AEO 'subalterna-4-AEO)

