Implement a type checker for the simple programming language with variability presented in the file VariabilityTypeChecker.scala. The file Expression.scala contains implementations of the programming language constructs and types. The file TypeChecking.scala contains the general interface for the type checkers. In addition, we provide an implementation of the type context for task a). This class is also reused for task b) for which we also provide an implementation of the variability context. The project skeleton also contains documentation for all provided classes and functions. You are not allowed to modify these provided classes and functions. The locations where you should add your implementation are marked with a TODO. We also provide some basic tests which can be found in the folder tests. The file build.sbt and the files in the folder project contain a build script that we use to build your submission and run the tests.2 You must not edit these files. The build script should also enable you to import the project skeleton into any IDE with Scala support (e.g., IntelliJ with the Scala plugin). Scala can be quite sensitive regarding the used language version and things might break if you use the wrong one. For the assignment, we use Scala 3.2.1 which is also specified in the build script. You can also run the tests included with the project skeleton using the build script. To run all tests execute the command sbt test. Type Checker Result The type checker result is represented by the interface TypeCheckResult and its implemen- tations Success and Failure. In the case of a successful type check an instance of Success has to be returned with the inferred type as its parameter. If the type checker detects a type error, it has to return an instance of Failure with the (sub-) expression that is currently checked, the context object, and an optional message describing the type error as parameters. This information is used by our tests to determine whether your implementation detected the error correctly. The message is not checked in the tests but can help you during debugging. Note for advanced users: The result type supports monad operations meaning it can be used in for-comprehensions.3 SAT Solver For some type rules of task b), you will need a SAT solver to check certain preconditions. For this assignment, we use CafeSAT4 which is a simple SAT solver implemented in Scala. The project skeleton already imports all the relevant packages. Checking whether a formula is satisfiable is as simple as this (assuming a, b, c are formulas): Solver.solveForSatisfiability((!a || b) && c) match { case None => print("Not satisfiable"); case Some(_) => print("Satisfiable") } Note how you can use !, ||, and && for not, or, and and. The API does not support implication so you have to encode implication using the other operators. The primitives true and false are available as Formulas.True and Formulas.False. Mind the prepended Formulas as, otherwise, you might confuse them with the True and False literals from our programming language! Below are the scala code for the given classes: 1-Expression.scala :

import cafesat.api.Formulas.Formula import cafesat.api.{Formulas, Solver} import scala.language.implicitConversions /** Constants  */ enum Constant: case True case False case Num(value: Int) /** Identifiers  */ case class Identifier(name: String) { override def toString: String = name }  enum Type: case NumTy case BoolTy  enum VExpression { case Const(c: Constant) case Id(id: Identifier) case Smaller(lhs: VExpression, rhs: VExpression) case If(condition: VExpression, thenExpr: VExpression, elseExpr: VExpression) case Let(variable: Identifier, varValue: VExpression, inExpr: VExpression) case Choice( presenceCondition: Formula, trueChoice: VExpression, falseChoice: VExpression ) def _lt(expression: VExpression): Smaller = Smaller(this, expression) }  class VType(val types: Map[Type, Formula] = Map()) {   def dom(): Set[Type] = types.keys.toSet   def formulaForType(t: Type): Option[Formula] = types.get(t) override def toString: String = { types.toSeq .map({ case (t: Type, pc: Formula) => s"($t => $pc)" }) .mkString(" ") }   override def equals(obj: Any): Boolean = { obj match { case typeB: VType => if (dom() == typeB.dom()) { dom().forall(t => { val formulaA = formulaForType(t).get val formulaB = typeB.formulaForType(t).get Solver.solveForSatisfiability(!(formulaA iff formulaB)) match { case Some(_) => false case None => true } }) } else { false } case _ => false } } }  object VType { def apply(elems: (Type, Formula)*): VType = new VType(Map.from(elems)) } object VExpression { given intToConst: Conversion[Int, Constant] = Constant.Num(_) given constantToExpr: Conversion[Constant, VExpression] = VExpression.Const(_) given intToExpr: Conversion[Int, VExpression] = VExpression.Const(_) given stringToIdentifier: Conversion[String, Identifier] = Identifier(_) given identifierToExpr: Conversion[Identifier, VExpression] = VExpression.Id(_) given stringToExpr: Conversion[String, VExpression] = VExpression.Id(_) def _if(cond: VExpression): VIfThen = VIfThen(cond) def _let(varName: Identifier): VLetIs = VLetIs(varName) } case class VIfThen(cond: VExpression) { def _then(expr: VExpression): VIfElse = VIfElse(cond, expr) } case class VIfElse(cond: VExpression, thenExpr: VExpression) { def _else(expr: VExpression): VExpression.If = VExpression.If(cond, thenExpr, expr) } case class VLetIs(varName: Identifier) { def _is(expr: VExpression): VLetIn = VLetIn(varName, expr) } case class VLetIn(varName: Identifier, varExpr: VExpression) { def _in(expr: VExpression): VExpression.Let = VExpression.Let(varName, varExpr, expr) } 2-TypeChecking.scala: 

import Constant.* import Expression.* import Type.* import cafesat.api.Formulas.Formula import cafesat.api.{Formulas, Solver}  sealed abstract class TypeCheckResult[ExpressionT, TypeT, ContextT] { def pure(t: TypeT): TypeCheckResult[ExpressionT, TypeT, ContextT] = Success(t) def flatMap( fn: TypeT => TypeCheckResult[ExpressionT, TypeT, ContextT] ): TypeCheckResult[ExpressionT, TypeT, ContextT] = this match { case Success(vtype) => fn(vtype) case f: Failure[ExpressionT, TypeT, ContextT] => f } def map( fn: TypeT => TypeT ): TypeCheckResult[ExpressionT, TypeT, ContextT] = flatMap(fn.andThen(pure)) }  case class Success[ExpressionT, TypeT, ContextT](t: TypeT) extends TypeCheckResult[ExpressionT, TypeT, ContextT]  case class Failure[ExpressionT, TypeT, ContextT]( expr: ExpressionT, context: ContextT, message: String = "" ) extends TypeCheckResult[ExpressionT, TypeT, ContextT] { override def toString: String = { s"Error @ $expr " + (message match { case "" => "" case m => s" Message: $m " }) + s" Context: $context" }   override def equals(obj: Any): Boolean = { obj match { case errorB: Failure[_, _, _] => expr == errorB.expr && context == errorB.context case _ => false } } } trait TypeChecker[ExpressionT, TypeT, ContextT] {   def checkType( expr: ExpressionT, context: ContextT ): TypeCheckResult[ExpressionT, TypeT, ContextT] } 3-VariablityTypeChecker: 

/** Type checking with variability.  */ package de.uni_saarland.cs.se import Constant.* import Type.* import VExpression.* import cafesat.api.Formulas.Formula import cafesat.api.{Formulas, Solver} /** Variability context as in lecture slides 74.  */ case class VariabilityContext(formula: Formula) { /** Make equality consider logical equality of formulas.  */  override def equals(obj: Any): Boolean = { obj match { case other: VariabilityContext => Solver.solveForSatisfiability(!(formula iff other.formula)) match { case Some(_) => false case None => true } case _ => false } } override def toString: String = formula.toString } object VariabilityContext {  def emptyContext(): VariabilityContext = new VariabilityContext(Formulas.True)   given formulaToVarCtx: Conversion[Formula, VariabilityContext] = VariabilityContext(_) }  type VTypeContext = TypeContext[Identifier, VType]  type VContext = (VariabilityContext, VTypeContext)  type VResult = TypeCheckResult[VExpression, VType, VContext] object VariabilityTypeChecker {   def checkType( expr: VExpression, context: VContext = createContext() ): VResult = { new VariabilityTypeChecker().checkType(expr, context) }   def createContext( variabilityContext: VariabilityContext = VariabilityContext.emptyContext(), typeContext: VTypeContext = TypeContext() ): VContext = (variabilityContext, typeContext) }   class VariabilityTypeChecker extends TypeChecker[VExpression, VType, VContext] { override def checkType(expr: VExpression, context: VContext): VResult = { // TODO: implement task b) ,I did just a part of it, continue the rest till it passes all unit tests provided at the end  expr match { case Const(c) => c match { case Num(_) => Success(VType(NumTy -> Formulas.True)) case True => Success(VType(BoolTy -> Formulas.True)) case False => Success(VType(BoolTy -> Formulas.True)) } case Id(id) => context._2.typeForVar(id) match { case Some(t) => Success(t) case None => Failure(expr,context,s"Identifier $id not found in type context.") } case Smaller(lhs, rhs) => checkType(lhs, context).flatMap { case VType(NumTy -> pc) => checkType(rhs, context).flatMap { case VType(NumTy -> pc2) => Solver.solveForSatisfiability(pc && pc2) match { case Some(_) => Success(VType(Map(BoolTy -> (pc && pc2))), context) case None => Failure( expr, context, s"Presence conditions of NumTy in $lhs and $rhs are not satisfiable." ) } case VType(dom) => Failure(expr, context, s"Expected NumTy but found $dom in $rhs.") case Failure(expr, context, "Error") => Failure(expr, context, "Error") case VType(dom) => Failure(expr, context, s"Expected NumTy but found $dom in $lhs.") case Failure(expr, context, "Error") => Failure(expr, context, "Error") } } //TODO:Continue the other cases, the above cases are written by me and they run successfully } } } and finally the unit tests: 4-BasicVariabilityTypeTests.scala: 

package de.uni_saarland.cs.se import Constant.* import Type.* import VExpression.{*, given} import VariabilityContext.given import cafesat.api.{FormulaBuilder, Formulas} import org.scalatest.flatspec.AnyFlatSpec import org.scalatest.matchers.should.Matchers class BasicVariabilityTypeTests extends AnyFlatSpec with Matchers { "The expression 'Const(True)'" should "have the type 'BoolTy'" in { val testExpr: VExpression = Const(True) val t = VariabilityTypeChecker.checkType(testExpr) t should equal(Success(VType(BoolTy -> Formulas.True))) } "The expression 'Const(False)'" should "have the type 'BoolTy'" in { val testExpr: VExpression = Const(False) val t = VariabilityTypeChecker.checkType(testExpr) t should equal(Success(VType(BoolTy -> Formulas.True))) } "The expression 'Const(Num(42))'" should "have the type 'NumTy'" in { val testExpr: VExpression = Const(Num(42)) val t = VariabilityTypeChecker.checkType(testExpr) t should equal(Success(VType(NumTy -> Formulas.True))) } "The variable in 'x'" must "be in the context" in { val testExpr: VExpression = Id("x") val error = VariabilityTypeChecker.checkType(testExpr) error should equal( Failure(testExpr, VariabilityTypeChecker.createContext()) ) } "The arguments to 'Smaller'" must "have the type 'Num'" in { val testExpr: VExpression = 5 _lt False val error = VariabilityTypeChecker.checkType(testExpr) error should equal( Failure(testExpr, VariabilityTypeChecker.createContext()) ) } "The condition in 'If'" must "have the type 'BoolTy'" in { val testExpr: VExpression = _if(3) _then True _else False val error = VariabilityTypeChecker.checkType(testExpr) error should equal( Failure(testExpr, VariabilityTypeChecker.createContext()) ) } "The 'Id' in 'Let'" must "not be in the context already" in { val testExpr: VExpression = _let("x") _is 5 _in ("x" _lt 4) val context = VariabilityTypeChecker.createContext( typeContext = TypeContext(("x", VType(NumTy -> Formulas.True))) ) val error = VariabilityTypeChecker.checkType(testExpr, context) error should equal(Failure(testExpr, context)) } "The expression 'Choice(A || B, True, 5)'" should "have a VType with two entries" in { val A = FormulaBuilder.propVar("A") val B = FormulaBuilder.propVar("B") val testExpr: VExpression = Choice(A || B, True, 5) val t = VariabilityTypeChecker.checkType(testExpr) t should equal(Success(VType(BoolTy -> (A || B), NumTy -> !(A || B)))) } }