#lang scheme

;;ejercicios
(define ej1 '( ((p y q) c r) (r c s) ((p y q) c s) ))
(define ej2 '( ((p c q) y (r c s)) (p o s) ((q c r) y (s c w)) (r o w) ))
(define ej3 '( (p c (n q)) (r c q) (n (p y r)) ))
;;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))
(define VV (list #t #f))
;;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)
    ))
(define neg?
  (lambda (f)
    (if (and (list? f) (= (length f) 2))
        (if (eq? (first f) 'n)
            #t
            #f)
        #f)
    ))
(define bin?
  (lambda (f)
    (if (and (list? f) (= (length f) 3))
        (if (member (second f) BIN) #t #f)
        #f)
    ))
;;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")
    ))
;;Formar expresión única
(define expresiones->una-expr
  (lambda (lista-expr)
    (let ((premisas (rest lista-expr))
          (conclusion (first lista-expr))
          )
      (if (and (list? conclusion) (null? premisas))
          conclusion
          (expresion-unica (reverse premisas) conclusion)
          )
      )
    ))
(define expresion-unica
  (lambda (lista-prem conclusion)
    (make-condicional
     (make-conjuncion lista-prem)
     conclusion)
    ))
(define make-conjuncion
  (lambda (lista-prem)
    (cond
      ((null? (rest lista-prem)) (first lista-prem))
      (else
       (list
        (first lista-prem)
        'y
        (make-conjuncion (rest lista-prem))))) ))
(define make-condicional
  (lambda (antecedente consecuente)
    (list
     antecedente
     'c
     consecuente) ))
;;Asignaciones elementales
;;ASIGNANDO crea la lista, de tamaño igual al número de variables proposicionales distintas,
;;de todas las posibles combinaciones distintas de valores de verdad 
(define asignando
  (lambda (lista-variables-prop)
    (let go ((x (sub1 (length lista-variables-prop)))
             (temp VV))
      (cond
        ((= x 0) temp)
        (else
         (go (sub1 x) (genera-asig temp))))
      ) ))
;;Cuando el número de variables proposicionales es 1, dos son las asignaciones posibles
;;En otro caso, cada combinación se hace a partir de una sub-combinación formada por
;;varias asignaciones. Al inicio, se cuenta con una lista de sub-combinaciones.
;;Por ejemplo, para (p q) se tendría al inicio: ((#t) (#f))
;;GENERA-ASIG
(define genera-asig
  (lambda (lista-subcombi)
    (append-map 
     (lambda (subcombi)
       (map
	(lambda (val-verdad)
          (if (list? subcombi)
              (append subcombi (list val-verdad))
              (list subcombi val-verdad))) 
        VV))
     lista-subcombi) ))
;;Una vez que se tiene una tabla con todas las combinaciones posibles, hay que formar los pares
;;variable-proposicional . valor-veritativo
(define make-asignaciones
  (lambda (vp comb-vv)
    (map
     (lambda (asig)
       (map cons vp asig))
     comb-vv)
    ))
;;Subfórmulas
(define subformulas
  (lambda (expr)
    (letrec ((subf
              (lambda (expr)
                (cond
                  ((atomica? expr) (list expr))
                  ((neg? expr)
                   (cons expr
                         (subf (second expr))))
                  ((bin? expr)
                   (cons expr
                         (append (subf (first expr))
                                 (subf (third expr)))))
                  )))
             )
      (remove-duplicates (subf expr))
      ) ))
(define son-atomicas
  (lambda (subform)
     (append-map 
      (lambda (s)
        (if (atomica? s) (list s) '())) 
      subform)
    ))
(define no-son-atomicas
  (lambda (subform)
    (append-map
     (lambda (form)
       (if (atomica? form)
           '()
           (list form)))
     subform)
    ))
;;
(define sustitucion
  (lambda (formula asignaciones)
    (cond
      ((atomica? formula)
       (vprop->boolean formula asignaciones))
      ((neg? formula)
       (list
        (first formula)
        (sustitucion (second formula) asignaciones)))
      ((bin? formula)
       (list
         (second formula)
         (sustitucion (first formula) asignaciones)
         (sustitucion (third formula) asignaciones)))
      (else error)
      )
    ))
(define vprop->boolean
  (lambda (signo asignaciones)
    (if (null? asignaciones)
        '()
        (if (eq? signo (car (first asignaciones)))
            (cdr (first asignaciones))
            (vprop->boolean signo (rest asignaciones))))
    ))
;; Operaciones lógicas
(define-syntax neg
  (syntax-rules ()
    [
     (neg formula)
     (not formula)
     ]
    ))
(define-syntax conj
  (syntax-rules ()
    [
     (conj form1 form2)
     (if form1
         (if form2
             #t
             #f)
         #f)
     ]
    ))
(define-syntax disy
  (syntax-rules ()
    [
     (disy form1 form2)
     (if form1
         #t
         (if form2
             #t
             #f)
         )
     ]
    ))
(define-syntax imp
  (syntax-rules ()
    [
     (imp form1 form2)
     (if form1
         (if form2
             #t
             #f)
         #t)
     ]
    ))
(define-syntax bicond
  (syntax-rules ()
    [
     (bicond form1 form2)
     (conj
      (imp form1 form2)
      (imp form2 form1))
     ]
    ))
(define-syntax xor
  (syntax-rules ()
    [
     (bicond form1 form2)
     (neg
      (bicond form1 form2))
     ]
    ))
;;Valoracion de una formula
(define valoracion-una-formula
  (lambda (formula)
    (if (boolean? formula)
        formula
        (case (first formula)
          ((n) (neg 
                (valoracion-una-formula (second formula))) )
          ((y) (conj 
                (valoracion-una-formula (second formula)) 
                (valoracion-una-formula (third formula))) )
          ((o) (disy
                (valoracion-una-formula (second formula)) 
                (valoracion-una-formula (third formula))) )
          ((c) (imp
                (valoracion-una-formula (second formula)) 
                (valoracion-una-formula (third formula))) )
          ((b) (bicond
                (valoracion-una-formula (second formula)) 
                (valoracion-una-formula (third formula))) )
          ((x) (xor
                (valoracion-una-formula (second formula)) 
                (valoracion-una-formula (third formula))) )
          )
        )
    ))
;;
(define interpretacion
  (lambda (subformula asignaciones)
    (printf "->~a: ~a ~n~n"
            subformula
            (valoracion-una-formula 
             (sustitucion subformula asignaciones)))
    ))
;;
(define tabla
  (lambda (lista-subformulas combinaciones-asig)
    (for-each
     (lambda (asignaciones)
       (printf "asignaciones: ~a:: ~n" asignaciones)
       (for-each
        (lambda (subformula)
          (interpretacion subformula asignaciones)
          )
        lista-subformulas))
     combinaciones-asig)
    ))
;;;;;;;;;;;;;;;;
(let* ((formulas (lectura-formulas))
       (expresion (expresiones->una-expr formulas))
       (subformulas (subformulas expresion))
       (sub-no-atomicas (no-son-atomicas subformulas))
       (sub-atomicas (son-atomicas subformulas))
       (lista-asignaciones 
        (make-asignaciones sub-atomicas 
                           (asignando sub-atomicas)))
       )
  (tabla sub-no-atomicas lista-asignaciones)
  )
