# Sequences

The sort constructor `Seq`

can be used to create sequences over any base sort.
For example, a sequence of integers is `(Seq Int)`

, and `(Seq Unicode)`

is the definition of `String`

.

## Operations

Most string operations have corresponding sequence variants. In addition, there are operations to create a unit sequence and the empty sequence over any base sort.

Operation | Brief description |
---|---|

`(seq.unit elem)` | Sequence with a single element `elem` |

`(as seq.empty (Seq Int))` | The empty sequence of integers |

`(seq.++ a b c)` | Concatenation of one or more sequences |

`(seq.len s)` | Sequence length. Returns an integer |

`(seq.extract s offset length)` | Retrieves sub-sequence of `s` at `offset` |

`(seq.indexof s sub [offset])` | Retrieves first position of `sub` in `s` , -1 if there are no occurrences |

`(seq.at s offset)` | Sub-sequence of length 1 at `offset` in `s` |

`(seq.nth s offset)` | Element at `offset` in `s` . If `offset` is out of bounds the result is under-specified. In other words, it is treated as a fresh variable |

`(seq.contains s sub)` | Does `s` contain the sub-sequence `sub` ? |

`(seq.prefixof pre s)` | Is `pre` a prefix of `s` ? |

`(seq.suffixof suf s)` | Is `suf` a suffix of `s` ? |

`(seq.replace s src dst)` | Replace the first occurrence of `src` by `dst` in `s` |

`(seq.map fn s)` | Map function (an expression of sort `(Array S T)` ) on sequence `s` of sort `(Seq S)` |

`(seq.mapi fn o s)` | Map function (an expression of sort `(Array Int S T)` ) on offset `o` and sequence `s` of sort `(Seq S)` |

`(seq.fold_left fn b s)` | Fold function (an expression of sort `(Array T S T)` ) on initial value `b` of sort `T` and sequence `s` of sort `(Seq S)` |

`(seq.fold_lefti fn o b s)` | Fold function (an expression of sort `(Array Int T S T)` ) on offset `o` , initial value `b` of sort `T` and sequence `s` of sort `(Seq S)` |

A few operations are also overloaded.

Overloaded operations | Base form |
---|---|

`seq.foldl` | `seq.fold_left` |

`seq.foldli` | `seq.fold_lefti` |

## Sequence Examples

When inserting `b`

at or after position 8, but before the length of the string, which is at least 10,
then the resulting string has the same length, and either character 8 or 9 are unchanged.

## Map and Fold

The functions map and fold (left) are modeled after the functions found in ML languages.
Our version of `fold_lefti`

, where the current index of the sequence element is available is slightly different, it takes as an additional argument
also an offset. The advantage of including the offset is that it is easier to formulate how the function decomposes over sequence concatenation.
The decision procedure for map and fold behaves similar to recursive function unfolding, thus they are mostly effective when
there is a finite satisfying model or the proof of unsatisfiability does not require inventing auxiliary inductive relations.