Tarea 2

Esta tarea se distribuye con dos ficheros base.rkt y tests.rkt (base tarea 2). Considere las definiciones del archivo base.rkt y escriba sus funciones en él. Escriba sus tests en el archivo tests.rkt adjunto. Ambos ficheros deben ser entregados vía U-Cursos. Los tests forman parte de su evaluación! Consulte las normas de entrega de tareas en http://pleiad.cl/teaching/cc4101.

El objetivo de esta tarea es construir un lenguaje

• donde se puedan definir tipos inductivos propios (los únicos valores atómicos del lenguaje van a ser de algún tipo definido por el usuario), y
• que soporte funciones de primera clase de múltiples argumentos y anotaciones de tipo.

A continuación se presenta la gramática BNF del lenguaje y las especificaciones para los aspectos mas importantes del mismo.

<prog>    ::= (<def>* <expr>)
 
<def>     ::= (deftype <id> (<id> : <type>)+)
            | (def <id> (<id> : <type>)* : <type> <expr>)
 
<type>    ::= <id>
            | (<type>+ -> <type>)
 
<expr>    ::= <id>
            | (fun (<id> : <type>)+ <expr>)
            | (match <expr> (<case>+))
            | (<expr> <expr>+)
 
<case>    ::= (case <pattern> => <expr>)
 
<pattern> ::= <id>
             | (<id> <id>*)

Recuerde que para una cadena w, w+ representa una secuencia de al menos un w, mientras que w* representa una secuencia posiblemente vacía de w.

Un tipo de datos inductivo se define a través de una cláusula deftype, proveyendo el nombre del tipo y los constructores asociados.

Ejemplo 1. En el siguiente ejemplo el programador define los números naturales a través de un tipo inductivo nat y dos constructores O y S, que simbolizan el 0 y el sucesor de un natural, respectivamente.

(run '((deftype nat 
          (O : nat)
          (S : (nat -> nat)))
       (O)))
> "(O) : nat"            

Al ser aplicados, cada constructor genera estructuras de tipo nat. Puede representar sus estructuras como le parezca conveniente pero la función run siempre debe retornar un String con el tipo correspondiente como en los ejemplos.

Observe que existen dos tipos de constructores posibles: aquellos con argumentos y aquellos sin argumentos. En el ejemplo, O corresponde a un constructor que no requiere argumentos y construye un elemento de tipo nat; (O : nat) es azúcar sintáctico para una función de tipo () → nat. El constructor S usa, en cambio, un elemento de tipo nat para construir otro elemento de tipo nat.

Ejemplo 2. El tipo expr definido abajo posee dos constructores, num y add, cada uno de los cuales utiliza dos argumentos de tipo expr para construir otro valor de tipo expr.

(run '((deftype nat 
               (O : nat)
               (S : (nat -> nat)))
             (deftype expr 
               (num : (nat -> expr))
               (add : (expr expr -> expr)))   
             (add (num (S (O))) (num (O)))))
> "(add (num (S (O))) (num (O))) : expr"

Para la resolución de la tarea podemos asumir que nunca se van a proveer dos definiciones distintas para un mismo tipo inductivo.

Asociar una función a un nombre se realiza usando def, donde las funciones tienen anotación de tipo para sus argumentos y retorno. Como ejemplo, en el caso de pred la función utiliza pattern matching para retornar su resultado, en ese caso se espera que primero se interprete el elemento sobre el cual matchear, n, para luego ir comprobando uno a uno con que patrón coincide. Si en un case el patrón incluye un identificador libre, este funciona como un binding para el cuerpo del caso (ejemplo (case (S n1) ⇒ n1))

(run '((deftype nat
          (O : nat)
          (S : (nat -> nat)))
       (def pred (n : nat) : nat
               (match n
                 ((case (O) => (O))
                  (case (S n1) => n1))))
       (pred (S (O)))))
> "(O) : nat"            

En caso de no encontrar un case que corresponda:

(test/exn 
 (run '((deftype bool 
          (t : bool)
          (f : bool))
       (def not (b : bool) : bool
                (match b
                 ((case (t) => (f)))))
       (not {f)))
   "match error")

De todas formas un identificador puede servir para hacer match de los casos restantes:

(run '((deftype day 
         (monday : day)
         (tuesday : day)
         (wednesday : day)
         (thursday : day)
         (friday : day)
         (saturday : day)
         (sunday : day))
       (deftype bool
         (t : bool)
         (f : bool))
       (def weekday (d : day) : bool
         (match d
           ((case (saturday) => (f))
            (case (sunday) => (f))
            (case otherday => (t)))))
       (weekday (monday))))
> "(t) : bool"         

Funciones definidas con def pueden ser recursivas y tener más de un argumento.

(run '((deftype bool 
          (t : bool)
          (f : bool))
       (deftype nat 
          (O : nat)
          (S : (nat -> nat)))
       (def not (b : bool) : bool
                (match b
                 ((case (t) => (f))
                  (case (f) => (t)))))
       (def even (n : nat) (b : bool) : bool 
               (match n
                 ((case (O) => b)
                  (case (S n1) => (even n1 (not b))))))
       (even (S (S (S (O)))) (t))))
> "(f) : bool"

Las funciones se representan por el simbolo lambda:

(run '((deftype bool 
          (t : bool)
          (f : bool))
       (fun (x : bool) x)))
> "λ"

Con esto en mente, se pide que:

Defina el AST para soportar programas del lenguaje. Note que un programa es una lista de definiciones seguida de una expresión. Dos tipos de definiciones son posibles deftype y def.

Defina la función parser :: s-expr -> Expr que parsea el lenguaje.

Defina la función interp :: Expr x Env -> Val que evalua un programa con semántica eager.

Defina la función run :: s-expr -> String que toma un programa fuente y retorna la representación en String del valor resultante de la interpretación con su tipo anotado. Es recomendable definir una función auxiliar que le permita pasar de su representación de estructuras a la notación de los ejemplos con Strings.

Nota: Observe que la definición de funciones con def permite múltiples argumentos y por tanto el constructor de tipos → recibe una lista de tipos en la entrada. Puede asumir que para toda la tarea nunca se van a entregar dos argumentos con el mismo nombre.

(terminate '{{deftype bool 
                {t : bool}
                {f : bool}}
             {deftype nat 
                {O : nat}
                {S : {nat -> nat}}}
             {def even {n : nat} : bool 
                    {match n
                      {{case {O} => {t}}
                       {case {S n1} => {match n1
                                         {{case {O} => {f}}
                                          {case {S n2} => {even n2}}}}}}}}
             {even {S {S {O}}}}})
> "terminate"