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:16] – [Tipos estáticos y contratos] 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 55: Line 55:
 { ;; Programa de Ejemplo 1 { ;; Programa de Ejemplo 1
    {define {sum x y z} {+ x {+ y z}}}    {define {sum x y z} {+ x {+ y z}}}
-   {define {second-first x} {fst {snd x}}}+   {define {cadr x} {fst {snd x}}}
    {with {{x 9} {y {cons 1 {cons 3 4}}}}    {with {{x 9} {y {cons 1 {cons 3 4}}}}
-        {sum x {fst y} {second-first y}} }+        {sum x {fst y} {cadr y}} }
 } }
 { ;; Programa de Ejemplo 2 { ;; Programa de Ejemplo 2
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: 
 <code scheme> <code scheme>
-{{with {{x : Num 5} {y : Num 10}} {+ x y}}}+{ ; Programa de ejemplo 1 
 +  {with {{x : Num 5} {y : Num 10}}  
 +    {+ x y}} 
 +}
  
-{{with {{x 5}} +{ ; Programa de ejemplo 2 
- {with {{y : Num {+ x 1}}} {+ x y}}}+  {with {{x 5}} 
 +    {with {{y : Num {+ x 1}}}  
 +      {+ x y}} 
 +}
  
-{{define {add-pair {p : {Pair Num Num}} {x : Num}} : {Pair Num Num} {cons (+ (fst p) x) (+ (snd p) x)}} +{ ; Programa de ejemplo 3 
- {add-pair {cons 1 1} 1}}+  {define {add-pair {p : {Pair Num Num}} {x : Num}} : {Pair Num Num}  
 +    {cons {+ {fst p} x} {+ {snd p} x}}} 
 +  {add-pair {cons 1 1} 1} 
 +}
  
-{{define {id {x : Num}} x} +{ ; Programa de ejemplo 4 
- {id 5}}+  {define {id {x : Num}} x} 
 +  {id 5} 
 +} 
 + 
 +{ ; Programa de ejemplo 5 
 +  {define {sum {x : Num} {y : Num} {z : Num}}  
 +    {+ x {+ y z}}} 
 +  {define {cadr {x : {Pair Num {Pair Num Num}}}} : Num  
 +    {fst {snd x}}} 
 +  {with {{x 9} {y {cons 1 {cons 3 4}}}} 
 +        {sum x {fst y} {cadr y}} } 
 +}
  
 </code> </code>
Line 131: 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 138: 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 171: 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 177: Line 197:
 Un contrato corresponde a un predicado, una función que recibe exactamente un argumento y retorna un booleano. Un ejemplo de programa válido puede ser: Un contrato corresponde a un predicado, una función que recibe exactamente un argumento y retorna un booleano. Un ejemplo de programa válido puede ser:
 <code scheme> <code scheme>
-{{define {positive {x : Num}} : Bool {< 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}}
Line 187: 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.
Line 198: Line 218:
 Más ejemplos: Más ejemplos:
 <code scheme> <code scheme>
-{{define {positive {x : Num}} : Bool {< 0 x}} +{{define {positive {x : Num}} {< 0 x}} 
- {define {negate {x : Num @ positive}} : Num -x}+ {define {negate {x : Num @ positive}} -x}
  {negate 23}}  {negate 23}}
 </code> </code>
  
 <code scheme> <code scheme>
-{{define {pair-lt100? {x : {Num x Num}}} : Bool {if {< {fst x} 100} {< {snd x} 100} #f}} +{{define {pair-lt100? {x : {Pair Num Num}}} {if {< {fst x} 100} {< {snd x} 100} #f}} 
- {define {sum-pair {x : {Num x Num} @ pair-lt100?} {+ {fst x} {snd x}}}}+ {define {sum-pair {x : {Pair Num Num} @ pair-lt100?} {+ {fst x} {snd x}}}}
  {< 200 {sum-pair {cons 80 50}}}}  {< 200 {sum-pair {cons 80 50}}}}
 </code> </code>
Line 211: Line 231:
  
 <code scheme> <code scheme>
-> (run '{{define {add {x : Num} {y : Num}} : Num {+ x y}} +> (run '{{define {add {x : Num} {y : Num}} {+ x y}} 
-         {define {oh-no {x : Num @ add}} : Num x}+         {define {oh-no {x : Num @ add}} x}
                     #t}                     #t}
          {oh-no 21 21}})          {oh-no 21 21}})