This commit is contained in:
2025-11-17 17:02:18 +01:00
parent 9bdbe830d2
commit 2e6172c115
3 changed files with 53 additions and 7 deletions

25
3/Assignment.hs Normal file
View File

@ -0,0 +1,25 @@
{-# Language LambdaCase #-}
module Assignment where
import Chi
subst :: Variable -> Exp -> Exp -> Exp
subst var e = \case
Apply e1 e2 -> Apply (subst var e e1) (subst var e e2)
Lambda x e' -> Lambda x $ if var /= x then (subst var e e') else e'
Var x -> if var == x then e else Var x
Const c es -> Const c $ map (subst var e) es
Rec x e' -> Rec x $ if var /= x then (subst var e e') else e'
Case e' branches -> Case (subst var e e') $ map substBr branches
where
substBr :: Br -> Br
substBr (Branch c vs e') = Branch c vs $ if var `notElem` vs then (subst var e e') else e'
eval' :: Exp -> Reader (Map Variable Exp) Exp
eval' = undefined
eval :: Exp -> Exp
eval = undefined
main :: IO ()
main = getLine >>= print . eval . parse

View File

@ -3,10 +3,8 @@
#+latex_header: \usepackage{parskip} #+latex_header: \usepackage{parskip}
* Supporting files * Supporting files
This time you can make use of a [[http://bnfc.digitalgrammars.com/][BNFC]] specification ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) of a variant of the concrete syntax of $\chi$. This grammar gives specific rules for variable and constructor names, and differs from the concrete syntax presented in the lectures in some ways:
~This~ time you can make use of a [[http://bnfc.digitalgrammars.com/][BNFC]] specification ([[https://chalmers.instructure.com/courses/36941/file_contents/course%20files/chi/Chi.cf][~Chi.cf~]]) of a variant of the concrete syntax of $\chi$. This grammar gives specific rules for variable and constructor names, and differs from the concrete syntax presented in the lectures in some ways: - Variables and constructors are sequences of letters (~a~ to ~z~ and ~A~ to ~Z~), digits (~0~ to ~9~), underscores (~_~), dashes (~-~) and primes (='=), and variables have to start with lower-case letters or underscores, whereas constructors have to start with upper-case letters.
# TODO: Fix '
- Variables and constructors are sequences of letters (~a~ to ~z~ and ~A~ to ~Z~), digits (~0~ to ~9~), underscores (~_~), dashes (~-~) and primes ('), and variables have to start with lower-case letters or underscores, whereas constructors have to start with upper-case letters.
- Lambdas are written using backslash characters (~\~) and arrows are written using the string ~->~. - Lambdas are written using backslash characters (~\~) and arrows are written using the string ~->~.
- End-of-line comments of the form ~-- ...~ are allowed, as are (non-nested) comments of the form ~{- ... -}~. - End-of-line comments of the form ~-- ...~ are allowed, as are (non-nested) comments of the form ~{- ... -}~.
- There can be a final comma after a non-empty list of constructor arguments, and there can be a final semicolon after a non-empty list of branches. - There can be a final comma after a non-empty list of constructor arguments, and there can be a final semicolon after a non-empty list of branches.
@ -61,10 +59,14 @@ Consider the $\chi$ term /t/ with concrete syntax $C (\lambda z.z)$:
In the abstract syntax the constructor ~C~ should be represented by $\underline{C} \in \text{Const}$, and the variable ~z~ by $\underline{z} \in \text{Var}$. When giving the $\chi$ representation of the term you should use (the representation of) the number 0 to represent $\underline{C}$, and 1 to represent $\underline{z}$. In the abstract syntax the constructor ~C~ should be represented by $\underline{C} \in \text{Const}$, and the variable ~z~ by $\underline{z} \in \text{Var}$. When giving the $\chi$ representation of the term you should use (the representation of) the number 0 to represent $\underline{C}$, and 1 to represent $\underline{z}$.
*** Answer *** Answer
The abstract syntax is the following: $\text{const}\ \underline{C}\ (\text{cons}\ (\text{lambda}\ \underline{z}\ (\text{var}\ \underline{z}))\ \text{nil})$. The abstract syntax is the following:
\[ \text{const}\ \underline{C}\ (\text{cons}\ (\text{lambda}\ \underline{z}\ (\text{var}\ \underline{z}))\ \text{nil}) \]
The concrete syntax of the standard representation is the following: $Const(\ulcorner \underline{C} \urcorner, Cons(Lambda(\ulcorner \underline{z} \urcorner, Cons (Var(\ulcorner \underline{z} \urcorner), Nil())), Nil())$ The concrete syntax of the standard representation is the following:
# TODO: check parenthesis above \[ \text{Const}(\ulcorner \underline{C} \urcorner, \text{Cons}(\text{Lambda}(\ulcorner \underline{z} \urcorner, \text{Cons} (\text{Var}(\ulcorner \underline{z} \urcorner), \text{Nil}())), \text{Nil}())) \]
The abstract syntax of the standard representation, given that $\underline{z}$ and $\underline{C}$ corresponds to zero:
\[ \text{Const}(\text{Zero}(), \text{Cons}(\text{Lambda}(\text{Zero}(), \text{Cons} (\text{Var}(\text{Zero}()), \text{Nil}())), \text{Nil}())) \]
** (2p) [BN] ** (2p) [BN]
@ -82,6 +84,7 @@ Test your implementation. Here are some test cases that must work:
| ~z~ | $C(\lambda z . z)$ | $\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$ | $\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$ | | ~z~ | $C(\lambda z . z)$ | $\text{case}\ z\ \text{of}\ \{ C(z) \rightarrow z \}$ | $\text{case}\ C(\lambda z. z) \ \text{of}\ \{ C(z) \rightarrow z \}$ |
*** Answer *** Answer
See Assignment.hs
** (1p) ** (1p)
Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ specification. Implement multiplication of natural numbers in $\chi$, using the representation of natural numbers given in the $\chi$ specification.
@ -89,6 +92,19 @@ Implement multiplication of natural numbers in $\chi$, using the representation
Hint: If you want to make use of addition in the implementation of multiplication, then you can define multiplication using a free variable ~add~, and use the substitution operation from the previous exercise to substitute a complete (closed) implementation of addition for this variable. Hint: If you want to make use of addition in the implementation of multiplication, then you can define multiplication using a free variable ~add~, and use the substitution operation from the previous exercise to substitute a complete (closed) implementation of addition for this variable.
*** Answer *** Answer
#+begin_src chi
\m. rec mult = \n. case n of
{ Zero() -> Zero()
; Succ(n) -> add m (mult n)
}
#+end_src
where we substitute ~add~ for the following:
#+begin_src chi
\m. rec add = \n. case n of
{ Zero() -> m
; Succ(n) -> Suc(add n)
}
#+end_src
** (2p) [BN] ** (2p) [BN]
Implement an interpreter for $\chi$. The interpreter should be a partial function from closed terms to values, and should implement the operational semantics of $\chi$. Implement an interpreter for $\chi$. The interpreter should be a partial function from closed terms to values, and should implement the operational semantics of $\chi$.

View File

@ -26,3 +26,8 @@ library
PrintChi PrintChi
hs-source-dirs: hs-source-dirs:
. .
executable interpreter
main-is: Assignment.hs
build-depends: base
, chi