From 11c7045f4bbb91dab26caf3f574e7dc262f3ba46 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Dec 2019 08:17:55 -0800 Subject: [PATCH] feat: add `elabLevel` --- src/Init/Lean/Elab/Level.lean | 85 +++++++++++++++++++++++++++++++++++ src/Init/Lean/Elab/Log.lean | 36 ++++++++------- 2 files changed, 105 insertions(+), 16 deletions(-) create mode 100644 src/Init/Lean/Elab/Level.lean diff --git a/src/Init/Lean/Elab/Level.lean b/src/Init/Lean/Elab/Level.lean new file mode 100644 index 0000000000..3b200766f4 --- /dev/null +++ b/src/Init/Lean/Elab/Level.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2019 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Init.Lean.Meta +import Init.Lean.Elab.Exception +import Init.Lean.Elab.Log + +namespace Lean +namespace Elab +namespace Level + +structure Context := +(fileName : String) +(fileMap : FileMap) +(cmdPos : String.Pos) +(univNames : List Name := []) + +structure State := +(ngen : NameGenerator) +(mctx : MetavarContext) + +abbrev LevelElabM := ReaderT Context (EStateM Exception State) + +instance LevelElabM.MonadLog : MonadPosInfo LevelElabM := +{ getCmdPos := do ctx ← read; pure ctx.cmdPos, + getFileMap := do ctx ← read; pure ctx.fileMap, + getFileName := do ctx ← read; pure ctx.fileName } + +def mkFreshId : LevelElabM Name := do +s ← get; +let id := s.ngen.curr; +modify $ fun s => { ngen := s.ngen.next, .. s }; +pure id + +def mkFreshLevelMVar : LevelElabM Level := do +mvarId ← mkFreshId; +modify $ fun s => { mctx := s.mctx.addLevelMVarDecl mvarId, .. s}; +pure $ mkLevelMVar mvarId + +partial def elabLevel : Syntax → LevelElabM Level +| stx => do + let kind := stx.getKind; + if kind == `Lean.Parser.Level.paren then + elabLevel (stx.getArg 1) + else if kind == `Lean.Parser.Level.max then do + let args := (stx.getArg 1).getArgs; + lvl ← elabLevel args.back; + args.foldrRangeM 0 (args.size - 1) + (fun stx lvl => do + arg ← elabLevel stx; + pure (mkLevelMax lvl arg)) + lvl + else if kind == `Lean.Parser.Level.imax then do + let args := (stx.getArg 1).getArgs; + lvl ← elabLevel args.back; + args.foldrRangeM 0 (args.size - 1) + (fun stx lvl => do + arg ← elabLevel stx; + pure (mkLevelIMax lvl arg)) + lvl + else if kind == `Lean.Parser.Level.hole then do + mkFreshLevelMVar + else if kind == `Lean.Parser.Level.num then do + match (stx.getArg 0).isNatLit? with + | some val => pure (Level.ofNat val) + | none => throwError stx "ill-formed universe level syntax" + else if kind == `Lean.Parser.Level.ident then do + let paramName := stx.getIdAt 0; + ctx ← read; + unless (ctx.univNames.contains paramName) $ throwError stx ("unknown universe level " ++ paramName); + pure $ mkLevelParam paramName + else if kind == `Lean.Parser.Level.addLit then do + lvl ← elabLevel (stx.getArg 0); + match (stx.getArg 2).isNatLit? with + | some val => pure (lvl.addOffset val) + | none => throwError stx "ill-formed universe level syntax" + else + throwError stx "unexpected universe level syntax kind" + +end Level +end Elab +end Lean diff --git a/src/Init/Lean/Elab/Log.lean b/src/Init/Lean/Elab/Log.lean index a7e4c8df74..6e90d44e08 100644 --- a/src/Init/Lean/Elab/Log.lean +++ b/src/Init/Lean/Elab/Log.lean @@ -10,61 +10,65 @@ import Init.Lean.Elab.Exception namespace Lean namespace Elab -class MonadLog (m : Type → Type) := -(logMessage {} : Message → m Unit) +class MonadPosInfo (m : Type → Type) := (getFileMap {} : m FileMap) (getFileName {} : m String) (getCmdPos {} : m String.Pos) -export MonadLog (logMessage getFileMap getFileName getCmdPos) +export MonadPosInfo (getFileMap getFileName getCmdPos) -variables {m : Type → Type} [Monad m] [MonadLog m] +class MonadLog (m : Type → Type) extends MonadPosInfo m := +(logMessage {} : Message → m Unit) -def getPosition (pos : Option String.Pos := none) : m Position := do +export MonadLog (logMessage) + +variables {m : Type → Type} [Monad m] + +def getPosition [MonadPosInfo m] (pos : Option String.Pos := none) : m Position := do fileMap ← getFileMap; cmdPos ← getCmdPos; pure $ fileMap.toPosition (pos.getD cmdPos) -def mkMessageAt (msgData : MessageData) (severity : MessageSeverity) (pos : Option String.Pos := none) : m Message := do +def mkMessageAt [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (pos : Option String.Pos := none) : m Message := do fileMap ← getFileMap; fileName ← getFileName; cmdPos ← getCmdPos; let pos := fileMap.toPosition (pos.getD cmdPos); pure { fileName := fileName, pos := pos, data := msgData, severity := severity } -def getPos (stx : Syntax) : m String.Pos := +def getPos [MonadPosInfo m] (stx : Syntax) : m String.Pos := match stx.getPos with | some p => pure p | none => getCmdPos -def mkMessage (msgData : MessageData) (severity : MessageSeverity) (stx : Syntax) : m Message := do +def mkMessage [MonadPosInfo m] (msgData : MessageData) (severity : MessageSeverity) (stx : Syntax) : m Message := do pos ← getPos stx; mkMessageAt msgData severity pos -def logAt (pos : String.Pos) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do +def logAt [MonadLog m] (pos : String.Pos) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do msg ← mkMessageAt msgData severity pos; logMessage msg -def logInfoAt (pos : String.Pos) (msgData : MessageData) : m Unit := +def logInfoAt [MonadLog m] (pos : String.Pos) (msgData : MessageData) : m Unit := logAt pos MessageSeverity.information msgData -def log (stx : Syntax) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do +def log [MonadLog m] (stx : Syntax) (severity : MessageSeverity) (msgData : MessageData) : m Unit := do pos ← getPos stx; logAt pos severity msgData -def logError (stx : Syntax) (msgData : MessageData) : m Unit := +def logError [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit := log stx MessageSeverity.error msgData -def logWarning (stx : Syntax) (msgData : MessageData) : m Unit := +def logWarning [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit := log stx MessageSeverity.warning msgData -def logInfo (stx : Syntax) (msgData : MessageData) : m Unit := +def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit := log stx MessageSeverity.information msgData -def throwError {α} [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do +def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do msg ← mkMessage msgData MessageSeverity.error ref; throw msg -def throwErrorUsingCmdPos {α} [MonadExcept Exception m] (msgData : MessageData) : m α := do +def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do cmdPos ← getCmdPos; msg ← mkMessageAt msgData MessageSeverity.error cmdPos; throw msg