Pantograph/Library.lean

@@ -116,17 +116,9 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Arr
   liftExcept e
 
 @[export pantograph_goal_start_expr_m]
-def goalStartExpr (expr: String) (levels: Array String): Protocol.FallibleT CoreM GoalState := do
-  let e : Except Protocol.InteractionError _ ← runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
-    let expr ← match ← parseElabType expr |>.run with
-      | .error e => return .error e
-      | .ok expr => pure $ expr
-    return .ok $ .ok $ ← GoalState.create expr
-  liftExcept e
-
-@[export pantograph_goal_resume]
-def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
-  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
+def goalStartExpr (expr: String) : Protocol.FallibleT Elab.TermElabM GoalState := do
+  let t ← parseElabType expr
+  GoalState.create t
 
 @[export pantograph_goal_serialize_m]
 def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
@@ -164,48 +156,27 @@ def goalPrint (state: GoalState) (rootExpr: Bool) (parentExpr: Bool) (goals: Boo
     extraMVars,
   }
 
-@[export pantograph_goal_tactic_m]
-def goalTactic (state: GoalState) (goal:  MVarId) (tactic: String): CoreM TacticResult :=
-  runTermElabM <| state.tryTactic goal tactic
-@[export pantograph_goal_assign_m]
-def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
-  runTermElabM <| state.tryAssign goal expr
 @[export pantograph_goal_have_m]
-protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
+protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): Elab.TermElabM TacticResult := do
   let type ← match (← parseTermM type) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
   state.restoreElabM
   state.tryTacticM goal $ Tactic.evalHave binderName.toName type
 @[export pantograph_goal_try_define_m]
-protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
   state.restoreElabM
   state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
 @[export pantograph_goal_try_draft_m]
-protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult := do
+protected def GoalState.tryDraft (state: GoalState) (goal: MVarId) (expr: String): Elab.TermElabM TacticResult := do
   let expr ← match (← parseTermM expr) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  runTermElabM do
   state.restoreElabM
   state.tryTacticM goal (Tactic.evalDraft expr)
-@[export pantograph_goal_let_m]
-def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
-  runTermElabM <| state.tryLet goal binderName type
-@[export pantograph_goal_conv_m]
-def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
-  runTermElabM <| state.conv goal
-@[export pantograph_goal_conv_exit_m]
-def goalConvExit (state: GoalState): CoreM TacticResult :=
-  runTermElabM <| state.convExit
-@[export pantograph_goal_calc_m]
-def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
-  runTermElabM <| state.tryCalc goal pred
 
 -- Cancel the token after a timeout.
 @[export pantograph_run_cancel_token_with_timeout_m]

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,16 @@ 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 α) (levelNames : List Name := [])
+    : EMainM α := do
+  let scope := (← get).scope
+  let context := {
+    isNoncomputableSection := scope.isNoncomputable,
+  }
+  let state := {
+    levelNames := scope.levelNames ++ levelNames,
+  }
+  runCoreM $ termElabM.run' context state |>.run'
 
 section Frontend
 
@@ -227,7 +236,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 +247,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
@@ -260,14 +269,16 @@ def execute (command: Protocol.Command): MainM Json := do
   options_print (_: Protocol.OptionsPrint): EMainM Protocol.Options := 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
+    let levelNames := (args.levels?.getD #[]).toList.map (·.toName)
+    let expr?: Except _ GoalState ← liftTermElabM (levelNames := levelNames) do
+      match args.expr, args.copyFrom with
+      | .some expr, .none => goalStartExpr expr |>.run
       | .none, .some copyFrom => do
         (match (← getEnv).find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok (← GoalState.create cInfo.type))
       | _, _ =>
-        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied"
     match expr? with
     | .error error => Protocol.throw error
     | .ok goalState =>
@@ -341,7 +352,8 @@ def execute (command: Protocol.Command): MainM Json := do
         | .none => Protocol.throw $ errorIndex s!"Invalid state index {branchId}"
         | .some branch => pure $ target.continue branch
       | .none, .some goals =>
-        pure $ goalResume target goals
+        let goals := goals.toList.map (λ n => { name := n.toName })
+        pure $ target.resume goals
       | _, _ => Protocol.throw $ errorI "arguments" "Exactly one of {branch, goals} must be supplied"
     match nextGoalState? with
     | .error error => Protocol.throw $ errorI "structure" error

Test/Environment.lean

@@ -114,12 +114,20 @@ def test_symbol_location : TestT IO Unit := do
     checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"]
     checkTrue "constNames" $ constNames.contains "Nat.succ_add"
 
+def test_matcher : TestT IO Unit := do
+  let env: Environment ← importModules
+    (imports := #[`Init])
+    (opts := {})
+    (trustLevel := 1)
+  checkTrue "not matcher" $ ¬ Meta.isMatcherCore env `Nat.strongRecOn
+
 def suite: List (String × IO LSpec.TestSeq) :=
   [
     ("Catalog", test_catalog),
     ("Symbol Visibility", test_symbol_visibility),
     ("Inspect", test_inspect),
     ("Symbol Location", runTest test_symbol_location),
+    ("Matcher", runTest test_matcher),
   ]
 
 end Pantograph.Test.Environment

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 := 3, root := "_uniq.5" }: Protocol.GoalStartResult),
   ]
 
 def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do