{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | Exact preparation and atomic publication of direct set inductives. module Felix.Checking.Exact.Inductive ( PreparedExactInductive , preparedExactInductiveCarrierId , preparedExactInductiveCarrierType , preparedExactInductiveCarrierBody , preparedExactInductiveGuardTargets , preparedExactInductiveFacts , prepareExactInductive , CheckedExactInductiveAuthorization , lowerPreparedExactInductive , authorizeCheckedExactInductive , ExactInductiveError(..) , exactInductiveErrorLocation , renderExactInductiveError ) where import Base hiding (Empty) import Felix.Checking.Authority import Felix.Checking.Core import Felix.Checking.Declaration qualified as Declaration import Felix.Checking.Exact.Global qualified as ExactGlobal import Felix.Checking.Exact.Vocabulary import Felix.Checking.Foundation import Felix.Checking.Identity import Felix.Checking.Semantic import Felix.Checking.Typed.Inductive qualified as Typed import Felix.Cache.Codec import Felix.Meaning qualified as Meaning import Felix.Report.Location import Felix.Syntax.Abstract qualified as Raw import Felix.Syntax.Interface import Felix.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] ![(Location, Declaration.PreparedVampireObligation Void ())] 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 | ExactInductiveRecursiveCarrierWrongArguments !Location | ExactInductiveRecursiveCarrierOutsideMembership !Location | ExactInductiveUnsupportedRecursiveCarrierContext !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 ExactInductiveRecursiveCarrierWrongArguments location -> location ExactInductiveRecursiveCarrierOutsideMembership location -> location ExactInductiveUnsupportedRecursiveCarrierContext 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" ExactInductiveRecursiveCarrierWrongArguments{} -> "the inductive carrier occurs with arguments other than its declared parameters" ExactInductiveRecursiveCarrierOutsideMembership{} -> "an inductive carrier occurrence must be in the set operand of a membership premise" ExactInductiveUnsupportedRecursiveCarrierContext{} -> "this recursive carrier context is outside the supported first-order set-term fragment" 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)) | otherwise -> do context <- first recursiveCarrierContextError (Typed.prepareRecursiveCarrierContext carrier parameters recursiveCarrier) Right (Typed.DirectRecursiveCondition recursiveTerm context) _ -> Left (ExactInductiveRecursiveCarrierOutsideMembership (termLocation formula)) recursiveCarrierContextError :: Typed.RecursiveCarrierContextError -> ExactInductiveError recursiveCarrierContextError = \case Typed.RecursiveCarrierWrongArguments location -> ExactInductiveRecursiveCarrierWrongArguments location Typed.RecursiveCarrierUnsupportedContext location -> ExactInductiveUnsupportedRecursiveCarrierContext location 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 context -> Internal.mentionedSymbols term <> Typed.recursiveCarrierContextSymbols context 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 monotonicities = Vector.toList (Typed.typedInductiveMonotonicities typed) objects = maybeToList asserted definition <- Declaration.prepareDefinitionEquationSpecLowering objects identity alias preparedMonotonicities <- traverse (\monotonicity -> Except.runExceptT do let factLocation = Typed.typedInductiveMonotonicityLocation monotonicity target = Typed.typedInductiveMonotonicityTarget monotonicity spec <- Except.lift (Declaration.prepareFrozenCandidateSpecLowering objects target SearchIneligible []) >>= Except.liftEither obligation <- Except.lift (Declaration.prepareScopedVampireObligationLowering Vector.empty (embedClosedCore [] target) [] [] Declaration.VampireImplicitPremises) >>= either (Except.throwError . Declaration.ProofObligationFailedAt factLocation . Declaration.CurrentCandidateVampirePreparationFailed) pure pure ( Declaration.checkedCandidate spec (Declaration.checkedSourceProofPlanning [ Declaration.checkedPlannedVampireRequest factLocation obligation ] []) , (factLocation, obligation) )) monotonicities preparedCandidates <- traverse (\fact -> do prepared <- Declaration.prepareCandidateSpecLowering objects (embedClosedCore [] (Typed.typedInductiveFactTarget fact)) SearchEligible [markerAlias (Typed.typedInductiveFactMarker fact)] let descriptor = GuardedFoundationRules (guardedRuleSet (Typed.typedInductiveFactRules fact)) planning | null monotonicities = Declaration.checkedKernelPlanning descriptor guards | otherwise = Declaration.checkedKernelPlanningWithStaged descriptor guards (if Typed.typedInductiveFactRequiresMonotonicities fact then [ Declaration.plannedEarlierCandidate 1 index | (index, _target) <- zip [0 ..] monotonicities ] else []) pure (fmap (\spec -> Declaration.checkedCandidate spec planning) prepared)) facts pure do definitionSpec <- definition monotonicityCandidates <- sequence preparedMonotonicities factCandidates <- sequence preparedCandidates let stages | null monotonicityCandidates = [ Declaration.checkedCandidate definitionSpec (Declaration.checkedDefinitionEquationPlanning identity) :| toList factCandidates ] | otherwise = [ Declaration.checkedCandidate definitionSpec (Declaration.checkedDefinitionEquationPlanning identity) :| [] , NonEmpty.fromList (fst <$> monotonicityCandidates) , factCandidates ] pure (Declaration.checkedCompiledDeclaration syntax objects [] [semanticGlobalBinding key (GlobalReference identity)] [] stages (CheckedExactInductiveAuthorization identity typed guards (snd <$> monotonicityCandidates))) where markerAlias (Raw.Marker name) = semanticName name authorizeCheckedExactInductive :: CheckedExactInductiveAuthorization -> [NonEmpty Declaration.ReservedCandidate] -> Declaration.Declaration () authorizeCheckedExactInductive (CheckedExactInductiveAuthorization identity typed guards monotonicityObligations) = \case [definitionCandidate :| candidates] -> do unless (null monotonicityObligations) (Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch 3 1)) 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)) [ definitionCandidate :| [] , monotonicityCandidates , factCandidates ] | NonEmpty.length monotonicityCandidates == length monotonicityObligations , NonEmpty.length factCandidates == NonEmpty.length (Typed.typedInductiveFacts typed) -> do obligations <- maybe (Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch 1 0)) pure (NonEmpty.nonEmpty monotonicityObligations) Declaration.authorizeDefinitionEquationCandidate identity definitionCandidate Declaration.authorizeVampireCandidateBatch (NonEmpty.zipWith (\candidate (factLocation, obligation) -> (factLocation, candidate, pure obligation)) monotonicityCandidates obligations) sequence_ (NonEmpty.zipWith (\candidate fact -> authorizeFact (if Typed.typedInductiveFactRequiresMonotonicities fact then NonEmpty.toList monotonicityCandidates else []) candidate fact) factCandidates (Typed.typedInductiveFacts typed)) stages -> Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch (if null monotonicityObligations then 1 else 3) (length stages)) where authorizeFact monotonicityCandidates candidate fact = Declaration.authorizeKernelConstructionCandidate (GuardedFoundationRules (guardedRuleSet (Typed.typedInductiveFactRules fact))) candidate do traverse_ Declaration.useAuthorizedFact guards traverse_ Declaration.useStagedCandidate monotonicityCandidates 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)) putCacheList putFrozenTerm (Vector.toList (Typed.typedInductiveContextInventory typed)) putCacheList (putFrozenTerm . Typed.typedInductiveMonotonicityTarget) (Vector.toList (Typed.typedInductiveMonotonicities typed)) putCacheText (semanticNameText alias) putCacheList putFact (toList (Typed.typedInductiveFacts typed)) where putFrozenTerm = putCanonicalTermCache putObjectIdCache . frozenCoreTerm 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