Add support for pure functions

src/col/vct/col/ast/Node.scala

@@ -1081,36 +1081,35 @@ final case class BipInternal[G]()(implicit val o: Origin = DiagnosticOrigin) ext
 final case class BipPortSynchronization[G](ports: Seq[Ref[G, BipPort[G]]], wires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipSynchronizationFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with BipPortSynchronizationImpl[G]
 final case class BipTransitionSynchronization[G](transitions: Seq[Ref[G, BipTransition[G]]], wires: Seq[BipGlueDataWire[G]])(val blame: Blame[BipSynchronizationFailure])(implicit val o: Origin) extends GlobalDeclaration[G] with BipTransitionSynchronizationImpl[G]
 
-final class LlvmFunctionContract[G](val value:String, val variableRefs:Seq[(String, Ref[G, Variable[G]])], val invokableRefs:Seq[(String, Ref[G, LlvmFunctionDefinition[G]])])
+final class LlvmFunctionContract[G](val value:String, val variableRefs:Seq[(String, Ref[G, Variable[G]])], val invokableRefs:Seq[(String, Ref[G, LlvmCallable[G]])])
                                    (val blame: Blame[NontrivialUnsatisfiable])
                                    (implicit val o: Origin) extends NodeFamily[G] with LLVMFunctionContractImpl[G] {
   var data: Option[ApplicableContract[G]] = None
 }
-
+sealed trait LlvmCallable[G] extends GlobalDeclaration[G]
 final class LlvmFunctionDefinition[G](val returnType: Type[G],
                                       val args: Seq[Variable[G]],
                                       val functionBody: Statement[G],
                                       val contract: LlvmFunctionContract[G],
                                       val pure: Boolean = false)
                                      (val blame: Blame[CallableFailure])(implicit val o: Origin)
-  extends GlobalDeclaration[G] with Applicable[G] with LLVMFunctionDefinitionImpl[G]
-
+  extends LlvmCallable[G] with Applicable[G] with LLVMFunctionDefinitionImpl[G]
+final class LlvmSpecFunction[G](val name: String, val returnType: Type[G], val args: Seq[Variable[G]], val typeArgs: Seq[Variable[G]],
+                                val body: Option[Expr[G]], val contract: ApplicableContract[G], val inline: Boolean = false, val threadLocal: Boolean = false)
+                               (val blame: Blame[ContractedFailure])(implicit val o: Origin)
+  extends LlvmCallable[G] with AbstractFunction[G] with LLVMSpecFunctionImpl[G]
 final case class LlvmFunctionInvocation[G](ref: Ref[G, LlvmFunctionDefinition[G]],
                                      args: Seq[Expr[G]],
                                      givenMap: Seq[(Ref[G, Variable[G]], Expr[G])],
                                      yields: Seq[(Expr[G], Ref[G, Variable[G]])])
                                     (val blame: Blame[InvocationFailure])(implicit val o: Origin) extends Apply[G] with LLVMFunctionInvocationImpl[G]
-
 final case class LlvmLoop[G](cond:Expr[G], contract:LlvmLoopContract[G], body:Statement[G])
                        (implicit val o: Origin) extends CompositeStatement[G] with LLVMLoopImpl[G]
-
 sealed trait LlvmLoopContract[G] extends NodeFamily[G] with LLVMLoopContractImpl[G]
 final case class LlvmLoopInvariant[G](value:String, references:Seq[(String, Ref[G, Declaration[G]])])
                                      (val blame: Blame[LoopInvariantFailure])
                                      (implicit val o: Origin) extends LlvmLoopContract[G] with LLVMLoopInvariantImpl[G]
-
 sealed trait LlvmExpr[G] extends Expr[G] with LLVMExprImpl[G]
-
 final case class LlvmLocal[G](name: String)(val blame: Blame[DerefInsufficientPermission])(implicit val o: Origin) extends LlvmExpr[G] with LLVMLocalImpl[G] {
   var ref: Option[Ref[G, Variable[G]]] = None
 }
@@ -1119,7 +1118,11 @@ final case class LlvmAmbiguousFunctionInvocation[G](name: String,
                                                     givenMap: Seq[(Ref[G, Variable[G]], Expr[G])],
                                                     yields: Seq[(Expr[G], Ref[G, Variable[G]])])
                                                    (val blame: Blame[InvocationFailure])(implicit val o: Origin) extends LlvmExpr[G] with LLVMAmbiguousFunctionInvocationImpl[G] {
-  var ref: Option[Ref[G, LlvmFunctionDefinition[G]]] = None
+  var ref: Option[Ref[G, LlvmCallable[G]]] = None
+}
+
+final class LlvmGlobal[G](val value: String)(implicit val o: Origin) extends GlobalDeclaration[G] with LLVMGlobalImpl[G] {
+  var data: Option[GlobalDeclaration[G]] = None
 }
 sealed trait PVLType[G] extends Type[G] with PVLTypeImpl[G]
 final case class PVLNamedType[G](name: String, typeArgs: Seq[Type[G]])(implicit val o: Origin = DiagnosticOrigin) extends PVLType[G] with PVLNamedTypeImpl[G] {

src/col/vct/col/ast/lang/LLVMAmbiguousFunctionInvocationImpl.scala

@@ -1,11 +1,12 @@
 package vct.col.ast.lang
 
-import vct.col.ast.{LlvmAmbiguousFunctionInvocation, Type}
+import vct.col.ast.{LlvmAmbiguousFunctionInvocation, LlvmFunctionDefinition, LlvmSpecFunction, Type}
 import vct.col.print.{Ctx, Doc, DocUtil, Group, Precedence, Text}
 
 trait LLVMAmbiguousFunctionInvocationImpl[G] { this: LlvmAmbiguousFunctionInvocation[G] =>
-  override lazy val t: Type[G] = ref match {
-    case Some(ref) => ref.decl.returnType
+  override lazy val t: Type[G] = ref.get.decl match {
+    case func: LlvmFunctionDefinition[G] => func.returnType
+    case func: LlvmSpecFunction[G] => func.returnType
   }
 
   override def precedence: Int = Precedence.POSTFIX

src/col/vct/col/ast/lang/LLVMGlobalImpl.scala

@@ -0,0 +1,7 @@
+package vct.col.ast.lang
+
+import vct.col.ast.LlvmGlobal
+
+trait LLVMGlobalImpl[G] { this: LlvmGlobal[G] =>
+
+}

src/col/vct/col/ast/lang/LLVMSpecFunctionImpl.scala

@@ -0,0 +1,31 @@
+package vct.col.ast.lang
+
+import vct.col.ast.LlvmSpecFunction
+import vct.col.ast.declaration.category.AbstractFunctionImpl
+import vct.col.ast.declaration.global.GlobalDeclarationImpl
+import vct.col.print.{Ctx, Doc, Empty, Group, Show, Text}
+
+import scala.collection.immutable.ListMap
+
+trait LLVMSpecFunctionImpl[G] extends GlobalDeclarationImpl[G] with AbstractFunctionImpl[G] {
+  this: LlvmSpecFunction[G] =>
+
+  def layoutModifiers(implicit ctx: Ctx): Seq[Doc] = ListMap(
+    inline -> "inline",
+    threadLocal -> "thread_local",
+  ).filter(_._1).values.map(Text).map(Doc.inlineSpec).toSeq
+
+  def layoutSpec(implicit ctx: Ctx): Doc =
+    Doc.stack(Seq(
+      contract,
+      Group(
+        Group(Doc.rspread(layoutModifiers) <> "pure" <+> returnType <+> ctx.name(this) <>
+          (if (typeArgs.nonEmpty) Text("<") <> Doc.args(typeArgs.map(ctx.name).map(Text)) <> ">" else Empty) <>
+          "(" <> Doc.args(args) <> ")") <>
+          body.map(Text(" =") <>> _ <> ";").getOrElse(Text(";"))
+      ),
+    ))
+
+  override def layout(implicit ctx: Ctx): Doc = Doc.spec(Show.lazily(layoutSpec(_)))
+
+}