-
Notifications
You must be signed in to change notification settings - Fork 335
/
Syntax.lean
47 lines (40 loc) · 1.78 KB
/
Syntax.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Data.Format.Macro
import Init.Data.Format.Instances
import Init.Meta
namespace Lean.Syntax
open Std
open Std.Format
private def formatInfo (showInfo : Bool) (info : SourceInfo) (f : Format) : Format :=
match showInfo, info with
| true, SourceInfo.original lead pos trail endPos => f!"{lead}:{pos}:{f}:{endPos}:{trail}"
| true, SourceInfo.synthetic pos endPos => f!"{pos}:{f}:{endPos}"
| _, _ => f
partial def formatStxAux (maxDepth : Option Nat) (showInfo : Bool) : Nat → Syntax → Format
| _, atom info val => formatInfo showInfo info $ format (repr val)
| _, ident info _ val pre => formatInfo showInfo info $ format "`" ++ format val
| _, missing => "<missing>"
| depth, node _ kind args =>
let depth := depth + 1;
if kind == nullKind then
sbracket $
if args.size > 0 && depth > maxDepth.getD depth then
".."
else
joinSep (args.toList.map (formatStxAux maxDepth showInfo depth)) line
else
let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous;
let header := format shorterName;
let body : List Format :=
if args.size > 0 && depth > maxDepth.getD depth then [".."] else args.toList.map (formatStxAux maxDepth showInfo depth);
paren $ joinSep (header :: body) line
def formatStx (stx : Syntax) (maxDepth : Option Nat := none) (showInfo := false) : Format :=
formatStxAux maxDepth showInfo 0 stx
instance : ToFormat (Syntax) := ⟨formatStx⟩
instance : ToString (Syntax) := ⟨@toString Format _ ∘ format⟩
end Lean.Syntax