kdrag.theories.list

Algebraic datatype of lists.

You may prefer using theories.seq which offers more builtin support for things like associativity.

Functions

Cons(x, xs)	Helper to construct Cons values >>> Cons(1, Nil(smt.IntSort())) Cons(1, Nil)
List(sort)	Build List sort >>> IntList = List(smt.IntSort()) >>> IntList.Cons(1, IntList.Nil) Cons(1, Nil)
Nil(sort)	Helper to construct Nil values >>> Nil(smt.IntSort()) Nil
Unit(x)	Helper to create Unit values >>> Unit(42) Cons(42, Nil) >>> Unit(42).sort() List_Int
list(*args)	Helper to construct List values >>> list(1, 2, 3) Cons(1, Cons(2, Cons(3, Nil)))

kdrag.theories.list.Cons(x: ExprRef, xs: DatatypeRef) → DatatypeRef

Helper to construct Cons values >>> Cons(1, Nil(smt.IntSort())) Cons(1, Nil)

Parameters:

• x (ExprRef)

• xs (DatatypeRef)

Return type:

DatatypeRef

kdrag.theories.list.List(sort: SortRef) → DatatypeSortRef

Build List sort >>> IntList = List(smt.IntSort()) >>> IntList.Cons(1, IntList.Nil) Cons(1, Nil)

Parameters:

sort (SortRef)

Return type:

DatatypeSortRef

kdrag.theories.list.Nil(sort: SortRef) → DatatypeRef

Helper to construct Nil values >>> Nil(smt.IntSort()) Nil

Parameters:

sort (SortRef)

Return type:

DatatypeRef

kdrag.theories.list.Unit(x: ExprRef) → DatatypeRef

Helper to create Unit values >>> Unit(42) Cons(42, Nil) >>> Unit(42).sort() List_Int

Parameters:

x (ExprRef)

Return type:

DatatypeRef

kdrag.theories.list.list(*args: ExprRef) → DatatypeRef

Helper to construct List values >>> list(1, 2, 3) Cons(1, Cons(2, Cons(3, Nil)))

Parameters:

args (ExprRef)

Return type:

DatatypeRef

"""
Algebraic datatype of lists.

You may prefer using theories.seq which offers more builtin support for things like associativity.
"""

import kdrag as kd
import functools
import kdrag.smt as smt


@functools.cache
def List(sort: smt.SortRef) -> smt.DatatypeSortRef:
    """
    Build List sort
    >>> IntList = List(smt.IntSort())
    >>> IntList.Cons(1, IntList.Nil)
    Cons(1, Nil)
    """
    dt = kd.Inductive("List_" + sort.name())
    dt.declare("Nil")
    dt.declare("Cons", ("head", sort), ("tail", dt))
    return dt.create()


def list(*args: smt.ExprRef) -> smt.DatatypeRef:
    """
    Helper to construct List values
    >>> list(1, 2, 3)
    Cons(1, Cons(2, Cons(3, Nil)))
    """
    if len(args) == 0:
        raise ValueError("list() requires at least one argument")
    LT = List(smt._py2expr(args[0]).sort())
    acc = LT.Nil
    for a in reversed(args):
        acc = LT.Cons(a, acc)
    return acc


def Cons(x: smt.ExprRef, xs: smt.DatatypeRef) -> smt.DatatypeRef:
    """
    Helper to construct Cons values
    >>> Cons(1, Nil(smt.IntSort()))
    Cons(1, Nil)
    """
    LT = List(smt._py2expr(x).sort())
    return LT.Cons(x, xs)


def Nil(sort: smt.SortRef) -> smt.DatatypeRef:
    """
    Helper to construct Nil values
    >>> Nil(smt.IntSort())
    Nil
    """
    return List(sort).Nil


def Unit(x: smt.ExprRef) -> smt.DatatypeRef:
    """
    Helper to create Unit values
    >>> Unit(42)
    Cons(42, Nil)
    >>> Unit(42).sort()
    List_Int
    """
    x = smt._py2expr(x)
    LT = List(x.sort())
    return LT.Cons(x, LT.Nil)