Copyright	(c) Galois Inc, 2015
License	Apache-2
Maintainer	jhendrix@galois.com, lcasburn@galois.com
Safe Haskell	Trustworthy
Language	Haskell98

Language.Lean.List

Contents

Re-exports

Description

Declares a data family List for associating a list type to different Lean values, and provides a typeclass along with associated operations for constructing and viewing Lean lists.

Synopsis

Documentation

data family List a Source

A type family for mapping a Lean value to the internal list representation.

Instances

IsList (List Name)
IsList (List Univ)	Allow `(List Univ)` to use `OverloadedLists` extensions.
IsList (List Expr)
IsList (List InductiveType)
Eq (List Name)
Eq (List Univ)
Eq (List Expr)
Eq (List InductiveType)
Show (List Name)
Show (List Univ)
Show (List Expr)
IsListIso (List Name) Source
IsListIso (List Univ) Source
IsListIso (List Expr) Source
IsListIso (List InductiveType) Source
IsLeanValue (List Name) (Ptr (List Name)) Source
IsLeanValue (List Univ) (Ptr (List Univ)) Source
IsLeanValue (List Expr) (Ptr (List Expr)) Source
IsLeanValue (List InductiveType) (Ptr (List InductiveType)) Source
type Item ListName = Name
type Item ListExpr = Expr
data List Name = ListName (ForeignPtr (List Name)) Source	A list of names (constructor not actually exported)
data List Univ = ListUniv (ForeignPtr (List Univ)) Source	A list of universes (constructor not actually exported)
data List Expr = ListExpr (ForeignPtr (List Expr)) Source	A list of expressions (constructor not actually exported)
data List InductiveType = ListInductiveType (ForeignPtr (List InductiveType)) Source	A list of inductive types (constructor not actually exported)
type Item (List Univ) = Univ
type Item (List InductiveType) = InductiveType

class IsList l => IsListIso l where Source

A typeclass for types that are isomorphic to lists.

This is used to provide functions for manipulating Lean's internal lists without the overhead of converting to and from Haskell lists.

Methods

nil :: l Source

The empty list

(<|) :: Item l -> l -> l Source

Cons an element to the front of a list.

listView :: l -> ListView l (Item l) Source

View the front of a list.

Instances

IsListIso (List Name) Source
IsListIso (List Univ) Source
IsListIso (List Expr) Source
IsListIso (List InductiveType) Source

data ListView l a Source

View of the front of a list

Constructors

Nil
a :< l

fromListDefault :: IsListIso l => [Item l] -> l Source

Convert a ordinary Haskell list to an opague list

concatList :: IsListIso l => l -> l -> l Source

Concatenate two lists

mapList :: (IsListIso s, IsListIso t) => (Item s -> Item t) -> s -> t Source

Apply a function to map one list to another.

traverseList :: (IsListIso s, IsListIso t) => Traversal s t (Item s) (Item t) Source

A traversal of the elements in a list.

Re-exports

class IsList l where

The IsList class and its methods are intended to be used in conjunction with the OverloadedLists extension.

Since: 4.7.0.0

Minimal complete definition

fromList, toList

Associated Types

type Item l :: *

The Item type function returns the type of items of the structure l.

Methods

fromList :: [Item l] -> l

The fromList function constructs the structure l from the given list of Item l

fromListN :: Int -> [Item l] -> l

The fromListN function takes the input list's length as a hint. Its behaviour should be equivalent to fromList. The hint can be used to construct the structure l more efficiently compared to fromList. If the given hint does not equal to the input list's length the behaviour of fromListN is not specified.

toList :: l -> [Item l]

The toList function extracts a list of Item l from the structure l. It should satisfy fromList . toList = id.

Instances

IsList Version	Since: 4.8.0.0
IsList IntSet
IsList [a]
IsList (IntMap a)
Ord a => IsList (Set a)
IsList (Seq a)
IsList (Vector a)
Prim a => IsList (Vector a)
Storable a => IsList (Vector a)
(Eq a, Hashable a) => IsList (HashSet a)
IsList (NonEmpty a)
IsList (List Name)
IsList (List Univ)	Allow `(List Univ)` to use `OverloadedLists` extensions.
IsList (List Expr)
IsList (List InductiveType)
Ord k => IsList (Map k v)
(Eq k, Hashable k) => IsList (HashMap k v)