#lang scheme

;;Lectura y comprobación de expresiones
(define S (list 'p 'q 'r 's 'w 'z 
                'p1 'q1 'r1 's1 'w1 'z1 
                'p2 'q2 'r2 's2 'w2 'z2))
(define BIN (list 'y 'o 'c 'b 'x));x= xor
;;definición b=((Y c Z) y (Z c Y))
;;definición x=(n (Y b Z))
;;;;GRAMÁTICA
;;predicados de tipo y subtipos
(define ebf?
  (lambda (formula)
    (cond
      ((atomica? formula) #t)
      ((neg? formula)
       (ebf? (second formula)))
      ((bin? formula)
       (and;conj
        (ebf? (first formula))
        (ebf? (third formula))))
      (else #f)
      )
    ))
(define atomica?
  (lambda (f)
    (if (symbol? f)
        (if (member f S) #t #f)
        #f)
    ))
;;Expresión compuesta: una lista
(define compuesta?
  (lambda (expr)
    (if (list? expr)
        (or (= (length expr) 2) (= (length expr) 3))
        #f) ))
;;
(define neg?
  (lambda (expr)
    (if (compuesta? expr)
        (eq? (first expr) 'n)
        #f) ))

(define bin?
  (lambda (expr)
    (if (compuesta? expr)
        (if (member (second expr) BIN)
            #t
            #f)
        #f) ))
;;;Otros tipos
;; CONJUNCIÓN, DISYUNCIÓN, CONDICIONAL:
(define y?
  (lambda (expr)
    (if (compuesta? expr)
        (if (equal? (second expr) 'y)
            #t
            #f)
        #f) ))

(define o?
  (lambda (expr)
    (if (compuesta? expr)
        (if (equal? (second expr) 'o)
            #t
            #f)
        #f) ))

(define c?
  (lambda (expr)
    (if (compuesta? expr)
        (if (equal? (second expr) 'c)
            #t
            #f)
        #f) ))
(define b?
  (lambda (expr)
    (if (compuesta? expr)
        (if (equal? (second expr) 'b)
            #t
            #f)
        #f) ))
(define x?
  (lambda (expr)
    (if (compuesta? expr)
        (if (equal? (second expr) 'x)
            #t
            #f)
        #f) ))
;; Constructores
(define haz-no
  (lambda (a)
    (if (ebf? a)
        (list 'n a)
        (error "El argumento no es una ebf"))))
(define haz-bin
  (lambda (a b signo)
    (if (and (ebf? a) (ebf? b))
        (if (member signo BIN)
            (list a signo b)
            (error 
             "No es un signo lógico binario:" signo))
        (error "Los argumentos han de ser eebbff"))))
;; Extractores 
(define subf-neg second)

(define subf-iz first)

(define subf-dc third)
;; SECUENTES

;;Necesitaremos, como con las ebf, un predicado de tipo. Escribiremos, pues, un predicado de tipo que devuelva #T cuando su argumento sea un dato del tipo SECUENTE. 

;; Definiremos, antes, un predicado auxiliar "ebf-lista?" de un sólo argumento que devolverá falso sii algún elemento de la lista no es una ebf.
(define lista-de-ebf?
  (lambda (lst)
    (if (list? lst)
        (cond 
          ((null? lst) #t)
          (else
           (and 
            (ebf? (car lst))
            (lista-de-ebf? (cdr lst)) ) ) )
        #f) ))

;; Ahora el predicado de tipo "secuente?"
(define secuente?
  (lambda (lst)
    (and
     (list? lst)
     (= (length lst) 2)
     (lista-de-ebf? (lis lst))
     (lista-de-ebf? (lds lst)) )))

;;CONSTRUCTORES
;;Se entiende por procedimiento constructor aquel que devuelve un dato perteneciente a un tipo de datos, en nuestro caso secuentes.
;;Lado izquierdo del secuente o LIS:
(define haz-lis!
    (lambda (lst)
      (if (or
           (lista-de-ebf? lst) 
           (and (null? (car lst)) 
                (null? (cdr lst))))
          (remove-duplicates lst) 
          #f)))
;;Lado derecho del secuente o lds:
(define haz-lds!
    (lambda (lst)
      (if (or
           (lista-de-ebf? lst) 
           (and (null? (car lst)) 
                (null? (cdr lst))))
          (remove-duplicates lst) 
          #f)))
;;HAZ-SECUENTE ARG1 ARG2
(define haz-secuente!
  (lambda (lis lds)
    (list lis lds)))
;; EXTRACTORES
(define lis car)

(define lds cadr)
;; Axioma? expresa una de las condiciones de parada. La rama está por tanto cerrada
(define axioma?
  (lambda (a b)
    (cond
      ((null? a) #f)
      ((null? b) #f)
      ((member (car a) b) #t)
      (else
       (axioma? (cdr a) b))) ))

;; Otra condición de parada es que el secuente en el nudo terminal no sea transformable
(define no-transformable?
  (lambda (sec)
    (and
     (andmap atomica? (lis sec))
     (andmap atomica? (lds sec))) ))
;
(define no-trans-aux
  (lambda (lst)
    (cond
      ((null? lst) #t)
      ((atomica? (car lst))
       (no-trans-aux (cdr lst)))
      (else #f) ) ))

;;Reglas del cálculo como procedimientos
(define hay-una-form?
  (lambda (lado proc)
    (ormap
     (lambda (form)
       (if (proc form)
           form
           #f))
     lado) ))
;reglas alfa
(define neg-en-lis
  (lambda (sec)
    (let ((form (hay-una-form? (lis sec) neg?))
          (regla 'RNlis)
          )
      (if form
          (list
           regla
           (haz-secuente!
            (remove form (lis sec))
            (append (lds sec) (list (subf-neg form))) ))
          #f)
          )
      ) )
(define neg-en-lds
  (lambda (sec)
    (let ((form (hay-una-form? (lds sec) neg?)) 
          (regla 'RNlds)
          )
      (if form
          (list
           regla
           (haz-secuente!
            (append (lis sec) (list (subf-neg form))) 
            (remove form (lds sec))
           ))
          #f)
      ) ))
(define o-en-lds
  (lambda (sec)
    (let ((form (hay-una-form? (lds sec) o?)) 
          (regla 'ROlds)
          )
      (if form
          (list 
           regla
           (haz-secuente!
            (lis sec)
            (append 
             (remove form (lds sec))
             (list (subf-iz form))
             (list (subf-dc form)))
            ))
          #f)
      ) ))
(define y-en-lis
  (lambda (sec)
    (let ((form (hay-una-form? (lis sec) y?)) 
          (regla 'RYlis)
          )
      (if form
          (list
           regla
           (haz-secuente!
            (append 
             (remove form (lis sec))
             (list (subf-iz form))
             (list (subf-dc form)))
            (lds sec)
            ))
          #f)
      ) ))
(define c-en-lds
  (lambda (sec)
    (let ((form (hay-una-form? (lds sec) c?)) 
          (regla 'RClds)
          )
      (if form
          (list
           regla
           (haz-secuente!
            (append
             (lis sec)
             (list (subf-iz form)))
            (append 
             (remove form (lds sec))
             (list (subf-dc form)))
            ))
          #f)
      ) ))
;;reglas beta
(define o-en-lis
  (lambda (sec)
    (let ((form (hay-una-form? (lis sec) o?)) 
          (regla 'ROlis)
          )
      (if form
          (list
           regla
           (list
            (haz-secuente!
             (append 
              (remove form (lis sec)) 
              (list (subf-iz form)))
             (lds sec))
            (haz-secuente!
             (append 
              (remove form (lis sec)) 
              (list (subf-dc form)))
             (lds sec))
            ))
          #f)
      ) ))
(define y-en-lds
  (lambda (sec)
    (let ((form (hay-una-form? (lds sec) y?)) 
          (regla 'RYlds)
          )
      (if form
          (list
           regla
           (list
            (haz-secuente!
             (lis sec)
             (append 
              (remove form (lds sec)) 
              (list (subf-iz form))) )
            (haz-secuente!
             (lis sec)
             (append 
              (remove form (lds sec)) 
              (list (subf-dc form))) )
            ))
          #f)
      ) ))
(define c-en-lis
  (lambda (sec)
    (let ((form (hay-una-form? (lis sec) c?)) 
          (regla 'RClis)
          )
      (if form
          (list
           regla
           (list
            (haz-secuente!
             (remove form (lis sec)) 
             (append 
              (lds sec) 
              (list (subf-iz form))) )
            (haz-secuente!
             (append 
              (remove form (lis sec)) 
              (list (subf-dc form)))
             (lds sec))
            ))
          #f)
      ) ))
;;
(define reglas-alfa (list neg-en-lis neg-en-lds o-en-lds y-en-lis c-en-lds))
(define reglas-beta (list o-en-lis y-en-lds c-en-lis))
;;El procedimiento de transformación
(define transforma
  (lambda (sec x regla)
    (let ((Lis (lis sec))
          (Lds (lds sec))
          )
      (if (= x 1)
          (printf "~n ~a ~a ~a ~a ~a "
                  x Lis (integer->char 8658) Lds regla)
          (printf "~n ~a ~a ~a ~a por ~a en ~a. " 
                  x Lis (integer->char 8658) Lds regla (sub1 x)))
    (cond
      ((axioma? Lis Lds) (printf "Rama cerrada por Esquema-Axioma en ~a~n" x) #t)
      ((no-transformable? sec) (printf "Rama acabada y no cerrada en ~a~n" x) #f)
      (else
       (let* ((lista (ormap (lambda (proc) (proc sec)) reglas-alfa))
              (regla (if lista (first lista) #f))
              (new-sec (if lista (second lista) #f))
              )
         (if new-sec
             (list (transforma new-sec (add1 x) regla))
             (begin
               (set! lista (ormap (lambda (proc) (proc sec)) reglas-beta))
               (set! regla (first lista))
               (set! new-sec (second lista))
               (list
                (transforma (first new-sec) (add1 x) regla)
                (transforma (second new-sec) (add1 x) regla)
                )
             )
         )
       )
      )
      )
    )))
;;;;INTERFAZ
;;lectura de fórmulas
(define lectura-una-formula
  (lambda ()
    (let ((formula (read))
          )
      (if (equal? formula 'fin)
          'fin
          (if (ebf? formula)
              formula
              #f))
      )
    ))
(define lectura-formulas
  (lambda ()
    (mensaje1)
    (let go ((expr (lectura-una-formula))
             (todas '()))
      (cond
        ((equal? expr 'fin) todas)
        ((not expr)
         (mensaje2)
         (go (lectura-una-formula) todas) )
        (else
         (go (lectura-una-formula) (cons expr todas)))
        ))
    ))
;;Los mensajes de la interfaz
(define mensaje1
  (lambda ()
    (printf "La conectiva ~a se escribe como: ~a.~n" 
            (integer->char 172) "n")
    (printf "La conectiva ~a se escribe como: ~a.~n" 
            (integer->char 8744) "o")
    (printf "La conectiva ~a se escribe como: ~a.~n" 
            (integer->char 8743) "y")
    (printf "La conectiva ~a se escribe como: ~a.~n" 
            (integer->char 10230) "c")
    (printf "La conectiva ~a se escribe como: ~a.~n" 
            (integer->char 10231) "b")
    (printf "La conectiva ~a se escribe como: ~a.~n" 
            (integer->char 8802) "x")
    (printf "Cada expresión compuesta ha de escribirse entre paréntesis.~n")
    (printf "Por ejemplo: en lugar de escribir ~ap se escribirá (n p).~n" (integer->char 172))
    (printf "O, en lugar de escribir p~aq, se escribirá (p c q).~n" (integer->char 10230))
    (printf "Por tanto, ~a(p~aq) se escribirá (n (p b q)).~n" 
            (integer->char 172) (integer->char 10231))
    (printf "~nEscribe, una a una, cada premisa y la conclusión.~n")
    (printf "Escribe: ~a, para acabar.~n" "'fin'")
    ))
(define mensaje2
  (lambda ()
    (printf "La fórmula escrita no es correcta~n")
    ))
;;El driver
(define deduce
  (lambda ()
    (let* ((input-lst (lectura-formulas))
           (long (length input-lst))
           (lista-ebfs (lista-de-ebf? input-lst))
           (lis (haz-lis! (reverse (rest input-lst))))
           (lds (haz-lds! (list (first input-lst))))
           (deduccion (transforma (haz-secuente! lis lds) 1 ""))
           (validez (andmap (lambda (b) b) (flatten deduccion)))
           )
      (if validez
          (printf "~nSecuente válido en 1.~n")
          (printf "~nSecuente no válido en 1.~n"))
      ) ))
(deduce)