Differences

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

--- teaching:cc4101:tareas:2021-1:tarea1 [2021/04/20 00:20] – created tvallejos
+++ teaching:cc4101:tareas:2021-1:tarea1 [2021/05/10 14:34] (current) – P3, add '}' on first example bortiz
@@ Line 1: / Line 1: @@
-====== Tarea 1 (Entrega: 9 de mayo de 2021) ======
+====== Tarea 1 (Entrega: 7 de mayo de 2021) ======
 ==== Tipos estáticos, tipos opcionales, contratos ====
@@ Line 11: / Line 11: @@
 ----
-Deben entregar via U-cursos **un archivo .zip** que contenga los archivos ''t1.rkt'', ''p1-tests.rkt'', ''p2-tests.rkt'' y ''p3-tests.rkt'', los cuales deben que implementar lo que se solicita en las preguntas siguientes.
@@ Line 18: / Line 16: @@
 Recuerden que tienen que seguir la metodología [[https://users.dcc.uchile.cl/~etanter/preplai/defun.html|vista en las primeras clases]] y dejar sus funciones debidamente documentadas.
 </note>
+Deben entregar via U-cursos **un archivo .zip** que contenga los siguientes archivos: ''t1.rkt'' para el desarrollo de la tarea, y  ''p1-tests.rkt'', ''p2-tests.rkt'' y ''p3-tests.rkt'', para los tests de cada una de las partes.
 <note important>
@@ Line 27: / Line 29: @@
 ===== Parte 1. Lenguaje con funciones de primer orden =====
-En esta parte, buscamos definir un lenguaje que incluye primitivas útiles (números, booleanos, y sus operadores), que admita el uso de with (con n variables), 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, y sus operadores), identificadores locales (''with'' con n identificadores), y definiciones de funciones //top-level// de múltiples argumentos.
 Aquí está la gramática BNF del lenguaje:
@@ Line 41: / Line 43: @@
            | {<binop> <expr> <expr>}
            | {if <expr> <expr> <expr>}
-           | {with { {<id> <expr>}* } <expr>}
+           | {with {{<id> <expr>}*} <expr>}
            | {<id> <expr>*}
 <unop>   ::= ! | add1 | sub1
-<binop>  ::= + | - | * | / | && | eq? | < | ...
+<binop>  ::= + | - | * | / | && | = | < | ...
 </code>
-Un programa está compuesto de (0 o más -- por eso la estrella ''*'' en el BNF) definiciones de funciones, además de una expresión final que sirve de punto de entrada (como el //main// en C y Java).
+Un programa está compuesto de (0 o más -- por eso la estrella ''*'' en el BNF) 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 son estándar. Note que se define un nodo para cada familia de operadores (unarios y binarios), para evitar tener un nodo propio a cada operador en el AST.
 <note>Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.</note>
@@ Line 67: / Line 69: @@
    {define {add2 x} {+ 2 x}}
    {add2 {triple 2}}
-}
-{ ;; Programa de Ejemplo 4
-   {define {two-or-forty-two? x} {or {eq? x 2} {eq? x 42}}}
-   {define {magic x y} {if {two-or-forty-two x}
-                           {two-or-forty-two y}
-                           #f}}
-   {magic 42 2}
 }
 </code>
+En esta parte, su función ''run'' debe, como en clases, parsear y luego interpretar.
 **Instrucciones importantes**:
   * 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.
+  * Tienen que verificar que los argumentos de los operadores booleanos sean booleanos (eso para alinear la verificación dinámica con la verificación estática que harán en la parte 2)
   * En caso de programas con errores dinámicos, su interprete tiene que reportarlos explícitamente. Por ejemplo:
@@ Line 85: / Line 82: @@
 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)
 <code scheme>"Runtime type error: expected Number found Boolean"</code>
+Recuerde que puede testear estos errores con ''test/exn''.
-En esta parte, su función ''run'' debe, como en clases, parsear y luego interpretar.
 -----
 ===== Parte 2. Verificación estática y opcional de tipos =====
-En esta parte usaremos de base el lenguaje logrado en la pregunta 1 y le añadiremos anotaciones de tipos. Las diferencias en la sintaxis del lenguaje (con respecto a 1), serán que en esta parte las declaraciones de función y las expresiones ''with'' aceptan tipos **opcionales** en cada uno de sus argumentos y que además, las funciones pueden poseer anotado un tipo de retorno (también opcional).
+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 aceptan anotaciones de tipos en cada uno de sus argumentos, y también para el retorno
+  * las expresiones ''with'' aceptan anotaciones de tipos en cada identificador introducido
-La sintaxis es la siguiente:
+Observe que las anotaciones de tipos son siempre *opcionales* (en el BNF aquí usamos ''['' '']'' para especificar que lo que va adentro es opcional). La sintaxis es la siguiente:
 <code scheme>
 <fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; <prog> no cambia
@@ Line 103: / Line 102: @@
 </code>
-Note que los ''['' '']'' son parte de la notación BNF, especificando que lo que va adentro es opcional. Note que ''%%with%%'' no incluye anotación del tipo del cuerpo.
+Note que ''%%with%%'' no incluye anotación del tipo del cuerpo.
-Para soportar la verificación opcional, lo que haremos es introducir un tipo comodín ''Any''. Cuando el usuario no especifica ningún tipo, significa lo mismo que especificar ''Any''. El tipo ''Any'' es compatible con cualquier otro tipo: si una función espera un argumento de tipo ''Bool'', es válido pasarle algo de tipo ''Any''.
+Para soportar la verificación opcional, lo que haremos es introducir un tipo comodín ''Any''. Cuando el usuario omite una anotación tipo, significa lo mismo que especificar ''Any''. El tipo ''Any'' es compatible con cualquier otro tipo: si una función espera un argumento de tipo ''Bool'', es válido pasarle algo de tipo ''Any''. Y vice versa: si una función espera un argumento de tipo ''Any'', es válido pasarle cualquier tipo de argumento.
 <note>
@@ Line 113: / Line 112: @@
 Los programas siguientes son válidos, y bien tipados:
 <code scheme>
-{{with {x : Num 5} {+ x 3}}}
+{{with {{x : Num 5} {y : Num 10}} {+ x y}}}
 {{define {gt42 x} : Bool {> x 42}}
@@ Line 121: / Line 120: @@
  {id 5}}
-{{define {add1 {x : Num}} {+ x 1}}
+{{define {add2 {x : Num}} {+ x 2}}
- {with {oops #f}
+ {with {{oops #f}}
-   {add1 oops}}}
+   {add2 oops}}}
 </code>
-En particular, fíjese que el último ejemplo está bien tipado solamente porque se usa ''Any'' para ''oops''. Se debe caer con un error de tipo en ejecución (tal como en el parte 1). Si uno cambia la declaración de ''oops'' para especificar que es de tipo ''Bool'', entonces el programa ya no tipea, es decir, se reporta el error estáticamente.
+En particular, fíjese que el último ejemplo está bien tipado solamente porque se usa ''Any'' para ''oops''. Se debe caer con un error de tipo en ejecución (tal como en el parte 1). Si uno cambia la declaración de ''oops'' para especificar que es de tipo ''Bool''), entonces el programa ya no tipea, es decir, se reporta el error estáticamente.
 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.
@@ Line 134: / Line 133: @@
   * 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 cual).
   * 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. Recuerde que si no se especifica un tipo, se considera ''Any'', y que ''Any'' es válido en cualquier posición.
-  * Deben definir los tipos de los operadores primitivos de manera exacta, p.ej. ''%%!%%'' es como una función de ''Bool'' a ''Bool''. Para ''eq?'', considere que es de tipo ''Any Any → Bool'', para poder comparar números o booleanos (ojo, comparar un booleano con un numero debe levantar un error de tipo dinámico).
+  * Debe definir los tipos de los operadores primitivos de manera exacta, p.ej. ''%%!%%'' es como una función de ''Bool'' a ''Bool''. Para ''='', considere que solamente se aplica a números.
-  * Para la sentencia ''%%if%%'' se verifica que la condición tenga tipo ''%%'Bool%%'' y que ambas ramas tengan el mismo tipo ''%%t%%''. El tipo resultante es t.
+  * Para una expresión ''%%if%%'' se verifica que la condición tenga tipo ''%%'Bool%%'' y que ambas ramas tengan el mismo tipo ''%%t%%''. El tipo resultante es t.
   * Para ''%%with%%'' se verifica que todos los argumentos cumplan con el tipo y el tipo resultante será el del cuerpo de la expresión.
-  * En la aplicación de función se valida que:
+  * 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.
-      - El número de argumentos coincide
-      - El tipo de los argumentos coincida con los tipos esperados de la función aplicada (aquí nuevamente, módulo ''Any'').
 Para los errores:
-  * Los errores de identificadores libres se tienen que detectar estáticamente, antes o durante la verificación de tipos.
+  * Los errores de identificadores libres (o funciones no definidas) se tienen que detectar estáticamente, antes o durante la verificación de tipos.
-  * Los mensaje de error de tipo 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.
 Algunos ejemplos (no representan todos los casos, es de su responsabilidad entregar //test suites// completos):
  <code scheme>
-  > (typecheck '{{define {false {p : Bool}} {&& p {not p}}}
+  >  (typecheck '{3})
-                          {false {> 3 4}}})
+  'Num  </code> <code scheme>
-  (TBool) </code> <code scheme>
+  > (typecheck '{{define {f {p : Bool}} {&& p {! p}}}
+                          {f {> 3 4}}})
+  'Any </code> <code scheme>
   > (typecheck '{{define {one {x : Num}} 1}
                           {one #t}})
   "Static type error: expected Num found Bool" </code> <code scheme>
-  > (typecheck '{> 10 #t})
+  > (typecheck '{{> 10 #t}})
   "Static type error: expected Num found Bool"</code> <code scheme>
-   > (typecheck '{if 73 #t #t})
+   > (typecheck '{{if 73 #t #t}})
   "Static type error: expected Bool found Num"</code> <code scheme>
-  > (typecheck '{with {{x 5} {y : Num #t} {z 42}}
+  > (typecheck '{{with {{x 5} {y : Num #t} {z 42}}
-                            z})
+                            z}})
-  "Static type error: expected Num found Bool"</code> <code scheme>
+  "Static type error: expected Num found Bool"</code>
-  >  (typecheck '{3})
-  (TNum)  </code>
+¿Puede efectivamente convencerse de que todo programa que pasa la verificación de tipo no se cae con un error de tipo durante la ejecución?
 ----
 ===== Parte 3. Contratos en funciones de primer orden (2.0 pt) =====
-Tomando como base el lenguaje generado en el ítem anterior, se procede a añadir una verificación dinámica mediante contratos en funciones de primer orden. 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>
 <fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; como antes
@@ Line 173: / Line 172: @@
            | {<id> [: <type>] @ <contract>}  ; lo único nuevo
 </code>
-Un contrato corresponde a un predicado, una función que reciba exactamente **un argumento** y retorne un **booleano**. Un ejemplo de programa válido puede ser:
+Un contrato corresponde a un predicado, una función que reciba exactamente un argumento y retorne un booleano. Un ejemplo de programa válido puede ser:
 <code scheme>
-{
+{{define {positive x} : Bool {> x 0}}
-   {define {positive x} : Bool {> x 0}}
+ {define {div {x : Num @ positive} y}
-   {define {div {x : Num @ positive} y}
            {/ y x}}
-   {div 5 3}
+ {div 5 3}}
-}
 </code>
 Donde el ''x'' posee como contrato la función ''positive'', que comprueba en tiempo de ejecución que ''x'' sea mayor que 0.
@@ Line 186: / Line 183: @@
 Note que la información de tipo estático es opcional, por lo que uno puede especificar una función solamente mediante contratos.
 <code scheme>
-{
+{{define {positive x} : Bool {> x 0}}
-   {define {positive x} : Bool {> x 0}}
+ {define {div {x @ positive} y}  ; aquí sólo se especifica un contrato
-   {define {div {x @ positive} y}  ; aquí sólo se especifica un contrato
            {/ y x}}
-   {div 5 3}
+ {div 5 3}}
-}
 </code>
@@ Line 199: / Line 194: @@
   * En el intérprete, cuando se efectua 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>
-"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.
-  * Cuando el contrato no tenga firma '((Any) -> Bool) el patrón de error es : <code scheme>
+  * Para poder ser usado como contrato, una función *debe* tener aceptar un argumento de tipo ''Any'' y retornar un valor de tipo ''Bool''. Sino, el patrón de error es : <code scheme>
-"Static contract Error: <c>'s type is not ((Any) -> Bool)"
+"Static contract error: invalid type for <c>"
 </code>  donde ''<c>'' es el nombre del contrato que no tipa.
 Más ejemplos:
 <code scheme>
-{
+{{define {lt100 x} {< x 100}}
-   {define {lt100 x} {< x 100}}
+ {define {positive x} : Bool {> x 0}}
-   {define {positive x} : Bool {> x 0}}
+ {define {percentage? x} : Bool {&& {lt100 x} {positive x}}}
-   {define {percentage? x} {&& {lt100 x} {positive x}}}
+ {define {calc {x @ positive} {y @ percentage?}}
-   {define {calc {x @ positive} {y @ percentage?}
            {/ {* y y} x}}
-   {calc 25 3}
+ {calc 25 3}}
-}
 </code>
 <code scheme>
-(run '{
+> (run '{{define {add x y} : Num {+ x y}}
-       {define {add x y} : Num {+ x y}}
+         {define {oh-no {x @ add} y}
-       {define {oh-no {x @ add} y}
+                    #t}
-               #t}
+         {oh-no 21 21}})
-       {oh-no 21 21}
+"Static contract error: invalid type for add"
- })
-> "Static contract Error: add's type is not ((Any) -> Bool)"
 </code>