{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}

-- | Revision-bound Lean identities and statement anchors.
module Conformance.Story.Binding
    ( BoundObligation (..)
    , Binding
    , ManifestEntry (..)
    , mkBoundObligation
    , firstExisting
    , loadManifest
    , resolveBinding
    , loadStatementSource
    , anchorsPresent
    , nameViolation
    , resolveClause
    ) where

import Data.Aeson (FromJSON (..), eitherDecode, withObject, (.:))
import Data.ByteString.Lazy qualified as BSL
import Data.List (isInfixOf)
import Data.Maybe (fromMaybe)
import Data.Text (Text)
import Data.Text qualified as T
import System.Directory (doesFileExist)

-- | A Lean obligation the programs bind to.
data BoundObligation = BoundObligation
    { BoundObligation -> String
boName :: !String
    , BoundObligation -> String
boDigest :: !String
    , BoundObligation -> String
boRevision :: !String
    }
    deriving stock (Int -> BoundObligation -> ShowS
[BoundObligation] -> ShowS
BoundObligation -> String
(Int -> BoundObligation -> ShowS)
-> (BoundObligation -> String)
-> ([BoundObligation] -> ShowS)
-> Show BoundObligation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BoundObligation -> ShowS
showsPrec :: Int -> BoundObligation -> ShowS
$cshow :: BoundObligation -> String
show :: BoundObligation -> String
$cshowList :: [BoundObligation] -> ShowS
showList :: [BoundObligation] -> ShowS
Show, BoundObligation -> BoundObligation -> Bool
(BoundObligation -> BoundObligation -> Bool)
-> (BoundObligation -> BoundObligation -> Bool)
-> Eq BoundObligation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BoundObligation -> BoundObligation -> Bool
== :: BoundObligation -> BoundObligation -> Bool
$c/= :: BoundObligation -> BoundObligation -> Bool
/= :: BoundObligation -> BoundObligation -> Bool
Eq)

-- | Name a bound obligation by qualified declaration, digest, revision.
mkBoundObligation :: String -> String -> String -> BoundObligation
mkBoundObligation :: String -> String -> String -> BoundObligation
mkBoundObligation = String -> String -> String -> BoundObligation
BoundObligation

-- | A binding is a bound obligation.
type Binding = BoundObligation

-- | One row of the repository's statement manifest.
data ManifestEntry = ManifestEntry
    { ManifestEntry -> String
meName :: !String
    , ManifestEntry -> String
meDigest :: !String
    }

instance FromJSON ManifestEntry where
    parseJSON :: Value -> Parser ManifestEntry
parseJSON = String
-> (Object -> Parser ManifestEntry)
-> Value
-> Parser ManifestEntry
forall a. String -> (Object -> Parser a) -> Value -> Parser a
withObject String
"ManifestEntry" ((Object -> Parser ManifestEntry) -> Value -> Parser ManifestEntry)
-> (Object -> Parser ManifestEntry)
-> Value
-> Parser ManifestEntry
forall a b. (a -> b) -> a -> b
$ \Object
o ->
        String -> String -> ManifestEntry
ManifestEntry (String -> String -> ManifestEntry)
-> Parser String -> Parser (String -> ManifestEntry)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Object
o Object -> Key -> Parser String
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"name" Parser (String -> ManifestEntry)
-> Parser String -> Parser ManifestEntry
forall a b. Parser (a -> b) -> Parser a -> Parser b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Object
o Object -> Key -> Parser String
forall a. FromJSON a => Object -> Key -> Parser a
.: Key
"statementSha256"

-- | First of the candidate paths that exists on disk.
firstExisting :: [FilePath] -> IO (Maybe FilePath)
firstExisting :: [String] -> IO (Maybe String)
firstExisting [] = Maybe String -> IO (Maybe String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
firstExisting (String
p : [String]
ps) = do
    exists <- String -> IO Bool
doesFileExist String
p
    if exists then pure (Just p) else firstExisting ps

-- | Read the repository's own statement manifest.
loadManifest :: IO (Either String [(String, String)])
loadManifest :: IO (Either String [(String, String)])
loadManifest = do
    found <-
        [String] -> IO (Maybe String)
firstExisting [String
"../lean/theorem-debt.json", String
"lean/theorem-debt.json"]
    case found of
        Maybe String
Nothing ->
            Either String [(String, String)]
-> IO (Either String [(String, String)])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                (String -> Either String [(String, String)]
forall a b. a -> Either a b
Left String
"statement manifest not found: want ../lean/theorem-debt.json")
        Just String
path -> do
            content <- String -> IO ByteString
BSL.readFile String
path
            case eitherDecode content :: Either String [ManifestEntry] of
                Left String
err -> Either String [(String, String)]
-> IO (Either String [(String, String)])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String [(String, String)]
forall a b. a -> Either a b
Left (String
"statement manifest does not parse: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
err))
                Right [ManifestEntry]
entries -> Either String [(String, String)]
-> IO (Either String [(String, String)])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(String, String)] -> Either String [(String, String)]
forall a b. b -> Either a b
Right [(ManifestEntry -> String
meName ManifestEntry
e, ManifestEntry -> String
meDigest ManifestEntry
e) | ManifestEntry
e <- [ManifestEntry]
entries])

{- | A binding resolves exactly when the manifest carries the named
declaration under the pinned digest.
-}
resolveBinding :: [(String, String)] -> Binding -> Bool
resolveBinding :: [(String, String)] -> BoundObligation -> Bool
resolveBinding [(String, String)]
manifest BoundObligation
obligation =
    String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (BoundObligation -> String
boName BoundObligation
obligation) [(String, String)]
manifest Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just (BoundObligation -> String
boDigest BoundObligation
obligation)

-- | Read the bound Lean source.
loadStatementSource :: IO (Either String String)
loadStatementSource :: IO (Either String String)
loadStatementSource = do
    found <-
        [String] -> IO (Maybe String)
firstExisting
            [String
"../lean/Singular/Statements.lean", String
"lean/Singular/Statements.lean"]
    case found of
        Maybe String
Nothing ->
            Either String String -> IO (Either String String)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( String -> Either String String
forall a b. a -> Either a b
Left
                    String
"statement source not found: want ../lean/Singular/Statements.lean"
                )
        Just String
path -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String)
-> IO String -> IO (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
path

{- | Every anchor quoted anywhere in the inventory appears verbatim in
the source.
-}
anchorsPresent :: String -> [(String, [String])] -> Bool
anchorsPresent :: String -> [(String, [String])] -> Bool
anchorsPresent String
source [(String, [String])]
inventory =
    (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all
        (String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
source)
        [String
anchor | (String
_, [String]
anchors) <- [(String, [String])]
inventory, String
anchor <- [String]
anchors]

{- | Whether a clause or example name smuggles in a row ID or ticket
number. One predicate, used by every hygiene check.
-}
nameViolation :: String -> Bool
nameViolation :: String -> Bool
nameViolation String
n = String
"CG" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
n Bool -> Bool -> Bool
|| Char
'#' Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
n

{- | A clause resolves exactly when every selected anchor belongs to
the named obligation's inventory.
-}
resolveClause :: [(String, [String])] -> Binding -> [Text] -> Bool
resolveClause :: [(String, [String])] -> BoundObligation -> [Text] -> Bool
resolveClause [(String, [String])]
inventory BoundObligation
obligation [Text]
anchors =
    Bool -> Bool
not ([Text] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Text]
anchors)
        Bool -> Bool -> Bool
&& (Text -> Bool) -> [Text] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Text -> [Text] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack (String -> [String]
anchorsFor (BoundObligation -> String
boName BoundObligation
obligation))) [Text]
anchors
  where
    anchorsFor :: String -> [String]
anchorsFor String
name = [String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe [] (String -> [(String, [String])] -> Maybe [String]
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
name [(String, [String])]
inventory)