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

refactor: make all fields of SourceInfo optional

Browse source
This commit is contained in:
Sebastian Ullrich 2020-05-14 18:46:58 +02:00 • committed by Leonardo de Moura
parent 493cbd5582
commit b28eedbd98
7 changed files with 63 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Elab/Syntax.lean
View file

@ -335,7 +335,7 @@ else
def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind;
if k == `Lean.Parser.Command.identPrec then
let info := stx.getHeadInfo;
let info := stx.getHeadInfo.getD {};
let id := (stx.getArg 0).getId;
pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1]
else

2
src/Init/Lean/Elab/SyntheticMVars.lean
View file

@ -27,7 +27,7 @@ when val.hasExprMVar $ throwError ref ("tactic failed, result still contain meta
def runTactic (ref : Syntax) (mvarId : MVarId) (tacticCode : Syntax) : TermElabM Unit := do
modify $ fun s => { mctx := s.mctx.instantiateMVarDeclMVars mvarId, .. s };
remainingGoals ← liftTacticElabM ref mvarId $ do { evalTactic tacticCode; getUnsolvedGoals };
let tailRef := ref.getTailWithInfo.getD ref;
let tailRef := ref.getTailWithPos.getD ref;
unless remainingGoals.isEmpty (reportUnsolvedGoals tailRef remainingGoals);
ensureAssignmentHasNoMVars tailRef mvarId

2
src/Init/Lean/Elab/Tactic/Basic.lean
View file

@ -20,7 +20,7 @@ def goalsToMessageData (goals : List MVarId) : MessageData :=
MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line)
def Term.reportUnsolvedGoals (ref : Syntax) (goals : List MVarId) : TermElabM Unit :=
let tailRef := ref.getTailWithInfo.getD ref;
let tailRef := ref.getTailWithPos.getD ref;
Term.throwError tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
namespace Tactic

12
src/Init/Lean/Parser/Parser.lean
View file

@ -23,7 +23,7 @@ abbrev mkAtom (info : SourceInfo) (val : String) : Syntax :=
Syntax.atom info val
abbrev mkIdent (info : SourceInfo) (rawVal : Substring) (val : Name) : Syntax :=
Syntax.ident (some info) rawVal val []
Syntax.ident info rawVal val []
/- Return character after position `pos` -/
def getNext (input : String) (pos : Nat) : Char :=
@ -639,7 +639,7 @@ let s := whitespace c s;
let wsStopPos := s.pos;
let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos };
let info := { SourceInfo . leading := leading, pos := startPos, trailing := trailing };
s.pushSyntax (mkStxLit n val (some info))
s.pushSyntax (mkStxLit n val info)
def charLitFnAux (startPos : Nat) : ParserFn
| c, s =>
@ -973,8 +973,8 @@ partial def strAux (sym : String) (errorMsg : String) : Nat → ParserFn
def checkTailWs (prev : Syntax) : Bool :=
match prev.getTailInfo with
| some info => info.trailing.stopPos > info.trailing.startPos
| none => false
| some { trailing := some trailing, .. } => trailing.stopPos > trailing.startPos
| _ => false
def checkWsBeforeFn (errorMsg : String) : ParserFn :=
fun c s =>
@ -987,8 +987,8 @@ def checkWsBefore (errorMsg : String) : Parser :=
def checkTailNoWs (prev : Syntax) : Bool :=
match prev.getTailInfo with
| some info => info.trailing.stopPos == info.trailing.startPos
| none => false
| some { trailing := some trailing, .. } => trailing.stopPos == trailing.startPos
| _ => false
private def pickNonNone (stack : Array Syntax) : Syntax :=
match stack.findRev? $ fun stx => !stx.isNone with

12
src/Init/Lean/Parser/Transform.lean
View file

@ -15,12 +15,12 @@ match stx with
let prevArg := newArgs.back;
match prevArg.getTailInfo with
| some info =>
let prevArg := prevArg.setTailInfo info.truncateTrailing;
let prevArg := prevArg.setTailInfo { trailing := none };
let newArgs := newArgs.set! (newArgs.size - 1) prevArg;
let newArgs := newArgs.push (atom info sepTk);
newArgs.push arg
| none =>
let newArgs := newArgs.push (atom none sepTk);
let newArgs := newArgs.push (atom {} sepTk);
newArgs.push arg)
#[args.get! 0]
1;
@ -35,10 +35,10 @@ stx.ifNodeKind `Lean.Parser.Term.paren
else if (body.getArg 1).isNone then
let body := body.getArg 0;
match stx.getArg 2, body.getTailInfo with
| atom (some info) ")", some bodyInfo =>
let bodyInfoTrail := bodyInfo.trailing.toString ++ " "; -- add whithespaces for removed parentheses
let bodyInfoTrail := bodyInfoTrail ++ info.trailing.toString; -- add close paren trailing spaces
body.setTailInfo (some { trailing := bodyInfoTrail.toSubstring, .. bodyInfo })
| atom { trailing := some outer } ")", some bodyInfo@{ trailing := some inner } =>
let bodyInfoTrail := inner.toString ++ " "; -- add whithespaces for removed parentheses
let bodyInfoTrail := bodyInfoTrail ++ outer.toString; -- add close paren trailing spaces
body.setTailInfo { trailing := bodyInfoTrail.toSubstring, .. bodyInfo }
| _, _ => stx.val
else stx.val)
(fun _ => stx)

67
src/Init/Lean/Syntax.lean
View file

@ -11,20 +11,9 @@ import Init.Lean.Data.Format
namespace Lean
namespace SourceInfo
def updateTrailing (info : SourceInfo) (trailing : Substring) : SourceInfo :=
def updateTrailing (info : SourceInfo) (trailing : Option Substring) : SourceInfo :=
{ trailing := trailing, .. info }
def truncateTrailing (info : SourceInfo) : SourceInfo :=
{ trailing := { stopPos := info.trailing.startPos, .. info.trailing }, .. info }
/- Update `info₁.trailing.stopPos` to `info₂.trailing.stopPos` -/
def appendToTrailing (info₁ info₂ : SourceInfo) : SourceInfo :=
{ trailing := { stopPos := info₂.trailing.stopPos, .. info₁.trailing }, .. info₁ }
/- Update `info₁.leading.startPos` to `info₂.leading.startPos` -/
def appendToLeading (info₁ info₂ : SourceInfo) : SourceInfo :=
{ leading := { startPos := info₂.leading.startPos, .. info₁.leading }, .. info₁ }
end SourceInfo
/- Syntax AST -/
@ -140,23 +129,24 @@ def getIdAt (stx : Syntax) (i : Nat) : Name :=
Id.run $ stx.mrewriteBottomUp fn
private def updateInfo : SourceInfo → String.Pos → SourceInfo
| {leading := {str := s, startPos := _, stopPos := _}, pos := pos, trailing := trailing}, last =>
{leading := {str := s, startPos := last, stopPos := pos}, pos := pos, trailing := trailing}
| {leading := some {str := s, startPos := _, stopPos := _}, pos := some pos, trailing := trailing}, last =>
{leading := some {str := s, startPos := last, stopPos := pos}, pos := some pos, trailing := trailing}
| info, _ => info
/- Remark: the State `String.Pos` is the `SourceInfo.trailing.stopPos` of the previous token,
or the beginning of the String. -/
@[inline]
private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
| atom (some info) val => do
| atom info@{trailing := some trail, ..} val => do
last ← get;
set info.trailing.stopPos;
set trail.stopPos;
let newInfo := updateInfo info last;
pure $ some (atom (some newInfo) val)
| ident (some info) rawVal val pre => do
pure $ some (atom newInfo val)
| ident info@{trailing := some trail, ..} rawVal val pre => do
last ← get;
set info.trailing.stopPos;
set trail.stopPos;
let newInfo := updateInfo info last;
pure $ some (ident (some newInfo) rawVal val pre)
pure $ some (ident newInfo rawVal val pre)
| _ => pure none
/-- Set `SourceInfo.leading` according to the trailing stop of the preceding token.
@ -173,9 +163,9 @@ private def updateLeadingAux : Syntax → StateM String.Pos (Option Syntax)
def updateLeading : Syntax → Syntax :=
fun stx => (mreplace updateLeadingAux stx).run' 0
partial def updateTrailing (trailing : Substring) : Syntax → Syntax
| Syntax.atom (some info) val => Syntax.atom (some (info.updateTrailing trailing)) val
| Syntax.ident (some info) rawVal val pre => Syntax.ident (some (info.updateTrailing trailing)) rawVal val pre
partial def updateTrailing (trailing : Option Substring) : Syntax → Syntax
| Syntax.atom info val => Syntax.atom (info.updateTrailing trailing) val
| Syntax.ident info rawVal val pre => Syntax.ident (info.updateTrailing trailing) rawVal val pre
| n@(Syntax.node k args) =>
if args.size == 0 then n
else
@ -186,13 +176,13 @@ partial def updateTrailing (trailing : Substring) : Syntax → Syntax
| s => s
def getPos (stx : Syntax) : Option String.Pos :=
SourceInfo.pos <$> stx.getHeadInfo
stx.getHeadInfo >>= SourceInfo.pos
partial def getTailWithInfo : Syntax → Option Syntax
| stx@(atom (some _) _) => some stx
| stx@(ident (some _) _ _ _) => some stx
| node _ args => args.findSomeRev? getTailWithInfo
| _ => none
partial def getTailWithPos : Syntax → Option Syntax
| stx@(atom { pos := some _, .. } _) => some stx
| stx@(ident { pos := some _, .. } _ _ _) => some stx
| node _ args => args.findSomeRev? getTailWithPos
| _ => none
partial def getTailInfo : Syntax → Option SourceInfo
| atom info _ => info
@ -210,7 +200,7 @@ partial def getTailInfo : Syntax → Option SourceInfo
| some v => some $ a.set! i v
| none => updateLast i
partial def setTailInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
partial def setTailInfoAux (info : SourceInfo) : Syntax → Option Syntax
| atom _ val => some $ atom info val
| ident _ rawVal val pre => some $ ident info rawVal val pre
| node k args =>
@ -219,7 +209,7 @@ partial def setTailInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
| none => none
| stx => none
def setTailInfo (stx : Syntax) (info : Option SourceInfo) : Syntax :=
def setTailInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
match setTailInfoAux info stx with
| some stx => stx
| none => stx
@ -227,7 +217,7 @@ match setTailInfoAux info stx with
def truncateTrailing (stx : Syntax) : Syntax :=
match stx.getTailInfo with
| none => stx
| some info => stx.setTailInfo info.truncateTrailing
| some info => stx.setTailInfo { info with trailing := none }
@[specialize] private partial def updateFirst {α} [Inhabited α] (a : Array α) (f : α → Option α) : Nat → Option (Array α)
| i =>
@ -239,7 +229,7 @@ match stx.getTailInfo with
else
none
partial def setHeadInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
partial def setHeadInfoAux (info : SourceInfo) : Syntax → Option Syntax
| atom _ val => some $ atom info val
| ident _ rawVal val pre => some $ ident info rawVal val pre
| node k args =>
@ -248,7 +238,7 @@ partial def setHeadInfoAux (info : Option SourceInfo) : Syntax → Option Syntax
| noxne => none
| stx => none
def setHeadInfo (stx : Syntax) (info : Option SourceInfo) : Syntax :=
def setHeadInfo (stx : Syntax) (info : SourceInfo) : Syntax :=
match setHeadInfoAux info stx with
| some stx => stx
| none => stx
@ -262,13 +252,12 @@ partial def replaceInfo (info : SourceInfo) : Syntax → Syntax
| node k args => node k $ args.map replaceInfo
| stx => setInfo info stx
private def reprintLeaf : Option SourceInfo → String → String
private def reprintLeaf (info : SourceInfo) (val : String) : String :=
-- no source info => add gracious amounts of whitespace to definitely separate tokens
-- Note that the proper pretty printer does not use this function.
-- The parser as well always produces source info, so round-tripping is still
-- guaranteed.
| none, val => " " ++ val ++ " "
| some info, val => info.leading.toString ++ val ++ info.trailing.toString
(Substring.toString <$> info.leading).getD " " ++ val ++ (Substring.toString <$> info.trailing).getD " "
partial def reprint : Syntax → Option String
| atom info val => reprintLeaf info val
@ -327,14 +316,14 @@ end SyntaxNode
@[export lean_mk_syntax_atom]
def mkSimpleAtom (val : String) : Syntax :=
Syntax.atom none val
Syntax.atom {} val
@[export lean_mk_syntax_list]
def mkListNode (args : Array Syntax) : Syntax :=
Syntax.node nullKind args
def mkAtom (val : String) : Syntax :=
Syntax.atom none val
Syntax.atom {} val
@[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax :=
Syntax.node k args

34
src/Init/LeanInit.lean
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura and Sebastian Ullrich
-/
prelude
import Init.Data.Option.BasicAux
import Init.Data.String.Basic
import Init.Data.Array.Basic
import Init.Data.UInt
@ -161,14 +162,19 @@ abbrev TrailingParserDescr := ParserDescr
/- Syntax -/
/--
Source information of syntax atoms. All information is generally set for unquoted syntax and unset for syntax in
syntax quotations, but syntax transformations might want to invalidate only one side to make the pretty printer
reformat it. In the special case of the delaborator, we also use purely synthetic position information without
whitespace information. -/
structure SourceInfo :=
/- Will be inferred after parsing by `Syntax.updateLeading`. During parsing,
it is not at all clear what the preceding token was, especially with backtracking. -/
(leading : Substring)
(pos : String.Pos)
(trailing : Substring)
(leading : Option Substring := none)
(pos : Option String.Pos := none)
(trailing : Option Substring := none)
instance SourceInfo.inhabited : Inhabited SourceInfo := ⟨⟨"".toSubstring, arbitrary _, "".toSubstring⟩⟩
instance SourceInfo.inhabited : Inhabited SourceInfo := ⟨{}⟩
abbrev SyntaxNodeKind := Name
@ -177,8 +183,8 @@ abbrev SyntaxNodeKind := Name
inductive Syntax
| missing : Syntax
| node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
| atom (info : Option SourceInfo) (val : String) : Syntax
| ident (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
| atom (info : SourceInfo) (val : String) : Syntax
| ident (info : SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax
instance Syntax.inhabited : Inhabited Syntax :=
⟨Syntax.missing⟩
@ -412,7 +418,7 @@ abbrev Macro := Syntax → MacroM Syntax
Create an identifier using `SourceInfo` from `src`.
To refer to a specific constant, use `mkCIdentFrom` instead. -/
def mkIdentFrom (src : Syntax) (val : Name) : Syntax :=
let info := src.getHeadInfo;
let info := src.getHeadInfo.getD {};
Syntax.ident info (toString val).toSubstring val []
/--
@ -420,13 +426,13 @@ Syntax.ident info (toString val).toSubstring val []
This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally
be captured. -/
def mkCIdentFrom (src : Syntax) (c : Name) : Syntax :=
let info := src.getHeadInfo;
let info := src.getHeadInfo.getD {};
-- Remark: We use the reserved macro scope to make sure there are no accidental collision with our frontend
let id := addMacroScope `_internal c reservedMacroScope;
Syntax.ident info (toString id).toSubstring id [(c, [])]
def mkAtomFrom (src : Syntax) (val : String) : Syntax :=
let info := src.getHeadInfo;
let info := src.getHeadInfo.getD {};
Syntax.atom info val
def Syntax.identToAtom (stx : Syntax) : Syntax :=
@ -436,7 +442,7 @@ match stx with
@[export lean_mk_syntax_ident]
def mkIdent (val : Name) : Syntax :=
Syntax.ident none (toString val).toSubstring val []
Syntax.ident {} (toString val).toSubstring val []
@[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax :=
Syntax.node nullKind args
@ -488,14 +494,14 @@ mkCTermIdFrom Syntax.missing c
def mkCAppStx (fn : Name) (args : Array Syntax) : Syntax :=
mkAppStx (mkCTermId fn) args
def mkStxLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
def mkStxLit (kind : SyntaxNodeKind) (val : String) (info : SourceInfo := {}) : Syntax :=
let atom : Syntax := Syntax.atom info val;
Syntax.node kind #[atom]
def mkStxStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
def mkStxStrLit (val : String) (info : SourceInfo := {}) : Syntax :=
mkStxLit strLitKind (repr val) info
def mkStxNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
def mkStxNumLit (val : String) (info : SourceInfo := {}) : Syntax :=
mkStxLit numLitKind val info
namespace Syntax
@ -696,7 +702,7 @@ match stx with
def strLitToAtom (stx : Syntax) : Syntax :=
match stx.isStrLit? with
| none => stx
| some val => Syntax.atom stx.getHeadInfo val
| some val => Syntax.atom stx.getHeadInfo.get! val
def isAtom : Syntax → Bool
| atom _ _ => true