Language.Fixpoint.Graph.Types

This module contains the types for representing dependency graphs between kvars and constraints.

Graphs

data CVertex

Constructors

KVar !KVar

real kvar vertex

DKVar !KVar

dummy to ensure each kvar has a successor

EBind !Symbol

existentially bound "ghost paramter" to solve for

Cstr !Integer

constraint-id which creates a dependency

Instances

Generic CVertex

Defined in Language.Fixpoint.Graph.Types

Associated Types

type Rep CVertex :: Type -> Type

Methods

from :: CVertex -> Rep CVertex x

to :: Rep CVertex x -> CVertex

Show CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> CVertex -> ShowS

show :: CVertex -> String

showList :: [CVertex] -> ShowS

Eq CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

(==) :: CVertex -> CVertex -> Bool

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

Ord CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

compare :: CVertex -> CVertex -> Ordering

(<) :: CVertex -> CVertex -> Bool

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

(>) :: CVertex -> CVertex -> Bool

(>=) :: CVertex -> CVertex -> Bool

max :: CVertex -> CVertex -> CVertex

min :: CVertex -> CVertex -> CVertex

Hashable CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

hashWithSalt :: Int -> CVertex -> Int

hash :: CVertex -> Int

PPrint CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> CVertex -> Doc

pprintPrec :: Int -> Tidy -> CVertex -> Doc

type Rep CVertex

Defined in Language.Fixpoint.Graph.Types

type Rep CVertex = D1 ('MetaData "CVertex" "Language.Fixpoint.Graph.Types" "liquid-fixpoint-0.9.2.5-8VOJ4a5jXPy7nyhLFTxkOW" 'False) ((C1 ('MetaCons "KVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar)) :+: C1 ('MetaCons "DKVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 KVar))) :+: (C1 ('MetaCons "EBind" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Symbol)) :+: C1 ('MetaCons "Cstr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Integer))))

type CEdge = (CVertex, CVertex)

isRealEdge :: CEdge -> Bool

newtype KVGraph

Constructors

KVGraph

Fields

• kvgEdges :: [(CVertex, CVertex, [CVertex])]

Instances

PPrint KVGraph

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> KVGraph -> Doc

pprintPrec :: Int -> Tidy -> KVGraph -> Doc

Components

type Comps a = [[a]]

type KVComps = Comps CVertex

Printing

writeGraph :: FilePath -> KVGraph -> IO ()

writeEdges :: FilePath -> [CEdge] -> IO ()

Constraints

type SubcId = Integer

type KVRead = HashMap KVar [SubcId]

Dramatis Personae

type DepEdge = (SubcId, SubcId, [SubcId])

(Constraint id, vertex key, edges to other constraints)

The vertex key is always equal to the constraint id. The redundancy is imposed by how containers:Data.Graph requires graphs to be created.

Slice of relevant constraints

data Slice

Constructors

Slice

Fields

• slKVarCs :: [SubcId]

  F.SubcIds that transitively "reach" below

• slConcCs :: [SubcId]

  F.SubcIds with Concrete RHS

• slEdges :: [DepEdge]

  Dependencies between slKVarCs

Instances

Show Slice

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Slice -> ShowS

show :: Slice -> String

showList :: [Slice] -> ShowS

Eq Slice

Defined in Language.Fixpoint.Graph.Types

Methods

(==) :: Slice -> Slice -> Bool

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

Constraint Dependency Graphs

data CGraph

Constructors

CGraph

Fields

• gEdges :: [DepEdge]
• gRanks :: !(CMap Int)

  Maps a constraint id to an index identifying the strongly connected component to which it belongs. The scc indices correspond with a topological ordering of the sccs.

• gSucc :: !(CMap [SubcId])

  Tells for each constraint C, which constraints read any kvars that C writes.

  This is redundant with gEdges, so both fields need to express the exact same dependencies.

• gSccs :: !Int

  Amount of strongly connected components

Alias for Constraint Maps

type CMap a = HashMap SubcId a

lookupCMap :: (?callStack :: CallStack) => CMap a -> SubcId -> a

CMap API -------------------------------------------------------------

Ranks

data Rank

Ranks ---------------------------------------------------------------------

Constructors

Rank

Fields

• rScc :: !Int

  SCC number with ALL dependencies

• rIcc :: !Int

  SCC number without CUT dependencies

• rTag :: !Tag

  The constraint's Tag

Instances

Show Rank

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Rank -> ShowS

show :: Rank -> String

showList :: [Rank] -> ShowS

Eq Rank

Defined in Language.Fixpoint.Graph.Types

Methods

(==) :: Rank -> Rank -> Bool

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

PPrint Rank

Defined in Language.Fixpoint.Graph.Types

Methods

pprintTidy :: Tidy -> Rank -> Doc

pprintPrec :: Int -> Tidy -> Rank -> Doc

Constraint Dependencies

data CDeps

Constraint Dependencies ---------------------------------------------------

Constructors

CDs

Fields

• cSucc :: !(CMap [SubcId])

  Constraints *written by* a SubcId

• cPrev :: !(CMap [KVar])

  (Cut) KVars *read by* a SubcId

• cRank :: !(CMap Rank)

  SCC rank of a SubcId

• cNumScc :: !Int

  Total number of Sccs

Solver Info

data SolverInfo a b

SolverInfo contains all the stuff needed to produce a result, and is the the essential ingredient of the state needed by solve_

Constructors

SI

Fields

• siSol :: !(Sol b QBind)

  the initial solution

• siQuery :: !(SInfo a)

  the whole input query

• siDeps :: !CDeps

  dependencies between constraints/ranks etc.

• siVars :: !(HashSet KVar)

  set of KVars to actually solve for