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:tarea1xyz [2023/04/03 16:17] – [Tipos estáticos y contratos] rodrigo.urreateaching:cc4101:tareas:tarea1xyz [2023/04/05 21:02] (current) – etanter
Line 17: Line 17:
  
  
-Deben entregar via U-cursos **un archivo .zip** que contenga los siguientes archivos: ''p1.rkt'', ''p2.rkt'' y ''p3.rkt'', archivos que deberán contener las funcionalidades solicitadas en cada pregunta y los test respectivos.+Deben entregar via U-cursos **un archivo .zip** que contenga los siguientes archivos: ''p1.rkt'', ''p1-test.rkt'', ''p2.rkt'', ''p2-test.rkt'', ''p3.rkt'' y ''p3-test.rkt'', archivos que deberán contener las funcionalidades solicitadas en cada pregunta y los tests respectivos. Puede usar como base los archivos que se encuentra aquí.
  
  
Line 30: Line 30:
 En esta parte, vamos a implementar un lenguaje que incluye primitivas útiles (números, booleanos, pares, y operadores simples), identificadores locales (''with'' con una cantidad arbitraria de identificadores), y definiciones de funciones //top-level// de múltiples argumentos. En esta parte, vamos a implementar un lenguaje que incluye primitivas útiles (números, booleanos, pares, y operadores simples), identificadores locales (''with'' con una cantidad arbitraria de identificadores), y definiciones de funciones //top-level// de múltiples argumentos.
  
-Aquí está la gramática BNF del lenguaje:+La gramática BNF del lenguaje se  define a continuación:
 <code scheme> <code scheme>
 <prog>   ::= {<fundef>* <expr>} <prog>   ::= {<fundef>* <expr>}
Line 55: Line 55:
 </code> </code>
 Un programa está compuesto de 0 o más definiciones de funciones, además de una expresión final que sirve de punto de entrada (como el //main// en C y Java). Una definición de función incluye el nombre de la función, el nombre de los parámetros formales, y finalmente la expresión del cuerpo de la función. Las expresiones ''fst'' y ''snd'' obtienen el primer y segundo elemento de un par, respectivamente (similar a ''car'' y ''cdr'' de Racket). Las demás expresiones siguen la presentación estándar vista en clases. Un programa está compuesto de 0 o más definiciones de funciones, además de una expresión final que sirve de punto de entrada (como el //main// en C y Java). Una definición de función incluye el nombre de la función, el nombre de los parámetros formales, y finalmente la expresión del cuerpo de la función. Las expresiones ''fst'' y ''snd'' obtienen el primer y segundo elemento de un par, respectivamente (similar a ''car'' y ''cdr'' de Racket). Las demás expresiones siguen la presentación estándar vista en clases.
 +
 +Los programas que terminan reducen a valores. Estos pueden ser números, booleanos o pares de valores. Siguiendo buenas prácticas, definimos un tipo de dato inductivo ''Val'' para los valores (provisto en el código fuente de la parte 1).
  
 Algunos ejemplos de programas válidos para este lenguaje pueden ser: Algunos ejemplos de programas válidos para este lenguaje pueden ser:
Line 80: Line 82:
 </code> </code>
  
-En esta parte, su función ''run'' debe, como en clases, parsear y luego interpretar.+Su función ''run'' debe ser capaz de recibir un programa en sintaxis concreta e interpretarlo para producir un valor. 
 + 
 +  * Implemente la función ''parse :: s-Prog -> Prog'' 
 +  * Implemente la función ''interp :: Expr -> Env -> list Fundef -> Val''
  
 **Observaciones importantes**: **Observaciones importantes**:
   * Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.   * Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.
-  * Para implementar el lenguaje, tiene que [[https://users.dcc.uchile.cl/~etanter/play-interps/Functions_with_Environments.html|usar ambientes]], y no una función de substitución. +  * Al implementar el lenguaje, asegúrese de hacerlo [[https://users.dcc.uchile.cl/~etanter/play-interps/Functions_with_Environments.html|utilizando ambientes]], y no una función de substitución. 
-  * La semántica debe considerar scoping léxico, no dinámico. +  * La semántica debe considerar alcance léxico, no dinámico. 
-  * Tienen que verificar que los argumentos de los operadores numéricos sean numéricos y que los argumentos de los operadores de pares sean pares (eso para alinear la verificación dinámica con la verificación estática que harán en la parte 2).+  * Verifique en tiempo de ejecución que los argumentos de los operadores numéricos sean numéricos. Y que los argumentos de los operadores de pares sean pares (En la parse 2 se alineará la verificación dinámica con la verificación estática).
   * Considere que la igualdad solo es válida sobre números.   * Considere que la igualdad solo es válida sobre números.
-  * La condición de ''if'' debe ser un booleano.+  * La condición de una expresión ''if'' deben ser un booleano.
   * En caso de programas con errores dinámicos, su intérprete tiene que reportarlos explícitamente. Por ejemplo:   * En caso de programas con errores dinámicos, su intérprete tiene que reportarlos explícitamente. Por ejemplo:
  
 <code scheme>{+ 1 {cons 3 4}}</code>  <code scheme>{+ 1 {cons 3 4}}</code> 
-debe caerse en tiempo de ejecución con un error (se levantan con ''(error msg)'', tal como lo hacemos en clase con los identificadores libres)+debe fallar en tiempo de ejecución con un error (se levantan con ''(error msg)'', tal como lo hacemos en clase con los identificadores libres)
 <code scheme>"Runtime type error: expected Number found Pair"</code> <code scheme>"Runtime type error: expected Number found Pair"</code>
-Recuerde que puede testear estos errores con ''test/exn''.+Recuerde que puede verificar si un test lanza una excepción con ''test/exn''.
  
  
Line 100: Line 105:
 ===== Parte 2. Verificación estática de tipos (2.5 ptos.) =====  ===== Parte 2. Verificación estática de tipos (2.5 ptos.) ===== 
 En esta parte vamos a extender el lenguaje de la Parte 1 con anotaciones de tipos y verificación estática de ellos. Las diferencias en la sintaxis del lenguaje respecto de la parte anterior son: En esta parte vamos a extender el lenguaje de la Parte 1 con anotaciones de tipos y verificación estática de ellos. Las diferencias en la sintaxis del lenguaje respecto de la parte anterior son:
-  * las declaraciones de función incluyen anotaciones de tipos en cada uno de sus argumentos y también para el tipo de retorno +  * Las declaraciones de función incluyen anotaciones de tipos en cada uno de sus argumentos y también para el tipo de retorno. 
-  * las expresiones ''with'' incluyen anotaciones de tipos en cada identificador introducido+  * Las expresiones ''with'' incluyen anotaciones de tipos en cada identificador introducido.
  
 La nueva sintaxis es la siguiente: La nueva sintaxis es la siguiente:
Line 107: Line 112:
 ;; <prog> no cambia ;; <prog> no cambia
  
-<fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} +<fundef> ::= {define {<id> {arg}*} [: <type>] <expr>} 
    
-<arg>    ::= {<id> : <type>}+<arg>    ::= {<id> : <type>}   
  
 <expr>   ::= ... | {with { {<id> [: <type>] <expr>}* } <expr>}  ; los otros casos no cambian <expr>   ::= ... | {with { {<id> [: <type>] <expr>}* } <expr>}  ; los otros casos no cambian
Line 154: Line 159:
  
  
-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.+  * Defina una función ''typecheck :: Prog -> Type/err'' que toma un programa y nos retorna su tipo, o lanza un error.  
 +  * Extienda su función ''run'' para que verifique el tipo del programa (este paso puede fallar) antes de interpretarlo.
  
 **Observaciones importantes**: **Observaciones importantes**:
Line 161: Line 167:
   * Para una definición de función, se valida que la expresión del cuerpo tenga el mismo tipo que el tipo de retorno declarado, suponiendo que cada argumento tiene el tipo declarado. Si el tipo de retorno no se especifica, entonces se usa el tipo del cuerpo.   * Para una definición de función, se valida que la expresión del cuerpo tenga el mismo tipo que el tipo de retorno declarado, suponiendo que cada argumento tiene el tipo declarado. Si el tipo de retorno no se especifica, entonces se usa el tipo del cuerpo.
   * Debe definir los tipos de los operadores primitivos de manera exacta, p.ej. ''%%<%%'' es una operación que toma dos ''Num'' y retorna ''Bool''.    * Debe definir los tipos de los operadores primitivos de manera exacta, p.ej. ''%%<%%'' es una operación que toma dos ''Num'' y retorna ''Bool''. 
-  * Para ''='', considere que solamente se aplica a números.+  * Considere que la igualdad (''='') solo puede comparar 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. Si los identificadores no tienen tipo explícito, entonces se les asigna el de la expresión asociada.   * 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. El tipo resultante de una aplicación es el tipo de retorno de la función aplicada.
  
 Para los errores: Para los errores:
-  * Los errores de identificadores libres (o funciones no definidas) se tienen que detectar estáticamente, antes o durante la verificación de tipos.+  * Los errores de identificadores libres (o funciones no definidas). Este error debe detectarse estáticamente.
   * Los mensajes de error de tipo detectados estáticamente tienen que seguir el siguiente patrón:    * Los mensajes de error de tipo detectados estáticamente tienen que seguir el siguiente patrón: 
 <code scheme>"Static type error: expected T1 found T2"</code> donde ''T1'' es el tipo esperado y ''T2'' el tipo encontrado. <code scheme>"Static type error: expected T1 found T2"</code> donde ''T1'' es el tipo esperado y ''T2'' el tipo encontrado.
Line 174: Line 180:
  <code scheme>  <code scheme>
   >  (typecheck '{3})   >  (typecheck '{3})
-  (Num)  </code> <code scheme>+  (numT)  </code> <code scheme>
   > (typecheck '{{define {f {p : Bool}} {if p 23 42}}   > (typecheck '{{define {f {p : Bool}} {if p 23 42}}
                           {f {< 3 4}}})                           {f {< 3 4}}})
-  (Num) </code> <code scheme>   +  (numT) </code> <code scheme>   
   > (typecheck '{{define {one {x : Num}} 1}   > (typecheck '{{define {one {x : Num}} 1}
                           {one #t}})                           {one #t}})
Line 204: Line 210:
 {{define {positive {x : Num}} {< 0 x}} {{define {positive {x : Num}} {< 0 x}}
  {define {sub {x : Num @ positive} {y : Num}} : Num  {define {sub {x : Num @ positive} {y : Num}} : Num
-           {+ y -x}}+           {- y x}}
  {sub 5 3}}  {sub 5 3}}
 </code> </code>
-Donde el ''x'' posee como contrato la función ''positive'', que comprueba en tiempo de ejecución que ''x'' sea mayor que 0.+Donde el argumento ''x'' posee como contrato la función ''positive'', que comprueba en tiempo de ejecución que ''x'' sea mayor que 0.
  
  
-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.+  * Extienda nuevamente su función ''run'' para que verifique los contratos en tiempo de ejecución. 
  
 **Observaciones importantes**: **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 debe que verificar que los argumentos cumplan con los contratos declarados (en caso de que existan).  
-  * Cuando el contrato no se cumpla, el patrón de error es: <code scheme>+  * Cuando el contrato no se cumpla, se debe lanzar un error con el siguiente patrón: <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''. En caso de no cumplir esta condición se debe lanzar un error con el siguiente patrón: <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.
Line 224: Line 230:
 <code scheme> <code scheme>
 {{define {positive {x : Num}} {< 0 x}} {{define {positive {x : Num}} {< 0 x}}
- {define {negate {x : Num @ positive}} -x}+ {define {negate {x : Num @ positive}} {- 0 x}}
  {negate 23}}  {negate 23}}
 </code> </code>
Line 240: Line 246:
 > (run '{{define {add {x : Num} {y : Num}} {+ x y}} > (run '{{define {add {x : Num} {y : Num}} {+ x y}}
          {define {oh-no {x : Num @ add}} x}          {define {oh-no {x : Num @ add}} x}
-                    #t} 
          {oh-no 21 21}})          {oh-no 21 21}})
 "Static contract error: invalid type for add" "Static contract error: invalid type for add"
 </code> </code>