{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
-- SPDX-License-Identifier: MIT

module Inference (Conclusion (..), Inference, Premises (..), Way (..), dataizationOf, dataizationSpine, direct, morphingOf, morphingSpine) where

import AST
import Builder (buildBytesThrows, buildExpressionThrows)
import Control.Exception (throwIO)
import Data.List (find)
import Data.Maybe (listToMaybe)
import qualified Data.Text as T
import Deps (Judgment (..))
import Matcher (MetaValue (..), Subst, combine, matchExpression', substSingle)
import Rule (RuleContext, matchExpressionWithRule')
import Text.Printf (printf)
import qualified Yaml as Y

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

data Premises value
  = 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 Conclusion value
  = Answered (Judgment, String) value
  | Onward Way Expression Expression
  deriving (Conclusion value -> Conclusion value -> Bool
(Conclusion value -> Conclusion value -> Bool)
-> (Conclusion value -> Conclusion value -> Bool)
-> Eq (Conclusion value)
forall value.
Eq value =>
Conclusion value -> Conclusion value -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall value.
Eq value =>
Conclusion value -> Conclusion value -> Bool
== :: Conclusion value -> Conclusion value -> Bool
$c/= :: forall value.
Eq value =>
Conclusion value -> Conclusion value -> Bool
/= :: Conclusion value -> Conclusion value -> Bool
Eq, Int -> Conclusion value -> ShowS
[Conclusion value] -> ShowS
Conclusion value -> String
(Int -> Conclusion value -> ShowS)
-> (Conclusion value -> String)
-> ([Conclusion value] -> ShowS)
-> Show (Conclusion value)
forall value. Show value => Int -> Conclusion value -> ShowS
forall value. Show value => [Conclusion value] -> ShowS
forall value. Show value => Conclusion value -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall value. Show value => Int -> Conclusion value -> ShowS
showsPrec :: Int -> Conclusion value -> ShowS
$cshow :: forall value. Show value => Conclusion value -> String
show :: Conclusion value -> String
$cshowList :: forall value. Show value => [Conclusion value] -> ShowS
showList :: [Conclusion value] -> ShowS
Show)

data Way
  = Taken (Judgment, String)
  | Normalized (Judgment, String)
  | Named (Judgment, String)
  | Staged Expression
  deriving (Way -> Way -> Bool
(Way -> Way -> Bool) -> (Way -> Way -> Bool) -> Eq Way
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Way -> Way -> Bool
== :: Way -> Way -> Bool
$c/= :: Way -> Way -> Bool
/= :: Way -> Way -> Bool
Eq, Int -> Way -> ShowS
[Way] -> ShowS
Way -> String
(Int -> Way -> ShowS)
-> (Way -> String) -> ([Way] -> ShowS) -> Show Way
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Way -> ShowS
showsPrec :: Int -> Way -> ShowS
$cshow :: Way -> String
show :: Way -> String
$cshowList :: [Way] -> ShowS
showList :: [Way] -> ShowS
Show)

morphingSpine :: Y.MorphRule -> Either String ([Y.Premise], Conclusion Expression)
morphingSpine :: MorphRule -> Either String ([Premise], Conclusion Expression)
morphingSpine MorphRule
rule = case Expression -> [Premise] -> Maybe Premise
producer MorphRule
rule.nresult MorphRule
rule.premises of
  Maybe Premise
Nothing -> ([Premise], Conclusion Expression)
-> Either String ([Premise], Conclusion Expression)
forall a b. b -> Either a b
Right (MorphRule
rule.premises, (Judgment, String) -> Expression -> Conclusion Expression
forall value. (Judgment, String) -> value -> Conclusion value
Answered (Judgment, String)
step MorphRule
rule.nresult)
  Just concl :: Premise
concl@(Y.Premise Text
_ (Y.OpMorph Expression
arg Expression
universe)) -> case Expression -> [Premise] -> Maybe Premise
producer Expression
arg MorphRule
rule.premises of
    Just normal :: Premise
normal@(Y.Premise Text
_ (Y.OpNormalize Expression
inner)) ->
      ([Premise], Conclusion Expression)
-> Either String ([Premise], Conclusion Expression)
forall a b. b -> Either a b
Right (MorphRule
rule.premises [Premise] -> [Premise] -> [Premise]
`excluding` [Premise
concl, Premise
normal], Way -> Expression -> Expression -> Conclusion Expression
forall value. Way -> Expression -> Expression -> Conclusion value
Onward ((if Expression
inner Expression -> Expression -> Bool
forall a. Eq a => a -> a -> Bool
== MorphRule
rule.ematch then (Judgment, String) -> Way
Named else (Judgment, String) -> Way
Normalized) (Judgment, String)
step) Expression
inner Expression
universe)
    Maybe Premise
_ -> ([Premise], Conclusion Expression)
-> Either String ([Premise], Conclusion Expression)
forall a b. b -> Either a b
Right (MorphRule
rule.premises [Premise] -> [Premise] -> [Premise]
`excluding` [Premise
concl], Way -> Expression -> Expression -> Conclusion Expression
forall value. Way -> Expression -> Expression -> Conclusion value
Onward ((Judgment, String) -> Way
Taken (Judgment, String)
step) Expression
arg Expression
universe)
  Just Premise
_ -> String -> Either String ([Premise], Conclusion Expression)
forall a b. a -> Either a b
Left String
"it concludes with no 'morph' premise"
  where
    step :: (Judgment, String)
    step :: (Judgment, String)
step = (Judgment
Morphing, MorphRule
rule.name)

dataizationSpine :: Y.DataizeRule -> Either String ([Y.Premise], Conclusion Bytes)
dataizationSpine :: DataizeRule -> Either String ([Premise], Conclusion Bytes)
dataizationSpine DataizeRule
rule = case Bytes -> Maybe Premise
bytesProducer DataizeRule
rule.dresult of
  Maybe Premise
Nothing -> ([Premise], Conclusion Bytes)
-> Either String ([Premise], Conclusion Bytes)
forall a b. b -> Either a b
Right (DataizeRule
rule.premises, (Judgment, String) -> Bytes -> Conclusion Bytes
forall value. (Judgment, String) -> value -> Conclusion value
Answered (Judgment
Dataization, DataizeRule
rule.name) DataizeRule
rule.dresult)
  Just concl :: Premise
concl@(Y.Premise Text
_ (Y.OpDataize Expression
arg Expression
universe)) -> case Expression -> [Premise] -> Maybe Premise
producer Expression
arg DataizeRule
rule.premises of
    Just normal :: Premise
normal@(Y.Premise Text
_ (Y.OpNormalize Expression
inner)) ->
      let side :: [Premise]
side = DataizeRule
rule.premises [Premise] -> [Premise] -> [Premise]
`excluding` [Premise
concl, Premise
normal]
       in ([Premise], Conclusion Bytes)
-> Either String ([Premise], Conclusion Bytes)
forall a b. b -> Either a b
Right ([Premise]
side, Way -> Expression -> Expression -> Conclusion Bytes
forall value. Way -> Expression -> Expression -> Conclusion value
Onward ((Judgment, String) -> Way
Normalized ((Judgment, String) -> [Premise] -> (Judgment, String)
labelled (Judgment
Dataization, DataizeRule
rule.name) [Premise]
side)) Expression
inner Expression
universe)
    Just morphed :: Premise
morphed@(Y.Premise Text
_ (Y.OpMorph Expression
inner Expression
scene)) ->
      ([Premise], Conclusion Bytes)
-> Either String ([Premise], Conclusion Bytes)
forall a b. b -> Either a b
Right (DataizeRule
rule.premises [Premise] -> [Premise] -> [Premise]
`excluding` [Premise
concl, Premise
morphed], Way -> Expression -> Expression -> Conclusion Bytes
forall value. Way -> Expression -> Expression -> Conclusion value
Onward (Expression -> Way
Staged Expression
scene) Expression
inner Expression
universe)
    Maybe Premise
_ ->
      let side :: [Premise]
side = DataizeRule
rule.premises [Premise] -> [Premise] -> [Premise]
`excluding` [Premise
concl]
       in ([Premise], Conclusion Bytes)
-> Either String ([Premise], Conclusion Bytes)
forall a b. b -> Either a b
Right ([Premise]
side, Way -> Expression -> Expression -> Conclusion Bytes
forall value. Way -> Expression -> Expression -> Conclusion value
Onward ((Judgment, String) -> Way
Taken ((Judgment, String) -> [Premise] -> (Judgment, String)
labelled (Operation -> (Judgment, String)
label Premise
concl.operation) [Premise]
side)) Expression
arg Expression
universe)
  Just Premise
_ -> String -> Either String ([Premise], Conclusion Bytes)
forall a b. a -> Either a b
Left String
"it concludes with no 'dataize' premise"
  where
    bytesProducer :: Bytes -> Maybe Y.Premise
    bytesProducer :: Bytes -> Maybe Premise
bytesProducer (BtMeta Text
name) = (Premise -> Bool) -> [Premise] -> Maybe Premise
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Premise
premise -> Premise
premise.result Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
name) DataizeRule
rule.premises
    bytesProducer Bytes
_ = Maybe Premise
forall a. Maybe a
Nothing
    labelled :: (Judgment, String) -> [Y.Premise] -> (Judgment, String)
    labelled :: (Judgment, String) -> [Premise] -> (Judgment, String)
labelled (Judgment, String)
_ (Premise
premise : [Premise]
_) = Operation -> (Judgment, String)
label Premise
premise.operation
    labelled (Judgment, String)
fallback [] = (Judgment, String)
fallback

producer :: Expression -> [Y.Premise] -> Maybe Y.Premise
producer :: Expression -> [Premise] -> Maybe Premise
producer (ExMeta Text
name) = (Premise -> Bool) -> [Premise] -> Maybe Premise
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (\Premise
premise -> Premise
premise.result Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
name)
producer Expression
_ = Maybe Premise -> [Premise] -> Maybe Premise
forall a b. a -> b -> a
const Maybe Premise
forall a. Maybe a
Nothing

excluding :: [Y.Premise] -> [Y.Premise] -> [Y.Premise]
excluding :: [Premise] -> [Premise] -> [Premise]
excluding [Premise]
premises [Premise]
removed = (Premise -> Bool) -> [Premise] -> [Premise]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Premise
premise -> Premise
premise.result Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (Premise -> Text) -> [Premise] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (.result) [Premise]
removed) [Premise]
premises

label :: Y.Operation -> (Judgment, String)
label :: Operation -> (Judgment, String)
label (Y.OpMorph Expression
_ Expression
_) = (Judgment
Morphing, String
"morph")
label (Y.OpNormalize Expression
_) = (Judgment
Normalization, String
"normalize")
label (Y.OpEvaluate Expression
_ Expression
_) = (Judgment
Evaluation, String
"evaluate")
label (Y.OpContextualize Expression
_ Expression
_) = (Judgment
Contextualization, String
"contextualize")
label (Y.OpDataize Expression
_ Expression
_) = (Judgment
Dataization, String
"dataize")

morphingOf :: Y.MorphRule -> Inference Expression
morphingOf :: MorphRule -> Inference Expression
morphingOf MorphRule
rule = (Expression -> Subst -> IO Expression)
-> Rule
-> Expression
-> Either String ([Premise], Conclusion Expression)
-> Inference Expression
forall value.
(value -> Subst -> IO value)
-> Rule
-> Expression
-> Either String ([Premise], Conclusion value)
-> Inference value
interpreted Expression -> Subst -> IO Expression
buildExpressionThrows (String
-> Maybe String
-> Maybe String
-> Expression
-> Expression
-> Maybe Condition
-> Maybe [Extra]
-> Maybe Condition
-> Rule
Y.Rule MorphRule
rule.name Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing MorphRule
rule.match Expression
ExRoot MorphRule
rule.when Maybe [Extra]
forall a. Maybe a
Nothing Maybe Condition
forall a. Maybe a
Nothing) MorphRule
rule.ematch (MorphRule -> Either String ([Premise], Conclusion Expression)
morphingSpine MorphRule
rule)

dataizationOf :: Y.DataizeRule -> Inference Bytes
dataizationOf :: DataizeRule -> Inference Bytes
dataizationOf DataizeRule
rule = (Bytes -> Subst -> IO Bytes)
-> Rule
-> Expression
-> Either String ([Premise], Conclusion Bytes)
-> Inference Bytes
forall value.
(value -> Subst -> IO value)
-> Rule
-> Expression
-> Either String ([Premise], Conclusion value)
-> Inference value
interpreted Bytes -> Subst -> IO Bytes
buildBytesThrows (String
-> Maybe String
-> Maybe String
-> Expression
-> Expression
-> Maybe Condition
-> Maybe [Extra]
-> Maybe Condition
-> Rule
Y.Rule DataizeRule
rule.name Maybe String
forall a. Maybe a
Nothing Maybe String
forall a. Maybe a
Nothing DataizeRule
rule.match Expression
ExRoot DataizeRule
rule.when Maybe [Extra]
forall a. Maybe a
Nothing Maybe Condition
forall a. Maybe a
Nothing) DataizeRule
rule.ematch (DataizeRule -> Either String ([Premise], Conclusion Bytes)
dataizationSpine DataizeRule
rule)

interpreted :: forall value. (value -> Subst -> IO value) -> Y.Rule -> Expression -> Either String ([Y.Premise], Conclusion value) -> Inference value
interpreted :: forall value.
(value -> Subst -> IO value)
-> Rule
-> Expression
-> Either String ([Premise], Conclusion value)
-> Inference value
interpreted value -> Subst -> IO value
build Rule
rule Expression
ematch Either String ([Premise], Conclusion value)
spine RuleContext
ctx Expression
term Expression
univ = do
  [Subst]
matched <- [Subst] -> Expression -> Rule -> RuleContext -> IO [Subst]
matchExpressionWithRule' (MatchExpressionFunc
matchExpression' Expression
ematch Expression
univ) Expression
term Rule
rule RuleContext
ctx
  case ([Subst]
matched, Either String ([Premise], Conclusion value)
spine) of
    ([], Either String ([Premise], Conclusion value)
_) -> Maybe (Premises value) -> IO (Maybe (Premises value))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Premises value)
forall a. Maybe a
Nothing
    ([Subst]
_, Left String
reason) -> String -> IO (Maybe (Premises value))
forall a. String -> IO a
refuse String
reason
    (Subst
subst : [Subst]
_, Right ([Premise]
sides, Conclusion value
conclusion)) -> Premises value -> Maybe (Premises value)
forall a. a -> Maybe a
Just (Premises value -> Maybe (Premises value))
-> IO (Premises value) -> IO (Maybe (Premises value))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Premise] -> Conclusion value -> Subst -> IO (Premises value)
premised [Premise]
sides Conclusion value
conclusion Subst
subst
  where
    premised :: [Y.Premise] -> Conclusion value -> Subst -> IO (Premises value)
    premised :: [Premise] -> Conclusion value -> Subst -> IO (Premises value)
premised [] Conclusion value
conclusion Subst
subst = Conclusion value -> Premises value
forall value. Conclusion value -> Premises value
Concludes (Conclusion value -> Premises value)
-> IO (Conclusion value) -> IO (Premises value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Conclusion value -> Subst -> IO (Conclusion value)
concluded Conclusion value
conclusion Subst
subst
    premised (Premise
premise : [Premise]
rest) Conclusion value
conclusion Subst
subst = case Premise
premise.operation of
      Y.OpMorph Expression
expr Expression
universe -> do
        Expression
world <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
universe Subst
subst
        Expression
morphed <- Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst
        Premises value -> IO (Premises value)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
-> Expression
-> (Expression -> IO (Premises value))
-> Premises value
forall value.
Expression
-> Expression
-> (Expression -> IO (Premises value))
-> Premises value
Morphs Expression
morphed Expression
world Expression -> IO (Premises value)
next)
      Y.OpEvaluate Expression
expr Expression
universe -> Expression
-> Expression
-> (Expression -> IO (Premises value))
-> Premises value
forall value.
Expression
-> Expression
-> (Expression -> IO (Premises value))
-> Premises value
Evaluates (Expression
 -> Expression
 -> (Expression -> IO (Premises value))
 -> Premises value)
-> IO Expression
-> IO
     (Expression
      -> (Expression -> IO (Premises value)) -> Premises value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst IO
  (Expression
   -> (Expression -> IO (Premises value)) -> Premises value)
-> IO Expression
-> IO ((Expression -> IO (Premises value)) -> Premises value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
universe Subst
subst IO ((Expression -> IO (Premises value)) -> Premises value)
-> IO (Expression -> IO (Premises value)) -> IO (Premises value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expression -> IO (Premises value))
-> IO (Expression -> IO (Premises value))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression -> IO (Premises value)
next
      Y.OpContextualize Expression
expr Expression
context -> Expression
-> Expression
-> (Expression -> IO (Premises value))
-> Premises value
forall value.
Expression
-> Expression
-> (Expression -> IO (Premises value))
-> Premises value
Contextualizes (Expression
 -> Expression
 -> (Expression -> IO (Premises value))
 -> Premises value)
-> IO Expression
-> IO
     (Expression
      -> (Expression -> IO (Premises value)) -> Premises value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst IO
  (Expression
   -> (Expression -> IO (Premises value)) -> Premises value)
-> IO Expression
-> IO ((Expression -> IO (Premises value)) -> Premises value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
context Subst
subst IO ((Expression -> IO (Premises value)) -> Premises value)
-> IO (Expression -> IO (Premises value)) -> IO (Premises value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expression -> IO (Premises value))
-> IO (Expression -> IO (Premises value))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expression -> IO (Premises value)
next
      Operation
_ -> String -> IO (Premises value)
forall a. String -> IO a
refuse (String -> ShowS
forall r. PrintfType r => String -> r
printf String
"its premise '%s' runs beside the spine, which only a 'morph', an 'evaluate' or a 'contextualize' can" (Text -> String
T.unpack Premise
premise.result))
      where
        next :: Expression -> IO (Premises value)
        next :: Expression -> IO (Premises value)
next Expression
answer = case Subst -> Subst -> Maybe Subst
combine (Text -> MetaValue -> Subst
substSingle Premise
premise.result (Expression -> MetaValue
MvExpression Expression
answer)) Subst
subst of
          Just Subst
subst' -> [Premise] -> Conclusion value -> Subst -> IO (Premises value)
premised [Premise]
rest Conclusion value
conclusion Subst
subst'
          Maybe Subst
Nothing -> IOError -> IO (Premises value)
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError (String -> ShowS
forall r. PrintfType r => String -> r
printf String
"premise meta '%s' clashes with an existing binding" (Text -> String
T.unpack Premise
premise.result)))
    concluded :: Conclusion value -> Subst -> IO (Conclusion value)
    concluded :: Conclusion value -> Subst -> IO (Conclusion value)
concluded (Answered (Judgment, String)
step value
value) Subst
subst = (Judgment, String) -> value -> Conclusion value
forall value. (Judgment, String) -> value -> Conclusion value
Answered (Judgment, String)
step (value -> Conclusion value) -> IO value -> IO (Conclusion value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> value -> Subst -> IO value
build value
value Subst
subst
    concluded (Onward (Staged Expression
stage) Expression
expr Expression
world) Subst
subst = Way -> Expression -> Expression -> Conclusion value
forall value. Way -> Expression -> Expression -> Conclusion value
Onward (Way -> Expression -> Expression -> Conclusion value)
-> (Expression -> Way)
-> Expression
-> Expression
-> Expression
-> Conclusion value
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expression -> Way
Staged (Expression -> Expression -> Expression -> Conclusion value)
-> IO Expression
-> IO (Expression -> Expression -> Conclusion value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
stage Subst
subst IO (Expression -> Expression -> Conclusion value)
-> IO Expression -> IO (Expression -> Conclusion value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst IO (Expression -> Conclusion value)
-> IO Expression -> IO (Conclusion value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
world Subst
subst
    concluded (Onward Way
way Expression
expr Expression
world) Subst
subst = Way -> Expression -> Expression -> Conclusion value
forall value. Way -> Expression -> Expression -> Conclusion value
Onward Way
way (Expression -> Expression -> Conclusion value)
-> IO Expression -> IO (Expression -> Conclusion value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
expr Subst
subst IO (Expression -> Conclusion value)
-> IO Expression -> IO (Conclusion value)
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expression -> Subst -> IO Expression
buildExpressionThrows Expression
world Subst
subst
    refuse :: String -> IO a
    refuse :: forall a. String -> IO a
refuse String
reason = IOError -> IO a
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError (String -> String -> ShowS
forall r. PrintfType r => String -> r
printf String
"The rule '%s' cannot be run, since %s" Rule
rule.name String
reason))

direct :: (Expression -> Expression -> [Premises value]) -> Inference value
direct :: forall value.
(Expression -> Expression -> [Premises value]) -> Inference value
direct Expression -> Expression -> [Premises value]
rule RuleContext
_ Expression
term Expression
univ = Maybe (Premises value) -> IO (Maybe (Premises value))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Premises value] -> Maybe (Premises value)
forall a. [a] -> Maybe a
listToMaybe (Expression -> Expression -> [Premises value]
rule Expression
term Expression
univ))