phino-0.0.0: Command-Line Manipulator of 𝜑-Calculus Expressions

Safe Haskell	Safe-Inferred
Language	Haskell2010

Morph

Documentation

data Answer Source #

Constructors

Answer Expression Expression
Joined Expression

data Deadline Source #

Constructors

Deadline
Fields _seconds :: Int _until :: Double

data Firing Source #

Constructors

Firing Text [Either Int Bytes] [Expression]

Instances

Instances details

Eq Firing Source #
Instance details Defined in Morph Methods (==) :: Firing -> Firing -> Bool # (/=) :: Firing -> Firing -> Bool #
Ord Firing Source #
Instance details Defined in Morph Methods compare :: Firing -> Firing -> Ordering # (<) :: Firing -> Firing -> Bool # (<=) :: Firing -> Firing -> Bool # (>) :: Firing -> Firing -> Bool # (>=) :: Firing -> Firing -> Bool # max :: Firing -> Firing -> Firing # min :: Firing -> Firing -> Firing #

data Kept Source #

Constructors

Answered Answer
Looped Expression
Stalled Text Int

data ReduceContext Source #

Constructors

Fields

_locator :: Expression
_site :: Expression
_universe :: Maybe Expression
_maxDepth :: Int
_maxCycles :: Int
_steps :: Steps
_tally :: Maybe Tally
_minted :: IORef Int
_deadline :: Maybe Deadline
_memo :: Maybe Memo
_nesting :: Int
_opened :: Maybe (Int, Judgment, Expression)
_depthSensitive :: Bool
_shuffle :: Bool
_partial :: Bool
_acyclic :: Maybe Acyclic
_maxLoops :: Int
_judgment :: Judgment
_parked :: [Text]
_entered :: Seen
_placed :: Maybe (Expression, [Binding], Expression)
_symbolic :: Lambdas
_buildTerm :: BuildTermFunc
_reduce :: ReductionFunc
_evaluate :: EvaluationFunc
_saveStep :: SaveStepFunc
_saveEval :: SaveEvalFunc
_engine :: Engine

data ReduceException Source #

Constructors

OutOfSteps Budget
OutOfTime Int
Stuck Text
StuckAt Text (NonEmpty Rewritten) State
OutOfStepsAt Budget (NonEmpty Rewritten) State
Diverged Text
Looping Expression
LoopingAt Expression (NonEmpty Rewritten) State
Undataizable Expression (NonEmpty Rewritten) State
Unmorphable Expression

Instances

Instances details

Exception ReduceException Source #
Instance details Defined in Morph Methods toException :: ReduceException -> SomeException # fromException :: SomeException -> Maybe ReduceException # displayException :: ReduceException -> String #
Show ReduceException Source #
Instance details Defined in Morph Methods showsPrec :: Int -> ReduceException -> ShowS # show :: ReduceException -> String # showList :: [ReduceException] -> ShowS #

type EvaluationFunc = ReduceContext -> State -> Expression -> Expression -> IO (Expression, State) Source #

data Memo Source #

Constructors

Memo (IORef (Store (Int, Kept))) (IORef (Map Firing Answer)) (IORef Int) (IORef Int)

type ReductionFunc = Expression -> ReduceContext -> Expression -> State -> IO (Maybe Bytes, State) Source #

type Morphed = (Expression, NonEmpty Rewritten) Source #

data Steps Source #

Constructors

Steps
Fields _limit :: Int _spent :: Int

data Tally Source #

Constructors

Tally
Fields _ceiling :: Int _count :: IORef Int

admitting :: Expression -> ReduceContext -> IO (Either (Acyclic, Expression) ReduceContext) Source #

argued :: Expression -> ReduceContext -> State -> Expression -> [Binding] -> Expression -> IO Expression Source #

awaited :: ReduceContext -> IO a -> IO a Source #

boxed :: [Binding] -> Bool Source #

called :: Expression -> ReduceContext -> [Binding] -> Maybe Expression Source #

carried :: State -> ReduceContext -> (State, ReduceContext) Source #

charged :: ReduceContext -> IO () Source #

coined :: ReduceContext -> IO Int Source #

counted :: Maybe Memo -> IO Int Source #

deeper :: ReduceContext -> IO ReduceContext Source #

emptyState :: State Source #

ended :: Answer -> Expression Source #

enter :: Expression -> ReduceContext -> IO ReduceContext Source #

entering :: Expression -> ReduceContext -> IO ReduceContext Source #

execBuildTerm :: Expression -> ReduceContext -> BuildTermFunc Source #

expired :: ReduceContext -> Int -> IO a Source #

fired :: Expression -> ReduceContext -> Expression -> State -> Expression -> IO (Expression, State) Source #

inferred :: Expression -> Expression -> State -> ReduceContext -> [Inference value] -> IO (Maybe (Conclusion value, State)) Source #

insideUniverse :: Expression -> Expression -> ReduceContext -> IO (Expression, ReduceContext) Source #

isLambda :: Binding -> Bool Source #

lambda :: [Binding] -> Maybe (Text, Expression) Source #

leadsTo :: NonEmpty Rewritten -> (Judgment, String) -> Expression -> ReduceContext -> IO (NonEmpty Rewritten) Source #

memoized :: Maybe Acyclic -> IO (Maybe Memo) Source #

morph :: Expression -> State -> ReduceContext -> IO (Expression, [Rewritten], State) Source #

morph' :: Morphed -> Expression -> State -> ReduceContext -> IO (Morphed, State) Source #

morphing :: Expression -> ReduceContext -> Expression -> State -> IO (Expression, State) Source #

normalized :: Expression -> NonEmpty Rewritten -> ReduceContext -> IO (Expression, NonEmpty Rewritten) Source #

onward :: NonEmpty Rewritten -> State -> Way -> Expression -> ReduceContext -> IO (Morphed, State) Source #

opening :: Judgment -> ReduceContext -> IO ReduceContext Source #

origin :: Expression -> ReduceContext -> [Binding] -> Maybe (Expression, [Binding]) Source #

parking :: NonEmpty Rewritten -> State -> IO a -> IO a Source #

recalled :: Maybe Memo -> Expression -> Int -> IO (Maybe Kept) Source #

refused :: Expression -> ReduceContext -> (Acyclic, Expression) -> IO a Source #

remember :: Maybe Memo -> Firing -> Answer -> IO () Source #

remembered :: Maybe Memo -> Firing -> IO (Maybe Answer) Source #

retained :: Maybe Memo -> Expression -> Int -> Kept -> IO () Source #

settled :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, State) Source #

severing :: Expression -> Expression -> State -> ReduceContext -> IO (Expression, ReduceContext) Source #

starved :: Maybe Memo -> IO Int Source #

tallied :: Maybe Int -> IO (Maybe Tally) Source #

timed :: Maybe Int -> IO (Maybe Deadline) Source #

universed :: Expression -> ReduceContext -> IO ReduceContext Source #

unparked :: IO a -> IO a Source #