Add Isar output mode

src/col/vct/col/ast/declaration/adt/ADTAxiomImpl.scala

@@ -13,6 +13,7 @@ trait ADTAxiomImpl[G] extends ADTAxiomOps[G] {
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => Group(Text("axiom") <+> "{" <>> axiom.show <+/> "}")
+      case Ctx.Isar => Group(Text("assumes") <>> Text("\"") <> axiom.show <> Text("\""))
       case _ => Text("axiom") <+> axiom <> ";"
     }
 }

src/col/vct/col/ast/declaration/adt/ADTFunctionImpl.scala

@@ -12,13 +12,19 @@ trait ADTFunctionImpl[G]
   this: ADTFunction[G] =>
   override def body: Option[Node[G]] = None
 
+  def layoutIsar(implicit ctx: Ctx) : Doc = {
+    Group(
+       Text("fixes") <+> Text(ctx.name(this)) <+> Text("::") <+> Text("\"") <> Doc.foldr(args.map(_.t) :+ returnType)(_ <+> "⇒" <+> _) <> Text("\"")
+    )
+  }
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver =>
         Group(
           Text("function") <+> ctx.name(this) <> "(" <> Doc.args(args) <>
             "):" <+> returnType
         )
+      case Ctx.Isar => layoutIsar
       case _ =>
         Group(
           Text("pure") <+> returnType <+> ctx.name(this) <> "(" <>

src/col/vct/col/ast/declaration/global/AxiomaticDataTypeImpl.scala

@@ -10,6 +10,23 @@ trait AxiomaticDataTypeImpl[G]
   this: AxiomaticDataType[G] =>
   override def declarations: Seq[Declaration[G]] = decls ++ typeArgs
 
+  def layoutIsar(implicit ctx: Ctx): Doc = {
+    Group(
+      Group(
+        Text("typedecl") <+>
+          (if (typeArgs.nonEmpty)
+             Text("(") <> Doc.args(typeArgs.map(Text("'") <> _.show)) <>
+               Text(")")
+           else
+             Empty) <+> ctx.name(this)
+      ) <+/> Group(
+        Text("locale") <+> ctx.name(this) <> "_signature" <+>
+          (if (decls.isEmpty) { Empty }
+           else { Text(" =") <>> Doc.stack(decls) }) <+/> "begin" <+/> "end"
+      )
+    )
+  }
+
   def layoutSilver(implicit ctx: Ctx): Doc =
     Group(
       Text("domain") <+> ctx.name(this) <>
@@ -31,6 +48,7 @@ trait AxiomaticDataTypeImpl[G]
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => layoutIsar
       case _ => Doc.spec(Show.lazily(layoutSpec(_)))
     }
 }

src/col/vct/col/ast/declaration/global/FunctionImpl.scala

@@ -47,6 +47,7 @@ trait FunctionImpl[G]
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => Empty
       case _ => Doc.spec(Show.lazily(layoutSpec(_)))
     }
 }

src/col/vct/col/ast/declaration/global/ProcedureImpl.scala

@@ -58,5 +58,6 @@ trait ProcedureImpl[G] extends ProcedureOps[G] {
       case Ctx.Silver => layoutSilver
       case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP => layoutC
       case Ctx.PVL | Ctx.Java => Doc.spec(Show.lazily(layoutSpec(_)))
+      case Ctx.Isar => Empty
     }
 }

src/col/vct/col/ast/declaration/singular/VariableImpl.scala

@@ -11,6 +11,7 @@ trait VariableImpl[G] extends VariableOps[G] with VariableFamilyOps[G] {
       case Ctx.C | Ctx.Cuda | Ctx.OpenCL | Ctx.CPP =>
         val (spec, decl) = t.layoutSplitDeclarator
         spec <+> decl <> ctx.name(this)
+      case Ctx.Isar => Text(ctx.name(this))
       case Ctx.PVL | Ctx.Java => t.show <+> ctx.name(this)
       case Ctx.Silver => Text(ctx.name(this)) <> ":" <+> t
     }

src/col/vct/col/ast/expr/apply/ADTFunctionInvocationImpl.scala

@@ -33,10 +33,20 @@ trait ADTFunctionInvocationImpl[G] extends ADTFunctionInvocationOps[G] {
   def layoutSilver(implicit ctx: Ctx): Doc =
     Group(Text(ctx.name(ref)) <> "(" <> Doc.args(args) <> ")")
 
+  def layoutIsar(implicit ctx: Ctx): Doc =
+    Group(
+      (if (args.nonEmpty)
+        Text("(") <> Text(ctx.name(ref)) <+> Doc.spread(args) <> ")"
+      else
+        Text(ctx.name(ref))
+        )
+    )
+
   override def precedence: Int = Precedence.POSTFIX
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => layoutIsar
       case _ => layoutSpec
     }
 }

src/col/vct/col/ast/expr/apply/FunctionInvocationImpl.scala

@@ -20,10 +20,17 @@ trait FunctionInvocationImpl[G] extends FunctionInvocationOps[G] {
       ) <> Doc.args(args) <> ")" <> DocUtil.givenYields(givenMap, yields)
     )
 
+  def layoutIsar(implicit ctx: Ctx): Doc =
+    Group((if (args.nonEmpty)
+             Text("(") <> Text(ctx.name(ref)) <+> Doc.spread(args) <> ")"
+           else
+             Text(ctx.name(ref))))
+
   override def precedence: Int = Precedence.POSTFIX
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => layoutIsar
       case _ => layoutSpec
     }
 

src/col/vct/col/ast/expr/binder/ExistsImpl.scala

@@ -25,10 +25,16 @@ trait ExistsImpl[G] extends ExistsOps[G] {
         layoutTriggers <>> body </> ")"
     )
 
+  def layoutIsar(implicit ctx : Ctx): Doc =
+    Group(
+      Text("∃") <+> Doc.spread(bindings) <+> "." <+> body
+    )
+
   override def precedence: Int = Precedence.ATOMIC
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => layoutIsar
       case _ => layoutSpec
     }
 }

src/col/vct/col/ast/expr/binder/ForallImpl.scala

@@ -25,10 +25,16 @@ trait ForallImpl[G] extends ForallOps[G] {
         layoutTriggers <>> body </> ")"
     )
 
+  def layoutIsar(implicit ctx : Ctx): Doc =
+    Group(
+      Text("∀") <+> Doc.spread(bindings) <+> "." <+> body
+    )
+
   override def precedence: Int = Precedence.ATOMIC
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => layoutIsar
       case _ => layoutSpec
     }
 }

src/col/vct/col/ast/expr/binder/LetImpl.scala

@@ -20,10 +20,16 @@ trait LetImpl[G] extends LetOps[G] {
         ")" <+> "in" <>> main </> ")"
     )
 
+  def layoutIsar(implicit ctx : Ctx): Doc =
+    Group(
+      Text("(") <> Text("let") <+> ctx.name(binding) <+> "=" <+> value <+> "in" <>> main <> Text(")")
+    )
+
   override def precedence: Int = Precedence.ATOMIC
   override def layout(implicit ctx: Ctx): Doc =
     ctx.syntax match {
       case Ctx.Silver => layoutSilver
+      case Ctx.Isar => layoutIsar
       case _ => layoutSpec
     }
 }

src/col/vct/col/ast/expr/literal/build/EitherLeftImpl.scala

@@ -9,5 +9,10 @@ trait EitherLeftImpl[G] extends EitherLeftOps[G] {
   override def t: Type[G] = TEither(e.t, TNothing())
 
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc = Text("Left(") <> e <> ")"
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => Text("Inl") <+> e
+      case _ => Text("Left(") <> e <> ")"
+    }
+  }
 }

src/col/vct/col/ast/expr/literal/build/EitherRightImpl.scala

@@ -9,5 +9,10 @@ trait EitherRightImpl[G] extends EitherRightOps[G] {
   override def t: Type[G] = TEither(TNothing(), e.t)
 
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc = Text("Right(") <> e <> ")"
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => Text("Inr") <+> e
+      case _ => Text("Right(") <> e <> ")"
+    }
+  }
 }

src/col/vct/col/ast/expr/literal/build/LiteralBagImpl.scala

@@ -9,6 +9,13 @@ trait LiteralBagImpl[G] extends LiteralBagOps[G] {
   override def t: Type[G] = TBag(element)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("bag<") <> element <> ">{" <> Doc.args(values) <> "}")
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar =>
+        if (values.isEmpty) { Group(Text("{#}")) }
+        else { Group(Text("{#") <+> Doc.args(values) <+> Text("#}")) }
+      case _ =>
+        Group(Text("bag<") <> element <> ">{" <> Doc.args(values) <> "}")
+    }
+  }
 }

src/col/vct/col/ast/expr/literal/build/LiteralMapImpl.scala

@@ -9,8 +9,26 @@ trait LiteralMapImpl[G] extends LiteralMapOps[G] {
   override def t: Type[G] = TMap(k, v)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
+
+  def layoutIsar(implicit ctx: Ctx): Doc = {
+    if (values.isEmpty) { Group(Text("Map.empty")) }
+    else {
+      Group(Text("[") <+> Doc.args(values.map { case (k, v) =>
+        k.show <+> "↦" <+> v
+      }) <+> Text("]"))
+    }
+  }
+
+  def layoutPvl(implicit ctx: Ctx): Doc =
     Group(Text("map<") <> k <> "," <+> v <> ">{" <> Doc.args(values.map {
       case (k, v) => k.show <+> "->" <+> v
     }) <> "}")
+
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => layoutIsar
+      case _ => layoutPvl
+    }
+
+  }
 }

src/col/vct/col/ast/expr/literal/build/LiteralSeqImpl.scala

@@ -9,6 +9,13 @@ trait LiteralSeqImpl[G] extends LiteralSeqOps[G] {
   override def t: Type[G] = TSeq(element)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("seq<") <> element <> ">{" <> Doc.args(values) <> "}")
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar =>
+        if (values.isEmpty) { Group(Text("[]")) }
+        else { Group(Text("[") <> Doc.args(values) <> Text(")")) }
+      case _ =>
+        Group(Text("seq<") <> element <> ">{" <> Doc.args(values) <> "}")
+    }
+  }
 }

src/col/vct/col/ast/expr/literal/build/LiteralSetImpl.scala

@@ -9,6 +9,14 @@ trait LiteralSetImpl[G] extends LiteralSetOps[G] {
   override def t: Type[G] = TSet(element)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("set<") <> element <> ">{" <> Doc.args(values) <> "}")
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar =>
+        if (values.isEmpty) { Group(Text("{}")) }
+        else { Group(Text("{") <> Doc.args(values) <> "}") }
+      case _ =>
+        Group(Text("set<") <> element <> ">{" <> Doc.args(values) <> "}")
+    }
+
+  }
 }

src/col/vct/col/ast/expr/literal/build/LiteralTupleImpl.scala

@@ -15,6 +15,12 @@ trait LiteralTupleImpl[G] extends ExprImpl[G] with LiteralTupleOps[G] {
     else { Seq(TupleTypeCount(this)) }
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("tuple<") <> Doc.args(ts) <> ">{" <> Doc.args(values) <> "}")
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => Group(Text("(") <> "," <> Doc.args(values) <> Text(")"))
+      case _ =>
+        Group(Text("tuple<") <> Doc.args(ts) <> ">{" <> Doc.args(values) <> "}")
+    }
+
+  }
 }

src/col/vct/col/ast/expr/literal/build/OptSomeImpl.scala

@@ -9,5 +9,11 @@ trait OptSomeImpl[G] extends OptSomeOps[G] {
   override def t: Type[G] = TOption(e.t)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc = Text("Some(") <> e <> ")"
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => Text("(Some") <+> e <> ")"
+      case _ => Text("Some(") <> e <> ")"
+    }
+
+  }
 }

src/col/vct/col/ast/expr/literal/build/OptSomeTypedImpl.scala

@@ -9,5 +9,11 @@ trait OptSomeTypedImpl[G] extends OptSomeTypedOps[G] {
   override def t: Type[G] = TOption(element)
 
   override def precedence: Int = Precedence.POSTFIX
-  override def layout(implicit ctx: Ctx): Doc = Text("Some(") <> e <> ")"
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => Text("(Some ") <> e <> ")"
+      case _ => Text("Some(") <> e <> ")"
+    }
+
+  }
 }

src/col/vct/col/ast/expr/literal/build/UntypedLiteralBagImpl.scala

@@ -11,6 +11,10 @@ trait UntypedLiteralBagImpl[G] extends UntypedLiteralBagOps[G] {
   override def t: Type[G] = TBag(elementType)
 
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc =
-    Group(Text("b{") <> Doc.args(values) <> "}")
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => Group(Text("{#") <+> Doc.args(values) <+> Text("#}"))
+      case _ => Group(Text("b{") <> Doc.args(values) <> "}")
+    }
+  }
 }

src/col/vct/col/ast/expr/literal/constant/BooleanValueImpl.scala

@@ -27,12 +27,26 @@ trait BooleanValueImpl[G] extends BooleanValueOps[G] {
       SharedLayoutElement('e'),
     )
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc =
+  def layoutDefault(implicit ctx: Ctx) =
     Text(
       orderedLayoutFixture.collect {
         case e @ SharedLayoutElement(_) => e;
         case e @ DedicatedLayoutElement(r, _) if r.toString == value.toString =>
           e
       }.map(_.textualData).mkString("")
     )
+
+  def layoutIsar(implicit ctx: Ctx) =
+    if (value)
+      Text("True")
+    else
+      Text("False")
+
+  override def layout(implicit ctx: Ctx): Doc = {
+    ctx.syntax match {
+      case Ctx.Isar => layoutIsar
+      case _ => layoutDefault
+    }
+
+  }
 }

src/col/vct/col/ast/expr/literal/constant/NoPermImpl.scala

@@ -9,5 +9,9 @@ trait NoPermImpl[G] extends NoPermOps[G] {
   override def t: Type[G] = TBoundedInt(0, 1)
 
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc = Text("none")
+  override def layout(implicit ctx: Ctx): Doc =
+    ctx.syntax match {
+      case Ctx.Isar => Text("0")
+      case _ => Text("none")
+    }
 }

src/col/vct/col/ast/expr/literal/constant/WritePermImpl.scala

@@ -9,5 +9,9 @@ trait WritePermImpl[G] extends WritePermOps[G] {
   override def t: Type[G] = TBoundedInt(1, 2)
 
   override def precedence: Int = Precedence.ATOMIC
-  override def layout(implicit ctx: Ctx): Doc = Text("write")
+  override def layout(implicit ctx: Ctx): Doc =
+    ctx.syntax match {
+      case Ctx.Isar => Text("1")
+      case _ => Text("write")
+    }
 }