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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
|
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}
-- | Semantic classification shared by the exact source compilers.
module Felix.Checking.Exact.Vocabulary
( FixedSemanticMeaning(..)
, fixedSemanticMeaning
, lowerFixedEqualityPredicate
, ExactSymbolClass(..)
, classifyExactSymbol
, FixedSetTermDispatch(..)
, dispatchFixedSetTerm
) where
import Base hiding (Empty)
import Felix.Checking.Core
import Felix.Checking.Semantic
import Felix.Syntax.Abstract qualified as Raw
import Felix.Syntax.Internal qualified as Internal
import Felix.Syntax.Lexicon qualified as Lexicon
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
data FixedSemanticMeaning
= FixedEquality
| FixedDisequality
| FixedIntrinsic !CoreIntrinsicTag
| FixedNegatedIntrinsic !CoreIntrinsicTag
deriving stock (Show, Eq)
fixedSemanticMeaning
:: SemanticGlobalKey
-> Maybe FixedSemanticMeaning
fixedSemanticMeaning key =
Map.lookup key fixedSemanticVocabulary
-- This inventory owns every exact source form that bypasses global lookup.
fixedSemanticVocabulary
:: Map.Map SemanticGlobalKey FixedSemanticMeaning
fixedSemanticVocabulary =
Map.fromList
[ ( relationKey Raw.EqSymbol
, FixedEquality
)
, ( SemanticRightAdjective
(Raw.lexicalItemPattern
Lexicon.builtinEqualityRightAdjective)
, FixedEquality
)
, ( verbKey Lexicon.builtinEqualityVerb
, FixedEquality
)
, ( relationKey Raw.ElementSymbol
, FixedIntrinsic Member
)
, ( relationKey Raw.NotElementSymbol
, FixedNegatedIntrinsic Member
)
, ( relationKey Raw.NeqSymbol
, FixedDisequality
)
, ( nounKey Lexicon.builtinElementNoun
, FixedIntrinsic Member
)
, ( expressionKey
(Raw.TokenCons (Raw.Command "emptyset") Raw.End)
, FixedIntrinsic Empty
)
, ( expressionKey (Raw.mixfixPattern Raw.UnionsSymbol)
, FixedIntrinsic FamilyUnion
)
, ( expressionKey (unaryCommandPattern "pow")
, FixedIntrinsic PowerSet
)
, ( expressionKey (unaryCommandPattern "cumul")
, FixedIntrinsic UnivOf
)
, ( expressionKey (Raw.mixfixPattern Raw.UpairSymbol)
, FixedIntrinsic PairSet
)
]
where
relationKey relation =
SemanticRelation
(Raw.relationSymbolToken relation)
(Raw.relationSymbolParameterArity relation)
nounKey item =
let patterns = Raw.lexicalItemSgPlPattern item
in SemanticNoun (Raw.sg patterns) (Raw.pl patterns)
verbKey item =
let patterns = Raw.lexicalItemSgPlPattern item
in SemanticVerb (Raw.sg patterns) (Raw.pl patterns)
expressionKey = SemanticExpressionFunction
-- | Lower the fixed proposition meanings shared by raw exact elaboration and
-- the reusable internal-formula path. Membership deliberately retains its
-- carrier-aware source lowering and is not handled here.
lowerFixedEqualityPredicate
:: FixedSemanticMeaning
-> [CanonicalTerm global]
-> Maybe (CanonicalTerm global)
lowerFixedEqualityPredicate meaning arguments =
case (meaning, arguments) of
(FixedEquality, [left, right]) ->
Just (CEq TySet left right)
(FixedDisequality, [left, right]) ->
Just (CImp (CEq TySet left right) CFalsum)
_ ->
Nothing
unaryCommandPattern :: Text -> Raw.Pattern
unaryCommandPattern command =
Raw.TokenCons (Raw.Command command)
(Raw.TokenCons Raw.InvisibleBraceL
(Raw.HoleCons
(Raw.TokenCons Raw.InvisibleBraceR Raw.End)))
data ExactSymbolClass
= ExactClosedLiteral
| ExactFixedPrimitive !FixedSemanticMeaning
| ExactSourceGlobal !(NonEmpty SemanticGlobalKey)
| ExactUnsupportedSymbol
deriving stock (Show, Eq)
classifyExactSymbol :: Internal.Symbol -> ExactSymbolClass
classifyExactSymbol symbol =
case symbol of
Internal.SymbolInteger{} ->
ExactClosedLiteral
_ ->
case NonEmpty.nonEmpty (semanticKeys symbol) of
Nothing ->
ExactUnsupportedSymbol
Just keys ->
case firstFixed keys of
Just meaning ->
ExactFixedPrimitive meaning
Nothing ->
ExactSourceGlobal keys
where
firstFixed =
foldr
(\key found -> fixedSemanticMeaning key <|> found)
Nothing
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{} -> []
-- | Result of interpreting a symbol already classified by the fixed exact
-- vocabulary as a set-valued term.
data FixedSetTermDispatch global
= NotFixedSetTerm
| LoweredFixedSetTerm !(CanonicalTerm global)
| RejectedFixedSetTerm
deriving stock (Show, Eq)
-- | Interpret every fixed symbol that can occur in the reusable internal-term
-- lowering. Fixed relations are handled by formula lowering.
dispatchFixedSetTerm
:: Internal.Symbol
-> [CanonicalTerm global]
-> FixedSetTermDispatch global
dispatchFixedSetTerm symbol arguments =
case classifyExactSymbol symbol of
ExactFixedPrimitive meaning ->
case meaning of
FixedIntrinsic intrinsic ->
applyIntrinsic
(CIntrinsic intrinsic)
(coreIntrinsicType intrinsic)
arguments
FixedNegatedIntrinsic _intrinsic ->
RejectedFixedSetTerm
FixedEquality ->
RejectedFixedSetTerm
FixedDisequality ->
RejectedFixedSetTerm
_ ->
NotFixedSetTerm
where
applyIntrinsic term coreType remaining =
case (coreType, remaining) of
(TySet, []) ->
LoweredFixedSetTerm term
(TyArrow TySet resultType, argument : rest) ->
applyIntrinsic
(CApp term argument)
resultType
rest
_ ->
RejectedFixedSetTerm
|
