diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala new file mode 100644 index 0000000000..5761e003bc --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigLexer.scala @@ -0,0 +1,54 @@ +package at.forsyte.apalache.io.tlc + +import at.forsyte.apalache.io.tlc.config._ + +import scala.util.parsing.combinator.RegexParsers + +/** + * A lexer for the TLC configuration files. + * + * @author Igor Konnov + */ +object TlcConfigLexer extends RegexParsers { + override def skipWhitespace: Boolean = true + + def identifier: Parser[Ident] = { + "[a-zA-Z_][a-zA-Z0-9_]*".r ^^ { name => Ident(name) } + } + + def constant: Parser[Constant] = { + "CONSTANT(S|)".r ^^ (_ => Constant()) + } + + def init: Parser[Init] = { + "INIT" ^^ (_ => Init()) + } + + def next: Parser[Next] = { + "NEXT" ^^ (_ => Next()) + } + + def specification: Parser[Specification] = { + "SPECIFICATION" ^^ (_ => Specification()) + } + + def invariant: Parser[Invariant] = { + "INVARIANT" ^^ (_ => Invariant()) + } + + def property: Parser[Property] = { + "PROPERT(Y|IES)" ^^ (_ => Property()) + } + + def constraint: Parser[Constraint] = { + "CONSTRAINT" ^^ (_ => Constraint()) + } + + def assign: Parser[Assign] = { + "<-" ^^ (_ => Assign()) + } + + def eq: Parser[Eq] = { + "=" ^^ (_ => Eq()) + } +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala new file mode 100644 index 0000000000..3963e9da74 --- /dev/null +++ b/tla-import/src/main/scala/at/forsyte/apalache/io/tlc/TlcConfigParser.scala @@ -0,0 +1,10 @@ +package at.forsyte.apalache.io.tlc + +/** + * A parser for the TLC configuration files. + * + * @author Igor Konnov + */ +class TlcConfigParser { + +} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/dsl/dsl.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/dsl/dsl.scala deleted file mode 100644 index ea64903838..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/dsl/dsl.scala +++ /dev/null @@ -1,86 +0,0 @@ -import scala.collection.mutable - -package at.forsyte.apalache.tla.obsolete.dsl { - - -/** - * Domain-specific classes and objects that allow one to write TLA+ code directly. - */ - -abstract class TlaExpr - -case class TlaInt(v: Int) extends TlaExpr - -case class TlaStr(v: String) extends TlaExpr - - -abstract class TlaSym - -case class TlaVar(name: String) - -case class TlaConst(name: String) - -case class TlaOper(sname: Symbol, sargs: List[Symbol], var body: Option[TlaExpr]) { - def ARGS(args: Symbol*) = new TlaOper(sname, args.toList, None) - - def DEF(e: TlaExpr) = { - body = Some(e) - this - } -} - -case class TlaInstance(name: String) { - var subst: List[Tuple2[Symbol, TlaExpr]] = List() - - def WITH(params: Tuple2[Symbol, TlaExpr]*) = - subst = params.toList -} - - -class Module(private val builder: Builder, val namesym: Symbol) { - private val symbols: Map[String, TlaSym] = Map() - private var assumptions: List[TlaExpr] = List() - private var imports: List[String] = List() - - def name = namesym.name - - def EXTENDS(mods: Symbol*) = - for (s <- mods.reverseIterator) - imports = s.name :: imports - - def CONSTANT(s: Symbol) = symbols + (s.name -> TlaConst(s.name)) - - def CONSTANTS(syms: Symbol*) = for (s <- syms) CONSTANT(s) - - def VARIABLE(s: Symbol) = symbols + (s.name -> TlaVar(s.name)) - - def VARIABLES(syms: Symbol*) = for (s <- syms) VARIABLE(s) - - def ASSUME(e: TlaExpr) = - assumptions = e :: assumptions - - def OPER(opsym: Symbol) = { - val oper = new TlaOper(sname = opsym, sargs = List(), body = None) - symbols + (opsym.name -> oper) - oper - } - - def INSTANCE(opsym: Symbol) = new TlaInstance(opsym.name) -} - - -class Builder { - def MODULE(name: Symbol) = new Module(this, name) -} - - -/** - * Implicit conversions. Use import Implicit._ to enable the conversions. - */ -object Implicit { - implicit def intToTlaExpr(i: Int): TlaExpr = TlaInt(i) - - implicit def stringToTlaExpr(s: String): TlaExpr = TlaStr(s) -} - -} \ No newline at end of file diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Kind.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Kind.scala deleted file mode 100644 index ebc29920f1..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Kind.scala +++ /dev/null @@ -1,34 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * An entity kind, which mirrors the kind of a tla2sany.semantic.SemanticNode. - * - * @see tla2sany.semantic.SemanticNode of TLA Toolbox - * - * @author konnov - */ -object Kind extends Enumeration { - // value 1 is used for a module - val Const = Value(2, "Constant") - val Var = Value(3, "Variable") - val BoundSym = Value(4, "BoundSymbol") - val UserOp = Value(5, "UserDefinedOperator") - val ModInst = Value(6, "ModuleInstance") - val BuiltinOp = Value(7, "BuiltinOperator") - val OpArg = Value(8, "OperatorArgument") - val OpApp = Value(9, "OperatorApplication") - val LetIn = Value(10, "LetIn") - val FormalParam = Value(11, "FormalParam") - val Theorem = Value(12, "Theorem") - val SubstIn = Value(13, "SubstIn") - val AssumeProve = Value(14, "AssumeProve") - // value 15 is missing in SemanticNode - val Numeral = Value(16, "Numeral") - val Decimal = Value(17, "Decimal") - val String = Value(18, "String") - val AtNode = Value(19, "AtNode") - val Assume = Value(20, "Assume") - val Instance = Value(21, "Instance") - val NewSymb = Value(22, "NewSymb") // instance statement or definition - val ThmOrAssumpDef = Value(23, "ThmOrAssump") -} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Loc.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Loc.scala deleted file mode 100644 index 76644c5d3c..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Loc.scala +++ /dev/null @@ -1,23 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * A location in a text file characterized by line number and column. - * - * @author konnov - */ -class Loc(val lineno: Int, val colno: Int) extends Ordered[Loc] { - /** - * Compare locations as a natural order on (line, column) - * @param that the object to compare to - * @return -1 when less than, 0 when equal, and 1 otherwise - */ - override def compare(that: Loc): Int = - if (this.lineno == that.lineno) - Integer.compare(this.colno, that.colno) - else - Integer.compare(this.lineno, that.lineno) -} - -object Loc { - def apply(line: Int, col: Int): Loc = new Loc(line, col) -} \ No newline at end of file diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/LocRange.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/LocRange.scala deleted file mode 100644 index 456aa0ad4f..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/LocRange.scala +++ /dev/null @@ -1,60 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * A range in a file. - * - * @author konnov - */ -class LocRange(val start: Loc, val end: Loc) { - /** - * Compare non-intersecting ranges - * - * @param that the range to compare to - * @return true iff the ranges do not intersect and this range is before that range - */ - def before(that: LocRange): Boolean = - end < that.start - - /** - * Compare non-intersecting ranges - * - * @param that the range to compare to - * @return true iff the ranges do not intersect and this range is after that range - */ - def after(that: LocRange): Boolean = - start > that.end - - /** - * Check whether two ranges intersect - * - * @param that the range to compare to - * @return true iff the ranges intersect - */ - def intersects(that: LocRange): Boolean = { - val (left, right) = if (start < that.start) (this, that) else (that, this) - left.end >= right.start - } - - /** - * Check whether two ranges do not intersect - * - * @param that the range to compare to - * @return true iff the ranges do not intersect - */ - def not_intersect(that: LocRange): Boolean = - !this.intersects(that) - - /** - * Check whether the range is inside of another range - * - * @param larger the range that is supposed to be larger - * @return true iff this range is inside of the larger range (equal borders are included) - */ - def inside(larger: LocRange): Boolean = - larger.start <= start && end <= larger.end -} - - -object LocRange { - def apply(start: Loc, end: Loc) = new LocRange(start, end) -} \ No newline at end of file diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Module.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Module.scala deleted file mode 100644 index b24d386214..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Module.scala +++ /dev/null @@ -1,14 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * A TLA+ module. - * - * @author konnov - */ -class Module(val origin: Origin, - val uniqueName: String, - val constants: List[UserOpDecl], - val variables: List[UserOpDecl], - val operators: List[UserOpDef], - val assumptions: List[Assumption], - val theorems: List[Theorem]) diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Origin.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Origin.scala deleted file mode 100644 index ece9cdfcff..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Origin.scala +++ /dev/null @@ -1,13 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * Data on the symbol origin - * - * @author konnov - */ -class Origin( - val uid: Int, - val level: Int, - val filename: String, - val locRange: LocRange -) diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Spec.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Spec.scala deleted file mode 100644 index ea44b32e08..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/Spec.scala +++ /dev/null @@ -1,8 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * A complete TLA specification - * - * @author konnov - */ -class Spec(val modules: List[Module]) diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/SymbolTable.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/SymbolTable.scala deleted file mode 100644 index 6a5ff50543..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/SymbolTable.scala +++ /dev/null @@ -1,13 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * A place where all the definitions and declarations are kept. - * This is what goes under the tag in the XML format by tla2sany.XMLExporter. - * - * @todo the name may be misleading - * - * @author konnov - */ -class SymbolTable { - -} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/TlaNode.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/TlaNode.scala deleted file mode 100644 index 3743430170..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/ir/TlaNode.scala +++ /dev/null @@ -1,45 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -/** - * Every object of TLA intermediate representation inherits from this one. - * Case classes implement different types of TLA nodes. - * Note that using this hierarchy allows badly-formed expressions, - * i.e., one can define weird expressions like a variable with two formal parameters. - * We will probably add consistency checks later. - */ -sealed abstract class TlaNode -/** - * A declaration of a user-defined operator, e.g., of a variable. - * UserOpDecl differs from UserOpDef in that the former does not have a body. - */ -case class UserOpDecl(kind: Kind.Value, uniqueName: String, arity: Int, origin: Origin) - extends TlaNode -/** A user-defined operator */ -case class UserOpDef(uniqueName: String, params: List[FormalParam], body: TlaNode, origin: Origin) - extends TlaNode -/** A built-in operator */ -case class BuiltinOp(uniqueName: String, params: List[FormalParam], origin: Origin) - extends TlaNode -/** - * A formal parameter - * - * @param arity the arity of the parameter, i.e., the parameter is an operator - * @param isLeibniz when true, then the parameter is Leibniz, - * i.e., it respects substitution: A = B => F(A) = F(B). - * - * @see L. Lamport. TLA+2: a preliminary guide, p. 7. 15 Jan 2014. - */ -case class FormalParam(uniqueName: String, arity: Int, isLeibniz: Boolean = true) - extends TlaNode -/** Operator application */ -case class OpApply(oper: TlaNode, args: List[TlaNode], origin: Origin) - extends TlaNode -/** An assumption */ -case class Assumption(body: UserOpDef, origin: Origin) - extends TlaNode -/** An axiom */ -case class Axiom(body: UserOpDef, origin: Origin) - extends TlaNode -/** A theorem */ -case class Theorem(body: UserOpDef, origin: Origin) - extends TlaNode \ No newline at end of file diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlError.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlError.scala deleted file mode 100644 index 249b0e4410..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlError.scala +++ /dev/null @@ -1,10 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.parser - -/** - * An error reported by XmlImporter. - * - * @deprecated - * - * @author Igor Konnov - */ -class XmlError (val elem: xml.Node, val message: String) diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporter.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporter.scala deleted file mode 100644 index c900c81aa6..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporter.scala +++ /dev/null @@ -1,260 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.parser - -import String.format - -import at.forsyte.apalache.tla.obsolete.ir._ - -import scala.collection.immutable.TreeSet -import scala.xml.{Elem, Node} - -/** - * A parser of TLA+ code from XML generated by XMLExporter. - * Our goal is to make this parser to behave as a compiler, so it does not crash on the first error, - * but ignores the unexpected elements and then reports all the errors (up to a given limit). - * - * Note that the same instance of XmlImporter should not be used in different threads. - * - * @see tla2sany.XMLExporter - * - * @todo do a preliminary structure check with XML schema? - * - * @deprecated use at.forsyte.apalache.tla.SanyImporter - * - * @author konnov - */ -class XmlImporter { - var contextToParse: Map[Int, xml.Node] = Map() - var context: Map[Int, TlaNode] = Map() - var maxUid = 0 - - /** - * Parse an XML tree created by SANY - * @param node root node (tagged with modules) - * @return an internal representation of the TLA spec and the list of errors (if any were found) - */ - def parse(node: xml.Node): Tuple2[Spec, List[XmlError]] = { - maxUid = 0 - if (node.label != "modules") - throw new XmlImporterException(String.format("Expected ..., found <%s>", - node.label, node.label)) - - contextToParse = collectContextNodes(node \ "context" \ "entry") - context = Map() - (new Spec((node \ "ModuleNode").map(parseModule).toList), List()) - } - - private def nextUid() = { - val uid = maxUid - maxUid = maxUid + 1 - uid - } - - // updates maxUid and returns a map from uid to the corresponding node - private def collectContextNodes(nodes: xml.NodeSeq): Map[Int, xml.Node] = { - def getUid(node: xml.Node): Int = - (node \ "UID").text.toInt - - // pick any Elem (not Text!) different from UID - def getSub(node: xml.Node): xml.Node = { - val sub = (node \ "_").filter(_.label != "UID") - if (sub.length == 1) - sub.head - else - throw new XmlImporterException(format("Unexpected entry structure: %s (sub = %s)", - node.toString(), sub.toString())) - } - - maxUid = 1 + nodes.map(getUid).foldLeft(0)(Math.max) - nodes.foldLeft (Map[Int, xml.Node]()) ((m, n) => m + (getUid(n) -> getSub(n))) - } - - private def parseModule(node: xml.Node): Module = { - val uniqueName = (node \ "uniquename").text - val origin = parseOrigin(nextUid(), 0, (node \ "location").head) - val vars = (node \ "variables" \ "OpDeclNodeRef" \ "UID") - .map(n => ofKind(parseOpDecl(n.text.toInt), Kind.Var)).toList - - // - // - val operators = (node \ "definitions" \ "UserDefinedOpKindRef" \ "UID").map(n => parseOpDef (n.text.toInt)).toList - - new Module(origin, uniqueName, constants = List(), variables = vars, - operators = operators, assumptions = List(), theorems = List()) - } - - private def parseOpDecl(uid: Int): UserOpDecl = { - context.get(uid) match { - case Some(node) => - node.asInstanceOf[UserOpDecl] - - case _ => - val node = contextToParse(uid) - assert(node.label == "OpDeclNode") - val uniqueName = (node \ "uniquename").text - val level = (node \ "level").text.toInt - val origin = parseOrigin(uid, level, (node \ "location").head) - val arity = (node \ "arity").text.toInt - val kindId = (node \ "kind").text.toInt - val kind = Kind(kindId) - - val decl = UserOpDecl(uniqueName = uniqueName, origin = origin, arity = arity, kind = kind) - context += uid -> decl - decl - } - } - - private def ofKind(decl: UserOpDecl, expectedKind: Kind.Value): UserOpDecl = { - if (decl.kind != expectedKind) - throw new XmlImporterException(format("Expected kind %s, found %s", expectedKind, decl.kind)) - else - decl - } - - private def parseOpDef(uid: Int): UserOpDef = { - context.get(uid) match { - case Some(node) => - node.asInstanceOf[UserOpDef] - - case _ => - val node = contextToParse(uid) - assert(node.label == "UserDefinedOpKind") - val uniqueName = (node \ "uniquename").text - val level = (node \ "level").text.toInt - val origin = parseOrigin(uid, level, (node \ "location").head) - val arity = (node \ "arity").text.toInt - val body = parseChildExprNode((node \ "body").head) - val params = List() // todo: parse params - assert(params.size == arity) - val oper = UserOpDef(uniqueName = uniqueName, params, body, origin) - context += uid -> oper - oper - } - } - - private def parseBuiltinOp(uid: Int): BuiltinOp = { - context.get(uid) match { - case Some(node) => - node.asInstanceOf[BuiltinOp] - - case _ => - val node = contextToParse(uid) - assert(node.label == "BuiltInKind") - val uniqueName = (node \ "uniquename").text - val level = (node \ "level").text.toInt - val origin = parseOrigin(uid, level, (node \ "location").head) - val arity = (node \ "arity").text.toInt - val params = (node \ "params" \ "leibnizparam" \ "FormalParamNodeRef" \ "UID") - .map(n => parseFormalParam(n.text.toInt)).toList - assert(params.size == arity) - val oper = BuiltinOp(uniqueName = uniqueName, params, origin) - context += uid -> oper - oper - } - } - - private def parseFormalParam(uid: Int) = { - context.get(uid) match { - case Some(node) => - node.asInstanceOf[FormalParam] - - case _ => - val node = contextToParse(uid) - assert(node.label == "FormalParamNode") - val uniqueName = (node \ "uniquename").text - val arity = (node \ "arity").text.toInt - val param = FormalParam(uniqueName = uniqueName, arity = arity) - context += uid -> param - param - } - - } - - private def parseChildExprNode(parent: xml.Node): TlaNode = { - // make it final? - val options = TreeSet("AtNode", - "DecimalNode", "LabelNode", "LetInNode", "NumeralNode", "OpApplNode", "StringNode", "SubstInNode") - val exprNode = parent.child.find(n => options.contains(n.label)) - exprNode match { - case Some(n) => - parseExprNode(n) - - case None => - val msg = format("Expected one of the expression nodes at XML node@%s: %s", (parent \ "UID").text, options) - throw new XmlImporterException(msg) - } - } - - private def parseExprNode(node: xml.Node): TlaNode = { - node.label match { - case "OpApplNode" => - parseOpApplNode(node) - - case _ => // todo: parse the other types of nodes - throw new XmlImporterException("Unexpected expression type: " + node.label) - } - } - - private def parseOpApplNode(node: xml.Node): OpApply = { - val level = (node \ "level").text.toInt - val origin = parseOrigin(nextUid(), level, (node \ "location").head) - val operNodes = node \ "operator" - val oper = - if (operNodes.size == 1) - parseChildOperRef(operNodes.head) - else throw new XmlImporterException("Incorrect OpApplNode.operator: " + node) - def isElem (n: xml.Node): Boolean = n match { - case _: xml.Elem => true - case _ => false - } - val operandNodes = (node \ "operands").head.nonEmptyChildren.filter(isElem) /* ignore the text elements */ - val operands = - try operandNodes.map(parseExprNode).toList - catch { - case e: XmlImporterException => - throw new XmlImporterException(e.message + " in: " + node.toString()) - } - - // todo: parse boundSymbols - OpApply(oper = oper, args = operands, origin = origin) - } - - private def parseChildOperRef(parent: xml.Node) = { - // make it final? - val options = TreeSet("FormalParamNodeRef", "ModuleNodeRef", "OpDeclNodeRef", "TheoremNodeRef", - "AssumeNodeRef", "ModuleInstanceKindRef", "UserDefinedOpKindRef", "BuiltInKindRef") - val exprNode = parent.child.find(n => options.contains(n.label)) - exprNode match { - case Some(ref) => - parseOperRef(ref) - - case None => - val msg = format("Expected one of the expression nodes (%s) at XML node %s", options, parent) - throw new XmlImporterException(msg) - } - } - - private def parseOperRef(node: xml.Node) = { - node.label match { - case "BuiltInKindRef" => - parseBuiltinOp((node \ "UID").text.toInt) - - case "UserDefinedOpKindRef" => - parseOpDef((node \ "UID").text.toInt) - - case "OpDeclNodeRef" => - parseOpDecl((node \ "UID").text.toInt) - - case _ => // todo: parse the other kinds - throw new XmlImporterException("Unexpected expression type: " + node.label) - } - } - - private def parseOrigin(uid: Int, level: Int, node: xml.Node): Origin = { - val filename = (node \ "filename").text - val startCol = (node \ "column" \ "begin").text.toInt - val endCol = (node \ "column" \ "end").text.toInt - val startLine = (node \ "line" \ "begin").text.toInt - val endLine = (node \ "line" \ "end").text.toInt - new Origin(uid, level, filename, LocRange(Loc(startLine, startCol), Loc(endLine, endCol))) - } -} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporterConsole.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporterConsole.scala deleted file mode 100644 index 1ffd930a70..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporterConsole.scala +++ /dev/null @@ -1,28 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.parser - -import scala.xml.XML - -/** - * A command-line to check how good our parser is. - * - * @deprecated - * - * @author Igor Konnov - */ -object XmlImporterConsole { - def use(): Unit = { - println("Arguments: filename.xml") - System.exit(1) - } - - def main(args: Array[String]): Unit = { - Console.printf("*** APALACHE ***\n\n") - Console.printf("XmlImporterConsole\n") - - if (args.length < 1) - use() - - val xml = XML.loadFile(args(0)) - val spec = new XmlImporter().parse(xml) - } -} diff --git a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporterException.scala b/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporterException.scala deleted file mode 100644 index 8025ad8a13..0000000000 --- a/tla-import/src/main/scala/at/forsyte/apalache/tla/obsolete/parser/XmlImporterException.scala +++ /dev/null @@ -1,11 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.parser - -/** - * A general exception reported by XmlImporter - * - * @deprecated - * - * @author konnov - */ -class XmlImporterException(val message: String) - extends Exception(message) diff --git a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/dsl/TestTlaDsl.scala b/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/dsl/TestTlaDsl.scala deleted file mode 100644 index 9c66d18bd0..0000000000 --- a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/dsl/TestTlaDsl.scala +++ /dev/null @@ -1,36 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.dsl - -import org.junit.runner.RunWith -import org.scalatest.FunSuite -import org.scalatest.junit.JUnitRunner - -import Implicit._ - -/** - * Tests for DSL - * - * @author konnov - */ -@RunWith(classOf[JUnitRunner]) -class TestTlaDsl extends FunSuite { - test("all in one") { - /* - val b = new Builder - // top-level definitions - val m = b MODULE 'foo - m EXTENDS 'M1 - m CONSTANTS ('n, 't) - m VARIABLES 'x - m ASSUME 42 - m OPER 'F ARGS ('a, 'b) DEF 42 - m OPER 'G ARGS ('a, 'b) DEF "baz" - m INSTANCE 'M1 - m INSTANCE 'M2 WITH ('p1 -> 1, 'p2 -> 3) - - // set operations - m OPER 'OPER1 DEF SetEnum(1, 2, 3) CUP SetFilter('x, 'S, TRUE) CUP SetMap('x, 'S, 42) CAP SUBSET SetEnum(1, 2) - - assert("foo" == m.name) - */ - } -} diff --git a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/ir/TestLocRangeSuite.scala b/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/ir/TestLocRangeSuite.scala deleted file mode 100644 index d525a73b50..0000000000 --- a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/ir/TestLocRangeSuite.scala +++ /dev/null @@ -1,71 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -import org.junit.runner.RunWith -import org.scalatest.FunSuite -import org.scalatest.junit.JUnitRunner - -/** - * Tests for LocRange - * - * @see at.forsyte.apalache.tlair.LocRange - * - * @author konnov - */ -@RunWith(classOf[JUnitRunner]) -class TestLocRangeSuite extends FunSuite { - test("1:2-3:4 is before 3:5-4:6") { - assert(LocRange(Loc(1, 2), Loc(3, 4)) before LocRange(Loc(3, 5), Loc(4, 6))) - } - - test("1:2-3:4 is before 4:1-4:6") { - assert(LocRange(Loc(1, 2), Loc(3, 4)) before LocRange(Loc(4, 1), Loc(4, 6))) - } - - test("4:1-4:6 is not before 1:2-3:4") { - assert(!(LocRange(Loc(4, 1), Loc(4, 6)) before LocRange(Loc(1, 2), Loc(3, 4)))) - } - - test("1:2-4:2 is not before 4:1-4:6") { - assert(!(LocRange(Loc(1, 2), Loc(4, 2)) before LocRange(Loc(4, 1), Loc(4, 6)))) - } - - test("3:5-4:6 is after 1:2-3:4") { - assert(LocRange(Loc(3, 5), Loc(4, 6)) after LocRange(Loc(1, 2), Loc(3, 4))) - } - - test("4:1-4:6 is after 1:2-3:4") { - assert(LocRange(Loc(4, 1), Loc(4, 6)) after LocRange(Loc(1, 2), Loc(3, 4))) - } - - test("1:2-3:4 is not after 4:1-4:6") { - assert(!(LocRange(Loc(1, 2), Loc(3, 4)) after LocRange(Loc(4, 1), Loc(4, 6)))) - } - - test("4:1-4:6 is not after 1:2-4:2") { - assert(!(LocRange(Loc(4, 1), Loc(4, 6)) after LocRange(Loc(1, 2), Loc(4, 2)))) - } - - test("2:1-3:4 intersects 1:5-4:3") { - assert(LocRange(Loc(2, 1), Loc(3, 4)) intersects LocRange(Loc(1, 5), Loc(4, 3))) - } - - test("2:1-3:4 intersects 3:4-4:3") { - assert(LocRange(Loc(2, 1), Loc(3, 4)) intersects LocRange(Loc(3, 4), Loc(4, 3))) - } - - test("2:1-3:4 does not intersect 4:4-4:3") { - assert(!(LocRange(Loc(2, 1), Loc(3, 4)) intersects LocRange(Loc(4, 4), Loc(4, 3)))) - } - - test("2:1-3:4 not_intersect 4:4-4:3") { - assert(LocRange(Loc(2, 1), Loc(3, 4)) not_intersect LocRange(Loc(4, 4), Loc(4, 3))) - } - - test("2:1-3:4 inside 1:5-4:3") { - assert(LocRange(Loc(2, 1), Loc(3, 4)) inside LocRange(Loc(1, 5), Loc(4, 3))) - } - - test("1:4-3:4 not inside 1:5-4:3") { - assert(!(LocRange(Loc(1, 4), Loc(3, 4)) inside LocRange(Loc(1, 5), Loc(4, 3)))) - } -} diff --git a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/ir/TestLocSuite.scala b/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/ir/TestLocSuite.scala deleted file mode 100644 index cdc5beb938..0000000000 --- a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/ir/TestLocSuite.scala +++ /dev/null @@ -1,33 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.ir - -import org.scalatest.FunSuite -import org.scalatest.junit.JUnitRunner -import org.junit.runner.RunWith - -/** - * Tests for Loc - * - * @see at.forsyte.apalache.tlair.Loc - * - * @author konnov - */ -@RunWith(classOf[JUnitRunner]) -class TestLocSuite extends FunSuite { - test("different lines are compared correctly") { - val lesser = new Loc(2, 5) - val greater = new Loc(3, 3) - assert(lesser.compare(greater) < 0) - } - - test("different columns are compared correctly") { - val lesser = new Loc(3, 3) - val greater = new Loc(3, 4) - assert(lesser.compare(greater) < 0) - } - - test("equal locations are reported equal") { - val lesser = new Loc(3, 3) - val greater = new Loc(3, 4) - assert(lesser.compare(greater) < 0) - } -} diff --git a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/parser/TestXmlImporterSuite.scala b/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/parser/TestXmlImporterSuite.scala deleted file mode 100644 index 8d66e1834f..0000000000 --- a/tla-import/src/test/scala/at/forsyte/apalache/tla/obsolete/parser/TestXmlImporterSuite.scala +++ /dev/null @@ -1,331 +0,0 @@ -package at.forsyte.apalache.tla.obsolete.parser - -import at.forsyte.apalache.tla.obsolete.ir._ -import org.junit.runner.RunWith -import org.scalatest.FunSuite -import org.scalatest.junit.JUnitRunner - -/** - * Tests for XmlImporter - * - * @see at.forsyte.apalache.tla.obsolete.parser.XmlImporter - * - * @author konnov - */ -@RunWith(classOf[JUnitRunner]) -class TestXmlImporterSuite extends FunSuite { - test("empty spec") { - val xml = - val (spec, errors) = new XmlImporter().parse(xml) - assert(0 == spec.modules.size) - assert(errors.isEmpty) - } - - test("malformed xml") { - val xml = - intercept[XmlImporterException] { - new XmlImporter().parse(xml) - } - } - - test("one empty module") { - val xml = - - - - - 162 - 19 - HC - - HourClock - - - - - - - - - val (spec, errors) = new XmlImporter().parse(xml) - assert(errors.isEmpty) - assert(1 == spec.modules.size) - val module = spec.modules.head - assert("HourClock" == module.uniqueName) - assert("HC" == module.origin.filename) - assert(1 == module.origin.locRange.start.colno) - assert(1 == module.origin.locRange.start.lineno) - assert(62 == module.origin.locRange.end.colno) - assert(9 == module.origin.locRange.end.lineno) - } - - test("one variable") { - val xml = - - - - 9 - - - 510 - 34 - HourClock - - 1 - hr - 0 - 3 - - - - - - 162 - 19 - HourClock - - HourClock - - - 9 - - - - - - - - val (spec, errors) = new XmlImporter().parse(xml) - assert(errors.isEmpty) - assert(1 == spec.modules.size) - val module = spec.modules.head - assert(1 == module.variables.size) - val hr = module.variables.head - assert("hr" == hr.uniqueName) - assert(0 == hr.arity) - assert(1 == hr.origin.level) - assert(Kind.Var == hr.kind) - - assert("HourClock" == module.origin.filename) - assert(1 == module.origin.locRange.start.colno) - assert(1 == module.origin.locRange.start.lineno) - assert(62 == module.origin.locRange.end.colno) - assert(9 == module.origin.locRange.end.lineno) - } - - test("one definition") { - val xml = - - - - - 4 - - - 0 0 - 0 0 - --TLA+ BUILTINS-- - - 0 - = - 2 - - - - 5 - - - - - - 6 - - - - - - - - 5 - - Formal_0 - 0 - - - - 6 - - Formal_1 - 0 - - - - - 234 - - - 127 - 44 - HourClock - - 1 HCini 0 - - - 12 27 - 4 4 - HourClock - - 1 - - - 4 - - - - - 12 13 - 4 4 - HourClock - - 1 - - - 9 - - - - - - 12 13 - 4 4 - HourClock - - 1 - - - 9 - - - - - - - - - - - - - - 9 - - - 510 - 34 - HourClock - - 1 - hr - 0 - 3 - - - - - - 162 - 19 - HourClock - - HourClock - - - - - 234 - - - - - - - - val (spec, errors) = new XmlImporter().parse(xml) - assert(errors.isEmpty) - assert(1 == spec.modules.size) - val module = spec.modules.head - assert(1 == module.operators.size) - - // the standard things - val op = module.operators.head - assert(1 == op.origin.locRange.start.colno) - assert(4 == op.origin.locRange.start.lineno) - assert(27 == op.origin.locRange.end.colno) - assert(4 == op.origin.locRange.end.lineno) - assert(1 == op.origin.level) - assert("HourClock" == op.origin.filename) - - // the parameters - assert(op.params.isEmpty) - - // and now the body - op.body match { - case app: OpApply => - assert(4 == app.origin.locRange.start.lineno) - assert(4 == app.origin.locRange.end.lineno) - assert(12 == app.origin.locRange.start.colno) - assert(27 == app.origin.locRange.end.colno) - assert("HourClock" == app.origin.filename) - assert(1 == app.origin.level) - - // the operator is actually a built-in operator - app.oper match { - case bop: BuiltinOp => - assert("=" == bop.uniqueName) - assert("--TLA+ BUILTINS--" == bop.origin.filename) - assert(0 == bop.origin.level) - assert(2 == bop.params.size) - val param0 = bop.params.head - val param1 = bop.params.tail.head - assert("Formal_0" == param0.uniqueName) - assert(param0.isLeibniz) - assert(0 == param0.arity) - assert("Formal_1" == param1.uniqueName) - assert(param1.isLeibniz) - assert(0 == param1.arity) - - case _ => - fail("Expected BuiltinOp") - } - - assert(2 == app.args.length) - - def isHr(operand: TlaNode): Unit = operand match { - case opapp: OpApply => - assert(12 == opapp.origin.locRange.start.colno) - assert(13 == opapp.origin.locRange.end.colno) - assert(4 == opapp.origin.locRange.start.lineno) - assert(4 == opapp.origin.locRange.end.lineno) - assert("HourClock" == opapp.origin.filename) - assert(1 == opapp.origin.level) - - opapp.oper match { - case d: UserOpDecl => - assert("hr" == d.uniqueName) - - case _ => - fail("Expected hr") - } - - case _ => - fail("Expected OpApply as the 0th operand") - } - - isHr(app.args.head) - isHr(app.args.tail.head) - - case _ => - fail("Expected OpApply") - } - } -}