diff options
Diffstat (limited to 'source/Checking/Exact')
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 272 |
1 files changed, 211 insertions, 61 deletions
diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs index 40911b0..f3f3b9d 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Checking/Exact/Proof.hs @@ -56,8 +56,6 @@ import Numeric.Natural (Natural) data ExactProofError = ExactProofUnsupportedClaim !Location | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location | ExactProofSetInductionVariableRequired !Location | ExactProofSetInductionVariableNotActive !Location !Raw.VarSymbol @@ -86,8 +84,6 @@ exactProofErrorLocation :: ExactProofError -> Location exactProofErrorLocation = \case ExactProofUnsupportedClaim location -> location ExactProofUnsupportedStep location -> location - ExactProofBoundedFixNotSupported location -> location - ExactProofBoundedTakeNotSupported location -> location ExactProofSetInductionVariableRequired location -> location ExactProofSetInductionVariableNotActive location _variable -> location @@ -115,10 +111,6 @@ renderExactProofError = \case at location <> "this claim is not yet supported by the typed checker" ExactProofUnsupportedStep location -> at location <> "this proof step is not yet supported by the typed checker" - ExactProofBoundedFixNotSupported location -> - at location <> "bounded proof binders are not yet supported" - ExactProofBoundedTakeNotSupported location -> - at location <> "bounded proof witnesses are not yet supported" ExactProofSetInductionVariableRequired location -> at location <> "exact set induction requires a named set variable" ExactProofSetInductionVariableNotActive location variable -> @@ -485,34 +477,47 @@ prepareProof fallback context locals inductionAntecedents goal = \case goal justification Raw.FixSymbolic location variables bound continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedFixNotSupported location)) (context', goal', identities) <- openFixedVariables context goal variables - PreparedFix identities - <$> prepareProof - fallback - context' - locals - Nothing - goal' - continuation + case bound of + Raw.Unbounded -> + PreparedFix identities + <$> prepareProof + fallback + context' + locals + Nothing + goal' + continuation + _ -> do + constraint <- + prepareSymbolicBoundConstraints + context' variables bound + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation + Raw.FixSuchThat location variables statement continuation -> do + (context', goal', identities) <- + openFixedVariables context goal variables + constraint <- + Exact.preparedExactPropositionCore + <$> prepareStatement context' statement + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation Raw.Assume location statement continuation -> do - (antecedent, conclusion) <- + supplied <- prepareStatement context statement + when (isNothing (openScopedImplication goal)) + (throwProof (ExactProofExpectedImplicationGoal location)) + (assumption, conclusion) <- maybe - (throwProof - (ExactProofExpectedImplicationGoal location)) + (throwProof (ExactProofGoalStatementMismatch location)) pure - (openScopedImplication goal) - supplied <- prepareStatement context statement - unless - (Exact.preparedExactPropositionCore supplied - == antecedent) - (throwProof - (ExactProofGoalStatementMismatch location)) - local <- allocateLocal ExactAssumption context antecedent - PreparedAssume antecedent + (openScopedAssumption + (Exact.preparedExactPropositionCore supplied) + goal) + local <- allocateLocal ExactAssumption context assumption + PreparedAssume assumption <$> prepareProof fallback context @@ -521,36 +526,13 @@ prepareProof fallback context locals inductionAntecedents goal = \case conclusion continuation Raw.TakeVar location variables bound statement justification continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedTakeNotSupported location)) - identities <- - traverse (const allocateLocalIdentity) variables - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - (NonEmpty.zip identities variables) - context) - witness <- - Exact.preparedExactPropositionCore - <$> prepareStatement context' statement - let witnessCount = length (toList variables) - existence = closeTakenWitnesses witnessCount witness - goal' = weakenForTakenWitnesses witnessCount goal - discharge <- - prepareDischarge - location context locals existence justification - local <- allocateLocal ExactAssumption context' witness - PreparedTake (toList identities) witness discharge - <$> prepareProof - fallback - context' - (locals <> [local]) - Nothing - goal' - continuation + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation + Raw.TakeNoun location nounPhrase justification continuation -> + prepareNounTake + fallback location context locals goal nounPhrase + justification continuation Raw.BySetInduction location variable continuation -> case (inductionAntecedents, continuation) of (Nothing, _proof) -> @@ -593,6 +575,12 @@ prepareProof fallback context locals inductionAntecedents goal = \case justification (Just _antecedents, _proof) -> throwProof (ExactProofUnsupportedStep location) + Raw.Have location Nothing + (Raw.SymbolicExists _existential variables bound statement) + justification continuation -> + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation Raw.Have location since statement justification continuation -> do when (isJust since) (throwProof (ExactProofUnsupportedStep location)) @@ -756,6 +744,168 @@ prepareProof fallback context locals inductionAntecedents goal = \case (impossible "an exact claim antecedent changed context") (implyScopedCore antecedent conclusion) +prepareGuardedFix + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedProof +prepareGuardedFix + fallback location context locals goal identities constraint continuation = do + (antecedent, conclusion) <- + maybe + (throwProof (ExactProofExpectedImplicationGoal location)) + pure + (openScopedImplication goal) + unless (constraint == antecedent) + (throwProof (ExactProofGoalStatementMismatch location)) + local <- allocateLocal ExactAssumption context constraint + prepared <- + prepareProof + fallback + context + (locals <> [local]) + Nothing + conclusion + continuation + pure (PreparedFix identities (PreparedAssume constraint prepared)) + +prepareSymbolicBoundConstraints + :: Exact.ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Prepare (ScopedCheckedCore ObjectId) +prepareSymbolicBoundConstraints context variables bound = + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicBoundConstraints + context variables bound) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + +prepareSymbolicTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation = do + identities <- traverse (const allocateLocalIdentity) variables + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicWitnessConstraints + context' variables bound statement) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + (toList identities) witness justification continuation + +prepareNounTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Raw.NounPhrase [] + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareNounTake + fallback location context locals goal nounPhrase + justification continuation = do + (identities, context') <- + case nounPhrase of + Raw.NounPhrase _left _noun variables _right _suchThat -> + case NonEmpty.nonEmpty variables of + Just binders -> do + identities <- + traverse (const allocateLocalIdentity) binders + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities binders) + context) + pure (toList identities, context') + Nothing -> do + identity <- allocateLocalIdentity + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactAnonymousBinderContext + identity context) + pure ([identity], context') + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactNounWitnessConstraints + context' nounPhrase) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + identities witness justification continuation + +prepareTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Exact.ExactBinderContext + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareTake + fallback location context locals goal witnessContext + identities witness justification continuation = do + let witnessCount = length identities + existence = closeTakenWitnesses witnessCount witness + goal' = weakenForTakenWitnesses witnessCount goal + discharge <- + prepareDischarge + location context locals existence justification + local <- allocateLocal ExactAssumption witnessContext witness + PreparedTake identities witness discharge + <$> prepareProof + fallback + witnessContext + (locals <> [local]) + Nothing + goal' + continuation + -- The discharged existential and the opened witness premise are the same -- checked proposition viewed on opposite sides of existential elimination. closeTakenWitnesses |