Skip to content

Latest commit

 

History

History
333 lines (251 loc) · 9.18 KB

interpolations.md

File metadata and controls

333 lines (251 loc) · 9.18 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 symbols: inox.trees.Symbols = inox.trees.NoSymbols

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

val tpe = t"Boolean"
// tpe: Type = Boolean
val expr = e"1 + 1 == 2"
// expr: Expr = 1 + 1 == 2

It is also possible to embed types and expressions:

e"let x: $tpe = $expr in !x"
// res0: Expr = val x: Boolean = 1 + 1 == 2
// ¬x

Syntax

Literals

Boolean literals

e"true"
// res1: Expr = true
e"false"
// res2: Expr = false

Numeric literal

e"1"
// res3: Expr = 1

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

e"1".getType
// res4: Type = BigInt

It is however possible to annotate the desired type.

e"1 : Int".getType
// res5: Type = Int
e"1 : Real".getType
// res6: Type = Real

Real literals

e"3.75"
// res7: Expr = 15/4

String literals

e"'Hello world!'"
// res8: Expr = "Hello world!"

Character literals

e"`a`"
// res9: Expr = 'a'

Arithmetic

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

e"1 + 2 * 5 + 6 - 7 / 17"
// res10: Expr = ((1 + 2 * 5) + 6) - 7 / 17

Conditionals

e"if (1 == 2) 'foo' else 'bar'"
// res11: Expr = if (1 == 2) {
//   "foo"
// } else {
//   "bar"
// }

Let bindings

e"let word: String = 'World!' in concatenate('Hello ', word)"
// res12: Expr = val word: String = "World!"
// "Hello " + word

Lambda expressions

e"lambda x: BigInt, y: BigInt. x + y"
// res13: Expr = (x: BigInt, y: BigInt) => x + y

It is also possible to use the Unicode λ symbol.

e"λx: BigInt, y: BigInt. x + y"
// res14: Expr = (x: BigInt, y: BigInt) => x + y

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

e"lambda x. x * 0.5"
// res15: Expr = (x: Real) => x * 1/2

Quantifiers

Universal Quantifier

e"forall x: Int. x > 0"
// res16: Expr = ∀x: Int. (x > 0)
e"∀x. x || true"
// res17: Expr = ∀x: Boolean. (x || true)

Existential Quantifier

e"exists x: BigInt. x < 0"
// res18: Expr = ¬∀x: BigInt. ¬(x < 0)
e"∃x, y. x + y == 0"
// res19: Expr = ¬∀x: BigInt, y: BigInt. (x + y ≠ 0)

Choose

e"choose x. x * 3 < 17"
// res20: Expr = choose((x: BigInt) => x * 3 < 17)
e"choose x: String. true"
// res21: 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