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

Cstr !Integer

constraint-id which creates a dependency

Instances

Eq CVertex

Methods

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

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

Ord CVertex

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

Show CVertex

Methods

showsPrec :: Int -> CVertex -> ShowS

show :: CVertex -> String

showList :: [CVertex] -> ShowS

Generic CVertex

Associated Types

type Rep CVertex :: * -> *

Methods

from :: CVertex -> Rep CVertex x

to :: Rep CVertex x -> CVertex

Hashable CVertex

Methods

hashWithSalt :: Int -> CVertex -> Int

hash :: CVertex -> Int

PPrint CVertex

Methods

pprintTidy :: Tidy -> CVertex -> Doc

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

type Rep CVertex

type Rep CVertex = D1 (MetaData "CVertex" "Language.Fixpoint.Graph.Types" "liquid-fixpoint-0.7.0.2-3repHVQ2bkqGganvJ6cFNP" False) ((:+:) (C1 (MetaCons "KVar" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 KVar))) ((:+:) (C1 (MetaCons "DKVar" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 KVar))) (C1 (MetaCons "Cstr" PrefixI False) (S1 (MetaSel (Nothing Symbol) NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 Integer)))))

type CEdge = (CVertex, CVertex)

isRealEdge :: CEdge -> Bool

data KVGraph

Constructors

KVGraph

Fields

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

Instances

PPrint KVGraph

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])

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

Eq Slice

Methods

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

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

Show Slice

Methods

showsPrec :: Int -> Slice -> ShowS

show :: Slice -> String

showList :: [Slice] -> ShowS

Constraint Dependency Graphs

data CGraph

Constructors

CGraph

Fields

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

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

Eq Rank

Methods

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

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

Show Rank

Methods

showsPrec :: Int -> Rank -> ShowS

show :: Rank -> String

showList :: [Rank] -> ShowS

PPrint Rank

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