Language.Fixpoint.Types

This module contains the data types, operations and serialization functions for representing Fixpoint's implication (i.e. subtyping) and well-formedness constraints in Haskell. The actual constraint solving is done by the `fixpoint.native` which is written in Ocaml.

Top level serialization

class Fixpoint a where

Minimal complete definition

toFix

Methods

toFix :: a -> Doc

simplify :: a -> a

Instances

Fixpoint Bool

Fixpoint Double

Fixpoint Int

Fixpoint Integer

Fixpoint ()

Fixpoint Text

Fixpoint SourcePos

Fixpoint Symbol

Fixpoint Qualifier

Fixpoint Subst

Fixpoint BindEnv

Fixpoint IBindEnv

Fixpoint SortedReft

Fixpoint Reft

Fixpoint Refa

Fixpoint Pred

Fixpoint Expr

Fixpoint Bop

Fixpoint Brel

Fixpoint Constant

Fixpoint SymConst

Fixpoint Sort

Fixpoint FTycon

Fixpoint Kuts

Fixpoint KVar

Fixpoint Error

Fixpoint a => Fixpoint [a]

Fixpoint a => Fixpoint (Maybe a)

(Eq a, Hashable a, Fixpoint a) => Fixpoint (HashSet a)

Fixpoint a => Fixpoint (Located a)

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a))

Fixpoint a => Fixpoint (WfC a)

Fixpoint a => Fixpoint (SubC a)

Fixpoint a => Fixpoint (SEnv a)

(Fixpoint a, Fixpoint b) => Fixpoint (a, b)

(Fixpoint a, Fixpoint b, Fixpoint c) => Fixpoint (a, b, c)

toFixpoint :: Fixpoint a => Config -> FInfo a -> Doc

data FInfo a

Constructors

FI

Fields

cm :: HashMap Integer (SubC a)

ws :: ![WfC a]

bs :: !BindEnv

gs :: !FEnv

lits :: ![(Symbol, Sort)]

kuts :: Kuts

quals :: ![Qualifier]

bindInfo :: HashMap BindId a

Instances

(Show a, Fixpoint a) => Show (FInfo a)

Monoid (FInfo a)

Inputable (FInfo ())

Rendering

showFix :: Fixpoint a => a -> String

traceFix :: Fixpoint a => String -> a -> a

resultDoc :: (Ord a, Fixpoint a) => FixResult a -> Doc

Symbols

data Symbol

Instances

Eq Symbol

Data Symbol

Ord Symbol

Show Symbol

IsString Symbol

Generic Symbol

Monoid Symbol

NFData Symbol

Hashable Symbol

Symbolic Symbol

Subable Symbol

Predicate Symbol

Expression Symbol

The symbol may be an encoding of a SymConst.

Fixpoint Symbol

PPrint Symbol

SMTLIB2 Symbol

SMTLIB2 LocSymbol

Inputable Symbol

Typeable * Symbol

Solvable (Symbol, SortedReft)

type Rep Symbol

newtype KVar

Constructors

KV

Fields

kv :: Symbol

Instances

Eq KVar

Data KVar

Ord KVar

Show KVar

IsString KVar

Generic KVar

Hashable KVar

Fixpoint KVar

PPrint KVar

Solvable KVar

Typeable * KVar

Solvable (KVar, Subst)

Inputable (FixResult Integer, FixSolution)

type Rep KVar

anfPrefix :: Symbol

tempPrefix :: Symbol

vv :: Maybe Integer -> Symbol

vv_ :: Symbol

intKvar :: Integer -> KVar

symChars :: [Char]

isNonSymbol :: Symbol -> Bool

nonSymbol :: Symbol

isNontrivialVV :: Symbol -> Bool

symbolText :: Symbol -> Text

symbolString :: Symbol -> String

Creating Symbols

dummySymbol :: Symbol

intSymbol :: Show a => Symbol -> a -> Symbol

tempSymbol :: Symbol -> Integer -> Symbol

qualifySymbol :: Symbol -> Symbol -> Symbol

suffixSymbol :: Symbol -> Text -> Symbol

Embedding to Fixpoint Types

data Sort

Constructors

FInt

FReal

FNum

numeric kind for Num tyvars

FFrac

numeric kind for Fractional tyvars

FObj Symbol

uninterpreted type

FVar !Int

fixpoint type variable

FFunc !Int ![Sort]

type-var arity, in-ts ++ [out-t]

FApp FTycon [Sort]

constructed type

Instances

Eq Sort

Data Sort

Ord Sort

Show Sort

Generic Sort

Monoid Sort

NFData Sort

Hashable Sort

Fixpoint Sort

PPrint Sort

SMTLIB2 Sort

Typeable * Sort

type Rep Sort

data FTycon

Instances

Eq FTycon

Data FTycon

Ord FTycon

Show FTycon

Generic FTycon

NFData FTycon

Hashable FTycon

Fixpoint FTycon

Typeable * FTycon

type Rep FTycon

type TCEmb a = HashMap a FTycon

sortFTycon :: Sort -> Maybe FTycon

intFTyCon :: FTycon

boolFTyCon :: FTycon

realFTyCon :: FTycon

intSort :: Sort

Exported Basic Sorts -----------------------------------------------

realSort :: Sort

Exported Basic Sorts -----------------------------------------------

propSort :: Sort

Exported Basic Sorts -----------------------------------------------

boolSort :: Sort

Exported Basic Sorts -----------------------------------------------

strSort :: Sort

Exported Basic Sorts -----------------------------------------------

listFTyCon :: FTycon

appFTyCon :: FTycon

isListTC :: FTycon -> Bool

isFAppTyTC :: FTycon -> Bool

fTyconSymbol :: FTycon -> Located Symbol

symbolFTycon :: LocSymbol -> FTycon

fTyconSort :: FTycon -> Sort

fApp :: Either FTycon Sort -> [Sort] -> Sort

fObj :: LocSymbol -> Sort

Expressions and Predicates

data SymConst

Uninterpreted constants that are embedded as "constant symbol : Str"

Constructors

SL !Text

Instances

Eq SymConst

Data SymConst

Ord SymConst

Show SymConst

Generic SymConst

NFData SymConst

Hashable SymConst

Symbolic SymConst

Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.

Fixpoint SymConst

PPrint SymConst

SMTLIB2 SymConst

Typeable * SymConst

type Rep SymConst

data Constant

Constructors

I !Integer

R !Double

L !Text !Sort

Instances

Eq Constant

Data Constant

Ord Constant

Show Constant

Generic Constant

NFData Constant

Hashable Constant

Fixpoint Constant

PPrint Constant

SMTLIB2 Constant

Inputable Constant

Typeable * Constant

type Rep Constant

data Bop

Constructors

Plus

Minus

Times

Div

Mod

Instances

Eq Bop

Data Bop

Ord Bop

Show Bop

Generic Bop

NFData Bop

Hashable Bop

Fixpoint Bop

PPrint Bop

SMTLIB2 Bop

Typeable * Bop

type Rep Bop

data Brel

Constructors

Eq

Ne

Gt

Ge

Lt

Le

Ueq

Une

Instances

Eq Brel

Data Brel

Ord Brel

Show Brel

Generic Brel

NFData Brel

Hashable Brel

Fixpoint Brel

PPrint Brel

SMTLIB2 Brel

Typeable * Brel

type Rep Brel

data Expr

Constructors

ESym !SymConst

ECon !Constant

EVar !Symbol

ELit !LocSymbol !Sort

EApp !LocSymbol ![Expr]

ENeg !Expr

EBin !Bop !Expr !Expr

EIte !Pred !Expr !Expr

ECst !Expr !Sort

EBot

Instances

Eq Expr

Data Expr

Ord Expr

Show Expr

Generic Expr

NFData Expr

Hashable Expr

Subable Expr

Expression Expr

Fixpoint Expr

PPrint Expr

SMTLIB2 Expr

Inputable Expr

Typeable * Expr

type Rep Expr

data Pred

Constructors

PTrue

PFalse

PAnd !(ListNE Pred)

POr ![Pred]

PNot !Pred

PImp !Pred !Pred

PIff !Pred !Pred

PBexp !Expr

PAtom !Brel !Expr !Expr

PKVar !KVar !Subst

PAll ![(Symbol, Sort)] !Pred

PTop

Instances

Eq Pred

Data Pred

Ord Pred

Show Pred

Generic Pred

Monoid Pred

NFData Pred

Hashable Pred

Subable Pred

Predicate Pred

Fixpoint Pred

PPrint Pred

SMTLIB2 Pred

Solvable Pred

Inputable Pred

Typeable * Pred

Inputable (FixResult Integer, FixSolution)

type Rep Pred

eVar :: Symbolic a => a -> Expr

eProp :: Symbolic a => a -> Pred

pAnd :: ListNE Pred -> Pred

pOr :: [Pred] -> Pred

pIte :: Pred -> Pred -> Pred -> Pred

isTautoPred :: Pred -> Bool

symConstLits :: FInfo a -> [(Symbol, Sort)]

String Constants -----------------------------------------

Generalizing Embedding with Typeclasses

class Symbolic a where

Values that can be viewed as Symbols

Methods

symbol :: a -> Symbol

Instances

Symbolic String

Symbolic Text

Symbolic InternedText

Symbolic Symbol

Symbolic SymConst

Replace all symbol-representations-of-string-literals with string-literal Used to transform parsed output from fixpoint back into fq.

Symbolic a => Symbolic (Located a)

class Expression a where

Generalizing Symbol, Expression, Predicate into Classes -----------

Values that can be viewed as Constants

Values that can be viewed as Expressions

Methods

expr :: a -> Expr

Instances

Expression Int

Expression Integer

Expression Text

Expression Symbol

The symbol may be an encoding of a SymConst.

Expression Expr

Expression Bv

Construct an Expr using a raw string, e.g. (Bv S32 "#x02000000")

Expression a => Expression (Located a)

class Predicate a where

Values that can be viewed as Predicates

Methods

prop :: a -> Pred

Instances

Predicate Bool

Predicate Symbol

Predicate Pred

Constraints

data WfC a

Constructors

WfC

Fields

wenv :: !IBindEnv

wrft :: !SortedReft

wid :: !(Maybe Integer)

winfo :: !a

Instances

Fixpoint a => Show (WfC a)

Generic (WfC a)

NFData a => NFData (WfC a)

Fixpoint a => Fixpoint (WfC a)

type Rep (WfC a)

data SubC a

Instances

Fixpoint a => Show (SubC a)

Generic (SubC a)

NFData a => NFData (SubC a)

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a))

Fixpoint a => Fixpoint (SubC a)

type Rep (SubC a)

subcId :: SubC a -> Integer

sid :: SubC a -> Maybe Integer

sgrd :: SubC a -> Pred

senv :: SubC a -> IBindEnv

slhs :: SubC a -> SortedReft

srhs :: SubC a -> SortedReft

subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]

lhsCs :: SubC a -> Reft

rhsCs :: SubC a -> Reft

wfC :: IBindEnv -> SortedReft -> Maybe Integer -> a -> WfC a

type Tag = [Int]

Accessing Constraints

envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]

addIds :: [SubC a] -> [(Integer, SubC a)]

sinfo :: SubC a -> a

trueSubCKvar :: KVar -> a -> [SubC a]

removeLhsKvars :: t -> t1 -> t2

Solutions

data Result a

The output of the Solver

Constructors

Result

Fields

resStatus :: FixResult (SubC a)

resSolution :: HashMap KVar Pred

Instances

Fixpoint a => Show (Result a)

Monoid (Result a)

data FixResult a

Constructors

Crash [a] String

Safe

Unsafe ![a]

UnknownError !String

Instances

Functor FixResult

Eq a => Eq (FixResult a)

Show a => Show (FixResult a)

Generic (FixResult a)

Monoid (FixResult a)

(Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a))

Inputable (FixResult Integer)

Inputable (FixResult Integer, FixSolution)

type Rep (FixResult a)

type FixSolution = HashMap KVar Pred

Environments

data SEnv a

Instances

Functor SEnv

Foldable SEnv

Traversable SEnv

NFData FEnv

Eq a => Eq (SEnv a)

Data a => Data (SEnv a)

Fixpoint (SEnv a) => Show (SEnv a)

Generic (SEnv a)

Monoid (SEnv a)

Fixpoint a => Fixpoint (SEnv a)

Typeable (* -> *) SEnv

type Rep (SEnv a)

data SESearch a

Constructors

Found a

Alts [Symbol]

emptySEnv :: SEnv a

toListSEnv :: SEnv a -> [(Symbol, a)]

Environments ---------------------------------------------

fromListSEnv :: [(Symbol, a)] -> SEnv a

mapSEnvWithKey :: ((Symbol, a1) -> (Symbol, a)) -> SEnv a1 -> SEnv a

insertSEnv :: Symbol -> a -> SEnv a -> SEnv a

deleteSEnv :: Symbol -> SEnv a -> SEnv a

memberSEnv :: Symbol -> SEnv a -> Bool

lookupSEnv :: Symbol -> SEnv v -> Maybe v

intersectWithSEnv :: (v1 -> v2 -> a) -> SEnv v1 -> SEnv v2 -> SEnv a

filterSEnv :: (a -> Bool) -> SEnv a -> SEnv a

lookupSEnvWithDistance :: Symbol -> SEnv a -> SESearch a

type FEnv = SEnv SortedReft

insertFEnv :: Symbol -> a -> SEnv a -> SEnv a

data IBindEnv

Instances

Data IBindEnv

NFData IBindEnv

Fixpoint IBindEnv

Typeable * IBindEnv

type BindId = Int

type BindMap a = HashMap BindId a

emptyIBindEnv :: IBindEnv

Functions for Indexed Bind Environment

insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv

deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv

elemsIBindEnv :: IBindEnv -> [BindId]

data BindEnv

Instances

Show BindEnv

Monoid BindEnv

NFData BindEnv

Fixpoint BindEnv

beBinds :: BindEnv -> BindMap (Symbol, SortedReft)

insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)

Functions for Global Binder Environment

emptyBindEnv :: BindEnv

lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)

mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv

adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv

bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv

bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)]

unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv

Refinements

newtype Refa

Constructors

Refa

Fields

raPred :: Pred

Instances

Eq Refa

Data Refa

Ord Refa

Show Refa

Generic Refa

Monoid Refa

NFData Refa

Subable Refa

Fixpoint Refa

PPrint Refa

Solvable Refa

Inputable Refa

Typeable * Refa

type Rep Refa

data SortedReft

Constructors

RR

Fields

sr_sort :: !Sort

sr_reft :: !Reft

Instances

Eq SortedReft

Data SortedReft

Show SortedReft

Generic SortedReft

Monoid SortedReft

NFData FEnv

NFData SortedReft

Reftable SortedReft

Subable SortedReft

Fixpoint SortedReft

PPrint SortedReft

Solvable SortedReft

Typeable * SortedReft

Solvable (Symbol, SortedReft)

type Rep SortedReft

newtype Reft

Constructors

Reft (Symbol, Refa)

Instances

Eq Reft

Data Reft

Ord Reft

Show Reft

Generic Reft

Monoid Reft

NFData Reft

Reftable Reft

Subable Reft

Fixpoint Reft

PPrint Reft

Solvable Reft

Typeable * Reft

type Rep Reft

class (Monoid r, Subable r) => Reftable r where

A Class Predicates for Valid Refinements Types ---------------------

Minimal complete definition

isTauto, ppTy, bot, toReft, ofReft, params

Methods

isTauto :: r -> Bool

ppTy :: r -> Doc -> Doc

top :: r -> r

bot :: r -> r

meet :: r -> r -> r

toReft :: r -> Reft

ofReft :: Reft -> r

params

Arguments

:: r

-> [Symbol]

parameters for Reft, vv + others

Instances

Reftable ()

Reftable SortedReft

Reftable Reft

raConjuncts :: Refa -> [Pred]

Constructing Refinements

refa :: [Pred] -> Refa

reft :: Symbol -> Pred -> Reft

trueSortedReft :: Sort -> SortedReft

trueRefa :: Refa

trueReft :: Reft

exprReft :: Expression a => a -> Reft

notExprReft :: Expression a => a -> Reft

uexprReft :: Expression a => a -> Reft

symbolReft :: Symbolic a => a -> Reft

usymbolReft :: Symbolic a => a -> Reft

propReft :: Predicate a => a -> Reft

predReft :: Predicate a => a -> Reft

reftPred :: Reft -> Pred

reftBind :: Reft -> Symbol

isFunctionSortedReft :: SortedReft -> Bool

functionSort :: Sort -> Maybe (Int, [Sort], Sort)

isNonTrivial :: Reftable r => r -> Bool

isSingletonReft :: Reft -> Maybe Expr

isEVar :: Expr -> Bool

isFalse :: Falseable a => a -> Bool

flattenRefas :: [Refa] -> [Refa]

squishRefas :: [Refa] -> [Refa]

conjuncts :: Pred -> [Pred]

shiftVV :: Reft -> Symbol -> Reft

mapPredReft :: (Pred -> Pred) -> Reft -> Reft

Substitutions

newtype Subst

Constructors

Su [(Symbol, Expr)]

Instances

Eq Subst

Data Subst

Ord Subst

Show Subst

Generic Subst

Monoid Subst

NFData Subst

Hashable Subst

Fixpoint Subst

Typeable * Subst

Solvable (KVar, Subst)

type Rep Subst

class Subable a where

Minimal complete definition

syms, substa, substf, subst

Methods

syms :: a -> [Symbol]

substa :: (Symbol -> Symbol) -> a -> a

substf :: (Symbol -> Expr) -> a -> a

subst :: Subst -> a -> a

subst1 :: a -> (Symbol, Expr) -> a

Instances

Subable ()

Subable Symbol

Subable SortedReft

Subable Reft

Subable Refa

Subable Pred

Subable Expr

Subable a => Subable [a]

Subable a => Subable (Located a)

(Subable a, Subable b) => Subable (a, b)

Subable a => Subable (HashMap k a)

mkSubst :: [(Symbol, Expr)] -> Subst

isEmptySubst :: Subst -> Bool

substExcept :: Subst -> [Symbol] -> Subst

substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr

subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> a

sortSubst :: HashMap Symbol Sort -> Sort -> Sort

targetSubstSyms :: Subst -> [Symbol]

Functions on Result

colorResult :: FixResult a -> Moods

Cut KVars

newtype Kuts

Constructors

KS

Fields

ksVars :: HashSet KVar

Instances

Show Kuts

Monoid Kuts

NFData Kuts

Fixpoint Kuts

ksEmpty :: Kuts

ksUnion :: [KVar] -> Kuts -> Kuts

Qualifiers

data Qualifier

Constructors

Q

Fields

q_name :: Symbol

Name

q_params :: [(Symbol, Sort)]

Parameters

q_body :: Pred

Predicate

q_pos :: !SourcePos

Source Location

Instances

Eq Qualifier

Data Qualifier

Ord Qualifier

Show Qualifier

Generic Qualifier

NFData Qualifier

Fixpoint Qualifier

Typeable * Qualifier

type Rep Qualifier

Located Values

data Located a

Located Values ---------------------------------------------------------

Constructors

Loc

Fields

loc :: !SourcePos

Start Position

locE :: !SourcePos

End Position

val :: a

Instances

Functor Located

Foldable Located

Traversable Located

SMTLIB2 LocSymbol

Eq a => Eq (Located a)

Data a => Data (Located a)

Ord a => Ord (Located a)

Show a => Show (Located a)

IsString a => IsString (Located a)

Generic (Located a)

NFData a => NFData (Located a)

Hashable a => Hashable (Located a)

Symbolic a => Symbolic (Located a)

Subable a => Subable (Located a)

Expression a => Expression (Located a)

Fixpoint a => Fixpoint (Located a)

PPrint a => PPrint (Located a)

Typeable (* -> *) Located

type Rep (Located a)

type LocSymbol = Located Symbol

type LocText = Located Text

locAt :: String -> a -> Located a

dummyLoc :: a -> Located a

dummyPos :: String -> SourcePos

dummyName :: Symbol

isDummy :: Symbolic a => a -> Bool