path: root/source/Checking/Exact/Inductive.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Exact preparation and atomic publication of direct set inductives.
module Checking.Exact.Inductive
    ( PreparedExactInductive
    , preparedExactInductiveCarrierId
    , preparedExactInductiveCarrierType
    , preparedExactInductiveCarrierBody
    , preparedExactInductiveGuardTargets
    , preparedExactInductiveFacts
    , prepareExactInductive
    , CheckedExactInductiveAuthorization
    , lowerPreparedExactInductive
    , authorizeCheckedExactInductive
    , ExactInductiveError(..)
    , exactInductiveErrorLocation
    , renderExactInductiveError
    ) where

import Base hiding (Empty)
import Checking.Authority
import Checking.Core
import Checking.Declaration qualified as Declaration
import Checking.Exact.Global qualified as ExactGlobal
import Checking.Exact.Vocabulary
import Checking.Foundation
import Checking.Identity
import Checking.Semantic
import Checking.Typed.Inductive qualified as Typed
import Felix.Cache.Codec
import Meaning qualified
import Report.Location
import Syntax.Abstract qualified as Raw
import Syntax.Interface
import Syntax.Internal qualified as Internal

import Control.Monad (unless, when)
import Control.Monad.Except (ExceptT)
import Control.Monad.Except qualified as Except
import Data.Bifunctor (first)
import Data.ByteString (ByteString)
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Vector qualified as Vector


data PreparedExactInductive = PreparedExactInductive
    !Location
    !SemanticGlobalKey
    !ObjectId
    !(Maybe AssertedObject)
    !SemanticName
    !DeclarationSyntaxId
    !(Typed.PreparedTypedInductive ObjectId)
    ![SemanticFactOccurrenceFingerprint]

data CheckedExactInductiveAuthorization =
    CheckedExactInductiveAuthorization
        !ObjectId
        !(Typed.PreparedTypedInductive ObjectId)
        ![SemanticFactOccurrenceFingerprint]

preparedExactInductiveCarrierId
    :: PreparedExactInductive
    -> ObjectId
preparedExactInductiveCarrierId
        (PreparedExactInductive
            _location _key identity _asserted _alias _syntax _typed _guards) =
    identity

preparedExactInductiveCarrierType
    :: PreparedExactInductive
    -> CoreType
preparedExactInductiveCarrierType
        (PreparedExactInductive
            _location _key _identity _asserted _alias _syntax typed _guards) =
    Typed.typedInductiveCarrierType typed

preparedExactInductiveCarrierBody
    :: PreparedExactInductive
    -> FrozenCheckedCore ObjectId
preparedExactInductiveCarrierBody
        (PreparedExactInductive
            _location _key _identity _asserted _alias _syntax typed _guards) =
    Typed.typedInductiveCarrierBody typed

preparedExactInductiveGuardTargets
    :: PreparedExactInductive
    -> Vector.Vector (FrozenCheckedCore ObjectId)
preparedExactInductiveGuardTargets
        (PreparedExactInductive
            _location _key _identity _asserted _alias _syntax typed _guards) =
    Typed.typedInductiveGuardTargets typed

preparedExactInductiveFacts
    :: PreparedExactInductive
    -> NonEmpty (Typed.PreparedTypedInductiveFact ObjectId)
preparedExactInductiveFacts
        (PreparedExactInductive
            _location _key _identity _asserted _alias _syntax typed _guards) =
    Typed.typedInductiveFacts typed

data ExactInductiveError
    = ExactInductiveUnsupportedBlock !Location
    | ExactInductiveOccurrenceMissing !Location
    | ExactInductiveOccurrenceAmbiguous !Location
    | ExactInductiveHeadMismatch !Location
    | ExactInductiveGlossFailed !Location !Meaning.GlossError
    | ExactInductiveDuplicateParameter !Location !Internal.VarSymbol
    | ExactInductiveDomainFreeVariable !Location !Internal.VarSymbol
    | ExactInductiveDomainMentionsCarrier !Location
    | ExactInductiveResultShape !Location
    | ExactInductiveResultMentionsCarrier !Location
    | ExactInductiveRecursiveTermMentionsCarrier !Location
    | ExactInductiveNestedRecursion !Location
    | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey
    | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey
    | ExactInductiveGlobalNotVisible !Location !Internal.Symbol
    | ExactInductiveGlobalAmbiguous !Location !Internal.Symbol
    | ExactInductiveUnsupportedSymbol !Location !Internal.Symbol
    | ExactInductiveGlobalContentInvalid !Location !CoreCheckError
    | ExactInductivePreparationFailed
        !Location
        !Typed.TypedInductiveError
    | ExactInductiveGuardMissing !Location
    | ExactInductiveGuardAmbiguous !Location
    deriving stock (Show, Eq)

exactInductiveErrorLocation :: ExactInductiveError -> Location
exactInductiveErrorLocation = \case
    ExactInductiveUnsupportedBlock location -> location
    ExactInductiveOccurrenceMissing location -> location
    ExactInductiveOccurrenceAmbiguous location -> location
    ExactInductiveHeadMismatch location -> location
    ExactInductiveGlossFailed location _failure -> location
    ExactInductiveDuplicateParameter location _parameter -> location
    ExactInductiveDomainFreeVariable location _variable -> location
    ExactInductiveDomainMentionsCarrier location -> location
    ExactInductiveResultShape location -> location
    ExactInductiveResultMentionsCarrier location -> location
    ExactInductiveRecursiveTermMentionsCarrier location -> location
    ExactInductiveNestedRecursion location -> location
    ExactInductiveFixedSemanticCollision location _key -> location
    ExactInductiveGlobalAlreadyVisible location _key -> location
    ExactInductiveGlobalNotVisible location _symbol -> location
    ExactInductiveGlobalAmbiguous location _symbol -> location
    ExactInductiveUnsupportedSymbol location _symbol -> location
    ExactInductiveGlobalContentInvalid location _failure -> location
    ExactInductivePreparationFailed location _failure -> location
    ExactInductiveGuardMissing location -> location
    ExactInductiveGuardAmbiguous location -> location

renderExactInductiveError :: ExactInductiveError -> Text
renderExactInductiveError failure =
    locationToText (exactInductiveErrorLocation failure)
        <> ": "
        <> case failure of
            ExactInductiveUnsupportedBlock{} ->
                "this inductive source form is not supported by the typed checker"
            ExactInductiveOccurrenceMissing{} ->
                "the inductive declaration has no associated syntax occurrence"
            ExactInductiveOccurrenceAmbiguous{} ->
                "the inductive declaration has more than one semantic head"
            ExactInductiveHeadMismatch{} ->
                "the inductive head does not match its syntax occurrence"
            ExactInductiveGlossFailed _location glossFailure ->
                "inductive elaboration failed: " <> shown glossFailure
            ExactInductiveDuplicateParameter _location parameter ->
                "the inductive parameter is repeated: " <> shown parameter
            ExactInductiveDomainFreeVariable _location variable ->
                "the inductive domain contains an unbound variable: "
                    <> shown variable
            ExactInductiveDomainMentionsCarrier{} ->
                "the inductive domain must be independent of its carrier"
            ExactInductiveResultShape{} ->
                "an inductive result must have the form t \\in F(args)"
            ExactInductiveResultMentionsCarrier{} ->
                "an inductive result term must not mention its carrier"
            ExactInductiveRecursiveTermMentionsCarrier{} ->
                "a recursive occurrence must be in the carrier of a membership premise"
            ExactInductiveNestedRecursion{} ->
                "nested inductive recursion is not supported by the typed checker"
            ExactInductiveFixedSemanticCollision _location key ->
                "the inductive carrier collides with fixed semantics for "
                    <> shown key
            ExactInductiveGlobalAlreadyVisible _location key ->
                "the inductive carrier is already visible: " <> shown key
            ExactInductiveGlobalNotVisible _location symbol ->
                "an inductive source symbol is not visible: " <> shown symbol
            ExactInductiveGlobalAmbiguous _location symbol ->
                "an inductive source symbol has more than one meaning: "
                    <> shown symbol
            ExactInductiveUnsupportedSymbol _location symbol ->
                "this inductive source symbol is not supported: "
                    <> shown symbol
            ExactInductiveGlobalContentInvalid _location coreFailure ->
                "an inductive global has invalid checked content: "
                    <> shown coreFailure
            ExactInductivePreparationFailed _location typedFailure ->
                "typed inductive preparation failed: " <> shown typedFailure
            ExactInductiveGuardMissing{} ->
                "an inductive domain guard has no visible authorized fact"
            ExactInductiveGuardAmbiguous{} ->
                "an inductive domain guard matches more than one visible fact"
  where
    shown :: Show value => value -> Text
    shown = Text.pack . show

type Prepare =
    ExceptT
        ExactInductiveError
        (Declaration.LoweringDriver)

prepareExactInductive
    :: CheckedFoundation
    -> Raw.Block
    -> [CanonicalLexicalEntry]
    -> Declaration.LoweringDriver
        (Either ExactInductiveError PreparedExactInductive)
prepareExactInductive foundation block entries =
    Except.runExceptT do
        (location, marker, rawInductive) <-
            case block of
                Raw.BlockInductive blockLocation _title blockMarker inductive ->
                    pure (blockLocation, blockMarker, inductive)
                _ ->
                    Except.throwError
                        (ExactInductiveUnsupportedBlock (locate block))
        key <- validateOccurrence location rawInductive entries
        when
            (isJust (fixedSemanticMeaning key))
            (Except.throwError
                (ExactInductiveFixedSemanticCollision location key))
        visible <-
            Except.lift
                (Declaration.resolveVisibleGlobalLowering key)
        when (isJust visible)
            (Except.throwError
                (ExactInductiveGlobalAlreadyVisible location key))
        internal <-
            case Meaning.meaning [block] of
                Right
                    [Internal.BlockInductive
                        _internalLocation _internalMarker inductive] ->
                            pure inductive
                Left failure ->
                    Except.throwError
                        (ExactInductiveGlossFailed location failure)
                Right _ ->
                    Except.throwError
                        (ExactInductiveUnsupportedBlock location)
        direct <-
            Except.liftEither
                (normalizeDirectInductive internal)
        (sourceGlobals, globalTypes) <-
            resolveSourceGlobals location internal direct
        typed <-
            Except.liftEither
                (first
                    (ExactInductivePreparationFailed location)
                    (Typed.prepareTypedInductive
                        (requireGlobalType globalTypes)
                        foundation
                        (`Map.lookup` sourceGlobals)
                        marker
                        direct))
        guards <-
            traverse
                (resolveGuard location)
                (Vector.toList
                    (Typed.typedInductiveGuardTargets typed))
        theory <- Except.lift Declaration.currentTheoryLowering
        let carrierType = Typed.typedInductiveCarrierType typed
            carrierBody = Typed.typedInductiveCarrierBody typed
            carrierTerm = frozenCoreTerm carrierBody
            identity =
                transparentObjectId theory carrierType carrierTerm
            content =
                TransparentObjectContent theory carrierType carrierTerm
            alias = case marker of
                Raw.Marker name -> semanticName name
        available <-
            Except.lift
                (Declaration.objectAvailableLowering identity)
        let asserted
                | available = Nothing
                | otherwise = Just (assertedObject identity content)
            syntax =
                declarationSyntaxId
                    (encodePreparedInductive key alias typed)
        pure
            (PreparedExactInductive
                location
                key
                identity
                asserted
                alias
                syntax
                typed
                guards)
  where
    requireGlobalType types identity =
        fromMaybe
            (impossible
                "prepared inductive global has no checked type")
            (Map.lookup identity types)

validateOccurrence
    :: Location
    -> Raw.Inductive
    -> [CanonicalLexicalEntry]
    -> Prepare SemanticGlobalKey
validateOccurrence location rawInductive entries = do
    entry <-
        case entries of
            [] ->
                Except.throwError
                    (ExactInductiveOccurrenceMissing location)
            [single] -> pure single
            _ ->
                Except.throwError
                    (ExactInductiveOccurrenceAmbiguous location)
    key <-
        maybe
            (Except.throwError
                (ExactInductiveHeadMismatch location))
            pure
            (semanticGlobalKeyFromLexicalEntry entry)
    let Raw.SymbolPattern headSymbol _parameters =
            Raw.inductiveSymbolPattern rawInductive
        expected =
            SemanticExpressionFunction
                (Raw.mixfixPattern headSymbol)
    unless (key == expected)
        (Except.throwError
            (ExactInductiveHeadMismatch location))
    pure key

normalizeDirectInductive
    :: Internal.Inductive
    -> Either ExactInductiveError Typed.DirectInductive
normalizeDirectInductive inductive = do
    case firstDuplicate (Internal.inductiveParams inductive) of
        Just duplicate ->
            Left
                (ExactInductiveDuplicateParameter
                    (locate duplicate)
                    duplicate)
        Nothing -> pure ()
    let parameters = Internal.inductiveParams inductive
        parameterSet = Set.fromList parameters
        domain = Internal.inductiveDomain inductive
        carrier = Internal.inductiveSymbol inductive
        domainVariables =
            orderedUnique
                (toList domain)
    case find (`Set.notMember` parameterSet) domainVariables of
        Just variable ->
            Left
                (ExactInductiveDomainFreeVariable
                    (locate variable)
                    variable)
        Nothing -> pure ()
    when
        (Internal.SymbolMixfix carrier
            `Set.member` Internal.mentionedSymbols domain)
        (Left
            (ExactInductiveDomainMentionsCarrier
                (termLocation domain)))
    clauses <-
        traverse
            (normalizeClause carrier parameters)
            (Internal.inductiveIntros inductive)
    pure
        (Typed.DirectInductive
            parameters
            domain
            clauses)

normalizeClause
    :: Internal.FunctionSymbol
    -> [Internal.VarSymbol]
    -> Internal.IntroRule
    -> Either ExactInductiveError Typed.DirectInductiveClause
normalizeClause carrier parameters rule = do
    conditions <-
        traverse
            (normalizeCondition carrier parameters)
            (Internal.introConditions rule)
    result <-
        normalizeResult
            carrier
            parameters
            (Internal.introResult rule)
    let parameterSet = Set.fromList parameters
        variables =
            List.filter (`Set.notMember` parameterSet)
                (orderedUnique
                    ( concatMap toList
                        (Internal.introConditions rule)
                      <> toList result
                    ))
    pure
        (Typed.DirectInductiveClause
            variables
            conditions
            result)

normalizeResult
    :: Internal.FunctionSymbol
    -> [Internal.VarSymbol]
    -> Internal.Formula
    -> Either ExactInductiveError Internal.Term
normalizeResult carrier parameters = \case
    Internal.IsElementOf _location result target
        | not (matchesCarrier carrier parameters target) ->
            Left (ExactInductiveResultShape (termLocation target))
        | Internal.SymbolMixfix carrier
                `Set.member` Internal.mentionedSymbols result ->
            Left
                (ExactInductiveResultMentionsCarrier
                    (termLocation result))
        | otherwise ->
            Right result
    formula ->
        Left (ExactInductiveResultShape (termLocation formula))

normalizeCondition
    :: Internal.FunctionSymbol
    -> [Internal.VarSymbol]
    -> Internal.Formula
    -> Either ExactInductiveError Typed.DirectInductiveCondition
normalizeCondition carrier parameters formula
    | not
        (Internal.SymbolMixfix carrier
            `Set.member` Internal.mentionedSymbols formula) =
        Right (Typed.DirectSideCondition formula)
    | otherwise =
        case formula of
            Internal.IsElementOf _location recursiveTerm recursiveCarrier
                | Internal.SymbolMixfix carrier
                        `Set.member`
                            Internal.mentionedSymbols recursiveTerm ->
                    Left
                        (ExactInductiveRecursiveTermMentionsCarrier
                            (termLocation recursiveTerm))
                | matchesCarrier carrier parameters recursiveCarrier ->
                    Right
                        (Typed.DirectRecursiveCondition recursiveTerm)
                | otherwise ->
                    Left
                        (ExactInductiveNestedRecursion
                            (termLocation recursiveCarrier))
            _ ->
                Left
                    (ExactInductiveNestedRecursion
                        (termLocation formula))

matchesCarrier
    :: Internal.FunctionSymbol
    -> [Internal.VarSymbol]
    -> Internal.Term
    -> Bool
matchesCarrier carrier parameters = \case
    Internal.TermSymbol _location (Internal.SymbolMixfix actual) arguments ->
        actual == carrier
            && length arguments == length parameters
            && and
                (zipWith
                    (\argument parameter ->
                        argument == Internal.TermVar parameter)
                    arguments
                    parameters)
    _ -> False

resolveSourceGlobals
    :: Location
    -> Internal.Inductive
    -> Typed.DirectInductive
    -> Prepare
        ( Map.Map
            Internal.Symbol
            (Typed.SourceGlobal ObjectId)
        , Map.Map ObjectId CoreType
        )
resolveSourceGlobals location internal direct =
    Except.lift
        (ExactGlobal.resolveExactSourceGlobals symbols)
        >>= Except.liftEither
            . first (exactGlobalError location)
  where
    carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal)
    symbols =
        Set.delete carrier (directSymbols direct)

exactGlobalError
    :: Location
    -> ExactGlobal.ExactGlobalResolutionError
    -> ExactInductiveError
exactGlobalError location = \case
    ExactGlobal.ExactGlobalNotVisible symbol ->
        ExactInductiveGlobalNotVisible location symbol
    ExactGlobal.ExactGlobalAmbiguous symbol ->
        ExactInductiveGlobalAmbiguous location symbol
    ExactGlobal.ExactGlobalUnsupported symbol ->
        ExactInductiveUnsupportedSymbol location symbol
    ExactGlobal.ExactGlobalContextualUnsupported symbol ->
        ExactInductiveUnsupportedSymbol location symbol
    ExactGlobal.ExactGlobalContentInvalid failure ->
        ExactInductiveGlobalContentInvalid location failure

resolveGuard
    :: Location
    -> FrozenCheckedCore ObjectId
    -> Prepare SemanticFactOccurrenceFingerprint
resolveGuard location target = do
    matches <-
        Except.lift
            (Declaration.resolveVisibleFactTargetsLowering target)
    case matches of
        [] ->
            Except.throwError (ExactInductiveGuardMissing location)
        [fingerprint] ->
            pure fingerprint
        _ ->
            Except.throwError (ExactInductiveGuardAmbiguous location)

directSymbols :: Typed.DirectInductive -> Set.Set Internal.Symbol
directSymbols direct =
    Internal.mentionedSymbols (Typed.directInductiveDomain direct)
        <> foldMap clauseSymbols
            (Typed.directInductiveClauses direct)
  where
    clauseSymbols clause =
        foldMap conditionSymbols
                (Typed.directClauseConditions clause)
            <> Internal.mentionedSymbols
                (Typed.directClauseResult clause)
    conditionSymbols = \case
        Typed.DirectSideCondition formula ->
            Internal.mentionedSymbols formula
        Typed.DirectRecursiveCondition term ->
            Internal.mentionedSymbols term

lowerPreparedExactInductive
    :: PreparedExactInductive
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration
                CheckedExactInductiveAuthorization))
lowerPreparedExactInductive
        (PreparedExactInductive
            _location key identity asserted alias syntax typed guards) =
    do
        let facts = Typed.typedInductiveFacts typed
            objects = maybeToList asserted
        definition <-
            Declaration.prepareDefinitionEquationSpecLowering
                objects identity alias
        preparedCandidates <-
            traverse
                (\fact ->
                    fmap
                        (fmap
                            (\spec ->
                                Declaration.checkedCandidate spec
                                    (Declaration.checkedKernelPlanning
                                        (GuardedFoundationRules
                                            (guardedRuleSet
                                                (Typed.typedInductiveFactRules
                                                    fact)))
                                        guards)))
                        (Declaration.prepareCandidateSpecLowering
                            objects
                            (embedClosedCore []
                                (Typed.typedInductiveFactTarget fact))
                            SearchEligible
                            [markerAlias
                                (Typed.typedInductiveFactMarker fact)]))
                facts
        pure do
            definitionSpec <- definition
            factCandidates <- sequence preparedCandidates
            pure
                (Declaration.checkedCompiledDeclaration
                    syntax
                    objects
                    []
                    [semanticGlobalBinding key (GlobalReference identity)]
                    []
                    [ Declaration.checkedCandidate definitionSpec
                        (Declaration.checkedDefinitionEquationPlanning identity)
                        :| toList factCandidates
                    ]
                    (CheckedExactInductiveAuthorization
                        identity typed guards))
  where
    markerAlias (Raw.Marker name) =
        semanticName name

authorizeCheckedExactInductive
    :: CheckedExactInductiveAuthorization
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedExactInductive
        (CheckedExactInductiveAuthorization identity typed guards) = \case
    [definitionCandidate :| candidates] -> do
        Declaration.authorizeDefinitionEquationCandidate
            identity definitionCandidate
        let facts = Typed.typedInductiveFacts typed
        case NonEmpty.nonEmpty candidates of
            Just factCandidates
                | NonEmpty.length factCandidates == NonEmpty.length facts ->
                    sequence_
                        (NonEmpty.zipWith
                            authorizeFact
                            factCandidates
                            facts)
            _ ->
                Declaration.failDeclaration
                    (Declaration.CheckedAuthorizationCandidateShapeMismatch
                        (1 + NonEmpty.length facts)
                        (1 + length candidates))
    stages ->
        Declaration.failDeclaration
            (Declaration.CheckedAuthorizationCandidateShapeMismatch
                1 (length stages))
  where
    authorizeFact candidate fact =
        Declaration.authorizeKernelConstructionCandidate
            (GuardedFoundationRules
                (guardedRuleSet
                    (Typed.typedInductiveFactRules fact)))
            candidate do
                traverse_ Declaration.useAuthorizedFact guards
                pure (Typed.typedInductiveFactDerivation fact)

encodePreparedInductive
    :: SemanticGlobalKey
    -> SemanticName
    -> Typed.PreparedTypedInductive ObjectId
    -> ByteString
encodePreparedInductive key alias typed =
    encodeCache do
        putCacheTag 0x04
        putSemanticGlobalKeyCache key
        putCoreTypeCache
            (Typed.typedInductiveCarrierType typed)
        putCanonicalTermCache putObjectIdCache
            (frozenCoreTerm
                (Typed.typedInductiveCarrierBody typed))
        putCacheText (semanticNameText alias)
        putCacheList putFact
            (toList (Typed.typedInductiveFacts typed))
  where
    putFact fact = do
        let Raw.Marker marker =
                Typed.typedInductiveFactMarker fact
        putCacheText marker
        putCanonicalTermCache putObjectIdCache
            (frozenCoreTerm
                (Typed.typedInductiveFactTarget fact))
        putCacheList
            (putCacheBytes . encodeKernelRuleTag)
            (toList (Typed.typedInductiveFactRules fact))

firstDuplicate :: Ord value => [value] -> Maybe value
firstDuplicate =
    go Set.empty
  where
    go _seen [] = Nothing
    go seen (value : remaining)
        | value `Set.member` seen = Just value
        | otherwise =
            go (Set.insert value seen) remaining

orderedUnique :: Ord value => [value] -> [value]
orderedUnique =
    reverse . snd . foldl' step (Set.empty, [])
  where
    step (seen, values) value
        | value `Set.member` seen = (seen, values)
        | otherwise =
            (Set.insert value seen, value : values)

termLocation :: Internal.Expr -> Location
termLocation = Internal.exprLocation