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

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

Show CVertex

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> CVertex -> ShowS

show :: CVertex -> String

showList :: [CVertex] -> ShowS

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

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.8.10.2-Ld6PWXA9XrKe3HZnOCc57" 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

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

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

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

Show Slice

Defined in Language.Fixpoint.Graph.Types

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

Defined in Language.Fixpoint.Graph.Types

Methods

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

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

Show Rank

Defined in Language.Fixpoint.Graph.Types

Methods

showsPrec :: Int -> Rank -> ShowS

show :: Rank -> String

showList :: [Rank] -> ShowS

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