feat: Add definitions and theorems to the environment #41

Merged
aniva merged 9 commits from env/add-decl into dev 2023-12-26 12:41:02 -08:00
6 changed files with 35 additions and 32 deletions
Showing only changes of commit 09f5792d4a - Show all commits

View File

@ -102,12 +102,7 @@ unsafe def main (args: List String): IO Unit := do
options := options options := options
} }
try try
let termElabM := loop.run context |>.run' {} let coreM := loop.run context |>.run' {}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
IO.println "ready." IO.println "ready."
discard <| coreM.toIO coreContext { env := env } discard <| coreM.toIO coreContext { env := env }
catch ex => catch ex =>

View File

@ -16,11 +16,19 @@ structure State where
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
/-- Main state monad for executing commands -/ /-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM` -- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α abbrev CR α := Except Protocol.InteractionError α
def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=
metaM.run'
def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
termElabM.run' (ctx := {
declName? := .none,
errToSorry := false,
}) |>.run'
def execute (command: Protocol.Command): MainM Lean.Json := do def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with
@ -85,8 +93,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .none, .defnInfo _ => info.value? | .none, .defnInfo _ => info.value?
| .none, _ => .none | .none, _ => .none
return .ok { return .ok {
type := ← serialize_expression state.options info.type, type := ← (serialize_expression state.options info.type).run',
value? := ← value?.mapM (λ v => serialize_expression state.options v), value? := ← value?.mapM (λ v => serialize_expression state.options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString), publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug. -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none, typeDependency? := if args.dependency?.getD false then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n) else .none,
@ -129,8 +137,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
match syntax_from_str env args.expr with match syntax_from_str env args.expr with
| .error str => return .error $ errorI "parsing" str | .error str => return .error $ errorI "parsing" str
| .ok syn => do | .ok syn => runTermElabM do
match (← syntax_to_expr syn) with match ← syntax_to_expr syn with
| .error str => return .error $ errorI "elab" str | .error str => return .error $ errorI "elab" str
| .ok expr => do | .ok expr => do
try try
@ -161,24 +169,23 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => | .some expr, .none =>
(match syntax_from_str env expr with (match syntax_from_str env expr with
| .error str => return .error <| errorI "parsing" str | .error str => return .error <| errorI "parsing" str
| .ok syn => do | .ok syn => do
(match (← syntax_to_expr syn) with (match ← syntax_to_expr syn with
| .error str => return .error <| errorI "elab" str | .error str => return .error <| errorI "elab" str
| .ok expr => return .ok expr)) | .ok expr => return .ok (← GoalState.create expr)))
| .none, .some copyFrom => | .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with (match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok cInfo.type) | .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 match expr? with
| .error error => return .error error | .error error => return .error error
| .ok expr => | .ok goalState =>
let goalState ← GoalState.create expr
let stateId := state.nextId let stateId := state.nextId
set { state with set { state with
goalStates := state.goalStates.insert stateId goalState, goalStates := state.goalStates.insert stateId goalState,
@ -192,9 +199,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .some goalState => do | .some goalState => do
let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
| .some tactic, .none => do | .some tactic, .none => do
pure ( Except.ok (← GoalState.execute goalState args.goalId tactic)) pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
| .none, .some expr => do | .none, .some expr => do
pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr)) pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr))
| _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied") | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
match nextGoalState? with match nextGoalState? with
| .error error => return .error error | .error error => return .error error
@ -204,7 +211,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goalStates := state.goalStates.insert state.nextId nextGoalState, goalStates := state.goalStates.insert state.nextId nextGoalState,
nextId := state.nextId + 1, nextId := state.nextId + 1,
} }
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return .ok { return .ok {
nextStateId? := .some nextStateId, nextStateId? := .some nextStateId,
goals? := .some goals, goals? := .some goals,
@ -237,7 +244,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
goalStates := state.goalStates.insert nextStateId nextGoalState, goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1 nextId := state.nextId + 1
} }
let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
return .ok { return .ok {
nextStateId, nextStateId,
goals, goals,
@ -251,7 +258,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
let state ← get let state ← get
match state.goalStates.find? args.stateId with match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}" | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do | .some goalState => runMetaM <| do
goalState.restoreMetaM
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr) let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
return .ok { return .ok {
root?, root?,

View File

@ -51,6 +51,10 @@ protected def GoalState.env (state: GoalState): Environment :=
state.savedState.term.meta.core.env state.savedState.term.meta.core.env
private def GoalState.mvars (state: GoalState): SSet MVarId := private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
state.savedState.term.restore
def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
state.savedState.term.meta.restore
/-- Inner function for executing tactic on goal state -/ /-- Inner function for executing tactic on goal state -/
def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
@ -84,6 +88,7 @@ inductive TacticResult where
/-- Execute tactic on given state -/ /-- Execute tactic on given state -/
protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String): protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
M TacticResult := do M TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure $ goal | .some goal => pure $ goal
| .none => return .indexError goalId | .none => return .indexError goalId
@ -118,6 +123,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
} }
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal | .some goal => pure goal
| .none => return .indexError goalId | .none => return .indexError goalId

View File

@ -26,6 +26,7 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
(fileName := "<stdin>") (fileName := "<stdin>")
/-- Parse a syntax object. May generate additional metavariables! -/
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try try
let expr ← Elab.Term.elabType syn let expr ← Elab.Term.elabType syn
@ -242,8 +243,8 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
of_name (n: Name) := name_to_ast n (sanitize := false) of_name (n: Name) := name_to_ast n (sanitize := false)
protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
state.restoreMetaM
let goals := state.goals.toArray let goals := state.goals.toArray
state.savedState.term.meta.restore
let parentDecl? := parent.bind (λ parentState => let parentDecl? := parent.bind (λ parentState =>
let parentGoal := parentState.goals.get! state.parentGoalId let parentGoal := parentState.goals.get! state.parentGoalId
parentState.mctx.findDecl? parentGoal) parentState.mctx.findDecl? parentGoal)
@ -256,8 +257,8 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt
/-- Print the metavariables in a readable format -/ /-- Print the metavariables in a readable format -/
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
goalState.restoreMetaM
let savedState := goalState.savedState let savedState := goalState.savedState
savedState.term.meta.restore
let goals := savedState.tactic.goals let goals := savedState.tactic.goals
let mctx ← getMCtx let mctx ← getMCtx
let root := goalState.root let root := goalState.root

View File

@ -18,8 +18,6 @@ def test_symbol_visibility (env: Environment): IO LSpec.TestSeq := do
LSpec.TestSeq.append suites test) LSpec.TestSeq.done LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite return suite
def suite: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false })) (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))

View File

@ -33,12 +33,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
let result ← step let result ← step
return suite ++ result) LSpec.TestSeq.done return suite ++ result) LSpec.TestSeq.done
try try
let termElabM := commands.run context |>.run' {} let coreM := commands.run context |>.run' {}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
return Prod.fst $ (← coreM.toIO coreContext { env := env }) return Prod.fst $ (← coreM.toIO coreContext { env := env })
catch ex => catch ex =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false return LSpec.check s!"Uncaught IO exception: {ex.toString}" false