CS代考 COMP3161/9164 23T3 Assignment 1

COMP3161/9164 23T3 Assignment 1
Version 1.0.5 Marks : 17.5% of the mark for the course.
Due date: Thursday, 2nd of November 2023, 23:59:59 Sydney time Overview
In this assignment you will implement an interpreter for MinHs, a small functional language similar to ML and Haskell. It is fully typed, with types specified by the programmer.

Copyright By PowCoder代写 加微信 powcoder

However, we will not evaluate MinHS directly; instead, we’ll first compile it to an intermediate language we call hindsight. In hindsight we use neither call-by- value nor a call-by-name evaluation, but call-by-push-value. This means the program- mer gets to decide the evaluation order herself with explicit operators to steer the con- trol flow. Once we have implemented an evaluator for hindsight, we can then give MinHS either a call-by-value or a call-by-name evaluator, by going to hindsight via different compilation strategies.
The assignment consists of a base compulsory component, worth 70%, and four additional components which collectively are worth 50%, meaning that not all must be completed to earn full marks.
Your total mark can go up to 120%. Any marks above 100% will be converted to bonus exam marks, at a 20-to-3 exchange rate. For example, earning 110% on the assignment will yield 1.5 bonus marks on the final exam.
• Task 1 (70%)
Implement an interpreter for hindsight, using an environment semantics, in- cluding support for recursion and closures.
• Task 2 (10%)
Extend the interpreter to support partially applied primops.
• Task 3 (10%)
Extend the interpreter to support multiple bindings in the one let form.
• Task 4 (10%)
Implement an optimisation pass for hindsight.
• Task 5 (20%)
Implement a call-by-name compiler from MinHS to hindsight.

The front end of the interpreter (lexer, parser, type checker) is provided for you, along with the type of the evaluate function (found in the file hindsight/Evaluator.hs) and an implementation stub. The function evaluate returns an object of type Value. You may modify the constructors for Value if you wish, but not the type for evaluate. The return value of evaluate is used to check the correctness of your assignment.
You must provide an implementation of evaluate, in hindsight/Evaluator.hs. It is this file you will submit for Task 1. The only other files that can be modified are hindsight/Optimiser.hs (for Task 4) and hindsight/CBNCompile.hs (for Task 5)
You can assume the typechecker has done its job and will only give you type- correct programs to evaluate. The type checker will, in general, rule out type-incorrect programs, so the interpreter does not have to consider them.
Please use the Ed forum for questions about this assignment. Submission
Submit your (modified) hindsight/Evaluator.hs, hindsight/Optimiser.hs and hindsight/CBNCompile.hs using the CSE give system, by typing the com- mand
give cs3161 Eval Evaluator.hs Optimiser.hs CBNCompile.hs
or by using the CSE give web interface. Note that Optimiser.hs and CBNCompile.hs are optional, and should only be included if you completed the corresponding bonus tasks.
1 Primer on call-by-push-value
As mentioned, hindsight is a call-by-push-value language. The core of the lan- guage is similar to MinHS as seen in the lectures. This section will describe some of the key differences.
Following the call-by-push-value paradigm, hindsight distinguishes between two kinds of expressions: value expressions, ranged over by v, and computation ex- pressions, ranged over by c. A value expression denotes a value, and a computation expression denotes a process that might produce a value if we run it.
Computations can be suspended using the thunk operator, and suspended com- putations can be passed around as value expressions, and later resumed using force. Here’s an example program:
main :: F Bool
= let y :: U(F Bool) = thunk(1 == 2);
reduce 1 < 2 then produce True else force y The type annotation main :: F Bool means that main is a computation which produces a boolean result. The U in y :: U(F Bool) means that y is a suspended computation which, if resumed, would produce a boolean result. reduce 1 < 2 to x means that the computation 1 < 2 is evaluated, producing a value which is saved in the local binding x. If the True branch is chosen, we’ll run the trivial computation produce True which immediately produces a value True. Otherwise, we’ll resume the suspended computation from before. Thus, in this case the equality comparison 1 == 2 is never evaluated. If we want the equality comparison to be evaluated first (despite the fact that we don’t need its result), we can refrain from suspending it: main :: F Bool = reduce 1 == 2 reduce 1 < 2 then produce True else produce y This is the core part of the assignment. You are to implement an interpreter for hindsight. The following expressions must be handled: • variables. x,y,z • integerconstants.1,2,.. • boolean constants. True, False • someprimitivearithmeticandbooleanoperations.+,∗,<,<=,.. • constructors for lists. Nil, Cons • destructors for lists. head, tail • inspectors for lists. null • function application. f x • ifvthenc1 elsec2 • suspending computations. thunk c • resuming suspended computations. force v • letx::τx =v;ine • reducec1 toxinc2 • produce v • recfun f :: (τ1 → τ2) x = c expressions These cases are explained in detail below. The abstract syntax defining these syn- tactic entities is in hindsight/Syntax.hs, which inherits some definitions from MinHS/Syntax.hs You should understand the data types VExp, CExp, CBind and VBind well. Your implementation is to follow the dynamic semantics described in this docu- ment. You are not to use substitution as the evaluation strategy, but must use an envi- ronment/heap semantics. If a runtime error occurs, which is possible, you should use Haskell’s error :: String → a function to emit a suitable error message (the error code returned by error is non-zero, which is what will be checked for – the actual error message is not important). 2.1 Program structure A program in hindsight may evaluate to either an integer, a list of integers, or a boolean, depending on the type assigned to the main function. The main function is always defined (this is checked by the implementation). You need only consider the case of a single top-level binding for main, as e.g. here: main :: F Int = 1 + 2 2.2 Variables, Literals and Constants hindsight is a spartan language. We have to consider the following six forms of types: The first four are value types, and the latter two are computation types. We use vt to denote value types and ct to denote computation types. The only literals you will encounter are integers. The only non-literal constructors are True and False for the Bool type, and Nil and Cons for the [Int] type. 2.3 Function application A function in hindsight accepts exactly one argument, which must be a value. The body of the function must be a computation. Inside the body of a recursive function f :: vt − > ct, any recursive references to f are considered suspended; that is, they areregardedashavingtypef ::U(vt−>ct).
The result of a function application may in turn be a function.
2.4 Primitive operations
You need to implement the following primitive operations:
+ :: Int -> Int -> F Int
– :: Int -> Int -> F Int

:: Int -> Int -> F Int
/ ::Int->Int-> % ::Int->Int->
negate :: Int -> F Int
> ::Int->Int-> >= ::Int->Int-> < ::Int->Int-> <= ::Int->Int->
== ::Int->Int-> /= ::Int->Int->
head :: [Int] -> F Int
tail :: [Int] -> F [Int]
null :: [Int] -> F Bool
F Int F Int
F Bool F Bool
These operations are defined over Int s, [I nt]s, and Bool s, as usual.
primop representation of the unary negation function, i.e. -1. The abstract syntax for primops is inherited from MinHS/Syntax.hs.
2.5 if- then- else
hindsight has an if v then c1 else c2 construct. The types of c1 and c2 are the
same. The type of v is Bool . 2.6 let
For the first task you only need to handle simple let s of the kind we have discussed in the lectures. Like these:
main :: F Int
x :: Int = 3;
in produce x
main :: F Int
= let f :: U (Int -> F Int)
= thunk (recfun f :: (Int -> F Int) x = x + x);
in force f 3
For the base component of the assignment, you do not need to handle let bindings of more than one variable at a time (as is possible in Haskell). Remember, a let may bind a (suspended) recursive function defined with recfun.
2.7 force and thunk
thunk c is a value expression called a thunk or a suspended computation. A sustained
computation can be evaluated later by applying force to it. 5

2.8 reduce
reduce c1 to x in c2 is a computation which first executes c1 until a value is pro- duced. This value is then bound to x before evaluation c2. It is similar to let, but instead of binding a value expression to a name, it binds the value produced by a com- putation expression to a name.
2.9 recfun
The recfun expression introduces a new, named function computation. It has the
(recfun f :: (Int -> F Int) x = x + x)
Unlike in Haskell (and MinHS), a recfun is not a value, but a computation. It can be bound in let expressions if suspended. The value ‘f’ is bound in the body of the function, so it is possible to write recursive functions:
recfun f :: (Int -> F Int) x =
reduce x < 10 if b then force f (x+1) else produce x Note that inside the body of ‘f’, ‘f’ is considered suspended, hence force must be used to explicitly resume recursive calls. Be very careful when implementing this construct, as there can be problems when using environments in a language allowing functions to be returned by functions. 2.10 Evaluation strategy We have seen in the tutorials how it is possible to evaluate expressions via substitution. This is an extremely inefficient way to run a program. In this assignment you are to use an environment instead. You will be penalised for an interpreter that operates via substitution. The module MinHS/Env.hs provides a data type suitable for most uses. Consult the lecture notes on how environments are to be used in dynamic semantics. The strategy is to bind variables to values in the environment, and look them up when requried. In general, you will need to use: empty, lookup, add and addAll to begin with an empty environment, lookup the environment, or to add binding(s) to the environment, respectively. As these functions clash with functions in the Prelude, a good idea is to import the module Env qualified: import qualified Env This makes the functions accessible as Env.empty and Env.lookup, to disambiguate from the Prelude versions. 3 Dynamic Semantics of hindsight Big-step semantics We define two mutually recursive judgements, both named ⇓. The first relates an envi- ronment mapping variables to values Γ and a value expression v to the resultant value of that expression V . The second maps the same kind of environment Γ and a compu- tation expression e to a terminal computation T . Our value set for V will, to start with, consist of: • Machine integers • Boolean values • Lists of integers Our terminal computations T consist of: • P V , which denotes a trivial computation that immediately produces the value We will use t to range over terminal computations, and v to denote values. Note that v can also denote value expressions; it should be clear from context which one is intended. We will also need to add closures or function terminals to our terminal computation set, to deal with the recfun construct in a sound way, and a constructor for thunk values to our value set to deal with thunk. There are some design decisions to be made here, and they’re up to you. Environment The environment Γ maps variables to values, and is used in place of substitution. It is specified as follows: Γ::= ·|Γ,x=v Values bound in the environment are closed – they contain no free variables. This requirement creates a problem with thunk values created with thunk whose bodies contain variables bound in an outer scope. We must bundle them with their associ- ated environment. The same problem will also arise for computations created with recfun, and requires introducing closures. Care must also be taken to support sus- pended functions in thunk values. Constants and Boolean Constructors Γ⊢Numn⇓n Γ⊢ConTrue⇓True Γ⊢ConFalse⇓False Primitive operations Γ⊢v1 ⇓v1′ Γ⊢v2 ⇓v2′ Γ⊢Addv1 v2 ⇓P(v1′ +v2′) Similarly for the other arithmetic and comparison operations (as for the language of arithmetic expressions) Note that division by zero should cause your interpreter to throw an error using Haskell’s error function. The abstract syntax of the interpreter re-uses function application to represent ap- plication of primitive operations, so Add e1 e2 is actually represented as: App (App ( e1) e2) For this first part of the assignment, you may assume that primops are never partially applied — that is, they are fully saturated with arguments, so the term App ( e1) will never occur in isolation. Evaluation of if -expression List constructors and primops Γ⊢v⇓True Γ⊢c1 ⇓t Γ⊢Ifvc1 c2 ⇓t Γ⊢v⇓False Γ⊢c2 ⇓t Γ⊢Ifvc1 c2 ⇓t Γ ⊢ Var x ⇓ v Γ ⊢ x ⇓ vx Γ⊢ConNil⇓[] Γ⊢(force (Con Cons))xxs⇓P(vx :vxs) Γ ⊢ x ⇓ v : vs Γ ⊢ x ⇓ v : vs Γ ⊢ x ⇓ v : vs Γ⊢headx⇓P(v) Γ⊢tailx⇓P(vs) Γ⊢nullx⇓P(False) Γ ⊢ x ⇓ [] Γ ⊢ x ⇓ [] Γ ⊢ x ⇓ [] Γ⊢headx⇓error Γ⊢tailx⇓error Γ⊢nullx⇓P(True) Γ ⊢ xs ⇓ vxs For the first part of the assignment, you may assume that Cons is also never partially applied, as with primops. Γ⊢v1 ⇓v2 Γ⊢Producev1 ⇓P(v2) Variable Bindings with Let and Reduce Thunk values Γ⊢v1 ⇓v2 Γ,x=v2 ⊢c⇓t Γ⊢Letv1 (x.c)⇓t Γ⊢c1⇓P(v) Γ,x=v⊢c2⇓t Γ ⊢ Reduce c1 (x.c2) ⇓ t To maintain soundness with thunk values, we need to pair a function with its environ- ment, forming a closure. We introduce the following syntax for thunk values: You will need to decide on a suitable representation of thunk values as a Haskell data type. Also consider how you will represent suspended functions — can you reuse your existing representation, or do you need something different? Thunk and Force semantics Now we can give the semantics of suspending and resuming computations: Γ⊢v⇓⟨⟨Γ′;c⟩⟩ Γ′⊢c⇓t Γ ⊢ Thunk c ⇓ ⟨⟨Γ; c⟩⟩ Γ ⊢ Force v ⇓ t Function terminals For similar reasons, unapplied functions can be regarded as terminal computations, and you need to keep track of the environment in which they’ve been defined. We can reuse a similar representation: ⟨⟨Γ; Recfun τ1 τ2 f.x.e⟩⟩ The types are not needed at runtime, but included here for completeness. You will need to decide on a suitable representation of function terminals. Now we can specify how to introduce closed function terminals: Γ ⊢ Recfun τ1 τ2 f.x.e1 ⇓ ⟨⟨Γ; Recfun τ1 τ2 f.x.e1⟩⟩ 9 Function Application Γ ⊢ c1 ⇓ t1 t1 = ⟨⟨Γ′;Recfun τ1 τ2 f.x.cf⟩⟩ Γ⊢v1 ⇓v2 Γ′,f=t1,x=v2 ⊢cf ⇓t2 Γ⊢Appc1 v1 ⇓t2 This rule involves some notational abuse: t1 is a terminal, not a value. But we need to put it in the environment. Do you need to extend your value type to accommodate this? 4 Additional Tasks In order to get full marks in the assignment, you must do some of the following five tasks: 4.1 Task 2: Partial Primops (10%) In the base part of the assignment, you are allowed to assume that all primitive op- erations (and the constructor Cons) are fully saturated with arguments. In this task you are to implement partial application of primitive operations (and Cons), which removes this assumption. For example: main :: F Int = let inc :: U (Int -> F Int) = thunk ((+) 1);
in force inc 2 — returns 3
Note that the expression (+) 1 partially applies the primop Add to 1, returning a function from Int to Int.
You will need to develop a suitable dynamic semantics for such expressions and implement it in your evaluator. The parser and type checker are already capable of dealing with expressions of this form.
4.2 Task 3: Multiple bindings in let (10%)
In the base part of the assignment, we specify that let expressions contain only one binding. In this task, you are to extend the interpreter to let expressions with multiple bindings, like:
main :: F Int
= let a :: Int = 3;
b :: Int = 2;
These are evaluated the same way as multiple nested let expressions:
main :: F Int
= let a :: Int = 3;
in let b :: Int = 2;
Once again the only place where extensions need to be made are in the evaluator, as the type checker and parser are already capable of handling multiple let bindings.

4.3 Task 4: Code optimisation (10%)
In hindsight/Optimiser.hs you’ll find the skeleton for an optimisation pass, which we can think of as a compiler from hindsight to hindsight. Here, you can implement a code optimiser to eliminate certain redundant patterns. The main purpose of this phase is to get simpler, cleaner code after compiling from MinhS. You need to optimise away at least the following patterns:
Pattern to optimise
force (thunk v)
reduce produce v to x in c (recfunf::(τ1 →τ2)x=c)v
Desired result
c[x:=v] iff∈/FV(c)
You can do more optimisations if you want to; it shouldn’t influence your marks, since the marking makes no attempt to measure code quality. But make sure your opti- miser output is semantically equivalent to the input program, and contains no instances of the above three patterns.
Your optimiser must terminate for all input programs. Hence, your optimiser can’t be an evaluator, and you probably never want to unfold or inline functions that feature recursive calls.
The optimiser is the only place in the assignment where you can and should use substitution.
The optimiser is not invoked by default, but can be invoked stand-alone using minhs with –dump optimiser foo.hst, or executed after compilation from MinHSbyusing–dump compiler –optimise foo.mhs
4.4 Task 5: A call-by-name translation from MinHS (20%)
The main purpose of hindsight is to serve as an intermediate representation of MinHS programs, as part of a compiler or (in this case) interpreter. This requires a compiler from MinHS to hindsight. By choosing different compilation strategies, we can execute MinHS with either call-by-name semantics or call-by-value semantics.
In hindsight/CBVCompile.hs you’ll find a call-by-value compiler already implemented.
This task is to develop a call-by-name compiler in hindsight/CBNCompile.hs
The reference we used when implementing the call-by-value compiler was the translation from call-by-value λ-calculus to CBPV from ’s PhD thesis [3, Fig- ure 3.5]. The thesis also includes a translation from call-by-name λ-calculus [3, Fig- ure 3.6], which you should consult for inspiration. Not every MinHS primitive has a direct λ-calculus equivalent though, so there are some gaps you need to figure out how to bridge. Also, beware of idiosynchrasies in Levy’s notation.1
It is occasionally necessary for the compiler to invent new names. Obviously, these names should not clash with names occuring in the source program. Make sure you have a strategy for dealing with this. The CBV compiler solves this problem by pre- fixing an underscore to all names the programmer wrote, meaning there’s no risk of clashes so long as we don’t invent names starting in underscores.
The call-by-name compiler can be invoked stand-alone by using minhs like this (assuming you’re on stack):
stack exec minhs-1 — –dump compiler –cbn foo.mhs
1 For example, Levy writes function application as x ‘ f instead of f x 11

To immediately run your hindsight evaluator after CBN compilation, use –cbn foo.hst. Note that evaluation may fail on correct programs, unless you’ve imple- mented extension tasks 1 and 2.
There are ple

程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com