{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedRecordDot #-}

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

module Contextualize (concluded, contextualize, ContextualizeException (..)) where

import AST
import Builder (buildExpression)
import Control.Exception (Exception, throwIO)
import Control.Monad (foldM)
import Data.Bifunctor (first)
import Data.List (intercalate)
import qualified Data.Text as T
import Matcher (MetaValue (..), Subst, combine, matchExpression', substSingle)
import Printer (printExpression)
import Text.Printf (printf)
import qualified Yaml as Y

data ContextualizeException = Uncontextualizable Expression String
  deriving (Show ContextualizeException
Typeable ContextualizeException
(Typeable ContextualizeException, Show ContextualizeException) =>
(ContextualizeException -> SomeException)
-> (SomeException -> Maybe ContextualizeException)
-> (ContextualizeException -> [Char])
-> Exception ContextualizeException
SomeException -> Maybe ContextualizeException
ContextualizeException -> [Char]
ContextualizeException -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> [Char]) -> Exception e
$ctoException :: ContextualizeException -> SomeException
toException :: ContextualizeException -> SomeException
$cfromException :: SomeException -> Maybe ContextualizeException
fromException :: SomeException -> Maybe ContextualizeException
$cdisplayException :: ContextualizeException -> [Char]
displayException :: ContextualizeException -> [Char]
Exception)

instance Show ContextualizeException where
  show :: ContextualizeException -> [Char]
show (Uncontextualizable Expression
term [Char]
reason) = [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"Contextualization has no single conclusion, since %s: %s" [Char]
reason (Expression -> [Char]
printExpression Expression
term)

concluded :: Expression -> [(String, Either ContextualizeException Expression)] -> Either ContextualizeException Expression
concluded :: Expression
-> [([Char], Either ContextualizeException Expression)]
-> Either ContextualizeException Expression
concluded Expression
_ [([Char]
_, Either ContextualizeException Expression
answer)] = Either ContextualizeException Expression
answer
concluded Expression
term [] = ContextualizeException -> Either ContextualizeException Expression
forall a b. a -> Either a b
Left (Expression -> [Char] -> ContextualizeException
Uncontextualizable Expression
term [Char]
"no contextualization rule matches the term")
concluded Expression
term [([Char], Either ContextualizeException Expression)]
several = ContextualizeException -> Either ContextualizeException Expression
forall a b. a -> Either a b
Left (Expression -> [Char] -> ContextualizeException
Uncontextualizable Expression
term ([Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"the contextualization rules %s all match the term" ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " ((([Char], Either ContextualizeException Expression) -> [Char])
-> [([Char], Either ContextualizeException Expression)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char], Either ContextualizeException Expression) -> [Char]
forall a b. (a, b) -> a
fst [([Char], Either ContextualizeException Expression)]
several))))

contextualize :: Expression -> Expression -> IO Expression
contextualize :: Expression -> Expression -> IO Expression
contextualize Expression
expr Expression
context = (ContextualizeException -> IO Expression)
-> (Expression -> IO Expression)
-> Either ContextualizeException Expression
-> IO Expression
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ContextualizeException -> IO Expression
forall e a. Exception e => e -> IO a
throwIO Expression -> IO Expression
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expression
-> Expression -> Either ContextualizeException Expression
contextualized Expression
expr Expression
context)
  where
    contextualized :: Expression -> Expression -> Either ContextualizeException Expression
    contextualized :: Expression
-> Expression -> Either ContextualizeException Expression
contextualized Expression
term Expression
around =
      Expression
-> [([Char], Either ContextualizeException Expression)]
-> Either ContextualizeException Expression
concluded
        Expression
term
        [ (ContextualizeRule
rule.name, (Subst -> Premise -> Either ContextualizeException Subst)
-> Subst -> [Premise] -> Either ContextualizeException Subst
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Expression
-> ContextualizeRule
-> Subst
-> Premise
-> Either ContextualizeException Subst
premised Expression
term ContextualizeRule
rule) Subst
subst ContextualizeRule
rule.premises Either ContextualizeException Subst
-> (Subst -> Either ContextualizeException Expression)
-> Either ContextualizeException Expression
forall a b.
Either ContextualizeException a
-> (a -> Either ContextualizeException b)
-> Either ContextualizeException b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expression
-> ContextualizeRule
-> Expression
-> Subst
-> Either ContextualizeException Expression
built Expression
term ContextualizeRule
rule ContextualizeRule
rule.cresult)
        | (ContextualizeRule
rule, Subst
subst) <- Expression -> Expression -> [(ContextualizeRule, Subst)]
matching Expression
term Expression
around
        ]
    matching :: Expression -> Expression -> [(Y.ContextualizeRule, Subst)]
    matching :: Expression -> Expression -> [(ContextualizeRule, Subst)]
matching Expression
term Expression
around =
      [ (ContextualizeRule
rule, Subst
subst)
      | ContextualizeRule
rule <- [ContextualizeRule]
Y.contextualizationRules
      , Subst
matched <- MatchExpressionFunc
matchExpression' ContextualizeRule
rule.match Expression
term
      , Subst
surrounding <- MatchExpressionFunc
matchExpression' ContextualizeRule
rule.cmatch Expression
around
      , Just Subst
subst <- [Subst -> Subst -> Maybe Subst
combine Subst
matched Subst
surrounding]
      ]
    premised :: Expression -> Y.ContextualizeRule -> Subst -> Y.Premise -> Either ContextualizeException Subst
    premised :: Expression
-> ContextualizeRule
-> Subst
-> Premise
-> Either ContextualizeException Subst
premised Expression
term ContextualizeRule
rule Subst
subst (Y.Premise Text
result (Y.OpContextualize Expression
inner Expression
outer)) = do
      Expression
part <- Expression
-> ContextualizeRule
-> Expression
-> Subst
-> Either ContextualizeException Expression
built Expression
term ContextualizeRule
rule Expression
inner Subst
subst
      Expression
surrounding <- Expression
-> ContextualizeRule
-> Expression
-> Subst
-> Either ContextualizeException Expression
built Expression
term ContextualizeRule
rule Expression
outer Subst
subst
      Expression
answer <- Expression
-> Expression -> Either ContextualizeException Expression
contextualized Expression
part Expression
surrounding
      Either ContextualizeException Subst
-> (Subst -> Either ContextualizeException Subst)
-> Maybe Subst
-> Either ContextualizeException Subst
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
        (ContextualizeException -> Either ContextualizeException Subst
forall a b. a -> Either a b
Left (Expression -> [Char] -> ContextualizeException
Uncontextualizable Expression
term ([Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"the premise '%s' of the contextualization rule '%s' clashes with a binding" (Text -> [Char]
T.unpack Text
result) ContextualizeRule
rule.name)))
        Subst -> Either ContextualizeException Subst
forall a b. b -> Either a b
Right
        (Subst -> Subst -> Maybe Subst
combine (Text -> MetaValue -> Subst
substSingle Text
result (Expression -> MetaValue
MvExpression Expression
answer)) Subst
subst)
    premised Expression
term ContextualizeRule
rule Subst
_ Premise
premise =
      ContextualizeException -> Either ContextualizeException Subst
forall a b. a -> Either a b
Left (Expression -> [Char] -> ContextualizeException
Uncontextualizable Expression
term ([Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"the premise '%s' of the contextualization rule '%s' is not a contextualization" (Text -> [Char]
T.unpack Premise
premise.result) ContextualizeRule
rule.name))
    built :: Expression -> Y.ContextualizeRule -> Expression -> Subst -> Either ContextualizeException Expression
    built :: Expression
-> ContextualizeRule
-> Expression
-> Subst
-> Either ContextualizeException Expression
built Expression
term ContextualizeRule
rule Expression
template Subst
subst =
      ([Char] -> ContextualizeException)
-> Either [Char] Expression
-> Either ContextualizeException Expression
forall a b c. (a -> b) -> Either a c -> Either b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first
        (Expression -> [Char] -> ContextualizeException
Uncontextualizable Expression
term ([Char] -> ContextualizeException)
-> ([Char] -> [Char]) -> [Char] -> ContextualizeException
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"the contextualization rule '%s' cannot be built, %s" ContextualizeRule
rule.name)
        (Expression -> Subst -> Either [Char] Expression
buildExpression Expression
template Subst
subst)