phino-0.0.0: Command-Line Manipulator of 𝜑-Calculus Expressions
Safe HaskellSafe-Inferred
LanguageHaskell2010

Inference

Documentation

data Conclusion value Source #

Constructors

Answered (Judgment, String) value 
Onward Way Expression Expression 

Instances

Instances details
Show value => Show (Conclusion value) Source # 
Instance details

Defined in Inference

Methods

showsPrec :: Int -> Conclusion value -> ShowS #

show :: Conclusion value -> String #

showList :: [Conclusion value] -> ShowS #

Eq value => Eq (Conclusion value) Source # 
Instance details

Defined in Inference

Methods

(==) :: Conclusion value -> Conclusion value -> Bool #

(/=) :: Conclusion value -> Conclusion value -> Bool #

type Inference value = RuleContext -> Expression -> Expression -> IO (Maybe (Premises value)) Source #

data Premises value Source #

Constructors

Morphs Expression Expression (Expression -> IO (Premises value)) 
Evaluates Expression Expression (Expression -> IO (Premises value)) 
Contextualizes Expression Expression (Expression -> IO (Premises value)) 
Concludes (Conclusion value) 

data Way Source #

Constructors

Taken (Judgment, String) 
Normalized (Judgment, String) 
Named (Judgment, String) 
Staged Expression 

Instances

Instances details
Show Way Source # 
Instance details

Defined in Inference

Methods

showsPrec :: Int -> Way -> ShowS #

show :: Way -> String #

showList :: [Way] -> ShowS #

Eq Way Source # 
Instance details

Defined in Inference

Methods

(==) :: Way -> Way -> Bool #

(/=) :: Way -> Way -> Bool #

dataizationOf :: DataizeRule -> Inference Bytes Source #

dataizationSpine :: DataizeRule -> Either String ([Premise], Conclusion Bytes) Source #

direct :: (Expression -> Expression -> [Premises value]) -> Inference value Source #

morphingOf :: MorphRule -> Inference Expression Source #

morphingSpine :: MorphRule -> Either String ([Premise], Conclusion Expression) Source #