Flesh out NFAs

This commit is contained in:
Joscha 2019-10-24 20:00:00 +00:00
parent 4cae9af848
commit edd31cb52a

View file

@ -1,23 +1,53 @@
module Rextra.Nfa where
-- TODO don't export internals
module Rextra.Nfa (
-- * Nondeterministic Finite Automaton
Nfa
, State
-- ** Constructing
, nfa
, nfa'
-- ** Using
, nfaStates
, nfaEntryState
, nfaExitStates
, nfaTransition
-- ** Transitions
, TransitionCondition
, specialStates
, accepts
) where
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
-- | This condition determines which tokens a state transition applies to.
--
-- This representation is based on the assumption that there can be an
-- infinite number of different tokens. The condition thus contains a
-- default answer to the question "Does this transition apply to this
-- token?", and all the exceptions for which the answer is negated.
data TransitionCondition t
= Only (Set.Set t)
| AllExcept (Set.Set t)
-- | The states which are treated differently from the default by the
-- 'TransitionCondition'.
specialStates :: TransitionCondition t -> Set.Set t
specialStates (Only s) = s
specialStates (AllExcept s) = s
-- | Whether the condition holds true for a token.
accepts :: (Ord t) => TransitionCondition t -> t -> Bool
accepts (Only s) t = Set.member t s
accepts (AllExcept s) t = Set.notMember t s
-- | A state consists of the transitions to other states, and the
-- conditions under which those transitions happen.
type State s t = [(TransitionCondition t, s)]
-- | A type representing a nondeterministic finite automaton.
--
-- It has one entry state and any number of exit states, which can be
-- interpreted as accepting states when the NFA is run.
data Nfa s t = Nfa
{ nfaStates :: Map.Map s (State s t)
, nfaEntryState :: s
@ -25,10 +55,36 @@ data Nfa s t = Nfa
}
{-
- Constructing and modifying a NFA
- Constructing a NFA
-}
-- TODO
integrityCheck :: (Ord s) => Nfa s t -> Bool
integrityCheck nfa =
let referencedStates = Set.unions
[ Set.singleton (nfaEntryState nfa)
, nfaExitStates nfa
, Set.fromList . map snd . concat . Map.elems $ nfaStates nfa
]
in referencedStates `Set.isSubsetOf` Map.keysSet (nfaStates nfa)
-- | Construct an 'Nfa' from all its components.
--
-- This constructor function performs some error checking required to
-- keep the data structure internally consistent. At the moment, this
-- is limited to checking whether all state names mentioned anywhere
-- in the data struture actually exist in the state map.
nfa :: (Ord s)
=> Map.Map s (State s t) -- ^ The state lookup map (maps state name to state itself)
-> s -- ^ The entry state (starting state)
-> Set.Set s -- ^ The exit states
-> Maybe (Nfa s t) -- ^ The 'Nfa', if the data didn't show any inconsistencies
nfa states entryState exitStates =
let myNfa = Nfa{nfaStates=states, nfaEntryState=entryState, nfaExitStates=exitStates}
in if integrityCheck myNfa then Just myNfa else Nothing
-- | A version of 'nfa' using argument formats that should be easier to work with.
nfa' :: (Ord s) => [(s, State s t)] -> s -> [s] -> Maybe (Nfa s t)
nfa' states entryState exitStates = nfa (Map.fromList states) entryState (Set.fromList exitStates)
{-
- "Executing" a NFA
@ -37,9 +93,18 @@ data Nfa s t = Nfa
getState :: (Ord s) => Nfa s t -> s -> State s t
getState nfa s = nfaStates nfa Map.! s
-- * Starting from a state, find all the states that it can transition to with token 't'.
-- | Starting from a state, find all the states that it can transition to with token @t@.
nextStates :: (Ord s, Ord t) => State s t -> t -> Set.Set s
nextStates state t = Set.fromList . map snd . filter (\(cond, _) -> cond `accepts` t) $ state
-- | The NFA's transition function.
--
-- Since this is a /nondeterministic/ finite automaton, the transition
-- function does not operate on individual states, but rather on a set
-- of current states.
--
-- __Warning__: This function does /not/ check whether the states
-- actually exist in the automaton, and it crashes if an invalid state
-- is used.
nfaTransition :: (Ord s, Ord t) => Nfa s t -> Set.Set s -> t -> Set.Set s
nfaTransition nfa ss t = foldMap (\s -> nextStates (getState nfa s) t) ss