Safe Haskell	None
Language	Haskell2010

Data.ECTA.Internal.ECTA.Enumeration

Synopsis

data TermFragment
- = TermFragmentNode !Symbol ![TermFragment]
- | TermFragmentUVar UVar
termFragToTruncatedTerm :: TermFragment -> Term
data SuspendedConstraint = SuspendedConstraint !PathTrie !UVar
scGetPathTrie :: SuspendedConstraint -> PathTrie
scGetUVar :: SuspendedConstraint -> UVar
descendScs :: Int -> Seq SuspendedConstraint -> Seq SuspendedConstraint
data UVarValue
- = UVarUnenumerated {
  - contents :: !(Maybe Node)
  - constraints :: !(Seq SuspendedConstraint)
  }
- | UVarEnumerated {
  - termFragment :: !TermFragment
  }
- | UVarEliminated
data EnumerationState = EnumerationState {
- _uvarCounter :: UVarGen
- _uvarRepresentative :: UnionFind
- _uvarValues :: Seq UVarValue
}
uvarCounter :: Lens' EnumerationState UVarGen
uvarRepresentative :: Lens' EnumerationState UnionFind
uvarValues :: Lens' EnumerationState (Seq UVarValue)
initEnumerationState :: Node -> EnumerationState
type EnumerateM = StateT EnumerationState []
getUVarRepresentative :: UVar -> EnumerateM UVar
assimilateUvarVal :: UVar -> UVar -> EnumerateM ()
mergeNodeIntoUVarVal :: UVar -> Node -> Seq SuspendedConstraint -> EnumerateM ()
getUVarValue :: UVar -> EnumerateM UVarValue
getTermFragForUVar :: UVar -> EnumerateM TermFragment
runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)]
enumerateNode :: Seq SuspendedConstraint -> Node -> EnumerateM TermFragment
enumerateEdge :: Seq SuspendedConstraint -> Edge -> EnumerateM TermFragment
firstExpandableUVar :: EnumerateM ExpandableUVarResult
enumerateOutUVar :: UVar -> EnumerateM TermFragment
enumerateOutFirstExpandableUVar :: EnumerateM ()
enumerateFully :: EnumerateM ()
expandTermFrag :: TermFragment -> EnumerateM Term
expandUVar :: UVar -> EnumerateM Term
getAllTruncatedTerms :: Node -> [Term]
getAllTerms :: Node -> [Term]
naiveDenotation :: Node -> [Term]

Documentation

data TermFragment Source #

Constructors

TermFragmentNode !Symbol ![TermFragment]
TermFragmentUVar UVar

Instances

Instances details

Eq TermFragment Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods (==) :: TermFragment -> TermFragment -> Bool # (/=) :: TermFragment -> TermFragment -> Bool #
Ord TermFragment Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods compare :: TermFragment -> TermFragment -> Ordering # (<) :: TermFragment -> TermFragment -> Bool # (<=) :: TermFragment -> TermFragment -> Bool # (>) :: TermFragment -> TermFragment -> Bool # (>=) :: TermFragment -> TermFragment -> Bool # max :: TermFragment -> TermFragment -> TermFragment # min :: TermFragment -> TermFragment -> TermFragment #
Show TermFragment Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods showsPrec :: Int -> TermFragment -> ShowS # show :: TermFragment -> String # showList :: [TermFragment] -> ShowS #

termFragToTruncatedTerm :: TermFragment -> Term Source #

data SuspendedConstraint Source #

Constructors

SuspendedConstraint !PathTrie !UVar

Instances

Instances details

Eq SuspendedConstraint Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods (==) :: SuspendedConstraint -> SuspendedConstraint -> Bool # (/=) :: SuspendedConstraint -> SuspendedConstraint -> Bool #
Ord SuspendedConstraint Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods compare :: SuspendedConstraint -> SuspendedConstraint -> Ordering # (<) :: SuspendedConstraint -> SuspendedConstraint -> Bool # (<=) :: SuspendedConstraint -> SuspendedConstraint -> Bool # (>) :: SuspendedConstraint -> SuspendedConstraint -> Bool # (>=) :: SuspendedConstraint -> SuspendedConstraint -> Bool # max :: SuspendedConstraint -> SuspendedConstraint -> SuspendedConstraint # min :: SuspendedConstraint -> SuspendedConstraint -> SuspendedConstraint #
Show SuspendedConstraint Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods showsPrec :: Int -> SuspendedConstraint -> ShowS # show :: SuspendedConstraint -> String # showList :: [SuspendedConstraint] -> ShowS #

scGetPathTrie :: SuspendedConstraint -> PathTrie Source #

scGetUVar :: SuspendedConstraint -> UVar Source #

descendScs :: Int -> Seq SuspendedConstraint -> Seq SuspendedConstraint Source #

data UVarValue Source #

Constructors

UVarUnenumerated
Fields contents :: !(Maybe Node) constraints :: !(Seq SuspendedConstraint)
UVarEnumerated
Fields termFragment :: !TermFragment
UVarEliminated

Instances

Instances details

Eq UVarValue Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods (==) :: UVarValue -> UVarValue -> Bool # (/=) :: UVarValue -> UVarValue -> Bool #
Ord UVarValue Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods compare :: UVarValue -> UVarValue -> Ordering # (<) :: UVarValue -> UVarValue -> Bool # (<=) :: UVarValue -> UVarValue -> Bool # (>) :: UVarValue -> UVarValue -> Bool # (>=) :: UVarValue -> UVarValue -> Bool # max :: UVarValue -> UVarValue -> UVarValue # min :: UVarValue -> UVarValue -> UVarValue #
Show UVarValue Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods showsPrec :: Int -> UVarValue -> ShowS # show :: UVarValue -> String # showList :: [UVarValue] -> ShowS #

data EnumerationState Source #

Constructors

EnumerationState
Fields _uvarCounter :: UVarGen _uvarRepresentative :: UnionFind _uvarValues :: Seq UVarValue

Instances

Instances details

Eq EnumerationState Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods (==) :: EnumerationState -> EnumerationState -> Bool # (/=) :: EnumerationState -> EnumerationState -> Bool #
Ord EnumerationState Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods compare :: EnumerationState -> EnumerationState -> Ordering # (<) :: EnumerationState -> EnumerationState -> Bool # (<=) :: EnumerationState -> EnumerationState -> Bool # (>) :: EnumerationState -> EnumerationState -> Bool # (>=) :: EnumerationState -> EnumerationState -> Bool # max :: EnumerationState -> EnumerationState -> EnumerationState # min :: EnumerationState -> EnumerationState -> EnumerationState #
Show EnumerationState Source #
Instance details Defined in Data.ECTA.Internal.ECTA.Enumeration Methods showsPrec :: Int -> EnumerationState -> ShowS # show :: EnumerationState -> String # showList :: [EnumerationState] -> ShowS #

uvarCounter :: Lens' EnumerationState UVarGen Source #

uvarRepresentative :: Lens' EnumerationState UnionFind Source #

uvarValues :: Lens' EnumerationState (Seq UVarValue) Source #

initEnumerationState :: Node -> EnumerationState Source #

type EnumerateM = StateT EnumerationState [] Source #

getUVarRepresentative :: UVar -> EnumerateM UVar Source #

assimilateUvarVal :: UVar -> UVar -> EnumerateM () Source #

mergeNodeIntoUVarVal :: UVar -> Node -> Seq SuspendedConstraint -> EnumerateM () Source #

getUVarValue :: UVar -> EnumerateM UVarValue Source #

getTermFragForUVar :: UVar -> EnumerateM TermFragment Source #

runEnumerateM :: EnumerateM a -> EnumerationState -> [(a, EnumerationState)] Source #

enumerateNode :: Seq SuspendedConstraint -> Node -> EnumerateM TermFragment Source #

enumerateEdge :: Seq SuspendedConstraint -> Edge -> EnumerateM TermFragment Source #

firstExpandableUVar :: EnumerateM ExpandableUVarResult Source #

enumerateOutUVar :: UVar -> EnumerateM TermFragment Source #

enumerateOutFirstExpandableUVar :: EnumerateM () Source #

enumerateFully :: EnumerateM () Source #

expandTermFrag :: TermFragment -> EnumerateM Term Source #

expandUVar :: UVar -> EnumerateM Term Source #

getAllTruncatedTerms :: Node -> [Term] Source #

getAllTerms :: Node -> [Term] Source #

naiveDenotation :: Node -> [Term] Source #

Inefficient enumeration

For ECTAs with Mu nodes may produce an infinite list or may loop indefinitely, depending on the ECTAs. For example, for

createMu $ \r -> Node [Edge "f" [r], Edge "a" []]

it will produce

[ Term "a" []
, Term "f" [Term "a" []]
, Term "f" [Term "f" [Term "a" []]]
, ...
]

This happens to work currently because non-recursive edges are interned before recursive edges.

TODO: It would be much nicer if this did fair enumeration. It would avoid the beforementioned dependency on interning order, and it would give better enumeration for examples such as

Node [Edge "h" [
    createMu $ \r -> Node [Edge "f" [r], Edge "a" []]
  , createMu $ \r -> Node [Edge "g" [r], Edge "b" []]
  ]]

This will currently produce

[ Term "h" [Term "a" [], Term "b" []]
, Term "h" [Term "a" [], Term "g" [Term "b" []]]
, Term "h" [Term "a" [], Term "g" [Term "g" [Term "b" []]]]
, ..
]

where it always unfolds the second argument to h, never the first.