====== Tarea 1b (Entrega: Domingo 21 de Abril de 2024) ======

==== Lenguaje con tipos estáticos ====

Ya se habrán dado cuenta que ciertos lenguajes tienen tipos estáticos (C/C++, Java, C#, Scala, etc.) y otros tienen tipos dinámicos (Python, Racket, JavaScript, etc.).

En esta tarea van a implementar un lenguaje simple con funciones de primer orden, tipos de datos básicos y pares. Para implementar este lenguaje necesitaremos un parser (lo implementamos en la tarea 1a), y un intérprete, dividiremos el desarrollo de esta tarea en dos partes (más una opcional). Primero, el lenguaje contará sólo con chequeo dinámico de tipos (parte 1), para luego agregar verificación de tipos estáticos (parte 2). Opcionalmente (como bonus), puede agregar contratos dinámicos para funciones (parte 3). 

----

<note important>
Consulte las normas de entrega de tareas en http://pleiad.cl/teaching/cc4101.
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: ''{{ :teaching:cc4101:tareas:2024-1:tarea1b:p1.rkt |p1.rkt}}'', ''{{ :teaching:cc4101:tareas:2024-1:tarea1b:p1-test.rkt |p1-test.rkt}}'', ''{{ :teaching:cc4101:tareas:2024-1:tarea1b:p2.rkt |p2.rkt}}'', ''{{ :teaching:cc4101:tareas:2024-1:tarea1b:p2-test.rkt |p2-test.rkt}}'', archivos que deberán contener las funcionalidades solicitadas en cada pregunta y los tests respectivos.

Si lo desea, puede obtener un bonus resolviendo la tercera parte, que es opcional: ''{{ :teaching:cc4101:tareas:2024-1:tarea1b:p3.rkt |p3.rkt}}'' y ''{{ :teaching:cc4101:tareas:2024-1:tarea1b:p3-test.rkt |p3-test.rkt}}''. Más detalles al final del documento.

**Nota:** Es libre de implementar el intérprete usando sustitución inmediata o diferida (con ambientes), en cuyo caso podría serle útil el archivo {{ :teaching:cc4101:tareas:2023-1:env.rkt |env.rkt}}

Deben entregar vía U-Cursos **un único archivo .zip** que contenga todos los archivos de su entrega.

<note important>
  * Recuerde incluir tests con cobertura de todos los casos relevantes para todas las funciones que implemente y aquellas que extienda, pues esto se considerará en la evaluación.
</note>

===== Parte 1. Lenguaje con funciones de primer orden (1.5 ptos.) ===== 

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.

La gramática BNF del lenguaje se  define a continuación:
<code scheme>
<prog>   ::= {<fundef>* <expr>}
 
<fundef> ::= {define {<id> <id>*} <expr>}
 
<expr>   ::= <num>
           | <id>
           | <bool>
           | {cons <expr> <expr>}
           | {add1 <expr>}
           | {+ <expr> <expr>}
           | {- <expr> <expr>}
           | {< <expr> <expr>}
           | {= <expr> <expr>}
           | {! <expr>}
           | {&& <expr> <expr>}
           | {|| <expr> <expr>}
           | {fst <expr>}
           | {snd <expr>}
           | {if <expr> <expr> <expr>}
           | {with {<binding>*} <expr>}
           | {<id> <expr>*}

<binding> ::= {<id> <expr>}
           
</code>

Esta gramática es similar a la presentada en la tarea 1a, con las siguientes diferencias.
  * Se agregan dos operadores booleanos extra, estos son ''&&'' y ''||''.
  * Se agregan pares, los cuales se definen utilizando ''cons''. Las expresiones ''fst'' y ''snd'' permiten obtienen el primer y segundo elemento, respectivamente (similar a ''car'' y ''cdr'' de Racket).

Los programas que terminan reducen a valores. Estos pueden ser números, booleanos o pares de valores. Siguiendo las buenas prácticas de desarrollo del curso, se define un tipo de datos inductivo ''Val'' para los valores del lenguaje (provisto en el código fuente de la parte 1). 

Algunos ejemplos de programas válidos para el lenguaje descrito pueden ser:
<code scheme>
{
   {with {{x 3}
          {y {+ 1 2}}}
       {if {= x y} x y}}
}

{
   {with {{x 5}
          {y 42}}
       {cons x z}}
}

{
   {define {sum x y z} {+ x {+ y z}}}
   {define {cadr x} {fst {snd x}}}
   {with {{x 9}
          {y {cons 1 {cons 3 4}}}}
       {sum x {fst y} {cadr y}} }
}

{
   {define {implies p q} {|| {! p} q}}
   {implies #f #t}
}
</code>


**Observaciones importantes**:
  * Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.
  * La semántica del ''with'' es la del [[https://docs.racket-lang.org/reference/let.html#%28form._%28%28lib._racket%2Fprivate%2Fletstx-scheme..rkt%29._let%29%29|let]] de Racket. En particular esto significa que un binding no puede definirse en función de los bindings anteriores del mismo ''with''. Por ejemplo, el siguiente programa lanza un error de identificador libre, pues ''x'' no es "visible" desde la expresión nombrada por ''y'':
  <code scheme>
  {
    {with {{x 2}
           {y {add1 x}}}
        {add1 y}}
  }
  
  >> Free identifier: x
  </code>
En cambio, el siguiente programa si funciona, pues ''x'' fue introducido en el ''with'' que "engloba" al ''with'' donde se usa ''x''.
<code scheme>
  {
    {with {{x 2}}
       {with {{y {add1 x}}}
          {add1 y}}
  }
  </code>
Además de lo anterior, asumiremos por simplicidad que en los bindings de un mismo ''with'' no pueden haber repeticiones/reintroducciones de identificadores. **No es necesario que verifique este punto**, puede simplemente asumir que es parte del contrato. Por ejemplo, el comportamiento del siguiente programa estaría indefinido:
<code scheme>
  {
     {with {{x 2}
            {x 4}}
        x}
  }
</code>
  * Debe verificar en tiempo de ejecución que los argumentos de los operadores numéricos sean numéricos, que los argumentos de los operadores booleanos sean booleanos, y que los argumentos de los operadores de pares sean pares (En la parte 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.
  * La condición de una expresión ''if'' debe ser un booleano.
  * En caso de programas con errores dinámicos de tipo, su intérprete tiene que reportarlos explícitamente, mostrando un mensaje con el siguiente formato:
<code>Runtime type error: expected <type> found <value></code>
donde ''<type> ::= Number | Boolean | Pair'', y ''<value>'' es un valor en sintaxis concreta.
**Nota:** En el código base se provee la función ''pp-val :: Val -> String'', que dado un valor retorna un string con su representación en sintaxis concreta. Los errores se levantan con ''(error msg)'' (tal como lo hacemos en clase con los identificadores libres).

A continuación se muestran algunos programas que fallan dinámicamente por errores de tipo:

<code scheme>
{
  {+ 1 {cons 3 4}}
}

>> Runtime type error: expected Number found {cons 3 4}
</code>
<code scheme>
{
  {&& {+ 1 2} #f}
}

>> Runtime type error: expected Boolean found 3
</code>
<code scheme>
{
  {snd {! #t}}
}

>> Runtime type error: expected Pair found #f
</code>
<code scheme>
{
  {if {cons 2 3}
      1
      0}
}

>> Runtime type error: expected Boolean found {cons 2 3}
</code>
Recuerde que puede verificar si un test lanza una excepción con ''test/exn''.
  * Al aplicar una función, debe verificar en tiempo de ejecución que la función esté definida y que sea aplicada al número correcto de argumentos, de lo contrario debe lanzar un error. Por ejemplo, los siguientes programas lanzan errores:
<code scheme>
{
  {foo 2 3}
}

>> Undefined function: foo


{
  {define {bar p} {! p}}
  {bar #t #f}
}

>> Arity mismatch: function bar expected 1 arguments, received 2
</code>


Teniendo en cuenta todo lo descrito anteriormente, implemente las siguientes funciones:

  - **[1.0 pts]** ''interp :: Expr List[Fundef] -> Val or error'', que interpreta una expresión considerando una lista de funciones definidas al top-level. Si lo desea, puede implementar ''interp'' usando ambientes (sustitución diferida). Recuerde actualizar la firma de la función si elige dicha opción.
  - **[0.2 pts]** ''run :: s-expr -> Val or error'', que toma un programa escrito en sintaxis concreta, lo parsea e interpreta.

El testing recibe **0.3 pts**
-----

===== Parte 2. Verificación estática de tipos (2.5 ptos.) ===== 

En esta parte vamos a extender el lenguaje 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 expresiones ''with'' pueden incluir anotaciones de tipos en cada identificador introducido.

La nueva sintaxis concreta es la siguiente:
<code scheme>
;; <prog> y <expr> no cambian

<fundef> ::= {define {<id> <arg>*} : <type> <expr>} 
 
<arg>    ::= {<id> : <type>} 

<binding> ::= {<id> [: <type>] <expr>}

<type>   ::= Num | Bool | {Pair <type> <type>}
</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. 
Por otro lado, el tipo de retorno de una función siempre debe estar presente, al igual que el de cada uno de sus argumentos.

A continuación puede ver ejemplos de programas en la nueva sintaxis, los que (además) están bien tipados:
<code scheme>
{
  {with {{x : Num 5}
         {y : Num 10}} 
     {+ x y}}
}
</code>
<code scheme>
{
  {with {{x 5}}
     {with {{y : Num {+ x 1}}} 
        {+ x y}}
}
</code>
<code scheme>
{
  {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}
}
</code>
<code scheme>
{
  {define {id {x : Num}} : Num x}
  {id 5}
}
</code>
<code scheme>
{
  {define {sum {x : Num} {y : Num} {z : Num}} : 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>

===== Actualizando el AST y Parser =====

Note que se agregó el nodo ''<arg>'' al BNF, el cual especifica la sintaxis concreta de un argumento de función.
  - **[0.1 pts]** Defina el tipo de datos ''Arg'' que representa a un argumento de función en el AST.
  - **[0.2 pts]** Implemente la función ''parse-arg'' que parsea un argumento de función.
  - **[0.1 pts]** Modifique la función ''parse-fundef'' para que utilice ''parse-arg'' para parsear los argumentos.

Además de lo anterior, observe que el nodo ''<binding>'' en el BNF cambió, y ahora puede incluir una anotación opcional de tipo para el identificador que se introduce.

  - **[0.1 pts]** Modifique el tipo de datos ''Binding'' para que pueda almacenar el tipo del identificador.
  - **[0.1 pts]** Modifique la función ''parse-binding'' para que acepte una anotación opcional de tipo. **Nota:** Cuando no se especifica el tipo, puede guardar el valor ''#f'' en el lugar donde se almacenaría el tipo.


===== Checkeo Estático de Tipos =====

Para poder realizar un checkeo de tipos estático, necesitaremos:
  - **[0.7 pts]** Implementar la función ''typecheck-expr :: Exp Env List[Fundef] -> Type or error'' que toma una expresión, un ambiente y una lista de definiciones de funciones, y retorna el tipo de la expresión o lanza un error.
  - **[0.4 pts]** Implementar ''typecheck-fundef :: Fundef List[Fundef] -> Type or error'' que recibe una definición de función y una lista de definiciones de funciones, y retorna el tipo de retorno de la función, o lanza un error.
  - **[0.2 pts]** Implementar ''typecheck :: Prog -> Type or error'' que toma un programa y nos retorna su tipo, o lanza un error.
  - **[0.1 pts]** Extender la función ''run'' para que verifique el tipo del programa (este paso puede fallar) antes de interpretarlo. Note que tendrá que hacer pequeñas modificaciones a la función ''interp'' para que pueda procesar el nuevo AST con anotaciones de tipo. Unicamente los casos para el ''with'' y aplicaciones de función se verán afectados.


**Observaciones importantes**:
  * 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).
  * 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.
  * Debe definir los tipos de los operadores primitivos de manera exacta, p.ej. ''%%<%%'' es una operación que toma dos ''Num'' y retorna ''Bool''. 
  * 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 ''%%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. El tipo resultante de una aplicación es el tipo de retorno de la función aplicada.

**Para los errores**:
  * Los errores de identificadores libres, funciones no definidas y errores de aridad deben ahora detectarse estáticamente. El formato de los mensajes de error es el mismo que se especificó en la parte 1.
  * 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 (parse-prog '{3}))
  (numT)  </code> <code scheme>
  > (typecheck (parse-prog '{{define {f {p : Bool}} {if p 23 42}}
                             {f {< 3 4}}}))
  (numT) </code> <code scheme>   
  > (typecheck (parse-prog '{{define {one {x : Num}} 1}
                             {one #t}}))
  "Static type error: expected Num found Bool" </code> <code scheme>
  > (typecheck (parse-prog  '{{< 10 #t}}))
  "Static type error: operator < expected Num found Bool"</code> <code scheme>
   > (typecheck (parse-prog '{{if 73 #t #t}}))
  "Static type error: expected Bool found Num"</code> <code scheme>
  > (typecheck (parse-prog '{{with {{x : Num 5}
                                    {y : Num #t}
                                    {z : Num 42}}
                                 z}}))
  "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?

El testing de esta parte recibe **0.5 pts**
----

===== Parte 3. Contratos en funciones de primer orden (1 pt. de bonus) =====

<note important>
Esta parte es de realización **opcional**. Si la desarrolla correctamente obtendrá un bono de **1 pt** que podrán agregar a la nota de cualquiera de las tareas. 
</note>

El propósito de esta parte es 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
<arg>    ::= {<id> : <type>}        ; como antes
           | {<id> : <type> @ <contract>}  ; lo único nuevo
</code>

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>
{{define {positive {x : Num}} : Bool {< 0 x}}
 {define {sub {x : Num @ positive} {y : Num}} : Num
           {- y x}}
 {sub 5 3}}
</code>
Donde el argumento ''x'' posee como contrato la función ''positive'', que comprueba en tiempo de ejecución que ''x'' sea mayor que 0.

  * Extienda nuevamente su función ''run'' para que verifique los contratos en tiempo de ejecución. 

**Observaciones importantes**:
  * 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, se debe lanzar un error con el siguiente patrón: <code scheme>
"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.
  * Una función usada como contrato **debe** aceptar un solo argumento de cualquier tipo válido y **debe** retornar un valor de tipo ''Bool''. Esta verificación debe realizarse estáticamente y, en caso de no cumplir dicha condición, se debe lanzar un error con el siguiente patrón: <code scheme>
"Static contract error: invalid type for <c>"
</code>  donde ''<c>'' es el nombre del contrato que no tipa.

Más ejemplos:
<code scheme>
{{define {positive {x : Num}} : Bool {< 0 x}}
 {define {negate {x : Num @ positive}} : Num {- 0 x}}
 {negate 23}}
</code>

<code scheme>
{{define {pair-non-zero? {p : {Pair Num Num}}} : Bool {&& {= 0 {fst p}} {= 0 {snd p}}}}
 {define {pair-div {p : {Pair Num Num} @ pair-non-zero?}} : Num {/ {fst x} {snd x}}}
 {+ {pair-div {cons 30 5}} {pair-div {cons 60 0}}}
}
"Runtime contract error: {cons 60 0} does not satisfy pair-non-zero?"
</code>


<code scheme>
> (run '{{define {add {x : Num} {y : Num}} : Num {+ x y}}
         {define {oh-no {x : Num @ add}} : Bool x}
         {oh-no 21 21}})
"Static contract error: invalid type for add"
</code>