Robots y modelos

Notas sobre pruebas, modelado y aventuras en Java y Android

Versión 1.186 de ACL2::Procesador

leave a comment »

Acabo de marcar en SVN y subir a la forja de Rediris la versión 1.186 de ACL2::Procesador. Aceptaron el artículo que enviamos mis antiguos directores de PFC y yo a ACL2 2009, así que es hora de darle un lavado de cara en algunos aspectos, aprovechando que estoy en vacaciones de Semana Santa😀.

Las principales novedades que trae esta versión son básicamente:

  • Organización de órdenes en categorías: muchas órdenes repetían el mismo código una y otra vez. Este era sobre todo el caso de las órdenes que no producen prácticamente ninguna salida específica, como DEFPKG, DEFABBREV o DEFMACRO. Ahora lo que se hace es agrupar estas órdenes en categorías, para que compartan el mismo código. Con eso podré añadir más rápidamente órdenes de ACL2 que no sean tan usadas. Las órdenes que necesitan código específico se siguen usando directamente (como DEFUN, DEFTHM o ENCAPSULATE). De hecho, el orden actual para una orden X cualquiera es:
  1. Se intenta cargar el módulo ACL2::Orden::X, y analizar la orden mediante una instancia la clase contenida en dicho módulo.
  2. Si no funciona, se prueban en un orden prefijado todas las categorías, y se usa la primera que funcione. Actualmente, hay dos: DefinitionCategory (para las órdenes DEFXXX que no necesitan código especial) y FallbackCategory. La segunda categoría lo acepta todo, e imprime la salida de ACL2 como una lista de párrafos y S-expresiones, junto con el resumen debidamente procesado, si lo tenía. Su utilidad es para no fallar estrepitosamente ante órdenes de ACL2 aún no implementadas o código Lisp arbitrario (ACL2 es un entorno Lisp, al fin y al cabo). De todas formas, ACL2::Procesador sigue dando fallos fatales cuando no entiende algo en la salida de una orden para la que tiene código específico (de lo contrario, las pruebas de regresión serían inútiles).
  • Revisión del algoritmo de análisis de un fichero .lisp: ahora el grafo de dependencias es más sencillo, descartando los antiguos nodos que incluían a los ficheros .acl2 que servían para establecer el estado inicial de ACL2 antes de certificar un libro. Esto se debe a que ahora, cuando se procesa un fichero X.lisp y se encuentra un fichero X.acl2 o cert.acl2 en el mismo directorio, se usan los contenidos del primero de esos ficheros en vez del propio fichero X.lisp. Es ACL2 el que lee X.lisp y lo interpreta. De todas formas, ACL2 de hecho vuelve a volcar las fórmulas de X.lisp en la salida del evento CERTIFY-BOOK. Este nuevo esquema es más fiable de entrada, y además ahora le añadimos un prólogo y un epílogo a cada fichero .lisp procesado para asegurarnos de que funcione en más implementaciones de Lisp.

Esta versión ha sido probada con ACL2 2.9.4 bajo CLisp 2.44.1 (paquete Ubuntu 1:2.44.1-4ubuntu2), ACL2 3.0.1 bajo CMUCL (paquete Debian cmucl, versión 19a-release-20040728-9), ACL2 3.1 bajo CLisp, ACL2 3.2.1 bajo GCL (paquete Debian gcl 2.6.7-45), ACL2 3.3 bajo GCL, y ACL2 3.4 bajo GCL. Con eso tengo cubiertas varias implementaciones de Lisp y varias versiones de ACL2.

Para la siguiente versión, lo que quiero hacer es cambiar el “analizador” Lisp que tengo (me da vergüenza llamarlo así :-D) por uno que implemente el algoritmo de la función read, tal y como viene en el libro  de “Common Lisp, the Language”, particularmente en las secciones 22.1 y 22.2. Tenía hecho una gramática LALR(1) tentativa en Parse::Eyapp (muy buen módulo para los fans de bison/flex o ANTLR) en una de mis ramas, pero va a ser que no: la sintaxis es demasiado compleja como para hacerla fácilmente:-/. Por ejemplo, ahora mismo el código no tiene forma de saber si algún trozo de código Lisp es una lista, un átomo, una cadena, y no entiende de comentarios de bloque. Puestos a parchear el código que hay, prefiero hacer algo en condiciones, que además sea capaz de reconocer correctamente programas Lisp no válidos tal y como lo hace ACL2 (o casi). Seguramente revise un poco el algoritmo, ya que a diferencia del algoritmo original, me interesa poder recuperar el código fuente original al 100%.

Written by bluezio

7 de abril de 2009 a 16:53

Publicado en Uncategorized

Responder

Introduce tus datos o haz clic en un icono para iniciar sesión:

Logo de WordPress.com

Estás comentando usando tu cuenta de WordPress.com. Cerrar sesión / Cambiar )

Imagen de Twitter

Estás comentando usando tu cuenta de Twitter. Cerrar sesión / Cambiar )

Foto de Facebook

Estás comentando usando tu cuenta de Facebook. Cerrar sesión / Cambiar )

Google+ photo

Estás comentando usando tu cuenta de Google+. Cerrar sesión / Cambiar )

Conectando a %s

A %d blogueros les gusta esto: