unitarias - ¿Cómo utilizar la búsqueda automática de pruebas de Agda de manera efectiva?

testng

Question

Cuando escribía pruebas noté que la búsqueda automática de pruebas de Agda con frecuencia no encontraba soluciones que me parecieran obvias. Desafortunadamente, dar con un pequeño ejemplo, que ilustra el problema parece ser difícil, por lo que trato de describir los patrones más comunes.

• Olvidé agregar -m al agujero para que Agda vea el alcance del módulo. ¿Puedo hacer que esa bandera sea la predeterminada? ¿Qué desventajas tendría eso?
• A menudo, el agujero actual puede llenarse con un parámetro de la función que estoy a punto de implementar. Incluso al agregar -m , Agda no considerará los parámetros de función o los símbolos introducidos en las cláusulas let o where . ¿Hay algo malo con simplemente intentarlos todos?
• Al ver un objetivo, los símbolos introducidos en las cláusulas let o where ni siquiera se muestran. ¿Por qué?

¿Qué otros hábitos pueden hacer que el uso del auto sea más efectivo?

Answer 1

La búsqueda automática de pruebas de Agda está cableada en el compilador. Eso lo hace rápido, pero limita la cantidad de personalización que puedes hacer. Un enfoque alternativo sería implementar un procedimiento de búsqueda de pruebas similar utilizando el mecanismo de reflexión de Agda. Con la reciente versión reforzada de reflexión utilizando la mónada TC, ya no necesita implementar su propio procedimiento de unificación.

Carlos Tome ha estado trabajando para reimplementar estas ideas (consulte su código https://github.com/carlostome/AutoInAgda ). Ha estado trabajando en varias versiones que intentan usar información del contexto, imprimir información de depuración, etc. ¡Espero que esto ayude!