#lang scheme

(require "Gramatica-Lpo.rkt")

;;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~n" 
;            (integer->char 8802) "x")
;    (printf "~nSon variables individuales: ~a.~n"
;            (list '?x '?y '?z '?x1 '?y1 '?z1 '?X '?Y '?Z '?X1 '?Y1 '?Z1))
    (printf "~nLos predicados son símbolos.~n")
    (printf "Las constantes individuales son símbolos o números.~n")
    (printf "Las variables individuales son símbolos cuyo primer signo es una mayúscula.~n")
    (printf "~nCada expresión elemental se ha de escribir según el esquema siguiente:~n (predicado term-individual-1 ... term-individual-n)~n")
    (printf "~nCada expresión compuesta ha de escribirse entre paréntesis con notación prefija.~n")
    (printf "~nPor ejemplo: en lugar de escribir ~a(padre luis pedro) se escribirá (n (padre luis pedro)).~n" (integer->char 172))
    (printf "O, en lugar de escribir (padre luis pedro)~a(padre pedro juan), se escribirá (y (padre luis pedro) (padre pedro juan)).~n" 
            (integer->char 8743))
    (printf "Por tanto, ~a((padre luis pedro)~a(padre pedro juan)) se escribirá (n (y (padre luis pedro) (padre pedro juan))).~n~n" 
            (integer->char 172) (integer->char 8743))
    ))
(define mensaje2
  (lambda ()
    (printf "La expresión escrita no es correcta~n")
    ))
(define print-respuesta
  (lambda (lista)
    (if (null? lista)
        (newline)
        (begin
          (printf "~a~n" (first lista))
          (print-respuesta (rest lista)))
        ) ))
;;lectura de fórmulas
(define lectura-una-expresion
  (lambda ()
    ;(mensaje1)
    (let go ((s-expr (read))
             )
      (if (symbol? s-expr)
          'fin
          (if (ebf? s-expr)
              s-expr
              (begin
                (mensaje2)
                (go (read)))
              )
          )
      )
    ))
;;Instanciando
(define instanciar
  (lambda (query frame)
    (letrec ((respuesta #f)
             (instancias
              (lambda (frame)
                (if (null? frame)
                    frame
                    (if (first frame)
                        (cons
                         (instancia query (first frame))
                         (instancias (rest frame)))
                        (instancias (rest frame)))
                    )))
             (instancia 
              (lambda (preg sustitucion)
                (letrec
                    ((aux
                      (lambda (p s)
                        (cond ((variable? p)
                               (let ((par-sust (assoc p s)) )
                                 (if par-sust
                                     (instancia (cdr par-sust) s)
                                     p)
                                 ) )
                              ((pair? p)
                               (cons
                                (instancia (car p) s) 
                                (instancia (cdr p) s)))
                              (else p)
                              ) ))
                     )
                  (cond
                    ((eq? sustitucion 'fallo) 'falso);sustituir fallo por 'falso
                    ((null? sustitucion) preg);sustituir '() por 'verdadero
                    (else (aux preg sustitucion)))
                  ) ))
             )
      (set! respuesta (instancias frame))
      respuesta
      ) ))
(provide mensaje1 mensaje2 lectura-una-expresion instanciar print-respuesta)

