package goblint-cil

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities for managing "concatenable lists" (clists). We often need to concatenate sequences, and using lists for this purpose is expensive. This module provides routines to manage such lists more efficiently. In this model, we never do cons or append explicitly. Instead we maintain the elements of the list in a special data structure. Routines are provided to convert to/from ordinary lists, and carry out common list operations.

type 'a clist =
  1. | CList of 'a list
    (*

    The only representation for the empty list. Try to use sparingly.

    *)
  2. | CConsL of 'a * 'a clist
    (*

    Do not use this a lot because scanning * it is not tail recursive

    *)
  3. | CConsR of 'a clist * 'a
  4. | CSeq of 'a clist * 'a clist
    (*

    We concatenate only two of them at this time. Neither is the empty clist. To be sure always use append to make these

    *)

The clist datatype. A clist can be an ordinary list, or a clist preceded or followed by an element, or two clists implicitly appended together

val toList : 'a clist -> 'a list

Convert a clist to an ordinary list

val fromList : 'a list -> 'a clist

Convert an ordinary list to a clist

val single : 'a -> 'a clist

Create a clist containing one element

val empty : 'a clist

The empty clist

val append : 'a clist -> 'a clist -> 'a clist

Append two clists

val checkBeforeAppend : 'a clist -> 'a clist -> bool

A useful check to assert before an append. It checks that the two lists * are not identically the same (Except if they are both empty)

val length : 'a clist -> int

Find the length of a clist

val map : ('a -> 'b) -> 'a clist -> 'b clist

Map a function over a clist. Returns another clist

val fold_left : ('acc -> 'a -> 'acc) -> 'acc -> 'a clist -> 'acc

A version of fold_left that works on clists

val iter : ('a -> unit) -> 'a clist -> unit

A version of iter that works on clists

val rev : ('a -> 'a) -> 'a clist -> 'a clist

Reverse a clist. The first function reverses an element.

val docCList : Pretty.doc -> ('a -> Pretty.doc) -> unit -> 'a clist -> Pretty.doc

A document for printing a clist (similar to docList)