Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
teaching:cc4101:tareas:2022-1:tarea1 [2022/04/06 16:28] – [Parte 2. Verificación estática de tipos (2.5 ptos.)] tdiazteaching:cc4101:tareas:2022-1:tarea1 [2022/04/19 18:54] (current) – etanter
Line 1: Line 1:
-====== Tarea 1 (Entrega: XXX de Abril de 2022) ======+====== Tarea 1 (Entrega: 24 de Abril de 2022) ======
  
 ==== Tipos estáticos y contratos ==== ==== Tipos estáticos y contratos ====
Line 64: Line 64:
 } }
 { ;; Programa de Ejemplo 3 { ;; Programa de Ejemplo 3
-   {define {triple x} {* 3 x}}+   {define {triple x} {+ x {+ x x}}}
    {define {add2 x} {+ 2 x}}    {define {add2 x} {+ 2 x}}
    {add2 {triple 2}}    {add2 {triple 2}}
Line 111: Line 111:
 </code> </code>
  
-En el BNF utilizamos ''[ ]'' para denotar que algo es opcional. Note que ''%%with%%'' no incluye anotación del tipo del cuerpo y que los tipos de los identificadores son opcionales. Igualmente, el tipo de retorno de una función es opcional, pero el de cada argumento *sí* es necesario. +En el BNF utilizamos ''[ ]'' para denotar que algo es opcional. Note que ''%%with%%'' no incluye anotación del tipo del cuerpo y que los tipos de los identificadores son opcionales. Igualmente, el tipo de retorno de una función es opcional, pero el de cada argumento **sí** es necesario. Para funciones recursivas, pueden asumir que el tipo de retorno tiene que ser especificado.
  
 Los programas siguientes están bien tipados:  Los programas siguientes están bien tipados: 
Line 151: Line 151:
 En esta parte, deben definir una nueva función ''typecheck'' que toma un programa y nos retorna su tipo, o un error. A su vez, su función ''run'' debe parsear, typecheckear (este paso puede fallar), y luego interpretar. En esta parte, deben definir una nueva función ''typecheck'' que toma un programa y nos retorna su tipo, o un error. A su vez, su función ''run'' debe parsear, typecheckear (este paso puede fallar), y luego interpretar.
  
-**Instrucciones**:+**Observaciones importantes**:
   * Recuerden que la gramática BNF dicta la estructura de sus definiciones   * Recuerden que la gramática BNF dicta la estructura de sus definiciones
   * La verificación de tipos de un programa consiste en verificar que todas las definiciones de función estén bien tipadas, y que la última expresión tiene un tipo (no importa cuál).   * La verificación de tipos de un programa consiste en verificar que todas las definiciones de función estén bien tipadas, y que la última expresión tiene un tipo (no importa cuál).
Line 158: Line 158:
   * Para ''='', considere que solamente se aplica a números.   * Para ''='', considere que solamente se aplica a números.
   * Para una expresión ''%%if%%'' la condición debe tener tipo ''%%Bool%%'' y ambas ramas deben tener el mismo tipo ''%%t%%''. El tipo resultante de la expresión ''%%if%%'' es ''%%t%%''.   * Para una expresión ''%%if%%'' la condición debe tener tipo ''%%Bool%%'' y ambas ramas deben tener el mismo tipo ''%%t%%''. El tipo resultante de la expresión ''%%if%%'' es ''%%t%%''.
-  * Para ''%%with%%'' se verifica que todos los argumentos cumplan con el tipo declarado y el tipo resultante será el del cuerpo de la expresión.+  * Para ''%%with%%'' se verifica que todos los argumentos cumplan con el tipo declarado y el tipo resultante será el del cuerpo de la expresión. Si los identificadores no tienen tipo explícito, entonces se les asigna el de la expresión asociada.
   * En la aplicación de función se valida que el número de argumentos coincide, y que el tipo de los argumentos coincide con los tipos esperados de la función aplicada. La aplicación en sí tiene el tipo de retorno de la función aplicada.   * En la aplicación de función se valida que el número de argumentos coincide, y que el tipo de los argumentos coincide con los tipos esperados de la función aplicada. La aplicación en sí tiene el tipo de retorno de la función aplicada.
  
Line 191: Line 191:
 Ahora vamos a añadir verificación dinámica mediante contratos a las funciones de nuestro lenguaje. El único cambio en la sintaxis del lenguaje se ve reflejado en la definición de funciones, donde ahora se puede definir además un contrato para cada argumento: Ahora vamos a añadir verificación dinámica mediante contratos a las funciones de nuestro lenguaje. El único cambio en la sintaxis del lenguaje se ve reflejado en la definición de funciones, donde ahora se puede definir además un contrato para cada argumento:
 <code scheme> <code scheme>
-<fundef> ::= {define {<id> <arg>*} : <type> <expr>} ; como antes+<fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; como antes
 <arg>    ::= {<id> : <type>}        ; como antes <arg>    ::= {<id> : <type>}        ; como antes
            | {<id> : <type> @ <contract>}  ; lo único nuevo            | {<id> : <type> @ <contract>}  ; lo único nuevo
Line 207: Line 207:
 En esta parte, su función ''run'' debe hacer lo mismo que en la parte 2. Solamente que la interpretación ahora incluye verificar contratos. En esta parte, su función ''run'' debe hacer lo mismo que en la parte 2. Solamente que la interpretación ahora incluye verificar contratos.
  
-**Instrucciones**:+**Observaciones importantes**:
   * En el intérprete, cuando se efectúa una aplicación de función, se tiene que verificar que sus argumentos cumplan con los contratos declarados (de existir -- sino, procede como antes).    * En el intérprete, cuando se efectúa una aplicación de función, se tiene que verificar que sus argumentos cumplan con los contratos declarados (de existir -- sino, procede como antes). 
   * Cuando el contrato no se cumpla, el patrón de error es: <code scheme>   * Cuando el contrato no se cumpla, el patrón de error es: <code scheme>
 "Runtime contract error: <v> does not satisfy <contract>" "Runtime contract error: <v> does not satisfy <contract>"
 </code> donde ''<v>'' es el valor al que se le aplicó el contrato <contract> el nombre de este. </code> donde ''<v>'' es el valor al que se le aplicó el contrato <contract> el nombre de este.
-  * Una función usada como contrato *debe* aceptar un solo argumento de cualquier tipo válido y *debe* retornar un valor de tipo ''Bool''. Sino, el patrón de error es : <code scheme>+  * Una función usada como contrato **debe** aceptar un solo argumento de cualquier tipo válido y **debe** retornar un valor de tipo ''Bool''. Sino, el patrón de error es : <code scheme>
 "Static contract error: invalid type for <c>" "Static contract error: invalid type for <c>"
 </code>  donde ''<c>'' es el nombre del contrato que no tipa. </code>  donde ''<c>'' es el nombre del contrato que no tipa.