1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}
-- | Exact resolution of source symbols to checked semantic globals.
module Checking.Exact.Global
( ExactGlobalResolutionError(..)
, resolveExactSourceGlobals
) where
import Base
import Checking.Core
import Checking.Declaration qualified as Declaration
import Checking.Exact.Vocabulary
import Checking.Identity
import Checking.Semantic
import Checking.Typed.Inductive qualified as Typed
import Syntax.Internal qualified as Internal
import Control.Monad (foldM)
import Control.Monad.Except
( liftEither
, runExceptT
, throwError
)
import Control.Monad.Trans.Class (lift)
import Data.Bifunctor (first)
import Data.Map.Strict qualified as Map
import Data.Maybe (catMaybes)
import Data.Set qualified as Set
data ExactGlobalResolutionError
= ExactGlobalNotVisible !Internal.Symbol
| ExactGlobalAmbiguous !Internal.Symbol
| ExactGlobalUnsupported !Internal.Symbol
| ExactGlobalContextualUnsupported !Internal.Symbol
| ExactGlobalContentInvalid !CoreCheckError
deriving stock (Show, Eq)
resolveExactSourceGlobals
:: Set.Set Internal.Symbol
-> Declaration.LoweringDriver
(Either
ExactGlobalResolutionError
( Map.Map
Internal.Symbol
(Typed.SourceGlobal ObjectId)
, Map.Map ObjectId CoreType
))
resolveExactSourceGlobals symbols =
runExceptT
(foldM resolve (Map.empty, Map.empty)
(Set.toAscList symbols))
where
resolve (resolved, types) symbol =
case classifyExactSymbol symbol of
ExactClosedLiteral ->
pure (resolved, types)
ExactFixedPrimitive _meaning ->
pure (resolved, types)
ExactUnsupportedSymbol ->
throwError (ExactGlobalUnsupported symbol)
ExactSourceGlobal keys -> do
matches <-
catMaybes
<$> traverse
(lift
. Declaration.resolveVisibleGlobalContentLowering)
(toList keys)
case matches of
[] ->
throwError (ExactGlobalNotVisible symbol)
[match] -> do
(source, sourceTypes) <-
liftEither (prepareSourceGlobal symbol match)
pure
( Map.insert symbol source resolved
, Map.union sourceTypes types
)
_ ->
throwError (ExactGlobalAmbiguous symbol)
prepareSourceGlobal
:: Internal.Symbol
-> ( SemanticGlobalTarget
, ObjectContent
, Map.Map ObjectId CoreType
)
-> Either
ExactGlobalResolutionError
(Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
prepareSourceGlobal symbol (target, content, dependencies) = do
body <-
case target of
GlobalReference _identity ->
Right Nothing
TransparentExpansion _identity ->
case content of
TransparentObjectContent _theory _coreType canonical ->
Just
<$> first ExactGlobalContentInvalid
(checkCanonicalCore
(`Map.lookup` dependencies)
canonical)
_ ->
impossible
"validated transparent expansion has opaque content"
ContextualTransparentExpansion _identity _requirements ->
Left (ExactGlobalContextualUnsupported symbol)
let identity = semanticGlobalTargetObject target
types =
Map.insert
identity
(objectContentType content)
dependencies
pure (Typed.SourceGlobal identity body, types)
|
