Move fact selection into transition inventory

1 files changed, 36 insertions, 390 deletions

diff --git a/source/Checking/Backend/Problem.hs b/source/Checking/Backend/Problem.hs
index 7ed9464..f583bcd 100644
--- a/source/Checking/Backend/Problem.hs
+++ b/source/Checking/Backend/Problem.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
--- | Pure selection and complete-problem FOF/TH0 classification.
+-- | Complete-problem FOF/TH0 classification and construction.
 module Checking.Backend.Problem
     ( SupportedProposition
     , supportedProposition
@@ -15,20 +15,11 @@ module Checking.Backend.Problem
     , BackendFofExclusion(..)
     , BackendClassificationError(..)
     , classifySupportedProposition
-    , TypedBackendFactInput
-    , typedBackendFactInput
-    , preparedTypedBackendFactInput
     , TypedBackendFact
+    , typedBackendFact
     , typedBackendFactReference
-    , typedBackendFactAliases
-    , typedBackendFactOrigin
     , typedBackendFactProposition
     , typedBackendFactCapability
-    , TypedFactInventory
-    , prepareTypedFactInventory
-    , typedFactInventoryOrder
-    , typedFactInventoryFofOrder
-    , TypedFactInventoryError(..)
     , LocalPremiseOrdinal
     , localPremiseOrdinal
     , localPremiseOrdinalValue
@@ -45,7 +36,7 @@ module Checking.Backend.Problem
     , typedProblemAuxiliaryTag
     , typedProblemAuxiliaryProposition
     , typedProblemAuxiliaryCapability
-    , GlobalPremisePolicy(..)
+    , GlobalPremiseMode(..)
     , LocalPremisePolicy(..)
     , TypedProblemRoute(..)
     , TypedProblem
@@ -63,9 +54,8 @@ module Checking.Backend.Problem
 import Base
 import Checking.Core
 import Checking.Foundation
-import Syntax.Internal (Marker)
 
-import Control.Monad (foldM, unless, when)
+import Control.Monad (foldM, unless)
 import Data.Bifunctor (first)
 import Data.List qualified as List
 import Data.Map.Strict qualified as Map
@@ -472,325 +462,54 @@ canonicalGlobals = \case
         canonicalGlobals body
 
 
-data TypedBackendFactInput ref origin global =
-    UnclassifiedTypedBackendFactInput
-        !ref
-        !(NonEmpty Marker)
-        !origin
-        !(FrozenCheckedCore global)
-    | PreparedTypedBackendFactInput
+data TypedBackendFact ref global =
+    TypedBackendFact
         !ref
-        !(NonEmpty Marker)
-        !origin
         !(SupportedProposition Void global)
         !(FofCapability
             (CheckedFofProjection Void global))
+    deriving stock (Eq)
 
-typedBackendFactInput
-    :: ref
-    -> NonEmpty Marker
-    -> origin
-    -> FrozenCheckedCore global
-    -> TypedBackendFactInput ref origin global
-typedBackendFactInput =
-    UnclassifiedTypedBackendFactInput
-
-preparedTypedBackendFactInput
+typedBackendFact
     :: ref
-    -> NonEmpty Marker
-    -> origin
     -> SupportedProposition Void global
     -> FofCapability
         (CheckedFofProjection Void global)
-    -> TypedBackendFactInput ref origin global
-preparedTypedBackendFactInput =
-    PreparedTypedBackendFactInput
-
-data TypedBackendFact ref origin global =
+    -> TypedBackendFact ref global
+typedBackendFact =
     TypedBackendFact
-        !ref
-        !(NonEmpty Marker)
-        !origin
-        !(SupportedProposition Void global)
-        !(FofCapability
-            (CheckedFofProjection Void global))
-    deriving stock (Eq)
 
 typedBackendFactReference
-    :: TypedBackendFact ref origin global
+    :: TypedBackendFact ref global
     -> ref
 typedBackendFactReference
         (TypedBackendFact
             reference
-            _aliases
-            _origin
             _proposition
             _capability) =
     reference
 
-typedBackendFactAliases
-    :: TypedBackendFact ref origin global
-    -> NonEmpty Marker
-typedBackendFactAliases
-        (TypedBackendFact
-            _reference
-            aliases
-            _origin
-            _proposition
-            _capability) =
-    aliases
-
-typedBackendFactOrigin
-    :: TypedBackendFact ref origin global
-    -> origin
-typedBackendFactOrigin
-        (TypedBackendFact
-            _reference
-            _aliases
-            factOrigin
-            _proposition
-            _capability) =
-    factOrigin
-
 typedBackendFactProposition
-    :: TypedBackendFact ref origin global
+    :: TypedBackendFact ref global
     -> SupportedProposition Void global
 typedBackendFactProposition
         (TypedBackendFact
             _reference
-            _aliases
-            _origin
             proposition
             _capability) =
     proposition
 
 typedBackendFactCapability
-    :: TypedBackendFact ref origin global
+    :: TypedBackendFact ref global
     -> FofCapability
         (CheckedFofProjection Void global)
 typedBackendFactCapability
         (TypedBackendFact
             _reference
-            _aliases
-            _origin
             _proposition
             capability) =
     capability
 
-data TypedFactInventory ref origin global =
-    TypedFactInventory
-        !(Map ref (TypedBackendFact ref origin global))
-        !(Map Marker ref)
-        !(Vector ref)
-        !(Vector ref)
-
-data TypedFactInventoryError ref origin global
-    = TypedFactStatementIsNotProposition !ref !CoreType
-    | TypedFactClassificationFailed
-        !ref
-        !(BackendClassificationError global)
-    | TypedFactPreparedProjectionMismatch !ref
-    | DuplicateTypedFactReference !ref
-    | TypedFactAliasConflict
-        !Marker
-        !ref
-        !origin
-        !ref
-        !origin
-    deriving stock (Show, Eq)
-
-prepareTypedFactInventory
-    :: (Ord ref, Ord global)
-    => (global -> Maybe CoreType)
-    -> [TypedBackendFactInput ref origin global]
-    -> Either
-        (TypedFactInventoryError ref origin global)
-        (TypedFactInventory ref origin global)
-prepareTypedFactInventory globalType inputs = do
-    (byReference, byAlias, reversedOrder, reversedFofOrder) <-
-        foldM
-            insertInput
-            (Map.empty, Map.empty, [], [])
-            inputs
-    pure
-        (TypedFactInventory
-            byReference
-            byAlias
-            (Vector.fromList
-                (reverse reversedOrder))
-            (Vector.fromList
-                (reverse reversedFofOrder)))
-  where
-    insertInput
-            (byReference, byAlias, reversedOrder, reversedFofOrder)
-            (UnclassifiedTypedBackendFactInput
-                reference
-                aliases
-                factOrigin
-                statement) = do
-        when
-            (Map.member reference byReference)
-            (Left
-                (DuplicateTypedFactReference
-                    reference))
-        unless
-            (frozenCoreType statement == TyProp)
-            (Left
-                (TypedFactStatementIsNotProposition
-                    reference
-                    (frozenCoreType statement)))
-        scoped <-
-            pure (embedClosedCore [] statement)
-        proposition <-
-            first
-                (const
-                    (TypedFactStatementIsNotProposition
-                        reference
-                        (frozenCoreType statement)))
-                (supportedProposition
-                    Vector.empty
-                    scoped)
-        capability <-
-            first
-                (TypedFactClassificationFailed
-                    reference)
-                (classifySupportedProposition
-                    globalType
-                    proposition)
-        byAlias' <-
-            foldM
-                (insertAlias
-                    reference
-                    factOrigin
-                    byReference)
-                byAlias
-                aliases
-        let fact =
-                TypedBackendFact
-                    reference
-                    aliases
-                    factOrigin
-                    proposition
-                    capability
-            reversedFofOrder' =
-                case capability of
-                    FofProjectable{} ->
-                        reference : reversedFofOrder
-                    RequiresTh0{} ->
-                        reversedFofOrder
-        pure
-            ( Map.insert reference fact byReference
-            , byAlias'
-            , reference : reversedOrder
-            , reversedFofOrder'
-            )
-    insertInput
-            (byReference, byAlias, reversedOrder, reversedFofOrder)
-            (PreparedTypedBackendFactInput
-                reference
-                aliases
-                factOrigin
-                proposition
-                capability) = do
-        when
-            (Map.member reference byReference)
-            (Left
-                (DuplicateTypedFactReference
-                    reference))
-        case capability of
-            FofProjectable projection ->
-                unless
-                    (checkedFofProjectionProposition
-                        projection
-                        == proposition)
-                    (Left
-                        (TypedFactPreparedProjectionMismatch
-                            reference))
-            RequiresTh0{} ->
-                pure ()
-        byAlias' <-
-            foldM
-                (insertAlias
-                    reference
-                    factOrigin
-                    byReference)
-                byAlias
-                aliases
-        let fact =
-                TypedBackendFact
-                    reference
-                    aliases
-                    factOrigin
-                    proposition
-                    capability
-            reversedFofOrder' =
-                case capability of
-                    FofProjectable{} ->
-                        reference : reversedFofOrder
-                    RequiresTh0{} ->
-                        reversedFofOrder
-        pure
-            ( Map.insert reference fact byReference
-            , byAlias'
-            , reference : reversedOrder
-            , reversedFofOrder'
-            )
-
-    insertAlias
-            reference
-            factOrigin
-            byReference
-            byAlias
-            alias =
-        case Map.lookup alias byAlias of
-            Nothing ->
-                Right
-                    (Map.insert
-                        alias
-                        reference
-                        byAlias)
-            Just previousReference ->
-                if previousReference == reference
-                    then
-                        Right byAlias
-                    else
-                        case Map.lookup previousReference byReference of
-                            Nothing ->
-                                Left
-                                    (DuplicateTypedFactReference
-                                        previousReference)
-                            Just previous ->
-                                Left
-                                    (TypedFactAliasConflict
-                                        alias
-                                        previousReference
-                                        (typedBackendFactOrigin
-                                            previous)
-                                        reference
-                                        factOrigin)
-
-typedFactInventoryOrder
-    :: TypedFactInventory ref origin global
-    -> Vector ref
-typedFactInventoryOrder
-        (TypedFactInventory
-            _byReference
-            _byAlias
-            order
-            _fofOrder) =
-    order
-
-typedFactInventoryFofOrder
-    :: TypedFactInventory ref origin global
-    -> Vector ref
-typedFactInventoryFofOrder
-        (TypedFactInventory
-            _byReference
-            _byAlias
-            _order
-            fofOrder) =
-    fofOrder
-
 
 newtype LocalPremiseOrdinal =
     LocalPremiseOrdinal Natural
@@ -975,10 +694,10 @@ typedProblemAuxiliaryCapability
     capability
 
 
-data GlobalPremisePolicy
-    = ImplicitFofFacts
-    | ExplicitFacts !(NonEmpty Marker)
-    | NoGlobalFacts
+data GlobalPremiseMode
+    = ImplicitFofPremises
+    | ExplicitGlobalPremises
+    | NoGlobalPremises
     deriving stock (Show, Eq)
 
 data LocalPremisePolicy
@@ -995,21 +714,19 @@ data TypedProblem ref local origin global =
     TypedProblem
         !TypedProblemRoute
         !(SupportedProposition local global)
-        !(Vector (TypedBackendFact ref origin global))
+        !(Vector (TypedBackendFact ref global))
         !(Vector (TypedLocalPremise local origin global))
         !(Vector (TypedProblemAuxiliary global))
         !(Map global CoreType)
         !(Map local CoreType)
 
-data TypedProblemError ref local origin global
+data TypedProblemError local global
     = TypedProblemClaimClassificationFailed
         !(BackendClassificationError global)
-    | TypedProblemUnknownFactAlias !Marker
-    | TypedProblemFactReferenceMissing !ref
     | TypedProblemExplicitHigherOrderJustificationRequired
         !(NonEmpty BackendFofExclusion)
     | TypedProblemInvalidPolicyCombination
-        !GlobalPremisePolicy
+        !GlobalPremiseMode
         !LocalPremisePolicy
     | TypedProblemDuplicateLocalPremiseOrdinal
         !LocalPremiseOrdinal
@@ -1020,20 +737,20 @@ data TypedProblemError ref local origin global
     deriving stock (Show, Eq)
 
 planTypedProblem
-    :: (Ord ref, Ord local, Ord global)
+    :: (Ord local, Ord global)
     => (global -> Maybe CoreType)
-    -> TypedFactInventory ref origin global
+    -> Vector (TypedBackendFact ref global)
     -> SupportedProposition local global
     -> [TypedLocalPremise local origin global]
     -> [TypedFoundationAuxiliaryInput global]
-    -> GlobalPremisePolicy
+    -> GlobalPremiseMode
     -> LocalPremisePolicy
     -> Either
-        (TypedProblemError ref local origin global)
+        (TypedProblemError local global)
         (TypedProblem ref local origin global)
 planTypedProblem
         globalType
-        inventory
+        selectedFacts
         claim
         availableLocals
         auxiliaries
@@ -1050,10 +767,6 @@ planTypedProblem
             (classifySupportedProposition
                 globalType
                 claim)
-    selectedFacts <-
-        selectFacts
-            inventory
-            globalPolicy
     let selectedLocals =
             Vector.fromList
                 (List.sortOn
@@ -1072,7 +785,7 @@ planTypedProblem
                 [0..]
                 auxiliaries
     case globalPolicy of
-        ImplicitFofFacts ->
+        ImplicitFofPremises ->
             case implicitTh0Requirement
                     claimCapability
                     (typedProblemAuxiliaryCapability
@@ -1151,18 +864,18 @@ planTypedProblem
             capability
 
 validatePolicyCombination
-    :: GlobalPremisePolicy
+    :: GlobalPremiseMode
     -> LocalPremisePolicy
     -> Either
-        (TypedProblemError ref local origin global)
+        (TypedProblemError local global)
         ()
 validatePolicyCombination globalPolicy localPolicy =
     case (globalPolicy, localPolicy) of
-        (ImplicitFofFacts, FirstOrderLocals) ->
+        (ImplicitFofPremises, FirstOrderLocals) ->
             Right ()
-        (ExplicitFacts{}, FirstOrderLocals) ->
+        (ExplicitGlobalPremises, FirstOrderLocals) ->
             Right ()
-        (NoGlobalFacts, AllLocals) ->
+        (NoGlobalPremises, AllLocals) ->
             Right ()
         _ ->
             Left
@@ -1173,7 +886,7 @@ validatePolicyCombination globalPolicy localPolicy =
 validateLocalPremiseOrdinals
     :: [TypedLocalPremise local origin global]
     -> Either
-        (TypedProblemError ref local origin global)
+        (TypedProblemError local global)
         ()
 validateLocalPremiseOrdinals =
     void
@@ -1194,73 +907,6 @@ validateLocalPremiseOrdinals =
                                     seen))
             Set.empty
 
-selectFacts
-    :: Ord ref
-    => TypedFactInventory ref origin global
-    -> GlobalPremisePolicy
-    -> Either
-        (TypedProblemError ref local origin global)
-        (Vector (TypedBackendFact ref origin global))
-selectFacts
-        inventory@(TypedFactInventory
-            _byReference
-            byAlias
-            _order
-            fofOrder)
-        policy = do
-    references <-
-        case policy of
-            ImplicitFofFacts ->
-                Right (Vector.toList fofOrder)
-            ExplicitFacts aliases ->
-                stableUnique
-                    <$> traverse
-                        (\alias ->
-                            maybe
-                                (Left
-                                    (TypedProblemUnknownFactAlias
-                                        alias))
-                                Right
-                                (Map.lookup alias byAlias))
-                        (toList aliases)
-            NoGlobalFacts ->
-                Right []
-    Vector.fromList
-        <$> traverse
-            (\reference ->
-                maybe
-                    (Left
-                        (TypedProblemFactReferenceMissing
-                            reference))
-                    Right
-                    (lookupTypedFact reference inventory))
-            references
-  where
-    stableUnique =
-        reverse . snd
-            . foldl'
-                (\(seen, reversed) reference ->
-                    if reference `Set.member` seen
-                        then (seen, reversed)
-                        else
-                            ( Set.insert reference seen
-                            , reference : reversed
-                            ))
-                (Set.empty, [])
-
-lookupTypedFact
-    :: Ord ref
-    => ref
-    -> TypedFactInventory ref origin global
-    -> Maybe (TypedBackendFact ref origin global)
-lookupTypedFact reference
-        (TypedFactInventory
-            byReference
-            _byAlias
-            _order
-            _fofOrder) =
-    Map.lookup reference byReference
-
 isFofCapability :: FofCapability projection -> Bool
 isFofCapability = \case
     FofProjectable{} ->
@@ -1272,11 +918,11 @@ collectProblemGlobals
     :: Ord global
     => (global -> Maybe CoreType)
     -> SupportedProposition local global
-    -> Vector (TypedBackendFact ref origin global)
+    -> Vector (TypedBackendFact ref global)
     -> Vector (TypedLocalPremise local origin global)
     -> [TypedProblemAuxiliary global]
     -> Either
-        (TypedProblemError ref local origin global)
+        (TypedProblemError local global)
         (Map global CoreType)
 collectProblemGlobals
         globalType
@@ -1322,7 +968,7 @@ collectProblemLocals
     => SupportedProposition local global
     -> Vector (TypedLocalPremise local origin global)
     -> Either
-        (TypedProblemError ref local origin global)
+        (TypedProblemError local global)
         (Map local CoreType)
 collectProblemLocals claim locals =
     foldM
@@ -1387,7 +1033,7 @@ typedProblemClaim
 
 typedProblemGlobalPremises
     :: TypedProblem ref local origin global
-    -> Vector (TypedBackendFact ref origin global)
+    -> Vector (TypedBackendFact ref global)
 typedProblemGlobalPremises
         (TypedProblem
             _route