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:2021-1:tarea1 [2021/04/20 13:08] – etanterteaching:cc4101:tareas:2021-1:tarea1 [2021/05/10 14:34] (current) – P3, add '}' on first example bortiz
Line 43: Line 43:
            | {<binop> <expr> <expr>}            | {<binop> <expr> <expr>}
            | {if <expr> <expr> <expr>}            | {if <expr> <expr> <expr>}
-           | {with { {<id> <expr>}* } <expr>}+           | {with {{<id> <expr>}*} <expr>}
            | {<id> <expr>*}            | {<id> <expr>*}
                        
Line 69: Line 69:
    {define {add2 x} {+ 2 x}}    {define {add2 x} {+ 2 x}}
    {add2 {triple 2}}    {add2 {triple 2}}
-} 
- 
-{ ;; Programa de Ejemplo 4 
-   {define {two-or-forty-two? x} {or {= x 2} {= x 42}}} 
-   {define {magic x y} {if {two-or-forty-two x} 
-                           {two-or-forty-two y} 
-                           #f}} 
-   {magic 42 2} 
 } }
 </code> </code>
Line 84: Line 76:
 **Instrucciones importantes**: **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.   * 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:   * En caso de programas con errores dinámicos, su interprete tiene que reportarlos explícitamente. Por ejemplo:
  
Line 89: 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) 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> <code scheme>"Runtime type error: expected Number found Boolean"</code>
 +Recuerde que puede testear estos errores con ''test/exn''.
  
  
Line 126: Line 120:
  {id 5}}  {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> </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'' (''{with {{oops : Bool #f}} ...}''), 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. 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 139: 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).   * 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.   * 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 ''='', considere que es de tipo ''Num Num → Bool'', es decir solamente se aplica a números. +  * 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.   * 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: 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. <code scheme>"Static type error: expected T1 found T2"</code> donde ''T1'' es el tipo esperado y ''T2'' el tipo encontrado.
  
Line 155: Line 147:
   >  (typecheck '{3})   >  (typecheck '{3})
   'Num  </code> <code scheme>   'Num  </code> <code scheme>
-  > (typecheck '{{define {false {p : Bool}} {&& p {not p}}} +  > (typecheck '{{define {f {p : Bool}} {&& p {! p}}} 
-                          {false {> 3 4}}}) +                          {f {> 3 4}}}) 
-  'Bool </code> <code scheme>   +  'Any </code> <code scheme>   
   > (typecheck '{{define {one {x : Num}} 1}   > (typecheck '{{define {one {x : Num}} 1}
                           {one #t}})                           {one #t}})
   "Static type error: expected Num found Bool" </code> <code scheme>   "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>   "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>   "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>   "Static type error: expected Num found Bool"</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) ===== ===== 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> <code scheme>
 <fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; como antes <fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; como antes
Line 178: Line 172:
            | {<id> [: <type>] @ <contract>}  ; lo único nuevo            | {<id> [: <type>] @ <contract>}  ; lo único nuevo
 </code> </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> <code scheme>
 {{define {positive x} : Bool {> x 0}} {{define {positive x} : Bool {> x 0}}
Line 211: Line 205:
  {define {positive x} : Bool {> x 0}}  {define {positive x} : Bool {> x 0}}
  {define {percentage? x} : Bool {&& {lt100 x} {positive x}}}  {define {percentage? x} : Bool {&& {lt100 x} {positive x}}}
- {define {calc {x @ positive} {y @ percentage?}+ {define {calc {x @ positive} {y @ percentage?}}
            {/ {* y y} x}}            {/ {* y y} x}}
  {calc 25 3}}  {calc 25 3}}