refactor: Optional levels

Pantograph/Protocol.lean

@@ -107,7 +107,7 @@ structure ExprEcho where
   expr: String
   type?: Option String := .none
   -- universe levels
-  levels: Option (Array String) := .none
+  levels?: Option (Array String) := .none
   deriving Lean.FromJson
 structure ExprEchoResult where
   expr: Expression
@@ -204,7 +204,7 @@ structure EnvInspectResult where
 
 structure EnvAdd where
   name: String
-  levels: Array String := #[]
+  levels?: Option (Array String) := .none
   type?: Option String := .none
   value: String
   isTheorem: Bool := false
@@ -239,7 +239,7 @@ structure GoalStart where
   -- Only one of the fields below may be populated.
   expr: Option String     -- Directly parse in an expression
   -- universe levels
-  levels: Option (Array String) := .none
+  levels?: Option (Array String) := .none
   copyFrom: Option String := .none -- Copy the type from a theorem in the environment
   deriving Lean.FromJson
 structure GoalStartResult where

Repl.lean

@@ -45,9 +45,10 @@ def runCoreM { α } (coreM : CoreM α) : EMainM α := do
     | _ => .some <$> IO.CancelToken.new
   let coreCtx : Core.Context := {
     (← read).coreContext with
-    currNamespace      := scope.currNamespace
-    openDecls          := scope.openDecls
-    options            := scope.opts
+    currNamespace      := scope.currNamespace,
+    openDecls          := scope.openDecls,
+    options            := scope.opts,
+    initHeartbeats     :=  ← IO.getNumHeartbeats,
     cancelTk?,
   }
   let coreState : Core.State := {
@@ -76,8 +77,15 @@ def runCoreM' { α } (coreM : Protocol.FallibleT CoreM α) : EMainM α := do
 
 def liftMetaM { α } (metaM : MetaM α): EMainM α :=
   runCoreM metaM.run'
-def liftTermElabM { α } (termElabM: Elab.TermElabM α) : EMainM α :=
-  runCoreM $ termElabM.run' (ctx := defaultElabContext) |>.run'
+def liftTermElabM { α } (termElabM: Elab.TermElabM α) : EMainM α := do
+  let scope := (← get).scope
+  let context := {
+    isNoncomputableSection := scope.isNoncomputable,
+  }
+  let state := {
+    levelNames := scope.levelNames,
+  }
+  runCoreM $ termElabM.run' context state |>.run'
 
 section Frontend
 
@@ -227,7 +235,7 @@ def execute (command: Protocol.Command): MainM Json := do
     let state ← getMainState
     runCoreM' $ Environment.inspect args state.options
   env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
-    runCoreM' $ Environment.addDecl args.name args.levels args.type? args.value args.isTheorem
+    runCoreM' $ Environment.addDecl args.name (args.levels?.getD #[]) args.type? args.value args.isTheorem
   env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
     let env ← MonadEnv.getEnv
     environmentPickle env args.path
@@ -238,7 +246,7 @@ def execute (command: Protocol.Command): MainM Json := do
     return {}
   expr_echo (args: Protocol.ExprEcho): EMainM Protocol.ExprEchoResult := do
     let state ← getMainState
-    runCoreM' $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
+    runCoreM' $ exprEcho args.expr (expectedType? := args.type?) (levels := args.levels?.getD #[]) (options := state.options)
   options_set (args: Protocol.OptionsSet): EMainM Protocol.OptionsSetResult := do
     let state ← getMainState
     let options := state.options
@@ -261,7 +269,7 @@ def execute (command: Protocol.Command): MainM Json := do
     return (← getMainState).options
   goal_start (args: Protocol.GoalStart): EMainM Protocol.GoalStartResult := do
     let expr?: Except _ GoalState ← liftTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none => goalStartExpr expr (args.levels.getD #[]) |>.run
+      | .some expr, .none => goalStartExpr expr (args.levels?.getD #[]) |>.run
       | .none, .some copyFrom => do
         (match (← getEnv).find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"

Test/Integration.lean

@@ -30,7 +30,7 @@ abbrev Test := List (MainM LSpec.TestSeq)
 def test_expr_echo : Test :=
   [
     step "expr.echo"
-     ({ expr := "λ {α : Sort (u + 1)} => List α", levels := .some #["u"]}: Protocol.ExprEcho)
+     ({ expr := "λ {α : Sort (u + 1)} => List α", levels? := .some #["u"]}: Protocol.ExprEcho)
      ({
        type := { pp? := .some "{α : Type u} → Type u" },
        expr := { pp? := .some "fun {α} => List α" }
@@ -194,7 +194,7 @@ def test_env_add_inspect : Test :=
     step "env.add"
       ({
         name := name3,
-        levels := #["u"]
+        levels? := .some #["u"]
         type? := "(α : Type u) → α → (α × α)",
         value := "λ (α : Type u) (x : α) => (x, x)",
         isTheorem := false
@@ -273,7 +273,7 @@ def test_frontend_process_sorry : Test :=
   ]
 
 def test_import_open : Test :=
-  let header := "import Init\nopen Nat"
+  let header := "import Init\nopen Nat\nuniverse u"
   let goal1: Protocol.Goal := {
     name := "_uniq.67",
     target := { pp? := .some "n + 1 = n.succ" },
@@ -287,9 +287,10 @@ def test_import_open : Test :=
         inheritEnv := true,
       }: Protocol.FrontendProcess)
      ({
-       units := [{
-         boundary := (12, header.utf8ByteSize),
-       }],
+       units := [
+         { boundary := (12, 21) },
+         { boundary := (21, header.utf8ByteSize) },
+       ],
      }: Protocol.FrontendProcessResult),
     step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart)
      ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
@@ -297,6 +298,8 @@ def test_import_open : Test :=
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
     step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic)
      ({ nextStateId? := .some 2, goals? := .some #[], }: Protocol.GoalTacticResult),
+    step "goal.start" ({ expr := "∀ (x : Sort u), Sort (u + 1)"} : Protocol.GoalStart)
+     ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult),
   ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do