Add expression binding printing and import Lean

This commit is contained in:
Leni Aniva 2023-05-24 00:54:48 -07:00
parent 58367cef6c
commit fd536da55c
6 changed files with 151 additions and 70 deletions

View File

@ -14,7 +14,7 @@ structure Context where
/-- Stores state of the REPL -/
structure State where
--environments: Array Lean.Environment := #[]
proofTrees: Array Meta.ProofTree := #[]
proofTrees: Array ProofTree := #[]
-- State monad
abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM)
@ -36,8 +36,6 @@ def parse_command (s: String): Except String Command := do
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
def execute (command: Command): Subroutine Lean.Json := do
match command.cmd with
| "catalog" =>
@ -83,8 +81,12 @@ def execute (command: Command): Subroutine Lean.Json := do
let format ← Lean.Meta.ppExpr info.toConstantVal.type
let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
let boundExpr? ← (match info.toConstantVal.type with
| .forallE _ _ _ _ => return .some (← type_expr_to_bound info.toConstantVal.type)
| _ => return Option.none)
return Lean.toJson ({
type := toString format,
boundExpr? := boundExpr?,
module? := module?
}: InspectResult)
proof_start (args: ProofStart): Subroutine Lean.Json := do
@ -92,10 +94,10 @@ def execute (command: Command): Subroutine Lean.Json := do
let env ← Lean.MonadEnv.getEnv
let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with
| .some expr, .none =>
(match Serial.syntax_from_str env expr with
(match syntax_from_str env expr with
| .error str => return .error <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError)
| .ok syn => do
(match (← Meta.syntax_to_expr syn) with
(match (← syntax_to_expr syn) with
| .error str => return .error <| Lean.toJson ({ error := "elab", desc := str }: InteractionError)
| .ok expr => return .ok expr))
| .none, .some copyFrom =>
@ -108,7 +110,7 @@ def execute (command: Command): Subroutine Lean.Json := do
match expr? with
| .error error => return error
| .ok expr =>
let tree ← Meta.ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
let tree ← ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
-- Put the new tree in the environment
let nextTreeId := state.proofTrees.size
set { state with proofTrees := state.proofTrees.push tree }
@ -118,7 +120,7 @@ def execute (command: Command): Subroutine Lean.Json := do
match state.proofTrees.get? args.treeId with
| .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}"
| .some tree =>
let (result, nextTree) ← Meta.ProofTree.execute
let (result, nextTree) ← ProofTree.execute
(stateId := args.stateId)
(goalId := args.goalId.getD 0)
(tactic := args.tactic) |>.run tree
@ -155,12 +157,42 @@ unsafe def loop : Subroutine Unit := do
IO.println <| toString <| ret
loop
namespace Lean
-- This is better than the default version since it handles `.`
def setOptionFromString' (opts : Options) (entry : String) : IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := str_to_name key
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
| DataValue.ofBool _ =>
match val with
| "true" => pure $ opts.setBool key true
| "false" => pure $ opts.setBool key false
| _ => throw $ IO.userError s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw (IO.userError s!"invalid Nat option value '{val}'")
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw (IO.userError s!"invalid Int option value '{val}'")
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")
end Lean
unsafe def main (args: List String): IO Unit := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot)
-- Separate imports and options
let options := args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
let env ← Lean.importModules
(imports := args.map (λ str => { module := str_to_name str, runtimeOnly := false }))
(imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let context: Context := {
@ -169,7 +201,8 @@ unsafe def main (args: List String): IO Unit := do
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
fileMap := { source := "", positions := #[0], lines := #[1] },
options := ← options.foldlM Lean.setOptionFromString' Lean.Options.empty
}
try
let termElabM := loop.run context |>.run' {}

View File

@ -1,6 +1,8 @@
-- All the command input/output structures are stored here
import Lean.Data.Json
import Pantograph.Serial
namespace Pantograph.Commands
structure Command where
@ -30,6 +32,8 @@ structure Inspect where
deriving Lean.FromJson
structure InspectResult where
type: String
-- Decompose the bound expression when the type is forall.
boundExpr?: Option BoundExpression
module?: Option String
deriving Lean.ToJson

View File

@ -7,38 +7,39 @@ import Pantograph.Symbols
The proof state manipulation system
A proof state is launched by providing
1. Environment: `Lean.Environment`
2. Expression: `Lean.Expr`
1. Environment: `Environment`
2. Expression: `Expr`
The expression becomes the first meta variable in the saved tactic state
`Lean.Elab.Tactic.SavedState`.
`Elab.Tactic.SavedState`.
From this point on, any proof which extends
`Lean.Elab.Term.Context` and
`Elab.Term.Context` and
-/
def Lean.MessageLog.getErrorMessages (log : Lean.MessageLog) : Lean.MessageLog :=
{ msgs := log.msgs.filter fun m => match m.severity with | Lean.MessageSeverity.error => true | _ => false }
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
{ msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false }
namespace Pantograph.Meta
namespace Pantograph
open Lean
structure ProofState where
goals : List Lean.MVarId
savedState : Lean.Elab.Tactic.SavedState
goals : List MVarId
savedState : Elab.Tactic.SavedState
parent : Option Nat := none
parentGoalId : Nat := 0
structure ProofTree where
-- All parameters needed to run a `TermElabM` monad
name: Lean.Name
name: Name
-- Set of proof states
states : Array ProofState := #[]
abbrev M := Lean.Elab.TermElabM
abbrev M := Elab.TermElabM
def ProofTree.create (name: Lean.Name) (expr: Lean.Expr): M ProofTree := do
let expr ← Lean.instantiateMVars expr
let goal := (← Lean.Meta.mkFreshExprMVar expr (kind := Lean.MetavarKind.synthetic))
let savedStateMonad: Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.SavedState := Lean.MonadBacktrack.saveState
def ProofTree.create (name: Name) (expr: Expr): M ProofTree := do
let expr ← instantiateMVars expr
let goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic))
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
return {
name := name,
@ -54,42 +55,31 @@ def ProofTree.structure_array (tree: ProofTree): Array String :=
| .none => ""
| .some parent => s!"{parent}.{state.parentGoalId}"
-- Parsing syntax under the environment
def syntax_to_expr (syn: Lean.Syntax): Lean.Elab.TermElabM (Except String Lean.Expr) := do
try
let expr ← Lean.Elab.Term.elabType syn
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
--Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← Lean.instantiateMVars expr
return .ok expr
catch ex => return .error (← ex.toMessageData.toString)
def execute_tactic (state: Lean.Elab.Tactic.SavedState) (goal: Lean.MVarId) (tactic: String) :
M (Except (Array String) (Lean.Elab.Tactic.SavedState × List Lean.MVarId)):= do
let tacticM (stx: Lean.Syntax): Lean.Elab.Tactic.TacticM (Except (Array String) (Lean.Elab.Tactic.SavedState × List Lean.MVarId)) := do
def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: String) :
M (Except (Array String) (Elab.Tactic.SavedState × List MVarId)):= do
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) (Elab.Tactic.SavedState × List MVarId)) := do
state.restore
Lean.Elab.Tactic.setGoals [goal]
Elab.Tactic.setGoals [goal]
try
Lean.Elab.Tactic.evalTactic stx
if (← getThe Lean.Core.State).messages.hasErrors then
let messages := (← getThe Lean.Core.State).messages.getErrorMessages |>.toList.toArray
let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString
Elab.Tactic.evalTactic stx
if (← getThe Core.State).messages.hasErrors then
let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
let errors ← (messages.map Message.data).mapM fun md => md.toString
return .error errors
else
return .ok (← Lean.MonadBacktrack.saveState, ← Lean.Elab.Tactic.getUnsolvedGoals)
return .ok (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
catch exception =>
return .error #[← exception.toMessageData.toString]
match Lean.Parser.runParserCategory
(env := ← Lean.MonadEnv.getEnv)
match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `tactic)
(input := tactic)
(fileName := "<stdin>") with
| Except.error err => return .error #[err]
| Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
def goals_to_string (goals: List Lean.MVarId): M (Array String) := do
let goals ← goals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
def goals_to_string (goals: List MVarId): M (Array String) := do
let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
pure goals.toArray
@ -128,4 +118,4 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P
modify fun s => { s with states := s.states.push proofState }
return .success (.some nextId) (← goals_to_string nextGoals)
end Pantograph.Meta
end Pantograph

View File

@ -1,23 +1,44 @@
/-
All serialisation functions
-/
import Lean
/-
Expression IO
-/
namespace Pantograph.Serial
namespace Pantograph
open Lean
/-- Read a theorem from the environment -/
def expr_from_const (env: Lean.Environment) (name: Lean.Name): Except String Lean.Expr :=
def expr_from_const (env: Environment) (name: Name): Except String Lean.Expr :=
match env.find? name with
| none => throw s!"Symbol not found: {name}"
| some cInfo => return cInfo.type
def syntax_from_str (env: Lean.Environment) (s: String): Except String Lean.Syntax :=
Lean.Parser.runParserCategory
def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory
(env := env)
(catName := `term)
(input := s)
(fileName := "<stdin>")
end Pantograph.Serial
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try
let expr ← Elab.Term.elabType syn
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
-- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
--Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← instantiateMVars expr
return .ok expr
catch ex => return .error (← ex.toMessageData.toString)
structure BoundExpression where
binders: Array (String × String)
target: String
deriving ToJson
def type_expr_to_bound (expr: Expr): MetaM BoundExpression := do
Meta.forallTelescope expr fun arr body => do
let binders ← arr.mapM fun fvar => do
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
return { binders, target := toString (← Meta.ppExpr body) }
end Pantograph

View File

@ -4,15 +4,15 @@ import Pantograph.Serial
namespace Pantograph.Test
open Pantograph
open Lean
inductive Start where
| copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression
abbrev M := Meta.M
abbrev TestM := StateRefT Meta.ProofTree M
abbrev TestM := StateRefT ProofTree M
def start_proof (start: Start): M (LSpec.TestSeq × Option Meta.ProofTree) := do
def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
let env ← Lean.MonadEnv.getEnv
let mut testSeq := LSpec.TestSeq.done
match start with
@ -21,37 +21,37 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option Meta.ProofTree) := do
testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with
| .some cInfo =>
let state ← Meta.ProofTree.create
let state ← ProofTree.create
(name := str_to_name "TestExample")
(expr := cInfo.type)
return (testSeq, Option.some state)
| .none =>
return (testSeq, Option.none)
| .expr expr =>
let syn? := Serial.syntax_from_str env expr
let syn? := syntax_from_str env expr
testSeq := testSeq ++ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return (testSeq, Option.none)
| .ok syn =>
let expr? ← Meta.syntax_to_expr syn
let expr? ← syntax_to_expr syn
testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
return (testSeq, Option.none)
| .ok expr =>
let state ← Meta.ProofTree.create
let state ← ProofTree.create
(name := str_to_name "TestExample")
(expr := expr)
return (testSeq, Option.some state)
deriving instance DecidableEq, Repr for Meta.TacticResult
deriving instance DecidableEq, Repr for TacticResult
def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
(expected: Meta.TacticResult) : TestM LSpec.TestSeq := do
let result: Meta.TacticResult ← Meta.ProofTree.execute stateId goalId tactic
(expected: TacticResult) : TestM LSpec.TestSeq := do
let result: TacticResult ← ProofTree.execute stateId goalId tactic
match expected, result with
| .success (.some i) #[], .success (.some _) goals =>
-- If the goals are omitted but the next state is specified, we imply that

View File

@ -1,10 +1,43 @@
import LSpec
import Pantograph.Serial
import Pantograph.Symbols
namespace Pantograph.Test
open Pantograph
open Lean
deriving instance Repr, DecidableEq for BoundExpression
def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
let cases: List (String × BoundExpression) := [
("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
]
let coreM := cases.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := str_to_name symbol |> env.find? |>.get! |>.type
let test := LSpec.check symbol ((← type_expr_to_bound expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
let coreContext: Core.Context := {
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
}
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a
def test_serial: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return LSpec.group "Serialisation" $
LSpec.test "Symbol parsing" (Lean.Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
end Pantograph.Test