martes, 14 de agosto de 2007

Map y Find

Hice algunos cambios:
  • Ahora multiassign se llama map, es un poco más marketinero.
  • Modularice un poquito la semántica de (ahora llamado) map.
  • No se generan nombres nuevos para las variables al entrar a un if. En cambio se espera a que sean modificadas por primera vez para hacerlo.
  • Rompí un poco la estructura lineal de los Proofplans, de esta manera se pueden ir olvidando las cosas que se probaron dentro de un lema, dejando sólamente la conclusión de ese lema, para evitar enviarle al prover axiomas que no usará.
  • Ahora los procedimientos deben indicar explícitamente que parámetros tocan. Esto genera chequeos sintácticos que prohiben la asignación sobre los mismos. Esto permite usar procedimientos dentro de los bloques que de map (y otras construcciones de alto nivel) que restringen qué cosas se pueden tocar.
También implementé una nueva construcción, llamada find first. Más tarde los detalles.

No hay comentarios.: