summaryrefslogtreecommitdiff
path: root/source/Checking/Typed
diff options
context:
space:
mode:
Diffstat (limited to 'source/Checking/Typed')
-rw-r--r--source/Checking/Typed/Inductive.hs944
1 files changed, 829 insertions, 115 deletions
diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs
index 7a895c6..eb6c0f7 100644
--- a/source/Checking/Typed/Inductive.hs
+++ b/source/Checking/Typed/Inductive.hs
@@ -8,16 +8,27 @@ module Checking.Typed.Inductive
( DirectInductive(..)
, DirectInductiveClause(..)
, DirectInductiveCondition(..)
+ , RecursiveCarrierContext
+ , RecursiveCarrierContextError(..)
+ , prepareRecursiveCarrierContext
+ , directRecursiveCarrierContext
+ , recursiveCarrierContextSymbols
, SourceGlobal(..)
, PreparedTypedInductive
, typedInductiveCarrierType
, typedInductiveCarrierBody
, typedInductiveGuardTargets
+ , PreparedTypedInductiveMonotonicity
+ , typedInductiveMonotonicities
+ , typedInductiveMonotonicityLocation
+ , typedInductiveMonotonicityTarget
+ , typedInductiveContextInventory
, PreparedTypedInductiveFact
, typedInductiveFacts
, typedInductiveFactMarker
, typedInductiveFactTarget
, typedInductiveFactRules
+ , typedInductiveFactRequiresMonotonicities
, typedInductiveFactDerivation
, prepareTypedClosedTerm
, prepareTypedClosedFormula
@@ -31,6 +42,7 @@ import Checking.Exact.Vocabulary
import Checking.Foundation
import Checking.Kernel.Derivation
import Checking.Kernel.Proof
+import Report.Location (Location)
import Syntax.Internal
import Control.Monad ((<=<), foldM)
@@ -63,7 +75,73 @@ data DirectInductiveClause = DirectInductiveClause
data DirectInductiveCondition
= DirectSideCondition !Formula
- | DirectRecursiveCondition !Term
+ | DirectRecursiveCondition !Term !RecursiveCarrierContext
+
+data RecursiveCarrierVariable
+ = RecursiveCarrierHole
+ | RecursiveCarrierSourceVariable !VarSymbol
+ deriving stock (Show, Eq, Ord)
+
+-- | A validated, capture-free one-hole carrier context in the same
+-- first-order set-term fragment lowered by this module. The source carrier
+-- application itself has been replaced, so the inductive symbol cannot
+-- survive inside this value.
+data RecursiveCarrierContext = RecursiveCarrierContext
+ !Location
+ !(ExprOf RecursiveCarrierVariable)
+ deriving stock (Show, Eq, Ord)
+
+data RecursiveCarrierContextError
+ = RecursiveCarrierWrongArguments !Location
+ | RecursiveCarrierUnsupportedContext !Location
+ deriving stock (Show, Eq)
+
+prepareRecursiveCarrierContext
+ :: FunctionSymbol
+ -> [VarSymbol]
+ -> Term
+ -> Either RecursiveCarrierContextError RecursiveCarrierContext
+prepareRecursiveCarrierContext carrier parameters source =
+ RecursiveCarrierContext (exprLocation source) <$> go source
+ where
+ carrierSymbol = SymbolMixfix carrier
+
+ go = \case
+ TermVar variable ->
+ pure
+ (TermVar
+ (RecursiveCarrierSourceVariable variable))
+ TermSymbol location symbol arguments
+ | symbol == carrierSymbol ->
+ if sameCarrierArguments arguments parameters
+ then pure (TermVar RecursiveCarrierHole)
+ else Left (RecursiveCarrierWrongArguments location)
+ | otherwise ->
+ TermSymbol location symbol <$> traverse go arguments
+ unsupported ->
+ Left
+ (RecursiveCarrierUnsupportedContext
+ (exprLocation unsupported))
+
+ sameCarrierArguments arguments variables =
+ length arguments == length variables
+ && and
+ (zipWith
+ (\argument variable ->
+ argument == TermVar variable)
+ arguments
+ variables)
+
+recursiveCarrierContextSymbols
+ :: RecursiveCarrierContext
+ -> Set Symbol
+recursiveCarrierContextSymbols
+ (RecursiveCarrierContext _location source) =
+ mentionedSymbols source
+
+directRecursiveCarrierContext :: Location -> RecursiveCarrierContext
+directRecursiveCarrierContext location =
+ RecursiveCarrierContext location (TermVar RecursiveCarrierHole)
data SourceGlobal global = SourceGlobal
!global
@@ -93,8 +171,80 @@ data PreparedTypedInductive global = PreparedTypedInductive
!CoreType
!(FrozenCheckedCore global)
!(Vector (FrozenCheckedCore global))
+ !(Vector (PreparedTypedInductiveMonotonicity global))
+ !(Vector (FrozenCheckedCore global))
!(NonEmpty (PreparedTypedInductiveFact global))
+data PreparedTypedInductiveMonotonicity global =
+ PreparedTypedInductiveMonotonicity
+ !Location
+ !(FrozenCheckedCore global)
+
+typedInductiveMonotonicities
+ :: PreparedTypedInductive global
+ -> Vector (PreparedTypedInductiveMonotonicity global)
+typedInductiveMonotonicities
+ (PreparedTypedInductive
+ _carrierType
+ _body
+ _guards
+ monotonicities
+ _contexts
+ _facts) =
+ monotonicities
+
+typedInductiveMonotonicityLocation
+ :: PreparedTypedInductiveMonotonicity global
+ -> Location
+typedInductiveMonotonicityLocation
+ (PreparedTypedInductiveMonotonicity location _target) =
+ location
+
+typedInductiveMonotonicityTarget
+ :: PreparedTypedInductiveMonotonicity global
+ -> FrozenCheckedCore global
+typedInductiveMonotonicityTarget
+ (PreparedTypedInductiveMonotonicity _location target) =
+ target
+
+typedInductiveContextInventory
+ :: PreparedTypedInductive global
+ -> Vector (FrozenCheckedCore global)
+typedInductiveContextInventory
+ (PreparedTypedInductive
+ _carrierType _body _guards _monotonicities contexts _facts) =
+ contexts
+
+data CheckedRecursiveCarrierContext global =
+ CheckedRecursiveCarrierContext
+ ![VarSymbol]
+ !(FrozenCheckedCore global)
+
+data PreparedInductiveSource global = PreparedInductiveSource
+ { preparedInductiveParams :: ![VarSymbol]
+ , preparedInductiveDomain :: !Term
+ , preparedInductiveClauses
+ :: !(NonEmpty (PreparedInductiveClause global))
+ }
+
+data PreparedInductiveClause global = PreparedInductiveClause
+ { preparedClauseVariables :: ![VarSymbol]
+ , preparedClauseConditions
+ :: ![PreparedInductiveCondition global]
+ , preparedClauseResult :: !Term
+ }
+
+data PreparedInductiveCondition global
+ = PreparedSideCondition !Formula
+ | PreparedDirectRecursiveCondition
+ !Term
+ !(CheckedRecursiveCarrierContext global)
+ | PreparedNestedRecursiveCondition
+ !Term
+ !(CheckedRecursiveCarrierContext global)
+ !ImportIx
+ !(FrozenCheckedCore global)
+
data PreparedInductiveGuard global
= PreparedFoundationGuard !FoundationAxiomTag
| PreparedImportedGuard
@@ -109,6 +259,8 @@ typedInductiveCarrierType
carrierType
_body
_guards
+ _monotonicities
+ _contexts
_facts) =
carrierType
@@ -120,6 +272,8 @@ typedInductiveCarrierBody
_carrierType
body
_guards
+ _monotonicities
+ _contexts
_facts) =
body
@@ -131,6 +285,8 @@ typedInductiveGuardTargets
_carrierType
_body
guards
+ _monotonicities
+ _contexts
_facts) =
guards
@@ -139,6 +295,7 @@ newtype PreparedTypedInductiveFact global =
( Marker
, FrozenCheckedCore global
, NonEmpty KernelRuleTag
+ , Bool
, KernelDerivation global
)
@@ -150,6 +307,8 @@ typedInductiveFacts
_carrierType
_body
_guards
+ _monotonicities
+ _contexts
facts) =
facts
@@ -158,7 +317,7 @@ typedInductiveFactMarker
-> Marker
typedInductiveFactMarker
(PreparedTypedInductiveFact
- (marker, _target, _rule, _derivation)) =
+ (marker, _target, _rule, _monotonicities, _derivation)) =
marker
typedInductiveFactTarget
@@ -166,7 +325,7 @@ typedInductiveFactTarget
-> FrozenCheckedCore global
typedInductiveFactTarget
(PreparedTypedInductiveFact
- (_marker, target, _rule, _derivation)) =
+ (_marker, target, _rule, _monotonicities, _derivation)) =
target
typedInductiveFactRules
@@ -174,15 +333,23 @@ typedInductiveFactRules
-> NonEmpty KernelRuleTag
typedInductiveFactRules
(PreparedTypedInductiveFact
- (_marker, _target, rules, _derivation)) =
+ (_marker, _target, rules, _monotonicities, _derivation)) =
rules
+typedInductiveFactRequiresMonotonicities
+ :: PreparedTypedInductiveFact global
+ -> Bool
+typedInductiveFactRequiresMonotonicities
+ (PreparedTypedInductiveFact
+ (_marker, _target, _rules, required, _derivation)) =
+ required
+
typedInductiveFactDerivation
:: PreparedTypedInductiveFact global
-> KernelDerivation global
typedInductiveFactDerivation
(PreparedTypedInductiveFact
- (_marker, _target, _rule, derivation)) =
+ (_marker, _target, _rule, _monotonicities, derivation)) =
derivation
-- | Lower one closed source formula through the exact primitive/global
@@ -326,13 +493,9 @@ prepareTypedInductiveInternal
resolveGlobal
marker
inductive = do
- carrierBody <-
- prepareCarrierBody
- resolveGlobal
- inductive
guards <-
traverse
- (prepareGuardTarget
+ (prepareDirectGuardTarget
resolveGlobal
inductive)
(directInductiveClauses
@@ -340,12 +503,27 @@ prepareTypedInductiveInternal
let preparedGuards =
assignGuardSources foundation
(NonEmpty.toList guards)
+ nextImport =
+ fromIntegral
+ (length
+ [ ()
+ | PreparedImportedGuard{} <- preparedGuards
+ ])
+ (preparedSource, monotonicities, contexts) <-
+ prepareInductiveSource
+ resolveGlobal
+ nextImport
+ inductive
+ carrierBody <-
+ prepareCarrierBody
+ resolveGlobal
+ preparedSource
facts <-
prepareFacts
foundation
resolveGlobal
marker
- inductive
+ preparedSource
(case preparedGuards of
firstGuard : remainingGuards ->
firstGuard :| remainingGuards
@@ -361,6 +539,8 @@ prepareTypedInductiveInternal
| PreparedImportedGuard
_index target <- preparedGuards
])
+ (Vector.fromList monotonicities)
+ (Vector.fromList contexts)
facts)
where
carrierType =
@@ -385,34 +565,264 @@ mapPreparedTypedInductive
-> PreparedTypedInductive left
-> PreparedTypedInductive right
mapPreparedTypedInductive transform
- (PreparedTypedInductive carrierType body guards facts) =
+ (PreparedTypedInductive
+ carrierType body guards monotonicities contexts facts) =
PreparedTypedInductive
carrierType
(mapFrozenGlobals transform body)
(mapFrozenGlobals transform <$> guards)
+ (mapMonotonicity transform <$> monotonicities)
+ (mapFrozenGlobals transform <$> contexts)
(mapPreparedFact transform <$> facts)
where
+ mapMonotonicity mapGlobal
+ (PreparedTypedInductiveMonotonicity location target) =
+ PreparedTypedInductiveMonotonicity
+ location
+ (mapFrozenGlobals mapGlobal target)
+
mapPreparedFact mapGlobal
(PreparedTypedInductiveFact
- (marker, target, rule, derivation)) =
+ (marker, target, rule, requiresMonotonicities, derivation)) =
PreparedTypedInductiveFact
( marker
, mapFrozenGlobals mapGlobal target
, rule
+ , requiresMonotonicities
, mapKernelDerivationGlobals mapGlobal derivation
)
-prepareCarrierBody
+data MonotonicityInventory global = MonotonicityInventory
+ ![(FrozenCheckedCore global, ImportIx)]
+ !Natural
+ ![PreparedTypedInductiveMonotonicity global]
+ ![FrozenCheckedCore global]
+
+prepareInductiveSource
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
+ -> Natural
-> DirectInductive
-> Either
TypedInductiveError
+ ( PreparedInductiveSource (InductiveGlobal global)
+ , [PreparedTypedInductiveMonotonicity (InductiveGlobal global)]
+ , [FrozenCheckedCore (InductiveGlobal global)]
+ )
+prepareInductiveSource resolveGlobal firstImport inductive = do
+ (final, clauses) <-
+ prepareClauses
+ (MonotonicityInventory [] firstImport [] [])
+ (NonEmpty.toList (directInductiveClauses inductive))
+ let MonotonicityInventory
+ _targets _next monotonicities contexts = final
+ pure
+ ( PreparedInductiveSource
+ (directInductiveParams inductive)
+ (directInductiveDomain inductive)
+ (NonEmpty.fromList clauses)
+ , reverse monotonicities
+ , reverse contexts
+ )
+ where
+ variablesFor clause =
+ directInductiveParams inductive
+ <> directClauseVariables clause
+
+ prepareClauses inventory = \case
+ [] -> pure (inventory, [])
+ clause : remaining -> do
+ (afterClause, preparedClause) <-
+ prepareClause inventory clause
+ (final, preparedRemaining) <-
+ prepareClauses afterClause remaining
+ pure (final, preparedClause : preparedRemaining)
+
+ prepareClause inventory clause = do
+ (next, conditions) <-
+ prepareConditions inventory clause
+ (directClauseConditions clause)
+ pure
+ ( next
+ , PreparedInductiveClause
+ (directClauseVariables clause)
+ conditions
+ (directClauseResult clause)
+ )
+
+ prepareConditions inventory _clause [] =
+ pure (inventory, [])
+ prepareConditions inventory clause (condition : remaining) = do
+ (next, prepared) <-
+ prepareCondition inventory clause condition
+ (final, preparedRemaining) <-
+ prepareConditions next clause remaining
+ pure (final, prepared : preparedRemaining)
+
+ prepareCondition inventory _clause (DirectSideCondition formula) =
+ pure (inventory, PreparedSideCondition formula)
+ prepareCondition
+ (MonotonicityInventory targets next facts contexts)
+ clause
+ (DirectRecursiveCondition recursiveTerm sourceContext) = do
+ checkedContext <-
+ prepareRecursiveCarrierTemplate
+ resolveGlobal
+ (variablesFor clause)
+ sourceContext
+ let template = checkedRecursiveCarrierTemplate checkedContext
+ withContext currentFacts =
+ MonotonicityInventory
+ targets next currentFacts (template : contexts)
+ if recursiveCarrierContextIsDirect sourceContext
+ then pure
+ ( withContext facts
+ , PreparedDirectRecursiveCondition
+ recursiveTerm checkedContext
+ )
+ else do
+ target <-
+ prepareRecursiveCarrierMonotonicityTarget
+ checkedContext
+ let RecursiveCarrierContext location _source = sourceContext
+ case List.lookup target targets of
+ Just index ->
+ pure
+ ( MonotonicityInventory
+ targets next facts (template : contexts)
+ , PreparedNestedRecursiveCondition
+ recursiveTerm checkedContext index target
+ )
+ Nothing ->
+ let index = importIx next
+ in pure
+ ( MonotonicityInventory
+ ((target, index) : targets)
+ (next + 1)
+ (PreparedTypedInductiveMonotonicity
+ location target : facts)
+ (template : contexts)
+ , PreparedNestedRecursiveCondition
+ recursiveTerm checkedContext index target
+ )
+
+checkedRecursiveCarrierTemplate
+ :: CheckedRecursiveCarrierContext global
+ -> FrozenCheckedCore global
+checkedRecursiveCarrierTemplate
+ (CheckedRecursiveCarrierContext _variables template) =
+ template
+
+recursiveCarrierContextIsDirect :: RecursiveCarrierContext -> Bool
+recursiveCarrierContextIsDirect
+ (RecursiveCarrierContext _location source) =
+ source == TermVar RecursiveCarrierHole
+
+prepareRecursiveCarrierTemplate
+ :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
+ -> [VarSymbol]
+ -> RecursiveCarrierContext
+ -> Either
+ TypedInductiveError
+ (CheckedRecursiveCarrierContext (InductiveGlobal global))
+prepareRecursiveCarrierTemplate resolveGlobal variables context = do
+ body <-
+ buildUnderVariables emptyEnvironment variables \environment -> do
+ underHole <- shiftEnvironment environment
+ lowerRecursiveCarrierContext
+ resolveGlobal underHole (CBound 0) context
+ checked <-
+ first TypedInductiveCoreError
+ (checkCanonicalCore
+ (Just . inductiveGlobalType)
+ -- Transparent expansion may leave beta redexes. Freeze one
+ -- normalized template so routing, generated laws, and kernel
+ -- transport all see the same first-order shape.
+ (betaNormalizeCanonical
+ (closeLambdas (length variables + 1) body)))
+ pure (CheckedRecursiveCarrierContext variables checked)
+
+prepareRecursiveCarrierMonotonicityTarget
+ :: CheckedRecursiveCarrierContext (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
+ (FrozenCheckedCore (InductiveGlobal global))
+prepareRecursiveCarrierMonotonicityTarget
+ context@(CheckedRecursiveCarrierContext variables _template) = do
+ target <-
+ buildUnderVariables emptyEnvironment variables \environment -> do
+ underSets <- shiftEnvironment =<< shiftEnvironment environment
+ left <-
+ instantiateRecursiveCarrier
+ underSets (CBound 1) context
+ right <-
+ instantiateRecursiveCarrier
+ underSets (CBound 0) context
+ pure
+ (CImp
+ (subsetTerm (CBound 1) (CBound 0))
+ (subsetTerm left right))
+ freezeClosedTarget
+ (closeForalls (length variables + 2) target)
+
+instantiateRecursiveCarrier
+ :: InductiveEnvironment
+ -> CanonicalTerm (InductiveGlobal global)
+ -> CheckedRecursiveCarrierContext (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
+ (CanonicalTerm (InductiveGlobal global))
+instantiateRecursiveCarrier environment replacement
+ context@(CheckedRecursiveCarrierContext variables _template) = do
+ arguments <- traverse (`lookupEnvironment` environment) variables
+ foldM instantiateLambda
+ (frozenCoreTerm (checkedRecursiveCarrierTemplate context))
+ (arguments <> [replacement])
+ where
+ instantiateLambda term argument =
+ case term of
+ CLam TySet body ->
+ pure (instantiateCanonical argument body)
+ _ ->
+ Left
+ (TypedInductiveUnsupportedExpression
+ "a checked recursive carrier context lost its set telescope")
+
+lowerRecursiveCarrierContext
+ :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
+ -> InductiveEnvironment
+ -> CanonicalTerm (InductiveGlobal global)
+ -> RecursiveCarrierContext
+ -> Either
+ TypedInductiveError
+ (CanonicalTerm (InductiveGlobal global))
+lowerRecursiveCarrierContext resolveGlobal environment replacement
+ (RecursiveCarrierContext _location source) =
+ go source
+ where
+ go = \case
+ TermVar RecursiveCarrierHole ->
+ pure replacement
+ TermVar (RecursiveCarrierSourceVariable variable) ->
+ lookupEnvironment variable environment
+ TermSymbol _location symbol arguments -> do
+ lowered <- traverse go arguments
+ lowerApplicationTerms resolveGlobal symbol lowered
+ _ ->
+ Left
+ (TypedInductiveUnsupportedExpression
+ "a validated recursive carrier context left the supported set-term fragment")
+
+prepareCarrierBody
+ :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
+ -> PreparedInductiveSource (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
(FrozenCheckedCore (InductiveGlobal global))
prepareCarrierBody resolveGlobal inductive = do
body <-
buildUnderVariables
emptyEnvironment
- (directInductiveParams
+ (preparedInductiveParams
inductive)
(\env -> fixedPointTerm
resolveGlobal
@@ -420,8 +830,8 @@ prepareCarrierBody resolveGlobal inductive = do
env)
let closed =
closeLambdas
- (length
- (directInductiveParams
+ (length
+ (preparedInductiveParams
inductive))
body
checked <-
@@ -431,14 +841,14 @@ prepareCarrierBody resolveGlobal inductive = do
closed)
pure checked
-prepareGuardTarget
+prepareDirectGuardTarget
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> DirectInductive
-> DirectInductiveClause
-> Either
TypedInductiveError
(FrozenCheckedCore (InductiveGlobal global))
-prepareGuardTarget
+prepareDirectGuardTarget
resolveGlobal
inductive
clause = do
@@ -456,7 +866,7 @@ prepareGuardTarget
inductive)
conditions <-
traverse
- (conditionTerm
+ (directConditionTerm
resolveGlobal
environment
domain)
@@ -515,7 +925,7 @@ prepareFacts
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> Marker
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> NonEmpty (PreparedInductiveGuard (InductiveGlobal global))
-> Either
TypedInductiveError
@@ -545,7 +955,7 @@ prepareFacts
(0 :| [1 ..])
(NonEmpty.zip
guards
- (directInductiveClauses
+ (preparedInductiveClauses
inductive)))
domainSubset <-
first
@@ -583,9 +993,9 @@ prepareIntroductionFact
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> Marker
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> Natural
- -> (PreparedInductiveGuard (InductiveGlobal global), DirectInductiveClause)
+ -> (PreparedInductiveGuard (InductiveGlobal global), PreparedInductiveClause (InductiveGlobal global))
-> Either
TypedInductiveError
(PreparedTypedInductiveFact (InductiveGlobal global))
@@ -602,15 +1012,15 @@ prepareIntroductionFact
foundation
(Just . inductiveGlobalType))
emptyEnvironment
- (directInductiveParams inductive
- <> directClauseVariables clause)
+ (preparedInductiveParams inductive
+ <> preparedClauseVariables clause)
(\context environment -> do
domain <-
checkedTerm context
=<< lowerTerm
resolveGlobal
environment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operator <-
checkedTerm context
@@ -646,14 +1056,14 @@ prepareIntroductionFact
environment
(scopedCoreTerm
fixedPoint))
- (directClauseConditions
+ (preparedClauseConditions
clause)
result <-
checkedTerm context
=<< lowerTerm
resolveGlobal
environment
- (directClauseResult
+ (preparedClauseResult
clause)
let conditionTerms =
scopedCoreTerm <$> conditions
@@ -675,18 +1085,18 @@ prepareIntroductionFact
(eliminateWrittenForalls
context
environment
- (directInductiveParams
+ (preparedInductiveParams
inductive
- <> directClauseVariables
+ <> preparedClauseVariables
clause)
guardProof)
guardPremiseProofs <-
sequence
[ case condition of
- DirectSideCondition _formula ->
+ PreparedSideCondition _formula ->
pure premiseProof
- DirectRecursiveCondition
- recursiveTerm -> do
+ PreparedDirectRecursiveCondition
+ recursiveTerm _context -> do
bound <-
first
TypedInductiveProofError
@@ -713,9 +1123,32 @@ prepareIntroductionFact
context
implication
premiseProof)
+ nested@PreparedNestedRecursiveCondition{} -> do
+ bound <-
+ first TypedInductiveProofError
+ (setLfpBoundProof
+ context
+ domain
+ operator)
+ recursiveElement <-
+ checkedTerm context
+ =<< lowerTerm
+ resolveGlobal
+ environment
+ (preparedRecursiveTerm
+ nested)
+ transportNestedRecursiveMembership
+ context
+ environment
+ nested
+ fixedPoint
+ domain
+ recursiveElement
+ bound
+ premiseProof
| (condition, premiseProof) <-
zip
- (directClauseConditions
+ (preparedClauseConditions
clause)
premiseProofs
]
@@ -841,14 +1274,16 @@ prepareIntroductionFact
marker
(clauseIndex + 1))
(if any isRecursiveCondition
- (directClauseConditions clause)
+ (preparedClauseConditions clause)
then SetLfpBound :| [SetLfpFixed]
else SetLfpFixed :| [])
+ True
proof
where
isRecursiveCondition = \case
- DirectRecursiveCondition{} -> True
- DirectSideCondition{} -> False
+ PreparedDirectRecursiveCondition{} -> True
+ PreparedNestedRecursiveCondition{} -> True
+ PreparedSideCondition{} -> False
preparedGuardProof
:: ProofContext (InductiveGlobal global)
@@ -868,7 +1303,7 @@ prepareDomainSubsetFact
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> Marker
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> Either
TypedInductiveError
(PreparedTypedInductiveFact (InductiveGlobal global))
@@ -883,7 +1318,7 @@ prepareDomainSubsetFact
foundation
(Just . inductiveGlobalType))
emptyEnvironment
- (directInductiveParams
+ (preparedInductiveParams
inductive)
(\context environment -> do
domain <-
@@ -891,7 +1326,7 @@ prepareDomainSubsetFact
=<< lowerTerm
resolveGlobal
environment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operator <-
checkedTerm context
@@ -907,13 +1342,14 @@ prepareDomainSubsetFact
preparedFact
(derivedMarker marker "dom_subset")
(SetLfpBound :| [])
+ False
proof
prepareCasesFact
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> Marker
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> Either
TypedInductiveError
(PreparedTypedInductiveFact (InductiveGlobal global))
@@ -928,7 +1364,7 @@ prepareCasesFact
foundation
(Just . inductiveGlobalType))
emptyEnvironment
- (directInductiveParams
+ (preparedInductiveParams
inductive)
(\parameterContext parameterEnvironment ->
forallIntroductionTyped
@@ -943,7 +1379,7 @@ prepareCasesFact
=<< lowerTerm
resolveGlobal
environment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operator <-
checkedTerm context
@@ -1058,13 +1494,14 @@ prepareCasesFact
preparedFact
(derivedMarker marker "cases")
(SetLfpFixed :| [])
+ True
proof
prepareInductionFact
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> Marker
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> Either
TypedInductiveError
(PreparedTypedInductiveFact (InductiveGlobal global))
@@ -1079,7 +1516,7 @@ prepareInductionFact
foundation
(Just . inductiveGlobalType))
emptyEnvironment
- (directInductiveParams
+ (preparedInductiveParams
inductive)
(\parameterContext parameterEnvironment ->
forallIntroductionTyped
@@ -1123,7 +1560,7 @@ prepareInductionFact
=<< lowerTerm
resolveGlobal
elementEnvironment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operator <-
checkedTerm elementContext
@@ -1201,6 +1638,7 @@ prepareInductionFact
preparedFact
(derivedMarker marker "induct")
(SetLfpInduct :| [])
+ True
proof
proveUnderVariables
@@ -1248,11 +1686,12 @@ checkedTerm context =
preparedFact
:: Marker
-> NonEmpty KernelRuleTag
+ -> Bool
-> BuiltProof (InductiveGlobal global)
-> Either
TypedInductiveError
(PreparedTypedInductiveFact (InductiveGlobal global))
-preparedFact marker rules proof = do
+preparedFact marker rules requiresMonotonicities proof = do
target <-
maybe
(Left TypedInductiveProofRemainedOpen)
@@ -1264,6 +1703,7 @@ preparedFact marker rules proof = do
( marker
, target
, canonicalRules rules
+ , requiresMonotonicities
, builtProofDerivation proof
))
where
@@ -1407,8 +1847,8 @@ projectConjunctionList context terms proof = do
introduceClauseWitnesses
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
- -> DirectInductiveClause
+ -> PreparedInductiveSource (InductiveGlobal global)
+ -> PreparedInductiveClause (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
@@ -1427,7 +1867,7 @@ introduceClauseWitnesses
result
bodyProof =
introduce
- (directClauseVariables clause)
+ (preparedClauseVariables clause)
where
introduce [] =
pure bodyProof
@@ -1477,7 +1917,7 @@ introduceClauseWitnesses
clauseFormulaWithBinders
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductiveClause
+ -> PreparedInductiveClause (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> CanonicalTerm (InductiveGlobal global)
@@ -1498,13 +1938,13 @@ clauseFormulaWithBinders
resolveGlobal
environment
candidate)
- (directClauseConditions
+ (preparedClauseConditions
clause)
clauseResult <-
lowerTerm
resolveGlobal
environment
- (directClauseResult clause)
+ (preparedClauseResult clause)
pure
(fromMaybe
(CEq TySet result clauseResult)
@@ -1608,7 +2048,7 @@ injectDisjunction context index alternatives proof =
closureTerms
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> Either
@@ -1621,18 +2061,18 @@ closureTerms
subset =
traverse closureFor
(NonEmpty.toList
- (directInductiveClauses
+ (preparedInductiveClauses
inductive))
where
closureFor clause = do
clauseEnvironment <-
extendVariables
environment
- (directClauseVariables clause)
+ (preparedClauseVariables clause)
let binderCount =
fromIntegral
(length
- (directClauseVariables
+ (preparedClauseVariables
clause))
subset' =
shiftCanonicalTerm
@@ -1645,17 +2085,17 @@ closureTerms
resolveGlobal
clauseEnvironment
subset')
- (directClauseConditions
+ (preparedClauseConditions
clause)
result <-
lowerTerm
resolveGlobal
clauseEnvironment
- (directClauseResult clause)
+ (preparedClauseResult clause)
pure
(closeForalls
(length
- (directClauseVariables
+ (preparedClauseVariables
clause))
(impliesIfNeeded
(conjunctionList conditions)
@@ -1666,7 +2106,7 @@ closureTerms
proveBoundedMonotonicity
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> Either
@@ -1683,7 +2123,7 @@ proveBoundedMonotonicity
=<< lowerTerm
resolveGlobal
environment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operator <-
checkedTerm context
@@ -1712,7 +2152,7 @@ proveBoundedMonotonicity
=<< lowerTerm
resolveGlobal
elementEnvironment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
predicate <-
checkedTerm elementContext
@@ -1787,7 +2227,7 @@ proveBoundedMonotonicity
=<< lowerTerm
resolveGlobal
xyEnvironment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
relation <-
checkedTerm xyContext
@@ -1843,7 +2283,7 @@ proveBoundedMonotonicity
=<< lowerTerm
resolveGlobal
elementEnvironment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
predicateX <-
checkedTerm
@@ -2021,7 +2461,7 @@ proveBoundedMonotonicity
transformPredicateProof
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
@@ -2067,7 +2507,7 @@ transformPredicateProof
(atNatural
clauseIndex
(NonEmpty.toList
- (directInductiveClauses
+ (preparedInductiveClauses
inductive)))
first
(TypedInductivePreparationContext
@@ -2141,7 +2581,7 @@ transformPredicateProof
transformClauseBody
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductiveClause
+ -> PreparedInductiveClause (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
@@ -2168,13 +2608,13 @@ transformClauseBody
resolveGlobal
environment
candidateX)
- (directClauseConditions
+ (preparedClauseConditions
clause)
clauseResult <-
lowerTerm
resolveGlobal
environment
- (directClauseResult clause)
+ (preparedClauseResult clause)
let equality =
CEq TySet result clauseResult
bodyTermsX =
@@ -2191,9 +2631,10 @@ transformClauseBody
transformedConditions <-
sequence
[ case condition of
- DirectSideCondition _formula ->
+ PreparedSideCondition _formula ->
pure conditionProof
- DirectRecursiveCondition recursiveTerm -> do
+ PreparedDirectRecursiveCondition
+ recursiveTerm _context -> do
recursiveElement <-
checkedTerm context
=<< lowerTerm
@@ -2217,9 +2658,33 @@ transformClauseBody
context
implication
conditionProof)
+ nested@PreparedNestedRecursiveCondition{} -> do
+ recursiveElement <-
+ checkedTerm context
+ =<< lowerTerm
+ resolveGlobal
+ environment
+ (preparedRecursiveTerm nested)
+ subsetProof <-
+ subsetRelationHypothesis
+ context
+ candidateX
+ candidateY
+ domain
+ left <- checkedTerm context candidateX
+ right <- checkedTerm context candidateY
+ transportNestedRecursiveMembership
+ context
+ environment
+ nested
+ left
+ right
+ recursiveElement
+ subsetProof
+ conditionProof
| (condition, conditionProof) <-
zip
- (directClauseConditions clause)
+ (preparedClauseConditions clause)
conditionProofs
]
equalityProof <-
@@ -2270,9 +2735,163 @@ subsetRelationHypothesis
rightSubsetDomain
relationProof)
+preparedRecursiveTerm
+ :: PreparedInductiveCondition global
+ -> Term
+preparedRecursiveTerm = \case
+ PreparedDirectRecursiveCondition term _context -> term
+ PreparedNestedRecursiveCondition term _context _index _target -> term
+ PreparedSideCondition{} ->
+ impossible "a side condition has no recursive element"
+
+transportNestedRecursiveMembership
+ :: ProofContext (InductiveGlobal global)
+ -> InductiveEnvironment
+ -> PreparedInductiveCondition (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> BuiltProof (InductiveGlobal global)
+ -> BuiltProof (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
+ (BuiltProof (InductiveGlobal global))
+transportNestedRecursiveMembership
+ context
+ environment
+ condition
+ left
+ right
+ element
+ subsetProof
+ membership = do
+ monotonicity <-
+ nestedRecursiveMonotonicityProof
+ context environment condition left right subsetProof
+ implication <-
+ first TypedInductiveProofError
+ (forallEliminationProof
+ context monotonicity element)
+ first TypedInductiveProofError
+ (implicationEliminationProof
+ context implication membership)
+
+nestedRecursiveMonotonicityProof
+ :: ProofContext (InductiveGlobal global)
+ -> InductiveEnvironment
+ -> PreparedInductiveCondition (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> BuiltProof (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
+ (BuiltProof (InductiveGlobal global))
+nestedRecursiveMonotonicityProof
+ context
+ environment
+ (PreparedNestedRecursiveCondition
+ _term
+ (CheckedRecursiveCarrierContext variables _template)
+ index
+ target)
+ left
+ right
+ subsetProof = do
+ theorem <-
+ first TypedInductiveProofError
+ (importedProof context index target)
+ specialized <-
+ eliminateWrittenForalls
+ context environment variables theorem
+ atLeft <-
+ first TypedInductiveProofError
+ (forallEliminationProof context specialized left)
+ atRight <-
+ first TypedInductiveProofError
+ (forallEliminationProof context atLeft right)
+ first TypedInductiveProofError
+ (implicationEliminationProof
+ context atRight subsetProof)
+nestedRecursiveMonotonicityProof
+ _context _environment _condition _left _right _subsetProof =
+ Left
+ (TypedInductiveUnsupportedExpression
+ "nested carrier transport requires a monotonicity import")
+
+proveInductionCandidateSubset
+ :: ProofContext (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> ScopedCheckedCore (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
+ (BuiltProof (InductiveGlobal global))
+proveInductionCandidateSubset
+ context fixedPoint predicate candidate subset =
+ proveSubset
+ context candidate subset
+ (\elementContext element membership -> do
+ fixedPointAtElement <-
+ first TypedInductiveCoreError
+ (weakenScopedCore
+ (Just . inductiveGlobalType)
+ TySet
+ fixedPoint)
+ predicateAtElement <-
+ first TypedInductiveCoreError
+ (weakenScopedCore
+ (Just . inductiveGlobalType)
+ TySet
+ predicate)
+ explicitMembership <-
+ checkedTerm elementContext
+ (memberTerm
+ (scopedCoreTerm element)
+ (apply2
+ (CIntrinsic Sep)
+ (scopedCoreTerm fixedPointAtElement)
+ (scopedCoreTerm predicateAtElement)))
+ membership' <-
+ first TypedInductiveProofError
+ (conversionProof
+ elementContext membership explicitMembership)
+ characteristic <-
+ separationForward
+ elementContext
+ fixedPointAtElement
+ predicateAtElement
+ element
+ membership'
+ satisfies <-
+ first TypedInductiveProofError
+ (conjunctionRightProof
+ elementContext
+ (memberTerm
+ (scopedCoreTerm element)
+ (scopedCoreTerm fixedPointAtElement))
+ (CApp
+ (scopedCoreTerm predicateAtElement)
+ (scopedCoreTerm element))
+ characteristic)
+ expected <-
+ first TypedInductiveCoreError
+ (weakenScopedCore
+ (Just . inductiveGlobalType)
+ TySet
+ subset)
+ target <-
+ checkedTerm elementContext
+ (memberTerm
+ (scopedCoreTerm element)
+ (scopedCoreTerm expected))
+ first TypedInductiveProofError
+ (conversionProof
+ elementContext satisfies target))
+
eliminateClauseWitnesses
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductiveClause
+ -> PreparedInductiveClause (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
@@ -2310,7 +2929,7 @@ eliminateClauseWitnesses
initialResult
initialProof
initialTarget
- (directClauseVariables clause)
+ (preparedClauseVariables clause)
where
go depth context environment candidate result proof target = \case
[] ->
@@ -2442,7 +3061,7 @@ eliminateDisjunctionAlternatives
proveInductionClosure
:: CheckedFoundation
-> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> ScopedCheckedCore (InductiveGlobal global)
@@ -2521,7 +3140,7 @@ proveInductionClosure
=<< lowerTerm
resolveGlobal
elementEnvironment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operatorPredicate <-
checkedTerm withMember
@@ -2620,7 +3239,7 @@ proveInductionClosure
(atNatural
clauseIndex
(NonEmpty.toList
- (directInductiveClauses
+ (preparedInductiveClauses
inductive)))
first
(TypedInductivePreparationContext
@@ -2688,9 +3307,9 @@ proveInductionClosure
proveInductionClause
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> Natural
- -> DirectInductiveClause
+ -> PreparedInductiveClause (InductiveGlobal global)
-> ProofContext (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
@@ -2724,13 +3343,13 @@ proveInductionClause
(CIntrinsic Sep)
fixedPoint
predicate))
- (directClauseConditions
+ (preparedClauseConditions
clause)
clauseResult <-
lowerTerm
resolveGlobal
environment
- (directClauseResult clause)
+ (preparedClauseResult clause)
let equality =
CEq TySet result clauseResult
bodyTerms =
@@ -2750,9 +3369,10 @@ proveInductionClause
closureConditionProofs <-
sequence
[ case condition of
- DirectSideCondition _formula ->
+ PreparedSideCondition _formula ->
pure conditionProof
- DirectRecursiveCondition recursiveTerm -> do
+ PreparedDirectRecursiveCondition
+ recursiveTerm _context -> do
recursiveElement <-
checkedTerm context
=<< lowerTerm
@@ -2794,9 +3414,41 @@ proveInductionClause
context
predicateMembership
expected)
+ nested@PreparedNestedRecursiveCondition{} -> do
+ recursiveElement <-
+ checkedTerm context
+ =<< lowerTerm
+ resolveGlobal
+ environment
+ (preparedRecursiveTerm nested)
+ fixedPoint' <- checkedTerm context fixedPoint
+ predicate' <- checkedTerm context predicate
+ candidate <-
+ checkedTerm context
+ (apply2
+ (CIntrinsic Sep)
+ fixedPoint
+ predicate)
+ subset' <- checkedTerm context subset
+ candidateSubset <-
+ proveInductionCandidateSubset
+ context
+ fixedPoint'
+ predicate'
+ candidate
+ subset'
+ transportNestedRecursiveMembership
+ context
+ environment
+ nested
+ candidate
+ subset'
+ recursiveElement
+ candidateSubset
+ conditionProof
| (condition, conditionProof) <-
zip
- (directClauseConditions clause)
+ (preparedClauseConditions clause)
conditionProofs
]
closureConjunction <-
@@ -2840,7 +3492,7 @@ proveInductionClause
(eliminateWrittenForalls
context
environment
- (directClauseVariables clause)
+ (preparedClauseVariables clause)
selectedClosure)
resultMembership <-
case closureConditionProofs of
@@ -2951,7 +3603,7 @@ transportElementMembership
predicateAt
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> CanonicalTerm (InductiveGlobal global)
@@ -2974,7 +3626,7 @@ predicateAt
clauseFormulaTerms
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> CanonicalTerm (InductiveGlobal global)
@@ -2994,7 +3646,7 @@ clauseFormulaTerms
candidate
result)
(NonEmpty.toList
- (directInductiveClauses
+ (preparedInductiveClauses
inductive))
clauseFormulaAt
@@ -3002,7 +3654,7 @@ clauseFormulaAt
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> CanonicalTerm (InductiveGlobal global)
- -> DirectInductiveClause
+ -> PreparedInductiveClause (InductiveGlobal global)
-> Either
TypedInductiveError
(CanonicalTerm (InductiveGlobal global))
@@ -3015,11 +3667,11 @@ clauseFormulaAt
clauseEnvironment <-
extendVariables
environment
- (directClauseVariables clause)
+ (preparedClauseVariables clause)
let binderCount =
fromIntegral
(length
- (directClauseVariables
+ (preparedClauseVariables
clause))
candidate' =
shiftCanonicalTerm binderCount 0 candidate
@@ -3031,17 +3683,17 @@ clauseFormulaAt
resolveGlobal
clauseEnvironment
candidate')
- (directClauseConditions
+ (preparedClauseConditions
clause)
clauseResult <-
lowerTerm
resolveGlobal
clauseEnvironment
- (directClauseResult clause)
+ (preparedClauseResult clause)
pure
(closeExistentials
(length
- (directClauseVariables
+ (preparedClauseVariables
clause))
(fromMaybe
(CEq TySet result' clauseResult)
@@ -3101,7 +3753,7 @@ membershipPredicate context set = do
operatorPredicateAt
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> Either
@@ -3128,7 +3780,7 @@ operatorPredicateAt
separationSetAt
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
-> Either
@@ -3143,7 +3795,7 @@ separationSetAt
lowerTerm
resolveGlobal
environment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
predicate <-
operatorPredicateAt
@@ -3472,7 +4124,7 @@ buildUnderVariables
fixedPointTerm
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> Either
TypedInductiveError
@@ -3482,7 +4134,7 @@ fixedPointTerm resolveGlobal inductive environment = do
lowerTerm
resolveGlobal
environment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
operator <-
operatorTerm
@@ -3498,7 +4150,7 @@ fixedPointTerm resolveGlobal inductive environment = do
operatorTerm
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
- -> DirectInductive
+ -> PreparedInductiveSource (InductiveGlobal global)
-> InductiveEnvironment
-> Either
TypedInductiveError
@@ -3510,7 +4162,7 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do
lowerTerm
resolveGlobal
candidateEnvironment
- (directInductiveDomain
+ (preparedInductiveDomain
inductive)
resultEnvironment <-
shiftEnvironment candidateEnvironment
@@ -3519,7 +4171,7 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do
(clausePredicateTerm
resolveGlobal
resultEnvironment)
- (directInductiveClauses
+ (preparedInductiveClauses
inductive)
pure
(CLam TySet
@@ -3535,7 +4187,7 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do
clausePredicateTerm
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> InductiveEnvironment
- -> DirectInductiveClause
+ -> PreparedInductiveClause (InductiveGlobal global)
-> Either
TypedInductiveError
(CanonicalTerm (InductiveGlobal global))
@@ -3546,11 +4198,11 @@ clausePredicateTerm
clauseEnvironment <-
extendVariables
resultEnvironment
- (directClauseVariables clause)
+ (preparedClauseVariables clause)
let variableCount =
fromIntegral
(length
- (directClauseVariables
+ (preparedClauseVariables
clause))
resultVariable =
CBound variableCount
@@ -3562,18 +4214,18 @@ clausePredicateTerm
resolveGlobal
clauseEnvironment
candidate)
- (directClauseConditions
+ (preparedClauseConditions
clause)
result <-
lowerTerm
resolveGlobal
clauseEnvironment
- (directClauseResult
+ (preparedClauseResult
clause)
pure
(closeExistentials
(length
- (directClauseVariables clause))
+ (preparedClauseVariables clause))
(fromMaybe
(CEq
TySet
@@ -3586,7 +4238,7 @@ clausePredicateTerm
resultVariable
result]))))
-conditionTerm
+directConditionTerm
:: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
-> InductiveEnvironment
-> CanonicalTerm (InductiveGlobal global)
@@ -3594,19 +4246,47 @@ conditionTerm
-> Either
TypedInductiveError
(CanonicalTerm (InductiveGlobal global))
-conditionTerm resolveGlobal environment candidate = \case
+directConditionTerm resolveGlobal environment candidate = \case
DirectSideCondition formula ->
+ lowerFormula resolveGlobal environment formula
+ DirectRecursiveCondition term context -> do
+ carrier <-
+ betaNormalizeCanonical
+ <$> lowerRecursiveCarrierContext
+ resolveGlobal environment candidate context
+ memberTerm
+ <$> lowerTerm resolveGlobal environment term
+ <*> pure carrier
+
+conditionTerm
+ :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global)))
+ -> InductiveEnvironment
+ -> CanonicalTerm (InductiveGlobal global)
+ -> PreparedInductiveCondition (InductiveGlobal global)
+ -> Either
+ TypedInductiveError
+ (CanonicalTerm (InductiveGlobal global))
+conditionTerm resolveGlobal environment candidate = \case
+ PreparedSideCondition formula ->
lowerFormula
resolveGlobal
environment
formula
- DirectRecursiveCondition term ->
+ PreparedDirectRecursiveCondition term context -> do
+ carrier <-
+ instantiateRecursiveCarrier environment candidate context
memberTerm
<$> lowerTerm
resolveGlobal
environment
term
- <*> pure candidate
+ <*> pure carrier
+ PreparedNestedRecursiveCondition term context _index _target -> do
+ carrier <-
+ instantiateRecursiveCarrier environment candidate context
+ memberTerm
+ <$> lowerTerm resolveGlobal environment term
+ <*> pure carrier
shiftEnvironment
:: InductiveEnvironment
@@ -3708,7 +4388,7 @@ lowerFormulaWith allowQuantified resolveGlobal environment = \case
<*> lowerFormulaWith allowQuantified
resolveGlobal environment right
Atomic _location predicate arguments ->
- lowerApplication
+ lowerPredicateApplication
resolveGlobal
environment
(SymbolPredicate predicate)
@@ -3783,6 +4463,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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 08:43:00 +0000