feat: add elabLevel

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

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