diff --git a/Main.lean b/Main.lean index d7f936e..bed33bb 100644 --- a/Main.lean +++ b/Main.lean @@ -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 ' = '" - 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 := { diff --git a/Pantograph.lean b/Pantograph.lean index 0984db8..fb4cc41 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -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 diff --git a/Pantograph/Symbol.lean b/Pantograph/Symbol.lean index 81d7deb..fb0ea1d 100644 --- a/Pantograph/Symbol.lean +++ b/Pantograph/Symbol.lean @@ -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" diff --git a/Test/Holes.lean b/Test/Holes.lean index b6647ef..afad4e8 100644 --- a/Test/Holes.lean +++ b/Test/Holes.lean @@ -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 := [ diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 0d5fb4e..8992697 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -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 => diff --git a/Test/Serial.lean b/Test/Serial.lean index dfa3890..c057bfb 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -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))