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

Safe Haskell	Safe-Inferred
Language	Haskell2010

Rule

Documentation

data RuleContext Source #

Constructors

RuleContext
Fields _buildTerm :: BuildTermFunc _universe :: Maybe Expression _normal :: Expression -> Bool

data Step Source #

Constructors

Step
Fields _name :: String _applied :: RuleContext -> Expression -> IO (Maybe (Expression, [(Expression, Expression)]))

domainOf :: [Binding] -> Int Source #

isFormation :: Expression -> Bool Source #

isNF :: Expression -> RuleContext -> Bool Source #

matchExpressionWithRule :: Expression -> Rule -> RuleContext -> IO [Subst] Source #

matchExpressionWithRule' :: [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst] Source #

meetCondition :: Condition -> [Subst] -> RuleContext -> IO [Subst] Source #

normal :: Expression -> Bool Source #

normalHeld :: (Expression -> Bool) -> Expression -> Bool Source #

normalWith :: (Expression -> Bool) -> Expression -> Bool Source #

presentIn :: Attribute -> [Binding] -> Bool Source #

redex :: Rule -> Bool Source #

xiFree :: Expression -> Bool Source #