From 6a8048fb976192150109391dce574eff982dd75b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 31 Jul 2020 18:32:09 +0200 Subject: [PATCH] test: formatter: check for round-trip through parser --- tests/lean/PPRoundtrip.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 1cd6399ce8..83be375b5a 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -16,9 +16,12 @@ discard $ liftM $ MetaHasEval.eval env opts do stx' ← liftMetaM stx' $ PrettyPrinter.parenthesizeTerm stx'; f' ← liftMetaM stx' $ PrettyPrinter.formatTerm table stx'; dbgTrace $ toString f'; - e' ← elabTermAndSynthesize stx' none <* throwErrorIfErrors; - unlessM (isDefEq stx e e') $ - throwError stx (fmt "failed to elab round-trip" ++ line ++ fmt e ++ line ++ fmt e') + match Parser.runParserCategory env `term (toString f') "" with + | Except.error e => throwError stx e + | Except.ok stx'' => do + e' ← elabTermAndSynthesize stx'' none <* throwErrorIfErrors; + unlessM (isDefEq stx e e') $ + throwError stx (fmt "failed to round-trip" ++ line ++ fmt e ++ line ++ fmt e') -- #eval check `(?m) -- fails round-trip