max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: formatter: check for round-trip through parser

Browse source
This commit is contained in:
Sebastian Ullrich 2020-07-31 18:32:09 +02:00 • committed by Leonardo de Moura
parent e8ca2e3f62
commit 6a8048fb97
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
tests/lean/PPRoundtrip.lean
View file

@ -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') "<input>" 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