1.4. Built-in data types¶
DynSem has built-in support for the following types:
1.4.1. Numbers¶
-
Premises on numbers
- a == b
- Equality check. Fails if the two numbers are not equal.
a
andb
may be bound variables or number literals. - a != b
- Inequality check. Fails if the two numbers are equal.
a
andb
may be bound variables or number literals. - a => b
- Equivalent to
==
ifb
is a number literal. Binds new variableb
to the value ofa
ifb
is an unbound variable. Invalid ifb
is a bound variable. - a =!=> b
- Equivalent to
!=
ifb
is a number literal. Invalid ifb
is a variable (bound or unbound). - case a of { b => … }
- Switch-like premise for multiple cases.
a
must either be a number literal or a bound variable.b
must either be a number literal or an unbound variable.
One can write reduction rules directly on numbers, for example:
module nums
signature
arrows
Int -inc-> Int
rules
3 -inc-> 4
Int¶
The sort Int
denotes positive and negative whole numbers, e.g. 3, 99, -49
. The range of is the same as Java’s int
range: -2,147,483,648 to 2,147,483,647.
Integers can be typed literally, read or written from variables and matched against. Int terms are coerceable to Float where needed.
Long¶
Similar to Int, except for the range being the same as Java’s long
range: -9,223,372,036,854,775,808 to 9,223,372,036,854,775,807.
Long values are coercible to Real where needed.
Float¶
The sort Float
denotes positive and negative decimal numbers, e.g. 3.14
, 9.99
, -42.42
. The range is the same as Java’s float
range. Float
inherits the precision of Java’s float
.
All Int operations are supported on Float
. Note that due to precision issues equality/match checks between decimal vaues may unexpectedly fail.
Float values are coercible to Real where needed.
1.4.2. Bool¶
The sort Bool
denotes logical values. Values are either true
or false
.
-
Premises on booleans
- a == b
- Equality check. Fails if the two booleans are not equal.
a
andb
may be bound variables or boolean literals. - a != b
- Inequality check. Fails if the two boolean are equal.
a
andb
may be bound variables or boolean literals. - a => b
- Equivalent to
==
ifb
is a boolean literal. Binds new variableb
to the value ofa
ifb
is an unbound variable. Invalid ifb
is a bound variable. - a =!=> b
- Equivalent to
!=
ifb
is a boolean literal. Invalid ifb
is a variable (bound or unbound). - case a of { b => … }
- Switch-like premise for multiple cases.
a
must either be a boolean literal or a bound variable.b
must either be a boolean literal or an unbound variable.
There are no built-in logical operations on the sort Bool
. One can define meta-functions for these operations, for example:
module booleans
signature
arrows
not(Bool) --> Bool
rules
not(true) --> false
not(false) --> true
One can write reduction rules directly on boolean literals, for example:
module booleans
signature
arrows
Bool -not-> Bool
rules
true -not-> false
false -not-> true
1.4.3. String¶
The String
sort denotes ASCII strings. The maximum length of a string is the maximum size of an Int
.
-
string operations
- building: “hello”, “hello world”
- Builds a string from a literal
- matching: a => “hello”, a =!=> “hello”
- see
==
and!=
below - s1 == s2
- Compare strings
s1
ands2
for equality. Fail if the strings are not identical. - s1 != s2
- Compare strings
s1
ands2
for equality. Fail if the strings are identical.
1.4.4. List¶
The List
terms denote list terms of homogenously typed terms. Use of a list sort must specify the sort of the contained elements. For example, the following declares a constructor foo
having a list of integers as child:
module lists
signature
sorts
F
constructors
foo: List(Int) -> F
-
list operations
- building: [], [a, b], [a, b | xs]
Build an empty list, a list of two elements and a list of two or more elements, respectively. If
a
,b
and/orxs
are variables they must be bound variables. Ifa
is of sortS
thenb
has to be of sortS
andxs
must be of sortList(S)
or an empty list literal. Empty list literals -[]
- are coercible to any list sort.Examples of list build premises:
[] => x [1, 2, 3] => x [1, 2 | []] => x [1, 2 | [3, 4]] => x [a, b | [a, b]] => x
- matching: [], [a, b], [a, b, c | xs], [_, _ | xs]
Matches an empty list, a list of two elements, a list of three or more elements and a list of two or more elements, respectively. All variables in a list match must be unbound variables. Variables occuring in the pattern will be bound if the entire pattern match succeeds. If any of
a
,b
,c
,xs
is a term pattern (i.e. not a variable) then a pattern match will be attempted for that pattern.Examples of list pattern matching premises:
t => [] t => [_, _] t => [_, _ | _] t => [1, 2] t => [a, b | [c, d | xs]]
- l1 == l2
- Check lists
l1
andl2
for equality. Two lists are equal if they are of the same type, they have the same length and being element-wise equal. Premise fails if the two lists are not equal. - l1 != l2
- Check lists
l1
andl2
for inequality. See above for a definition of list equality. Premise fails if the two lists are equal.
- indexed access: l1[idx]
- Retrieves the element at index
idx
in the listl1
. Fails if the index is out of bounds. - concat: l1 ++ l2
- Concatenates two lists of the same type: if the type of
l1
isList(S)
, then the type ofl2
has to beList(S)
, unlessl2
is an empty list literal. The elements in thel2
list will be appended, in order, to the elements ofl1
. - reverse: `l1
Reverses the list
l1
. Example:`[1, 2, 3] // => [3, 2, 1] `[] // => [] `[1, 2, 3 | `[4, 5]] // => [4, 5, 3, 2, 1]
One may write reduction rules directly on list literals, but the type of the list has to be explicitly specified:
module lists
signature
arrows
List(Int) -empty-> Bool
rules
[] : List(Int) -empty-> true
[_|_] : List(Int) -empty-> false
1.4.5. Map¶
The sort Map
denotes associative arrays, or dictionaries. A use of the map sort must declare the types of keys and the type of values. The following declares the sort Env
as an alias to the sort mapping strings to integers:
signature
sort aliases
Env = Map(String, Int)
Note
Maps are immutable. Adding or removing entries from a map does not modify the existent map, instead it creates a new map.
-
map operations
- building: {}, {k1 |–> v1}, {k1 |–> v1, k2 |–> v2, …}
- Build an empty map, a map with one entry and a map with multiple entries, respectively. All appearing variables must be bound. All keys must be of the same type, and all values must be of the same type. Results in a new map, the old map is unmodified.
- extending: {k1 |–> v1, map}, {map, k1 |–> v1}
- Extend the map represented by variable
map
with a new binding from keyk1
to valuev1
. Entries on the left map replace entries with the same key on the right. Multiple additions can be performed at once:{k1 |--> v1, map, k2 |--> v2}
. This is equivalent to writing:{k1 |--> v1, {map, k2 |--> v2}}
. Multiple maps can be merged into one:{map1, map2, map3}
. Again, the left entries replace the right entries. It is equivalent to writing:{map1, {map2, map3}}
. The result is always a new map, the old map(s) remain(s) unmodified. - removing: map1 \ k1
- Return a new map containing all entries in map
map1
except for the entry with keyk1
. Fails ifmap1
has no entry for keyk1
. Mapmap1
remains unmodified. - access: map1[k1]
- Return the value associated with key
k1
in mapmap1
. Fails ifmap1
does not have an entry for keyk1
. - contains: map1[k1?]
- Check whether map
map1
has an entry for keyk1
. Returntrue
if an entry exists,false
otherwise. - matching
- Pattern matching is not possible on maps
Defining rules directly on maps is possible, but the type of the map has to be explicitly specified in the rule:
signature
arrows
Map(String, Int) -global-> Int
rules
m : Map(String, Int) -global-> m["global"]
1.4.6. Tuple¶
The Tuple
sort denotes pairs of terms of arbitrary (higher than 0) arity. Tuple sort usages must be accompanied by declarations of the types of their elements. For example:
signature
sort aliases
T = (S1 * S2 * S3)
declares sort T
to be an alias of the 3-tuple of terms of type S1
, S2
and S3
, respectively.
-
tuple operations
- building: (t1, t2, …)
- Build a tuple literal. All variables appearing in the construction must be bound. If the types of children
t1
,t2
, … areS1
,S2
, …, respectively, then the type of the resulting tuple is(S1 * S2 * ...)
. - matching: (p1, p2, p3)
- Match a term against a 3-tuple pattern. The patterns
p1
,p2
,p3
are matched against the respective child of the incoming tuple. A tuple pattern match succeeds if the term matched is a tuple of equal arity and if the sub-pattern matches succeed. Variables appearing in the pattern must be unbound. Variables appearing in the pattern will be bound if the pattern match succeeds.
It is possible to define rules directly on tuple literals, but the type of the tuple has to be explicitly specified in the rule:
signature
arrows
(Bool * Bool) -or-> Bool
rules
(true, _) : (Bool * Bool) -or-> true
(_, true) : (Bool * Bool) -or-> true
(false, false) : (Bool * Bool) -or-> false