Skip to content

interpolations.md

Latest commit

 

History

History
350 lines (260 loc) · 10.2 KB

interpolations.md

File metadata and controls

350 lines (260 loc) · 10.2 KB
Raw

Inox String Interpolation

Table of Content

Introduction

In this document, we describe the string interpolation facility offered in Inox. String interpolations make it possible to build and deconstruct Inox types and expressions using a succinct and expressive language. Throughout this document, we will describe the syntax of this language and its primitive constructs.

Importing the interpolator

The first step to use this feature is to import it. The string interpolator is located within the Symbols class.

import inox._
import inox.trees._
import inox.trees.interpolator._

implicit val mySymbols = NoSymbols

Once imported, it is possible to build Inox types and expressions using a friendlier syntax:

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

It is also possible to embed types and expressions:

scala> e"let x: $tpe = $expr in !x"
res1: inox.trees.interpolator.trees.Expr =
val x: Boolean = 1 + 1 == 2
¬x

Syntax

Literals

Boolean literals

scala> e"true"
res2: inox.trees.interpolator.trees.Expr = true

scala> e"false"
res3: inox.trees.interpolator.trees.Expr = false

Numeric literal

scala> e"1"
res4: inox.trees.interpolator.trees.Expr = 1

Note that the type of numeric expressions is inferred. In case of ambiguity, BigInt is chosen by default.

scala> val bigIntLit = e"1"
bigIntLit: inox.trees.interpolator.trees.Expr = 1

scala> bigIntLit.getType
res5: inox.trees.interpolator.trees.Type = BigInt

It is however possible to annotate the desired type.

scala> val intLit = e"1 : Int"
intLit: inox.trees.interpolator.trees.Expr = 1

scala> intLit.getType
res6: inox.trees.interpolator.trees.Type = Int
scala> val realLit = e"1 : Real"
realLit: inox.trees.interpolator.trees.Expr = 1

scala> realLit.getType
res7: inox.trees.interpolator.trees.Type = Real

Real literals

scala> e"3.75"
res8: inox.trees.interpolator.trees.Expr = 15/4

String literals

scala> e"'Hello world!'"
res9: inox.trees.interpolator.trees.Expr = "Hello world!"

Character literals

scala> e"`a`"
res10: inox.trees.interpolator.trees.Expr = 'a'

Arithmetic

Arithmetic operators are infix and have there usual associativity and priority.

scala> e"1 + 2 * 5 + 6 - 7 / 17"
res11: inox.trees.interpolator.trees.Expr = ((1 + 2 * 5) + 6) - 7 / 17

Conditionals

scala> e"if (1 == 2) 'foo' else 'bar'"
res12: inox.trees.interpolator.trees.Expr =
if (1 == 2) {
  "foo"
} else {
  "bar"
}

Let bindings

scala> e"let word: String = 'World!' in concatenate('Hello ', word)"
res13: inox.trees.interpolator.trees.Expr =
val word: String = "World!"
"Hello " + word

Lambda expressions

scala> e"lambda x: BigInt, y: BigInt. x + y"
res14: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y

It is also possible to use the Unicode λ symbol.

scala> e"λx: BigInt, y: BigInt. x + y"
res15: inox.trees.interpolator.trees.Expr = (x: BigInt, y: BigInt) => x + y

Type annotations can be omitted for any of the parameters if their type can be inferred.

scala> e"lambda x. x * 0.5"
res16: inox.trees.interpolator.trees.Expr = (x: Real) => x * 1/2

Quantifiers

Universal Quantifier

scala> e"forall x: Int. x > 0"
res17: inox.trees.interpolator.trees.Expr = ∀x: Int. (x > 0)

scala> e"∀x. x || true"
res18: inox.trees.interpolator.trees.Expr = ∀x: Boolean. (x || true)

Existential Quantifier

scala> e"exists x: BigInt. x < 0"
res19: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt. ¬(x < 0)

scala> e"∃x, y. x + y == 0"
res20: inox.trees.interpolator.trees.Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)

Choose

scala> e"choose x. x * 3 < 17"
res21: inox.trees.interpolator.trees.Expr = choose((x: BigInt) => x * 3 < 17)

scala> e"choose x: String. true"
res22: inox.trees.interpolator.trees.Expr = choose((x: String) => true)

Primitives

Strings

Literal Syntax

''
'hello world'
'hey!'

Functions

Function Type Description Inox Constructor
length String => BigInt Returns the length of the string. StringLength
concatenate (String, String) => String Returns the concatenation of the two strings. StringConcat
substring (String, BigInt, BigInt) => String Returns the substring from the first index inclusive to the second index exclusive. SubString

Operators

Operator Type Associativity Precedence Description Inox Constructor
++ (String, String) => String Left-associative ??? Returns the concatenation of the two strings. StringConcat

Sets

Constructor

Constructor Description Inox Constructor
Set[A](elements: A*) Returns a set containing the given elements. FiniteSet

Literal Syntax

{}
{1, 2, 3}
{'foo', 'bar', 'baz'}

Functions

Function Type Description Inox Constructor
contains[A] (Set[A], A) => Boolean Returns true if the given set contains the given element, false otherwise. ElementOfSet
add[A] (Set[A], A) => Set[A] Returns the set with an element added. SetAdd
subset[A] (Set[A], Set[A]) => Boolean Returns true if the first set is a subset of the second, false otherwise. SubsetOf
union[A] (Set[A], Set[A]) => Set[A] Returns the unions of the two sets. SetUnion
intersection[A] (Set[A], Set[A]) => Set[A] Returns the intersection of the two sets. SetIntersection
difference[A] (Set[A], Set[A]) => Set[A] Returns the elements of the first set minus the elements of the second set. SetDifference

Operators

Operator Type Associativity Precedence Description Inox Constructor
∈ (A, Set[A]) => Boolean Left-associative ??? Returns true if the element is part of the set, false otherwise. ElementOfSet
⊆ (Set[A], Set[A]) => Boolean Left-associative ??? Returns true if the first set is a subset of the second, false otherwise. SubsetOf
∪ (A, Set[A]) => Boolean Left-associative ??? Returns the unions of the two sets. SetUnion
∩ (A, Set[A]) => Boolean Left-associative ??? Returns the intersection of the two sets. SetIntersection
∖ (A, Set[A]) => Boolean Left-associative ??? Returns the elements of the first set minus the elements of the second set. SetDifference

Bags

Constructor

Constructor Description Inox Constructor
Bag[A](bindings: (A -> BigInt)*) Returns a bag containing the given bindings. FiniteBag

Literal Syntax

{1 -> 2, 2 -> 4, 3 -> 6}
{'foo' -> 5, 'bar' -> 2, 'baz' -> 2}

Functions

Function Type Description Inox Constructor
multiplicity[A] (Bag[A], A) => BigInt Returns the number of occurrences in the given bag of the given value. MultiplicityInBag
bagAdd[A] (Bag[A], A) => Bag[A] Returns the bag with an element added. BagAdd
bagUnion[A] (Bag[A], Bag[A]) => Bag[A] Returns the unions of the two bags. BagUnion
bagIntersection[A] (Bag[A], Bag[A]) => Bag[A] Returns the intersection of the two bags. BagIntersection
bagDifference[A] (Bag[A], Bag[A]) => Bag[A] Returns the elements of the first bag minus the elements of the second bag. BagDifference

Maps

Constructor

Constructor Description Inox Constructor
Map[A](default: A, bindings: (A -> BigInt)*) Returns a map with default value default containing the given bindings. FiniteMap

Literal syntax

{*: Int -> 42}
{* -> '???', 'hello' -> 'HELLO', 'world' -> 'WORLD'}

Functions

Function Type Description Inox Constructor
apply[K, V] (Map[K, V], K) => V Returns the value associated to the given key. MapApply
updated[K, V] (Map[K, V], K, V) => Map[K, V] Returns the map with a bidding from the key to the value added. MapUpdated