diff options
Diffstat (limited to 'source/Checking/Exact/Vocabulary.hs')
| -rw-r--r-- | source/Checking/Exact/Vocabulary.hs | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Checking/Exact/Vocabulary.hs index 5701f64..b1310f2 100644 --- a/source/Checking/Exact/Vocabulary.hs +++ b/source/Checking/Exact/Vocabulary.hs @@ -5,6 +5,7 @@ module Checking.Exact.Vocabulary ( FixedSemanticMeaning(..) , fixedSemanticMeaning + , lowerFixedEqualityPredicate , ExactSymbolClass(..) , classifyExactSymbol , FixedSetTermDispatch(..) @@ -43,6 +44,14 @@ fixedSemanticVocabulary = [ ( relationKey Raw.EqSymbol , FixedEquality ) + , ( SemanticRightAdjective + (Raw.lexicalItemPattern + Lexicon.builtinEqualityRightAdjective) + , FixedEquality + ) + , ( verbKey Lexicon.builtinEqualityVerb + , FixedEquality + ) , ( relationKey Raw.ElementSymbol , FixedIntrinsic Member ) @@ -80,8 +89,27 @@ fixedSemanticVocabulary = 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) |