From 37d890b95097f78a9030cd608fa7adde3caec148 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 31 Jul 2020 12:02:39 +0200 Subject: [PATCH] fix: atoms might need backtracking as well, e.g. in `fieldIdx <|> ident` --- src/Lean/PrettyPrinter/Formatter.lean | 23 +-- tests/lean/PPRoundtrip.lean.expected.out | 186 +++++------------------ 2 files changed, 49 insertions(+), 160 deletions(-) diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 706b11b551..b00d6d9042 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -189,18 +189,23 @@ visitToken stx.getId.toString @[builtinFormatter rawIdent] def rawIdent.formatter := identNoAntiquot.formatter @[builtinFormatter nonReservedSymbol] def nonReservedSymbol.formatter := identNoAntiquot.formatter -def visitAtom : Formatter | p => do +def visitAtom (k : SyntaxNodeKind) : Formatter | p => do stx ← getCur; +when (k != Name.anonymous && k != stx.getKind) $ do { + trace! `PrettyPrinter.format.backtrack ("unexpected node kind '" ++ toString stx.getKind ++ "', expected '" ++ toString k ++ "'"); + -- HACK; see `orelse.formatter` + throw $ Exception.other "BACKTRACK" +}; Syntax.atom _ val ← pure $ stx.getArg 0 | throw $ Exception.other $ "not an atom: " ++ toString stx; goLeft; pure val -@[builtinFormatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom -@[builtinFormatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom -@[builtinFormatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom -@[builtinFormatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom -@[builtinFormatter fieldIdx] def fieldIdx.formatter := visitAtom +@[builtinFormatter charLitNoAntiquot] def charLitNoAntiquot.formatter := visitAtom charLitKind +@[builtinFormatter strLitNoAntiquot] def strLitNoAntiquot.formatter := visitAtom strLitKind +@[builtinFormatter nameLitNoAntiquot] def nameLitNoAntiquot.formatter := visitAtom nameLitKind +@[builtinFormatter numLitNoAntiquot] def numLitNoAntiquot.formatter := visitAtom numLitKind +@[builtinFormatter fieldIdx] def fieldIdx.formatter := visitAtom fieldIdxKind @[builtinFormatter many] def many.formatter : Formatter | p => @@ -246,9 +251,9 @@ visit $ mkApp (p.getArg! 0) (mkConst `sorryAx [levelZero]) @[builtinFormatter checkColGe] def checkColGe.formatter : Formatter | p => pure Format.nil open Lean.Parser.Command -@[builtinFormatter commentBody] def commentBody.formatter := visitAtom -@[builtinFormatter quotedSymbol] def quotedSymbol.formatter := visitAtom -@[builtinFormatter unquotedSymbol] def unquotedSymbol.formatter := visitAtom +@[builtinFormatter commentBody] def commentBody.formatter := visitAtom Name.anonymous +@[builtinFormatter quotedSymbol] def quotedSymbol.formatter := visitAtom quotedSymbolKind +@[builtinFormatter unquotedSymbol] def unquotedSymbol.formatter := visitAtom Name.anonymous end Formatter diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out index 7c23ca06a3..c89452f512 100644 --- a/tests/lean/PPRoundtrip.lean.expected.out +++ b/tests/lean/PPRoundtrip.lean.expected.out @@ -1,151 +1,35 @@ -(Term.prop "Prop") -(Term.type "Type" (null)) -(Term.type "Type" (null)) -(Term.type "Type" (null (Level.num (numLit "1")))) -(Term.type "Type" (null (Level.hole "_"))) -(Term.type "Type" (null (Level.paren "(" (Level.addLit (Level.hole "_") "+" (numLit "2")) ")"))) -(Term.id `Nat (null)) -(Term.app (Term.id `List (null)) (null (Term.id `Nat (null)))) -(Term.app (Term.id `id (null)) (null (Term.id `Nat (null)))) -(Term.app - (Term.id `id (null)) - (null - (Term.paren - "(" - (null - (Term.app - (Term.id `id (null)) - (null (Term.paren "(" (null (Term.app (Term.id `id (null)) (null (Term.id `Nat (null)))) (null)) ")"))) - (null)) - ")"))) -(Term.app (Term.id `List (null)) (null (Term.id `Nat (null)))) -(Term.app (Term.explicit "@" (Term.id `id (null))) (null (Term.type "Type" (null)) (Term.id `Nat (null)))) -(Term.app - (Term.id `List (null (Term.explicitUniv ".{" (null (Level.num (numLit "0"))) "}"))) - (null (Term.id `Nat (null)))) -(Term.app - (Term.id `id (null (Term.explicitUniv ".{" (null (Level.num (numLit "2"))) "}"))) - (null (Term.id `Nat (null)))) -(Term.app - (Term.id `id (null)) - (null - (Term.paren - "(" - (null (Term.app (Term.explicit "@" (Term.id `id (null))) (null (Term.type "Type" (null)) (Term.id `Nat (null)))) (null)) - ")"))) -(Term.fun - "fun" - (null (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")")) - "=>" - (Term.id `a (null))) -(Term.fun - "fun" - (null - (Term.paren - "(" - (null (Term.app (Term.id `a (null)) (null (Term.id `b (null)))) (null (Term.typeAscription ":" (Term.id `Nat (null))))) - ")")) - "=>" - (Term.id `a (null))) -(Term.fun - "fun" - (null - (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")") - (Term.paren "(" (null (Term.id `b (null)) (null (Term.typeAscription ":" (Term.id `Bool (null))))) ")")) - "=>" - (Term.id `a (null))) -(Term.fun - "fun" - (null (Term.implicitBinder "{" (null `a `b) (null ":" (Term.id `Nat (null))) "}")) - "=>" - (Term.id `a (null))) -(Term.app - (Term.id `typeAs (null)) - (null - (Term.paren - "(" - (null - (Term.depArrow - (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}") - "→" - (Term.arrow (Term.id `α (null)) "→" (Term.id `α (null)))) - (null)) - ")") - (Term.fun - "fun" - (null - (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}") - (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")")) - "=>" - (Term.id `a (null))))) -(Term.fun - "fun" - (null - (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}") - (Term.instBinder "[" (null `_inst_1 ":") (Term.app (Term.id `HasToString (null)) (null (Term.id `α (null)))) "]") - (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")")) - "=>" - (Term.app - (Term.explicit "@" (Term.id `HasToString.toString (null))) - (null (Term.id `α (null)) (Term.id `_inst_1 (null)) (Term.id `a (null))))) -(Term.depArrow - (Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type" (null))) (null) ")") - "→" - (Term.id `α (null))) -(Term.depArrow - (Term.explicitBinder "(" (null `α `β) (null ":" (Term.type "Type" (null))) (null) ")") - "→" - (Term.id `α (null))) -(Term.arrow (Term.type "Type" (null)) "→" (Term.arrow (Term.type "Type" (null)) "→" (Term.type "Type" (null)))) -(Term.depArrow - (Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type" (null))) (null) ")") - "→" - (Term.arrow (Term.id `α (null)) "→" (Term.id `α (null)))) -(Term.depArrow - (Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type" (null))) (null) ")") - "→" - (Term.depArrow - (Term.explicitBinder "(" (null `a) (null ":" (Term.id `α (null))) (null) ")") - "→" - (Term.app (Term.id `Eq (null)) (null (Term.id `a (null)) (Term.id `a (null)))))) -(Term.depArrow (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}") "→" (Term.id `α (null))) -(Term.depArrow - (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type" (null))) "}") - "→" - (Term.depArrow - (Term.instBinder "[" (null `_inst_1 ":") (Term.app (Term.id `HasToString (null)) (null (Term.id `α (null)))) "]") - "→" - (Term.id `α (null)))) -(Term.num (numLit "0")) -(Term.num (numLit "1")) -(Term.num (numLit "42")) -(Term.str (strLit "\"hi\"")) -(Term.proj - (Term.paren - "(" - (null (Term.app (Term.id `Prod.mk (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2")))) (null)) - ")") - "." - `fst) -(Term.app - (Term.id `or (null)) - (null - (Term.paren - "(" - (null (Term.app (Term.id `HasLess.Less (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2")))) (null)) - ")") - (Term.id `Bool.true (null)))) -(Term.app - (Term.id `id (null)) - (null - (Term.paren - "(" - (null - (Term.fun - "fun" - (null (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")")) - "=>" - (Term.id `a (null))) - (null)) - ")") - (Term.num (numLit "0")))) +Prop +Type +Type +Type1 +Type_ +Type(_+2) +Nat +ListNat +idNat +id(id(idNat)) +ListNat +@idTypeNat +List.{0}Nat +id.{2}Nat +id(@idTypeNat) +λ(a : Nat)=>a +λ(ab : Nat)=>a +λ(a : Nat)(b : Bool)=>a +λ{ab : Nat}=>a +typeAs({α : Type} → α → α)λ{α : Type}(a : α)=>a +λ{α : Type}[_inst_1 : HasToStringα](a : α)=>@HasToString.toStringα_inst_1a +(α : Type) → α +(αβ : Type) → α +Type → Type → Type +(α : Type) → α → α +(α : Type) → (a : α) → Eqaa +{α : Type} → α +{α : Type} → [_inst_1 : HasToStringα] → α +0 +1 +42 +"hi" +(Prod.mk12).fst +or(HasLess.Less12)Bool.true +id(λ(a : Nat)=>a)0