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
    , commitPreparedExactInductive
    , ExactInductiveError(..)
    , exactInductiveErrorLocation
    , renderExactInductiveError
    ) where

import Base hiding (Empty)
import Checking.Authority
import Checking.Core
import Checking.Declaration qualified as Declaration
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 Syntax.Lexicon
    ( pattern ConsSymbol
    , pattern PairSymbol
    )

import Control.Monad (foldM, 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.Maybe (catMaybes)
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]

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
    | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey
    | ExactInductiveGlobalNotVisible !Location !Internal.Symbol
    | ExactInductiveGlobalAmbiguous !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
    ExactInductiveGlobalAlreadyVisible location _key -> location
    ExactInductiveGlobalNotVisible location _symbol -> location
    ExactInductiveGlobalAmbiguous 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"
            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
            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 failure =
    ExceptT
        ExactInductiveError
        (Declaration.ModuleDriver failure)

prepareExactInductive
    :: CheckedFoundation
    -> Raw.Block
    -> [CanonicalLexicalEntry]
    -> Declaration.ModuleDriver failure
        (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
        visible <-
            Except.lift
                (Declaration.resolveVisibleGlobalDriver 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.currentTheoryDriver
        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.objectAvailableDriver 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 failure 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 failure
        ( Map.Map
            Internal.Symbol
            (Typed.SourceGlobal ObjectId)
        , Map.Map ObjectId CoreType
        )
resolveSourceGlobals location internal direct =
    foldM resolve (Map.empty, Map.empty) symbols
  where
    carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal)
    symbols =
        Set.toAscList
            ( Set.delete carrier
                (directSymbols direct)
                `Set.difference` fixedInductiveSymbols
            )

    resolve (resolved, types) symbol = do
        let keys = semanticKeys symbol
        when (null keys)
            (Except.throwError
                (ExactInductiveGlobalNotVisible location symbol))
        matches <-
            catMaybes
                <$> traverse
                    (Except.lift
                        . Declaration.resolveVisibleGlobalContentDriver)
                    keys
        case matches of
            [] ->
                Except.throwError
                    (ExactInductiveGlobalNotVisible location symbol)
            [match] -> do
                (source, sourceTypes) <-
                    Except.liftEither
                        (prepareSourceGlobal location match)
                pure
                    ( Map.insert symbol source resolved
                    , Map.union sourceTypes types
                    )
            _ ->
                Except.throwError
                    (ExactInductiveGlobalAmbiguous location symbol)

prepareSourceGlobal
    :: Location
    -> ( SemanticGlobalTarget
       , ObjectContent
       , Map.Map ObjectId CoreType
       )
    -> Either
        ExactInductiveError
        (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
prepareSourceGlobal location (target, content, dependencies) = do
    body <-
        case target of
            GlobalReference _identity ->
                Right Nothing
            TransparentExpansion _identity ->
                case content of
                    TransparentObjectContent _theory _coreType canonical ->
                        Just
                            <$> first
                                (ExactInductiveGlobalContentInvalid location)
                                (checkCanonicalCore
                                    (`Map.lookup` dependencies)
                                    canonical)
                    _ ->
                        impossible
                            "validated transparent expansion has opaque content"
    let identity = semanticGlobalTargetObject target
        types =
            Map.insert
                identity
                (objectContentType content)
                dependencies
    pure (Typed.SourceGlobal identity body, types)

resolveGuard
    :: Location
    -> FrozenCheckedCore ObjectId
    -> Prepare failure SemanticFactOccurrenceFingerprint
resolveGuard location target = do
    matches <-
        Except.lift
            (Declaration.resolveVisibleFactTargetsDriver 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

fixedInductiveSymbols :: Set.Set Internal.Symbol
fixedInductiveSymbols =
    Set.fromList
        [ Internal.SymbolMixfix ConsSymbol
        , Internal.SymbolMixfix PairSymbol
        , Internal.SymbolMixfix (unarySymbol "pow")
        , Internal.SymbolMixfix (unarySymbol "cumul")
        , Internal.SymbolPredicate
            (Internal.PredicateRelation Raw.ElementSymbol)
        , Internal.SymbolPredicate
            (Internal.PredicateRelation Raw.EqSymbol)
        , Internal.SymbolPredicate
            (Internal.PredicateRelation Raw.NeqSymbol)
        , Internal.SymbolPredicate
            (Internal.PredicateRelation Raw.SubseteqSymbol)
        ]
  where
    unarySymbol command =
        Raw.MixfixItem
            (Raw.TokenCons (Raw.Command command)
                (Raw.TokenCons Raw.InvisibleBraceL
                    (Raw.HoleCons
                        (Raw.TokenCons Raw.InvisibleBraceR Raw.End))))
            (Raw.Marker command)
            Raw.NonAssoc

semanticKeys :: Internal.Symbol -> [SemanticGlobalKey]
semanticKeys = \case
    Internal.SymbolMixfix symbol ->
        [SemanticExpressionFunction (Raw.mixfixPattern symbol)]
    Internal.SymbolFun item ->
        let patterns = Raw.lexicalItemSgPlPattern item
        in [SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)]
    Internal.SymbolPredicate predicate ->
        case predicate of
            Internal.PredicateAdj item ->
                [ SemanticLeftAdjective (Raw.lexicalItemPattern item)
                , SemanticRightAdjective (Raw.lexicalItemPattern item)
                ]
            Internal.PredicateVerb item ->
                let patterns = Raw.lexicalItemSgPlPattern item
                in [SemanticVerb (Raw.sg patterns) (Raw.pl patterns)]
            Internal.PredicateNoun item ->
                let patterns = Raw.lexicalItemSgPlPattern item
                in [SemanticNoun (Raw.sg patterns) (Raw.pl patterns)]
            Internal.PredicateRelation relation ->
                [ SemanticRelation
                    (Raw.relationSymbolToken relation)
                    (Raw.relationSymbolParameterArity relation)
                ]
            Internal.PredicateSymbol{} -> []
            Internal.PredicateNounStruct{} -> []
    Internal.SymbolInteger{} -> []

commitPreparedExactInductive
    :: PreparedExactInductive
    -> Declaration.ModuleDriver failure
        ((), Declaration.CommittedDeclarationBatch)
commitPreparedExactInductive
        (PreparedExactInductive
            _location key identity asserted alias syntax typed guards) =
    Declaration.commitCompiledDeclaration syntax do
        traverse_ Declaration.addDeclarationObject asserted
        Declaration.stageSemanticGlobalBinding
            key
            (GlobalReference identity)
        let facts = Typed.typedInductiveFacts typed
            candidateInputs =
                fmap
                    (\fact ->
                        ( embedClosedCore []
                            (Typed.typedInductiveFactTarget fact)
                        , SearchEligible
                        , [markerAlias
                            (Typed.typedInductiveFactMarker fact)]
                        ))
                    facts
        (definitionCandidate, factCandidates) <-
            Declaration.reserveDefinitionEquationCandidateBatch
                identity
                alias
                candidateInputs
        Declaration.authorizeCompiledDeclaration do
            Declaration.authorizeDefinitionEquationCandidate
                identity
                definitionCandidate
            sequence_
                (NonEmpty.zipWith
                    authorizeFact
                    factCandidates
                    facts)
  where
    authorizeFact candidate fact =
        Declaration.authorizeKernelConstructionCandidate
            (GuardedFoundationRule
                (Typed.typedInductiveFactRule fact))
            candidate do
                traverse_ Declaration.useAuthorizedFact guards
                pure (Typed.typedInductiveFactDerivation fact)

    markerAlias (Raw.Marker name) =
        semanticName name

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))
        putCacheBytes
            (encodeKernelRuleTag
                (Typed.typedInductiveFactRule 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 = \case
    Internal.TermVar variable -> locate variable
    Internal.TermSymbol location _symbol _arguments -> location
    Internal.TermSymbolStruct _symbol expression ->
        maybe Nowhere termLocation expression
    Internal.Apply function _arguments -> termLocation function
    Internal.TermSep variable _bound _predicate -> locate variable
    Internal.ReplacePred value _domain _bound _predicate -> locate value
    Internal.ReplaceFun ((variable, _domain) :| _remaining) _value _condition ->
        locate variable
    Internal.Connected _connective left _right -> termLocation left
    Internal.Lambda{} -> Nowhere
    Internal.Quantified{} -> Nowhere
    Internal.PropositionalConstant{} -> Nowhere
    Internal.Not location _term -> location