diff options
Diffstat (limited to 'source/Checking/Typed/Inductive.hs')
| -rw-r--r-- | source/Checking/Typed/Inductive.hs | 36 |
1 files changed, 35 insertions, 1 deletions
diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs index 7a895c6..02e68ea 100644 --- a/source/Checking/Typed/Inductive.hs +++ b/source/Checking/Typed/Inductive.hs @@ -3708,7 +3708,7 @@ lowerFormulaWith allowQuantified resolveGlobal environment = \case <*> lowerFormulaWith allowQuantified resolveGlobal environment right Atomic _location predicate arguments -> - lowerApplication + lowerPredicateApplication resolveGlobal environment (SymbolPredicate predicate) @@ -3783,6 +3783,40 @@ lowerApplication resolveGlobal environment symbol arguments = do resolveGlobal environment) arguments + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerPredicateApplication + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> Symbol + -> [Expr] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerPredicateApplication resolveGlobal environment symbol arguments = do + arguments' <- + traverse + (lowerTerm + resolveGlobal + environment) + arguments + case classifyExactSymbol symbol of + ExactFixedPrimitive meaning -> + maybe + (lowerApplicationTerms resolveGlobal symbol arguments') + Right + (lowerFixedEqualityPredicate meaning arguments') + _ -> + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerApplicationTerms + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Symbol + -> [CanonicalTerm (InductiveGlobal global)] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerApplicationTerms resolveGlobal symbol arguments' = case dispatchFixedSetTerm symbol arguments' of LoweredFixedSetTerm term -> pure term |