#lang scheme

;;TÉRMINOS
;;Términos individuales
(define constante?
  (lambda (sexpr)
    (and
     (not (variable? sexpr))
     (or (symbol? sexpr) (number? sexpr) (string? sexpr)) 
     ) ))
(define-syntax variable?
  (syntax-rules ()
    [(variable? sexpr)
     (let ((str 
            (if (symbol? sexpr) 
                (symbol->string sexpr) 
                sexpr))
           )
       (cond
         ((string? str) 
          (and (char>=? (string-ref str 0) #\A)
               (char<=? (string-ref str 0) #\Z)))
         (else #f)))
     ]
    ))
(define termino-ind?
  (lambda (sexpr)
    (or (constante? sexpr) (variable? sexpr)) ))
;;Términos predicativos
(define-syntax predicado?
  (syntax-rules ()
    [(predicado? sexpr)
     (and
      (not (variable? sexpr))
      (or (symbol? sexpr) (string? sexpr)))
     ]
    ))
;;Un término de cualquiera de los dos tipos básicos
(define-syntax termino?
  (syntax-rules ()
    [(termino? sexpr)
     (or 
      (predicado? sexpr) (termino-ind? sexpr))
     ]
    ))
;;EXPRESIONES BIEN FORMADAS
;;Expresión atómica: hecho o función proposicional
(define expr-atomica?
  (lambda (expr tipo);hecho/func-prop
    (letrec ((pred 
              (if (eq? tipo 'hecho) constante? termino-ind?))
             (term-individuales?
              (lambda (exp)
                (cond 
                  ((null? exp) #t)
                  ((pred (first exp))
                   (term-individuales? (rest exp)) )
                  (else #f)
                  ) ))
             )
      (and
       (list? expr)
       (predicado? (first expr))
       (term-individuales? (rest expr)))
      ) ))
;;Expresiones compuestas por conectivas
;;Expresión compuesta: una lista
(define compuesta?
  (lambda (expr)
    (if (list? expr)
        (or (= (length expr) 2) (= (length expr) 3))
        #f) ))
;;Tipos negación y binaria
(define neg?
  (lambda (f)
    (if (compuesta? f)
        (eq? (first f) 'n)
        #f) ))
(define bin?
  (lambda (expr)
    (let ((BIN (list 'y 'o))); 'c 'b 'x
      (if (compuesta? expr)
          (if (member (first expr) BIN)
              #t
              #f)
          #f) ) ))
;;Predicado que subsume los tipos inmediatamente anteriores: ebf?
(define ebf?
  (lambda (s-expr)
    (cond
      ((expr-atomica? s-expr 'func-prop) #t)
      ((neg? s-expr)
       (ebf? (second s-expr)))
      ((bin? s-expr)
       (and
        (ebf? (second s-expr))
        (ebf? (third s-expr))))
      (else #f)
      ) ))
(provide constante? variable? termino-ind? predicado? termino?
         expr-atomica? compuesta? neg? bin? ebf?)