diff options
Diffstat (limited to 'source/Checking.hs')
| -rw-r--r-- | source/Checking.hs | 295 |
1 files changed, 295 insertions, 0 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index 3a50fd7..e94aa3f 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -23,6 +23,7 @@ import Checking.Obligation import Checking.Structure qualified as Structure import Checking.Transition qualified as Transition import Checking.Typed.Atomic qualified as TypedAtomic +import Checking.Typed.Inductive qualified as TypedInductive import Checking.Typed.Reflexivity qualified as TypedReflexivity import StructGraph import Syntax.Internal @@ -444,6 +445,7 @@ builtinReservedMixfixMarkers :: Set Marker builtinReservedMixfixMarkers = Set.fromList [ "cons" + , "cumul" , "emptyset" , "naturals" , "pair" @@ -3139,6 +3141,22 @@ checkInductive context inductive = do (SymbolMixfix (inductiveSymbol inductive)) st) checked <- normalizeInductive inductive + case checkingTransitionModuleBuilder st of + Nothing -> + checkLegacyInductive context checked st + Just builder -> + checkTypedInductive + context + checked + builder + st + +checkLegacyInductive + :: BlockContext + -> CheckedInductive + -> CheckingState + -> Checking +checkLegacyInductive context checked st = do soundnessGoals <- traverse canonicalize (inductiveSoundnessGoals checked) stagedFacts <- @@ -3175,6 +3193,283 @@ checkInductive context inductive = do <$> inductiveFactRoles checked ) +checkTypedInductive + :: BlockContext + -> CheckedInductive + -> Transition.TransitionModuleBuilder + -> CheckingState + -> Checking +checkTypedInductive context checked builder st = do + direct <- + either + throwIO + pure + (directInductive context checked) + prepared <- + either + ( throwIO + . typedInductiveError + context + "typed inductive preparation failed: " + ) + pure + (TypedInductive.prepareTypedInductive + (Transition.transitionBuilderFoundation + builder) + (typedSourceGlobal builder) + (blockContextMarker context) + direct) + imports <- + Vector.fromList + <$> traverse + (uncurry + (typedInductiveGuardImport + context + builder)) + (zip + [1 :: Int ..] + (Vector.toList + (TypedInductive.typedInductiveGuardTargets + prepared))) + builderWithCarrier <- + either + ( throwIO + . typedInductiveError + context + "typed inductive carrier registration failed: " + ) + pure + (Transition.commitTransitionTransparentGlobal + (SymbolMixfix + (checkedInductiveSymbol checked)) + (TypedInductive.typedInductiveCarrierType + prepared) + (TypedInductive.typedInductiveCarrierBody + prepared) + (typedFactOrigin context) + builder) + builder' <- + foldM + (commitTypedInductiveFact + context + imports) + builderWithCarrier + (TypedInductive.typedInductiveFacts + prepared) + committed <- + either + throwIO + pure + (commitTypedInductiveState + context + checked + (TypedInductive.typedInductiveFactMarker + <$> TypedInductive.typedInductiveFacts + prepared) + builder' + st) + putDeclarationCandidate committed + setDeclarationFactProducers [] + +directInductive + :: BlockContext + -> CheckedInductive + -> Either CheckingError TypedInductive.DirectInductive +directInductive context checked = + TypedInductive.DirectInductive + (checkedInductiveParams checked) + (checkedInductiveDomain checked) + <$> traverse directClause + (checkedInductiveIntros checked) + where + directClause intro = + TypedInductive.DirectInductiveClause + (checkedInductiveIntroVars intro) + <$> traverse directCondition + (checkedInductiveIntroConditions intro) + <*> pure + (checkedInductiveIntroResultTerm intro) + + directCondition = \case + CheckedInductiveSideCondition formula -> + Right + (TypedInductive.DirectSideCondition + formula) + CheckedInductiveRecursiveCondition + { checkedInductiveRecursiveTerm + , checkedInductiveRecursiveDirect = True + } -> + Right + (TypedInductive.DirectRecursiveCondition + checkedInductiveRecursiveTerm) + CheckedInductiveRecursiveCondition{} -> + Left + (checkingErrorAt context + "nested inductive recursion is not supported by the typed set-valued inductive slice") + +typedSourceGlobal + :: Transition.TransitionModuleBuilder + -> Symbol + -> Maybe TypedInductive.SourceGlobal +typedSourceGlobal builder symbol = do + reference <- + Transition.lookupTransitionGlobal + symbol + builder + pure + (TypedInductive.SourceGlobal + reference + (Transition.lookupTransitionGlobalBody + symbol + builder)) + +typedInductiveGuardImport + :: BlockContext + -> Transition.TransitionModuleBuilder + -> Int + -> Core.FrozenCheckedCore + Transition.CheckedGlobalRef + -> CheckingM Transition.TransitionDerivationImport +typedInductiveGuardImport + context + builder + ordinal + target = do + found <- + either + ( throwIO + . typedInductiveError + context + "typed inductive guard lookup failed: " + ) + pure + (Transition.lookupTransitionTypedImport + target + builder) + maybe + (throwIO + (checkingErrorAt context + ( "typed inductive domain guard " + <> Text.pack (show ordinal) + <> " has no authorized typed fact" + ))) + pure + found + +commitTypedInductiveFact + :: BlockContext + -> Vector Transition.TransitionDerivationImport + -> Transition.TransitionModuleBuilder + -> TypedInductive.PreparedTypedInductiveFact + -> CheckingM Transition.TransitionModuleBuilder +commitTypedInductiveFact context imports builder fact = do + admitted <- + either + ( throwIO + . typedInductiveError + context + "typed inductive replay failed: " + ) + pure + (Transition.authorizeTransitionKernelFactWithImports + imports + (TypedInductive.typedInductiveFactTarget + fact) + (TypedInductive.typedInductiveFactDerivation + fact) + builder) + either + ( throwIO + . typedInductiveError + context + "typed inductive fact registration failed: " + ) + pure + (Transition.commitTransitionTypedFact + (TypedInductive.typedInductiveFactMarker + fact + :| []) + (typedFactOrigin context) + admitted + builder) + +commitTypedInductiveState + :: BlockContext + -> CheckedInductive + -> NonEmpty Marker + -> Transition.TransitionModuleBuilder + -> CheckingState + -> Either CheckingError CheckingState +commitTypedInductiveState + context + checked + factMarkers + builder + st = do + markers' <- + validatedMarkers + location + (marker : NonEmpty.toList factMarkers) + st + (owners', ownedMarkers', dependencies') <- + validatedSymbolRegistration + context + OwnedByInductiveDefinition + carrier + mempty + st + frozenSymbols <- + first + ( checkingErrorAt context + . ("inductive specification mentions unknown symbol " <>) + . symbolText + ) + (checkedInductiveFrozenSymbols + dependencies' + checked) + let frozen = + HM.fromList + [ (symbol, marker) + | symbol <- Set.toList frozenSymbols + , ownableSymbol symbol + ] + pure + st + { checkingDependencies = dependencies' + , checkingOwnedSymbols = owners' + , checkingOwnedSymbolMarkers = ownedMarkers' + , checkingFrozenSymbols = + HM.union + (checkingFrozenSymbols st) + frozen + , definedMarkers = markers' + , blockLabel = marker + , stepLocation = location + , checkingHypothesisCounter = 0 + , checkingTransitionModuleBuilder = + Just builder + } + where + location = + blockContextLocation context + marker = + blockContextMarker context + carrier = + SymbolMixfix + (checkedInductiveSymbol checked) + +typedInductiveError + :: Show error + => BlockContext + -> Text + -> error + -> CheckingError +typedInductiveError context prefix = + checkingErrorAt context + . (prefix <>) + . Text.pack + . show + validateInductiveHeader :: BlockContext -> Symbol |