feat: Allow selective continuation of goals #27

Merged
aniva merged 14 commits from goal/continuation into dev 2023-11-07 16:49:56 -08:00
6 changed files with 29 additions and 23 deletions
Showing only changes of commit dbace9f2d5 - Show all commits

View File

@ -46,7 +46,7 @@ namespace Lean
def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO Options := do
let ps := (entry.splitOn "=").map String.trim
let [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'"
let key := Pantograph.str_to_name key
let key := key.toName
let defValue ← getOptionDefaultValue key
match defValue with
| DataValue.ofString _ => pure $ opts.setString key val
@ -88,7 +88,7 @@ unsafe def main (args: List String): IO Unit := do
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
let env ← Lean.importModules
(imports := imports.toArray.map (λ str => { module := str_to_name str, runtimeOnly := false }))
(imports := imports.toArray.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let context: Context := {

View File

@ -69,7 +69,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let name := str_to_name args.name
let name := args.name.toName
let info? := env.find? name
match info? with
| none => return .error $ errorIndex s!"Symbol not found {args.name}"
@ -132,7 +132,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .error str => return .error <| errorI "elab" str
| .ok expr => return .ok expr))
| .none, .some copyFrom =>
(match env.find? <| str_to_name copyFrom with
(match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok cInfo.type)
| _, _ =>
@ -182,7 +182,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
let goals := goals.map (λ name => { name := str_to_name name })
let goals := goals.map (λ name => { name := name.toName })
pure $ target.resume goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with

View File

@ -2,10 +2,6 @@ import Lean.Declaration
namespace Pantograph
/-- Converts a symbol of the form `aa.bb.cc` to a name -/
def str_to_name (s: String): Lean.Name :=
(s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
let nameDeduce: Bool := match n.getRoot with
| .str _ name => name.startsWith "_" name == "Lean"

View File

@ -172,6 +172,20 @@ def test_partial_continuation: TestM Unit := do
#[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Roundtrip
--let coupled_goals := coupled_goals.map (λ g =>
-- { name := str_to_name $ name_to_ast g.name (sanitize := false)})
let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false))
let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
let state1b ← match state2.resume (goals := coupled_goals) with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ Nat.succ ?m", .some "Nat.succ ?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Continuation should fail if the state does not exist:
match state0.resume coupled_goals with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
@ -185,7 +199,7 @@ def test_partial_continuation: TestM Unit := do
def suite: IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let tests := [

View File

@ -23,7 +23,7 @@ def startProof (start: Start): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
match start with
| .copy name =>
let cInfo? := str_to_name name |> env.find?
let cInfo? := name.toName |> env.find?
addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with
| .some cInfo =>

View File

@ -9,9 +9,6 @@ open Lean
deriving instance Repr, DecidableEq for Protocol.BoundExpression
def test_str_to_name: LSpec.TestSeq :=
LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
def test_name_to_ast: LSpec.TestSeq :=
let quote := "\""
let escape := "\\"
@ -21,14 +18,14 @@ def test_name_to_ast: LSpec.TestSeq :=
LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × Protocol.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 entries: List (Name × Protocol.BoundExpression) := [
("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
]
let coreM := entries.foldlM (λ suites (symbol, target) => do
let coreM: CoreM LSpec.TestSeq := entries.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)
let expr := env.find? symbol |>.get! |>.type
let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
let coreContext: Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
@ -54,7 +51,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
]
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := str_to_name symbol |> env.find? |>.get! |>.type
let expr := env.find? symbol.toName |>.get! |>.type
let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let coreM := metaM.run'
@ -72,12 +69,11 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return LSpec.group "Serialization" $
(LSpec.group "str_to_name" test_str_to_name) ++
(LSpec.group "name_to_ast" test_name_to_ast) ++
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))