QuickSpec.Term

This module is internal to QuickSpec.

Typed terms and operations on them.

Documentation

data Term f

A typed term.

Constructors

Var !Var

App !f ![Term f]

Instances

Functor Term

Methods

fmap :: (a -> b) -> Term a -> Term b

(<$) :: a -> Term b -> Term a

Symbolic f (Term f)

Methods

termsDL :: Term f -> DList (Term f)

subst :: (Var -> Term f) -> Term f -> Term f

Eq f => Eq (Term f)

Methods

(==) :: Term f -> Term f -> Bool

(/=) :: Term f -> Term f -> Bool

Ord f => Ord (Term f)

Methods

compare :: Term f -> Term f -> Ordering

(<) :: Term f -> Term f -> Bool

(<=) :: Term f -> Term f -> Bool

(>) :: Term f -> Term f -> Bool

(>=) :: Term f -> Term f -> Bool

max :: Term f -> Term f -> Term f

min :: Term f -> Term f -> Term f

Show f => Show (Term f)

Methods

showsPrec :: Int -> Term f -> ShowS

show :: Term f -> String

showList :: [Term f] -> ShowS

PrettyTerm f => Pretty (Term f)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Term f -> Doc

pPrint :: Term f -> Doc

pPrintList :: PrettyLevel -> [Term f] -> Doc

Typed f => Typed (Term f)

Methods

typ :: Term f -> Type

otherTypesDL :: Term f -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Term f -> Term f

Sized f => Sized (Term f)

Methods

size :: Term f -> Int

data Var

A variable, which has a type and a number.

Constructors

V

Fields

• var_ty :: !Type
• var_id :: !Int

Instances

Eq Var

Methods

(==) :: Var -> Var -> Bool

(/=) :: Var -> Var -> Bool

Ord Var

Methods

compare :: Var -> Var -> Ordering

(<) :: Var -> Var -> Bool

(<=) :: Var -> Var -> Bool

(>) :: Var -> Var -> Bool

(>=) :: Var -> Var -> Bool

max :: Var -> Var -> Var

min :: Var -> Var -> Var

Show Var

Methods

showsPrec :: Int -> Var -> ShowS

show :: Var -> String

showList :: [Var] -> ShowS

Generic Var

Associated Types

type Rep Var :: * -> *

Methods

from :: Var -> Rep Var x

to :: Rep Var x -> Var

CoArbitrary Var

Methods

coarbitrary :: Var -> Gen b -> Gen b

Pretty Var

Methods

pPrintPrec :: PrettyLevel -> Rational -> Var -> Doc

pPrint :: Var -> Doc

pPrintList :: PrettyLevel -> [Var] -> Doc

Typed Var

Methods

typ :: Var -> Type

otherTypesDL :: Var -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> Var -> Var

type Rep Var

type Rep Var = D1 * (MetaData "Var" "QuickSpec.Term" "quickspec-2.1-5fSNb7X5HLABGdHB0i89ut" False) (C1 * (MetaCons "V" PrefixI True) ((:*:) * (S1 * (MetaSel (Just Symbol "var_ty") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 * Type)) (S1 * (MetaSel (Just Symbol "var_id") SourceUnpack SourceStrict DecidedStrict) (Rec0 * Int))))

class Symbolic f a | a -> f where

A class for things that contain terms.

Minimal complete definition

termsDL, subst

Methods

termsDL :: a -> DList (Term f)

A different list of all terms contained in the thing.

subst :: (Var -> Term f) -> a -> a

Apply a substitution to all terms in the thing.

Instances

Symbolic f a => Symbolic f [a]

Methods

termsDL :: [a] -> DList (Term f)

subst :: (Var -> Term f) -> [a] -> [a]

Symbolic f (Term f)

Methods

termsDL :: Term f -> DList (Term f)

subst :: (Var -> Term f) -> Term f -> Term f

class Sized a where

Minimal complete definition

size

Methods

size :: a -> Int

Instances

Sized f => Sized (Term f)

Methods

size :: Term f -> Int

(Sized fun1, Sized fun2) => Sized ((:+:) fun1 fun2)

Methods

size :: (fun1 :+: fun2) -> Int

isApp :: Term f -> Bool

Is a term an application (i.e. not a variable)?

isVar :: Term f -> Bool

Is a term a variable?

terms :: Symbolic f a => a -> [Term f]

All terms contained in a Symbolic.

funs :: Symbolic f a => a -> [f]

All function symbols appearing in a Symbolic, in order of appearance, with duplicates included.

vars :: Symbolic f a => a -> [Var]

All variables appearing in a Symbolic, in order of appearance, with duplicates included.

freeVar :: Symbolic f a => a -> Int

Compute the number of a variable which does not appear in the Symbolic.

occ :: (Eq f, Symbolic f a) => f -> a -> Int

Count how many times a given function symbol occurs.

occVar :: Symbolic f a => Var -> a -> Int

Count how many times a given variable occurs.

mapVar :: (Var -> Var) -> Term f -> Term f

Map a function over variables.

subterms :: Term f -> [Term f]

Find all subterms of a term. Includes the term itself.

properSubterms :: Term f -> [Term f]

Find all subterms of a term. Does not include the term itself.

canonicalise :: Symbolic fun a => a -> a

Renames variables so that they appear in a canonical order. Also makes sure that variables of different types have different numbers.

evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a

Evaluate a term, given a valuation for variables and function symbols.

type Measure f = (Int, Int, MeasureFuns f, Int, [Var])

A standard term ordering - size, skeleton, generality. Satisfies the property: if measure (schema t) < measure (schema u) then t < u.

measure :: Sized f => Term f -> Measure f

Compute the term ordering for a term.

newtype MeasureFuns f

A helper for Measure.

Constructors

MeasureFuns (Term f)

Instances

Ord f => Eq (MeasureFuns f)

Methods

(==) :: MeasureFuns f -> MeasureFuns f -> Bool

(/=) :: MeasureFuns f -> MeasureFuns f -> Bool

Ord f => Ord (MeasureFuns f)

Methods

compare :: MeasureFuns f -> MeasureFuns f -> Ordering

(<) :: MeasureFuns f -> MeasureFuns f -> Bool

(<=) :: MeasureFuns f -> MeasureFuns f -> Bool

(>) :: MeasureFuns f -> MeasureFuns f -> Bool

(>=) :: MeasureFuns f -> MeasureFuns f -> Bool

max :: MeasureFuns f -> MeasureFuns f -> MeasureFuns f

min :: MeasureFuns f -> MeasureFuns f -> MeasureFuns f

compareFuns :: Ord f => Term f -> Term f -> Ordering

A helper for Measure.

Data types a la carte-ish.

data a :+: b

A sum type. Intended to be used to build the type of function symbols. Comes with instances that are useful for QuickSpec.

Constructors

Inl a

Inr b

Instances

(Eq b, Eq a) => Eq ((:+:) a b)

Methods

(==) :: (a :+: b) -> (a :+: b) -> Bool

(/=) :: (a :+: b) -> (a :+: b) -> Bool

(Ord b, Ord a) => Ord ((:+:) a b)

Methods

compare :: (a :+: b) -> (a :+: b) -> Ordering

(<) :: (a :+: b) -> (a :+: b) -> Bool

(<=) :: (a :+: b) -> (a :+: b) -> Bool

(>) :: (a :+: b) -> (a :+: b) -> Bool

(>=) :: (a :+: b) -> (a :+: b) -> Bool

max :: (a :+: b) -> (a :+: b) -> a :+: b

min :: (a :+: b) -> (a :+: b) -> a :+: b

(Pretty fun1, Pretty fun2) => Pretty ((:+:) fun1 fun2)

Methods

pPrintPrec :: PrettyLevel -> Rational -> (fun1 :+: fun2) -> Doc

pPrint :: (fun1 :+: fun2) -> Doc

pPrintList :: PrettyLevel -> [fun1 :+: fun2] -> Doc

(Arity fun1, Arity fun2) => Arity ((:+:) fun1 fun2)

Methods

arity :: (fun1 :+: fun2) -> Int

(PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm ((:+:) fun1 fun2)

Methods

termStyle :: (fun1 :+: fun2) -> TermStyle

(Typed fun1, Typed fun2) => Typed ((:+:) fun1 fun2)

Methods

typ :: (fun1 :+: fun2) -> Type

otherTypesDL :: (fun1 :+: fun2) -> DList Type

typeSubst_ :: (Var -> Builder TyCon) -> (fun1 :+: fun2) -> fun1 :+: fun2

(Sized fun1, Sized fun2) => Sized ((:+:) fun1 fun2)

Methods

size :: (fun1 :+: fun2) -> Int

module Twee.Base

module Twee.Pretty