Use mdoc in documentation

doc/API.md

@@ -1,7 +1,7 @@
 Inox API
 ========
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Trees
 -----

doc/interpolations.md

@@ -1,7 +1,7 @@
 Inox String Interpolation
 =========================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 # Table of Content
 
@@ -44,26 +44,30 @@ import inox._
 import inox.trees._
 import inox.trees.interpolator._
 
-implicit val symbols: trees.Symbols = trees.NoSymbols
+implicit val symbols: inox.trees.Symbols = inox.trees.NoSymbols
 ```
 
 Once imported, it is possible to build Inox types and expressions using a friendlier syntax:
 
 ```scala
-scala> val tpe = t"Boolean"
-tpe: inox.trees.interpolator.trees.Type = Boolean
-
-scala> val expr = e"1 + 1 == 2"
-expr: inox.trees.interpolator.trees.Expr = 1 + 1 == 2
+val tpe = t"Boolean"
+// tpe: Type = Boolean
+val expr = e"1 + 1 == 2"
+// expr: Expr = Equals(
+//   Plus(IntegerLiteral(1), IntegerLiteral(1)),
+//   IntegerLiteral(2)
+// )
 ```
 
 It is also possible to embed types and expressions:
 
 ```scala
-scala> e"let x: $tpe = $expr in !x"
-res0: inox.trees.interpolator.trees.Expr =
-val x: Boolean = 1 + 1 == 2
-¬x
+e"let x: $tpe = $expr in !x"
+// res0: Expr = Let(
+//   ValDef(x, Boolean, List()),
+//   Equals(Plus(IntegerLiteral(1), IntegerLiteral(1)), IntegerLiteral(2)),
+//   Not(Variable(x, Boolean, List()))
+// )
 ```
 
 <a name="syntax"></a>
@@ -76,62 +80,61 @@ val x: Boolean = 1 + 1 == 2
 ### Boolean literals
 
 ```scala
-scala> e"true"
-res1: inox.trees.interpolator.trees.Expr = true
-
-scala> e"false"
-res2: inox.trees.interpolator.trees.Expr = false
+e"true"
+// res1: Expr = BooleanLiteral(true)
+e"false"
+// res2: Expr = BooleanLiteral(false)
 ```
 
 <a name="numeric-literals"></a>
 ### Numeric literal
 
 ```scala
-scala> e"1"
-res3: inox.trees.interpolator.trees.Expr = 1
+e"1"
+// res3: Expr = IntegerLiteral(1)
 ```
 
 Note that the type of numeric expressions is inferred. In case of ambiguity, `BigInt` is chosen by default.
 
 ```scala
-scala> e"1".getType
-res4: inox.trees.interpolator.trees.Type = BigInt
+e"1".getType
+// res4: Type = BigInt
 ```
 
 It is however possible to annotate the desired type.
 
 ```scala
-scala> e"1 : Int".getType
-res5: inox.trees.interpolator.trees.Type = Int
+e"1 : Int".getType
+// res5: Type = BVType(true, 32)
 ```
 
 ```scala
-scala> e"1 : Real".getType
-res6: inox.trees.interpolator.trees.Type = Real
+e"1 : Real".getType
+// res6: Type = Real
 ```
 
 <a name="real-literals"></a>
 #### Real literals
 
 ```scala
-scala> e"3.75"
-res7: inox.trees.interpolator.trees.Expr = 15/4
+e"3.75"
+// res7: Expr = FractionLiteral(15, 4)
 ```
 
 <a name="string-literals"></a>
 ### String literals
 
 ```scala
-scala> e"'Hello world!'"
-res8: inox.trees.interpolator.trees.Expr = "Hello world!"
+e"'Hello world!'"
+// res8: Expr = StringLiteral("Hello world!")
 ```
 
 <a name="character-literals"></a>
 ### Character literals
 
 ```scala
-scala> e"`a`"
-res9: inox.trees.interpolator.trees.Expr = 'a'
+e"`a`"
+// res9: Expr = CharLiteral('a')
 ```
 
 <a name="arithmetic"></a>
@@ -140,53 +143,69 @@ res9: inox.trees.interpolator.trees.Expr = 'a'
 Arithmetic operators are infix and have there usual associativity and priority.
 
 ```scala
-scala> e"1 + 2 * 5 + 6 - 7 / 17"
-res10: inox.trees.interpolator.trees.Expr = ((1 + 2 * 5) + 6) - 7 / 17
+e"1 + 2 * 5 + 6 - 7 / 17"
+// res10: Expr = Minus(
+//   Plus(
+//     Plus(IntegerLiteral(1), Times(IntegerLiteral(2), IntegerLiteral(5))),
+//     IntegerLiteral(6)
+//   ),
+//   Division(IntegerLiteral(7), IntegerLiteral(17))
+// )
 ```
 
 <a name="conditionals"></a>
 ## Conditionals
 
 ```scala
-scala> e"if (1 == 2) 'foo' else 'bar'"
-res11: inox.trees.interpolator.trees.Expr =
-if (1 == 2) {
-  "foo"
-} else {
-  "bar"
-}
+e"if (1 == 2) 'foo' else 'bar'"
+// res11: Expr = IfExpr(
+//   Equals(IntegerLiteral(1), IntegerLiteral(2)),
+//   StringLiteral("foo"),
+//   StringLiteral("bar")
+// )
 ```
 
 <a name="let-bindings"></a>
 ## Let bindings
 
 ```scala
-scala> e"let word: String = 'World!' in concatenate('Hello ', word)"
-res12: inox.trees.interpolator.trees.Expr =
-val word: String = "World!"
-"Hello " + word
+e"let word: String = 'World!' in concatenate('Hello ', word)"
+// res12: Expr = Let(
+//   ValDef(word, String, List()),
+//   StringLiteral("World!"),
+//   StringConcat(StringLiteral("Hello "), Variable(word, String, List()))
+// )
 ```
 
 <a name="lambda-expressions"></a>
 ## Lambda expressions
 
 ```scala
-scala> e"lambda x: BigInt, y: BigInt. x + y"
-res13: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y
+e"lambda x: BigInt, y: BigInt. x + y"
+// res13: Expr = Lambda(
+//   List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
+//   Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List()))
+// )
 ```
 
 It is also possible to use the Unicode `λ` symbol.
 
 ```scala
-scala> e"λx: BigInt, y: BigInt. x + y"
-res14: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y
+e"λx: BigInt, y: BigInt. x + y"
+// res14: Expr = Lambda(
+//   List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
+//   Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List()))
+// )
 ```
 
 Type annotations can be omitted for any of the parameters if their type can be inferred.
 
 ```scala
-scala> e"lambda x. x * 0.5"
-res15: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2
+e"lambda x. x * 0.5"
+// res15: Expr = Lambda(
+//   List(ValDef(x, Real, List())),
+//   Times(Variable(x, Real, List()), FractionLiteral(1, 2))
+// )
 ```
 
 <a name="quantifiers"></a>
@@ -196,33 +215,60 @@ res15: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2
 ### Universal Quantifier
 
 ```scala
-scala> e"forall x: Int. x > 0"
-res16: inox.trees.interpolator.trees.Expr = ∀x: Int. (x > 0)
-
-scala> e"∀x. x || true"
-res17: inox.trees.interpolator.trees.Expr = ∀x: Boolean. (x || true)
+e"forall x: Int. x > 0"
+// res16: Expr = Forall(
+//   List(ValDef(x, Int, List())),
+//   GreaterThan(
+//     Variable(x, BVType(true, 32), List()),
+//     BVLiteral(true, BitSet(), 32)
+//   )
+// )
+e"∀x. x || true"
+// res17: Expr = Forall(
+//   List(ValDef(x, Boolean, List())),
+//   Or(List(Variable(x, Boolean, List()), BooleanLiteral(true)))
+// )
 ```
 
 <a name="existential-quantifiers"></a>
 ### Existential Quantifier
 
 ```scala
-scala> e"exists x: BigInt. x < 0"
-res18: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt. ¬(x < 0)
-
-scala> e"∃x, y. x + y == 0"
-res19: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)
+e"exists x: BigInt. x < 0"
+// res18: Expr = Not(
+//   Forall(
+//     List(ValDef(x, BigInt, List())),
+//     Not(LessThan(Variable(x, BigInt, List()), IntegerLiteral(0)))
+//   )
+// )
+e"∃x, y. x + y == 0"
+// res19: Expr = Not(
+//   Forall(
+//     List(ValDef(x, BigInt, List()), ValDef(y, BigInt, List())),
+//     Not(
+//       Equals(
+//         Plus(Variable(x, BigInt, List()), Variable(y, BigInt, List())),
+//         IntegerLiteral(0)
+//       )
+//     )
+//   )
+// )
 ```
 
 <a name="choose"></a>
 ## Choose
 
 ```scala
-scala> e"choose x. x * 3 < 17"
-res20: inox.trees.interpolator.trees.Expr = choose((x: BigInt) => x * 3 < 17)
-
-scala> e"choose x: String. true"
-res21: inox.trees.interpolator.trees.Expr = choose((x: String) => true)
+e"choose x. x * 3 < 17"
+// res20: Expr = Choose(
+//   ValDef(x, BigInt, List()),
+//   LessThan(
+//     Times(Variable(x, BigInt, List()), IntegerLiteral(3)),
+//     IntegerLiteral(17)
+//   )
+// )
+e"choose x: String. true"
+// res21: Expr = Choose(ValDef(x, String, List()), BooleanLiteral(true))
 ```
 
 <a name="primitives"></a>

doc/trees.md

@@ -1,7 +1,7 @@
 Extending the Trees
 ===================
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Inox trees are designed to be extensible with minimal pain and maximal gain.
 By extending the [```Trees```](/src/main/scala/inox/ast/Trees.scala) trait,

doc/tutorial.md

@@ -1,7 +1,7 @@
 Tutorial
 ========
 
-[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation source are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Let us consider the problem of checking whether the following size function on a list is always greater or equal to 0.
 ```scala
@@ -157,7 +157,7 @@ val sizeFunction = mkFunDef(size)("A") { case Seq(tp) => (
 
 A symbol table in Inox is an instance of `Symbols`. The easiest way to construct one is to use
 ```scala
-implicit val symbols: trees.Symbols = {
+implicit val symbols: inox.trees.Symbols = {
   NoSymbols
     .withFunctions(Seq(sizeFunction))
     .withSorts(Seq(listSort))

src/main/doc/API.md

@@ -1,7 +1,7 @@
 Inox API
 ========
 
-[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `tut`.)
+[//]: # (The documentation sources are stored in src/main/doc/, while doc/ contains the autogenerated version by `mdoc`.)
 
 Trees
 -----