Skip to content

Commit

Permalink
Merge recent changes in lore
Browse files Browse the repository at this point in the history
  • Loading branch information
@rmgk
rmgk committed Apr 12, 2024
2 parents 44e9866 + d89e90b commit 01ec7e2
Show file tree
Hide file tree
Showing 8 changed files with 213 additions and 8,190 deletions.
2 changes: 1 addition & 1 deletion Modules/Lore/src/main/scala/lore/Compiler.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -82,7 +82,7 @@ object Compiler extends IOApp {
ast <- Parser.parse(program) match {
case Left(e) =>
IO.raiseError(Parser.ParsingException(e.show))
case Right(a) => IO(a)
case Right(a) => IO.pure(a)
}
// perform requested subcommand
result <-
Expand Down
212 changes: 105 additions & 107 deletions Modules/Lore/src/main/scala/lore/ast/AST.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,12 @@ package lore.ast

import cats.data.NonEmptyList
import cats.parse.Caret
import io.circe.generic.auto.*
import io.circe.*
import com.github.plokhotnyuk.jsoniter_scala.macros.*
import com.github.plokhotnyuk.jsoniter_scala.core.*

import java.nio.file.Path
import scala.util.Try

sealed trait SourceType derives Codec.AsObject
sealed trait SourceType

case object Unknown extends SourceType

Expand All @@ -19,8 +18,8 @@ case class FromFile(path: Path) extends SourceType
case class SourcePos(start: Caret, end: Caret, _type: SourceType = Unknown)

/** The abstract syntax of the LoRe language.
*/
sealed trait Term derives Codec.AsObject {
*/
sealed trait Term {
def sourcePos: Option[SourcePos]
}

Expand All @@ -33,17 +32,16 @@ sealed trait BinaryOp {

// imports
case class TViperImport(path: Path, sourcePos: Option[SourcePos] = None)
extends TViper
extends TViper

implicit val pathEncoder: Encoder[Path] =
Encoder.encodeString.contramap[Path](_.toString)
implicit val pathDecoder: Decoder[Path] =
Decoder.decodeString.emapTry(str => Try(Path.of(str)))
// Encoder.encodeString.contramap[Path](_.toString)
//implicit val pathDecoder: Decoder[Path] =
// Decoder.decodeString.emapTry(str => Try(Path.of(str)))

// helper types
type ID = String

sealed trait Type derives Codec.AsObject
sealed trait Type

case class SimpleType(name: String, inner: List[Type]) extends Type

Expand All @@ -52,56 +50,56 @@ case class TupleType(inner: NonEmptyList[Type]) extends Type
type Number = Int

case class TArgT( // argument with type annotation
name: ID,
_type: Type,
sourcePos: Option[SourcePos] = None
) extends Term
name: ID,
_type: Type,
sourcePos: Option[SourcePos] = None
) extends Term

// basic terms
case class TVar( // variable
name: ID,
sourcePos: Option[SourcePos] = None
) extends Term
with TViper
name: ID,
sourcePos: Option[SourcePos] = None
) extends Term
with TViper

case class TAbs( // abstractions
name: ID,
_type: Type,
body: Term,
sourcePos: Option[SourcePos] = None
) extends Term
with TViper
name: ID,
_type: Type,
body: Term,
sourcePos: Option[SourcePos] = None
) extends Term
with TViper

case class TTuple( // tuples
factors: NonEmptyList[Term],
sourcePos: Option[SourcePos] = None
) extends Term
factors: NonEmptyList[Term],
sourcePos: Option[SourcePos] = None
) extends Term

case class TIf( // if clauses
cond: Term,
_then: Term,
_else: Option[Term],
sourcePos: Option[SourcePos] = None
) extends Term
cond: Term,
_then: Term,
_else: Option[Term],
sourcePos: Option[SourcePos] = None
) extends Term
// case class TApp(left: Term, right: Term) extends Term // application
// case class TUnit() extends Term // unit

// derived forms
case class TSeq( // sequences
body: NonEmptyList[Term],
sourcePos: Option[SourcePos] = None
) extends Term
with TViper
body: NonEmptyList[Term],
sourcePos: Option[SourcePos] = None
) extends Term
with TViper

case class TArrow( // anonymous functions
left: Term,
right: Term,
sourcePos: Option[SourcePos] = None
) extends Term
with BinaryOp {
left: Term,
right: Term,
sourcePos: Option[SourcePos] = None
) extends Term
with BinaryOp {
private def findBody: Term => Term = {
case t: TArrow => findBody(t.right)
case t => t
case t => t
}

def body: Term = findBody(right)
Expand All @@ -118,22 +116,22 @@ case class TArrow( // anonymous functions
}

case class TTypeAl(
name: ID,
_type: Type,
sourcePos: Option[SourcePos] = None
) extends Term // type aliases
name: ID,
_type: Type,
sourcePos: Option[SourcePos] = None
) extends Term // type aliases

// Viper terms
sealed trait TViper extends Term derives Codec.AsObject
sealed trait TViper extends Term

case class TAssert(
body: Term,
sourcePos: Option[SourcePos] = None
) extends Term
with TViper
body: Term,
sourcePos: Option[SourcePos] = None
) extends Term
with TViper

case class TAssume(body: Term, sourcePos: Option[SourcePos] = None)
extends Term
extends Term
with TViper

// reactives
Expand All @@ -142,53 +140,53 @@ sealed trait TReactive extends Term {
}

case class TSource(body: Term, sourcePos: Option[SourcePos] = None)
extends TReactive
extends TReactive

case class TDerived(body: Term, sourcePos: Option[SourcePos] = None)
extends TReactive
extends TReactive

// interactions
case class TInteraction(
reactiveType: Type,
argumentType: Type,
modifies: List[ID] = List(),
requires: List[Term] = List(),
ensures: List[Term] = List(),
executes: Option[Term] = None,
sourcePos: Option[SourcePos] = None
) extends Term
reactiveType: Type,
argumentType: Type,
modifies: List[ID] = List(),
requires: List[Term] = List(),
ensures: List[Term] = List(),
executes: Option[Term] = None,
sourcePos: Option[SourcePos] = None
) extends Term

// invariants
case class TInvariant(
condition: TBoolean,
sourcePos: Option[SourcePos] = None
) extends Term
condition: TBoolean,
sourcePos: Option[SourcePos] = None
) extends Term

// arithmetic expressions
sealed trait TArith extends Term with TViper

// numbers
case class TNum(value: Number, sourcePos: Option[SourcePos] = None)
extends TArith
extends TArith

// division
case class TDiv(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TArith
extends TArith
with BinaryOp

// multiplication
case class TMul(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TArith
extends TArith
with BinaryOp

// addition
case class TAdd(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TArith
extends TArith
with BinaryOp

// subtraction
case class TSub(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TArith // substraction
extends TArith // substraction
with BinaryOp

// boolean expressions
Expand All @@ -209,57 +207,57 @@ case class TTrue(sourcePos: Option[SourcePos] = None) extends TBoolean
case class TFalse(sourcePos: Option[SourcePos] = None) extends TBoolean

case class TNeg(body: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean

case class TLt(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

case class TGt(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

case class TLeq(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

case class TGeq(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

// equality
case class TEq(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

// inequality
case class TIneq(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

// disjunction
case class TDisj(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

// conjunction
case class TConj(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

// implication
case class TImpl(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp
// bi-implication

case class TBImpl(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

// in set
case class TInSet(left: Term, right: Term, sourcePos: Option[SourcePos] = None)
extends TBoolean
extends TBoolean
with BinaryOp

sealed trait TQuantifier extends TBoolean {
Expand All @@ -269,26 +267,26 @@ sealed trait TQuantifier extends TBoolean {
}

case class TForall(
vars: NonEmptyList[TArgT],
triggers: List[NonEmptyList[Term]],
body: Term,
sourcePos: Option[SourcePos] = None
) extends TQuantifier
vars: NonEmptyList[TArgT],
triggers: List[NonEmptyList[Term]],
body: Term,
sourcePos: Option[SourcePos] = None
) extends TQuantifier

case class TExists(
vars: NonEmptyList[TArgT],
body: Term,
sourcePos: Option[SourcePos] = None
) extends TQuantifier
vars: NonEmptyList[TArgT],
body: Term,
sourcePos: Option[SourcePos] = None
) extends TQuantifier

// parantheses
case class TParens(inner: Term, sourcePos: Option[SourcePos] = None)
extends Term
extends Term
with TViper

// strings
case class TString(value: String, sourcePos: Option[SourcePos] = None)
extends Term
extends Term

// Scala stuff
// field access
Expand All @@ -299,21 +297,21 @@ sealed trait TFAcc extends Term {
}

case class TFCall( // field call
parent: Term,
field: ID,
args: List[Term],
sourcePos: Option[SourcePos] = None
) extends TFAcc
with TViper
parent: Term,
field: ID,
args: List[Term],
sourcePos: Option[SourcePos] = None
) extends TFAcc
with TViper

case class TFCurly( // field call with curly braces
parent: Term,
field: ID,
body: Term,
sourcePos: Option[SourcePos] = None
) extends TFAcc
parent: Term,
field: ID,
body: Term,
sourcePos: Option[SourcePos] = None
) extends TFAcc

// function call
case class TFunC(name: ID, args: Seq[Term], sourcePos: Option[SourcePos] = None)
extends Term
extends Term
with TViper
Loading

0 comments on commit 01ec7e2

Please sign in to comment.