Merge pull request #1 from lukasrieger/develop

Develop

src/main/scala/Alpha.scala

@@ -0,0 +1,36 @@
+
+package alpha:
+
+  trait Term[E, V <: E]:
+    this: E =>
+
+      def free: Set[V]
+      def rename(re: Map[V, V]): E
+      def subst(su: Map[V, E]): E
+
+      def subst(v: V, e: E): E = subst(Map(v -> e))
+
+
+  trait X[E, V <: E] extends Term[E, V]:
+    this: V =>
+
+    def fresh(index: Int): V
+    def free: Set[V] = Set(this)
+    def rename(re: Map[V, V]): V = re.getOrElse(this, this)
+    def subst(su: Map[V, E]): E = su.getOrElse(this, this)
+
+
+
+trait Alpha[E <: alpha.Term[E, V], V <: E with alpha.X[E, V]]:
+  context =>
+
+  type Term = alpha.Term[E, V]
+  type X = alpha.X[E, V]
+
+  trait Bind[A]:
+    def bound: Set[V]
+    def rename(a: Map[V, V], re: Map[V, V]): A
+    def subst(a: Map[V, V], su: Map[V, E]): A
+
+
+

src/main/scala/Assert.scala

@@ -3,4 +3,4 @@ enum Assert:
   case SepImp(left: Assert, right: Assert)
   case CoImp(left: Assert, right: Assert)
   case Septract(left: Assert, right: Assert)
-  case PointsTo(pointer: Expression, arg: Expression)
+  case PointsTo(pointer: Expr, arg: Expr)

src/main/scala/Expr.scala

@@ -0,0 +1,16 @@
+import Expr.Var
+
+enum Expr:
+  case Var(name: String, index: Option[Int] = None)
+
+
+
+given exprShow: Show[Expr] with
+  override def show(value: Expr): String = value match
+    case Var(name, index) => s"$name$$$index"
+
+given [Sub <: Expr] (using s: Show[Expr]) : Show[Sub] with
+  override def show(value: Sub): String = s.show(value)
+
+
+

src/main/scala/Program.scala

@@ -1,11 +1,11 @@
-import Expression.Var
+import Expr.Var
 
 enum Program:
-  case Assign(x: Var, expr: Expression)
-  case Load(x: Expression, pointer: Expression)
-  case Store(pointer: Expression, arg: Expression)
-  case Alloc(pointer: Expression)
-  case Free(pointer: Expression)
+  case Assign(x: Var, expr: Expr)
+  case Load(x: Expr, pointer: Expr)
+  case Store(pointer: Expr, arg: Expr)
+  case Alloc(pointer: Expr)
+  case Free(pointer: Expr)
   case Block(programs: List[Program])
-  case If(test: Expression, left: Program, right: Program)
-  case While(test: Expression, inv: Assert, body: Program)
+  case If(test: Expr, left: Program, right: Program)
+  case While(test: Expr, inv: Assert, body: Program)

src/main/scala/Show.scala

@@ -0,0 +1,6 @@
+trait Show[A]:
+  def show(value: A): String
+
+
+extension [A: Show] (value: A)
+  def show: String = summon[Show[A]].show(value)

src/main/scala/Syntax.scala

@@ -1,4 +1,5 @@
 import Assert.{CoImp, PointsTo, SepAnd, SepImp, Septract}
+import Program.Block
 
 type Syntax = Syntax.type
 private object Syntax:
@@ -8,8 +9,18 @@ private object Syntax:
     infix def ~~> (that: Assert): Assert = CoImp(self, that)
     infix def ~@  (that: Assert): Assert = Septract(self, that)
 
-  extension (expr: Expression)
-    infix def |->(that: Expression): Assert = PointsTo(expr, that)
+  extension (expr: Expr)
+    infix def |->(that: Expr): Assert = PointsTo(expr, that)
+
+
+  extension (prog: Program)
+    infix def `;` (next: Program): Program =
+      def flatten = (prog, next) match
+        case (_@left, Block(right)) => left :: right
+        case (Block(left), _@right) => left ::: List(right)
+        case _ => List(prog, next)
+
+      Block(flatten)
 
 
 def dsl(fn: Syntax ?=> Assert): Assert =

src/main/scala/main.scala

@@ -1,10 +1,16 @@
-import Expression.Var
+import Expr.Var
+import Program.Free
 
 @main
 def main(): Unit = {
   val test = dsl {
-    Var("a") |-> Var("b")
+    (Var("a") |-> Var("b")) ~~> (Var("c") |-> Var("d"))
+
+    Free(Var("a")) `;` Free(Var("a"))
+
+    (Var("a") |-> Var("b")) ~~> (Var("c") |-> Var("d")) ** (Var("e") |-> Var("f"))
   }
 
+  println(Var("test").show)
   println(test)
 }