diff options
| -rw-r--r-- | source/Checking.hs | 19 | ||||
| -rw-r--r-- | source/Encoding.hs | 1 | ||||
| -rw-r--r-- | source/Test/Unit/Checking.hs | 69 |
3 files changed, 83 insertions, 6 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index ab3f346..e21857c 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -285,6 +285,7 @@ data CheckingError | SetExtensionalityWithTake Location Marker | ProofWithoutPrecedingTheorem Location Marker | CouldNotEliminateHigherOrder FunctionSymbol Term Location Marker + | UnresolvedStructureOperation StructSymbol Location Marker | AmbiguousInductionVar Location Marker | MismatchedSetExt [Formula] Location Marker | MismatchedAssume Formula Formula Location Marker @@ -1085,18 +1086,24 @@ desugarComprehensionsAt context = go pure e e@PropositionalConstant{} -> pure e - e@TermSymbolStruct{} -> - pure e + TermSymbolStruct symbol Nothing -> + throwIO + (UnresolvedStructureOperation + symbol + (blockContextLocation context) + (blockContextMarker context)) + TermSymbolStruct symbol (Just argument) -> + TermSymbolStruct symbol . Just <$> go argument -- Equals _pos e (TermSep x bound scope) -> - pure (desugarSeparation e x bound scope) + go (desugarSeparation e x bound scope) Equals _pos (TermSep x bound scope) e -> - pure (desugarSeparation e x bound scope) + go (desugarSeparation e x bound scope) -- Equals _pos e (ReplaceFun bounds scope cond) -> - pure (makeReplacementIff (F <$> e) bounds scope cond) + go (makeReplacementIff (F <$> e) bounds scope cond) Equals _pos (ReplaceFun bounds scope cond) e -> - pure (makeReplacementIff (F <$> e) bounds scope cond) + go (makeReplacementIff (F <$> e) bounds scope cond) -- Apply e es -> Apply <$> go e <*> traverse go es diff --git a/source/Encoding.hs b/source/Encoding.hs index 3fee51d..fd988de 100644 --- a/source/Encoding.hs +++ b/source/Encoding.hs @@ -307,6 +307,7 @@ encodeExpr :: EncodingEnv -> Expr -> Encode TextBuilder encodeExpr encodingEnv = buildExpr . fmap (encodeFreeVar encodingEnv) where + -- Source tasks reach encoding only after checker canonicalization. buildExpr :: ExprOf EncodedVar -> Encode TextBuilder buildExpr = \case Equals _pos left right -> do diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs index 7a2d61c..4a11bd9 100644 --- a/source/Test/Unit/Checking.hs +++ b/source/Test/Unit/Checking.hs @@ -125,6 +125,41 @@ unitTests = testGroup "Checking" , testCase "struct axioms annotate operations from the same structure" do text <- encodedTasksText structOperationRewriteBlocks assertContains "annotated struct operation in rule" "zf_u0(zf_s1(zf_f0),zf_s0(zf_f0))" text + , testCase "structure terms fail before task encoding" do + unresolved <- + try + (check + WithoutDumpPremselTraining + unresolvedStructOperationBlocks) + :: IO (Either CheckingError [Task]) + case unresolved of + Left + (UnresolvedStructureOperation + actualSymbol + actualLocation + actualMarker) -> do + assertEqual + "structure operation" + fooOp + actualSymbol + assertEqual + "block location" + structureTermErrorLocation + actualLocation + assertEqual + "block marker" + "unresolved_structure_operation" + actualMarker + Left err -> + assertFailure + ("expected unresolved structure operation, got " + <> show err) + Right _ -> + assertFailure + "expected unresolved structure operation to fail" + expectCheckingError + "Nested comprehensions are not supported" + nestedStructComprehensionBlocks , testCase "exact structure claims introduce carrier labels for continuations" do text <- encodedTasksText structClaimIntroducesContextBlocks assertContains "claim continuation carrier" "conjecture,zf_u0(zf_f1,zf_s0(zf_f0))" text @@ -791,6 +826,40 @@ structOperationRewriteBlocks = , BlockProof Nowhere Nowhere (Qed (Just Nowhere) (JustificationRef ("foo_op_rule" :| []))) ] +unresolvedStructOperationBlocks :: [Block] +unresolvedStructOperationBlocks = + [ fooStructBlock "unresolved_structure_definition" [] + , BlockAxiom + structureTermErrorLocation + "unresolved_structure_operation" + (Axiom [] + (TermSymbolStruct fooOp Nothing + `eq` TermSymbolStruct fooOp Nothing)) + ] + +nestedStructComprehensionBlocks :: [Block] +nestedStructComprehensionBlocks = + [ fooStructBlock "nested_structure_definition" [] + , BlockAxiom + structureTermErrorLocation + "nested_structure_comprehension" + (Axiom [] + (nestedOperation `eq` nestedOperation)) + ] + where + nestedOperation = + TermSymbolStruct + fooOp + (Just + (TermSep + "x" + emptySet + (toScope Top))) + +structureTermErrorLocation :: Location +structureTermErrorLocation = + mkLocation (FileId 50) 7 1 + structClaimIntroducesContextBlocks :: [Block] structClaimIntroducesContextBlocks = [ fooStructBlock "foo_claim_struct" [] |