Compare commits

..

53 Commits

Author SHA1 Message Date
Leni Aniva 79a63be619
Merge branch 'dev' into misc/interaction 2023-10-02 10:12:10 -07:00
Leni Aniva fd4d3226a1
Add ready message to indicate the main loop is up 2023-10-01 21:58:58 -07:00
Leni Aniva 1e637dabaa
Bump lean version to 4.0.0 2023-09-13 21:02:26 -07:00
Leni Aniva c4a97d8a76 Merge pull request 'Simplify goal bookkeeping mechanism' (#10) from tactic/book into dev
Reviewed-on: #10
2023-08-30 19:18:36 -07:00
Leni Aniva acfd4e8288
Merge branch 'dev' into tactic/book 2023-08-30 19:17:25 -07:00
Leni Aniva 46347d8244
Add SemihashMap interface, rename proof commands to goal commands, allow deletion 2023-08-30 19:16:33 -07:00
Leni Aniva 71327d2d55
Separate max and imax in sort level 2023-08-27 22:50:18 -07:00
Leni Aniva 8d5d7b6e3e
Version bump to 0.2.4 due to breaking change 2023-08-27 19:59:31 -07:00
Leni Aniva 80ad7a2bd0
Rename proof commands to goal commands 2023-08-27 19:58:52 -07:00
Leni Aniva 0c5f439067
Add SemihashMap structure for goal bookkeeping 2023-08-27 19:53:09 -07:00
Leni Aniva dea63ac5ea Merge pull request 'Remove the obsolete name field from proof tree structure' (#11) from misc/cleanup into dev
Reviewed-on: #11
2023-08-26 18:50:40 -07:00
Leni Aniva 81702d12ef Remove the obsolete name field from proof tree structure 2023-08-26 18:50:15 -07:00
Leni Aniva 51edc701fe
Add test cases for command error categories 2023-08-24 23:12:18 -07:00
Leni Aniva 95d26a2f50
Classify JSON error as command error
Also add documentation for this
2023-08-24 22:51:40 -07:00
Leni Aniva 5978e5f4f3 Merge pull request 'Add more serialisation options' (#2) from io/serial into dev
Reviewed-on: #2
2023-08-23 13:29:00 -07:00
Leni Aniva 7160f8aa61
Merge branch 'dev' into io/serial 2023-08-23 13:25:08 -07:00
Leni Aniva 85440e0278
Unify json and unknown error into command error 2023-08-23 13:00:11 -07:00
Leni Aniva e63f7c9afa
Add proper printing of sorts 2023-08-23 12:51:06 -07:00
Leni Aniva 1d1fa60175
Move all json-string functions to Main.lean 2023-08-22 09:54:37 -07:00
Leni Aniva ddf7ec21c8 Add compressed json print option; Rearrange commands into hierarchy 2023-08-16 19:25:32 -07:00
Leni Aniva 0e61093f47 Add proof variable delta; Bump version to 0.2.1 2023-08-15 15:40:54 -07:00
Leni Aniva d476354a4a Add expression sexp printing (2/2) 2023-08-14 21:43:40 -07:00
Leni Aniva 19c57ada1e Add expression sexp printing (1/2, tests pending) 2023-08-14 17:07:53 -07:00
Leni Aniva d705cdf0e5 version bump, restructure 2023-08-13 21:19:06 -07:00
Leni Aniva a00a2b4a42 Add documentation; Remove mathlib dependency 2023-06-09 14:45:45 -07:00
Leni Aniva 572548c1bd Add json goal printing 2023-05-27 23:10:39 -07:00
Leni Aniva 9fe3f62371 Add back the clear command to reset state 2023-05-26 16:55:33 -07:00
Leni Aniva 989130ecd2 Add expr.type 2023-05-25 13:40:03 -07:00
Leni Aniva 5beb911db5 Rename tactic failure mode to avoid confusion
Clean up README
2023-05-24 23:11:17 -07:00
Leni Aniva 9b8aff95e5 Update gitignore to exclude hidden files 2023-05-24 09:32:19 -07:00
Leni Aniva 4033722596 Add documentation about options 2023-05-24 00:55:54 -07:00
Leni Aniva fd536da55c Add expression binding printing and import Lean 2023-05-24 00:54:48 -07:00
Leni Aniva 58367cef6c Use TermElabM as the main monad stack instead of IO 2023-05-23 05:12:46 -07:00
Leni Aniva c781797898 Save core state in proofs 2023-05-22 22:48:48 -07:00
Leni Aniva 44d470d63e Rename ids so they are consistent 2023-05-22 19:51:16 -07:00
Leni Aniva 51477a4806 Remove testing stub in README.md 2023-05-22 19:12:07 -07:00
Leni Aniva 56b967ee7a Add module name for symbol 2023-05-22 16:00:41 -07:00
Leni Aniva 22202af24e Add option id handling with ? 2023-05-22 14:56:43 -07:00
Leni Aniva 111dea2093 Add option format for proof output and test cases 2023-05-22 14:49:56 -07:00
Leni Aniva 8a448fb114 Add testing stub 2023-05-22 11:47:46 -07:00
Leni Aniva 2772a394cc Add default arguments for Json 2023-05-22 00:49:37 -07:00
Leni Aniva 147079816d Add manifest file 2023-05-21 23:30:41 -07:00
Leni Aniva 41241bfa40 Add REPL tactics 2023-05-21 17:41:39 -07:00
Leni Aniva ed70875837 Remove ExceptT from main monad
Allow pretty printing of expr
2023-05-20 15:58:38 -07:00
Leni Aniva c4a1ccad13 Add expression IO stub for constant types 2023-05-20 14:04:09 -07:00
Leni Aniva 65da39440d Add alternative command input format and IO stub 2023-05-20 13:03:12 -07:00
Leni Ven 14a6eb1f59 Add tactic state manipulation 2023-05-17 21:58:03 -07:00
Leni Ven 2ec4efde55 Add stack size troubleshooting 2023-05-14 15:22:41 -07:00
Leni Ven 3cb0795bb6 Add unsafe filtering in catalog 2023-05-12 16:12:21 -07:00
Leni Aniva 9f53781ffe Add working catalog code and example 2023-05-12 01:08:36 -07:00
Leni Ven 5a297e8fef Add README and catalog functions 2023-05-09 22:51:19 -07:00
Leni Aniva 0b2db92b4a Separate commands into its own file 2023-05-09 18:01:09 -07:00
Leni Ven 9a957bce35 Add REPL 2023-05-09 16:39:24 -07:00
47 changed files with 1205 additions and 5699 deletions

1
.gitignore vendored
View File

@ -1,6 +1,5 @@
.*
!.gitignore
*.olean
/build
/lake-packages

190
LICENSE
View File

@ -1,190 +0,0 @@
Apache License
Version 2.0, January 2004
http://www.apache.org/licenses/
TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
1. Definitions.
"License" shall mean the terms and conditions for use, reproduction,
and distribution as defined by Sections 1 through 9 of this document.
"Licensor" shall mean the copyright owner or entity authorized by
the copyright owner that is granting the License.
"Legal Entity" shall mean the union of the acting entity and all
other entities that control, are controlled by, or are under common
control with that entity. For the purposes of this definition,
"control" means (i) the power, direct or indirect, to cause the
direction or management of such entity, whether by contract or
otherwise, or (ii) ownership of fifty percent (50%) or more of the
outstanding shares, or (iii) beneficial ownership of such entity.
"You" (or "Your") shall mean an individual or Legal Entity
exercising permissions granted by this License.
"Source" form shall mean the preferred form for making modifications,
including but not limited to software source code, documentation
source, and configuration files.
"Object" form shall mean any form resulting from mechanical
transformation or translation of a Source form, including but
not limited to compiled object code, generated documentation,
and conversions to other media types.
"Work" shall mean the work of authorship, whether in Source or
Object form, made available under the License, as indicated by a
copyright notice that is included in or attached to the work
(an example is provided in the Appendix below).
"Derivative Works" shall mean any work, whether in Source or Object
form, that is based on (or derived from) the Work and for which the
editorial revisions, annotations, elaborations, or other modifications
represent, as a whole, an original work of authorship. For the purposes
of this License, Derivative Works shall not include works that remain
separable from, or merely link (or bind by name) to the interfaces of,
the Work and Derivative Works thereof.
"Contribution" shall mean any work of authorship, including
the original version of the Work and any modifications or additions
to that Work or Derivative Works thereof, that is intentionally
submitted to Licensor for inclusion in the Work by the copyright owner
or by an individual or Legal Entity authorized to submit on behalf of
the copyright owner. For the purposes of this definition, "submitted"
means any form of electronic, verbal, or written communication sent
to the Licensor or its representatives, including but not limited to
communication on electronic mailing lists, source code control systems,
and issue tracking systems that are managed by, or on behalf of, the
Licensor for the purpose of discussing and improving the Work, but
excluding communication that is conspicuously marked or otherwise
designated in writing by the copyright owner as "Not a Contribution."
"Contributor" shall mean Licensor and any individual or Legal Entity
on behalf of whom a Contribution has been received by Licensor and
subsequently incorporated within the Work.
2. Grant of Copyright License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
copyright license to reproduce, prepare Derivative Works of,
publicly display, publicly perform, sublicense, and distribute the
Work and such Derivative Works in Source or Object form.
3. Grant of Patent License. Subject to the terms and conditions of
this License, each Contributor hereby grants to You a perpetual,
worldwide, non-exclusive, no-charge, royalty-free, irrevocable
(except as stated in this section) patent license to make, have made,
use, offer to sell, sell, import, and otherwise transfer the Work,
where such license applies only to those patent claims licensable
by such Contributor that are necessarily infringed by their
Contribution(s) alone or by combination of their Contribution(s)
with the Work to which such Contribution(s) was submitted. If You
institute patent litigation against any entity (including a
cross-claim or counterclaim in a lawsuit) alleging that the Work
or a Contribution incorporated within the Work constitutes direct
or contributory patent infringement, then any patent licenses
granted to You under this License for that Work shall terminate
as of the date such litigation is filed.
4. Redistribution. You may reproduce and distribute copies of the
Work or Derivative Works thereof in any medium, with or without
modifications, and in Source or Object form, provided that You
meet the following conditions:
(a) You must give any other recipients of the Work or
Derivative Works a copy of this License; and
(b) You must cause any modified files to carry prominent notices
stating that You changed the files; and
(c) You must retain, in the Source form of any Derivative Works
that You distribute, all copyright, patent, trademark, and
attribution notices from the Source form of the Work,
excluding those notices that do not pertain to any part of
the Derivative Works; and
(d) If the Work includes a "NOTICE" text file as part of its
distribution, then any Derivative Works that You distribute must
include a readable copy of the attribution notices contained
within such NOTICE file, excluding those notices that do not
pertain to any part of the Derivative Works, in at least one
of the following places: within a NOTICE text file distributed
as part of the Derivative Works; within the Source form or
documentation, if provided along with the Derivative Works; or,
within a display generated by the Derivative Works, if and
wherever such third-party notices normally appear. The contents
of the NOTICE file are for informational purposes only and
do not modify the License. You may add Your own attribution
notices within Derivative Works that You distribute, alongside
or as an addendum to the NOTICE text from the Work, provided
that such additional attribution notices cannot be construed
as modifying the License.
You may add Your own copyright statement to Your modifications and
may provide additional or different license terms and conditions
for use, reproduction, or distribution of Your modifications, or
for any such Derivative Works as a whole, provided Your use,
reproduction, and distribution of the Work otherwise complies with
the conditions stated in this License.
5. Submission of Contributions. Unless You explicitly state otherwise,
any Contribution intentionally submitted for inclusion in the Work
by You to the Licensor shall be under the terms and conditions of
this License, without any additional terms or conditions.
Notwithstanding the above, nothing herein shall supersede or modify
the terms of any separate license agreement you may have executed
with Licensor regarding such Contributions.
6. Trademarks. This License does not grant permission to use the trade
names, trademarks, service marks, or product names of the Licensor,
except as required for reasonable and customary use in describing the
origin of the Work and reproducing the content of the NOTICE file.
7. Disclaimer of Warranty. Unless required by applicable law or
agreed to in writing, Licensor provides the Work (and each
Contributor provides its Contributions) on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
implied, including, without limitation, any warranties or conditions
of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
PARTICULAR PURPOSE. You are solely responsible for determining the
appropriateness of using or redistributing the Work and assume any
risks associated with Your exercise of permissions under this License.
8. Limitation of Liability. In no event and under no legal theory,
whether in tort (including negligence), contract, or otherwise,
unless required by applicable law (such as deliberate and grossly
negligent acts) or agreed to in writing, shall any Contributor be
liable to You for damages, including any direct, indirect, special,
incidental, or consequential damages of any character arising as a
result of this License or out of the use or inability to use the
Work (including but not limited to damages for loss of goodwill,
work stoppage, computer failure or malfunction, or any and all
other commercial damages or losses), even if such Contributor
has been advised of the possibility of such damages.
9. Accepting Warranty or Additional Liability. While redistributing
the Work or Derivative Works thereof, You may choose to offer,
and charge a fee for, acceptance of support, warranty, indemnity,
or other liability obligations and/or rights consistent with this
License. However, in accepting such obligations, You may act only
on Your own behalf and on Your sole responsibility, not on behalf
of any other Contributor, and only if You agree to indemnify,
defend, and hold each Contributor harmless for any liability
incurred by, or claims asserted against, such Contributor by reason
of your accepting any such warranty or additional liability.
END OF TERMS AND CONDITIONS
Copyright 2024 Leni Aniva
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.

View File

@ -1,15 +1,14 @@
import Lean.Data.Json
import Lean.Environment
import Pantograph.Version
import Pantograph
import Repl
-- Main IO functions
open Pantograph.Repl
open Pantograph.Protocol
open Pantograph
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
def parseCommand (s: String): Except String Command := do
def parse_command (s: String): Except String Commands.Command := do
let s := s.trim
match s.get? 0 with
| .some '{' => -- Parse in Json mode
@ -23,50 +22,94 @@ def parseCommand (s: String): Except String Command := do
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
partial def loop : MainM Unit := do
unsafe def loop : MainM Unit := do
let state ← get
let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return ()
match parseCommand command with
match parse_command command with
| .error error =>
let error := Lean.toJson ({ error := "command", desc := error }: InteractionError)
let error := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
-- Using `Lean.Json.compress` here to prevent newline
IO.println error.compress
| .ok command =>
try
let ret ← execute command
let str := match state.options.printJsonPretty with
| true => ret.pretty
| false => ret.compress
IO.println str
catch e =>
let message ← e.toMessageData.toString
let error := Lean.toJson ({ error := "main", desc := message }: InteractionError)
IO.println error.compress
loop
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
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 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 s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
unsafe def main (args: List String): IO Unit := do
-- NOTE: A more sophisticated scheme of command line argument handling is needed.
-- Separate imports and options
if args == ["--version"] then do
IO.println s!"{Pantograph.version}"
println! s!"{version}"
return
Pantograph.initSearch ""
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot)
let coreContext ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
|>.toArray |> Pantograph.createCoreContext
let options? ← args.filterMap (λ s => if s.startsWith "--" then .some <| s.drop 2 else .none)
|>.foldlM Lean.setOptionFromString' Lean.Options.empty
|>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
let imports:= args.filter (λ s => ¬ (s.startsWith "--"))
let coreState ← Pantograph.createCoreState imports.toArray
let env ← Lean.importModules
(imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let context: Context := {
imports
}
let coreContext: Lean.Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] },
options := options
}
try
let coreM := loop.run context |>.run' {}
let termElabM := loop.run context |>.run' {}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
IO.println "ready."
discard <| coreM.toIO coreContext coreState
discard <| coreM.toIO coreContext { env := env }
catch ex =>
let message := ex.toString
let error := Lean.toJson ({ error := "io", desc := message }: InteractionError)
IO.println error.compress
IO.println "Uncaught IO exception"
IO.println ex.toString

View File

@ -1,8 +1,174 @@
import Pantograph.Condensed
import Pantograph.Environment
import Pantograph.Frontend
import Pantograph.Goal
import Pantograph.Library
import Pantograph.Protocol
import Pantograph.Commands
import Pantograph.Serial
import Pantograph.Version
import Pantograph.Symbols
import Pantograph.Tactic
import Pantograph.SemihashMap
namespace Pantograph
structure Context where
imports: List String
/-- Stores state of the REPL -/
structure State where
options: Commands.Options := {}
goalStates: SemihashMap GoalState := SemihashMap.empty
-- State monad
abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain
-- monadic features in `MainM`
abbrev CR α := Except Commands.InteractionError α
def execute (command: Commands.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with
| .ok args => do
match (← comm args) with
| .ok result => return Lean.toJson result
| .error ierror => return Lean.toJson ierror
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with
| "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo
| "lib.catalog" => run lib_catalog
| "lib.inspect" => run lib_inspect
| "options.set" => run options_set
| "options.print" => run options_print
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.delete" => run goal_delete
| cmd =>
let error: Commands.InteractionError :=
errorCommand s!"Unknown command {cmd}"
return Lean.toJson error
where
errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc }
errorCommand := errorI "command"
errorIndex := errorI "index"
-- Command Functions
reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
set { state with goalStates := SemihashMap.empty }
return .ok { nGoals }
stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
return .ok { nGoals }
lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do
let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with
| .some x => acc.push x
| .none => acc)
return .ok { symbols := names }
lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let name := str_to_name args.name
let info? := env.find? name
match info? with
| none => return .error $ errorIndex s!"Symbol not found {args.name}"
| some info =>
let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
let value? := match args.value?, info with
| .some true, _ => info.value?
| .some false, _ => .none
| .none, .defnInfo _ => info.value?
| .none, _ => .none
return .ok {
type := ← serialize_expression state.options info.type,
value? := ← value?.mapM (λ v => serialize_expression state.options v),
module? := module?
}
expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
match syntax_from_str env args.expr with
| .error str => return .error $ errorI "parsing" str
| .ok syn => do
match (← syntax_to_expr syn) with
| .error str => return .error $ errorI "elab" str
| .ok expr => do
try
let type ← Lean.Meta.inferType expr
return .ok {
type := (← serialize_expression (options := state.options) type),
expr := (← serialize_expression (options := state.options) expr)
}
catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString)
options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do
let state ← get
let options := state.options
set { state with
options := {
-- FIXME: This should be replaced with something more elegant
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST,
proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
}
}
return .ok { }
options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do
return .ok (← get).options
goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
| .some expr, .none =>
(match syntax_from_str env expr with
| .error str => return .error <| errorI "parsing" str
| .ok syn => do
(match (← syntax_to_expr syn) with
| .error str => return .error <| errorI "elab" str
| .ok expr => return .ok expr))
| .none, .some copyFrom =>
(match env.find? <| str_to_name copyFrom with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok cInfo.type)
| .none, .none =>
return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
| _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
match expr? with
| .error error => return .error error
| .ok expr =>
let goalState ← GoalState.create expr
let (goalStates, goalId) := state.goalStates.insert goalState
set { state with goalStates }
return .ok { goalId }
goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do
let state ← get
match state.goalStates.get? args.goalId with
| .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}"
| .some goalState =>
let result ← GoalState.execute goalState args.tactic |>.run state.options
match result with
| .success goals =>
if goals.isEmpty then
return .ok {}
else
-- Append all goals
let (goalStates, goalIds, sGoals) := Array.foldl (λ acc itr =>
let (map, indices, serializedGoals) := acc
let (goalState, sGoal) := itr
let (map, index) := map.insert goalState
(map, index :: indices, sGoal :: serializedGoals)
) (state.goalStates, [], []) goals
set { state with goalStates }
return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray }
| .failure messages =>
return .ok { tacticErrors? := .some messages }
goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do
let state ← get
let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates
set { state with goalStates }
return .ok {}
end Pantograph

163
Pantograph/Commands.lean Normal file
View File

@ -0,0 +1,163 @@
/-
All the command input/output structures are stored here
Note that no command other than `InteractionError` may have `error` as one of
its field names to avoid confusion with error messages generated by the REPL.
-/
import Lean.Data.Json
namespace Pantograph.Commands
/-- Main Option structure, placed here to avoid name collision -/
structure Options where
-- When false, suppress newlines in Json objects. Useful for machine-to-machine interaction.
-- This should be false` by default to avoid any surprises with parsing.
printJsonPretty: Bool := false
-- When enabled, pretty print every expression
printExprPretty: Bool := true
-- When enabled, print the raw AST of expressions
printExprAST: Bool := false
-- When enabled, the types and values of persistent variables in a proof goal
-- are not shown unless they are new to the proof step. Reduces overhead
proofVariableDelta: Bool := false
-- See `pp.auxDecls`
printAuxDecls: Bool := false
-- See `pp.implementationDetailHyps`
printImplementationDetailHyps: Bool := false
deriving Lean.ToJson
abbrev OptionsT := ReaderT Options
--- Expression Objects ---
structure BoundExpression where
binders: Array (String × String)
target: String
deriving Lean.ToJson
structure Expression where
-- Pretty printed expression
pp?: Option String := .none
-- AST structure
sexp?: Option String := .none
deriving Lean.ToJson
structure Variable where
name: String
/-- Does the name contain a dagger -/
isInaccessible?: Option Bool := .none
type?: Option Expression := .none
value?: Option Expression := .none
deriving Lean.ToJson
structure Goal where
/-- String case id -/
caseName?: Option String := .none
/-- Is the goal in conversion mode -/
isConversion: Bool := false
/-- target expression type -/
target: Expression
/-- Variables -/
vars: Array Variable := #[]
deriving Lean.ToJson
--- Individual Commands and return types ---
structure Command where
cmd: String
payload: Lean.Json
deriving Lean.FromJson
structure InteractionError where
error: String
desc: String
deriving Lean.ToJson
--- Individual command and return types ---
structure Reset where
deriving Lean.FromJson
structure Stat where
deriving Lean.FromJson
structure StatResult where
-- Number of goals states
nGoals: Nat
deriving Lean.ToJson
-- Return the type of an expression
structure ExprEcho where
expr: String
deriving Lean.FromJson
structure ExprEchoResult where
expr: Expression
type: Expression
deriving Lean.ToJson
-- Print all symbols in environment
structure LibCatalog where
deriving Lean.FromJson
structure LibCatalogResult where
symbols: Array String
deriving Lean.ToJson
-- Print the type of a symbol
structure LibInspect where
name: String
-- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden.
value?: Option Bool := .some false
deriving Lean.FromJson
structure LibInspectResult where
type: Expression
value?: Option Expression := .none
module?: Option String
deriving Lean.ToJson
/-- Set options; See `Options` struct above for meanings -/
structure OptionsSet where
printJsonPretty?: Option Bool
printExprPretty?: Option Bool
printExprAST?: Option Bool
proofVariableDelta?: Option Bool
printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool
deriving Lean.FromJson
structure OptionsSetResult where
deriving Lean.ToJson
structure OptionsPrint where
deriving Lean.FromJson
abbrev OptionsPrintResult := Options
structure GoalStart where
-- Only one of the fields below may be populated.
expr: Option String -- Proof expression
copyFrom: Option String -- Theorem name
deriving Lean.FromJson
structure GoalStartResult where
goalId: Nat := 0 -- Proof tree id
deriving Lean.ToJson
structure GoalTactic where
-- Identifiers for tree, state, and goal
goalId: Nat
tactic: String
deriving Lean.FromJson
structure GoalTacticResult where
-- Existence of this field shows success
goals?: Option (Array Goal) := .none
-- Next proof state id, if successful
goalIds?: Option (Array Nat) := .none
-- Existence of this field shows failure
tacticErrors?: Option (Array String) := .none
deriving Lean.ToJson
-- Remove a bunch of goals.
structure GoalDelete where
goalIds: List Nat
deriving Lean.FromJson
structure GoalDeleteResult where
deriving Lean.ToJson
end Pantograph.Commands

View File

@ -1,95 +0,0 @@
/- structures for FFI based interface -/
import Lean
import Pantograph.Goal
import Pantograph.Expr
open Lean
namespace Pantograph
namespace Condensed
-- Mirrors Lean's LocalDecl
structure LocalDecl where
-- Default value is for testing
fvarId: FVarId := { name := .anonymous }
userName: Name
-- Normalized expression
type : Expr
value? : Option Expr := .none
structure Goal where
mvarId: MVarId := { name := .anonymous }
userName: Name := .anonymous
context: Array LocalDecl
target: Expr
@[export pantograph_goal_is_lhs]
def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome
-- Functions for creating contexts and states
@[export pantograph_elab_context]
def elabContext: Elab.Term.Context := {
errToSorry := false
}
end Condensed
-- Get the list of visible (by default) free variables from a goal
@[export pantograph_visible_fvars_of_mvar]
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
let mvarDecl ← mctx.findDecl? mvarId
let lctx := mvarDecl.lctx
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
| some decl => if decl.isAuxDecl decl.isImplementationDetail then r else r.push decl.fvarId
| none => r
@[export pantograph_to_condensed_goal_m]
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
let mvarDecl ← mvarId.getDecl
let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
Meta.withLCtx lctx mvarDecl.localInstances do
let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
match localDecl with
| .cdecl _ fvarId userName type _ _ =>
let type ← instantiate type
return { fvarId, userName, type }
| .ldecl _ fvarId userName type value _ _ => do
let userName := userName.simpMacroScopes
let type ← instantiate type
let value ← instantiate value
return { fvarId, userName, type, value? := .some value }
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
!ppImplDetailHyps && localDecl.isImplementationDetail
if skip then
return acc
else
let var ← ppVar localDecl
return var::acc
return {
mvarId,
userName := mvarDecl.userName,
context := vars.reverse.toArray,
target := ← instantiate mvarDecl.type
}
where
instantiate := instantiateAll
@[export pantograph_goal_state_to_condensed_m]
protected def GoalState.toCondensed (state: GoalState):
CoreM (Array Condensed.Goal):= do
let metaM := do
let goals := state.goals.toArray
goals.mapM fun goal => do
match state.mctx.findDecl? goal with
| .some _ =>
let serializedGoal ← toCondensedGoal goal
pure serializedGoal
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
metaM.run' (s := state.savedState.term.meta.meta)
end Pantograph

View File

@ -1,153 +0,0 @@
import Pantograph.Protocol
import Pantograph.Serial
import Lean
open Lean
open Pantograph
namespace Pantograph.Environment
@[export pantograph_is_name_internal]
def isNameInternal (n: Name): Bool :=
-- Returns true if the name is an implementation detail which should not be shown to the user.
n.isAuxLemma n.hasMacroScopes
/-- Catalog all the non-internal and safe names -/
@[export pantograph_environment_catalog]
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ =>
match isNameInternal name with
| false => acc.push name
| true => acc)
@[export pantograph_environment_module_of_name]
def module_of_name (env: Environment) (name: Name): Option Name := do
let moduleId ← env.getModuleIdxFor? name
return env.allImportedModuleNames.get! moduleId.toNat
def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
let pref := match info with
| .axiomInfo _ => "a"
| .defnInfo _ => "d"
| .thmInfo _ => "t"
| .opaqueInfo _ => "o"
| .quotInfo _ => "q"
| .inductInfo _ => "i"
| .ctorInfo _ => "c"
| .recInfo _ => "r"
s!"{pref}{toString n}"
def toFilteredSymbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
if isNameInternal n || info.isUnsafe
then Option.none
else Option.some <| toCompactSymbolName n info
def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info =>
match toFilteredSymbol name info with
| .some x => acc.push x
| .none => acc)
return { symbols := names }
def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
let env ← Lean.MonadEnv.getEnv
let name := args.name.toName
let info? := env.find? name
let info ← match info? with
| none => return .error $ Protocol.errorIndex s!"Symbol not found {args.name}"
| some info => pure info
let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
let value? := match args.value?, info with
| .some true, _ => info.value?
| .some false, _ => .none
| .none, .defnInfo _ => info.value?
| .none, _ => .none
let type ← unfoldAuxLemmas info.type
let value? ← value?.mapM (λ v => unfoldAuxLemmas v)
-- Information common to all symbols
let core := {
type := ← (serializeExpression options type).run',
isUnsafe := info.isUnsafe,
value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
publicName? := Lean.privateToUserName? name |>.map (·.toString),
-- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
typeDependency? := if args.dependency?.getD false
then .some <| type.getUsedConstants.map (λ n => serializeName n)
else .none,
valueDependency? := if args.dependency?.getD false
then value?.map (λ e =>
e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
else .none,
module? := module?
}
let result ← match info with
| .inductInfo induct => pure { core with inductInfo? := .some {
numParams := induct.numParams,
numIndices := induct.numIndices,
all := induct.all.toArray.map (·.toString),
ctors := induct.ctors.toArray.map (·.toString),
isRec := induct.isRec,
isReflexive := induct.isReflexive,
isNested := induct.isNested,
} }
| .ctorInfo ctor => pure { core with constructorInfo? := .some {
induct := ctor.induct.toString,
cidx := ctor.cidx,
numParams := ctor.numParams,
numFields := ctor.numFields,
} }
| .recInfo r => pure { core with recursorInfo? := .some {
all := r.all.toArray.map (·.toString),
numParams := r.numParams,
numIndices := r.numIndices,
numMotives := r.numMotives,
numMinors := r.numMinors,
rules := ← r.rules.toArray.mapM (λ rule => do
pure {
ctor := rule.ctor.toString,
nFields := rule.nfields,
rhs := ← (serializeExpression options rule.rhs).run',
})
k := r.k,
} }
| _ => pure core
return .ok result
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
let type ← match parseTerm env args.type with
| .ok syn => do
match ← elabTerm syn with
| .error e => return .error e
| .ok expr => pure expr
| .error e => return .error e
let value ← match parseTerm env args.value with
| .ok syn => do
try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← instantiateMVars expr
pure $ expr
catch ex => return .error (← ex.toMessageData.toString)
| .error e => return .error e
pure $ .ok (type, value)
let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
| .ok t => pure t
| .error e => return .error $ Protocol.errorExpr e
let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
(name := args.name.toName)
(levelParams := [])
(type := type)
(value := value)
(hints := Lean.mkReducibilityHintsRegularEx 1)
(safety := Lean.DefinitionSafety.safe)
(all := [])
let env' ← match env.addDecl (← getOptions) constant with
| .error e => do
let options ← Lean.MonadOptions.getOptions
let desc ← (e.toMessageData options).toString
return .error $ { error := "kernel", desc }
| .ok env' => pure env'
Lean.MonadEnv.modifyEnv (λ _ => env')
return .ok {}
end Pantograph.Environment

View File

@ -1,162 +0,0 @@
import Lean
import Std.Data.HashMap
open Lean
namespace Pantograph
structure ProjectionApplication where
projector: Name
numParams: Nat
inner: Expr
@[export pantograph_expr_proj_to_app]
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
let (typeName, idx, inner) := match e with
| .proj typeName idx inner => (typeName, idx, inner)
| _ => panic! "Argument must be proj"
let ctor := getStructureCtor env typeName
let fieldName := getStructureFields env typeName |>.get! idx
let projector := getProjFnForField? env typeName fieldName |>.get!
{
projector,
numParams := ctor.numParams,
inner,
}
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
@[export pantograph_unfold_aux_lemmas]
def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
/--
Force the instantiation of delayed metavariables even if they cannot be fully
instantiated. This is used during resumption to provide diagnostic data about
the current goal.
Since Lean 4 does not have an `Expr` constructor corresponding to delayed
metavariables, any delayed metavariables must be recursively handled by this
function to ensure that nested delayed metavariables can be properly processed.
The caveat is this recursive call will lead to infinite recursion if a loop
between metavariable assignment exists.
This function ensures any metavariable in the result is either
1. Delayed assigned with its pending mvar not assigned in any form
2. Not assigned (delay or not)
-/
partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do
--let padding := String.join $ List.replicate level "│ "
--IO.println s!"{padding}Starting {toString eOrig}"
let mut result ← Meta.transform (← instantiateMVars eOrig)
(pre := fun e => e.withApp fun f args => do
let .mvar mvarId := f | return .continue
--IO.println s!"{padding}├V {e}"
let mvarDecl ← mvarId.getDecl
-- This is critical to maintaining the interdependency of metavariables.
-- Without setting `.syntheticOpaque`, Lean's metavariable elimination
-- system will not make the necessary delayed assigned mvars in case of
-- nested mvars.
mvarId.setKind .syntheticOpaque
mvarId.withContext do
let lctx ← MonadLCtx.getLCtx
if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then
let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with
| .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name]
| .none => acc) []
panic! s!"In the context of {mvarId.name}, there are local context variable violations: {violations}"
if let .some assign ← getExprMVarAssignment? mvarId then
--IO.println s!"{padding}├A ?{mvarId.name}"
assert! !(← mvarId.isDelayedAssigned)
return .visit (mkAppN assign args)
else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
--let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList
--IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]"
if args.size < fvars.size then
throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
--if !args.isEmpty then
--IO.println s!"{padding}├── Arguments Begin"
let args ← args.mapM self
--if !args.isEmpty then
--IO.println s!"{padding}├── Arguments End"
if !(← mvarIdPending.isAssignedOrDelayedAssigned) then
--IO.println s!"{padding}├T1"
let result := mkAppN f args
return .done result
let pending ← mvarIdPending.withContext do
let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1)
--IO.println s!"{padding}├Pre: {inner}"
pure <| (← inner.abstractM fvars).instantiateRev args
-- Tail arguments
let result := mkAppRange pending fvars.size args.size args
--IO.println s!"{padding}├MD {result}"
return .done result
else
assert! !(← mvarId.isAssigned)
assert! !(← mvarId.isDelayedAssigned)
--if !args.isEmpty then
-- IO.println s!"{padding}├── Arguments Begin"
let args ← args.mapM self
--if !args.isEmpty then
-- IO.println s!"{padding}├── Arguments End"
--IO.println s!"{padding}├M ?{mvarId.name}"
return .done (mkAppN f args))
--IO.println s!"{padding}└Result {result}"
return result
where
self e := instantiateDelayedMVars e --(level := level + 1)
/--
Convert an expression to an equiavlent form with
1. No nested delayed assigned mvars
2. No aux lemmas
3. No assigned mvars
-/
@[export pantograph_instantiate_all_m]
def instantiateAll (e: Expr): MetaM Expr := do
let e ← instantiateDelayedMVars e
let e ← unfoldAuxLemmas e
return e
structure DelayedMVarInvocation where
mvarIdPending: MVarId
args: Array (FVarId × (Option Expr))
-- Extra arguments applied to the result of this substitution
tail: Array Expr
-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
@[export pantograph_to_delayed_mvar_invocation_m]
def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
let .mvar mvarId := e.getAppFn | return .none
let .some decl ← getDelayedMVarAssignment? mvarId | return .none
let mvarIdPending := decl.mvarIdPending
let mvarDecl ← mvarIdPending.getDecl
-- Print the function application e. See Lean's `withOverApp`
let args := e.getAppArgs
assert! args.size ≥ decl.fvars.size
assert! !(← mvarIdPending.isAssigned)
assert! !(← mvarIdPending.isDelayedAssigned)
let fvarArgMap: Std.HashMap FVarId Expr := Std.HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
let fvarId := localDecl.fvarId
let a := fvarArgMap[fvarId]?
return acc ++ [(fvarId, a)]
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)
return .some {
mvarIdPending,
args := subst.toArray,
tail := args.toList.drop decl.fvars.size |>.toArray,
}
end Pantograph

View File

@ -1,4 +0,0 @@
/- Adapted from lean-training-data by semorrison -/
import Pantograph.Frontend.Basic
import Pantograph.Frontend.Elab
import Pantograph.Frontend.MetaTranslate

View File

@ -1,120 +0,0 @@
import Lean.Parser
import Lean.Elab.Frontend
open Lean
namespace Lean.FileMap
/-- Extract the range of a `Syntax` expressed as lines and columns. -/
-- Extracted from the private declaration `Lean.Elab.formatStxRange`,
-- in `Lean.Elab.InfoTree.Main`.
@[export pantograph_frontend_stx_range]
protected def stxRange (fileMap : FileMap) (stx : Syntax) : Position × Position :=
let pos := stx.getPos?.getD 0
let endPos := stx.getTailPos?.getD pos
(fileMap.toPosition pos, fileMap.toPosition endPos)
end Lean.FileMap
namespace Lean.PersistentArray
/--
Drop the first `n` elements of a `PersistentArray`, returning the results as a `List`.
-/
-- We can't remove the `[Inhabited α]` hypotheses here until
-- `PersistentArray`'s `GetElem` instance also does.
protected def drop [Inhabited α] (t : PersistentArray α) (n : Nat) : List α :=
List.range (t.size - n) |>.map fun i => t.get! (n + i)
end Lean.PersistentArray
namespace Pantograph.Frontend
abbrev FrontendM := Elab.Frontend.FrontendM
structure CompilationStep where
fileName : String
fileMap : FileMap
src : Substring
stx : Syntax
before : Environment
after : Environment
msgs : List Message
trees : List Elab.InfoTree
namespace CompilationStep
@[export pantograph_frontend_compilation_step_message_strings_m]
def messageStrings (step: CompilationStep) : IO (Array String) := do
List.toArray <$> step.msgs.mapM (·.toString)
end CompilationStep
/--
Process one command, returning a `CompilationStep` and
`done : Bool`, indicating whether this was the last command.
-/
@[export pantograph_frontend_process_one_command_m]
def processOneCommand: FrontendM (CompilationStep × Bool) := do
let s := (← get).commandState
let before := s.env
let done ← Elab.Frontend.processCommand
let stx := (← get).commands.back
let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
let s' := (← get).commandState
let after := s'.env
let msgs := s'.messages.toList.drop s.messages.toList.length
let trees := s'.infoState.trees.drop s.infoState.trees.size
let ⟨_, fileName, fileMap⟩ := (← read).inputCtx
return ({ fileName, fileMap, src, stx, before, after, msgs, trees }, done)
partial def mapCompilationSteps { α } (f: CompilationStep → IO α) : FrontendM (List α) := do
let (cmd, done) ← processOneCommand
if done then
if cmd.src.isEmpty then
return []
else
return [← f cmd]
else
return (← f cmd) :: (← mapCompilationSteps f)
@[export pantograph_frontend_find_source_path_m]
def findSourcePath (module : Name) : IO System.FilePath := do
return System.FilePath.mk ((← findOLean module).toString.replace ".lake/build/lib/" "") |>.withExtension "lean"
/--
Use with
```lean
let m: FrontendM α := ...
let (context, state) ← createContextStateFromFile ...
m.run context |>.run' state
```
-/
@[export pantograph_frontend_create_context_state_from_file_m]
def createContextStateFromFile
(file : String) -- Content of the file
(fileName : String := "<anonymous>")
(env? : Option Lean.Environment := .none) -- If set to true, assume there's no header.
(opts : Options := {})
: IO (Elab.Frontend.Context × Elab.Frontend.State) := unsafe do
--let file ← IO.FS.readFile (← findSourcePath module)
let inputCtx := Parser.mkInputContext file fileName
let (env, parserState, messages) ← match env? with
| .some env => pure (env, {}, .empty)
| .none =>
let (header, parserState, messages) ← Parser.parseHeader inputCtx
let (env, messages) ← Elab.processHeader header opts messages inputCtx
pure (env, parserState, messages)
let commandState := Elab.Command.mkState env messages opts
let context: Elab.Frontend.Context := { inputCtx }
let state: Elab.Frontend.State := {
commandState := { commandState with infoState.enabled := true },
parserState,
cmdPos := parserState.pos
}
return (context, state)
end Pantograph.Frontend

View File

@ -1,223 +0,0 @@
/- Adapted from https://github.com/semorrison/lean-training-data -/
import Lean.Elab.Import
import Lean.Elab.Command
import Lean.Elab.InfoTree
import Pantograph.Frontend.Basic
import Pantograph.Frontend.MetaTranslate
import Pantograph.Goal
import Pantograph.Protocol
open Lean
namespace Lean.Elab.Info
/-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
protected def stx? : Info → Option Syntax
| .ofTacticInfo info => info.stx
| .ofTermInfo info => info.stx
| .ofCommandInfo info => info.stx
| .ofMacroExpansionInfo info => info.stx
| .ofOptionInfo info => info.stx
| .ofFieldInfo info => info.stx
| .ofCompletionInfo info => info.stx
| .ofUserWidgetInfo info => info.stx
| .ofCustomInfo info => info.stx
| .ofFVarAliasInfo _ => none
| .ofFieldRedeclInfo info => info.stx
| .ofOmissionInfo info => info.stx
/-- Is the `Syntax` for this `Lean.Elab.Info` original, or synthetic? -/
protected def isOriginal (i : Info) : Bool :=
match i.stx? with
| none => true -- Somewhat unclear what to do with `FVarAliasInfo`, so be conservative.
| some stx => match stx.getHeadInfo with
| .original .. => true
| _ => false
end Lean.Elab.Info
namespace Lean.Elab.TacticInfo
/-- Find the name for the outermost `Syntax` in this `TacticInfo`. -/
def name? (t : TacticInfo) : Option Name :=
match t.stx with
| Syntax.node _ n _ => some n
| _ => none
/-- Decide whether a tactic is "substantive",
or is merely a tactic combinator (e.g. `by`, `;`, multiline tactics, parenthesized tactics). -/
def isSubstantive (t : TacticInfo) : Bool :=
match t.name? with
| none => false
| some `null => false
| some ``cdot => false
| some ``cdotTk => false
| some ``Lean.Parser.Term.byTactic => false
| some ``Lean.Parser.Tactic.tacticSeq => false
| some ``Lean.Parser.Tactic.tacticSeq1Indented => false
| some ``Lean.Parser.Tactic.«tactic_<;>_» => false
| some ``Lean.Parser.Tactic.paren => false
| _ => true
end Lean.Elab.TacticInfo
namespace Lean.Elab.InfoTree
/--
Keep `.node` nodes and `.hole` nodes satisfying predicates.
Returns a `List InfoTree`, although in most situations this will be a singleton.
-/
partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
InfoTree → List InfoTree
| .context ctx tree => tree.filter p m |>.map (.context ctx)
| .node info children =>
if p info then
[.node info (children.toList.map (filter p m)).join.toPArray']
else
(children.toList.map (filter p m)).join
| .hole mvar => if m mvar then [.hole mvar] else []
end Lean.Elab.InfoTree
namespace Pantograph.Frontend
-- Info tree filtering functions
structure TacticInvocation where
info : Elab.TacticInfo
ctx : Elab.ContextInfo
children : PersistentArray Elab.InfoTree
namespace TacticInvocation
/-- Return the range of the tactic, as a pair of file positions. -/
@[export pantograph_frontend_tactic_invocation_range]
protected def range (t : TacticInvocation) : Position × Position := t.ctx.fileMap.stxRange t.info.stx
/-- Pretty print a tactic. -/
protected def pp (t : TacticInvocation) : IO Format :=
t.ctx.runMetaM {} try
Lean.PrettyPrinter.ppTactic ⟨t.info.stx⟩
catch _ =>
pure "<failed to pretty print>"
/-- Run a tactic on the goals stored in a `TacticInvocation`. -/
protected def runMetaMGoalsBefore (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxBefore <| x t.info.goalsBefore
/-- Run a tactic on the after goals stored in a `TacticInvocation`. -/
protected def runMetaMGoalsAfter (t : TacticInvocation) (x : List MVarId → MetaM α) : IO α := do
t.ctx.runMetaM {} <| Meta.withMCtx t.info.mctxAfter <| x t.info.goalsAfter
/-- Run a tactic on the main goal stored in a `TacticInvocation`. -/
protected def runMetaM (t : TacticInvocation) (x : MVarId → MetaM α) : IO α := do
match t.info.goalsBefore.head? with
| none => throw <| IO.userError s!"No goals at {← t.pp}"
| some g => t.runMetaMGoalsBefore fun _ => do g.withContext <| x g
protected def goalState (t : TacticInvocation) : IO (List Format) := do
t.runMetaMGoalsBefore (fun gs => gs.mapM fun g => do Meta.ppGoal g)
protected def goalStateAfter (t : TacticInvocation) : IO (List Format) := do
t.runMetaMGoalsAfter (fun gs => gs.mapM fun g => do Meta.ppGoal g)
protected def ppExpr (t : TacticInvocation) (e : Expr) : IO Format :=
t.runMetaM (fun _ => do Meta.ppExpr (← instantiateMVars e))
protected def usedConstants (t: TacticInvocation) : NameSet :=
let info := t.info
info.goalsBefore
|>.filterMap info.mctxAfter.getExprAssignmentCore?
|>.map Expr.getUsedConstantsAsSet
|>.foldl .union .empty
end TacticInvocation
/-- Analogue of `Lean.Elab.InfoTree.findInfo?`, but that returns a list of all results. -/
partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo) (pred : Elab.Info → Bool) :
List (Elab.Info × Option Elab.ContextInfo × PersistentArray Elab.InfoTree) :=
match t with
| .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
| .node i children =>
(if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
| _ => []
/-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
each equipped with its relevant `ContextInfo`, and any children info trees. -/
private def collectTacticNodes (t : Elab.InfoTree) : List TacticInvocation :=
let infos := findAllInfo t none fun i => match i with
| .ofTacticInfo _ => true
| _ => false
infos.filterMap fun p => match p with
| (.ofTacticInfo i, some ctx, children) => .some ⟨i, ctx, children⟩
| _ => none
def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
collectTacticNodes t |>.filter fun i => i.info.isSubstantive
@[export pantograph_frontend_collect_tactics_from_compilation_step_m]
def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
| info@(.ofTacticInfo _) => info.isOriginal
| _ => false
let tactics := tacticInfoTrees.bind collectTactics
tactics.mapM λ invocation => do
let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
let tactic ← invocation.ctx.runMetaM {} do
let t ← PrettyPrinter.ppTactic ⟨invocation.info.stx⟩
return t.pretty
let usedConstants := invocation.usedConstants.toArray.map λ n => n.toString
return {
goalBefore,
goalAfter,
tactic,
usedConstants,
}
structure InfoWithContext where
info: Elab.Info
context?: Option Elab.ContextInfo := .none
private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
let infos := findAllInfo t none fun i => match i with
| .ofTermInfo { expectedType?, expr, stx, .. } =>
expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
| .ofTacticInfo { stx, goalsBefore, .. } =>
-- The `sorry` term is distinct from the `sorry` tactic
let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
isSorry ∧ !goalsBefore.isEmpty
| _ => false
infos.map fun (info, context?, _) => { info, context? }
-- NOTE: Plural deliberately not spelled "sorries"
@[export pantograph_frontend_collect_sorrys_m]
def collectSorrys (step: CompilationStep) : List InfoWithContext :=
step.trees.bind collectSorrysInTree
/--
Since we cannot directly merge `MetavarContext`s, we have to get creative. This
function duplicates frozen mvars in term and tactic info nodes, and add them to
the current `MetavarContext`.
-/
@[export pantograph_frontend_sorrys_to_goal_state]
def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
assert! !sorrys.isEmpty
let goalsM := sorrys.mapM λ i => do
match i.info with
| .ofTermInfo termInfo => do
let mvarId ← MetaTranslate.translateMVarFromTermInfo termInfo i.context?
return [mvarId]
| .ofTacticInfo tacticInfo => do
MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
| _ => panic! "Invalid info"
let goals := List.join (← goalsM.run {} |>.run' {})
let root := match goals with
| [] => panic! "No MVars generated"
| [g] => g
| _ => { name := .anonymous }
GoalState.createFromMVars goals root
end Pantograph.Frontend

View File

@ -1,164 +0,0 @@
import Lean.Meta
import Std.Data.HashMap
open Lean
namespace Pantograph.Frontend
namespace MetaTranslate
structure Context where
sourceMCtx : MetavarContext := {}
sourceLCtx : LocalContext := {}
abbrev FVarMap := Std.HashMap FVarId FVarId
structure State where
-- Stores mapping from old to new mvar/fvars
mvarMap: Std.HashMap MVarId MVarId := {}
fvarMap: Std.HashMap FVarId FVarId := {}
/-
Monadic state for translating a frozen meta state. The underlying `MetaM`
operates in the "target" context and state.
-/
abbrev MetaTranslateM := ReaderT Context StateRefT State MetaM
def getSourceLCtx : MetaTranslateM LocalContext := do pure (← read).sourceLCtx
def getSourceMCtx : MetaTranslateM MetavarContext := do pure (← read).sourceMCtx
def addTranslatedFVar (src dst: FVarId) : MetaTranslateM Unit := do
modifyGet λ state => ((), { state with fvarMap := state.fvarMap.insert src dst })
def addTranslatedMVar (src dst: MVarId) : MetaTranslateM Unit := do
modifyGet λ state => ((), { state with mvarMap := state.mvarMap.insert src dst })
def saveFVarMap : MetaTranslateM FVarMap := do
return (← get).fvarMap
def restoreFVarMap (map: FVarMap) : MetaTranslateM Unit := do
modifyGet λ state => ((), { state with fvarMap := map })
def resetFVarMap : MetaTranslateM Unit := do
modifyGet λ state => ((), { state with fvarMap := {} })
mutual
private partial def translateLevel (srcLevel: Level) : MetaTranslateM Level := do
let sourceMCtx ← getSourceMCtx
let (_, level) := instantiateLevelMVarsImp sourceMCtx srcLevel
match level with
| .zero => return .zero
| .succ inner => do
let inner' ← translateLevel inner
return .succ inner'
| .max l1 l2 => do
let l1' ← translateLevel l1
let l2' ← translateLevel l2
return .max l1' l2'
| .imax l1 l2 => do
let l1' ← translateLevel l1
let l2' ← translateLevel l2
return .imax l1' l2'
| .param p => return .param p
| .mvar _ =>
Meta.mkFreshLevelMVar
private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
let sourceMCtx ← getSourceMCtx
-- We want to create as few mvars as possible
let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
--IO.println s!"Transform src: {srcExpr}"
let result ← Core.transform srcExpr λ e => do
let state ← get
match e with
| .fvar fvarId =>
let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
assert! (← getLCtx).contains fvarId'
return .done $ .fvar fvarId'
| .mvar mvarId => do
-- Must not be assigned
assert! !(sourceMCtx.eAssignment.contains mvarId)
match state.mvarMap[mvarId]? with
| .some mvarId' => do
return .done $ .mvar mvarId'
| .none => do
-- Entering another LCtx, must save the current one
let fvarMap ← saveFVarMap
let mvarId' ← translateMVarId mvarId
restoreFVarMap fvarMap
return .done $ .mvar mvarId'
| .sort level => do
let level' ← translateLevel level
return .done $ .sort level'
| _ => return .continue
Meta.check result
return result
partial def translateLocalInstance (srcInstance: LocalInstance) : MetaTranslateM LocalInstance := do
return {
className := srcInstance.className,
fvar := ← translateExpr srcInstance.fvar
}
partial def translateLocalDecl (srcLocalDecl: LocalDecl) : MetaTranslateM LocalDecl := do
let fvarId ← mkFreshFVarId
addTranslatedFVar srcLocalDecl.fvarId fvarId
match srcLocalDecl with
| .cdecl index _ userName type bi kind => do
--IO.println s!"[CD] {userName} {toString type}"
return .cdecl index fvarId userName (← translateExpr type) bi kind
| .ldecl index _ userName type value nonDep kind => do
--IO.println s!"[LD] {toString type} := {toString value}"
return .ldecl index fvarId userName (← translateExpr type) (← translateExpr value) nonDep kind
partial def translateLCtx : MetaTranslateM LocalContext := do
resetFVarMap
let lctx ← MonadLCtx.getLCtx
assert! lctx.isEmpty
(← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
let localDecl ← Meta.withLCtx lctx #[] do
translateLocalDecl srcLocalDecl
pure $ lctx.addDecl localDecl
) lctx
partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
return mvarId'
let mvarId' ← Meta.withLCtx .empty #[] do
let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
let lctx' ← translateLCtx
let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
Meta.withLCtx lctx' localInstances' do
let target' ← translateExpr srcDecl.type
let mvar' ← Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
let mvarId' := mvar'.mvarId!
if let .some { fvars, mvarIdPending }:= (← getSourceMCtx).getDelayedMVarAssignmentExp srcMVarId then
-- Map the fvars in the pending context.
let mvarIdPending' ← translateMVarId mvarIdPending
let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
assignDelayedMVar mvarId' fvars' mvarIdPending'
pure mvarId'
addTranslatedMVar srcMVarId mvarId'
return mvarId'
end
def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)
: MetaTranslateM MVarId := do
withTheReader Context (λ ctx => { ctx with
sourceMCtx := context?.map (·.mctx) |>.getD {},
sourceLCtx := termInfo.lctx,
}) do
let type := termInfo.expectedType?.get!
let lctx' ← translateLCtx
let mvar ← Meta.withLCtx lctx' #[] do
let type' ← translateExpr type
Meta.mkFreshExprSyntheticOpaqueMVar type'
return mvar.mvarId!
def translateMVarFromTacticInfoBefore (tacticInfo : Elab.TacticInfo) (_context? : Option Elab.ContextInfo)
: MetaTranslateM (List MVarId) := do
withTheReader Context (λ ctx => { ctx with sourceMCtx := tacticInfo.mctxBefore }) do
tacticInfo.goalsBefore.mapM translateMVarId
end MetaTranslate
export MetaTranslate (MetaTranslateM)
end Pantograph.Frontend

View File

@ -1,397 +0,0 @@
/-
Functions for handling metavariables
All the functions starting with `try` resume their inner monadic state.
-/
import Pantograph.Tactic
import Lean
namespace Pantograph
open Lean
def filename: String := "<pantograph>"
/--
Represents an interconnected set of metavariables, or a state in proof search
-/
structure GoalState where
savedState : Elab.Tactic.SavedState
-- The root hole which is the search target
root: MVarId
-- Parent state metavariable source
parentMVar?: Option MVarId
-- Existence of this field shows that we are currently in `conv` mode.
-- (convRhs, goal, dormant)
convMVar?: Option (MVarId × MVarId × List MVarId) := .none
-- Previous RHS for calc, so we don't have to repeat it every time
-- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
calcPrevRhs?: Option (MVarId × Expr) := .none
@[export pantograph_goal_state_create_m]
protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
-- May be necessary to 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
let root ← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous)
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root.mvarId!]}
return {
root := root.mvarId!,
savedState,
parentMVar? := .none,
}
@[export pantograph_goal_state_create_from_mvars_m]
protected def GoalState.createFromMVars (goals: List MVarId) (root: MVarId): MetaM GoalState := do
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals } |>.run' {}
return {
root,
savedState,
parentMVar? := .none,
}
@[export pantograph_goal_state_is_conv]
protected def GoalState.isConv (state: GoalState): Bool :=
state.convMVar?.isSome
protected def GoalState.goals (state: GoalState): List MVarId :=
state.savedState.tactic.goals
@[export pantograph_goal_state_goals]
protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
protected def GoalState.mctx (state: GoalState): MetavarContext :=
state.savedState.term.meta.meta.mctx
protected def GoalState.env (state: GoalState): Environment :=
state.savedState.term.meta.core.env
@[export pantograph_goal_state_meta_context_of_goal]
protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
let mvarDecl ← state.mctx.findDecl? mvarId
return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
protected def GoalState.metaState (state: GoalState): Meta.State :=
state.savedState.term.meta.meta
protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
mvarId.withContext m |>.run' (← read) state.metaState
protected def GoalState.withParentContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
Meta.mapMetaM <| state.withContext state.parentMVar?.get!
protected def GoalState.withRootContext { n } [MonadControlT MetaM n] [Monad n] (state: GoalState): n α → n α :=
Meta.mapMetaM <| state.withContext state.root
private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit :=
state.savedState.term.meta.restore
protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit :=
state.savedState.term.restore
private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do
state.savedState.restore
Elab.Tactic.setGoals [goal]
@[export pantograph_goal_state_focus]
protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do
let goal ← state.savedState.tactic.goals.get? goalId
return {
state with
savedState := {
state.savedState with
tactic := { goals := [goal] },
},
calcPrevRhs? := .none,
}
/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
@[export pantograph_goal_state_immediate_resume_parent]
protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
-- Prune parents solved goals
let mctx := state.mctx
let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
{
state with
savedState := {
state.savedState with
tactic := { goals := state.goals ++ parentGoals },
},
}
/--
Brings into scope a list of goals
-/
@[export pantograph_goal_state_resume]
protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
.error s!"Goals {invalid_goals} are not in scope"
else
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := goals.filter (λ goal =>
let mctx := state.mctx
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
.ok {
state with
savedState := {
term := state.savedState.term,
tactic := { goals := unassigned },
},
}
/--
Brings into scope all goals from `branch`
-/
@[export pantograph_goal_state_continue]
protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState :=
if !target.goals.isEmpty then
.error s!"Target state has unresolved goals"
else if target.root != branch.root then
.error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}"
else
target.resume (goals := branch.goals)
@[export pantograph_goal_state_root_expr]
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
if goalState.root.name == .anonymous then
.none
let expr ← goalState.mctx.eAssignment.find? goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasExprMVar then
-- Must not assert that the goal state is empty here. We could be in a branch goal.
--assert! ¬goalState.goals.isEmpty
.none
else
assert! goalState.goals.isEmpty
return expr
@[export pantograph_goal_state_parent_expr]
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let parent ← goalState.parentMVar?
let expr := goalState.mctx.eAssignment.find! parent
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr
@[export pantograph_goal_state_get_mvar_e_assignment]
protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? mvarId
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr
--- Tactic execution functions ---
protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
: Elab.TermElabM GoalState := do
unless (← getMCtx).decls.contains goal do
throwError s!"Goal is not in context: {goal.name}"
goal.checkNotAssigned `GoalState.step
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
let nextElabState ← MonadBacktrack.saveState
return {
state with
savedState := { term := nextElabState, tactic := newGoals },
parentMVar? := .some goal,
calcPrevRhs? := .none,
}
/-- Response for executing a tactic -/
inductive TacticResult where
-- Goes to next state
| success (state: GoalState)
-- Tactic failed with messages
| failure (messages: Array String)
-- Could not parse tactic
| parseError (message: String)
-- The given action cannot be executed in the state
| invalidAction (message: String)
/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
Elab.TermElabM TacticResult := do
try
let nextState ← state.step goal tacticM
return .success nextState
catch exception =>
return .failure #[← exception.toMessageData.toString]
/-- Execute a string tactic on given state. Restores TermElabM -/
protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let tactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := if state.isConv then `conv else `tactic)
(input := tactic)
(fileName := filename) with
| .ok stx => pure $ stx
| .error error => return .parseError error
state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let expr ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := expr)
(fileName := filename) with
| .ok syn => pure syn
| .error error => return .parseError error
state.tryTacticM goal $ Tactic.evalAssign expr
-- Specialized Tactics
protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let type ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := type)
(fileName := filename) with
| .ok syn => pure syn
| .error error => return .parseError error
state.tryTacticM goal $ Tactic.evalLet binderName.toName type
/-- Enter conv tactic mode -/
protected def GoalState.conv (state: GoalState) (goal: MVarId):
Elab.TermElabM TacticResult := do
if state.convMVar?.isSome then
return .invalidAction "Already in conv state"
goal.checkNotAssigned `GoalState.conv
let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
state.restoreTacticM goal
-- See Lean.Elab.Tactic.Conv.convTarget
let convMVar ← Elab.Tactic.withMainContext do
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
pure rhs.mvarId!
return (← MonadBacktrack.saveState, convMVar)
try
let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-- Other goals are now dormant
let otherGoals := state.goals.filter $ λ g => g != goal
return .success {
root := state.root,
savedState := nextSavedState
parentMVar? := .some goal,
convMVar? := .some (convRhs, goal, otherGoals),
calcPrevRhs? := .none
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
@[export pantograph_goal_state_conv_exit_m]
protected def GoalState.convExit (state: GoalState):
Elab.TermElabM TacticResult := do
let (convRhs, convGoal, _) ← match state.convMVar? with
| .some mvar => pure mvar
| .none => return .invalidAction "Not in conv state"
let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
-- Vide `Lean.Elab.Tactic.Conv.convert`
state.savedState.restore
-- Close all existing goals with `refl`
for mvarId in (← Elab.Tactic.getGoals) do
liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
Elab.Tactic.pruneSolvedGoals
unless (← Elab.Tactic.getGoals).isEmpty do
throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
Elab.Tactic.setGoals [convGoal]
let targetNew ← instantiateMVars (.mvar convRhs)
let proof ← instantiateMVars (.mvar convGoal)
Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
MonadBacktrack.saveState
try
let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
return .success {
root := state.root,
savedState := nextSavedState
parentMVar? := .some convGoal,
convMVar? := .none
calcPrevRhs? := .none
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
let (mvarId, rhs) ← state.calcPrevRhs?
if mvarId == goal then
.some rhs
else
.none
@[export pantograph_goal_state_try_calc_m]
protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
if state.convMVar?.isSome then
return .invalidAction "Cannot initiate `calc` while in `conv` state"
let `(term|$pred) ← match Parser.runParserCategory
(env := state.env)
(catName := `term)
(input := pred)
(fileName := filename) with
| .ok syn => pure syn
| .error error => return .parseError error
goal.checkNotAssigned `GoalState.tryCalc
let calcPrevRhs? := state.calcPrevRhsOf? goal
let decl ← goal.getDecl
let target ← instantiateMVars decl.type
let tag := decl.userName
try
goal.withContext do
let mut step ← Elab.Term.elabType <| ← do
if let some prevRhs := calcPrevRhs? then
Elab.Term.annotateFirstHoleWithType pred (← Meta.inferType prevRhs)
else
pure pred
let some (_, lhs, rhs) ← Elab.Term.getCalcRelation? step |
throwErrorAt pred "invalid 'calc' step, relation expected{indentExpr step}"
if let some prevRhs := calcPrevRhs? then
unless ← Meta.isDefEqGuarded lhs prevRhs do
throwErrorAt pred "invalid 'calc' step, left-hand-side is{indentD m!"{lhs} : {← Meta.inferType lhs}"}\nprevious right-hand-side is{indentD m!"{prevRhs} : {← Meta.inferType prevRhs}"}" -- "
-- Creates a mvar to represent the proof that the calc tactic solves the
-- current branch
-- In the Lean `calc` tactic this is gobbled up by
-- `withCollectingNewGoalsFrom`
let mut proof ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) step
(userName := tag ++ `calc)
let mvarBranch := proof.mvarId!
let mut proofType ← Meta.inferType proof
let mut remainder? := Option.none
-- The calc tactic either solves the main goal or leaves another relation.
-- Replace the main goal, and save the new goal if necessary
unless ← Meta.isDefEq proofType target do
let rec throwFailed :=
throwError "'calc' tactic failed, has type{indentExpr proofType}\nbut it is expected to have type{indentExpr target}"
let some (_, _, rhs) ← Elab.Term.getCalcRelation? proofType | throwFailed
let some (r, _, rhs') ← Elab.Term.getCalcRelation? target | throwFailed
let lastStep := mkApp2 r rhs rhs'
let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
(proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
unless ← Meta.isDefEq proofType target do throwFailed
remainder? := .some lastStepGoal.mvarId!
goal.assign proof
let goals := [ mvarBranch ] ++ remainder?.toList
let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
return .success {
root := state.root,
savedState := {
term := ← MonadBacktrack.saveState,
tactic := { goals },
},
parentMVar? := .some goal,
calcPrevRhs?
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
end Pantograph

View File

@ -1,205 +0,0 @@
import Pantograph.Condensed
import Pantograph.Environment
import Pantograph.Goal
import Pantograph.Protocol
import Pantograph.Serial
import Pantograph.Version
import Lean
namespace Lean
/-- This is better than the default version since it handles `.` and doesn't
crash the program when it fails. -/
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 := key.toName
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 s!"invalid Bool option value '{val}'"
| DataValue.ofName _ => pure $ opts.setName key val.toName
| DataValue.ofNat _ =>
match val.toNat? with
| none => throw s!"invalid Nat option value '{val}'"
| some v => pure $ opts.setNat key v
| DataValue.ofInt _ =>
match val.toInt? with
| none => throw s!"invalid Int option value '{val}'"
| some v => pure $ opts.setInt key v
| DataValue.ofSyntax _ => throw s!"invalid Syntax option value"
end Lean
open Lean
namespace Pantograph
def runMetaM { α } (metaM: MetaM α): CoreM α :=
metaM.run'
def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
termElabM.run' (ctx := Condensed.elabContext) |>.run'
def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
/-- Adds the given paths to Lean package search path -/
@[export pantograph_init_search]
unsafe def initSearch (sp: String): IO Unit := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) (sp := System.SearchPath.parse sp)
/-- Creates a Core.Context object needed to run all monads -/
@[export pantograph_create_core_context]
def createCoreContext (options: Array String): IO Core.Context := do
let options? ← options.foldlM setOptionFromString' Options.empty |>.run
let options ← match options? with
| .ok options => pure options
| .error e => throw $ IO.userError s!"Options cannot be parsed: {e}"
return {
currNamespace := Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0] },
options := options
}
/-- Creates a Core.State object needed to run all monads -/
@[export pantograph_create_core_state]
def createCoreState (imports: Array String): IO Core.State := do
let env ← Lean.importModules
(imports := imports.map (λ str => { module := str.toName, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return { env := env }
@[export pantograph_env_add_m]
def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
CoreM (Protocol.CR Protocol.EnvAddResult) :=
Environment.addDecl { name, type, value, isTheorem }
@[export pantograph_parse_elab_type_m]
def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
let env ← MonadEnv.getEnv
let syn ← match parseTerm env type with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← elabType syn with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok (← instantiateMVars expr)
/-- This must be a TermElabM since the parsed expr contains extra information -/
@[export pantograph_parse_elab_expr_m]
def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
let env ← MonadEnv.getEnv
let expectedType? ← match ← expectedType?.mapM parseElabType with
| .none => pure $ .none
| .some (.ok t) => pure $ .some t
| .some (.error e) => return .error e
let syn ← match parseTerm env expr with
| .error str => return .error $ errorI "parsing" str
| .ok syn => pure syn
match ← elabTerm syn expectedType? with
| .error str => return .error $ errorI "elab" str
| .ok expr => return .ok (← instantiateMVars expr)
@[export pantograph_expr_echo_m]
def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[]) (options: @&Protocol.Options := {}):
CoreM (Protocol.CR Protocol.ExprEchoResult) :=
runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
let expr ← match ← parseElabExpr expr expectedType? with
| .error e => return .error e
| .ok expr => pure expr
try
let type ← unfoldAuxLemmas (← Meta.inferType expr)
return .ok {
type := (← serializeExpression options type),
expr := (← serializeExpression options expr)
}
catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString)
@[export pantograph_goal_start_expr_m]
def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) :=
runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do
let expr ← match ← parseElabType expr with
| .error e => return .error e
| .ok expr => pure $ expr
return .ok $ ← GoalState.create expr
@[export pantograph_goal_resume]
def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options
@[export pantograph_goal_print_m]
def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult :=
runMetaM do
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr =>
state.withRootContext do
serializeExpression options (← instantiateAll expr)),
parent? := ← state.parentExpr?.mapM (λ expr =>
state.withParentContext do
serializeExpression options (← instantiateAll expr)),
}
@[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
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
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_motivated_apply_m]
protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let recursor ← match (← parseTermM recursor) with
| .ok syn => pure syn
| .error error => return .parseError error
state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
@[export pantograph_goal_try_no_confuse_m]
protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let eq ← match (← parseTermM eq) with
| .ok syn => pure syn
| .error error => return .parseError error
state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
@[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
end Pantograph

View File

@ -1,321 +0,0 @@
/-
All the command input/output structures are stored here
Note that no command other than `InteractionError` may have `error` as one of
its field names to avoid confusion with error messages generated by the REPL.
-/
import Lean.Data.Json
namespace Pantograph.Protocol
/-- Main Option structure, placed here to avoid name collision -/
structure Options where
-- When false, suppress newlines in Json objects. Useful for machine-to-machine interaction.
-- This should be false` by default to avoid any surprises with parsing.
printJsonPretty: Bool := false
-- When enabled, pretty print every expression
printExprPretty: Bool := true
-- When enabled, print the raw AST of expressions
printExprAST: Bool := false
printDependentMVars: Bool := false
-- When enabled, the types and values of persistent variables in a goal
-- are not shown unless they are new to the proof step. Reduces overhead.
-- NOTE: that this assumes the type and assignment of variables can never change.
noRepeat: Bool := false
-- See `pp.auxDecls`
printAuxDecls: Bool := false
-- See `pp.implementationDetailHyps`
printImplementationDetailHyps: Bool := false
-- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
automaticMode: Bool := true
deriving Lean.ToJson
abbrev OptionsT := ReaderT Options
--- Expression Objects ---
structure BoundExpression where
binders: Array (String × String)
target: String
deriving Lean.ToJson
structure Expression where
-- Pretty printed expression
pp?: Option String := .none
-- AST structure
sexp?: Option String := .none
dependentMVars?: Option (Array String) := .none
deriving Lean.ToJson
structure Variable where
/-- The internal name used in raw expressions -/
name: String := ""
/-- The name displayed to the user -/
userName: String
/-- Does the name contain a dagger -/
isInaccessible: Bool := false
type?: Option Expression := .none
value?: Option Expression := .none
deriving Lean.ToJson
structure Goal where
name: String := ""
/-- Name of the metavariable -/
userName?: Option String := .none
/-- Is the goal in conversion mode -/
isConversion: Bool := false
/-- target expression type -/
target: Expression
/-- Variables -/
vars: Array Variable := #[]
deriving Lean.ToJson
--- Individual Commands and return types ---
structure Command where
cmd: String
payload: Lean.Json
deriving Lean.FromJson
structure InteractionError where
error: String
desc: String
deriving Lean.ToJson
def errorIndex (desc: String): InteractionError := { error := "index", desc }
def errorExpr (desc: String): InteractionError := { error := "expr", desc }
--- Individual command and return types ---
structure Reset where
deriving Lean.FromJson
structure Stat where
deriving Lean.FromJson
structure StatResult where
-- Number of goals states
nGoals: Nat
deriving Lean.ToJson
-- Return the type of an expression
structure ExprEcho where
expr: String
type?: Option String
-- universe levels
levels: Option (Array String) := .none
deriving Lean.FromJson
structure ExprEchoResult where
expr: Expression
type: Expression
deriving Lean.ToJson
-- Print all symbols in environment
structure EnvCatalog where
deriving Lean.FromJson
structure EnvCatalogResult where
symbols: Array String
deriving Lean.ToJson
-- Print the type of a symbol
structure EnvInspect where
name: String
-- If true/false, show/hide the value expressions; By default definitions
-- values are shown and theorem values are hidden.
value?: Option Bool := .some false
-- If true, show the type and value dependencies
dependency?: Option Bool := .some false
deriving Lean.FromJson
-- See `InductiveVal`
structure InductInfo where
numParams: Nat
numIndices: Nat
all: Array String
ctors: Array String
isRec: Bool := false
isReflexive: Bool := false
isNested: Bool := false
deriving Lean.ToJson
-- See `ConstructorVal`
structure ConstructorInfo where
induct: String
cidx: Nat
numParams: Nat
numFields: Nat
deriving Lean.ToJson
/-- See `Lean/Declaration.lean` -/
structure RecursorRule where
ctor: String
nFields: Nat
rhs: Expression
deriving Lean.ToJson
structure RecursorInfo where
all: Array String
numParams: Nat
numIndices: Nat
numMotives: Nat
numMinors: Nat
rules: Array RecursorRule
k: Bool
deriving Lean.ToJson
structure EnvInspectResult where
type: Expression
isUnsafe: Bool := false
value?: Option Expression := .none
module?: Option String := .none
-- If the name is private, displays the public facing name
publicName?: Option String := .none
typeDependency?: Option (Array String) := .none
valueDependency?: Option (Array String) := .none
inductInfo?: Option InductInfo := .none
constructorInfo?: Option ConstructorInfo := .none
recursorInfo?: Option RecursorInfo := .none
deriving Lean.ToJson
structure EnvAdd where
name: String
type: String
value: String
isTheorem: Bool
deriving Lean.FromJson
structure EnvAddResult where
deriving Lean.ToJson
/-- Set options; See `Options` struct above for meanings -/
structure OptionsSet where
printJsonPretty?: Option Bool
printExprPretty?: Option Bool
printExprAST?: Option Bool
printDependentMVars?: Option Bool
noRepeat?: Option Bool
printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool
automaticMode?: Option Bool
deriving Lean.FromJson
structure OptionsSetResult where
deriving Lean.ToJson
structure OptionsPrint where
deriving Lean.FromJson
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
copyFrom: Option String -- Copy the type from a theorem in the environment
deriving Lean.FromJson
structure GoalStartResult where
stateId: Nat := 0
-- Name of the root metavariable
root: String
deriving Lean.ToJson
structure GoalTactic where
-- Identifiers for tree, state, and goal
stateId: Nat
goalId: Nat := 0
-- One of the fields here must be filled
tactic?: Option String := .none
expr?: Option String := .none
have?: Option String := .none
let?: Option String := .none
calc?: Option String := .none
-- true to enter `conv`, `false` to exit. In case of exit the `goalId` is ignored.
conv?: Option Bool := .none
-- In case of the `have` tactic, the new free variable name is provided here
binderName?: Option String := .none
deriving Lean.FromJson
structure GoalTacticResult where
-- The next goal state id. Existence of this field shows success
nextStateId?: Option Nat := .none
-- If the array is empty, it shows the goals have been fully resolved.
goals?: Option (Array Goal) := .none
-- Existence of this field shows tactic execution failure
tacticErrors?: Option (Array String) := .none
-- Existence of this field shows the tactic parsing has failed
parseError?: Option String := .none
deriving Lean.ToJson
structure GoalContinue where
-- State from which the continuation acquires the context
target: Nat
-- One of the following must be supplied
-- The state which is an ancestor of `target` where goals will be extracted from
branch?: Option Nat := .none
-- Or, the particular goals that should be brought back into scope
goals?: Option (Array String) := .none
deriving Lean.FromJson
structure GoalContinueResult where
nextStateId: Nat
goals: (Array Goal)
deriving Lean.ToJson
-- Remove goal states
structure GoalDelete where
-- This is ok being a List because it doesn't show up in the ABI
stateIds: List Nat
deriving Lean.FromJson
structure GoalDeleteResult where
deriving Lean.ToJson
structure GoalPrint where
stateId: Nat
deriving Lean.FromJson
structure GoalPrintResult where
-- The root expression
root?: Option Expression := .none
-- The filling expression of the parent goal
parent?: Option Expression
deriving Lean.ToJson
-- Diagnostic Options, not available in REPL
structure GoalDiag where
printContext: Bool := true
printValue: Bool := true
printNewMVars: Bool := false
-- Print all mvars
printAll: Bool := false
instantiate: Bool := true
printSexp: Bool := false
/-- Executes the Lean compiler on a single file -/
structure FrontendProcess where
-- One of these two must be supplied: Either supply the file name or the content.
fileName?: Option String := .none
file?: Option String := .none
-- If set to true, collect tactic invocations
invocations: Bool := false
-- If set to true, collect `sorry`s
sorrys: Bool := false
deriving Lean.FromJson
structure InvokedTactic where
goalBefore: String
goalAfter: String
tactic: String
-- List of used constants
usedConstants: Array String
deriving Lean.ToJson
structure CompilationUnit where
-- String boundaries of compilation units
boundary: (Nat × Nat)
-- Tactic invocations
invocations?: Option (List InvokedTactic) := .none
goalStateId?: Option Nat := .none
goals: Array Goal := #[]
messages: Array String := #[]
deriving Lean.ToJson
structure FrontendProcessResult where
units: List CompilationUnit
deriving Lean.ToJson
abbrev CR α := Except InteractionError α
end Pantograph.Protocol

149
Pantograph/SemihashMap.lean Normal file
View File

@ -0,0 +1,149 @@
namespace Pantograph.SemihashMap
structure Imp (β: Type u) where
data: Array (Option β)
-- Number of elements currently in use
size: Nat
-- Next index that has never been touched
allocFront: Nat
-- Deallocated indices
deallocs: Array Nat
-- Number of valid entries in `deallocs` array
lastDealloc: Nat
namespace Imp
structure WF (m: Imp β): Prop where
capacity: m.data.size = m.deallocs.size
front_dealloc: ∀ i: Fin m.deallocs.size, (i < m.allocFront) → (m.deallocs.get i) < m.allocFront
front_data: ∀ i: Fin m.data.size, (i ≥ m.allocFront) → (m.data.get i).isNone
def empty (capacity := 16): Imp β :=
{
data := mkArray capacity .none,
size := 0,
allocFront := 0,
deallocs := mkArray capacity 0,
lastDealloc := 0,
}
private theorem list_get_replicate (x: α) (i: Fin (List.replicate n x).length):
List.get (List.replicate n x) i = x := by
sorry
theorem empty_wf : WF (empty n: Imp β) := by
unfold empty
apply WF.mk
case capacity =>
conv =>
lhs
congr
simp
conv =>
rhs
congr
simp
simp
case front_dealloc =>
simp_all
intro i
intro a
contradiction
case front_data =>
simp_all
intro i
unfold Imp.data at i
simp at i
conv =>
lhs
unfold Array.get
unfold mkArray
simp [List.replicate]
rewrite [list_get_replicate]
-- FIXME: Merge this with the well-formed versions below so proof and code can
-- mesh seamlessly.
@[inline] def insert (map: Imp β) (v: β): (Imp β × Nat) :=
match map.lastDealloc with
| 0 => -- Capacity is full, buffer expansion is required
if map.size == map.data.size then
let nextIndex := map.data.size
let extendCapacity := map.size
let result: Imp β := {
data := (map.data.append #[Option.some v]).append (mkArray extendCapacity .none),
size := map.size + 1,
allocFront := map.size + 1,
deallocs := mkArray (map.data.size + 1 + extendCapacity) 0,
lastDealloc := 0,
}
(result, nextIndex)
else
let nextIndex := map.size
let result: Imp β := {
map
with
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
size := map.size + 1,
allocFront := map.allocFront + 1,
}
(result, nextIndex)
| (.succ k) => -- Allocation list has space
let nextIndex := map.deallocs.get! k
let result: Imp β := {
map with
data := map.data.set ⟨nextIndex, sorry⟩ (Option.some v),
size := map.size + 1,
lastDealloc := map.lastDealloc - 1
}
(result, nextIndex)
@[inline] def remove (map: Imp β) (index: Fin (map.size)): Imp β :=
have h: index.val < map.data.size := by sorry
match map.data.get ⟨index.val, h⟩ with
| .none => map
| .some _ =>
{
map with
data := map.data.set ⟨index, sorry⟩ .none,
size := map.size - 1,
deallocs := map.deallocs.set ⟨map.lastDealloc, sorry⟩ index,
lastDealloc := map.lastDealloc + 1,
}
/-- Retrieval is efficient -/
@[inline] def get? (map: Imp β) (index: Fin (map.size)): Option β :=
have h: index.val < map.data.size := by sorry
map.data.get ⟨index.val, h⟩
@[inline] def capacity (map: Imp β): Nat := map.data.size
end Imp
/--
This is like a hashmap but you cannot control the keys.
-/
def _root_.Pantograph.SemihashMap β := {m: Imp β // m.WF}
@[inline] def empty (capacity := 16): SemihashMap β :=
⟨ Imp.empty capacity, Imp.empty_wf ⟩
@[inline] def insert (map: SemihashMap β) (v: β): (SemihashMap β × Nat) :=
let ⟨imp, pre⟩ := map
let ⟨result, id⟩ := imp.insert v
( ⟨ result, sorry ⟩, id)
@[inline] def remove (map: SemihashMap β) (index: Nat): SemihashMap β :=
let ⟨imp, pre⟩ := map
let result := imp.remove ⟨index, sorry⟩
⟨ result, sorry ⟩
@[inline] def get? (map: SemihashMap β) (index: Nat): Option β :=
let ⟨imp, _⟩ := map
imp.get? ⟨index, sorry⟩
@[inline] def size (map: SemihashMap β): Nat :=
let ⟨imp, _⟩ := map
imp.size
end Pantograph.SemihashMap

View File

@ -1,214 +1,196 @@
/-
All serialisation functions;
This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
using `Scope`s.
All serialisation functions
-/
import Lean
import Pantograph.Condensed
import Pantograph.Expr
import Pantograph.Goal
import Pantograph.Protocol
open Lean
-- Symbol processing functions --
import Pantograph.Commands
namespace Pantograph
open Lean
--- Input Functions ---
/-- Read a theorem from the environment -/
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
/-- Read syntax object from string -/
def parseTerm (env: Environment) (s: String): Except String Syntax :=
def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory
(env := env)
(catName := `term)
(input := s)
(fileName := "<stdin>")
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
return Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := s)
(fileName := "<stdin>")
/-- Parse a syntax object. May generate additional metavariables! -/
def elabType (syn: Syntax): Elab.TermElabM (Except String Expr) := do
def syntax_to_expr_type (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)
def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElabM (Except String Expr) := do
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try
let expr ← Elab.Term.elabTerm (stx := syn) expectedType?
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none)
-- 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)
--- Output Functions ---
def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
def type_expr_to_bound (expr: Expr): MetaM Commands.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) }
def serializeName (name: Name) (sanitize: Bool := true): String :=
let internal := name.isInaccessibleUserName || name.hasMacroScopes
if sanitize && internal then "_"
else toString name |> addQuotes
where
addQuotes (n: String) :=
let quote := "\""
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
private def name_to_ast: Lean.Name → String
| .anonymous
| .num _ _ => ":anon"
| n@(.str _ _) => toString n
private def level_depth: Level → Nat
| .zero => 0
| .succ l => 1 + (level_depth l)
| .max u v | .imax u v => 1 + max (level_depth u) (level_depth v)
| .param _ | .mvar _ => 0
theorem level_depth_max_imax (u v: Level): (level_depth (Level.max u v) = level_depth (Level.imax u v)) := by
constructor
theorem level_max_depth_decrease (u v: Level): (level_depth u < level_depth (Level.max u v)) := by
have h1: level_depth (Level.max u v) = 1 + Nat.max (level_depth u) (level_depth v) := by constructor
rewrite [h1]
simp_arith
conv =>
rhs
apply Nat.max_def
sorry
theorem level_offset_decrease (u v: Level): (level_depth u ≤ level_depth (Level.max u v).getLevelOffset) := sorry
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
def serialize_sort_level_ast (level: Level): String :=
let k := level.getOffset
let u := level.getLevelOffset
let u_str := match u with
| .zero => "0"
| .succ _ => panic! "getLevelOffset should not return .succ"
| .max v w =>
let v := serializeSortLevel v sanitize
let w := serializeSortLevel w sanitize
let v := serialize_sort_level_ast v
let w := serialize_sort_level_ast w
s!"(:max {v} {w})"
| .imax v w =>
let v := serializeSortLevel v sanitize
let w := serializeSortLevel w sanitize
let v := serialize_sort_level_ast v
let w := serialize_sort_level_ast w
s!"(:imax {v} {w})"
| .param name =>
let name := serializeName name sanitize
let name := name_to_ast name
s!"{name}"
| .mvar id =>
let name := serializeName id.name sanitize
let name := name_to_ast id.name
s!"(:mv {name})"
match k, u with
| 0, _ => u_str
| _, .zero => s!"{k}"
| _, _ => s!"(+ {u_str} {k})"
termination_by serialize_sort_level_ast level => level_depth level
decreasing_by
. sorry
/--
Completely serializes an expression tree. Json not used due to compactness
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
-/
partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
self expr
where
delayedMVarToSexp (e: Expr): MetaM (Option String) := do
let .some invocation ← toDelayedMVarInvocation e | return .none
let callee ← self $ .mvar invocation.mvarIdPending
let sites ← invocation.args.mapM (λ (fvarId, arg) => do
let arg := match arg with
| .some arg => arg
| .none => .fvar fvarId
self arg
)
let tailArgs ← invocation.tail.mapM self
let sites := " ".intercalate sites.toList
let result := if tailArgs.isEmpty then
s!"(:subst {callee} {sites})"
else
let tailArgs := " ".intercalate tailArgs.toList
s!"((:subst {callee} {sites}) {tailArgs})"
return .some result
self (e: Expr): MetaM String := do
if let .some result ← delayedMVarToSexp e then
return result
match e with
def serialize_expression_ast (expr: Expr): MetaM String := do
match expr with
| .bvar deBruijnIndex =>
-- This is very common so the index alone is shown. Literals are handled below.
-- The raw de Bruijn index should never appear in an unbound setting. In
-- Lean these are handled using a `#` prefix.
pure s!"{deBruijnIndex}"
return s!"{deBruijnIndex}"
| .fvar fvarId =>
let name := ofName fvarId.name
pure s!"(:fv {name})"
| .mvar mvarId => do
let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
let name := ofName mvarId.name
pure s!"(:{pref} {name})"
let name := (← fvarId.getDecl).userName
return s!"(:fv {name})"
| .mvar mvarId =>
let name := name_to_ast mvarId.name
return s!"(:mv {name})"
| .sort level =>
let level := serializeSortLevel level sanitize
pure s!"(:sort {level})"
let level := serialize_sort_level_ast level
return s!"(:sort {level})"
| .const declName _ =>
-- The universe level of the const expression is elided since it should be
-- inferrable from surrounding expression
pure s!"(:c {declName})"
| .app _ _ => do
let fn' ← self e.getAppFn
let args := (← e.getAppArgs.mapM self) |>.toList
let args := " ".intercalate args
pure s!"({fn'} {args})"
| .lam binderName binderType body binderInfo => do
let binderName' := ofName binderName
let binderType' ← self binderType
let body' ← self body
let binderInfo' := binderInfoSexp binderInfo
pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
| .forallE binderName binderType body binderInfo => do
let binderName' := ofName binderName
let binderType' ← self binderType
let body' ← self body
let binderInfo' := binderInfoSexp binderInfo
pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
| .letE name type value body _ => do
return s!"(:c {declName})"
| .app fn arg =>
let fn' ← serialize_expression_ast fn
let arg' ← serialize_expression_ast arg
return s!"({fn'} {arg'})"
| .lam binderName binderType body binderInfo =>
let binderName' := name_to_ast binderName
let binderType' ← serialize_expression_ast binderType
let body' ← serialize_expression_ast body
let binderInfo' := binder_info_to_ast binderInfo
return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
| .forallE binderName binderType body binderInfo =>
let binderName' := name_to_ast binderName
let binderType' ← serialize_expression_ast binderType
let body' ← serialize_expression_ast body
let binderInfo' := binder_info_to_ast binderInfo
return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
| .letE name type value body _ =>
-- Dependent boolean flag diacarded
let name' := serializeName name
let type' ← self type
let value' ← self value
let body' ← self body
pure s!"(:let {name'} {type'} {value'} {body'})"
let name' := name_to_ast name
let type' ← serialize_expression_ast type
let value' ← serialize_expression_ast value
let body' ← serialize_expression_ast body
return s!"(:let {name'} {type'} {value'} {body'})"
| .lit v =>
-- To not burden the downstream parser who needs to handle this, the literal
-- is wrapped in a :lit sexp.
let v' := match v with
| .natVal val => toString val
| .strVal val => s!"\"{val}\""
pure s!"(:lit {v'})"
| .mdata _ inner =>
return s!"(:lit {v'})"
| .mdata _ expr =>
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-- It may become necessary to incorporate the metadata.
self inner
| .proj _ _ _ => do
let env ← getEnv
let projApp := exprProjToApp env e
let autos := String.intercalate " " (List.replicate projApp.numParams "_")
let inner ← self projApp.inner
pure s!"((:c {projApp.projector}) {autos} {inner})"
return (← serialize_expression_ast expr)
| .proj typeName idx struct =>
let struct' ← serialize_expression_ast struct
return s!"(:proj {typeName} {idx} {struct'})"
where
-- Elides all unhygenic names
binderInfoSexp : Lean.BinderInfo → String
binder_info_to_ast : Lean.BinderInfo → String
| .default => ""
| .implicit => " :implicit"
| .strictImplicit => " :strictImplicit"
| .instImplicit => " :instImplicit"
ofName (name: Name) := serializeName name sanitize
def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
let pp?: Option String ← match options.printExprPretty with
| true => pure $ .some $ toString $ ← Meta.ppExpr e
| false => pure $ .none
let sexp?: Option String ← match options.printExprAST with
| true => pure $ .some $ ← serializeExpressionSexp e
| false => pure $ .none
let dependentMVars? ← match options.printDependentMVars with
| true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
| false => pure $ .none
def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do
let pp := toString (← Meta.ppExpr e)
let pp?: Option String := match options.printExprPretty with
| true => .some pp
| false => .none
let sexp: String := (← serialize_expression_ast e)
let sexp?: Option String := match options.printExprAST with
| true => .some sexp
| false => .none
return {
pp?,
sexp?
dependentMVars?,
}
/-- Adapted from ppGoal -/
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
: MetaM Protocol.Goal := do
def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Commands.Goal := do
-- Options for printing; See Meta.ppGoal for details
let showLetValues := true
let ppAuxDecls := options.printAuxDecls
@ -216,44 +198,39 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
Meta.withLCtx lctx mvarDecl.localInstances do
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
match localDecl with
| .cdecl _ fvarId userName _ _ _ =>
| .cdecl _ _ varName _ _ _ =>
let varName := varName.simpMacroScopes
return {
name := ofName fvarId.name,
userName:= ofName userName.simpMacroScopes,
isInaccessible := userName.isInaccessibleUserName
name := toString varName,
}
| .ldecl _ fvarId userName _ _ _ _ => do
| .ldecl _ _ varName _ _ _ _ => do
return {
name := ofName fvarId.name,
userName := toString userName.simpMacroScopes,
isInaccessible := userName.isInaccessibleUserName
name := toString varName,
}
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
match localDecl with
| .cdecl _ fvarId userName type _ _ =>
let userName := userName.simpMacroScopes
let type ← instantiate type
| .cdecl _ _ varName type _ _ =>
let varName := varName.simpMacroScopes
let type ← instantiateMVars type
return {
name := ofName fvarId.name,
userName:= ofName userName,
isInaccessible := userName.isInaccessibleUserName
type? := .some (← serializeExpression options type)
name := toString varName,
isInaccessible? := .some varName.isInaccessibleUserName
type? := .some (← serialize_expression options type)
}
| .ldecl _ fvarId userName type val _ _ => do
let userName := userName.simpMacroScopes
let type ← instantiate type
| .ldecl _ _ varName type val _ _ => do
let varName := varName.simpMacroScopes
let type ← instantiateMVars type
let value? ← if showLetValues then
let val ← instantiate val
pure $ .some (← serializeExpression options val)
let val ← instantiateMVars val
pure $ .some (← serialize_expression options val)
else
pure $ .none
return {
name := ofName fvarId.name,
userName:= ofName userName,
isInaccessible := userName.isInaccessibleUserName
type? := .some (← serializeExpression options type)
name := toString varName,
isInaccessible? := .some varName.isInaccessibleUserName
type? := .some (← serialize_expression options type)
value? := value?
}
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
@ -262,101 +239,21 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
if skip then
return acc
else
let nameOnly := options.noRepeat && (parentDecl?.map
let nameOnly := options.proofVariableDelta && (parentDecl?.map
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
let var ← match nameOnly with
| true => ppVarNameOnly localDecl
| false => ppVar localDecl
return var::acc
return {
name := ofName goal.name,
userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serializeExpression options (← instantiate mvarDecl.type)),
caseName? := match mvarDecl.userName with
| Name.anonymous => .none
| name => .some <| toString name,
isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
vars := vars.reverse.toArray
}
where
instantiate := instantiateAll
ofName (n: Name) := serializeName n (sanitize := false)
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 parentDecl? := parent.bind (λ parentState => parentState.mctx.findDecl? state.parentMVar?.get!)
goals.mapM fun goal => do
match state.mctx.findDecl? goal with
| .some mvarDecl =>
let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
pure serializedGoal
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
/-- Print the metavariables in a readable format -/
@[export pantograph_goal_state_diag_m]
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
let metaM: MetaM String := do
goalState.restoreMetaM
let savedState := goalState.savedState
let goals := savedState.tactic.goals
let mctx ← getMCtx
let root := goalState.root
-- Print the root
let result: String ← match mctx.decls.find? root with
| .some decl => printMVar ">" root decl
| .none => pure s!">{root.name}: ??"
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
match mctx.decls.find? mvarId with
| .some decl => printMVar "⊢" mvarId decl
| .none => pure s!"⊢{mvarId.name}: ??"
)
let goals := goals.toSSet
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
!(goals.contains mvarId || mvarId == root) && options.printAll)
|>.mapM (fun (mvarId, decl) => do
let pref := if parentHasMVar mvarId then " " else "~"
printMVar pref mvarId decl
)
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
metaM.run' {}
where
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
let resultFVars: List String ←
if options.printContext then
decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) =>
do pure $ (← printFVar fvarId decl) ++ "\n")
else
pure []
let type ← if options.instantiate
then instantiateAll decl.type
else pure $ decl.type
let type_sexp ← if options.printSexp then
let sexp ← serializeExpressionSexp type (sanitize := false)
pure <| " " ++ sexp
else
pure ""
let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}"
let resultValue: String ←
if options.printValue then
if let .some value ← getExprMVarAssignment? mvarId then
let value ← if options.instantiate
then instantiateAll value
else pure $ value
pure s!"\n := {← Meta.ppExpr value}"
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
pure s!"\n ::= {mvarIdPending.name}"
else
pure ""
else
pure ""
pure $ (String.join resultFVars) ++ resultMain ++ resultValue
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do
pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
userNameToString : Name → String
| .anonymous => ""
| other => s!"[{other}]"
parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
end Pantograph

38
Pantograph/Symbols.lean Normal file
View File

@ -0,0 +1,38 @@
/-
- Manages the visibility status of symbols
-/
import Lean.Declaration
namespace Pantograph
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"
| _ => true
let stemDeduce: Bool := match n with
| .anonymous => true
| .str _ name => name.startsWith "_"
| .num _ _ => true
nameDeduce stemDeduce info.isUnsafe
def to_compact_symbol_name (n: Lean.Name) (info: Lean.ConstantInfo): String :=
let pref := match info with
| .axiomInfo _ => "axiom"
| .defnInfo _ => "defn"
| .thmInfo _ => "thm"
| .opaqueInfo _ => "opaque"
| .quotInfo _ => "quot"
| .inductInfo _ => "induct"
| .ctorInfo _ => "ctor"
| .recInfo _ => "rec"
s!"{pref}|{toString n}"
def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :=
if is_symbol_unsafe_or_internal n info
then Option.none
else Option.some <| to_compact_symbol_name n info
end Pantograph

View File

@ -1,5 +1,102 @@
import Pantograph.Tactic.Assign
import Pantograph.Tactic.Congruence
import Pantograph.Tactic.MotivatedApply
import Pantograph.Tactic.NoConfuse
import Pantograph.Tactic.Prograde
import Lean
import Pantograph.Symbols
import Pantograph.Serial
/-
The proof state manipulation system
A proof state is launched by providing
1. Environment: `Environment`
2. Expression: `Expr`
The expression becomes the first meta variable in the saved tactic state
`Elab.Tactic.SavedState`.
From this point on, any proof which extends
`Elab.Term.Context` and
-/
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
{
msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.error => true | _ => false
}
namespace Pantograph
open Lean
structure GoalState where
mvarId: MVarId
savedState : Elab.Tactic.SavedState
abbrev M := Elab.TermElabM
def GoalState.create (expr: Expr): M GoalState := 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 {
savedState := savedState,
mvarId := goal.mvarId!
}
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
Elab.Tactic.setGoals [goal]
try
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 (← MonadBacktrack.saveState, ← Elab.Tactic.getUnsolvedGoals)
catch exception =>
return .error #[← exception.toMessageData.toString]
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
/-- Response for executing a tactic -/
inductive TacticResult where
-- Goes to next state
| success (goals: Array (GoalState × Commands.Goal))
-- Fails with messages
| failure (messages: Array String)
namespace TacticResult
def is_success: TacticResult → Bool
| .success _ => true
| .failure _ => false
end TacticResult
/-- Execute tactic on given state -/
def GoalState.execute (goal: GoalState) (tactic: String):
Commands.OptionsT M TacticResult := do
let options ← read
match (← execute_tactic (state := goal.savedState) (goal := goal.mvarId) (tactic := tactic)) with
| .error errors =>
return .failure errors
| .ok (nextState, nextGoals) =>
if nextGoals.isEmpty then
return .success #[]
else
let nextGoals: List GoalState := nextGoals.map fun mvarId => { mvarId, savedState := nextState }
let parentDecl? := (← MonadMCtx.getMCtx).findDecl? goal.mvarId
let goals ← nextGoals.mapM fun nextGoal => do
match (← MonadMCtx.getMCtx).findDecl? nextGoal.mvarId with
| .some mvarDecl =>
let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
return (nextGoal, serializedGoal)
| .none => throwError nextGoal.mvarId
return .success goals.toArray
end Pantograph

View File

@ -1,31 +0,0 @@
import Lean
open Lean
namespace Pantograph.Tactic
/-- WARNING: This should be used with a function like `elabTermWithHoles` that properly collects the mvar information from `expr`. -/
def assign (goal: MVarId) (expr: Expr) (nextGoals: List MVarId): MetaM (List MVarId) := do
goal.checkNotAssigned `Pantograph.Tactic.assign
-- This run of the unifier is critical in resolving mvars in passing
let exprType ← Meta.inferType expr
let goalType ← goal.getType
unless ← Meta.isDefEq goalType exprType do
throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
goal.assign expr
nextGoals.filterM (not <$> ·.isAssigned)
def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
let target ← Elab.Tactic.getMainTarget
let goal ← Elab.Tactic.getMainGoal
goal.checkNotAssigned `Pantograph.Tactic.evalAssign
let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx
(expectedType? := .some target)
(tagSuffix := .anonymous )
(allowNaturalHoles := true)
goal.assign expr
Elab.Tactic.replaceMainGoal nextGoals
end Pantograph.Tactic

View File

@ -1,98 +0,0 @@
import Lean
open Lean
namespace Pantograph.Tactic
def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceArg
let target ← mvarId.getType
let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
let userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
(tag := userName ++ `α)
let f ← Meta.mkFreshExprSyntheticOpaqueMVar (.forallE .anonymous α β .default)
(tag := userName ++ `f)
let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
(tag := userName ++ `a₁)
let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
(tag := userName ++ `a₂)
let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
(tag := userName ++ `h)
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) target
let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
(tag := userName ++ `conduit)
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h)
let result := [α, a₁, a₂, f, h, conduit]
return result.map (·.mvarId!)
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← congruenceArg goal
Elab.Tactic.replaceMainGoal nextGoals
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
let target ← mvarId.getType
let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
let userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
(tag := userName ++ `α)
let fType := .forallE .anonymous α β .default
let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
(tag := userName ++ `f₁)
let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
(tag := userName ++ `f₂)
let a ← Meta.mkFreshExprSyntheticOpaqueMVar α
(tag := userName ++ `a)
let h ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
(tag := userName ++ `h)
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) target
let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
(tag := userName ++ `conduit)
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a)
let result := [α, f₁, f₂, h, a, conduit]
return result.map (·.mvarId!)
def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← congruenceFun goal
Elab.Tactic.replaceMainGoal nextGoals
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
let target ← mvarId.getType
let .some (β, _, _) := (← instantiateMVars target).eq? | throwError "Goal is not an Eq"
let userName := (← mvarId.getDecl).userName
let u ← Meta.mkFreshLevelMVar
let α ← Meta.mkFreshExprSyntheticOpaqueMVar (mkSort u)
(tag := userName ++ `α)
let fType := .forallE .anonymous α β .default
let f₁ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
(tag := userName ++ `f₁)
let f₂ ← Meta.mkFreshExprSyntheticOpaqueMVar fType
(tag := userName ++ `f₂)
let a₁ ← Meta.mkFreshExprSyntheticOpaqueMVar α
(tag := userName ++ `a₁)
let a₂ ← Meta.mkFreshExprSyntheticOpaqueMVar α
(tag := userName ++ `a₂)
let h₁ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq f₁ f₂)
(tag := userName ++ `h₁)
let h₂ ← Meta.mkFreshExprSyntheticOpaqueMVar (← Meta.mkEq a₁ a₂)
(tag := userName ++ `h₂)
let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) target
let conduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType
(tag := userName ++ `conduit)
mvarId.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂)
let result := [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit]
return result.map (·.mvarId!)
def evalCongruence: Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← congruence goal
Elab.Tactic.replaceMainGoal nextGoals
end Pantograph.Tactic

View File

@ -1,106 +0,0 @@
import Lean
open Lean
namespace Pantograph.Tactic
def getForallArgsBody: Expr → List Expr × Expr
| .forallE _ d b _ =>
let (innerArgs, innerBody) := getForallArgsBody b
(d :: innerArgs, innerBody)
| e => ([], e)
def replaceForallBody: Expr → Expr → Expr
| .forallE param domain body binderInfo, target =>
let body := replaceForallBody body target
.forallE param domain body binderInfo
| _, target => target
structure RecursorWithMotive where
args: List Expr
body: Expr
-- .bvar index for the motive and major from the body
iMotive: Nat
namespace RecursorWithMotive
protected def nArgs (info: RecursorWithMotive): Nat := info.args.length
protected def getMotiveType (info: RecursorWithMotive): Expr :=
let level := info.nArgs - info.iMotive - 1
let a := info.args.get! level
a
protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
let motiveType := Expr.instantiateRev info.getMotiveType mvars
let resultantType ← Meta.inferType resultant
return replaceForallBody motiveType resultantType
protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do
let motiveCall := Expr.instantiateRev info.body mvars
Meta.mkEq motiveCall resultant
end RecursorWithMotive
def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do
let (args, body) := getForallArgsBody recursorType
if ¬ body.isApp then
.none
let iMotive ← match body.getAppFn with
| .bvar iMotive => pure iMotive
| _ => .none
return {
args,
body,
iMotive,
}
def collectMotiveArguments (forallBody: Expr): SSet Nat :=
match forallBody with
| .app (.bvar i) _ => SSet.empty.insert i
| _ => SSet.empty
/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/
def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.InductionSubgoal) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.motivatedApply
let recursorType ← Meta.inferType recursor
let resultant ← mvarId.getType
let tag ← mvarId.getTag
let info ← match getRecursorInformation recursorType with
| .some info => pure info
| .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}"
let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
if i ≥ info.nArgs then
return prev
else
let argType := info.args.get! i
-- If `argType` has motive references, its goal needs to be placed in it
let argType := argType.instantiateRev prev
let bvarIndex := info.nArgs - i - 1
let argGoal ← if bvarIndex = info.iMotive then
let surrogateMotiveType ← info.surrogateMotiveType prev resultant
Meta.mkFreshExprSyntheticOpaqueMVar surrogateMotiveType (tag := tag ++ `motive)
else
Meta.mkFreshExprSyntheticOpaqueMVar argType (tag := .anonymous)
let prev := prev ++ [argGoal]
go (i + 1) prev
termination_by info.nArgs - i
let mut newMVars ← go 0 #[]
-- Create the conduit type which proves the result of the motive is equal to the goal
let conduitType ← info.conduitType newMVars resultant
let goalConduit ← Meta.mkFreshExprSyntheticOpaqueMVar conduitType (tag := `conduit)
mvarId.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars)
newMVars := newMVars ++ [goalConduit]
return newMVars.map (λ mvar => { mvarId := mvar.mvarId!})
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
let recursor ← Elab.Term.elabTerm (stx := stx) .none
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
end Pantograph.Tactic

View File

@ -1,22 +0,0 @@
import Lean
open Lean
namespace Pantograph.Tactic
def noConfuse (mvarId: MVarId) (h: Expr): MetaM Unit := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.noConfuse
let target ← mvarId.getType
let noConfusion ← Meta.mkNoConfusion (target := target) (h := h)
unless ← Meta.isDefEq (← Meta.inferType noConfusion) target do
throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr target}"
mvarId.assign noConfusion
def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
let goal ← Elab.Tactic.getMainGoal
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
noConfuse goal h
Elab.Tactic.replaceMainGoal []
end Pantograph.Tactic

View File

@ -1,88 +0,0 @@
/- Prograde (forward) reasoning tactics -/
import Lean
open Lean
namespace Pantograph.Tactic
private def mkUpstreamMVar (goal: MVarId) : MetaM Expr := do
Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) (tag := ← goal.getTag)
/-- Introduces a fvar to the current mvar -/
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.define
let type ← Meta.inferType expr
Meta.withLetDecl binderName type expr λ fvar => do
let mvarUpstream ← mkUpstreamMVar mvarId
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
pure (fvar.fvarId!, mvarUpstream.mvarId!)
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
let (_, mvarId) ← define goal binderName expr
Elab.Tactic.replaceMainGoal [mvarId]
structure BranchResult where
fvarId?: Option FVarId := .none
branch: MVarId
main: MVarId
def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.have
let lctx ← MonadLCtx.getLCtx
-- The branch goal inherits the same context, but with a different type
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-- Create the context for the `upstream` goal
let fvarId ← mkFreshFVarId
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
let mvarUpstream ←
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
let mvarUpstream ← mkUpstreamMVar mvarId
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
pure mvarUpstream
return {
fvarId? := .some fvarId,
branch := mvarBranch.mvarId!,
main := mvarUpstream.mvarId!,
}
def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals: List MVarId ← goal.withContext do
let type ← Elab.Term.elabType (stx := type)
let result ← «have» goal binderName type
pure [result.branch, result.main]
Elab.Tactic.replaceMainGoal nextGoals
def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
mvarId.checkNotAssigned `Pantograph.Tactic.let
let lctx ← MonadLCtx.getLCtx
-- The branch goal inherits the same context, but with a different type
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName)
assert! ¬ type.hasLooseBVars
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
let mvarUpstream ← mkUpstreamMVar mvarId
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
pure mvarUpstream
return {
branch := mvarBranch.mvarId!,
main := mvarUpstream.mvarId!,
}
def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
let result ← «let» goal binderName type
Elab.Tactic.replaceMainGoal [result.branch, result.main]
end Pantograph.Tactic

View File

@ -1,6 +1,5 @@
namespace Pantograph
@[export pantograph_version]
def version := "0.2.19"
def version := "0.2.5"
end Pantograph

158
README.md
View File

@ -1,30 +1,29 @@
# Pantograph
A Machine-to-Machine interaction system for Lean 4.
An interaction system for Lean 4.
![Pantograph](doc/icon.svg)
Pantograph provides interfaces to execute proofs, construct expressions, and
examine the symbol list of a Lean project for machine learning.
## Installation
For Nix users, run
``` sh
nix build .#{sharedLib,executable}
```
to build either the shared library or executable.
Install `elan` and `lake`, and run
Install `elan` and `lean4`. Then, execute
``` sh
lake build
```
This builds the executable in `.lake/build/bin/pantograph-repl`.
Then, setup the `LEAN_PATH` environment variable so it contains the library path of lean libraries. The libraries must be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
``` sh
LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
## Executable Usage
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
```
Note that `lean-toolchain` must be present in the `$PWD` in order to run Pantograph! This is because Pantograph taps into Lean's internals.
## Usage
``` sh
pantograph MODULES|LEAN_OPTIONS
build/bin/pantograph MODULES|LEAN_OPTIONS
```
The REPL loop accepts commands as single-line JSON inputs and outputs either an
@ -34,84 +33,59 @@ result of a command execution. The command can be passed in one of two formats
command { ... }
{ "cmd": command, "payload": ... }
```
The list of available commands can be found in `Pantograph/Protocol.lean` and below. An
The list of available commands can be found in `Pantograph/Commands.lean` and below. An
empty command aborts the REPL.
The `pantograph` executable must be run with a list of modules to import. It can
The `Pantograph` executable must be run with a list of modules to import. It can
also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
Example: (~5k symbols)
```
$ pantograph Init
env.catalog
env.inspect {"name": "Nat.le_add_left"}
$ build/bin/Pantograph Init
lib.catalog
lib.inspect {"name": "Nat.le_add_left"}
```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
```
$ pantograph Mathlib.Analysis.Seminorm
env.catalog
$ lake env build/bin/Pantograph Mathlib.Analysis.Seminorm
lib.catalog
```
Example proving a theorem: (alternatively use `goal.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
```
$ pantograph Init
$ env build/bin/Pantograph Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"stateId": 0, "goalId": 0, "tactic": "intro n m"}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "assumption"}
goal.delete {"stateIds": [0]}
goal.tactic {"goalId": 0, "tactic": "intro n m"}
goal.tactic {"goalId": 1, "tactic": "assumption"}
goal.delete {"goalIds": [0]}
stat {}
goal.tactic {"stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
stat
```
where the application of `assumption` should lead to a failure.
### Commands
## Commands
See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON.
* `reset`: Delete all cached expressions and proof trees
* `stat`: Display resource usage
* `expr.echo {"expr": <expr>, "type": <optional expected type>, ["levels": [<levels>]]}`: Determine the
type of an expression and format it.
* `env.catalog`: Display a list of all safe Lean symbols in the current environment
* `env.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
See `Pantograph/Commands.lean` for a description of the parameters and return values in JSON.
- `reset`: Delete all cached expressions and proof trees
- `expr.echo {"expr": <expr>}`: Determine the type of an expression and round-trip it
- `lib.catalog`: Display a list of all safe Lean symbols in the current context
- `lib.inspect {"name": <name>, "value": <bool>}`: Show the type and package of a
given symbol; If value flag is set, the value is printed or hidden. By default
only the values of definitions are printed.
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
- `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
- `options.print`: Display the current set of options
- `goal.start {["name": <name>], ["expr": <expr>], ["copyFrom": <symbol>]}`: Start a new goal from a given expression or symbol
- `goal.tactic {"goalId": <id>, "tactic": <tactic>}`: Execute a tactic string on a given goal
- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals.
- `stat`: Display resource usage
One particular option for interest for machine learning researchers is the
automatic mode (flag: `"automaticMode"`). By default it is turned on, with
all goals automatically resuming. This makes Pantograph act like a gym,
with no resumption necessary to manage your goals.
* `options.print`: Display the current set of options
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
Start a new proof from a given expression or symbol
* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
- `{ "tactic": <tactic> }`: Execute an ordinary tactic
- `{ "expr": <expr> }`: Assign the given proof term to the current goal
- `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
- `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
to the previous `rhs`.
- `{ "conv": <bool> }`: Enter or exit conversion tactic mode. In the case of
exit, the goal id is ignored.
* `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`:
Execute continuation/resumption
- `{ "branch": <id> }`: Continue on branch state. The current state must have no goals.
- `{ "goals": <names> }`: Resume the given goals
* `goal.remove {"stateIds": [<id>]}"`: Drop the goal states specified in the list
* `goal.print {"stateId": <id>}"`: Print a goal state
* `frontend.process { ["fileName": <fileName>",] ["file": <str>], invocations:
<bool>, sorrys: <bool> }`: Executes the Lean frontend on a file, collecting
either the tactic invocations (`"invocations": true`) or the sorrys into goal
states (`"sorrys": true`)
### Errors
## Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
``` json
{ "error": "type", "desc": "description" }
{ error: "type", desc: "description" }
```
Common error forms:
* `command`: Indicates malformed command structure which results from either
@ -121,60 +95,16 @@ Common error forms:
input of another is broken. For example, attempting to query a symbol not
existing in the library or indexing into a non-existent proof state.
### Project Environment
To use Pantograph in a project environment, setup the `LEAN_PATH` environment
variable so it contains the library path of lean libraries. The libraries must
be built in advance. For example, if `mathlib4` is stored at `../lib/mathlib4`,
the environment might be setup like this:
``` sh
LIB="../lib"
LIB_MATHLIB="$LIB/mathlib4/lake-packages"
export LEAN_PATH="$LIB/mathlib4/build/lib:$LIB_MATHLIB/aesop/build/lib:$LIB_MATHLIB/Qq/build/lib:$LIB_MATHLIB/std/build/lib"
LEAN_PATH=$LEAN_PATH build/bin/pantograph $@
```
The `$LEAN_PATH` executable of any project can be extracted by
``` sh
lake env printenv LEAN_PATH
```
### Troubleshooting
## Troubleshooting
If lean encounters stack overflow problems when printing catalog, execute this before running lean:
```sh
ulimit -s unlimited
```
## Library Usage
## Testing
`Pantograph/Library.lean` exposes a series of interfaces which allow FFI call
with `Pantograph` which mirrors the REPL commands above. It is recommended to
call Pantograph via this FFI since it provides a tremendous speed up.
The executable can be used as-is, but linking against the shared library
requires the presence of `lean-all`. Note that there isn't a 1-1 correspondence
between executable (REPL) commands and library functions.
Inject any project path via the `pantograph_init_search` function.
## Developing
A Lean development shell is provided in the Nix flake.
### Testing
The tests are based on `LSpec`. To run tests, use either
The tests are based on `LSpec`. To run tests,
``` sh
nix flake check
```
or
``` sh
lake test
```
You can run an individual test by specifying a prefix
``` sh
lake test -- "Tactic/No Confuse"
test/all.sh
```

260
Repl.lean
View File

@ -1,260 +0,0 @@
import Std.Data.HashMap
import Pantograph
namespace Pantograph.Repl
structure Context where
imports: List String
/-- Stores state of the REPL -/
structure State where
options: Protocol.Options := {}
nextId: Nat := 0
goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
/-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α
def runMetaInMainM { α } (metaM: Lean.MetaM α): MainM α :=
metaM.run'
def runTermElabInMainM { α } (termElabM: Lean.Elab.TermElabM α) : MainM α :=
termElabM.run' (ctx := Condensed.elabContext) |>.run'
def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with
| .ok args => do
match (← comm args) with
| .ok result => return Lean.toJson result
| .error ierror => return Lean.toJson ierror
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with
| "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo
| "env.catalog" => run env_catalog
| "env.inspect" => run env_inspect
| "env.add" => run env_add
| "options.set" => run options_set
| "options.print" => run options_print
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete
| "goal.print" => run goal_print
| "frontend.process" => run frontend_process
| cmd =>
let error: Protocol.InteractionError :=
errorCommand s!"Unknown command {cmd}"
return Lean.toJson error
where
errorCommand := errorI "command"
errorIndex := errorI "index"
newGoalState (goalState: GoalState) : MainM Nat := do
let state ← get
let stateId := state.nextId
set { state with
goalStates := state.goalStates.insert stateId goalState,
nextId := state.nextId + 1
}
return stateId
-- Command Functions
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
set { state with nextId := 0, goalStates := .empty }
return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
return .ok { nGoals }
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
let result ← Environment.catalog args
return .ok result
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
let state ← get
Environment.inspect args state.options
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get
exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get
let options := state.options
set { state with
options := {
-- FIXME: This should be replaced with something more elegant
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST,
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
noRepeat := args.noRepeat?.getD options.noRepeat,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
automaticMode := args.automaticMode?.getD options.automaticMode,
}
}
return .ok { }
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
return .ok (← get).options
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabInMainM (match args.expr, args.copyFrom with
| .some expr, .none => goalStartExpr expr (args.levels.getD #[])
| .none, .some copyFrom =>
(match env.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")
match expr? with
| .error error => return .error error
| .ok goalState =>
let stateId ← newGoalState goalState
return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get
let .some goalState := state.goalStates[args.stateId]? |
return .error $ errorIndex s!"Invalid state index {args.stateId}"
let .some goal := goalState.goals.get? args.goalId |
return .error $ errorIndex s!"Invalid goal index {args.goalId}"
let nextGoalState?: Except _ TacticResult ← runTermElabInMainM do
match args.tactic?, args.expr?, args.have?, args.let?, args.calc?, args.conv? with
| .some tactic, .none, .none, .none, .none, .none => do
pure <| Except.ok <| ← goalState.tryTactic goal tactic
| .none, .some expr, .none, .none, .none, .none => do
pure <| Except.ok <| ← goalState.tryAssign goal expr
| .none, .none, .some type, .none, .none, .none => do
let binderName := args.binderName?.getD ""
pure <| Except.ok <| ← goalState.tryHave goal binderName type
| .none, .none, .none, .some type, .none, .none => do
let binderName := args.binderName?.getD ""
pure <| Except.ok <| ← goalState.tryLet goal binderName type
| .none, .none, .none, .none, .some pred, .none => do
pure <| Except.ok <| ← goalState.tryCalc goal pred
| .none, .none, .none, .none, .none, .some true => do
pure <| Except.ok <| ← goalState.conv goal
| .none, .none, .none, .none, .none, .some false => do
pure <| Except.ok <| ← goalState.convExit
| _, _, _, _, _, _ =>
let error := errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied"
pure $ Except.error $ error
match nextGoalState? with
| .error error => return .error error
| .ok (.success nextGoalState) => do
let nextGoalState ← match state.options.automaticMode, args.conv? with
| true, .none => do
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
throwError "Resuming known goals"
pure result
| true, .some true => pure nextGoalState
| true, .some false => do
let .some (_, _, dormantGoals) := goalState.convMVar? |
throwError "If conv exit succeeded this should not fail"
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
throwError "Resuming known goals"
pure result
| false, _ => pure nextGoalState
let nextStateId ← newGoalState nextGoalState
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return .ok {
nextStateId? := .some nextStateId,
goals? := .some goals,
}
| .ok (.parseError message) =>
return .ok { parseError? := .some message }
| .ok (.invalidAction message) =>
return .error $ errorI "invalid" message
| .ok (.failure messages) =>
return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
let .some target := state.goalStates[args.target]? |
return .error $ errorIndex s!"Invalid state index {args.target}"
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates[branchId]? with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with
| .error error => return .error <| errorI "structure" error
| .ok nextGoalState =>
let nextStateId := state.nextId
set { state with
goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1
}
let goals ← goalSerialize nextGoalState (options := state.options)
return .ok {
nextStateId,
goals,
}
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
set { state with goalStates }
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
let .some goalState := state.goalStates[args.stateId]? |
return .error $ errorIndex s!"Invalid state index {args.stateId}"
let result ← runMetaInMainM <| goalPrint goalState state.options
return .ok result
frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
let options := (← get).options
try
let (fileName, file) ← match args.fileName?, args.file? with
| .some fileName, .none => do
let file ← IO.FS.readFile fileName
pure (fileName, file)
| .none, .some file =>
pure ("<anonymous>", file)
| _, _ => return .error <| errorI "arguments" "Exactly one of {fileName, file} must be supplied"
let env?: Option Lean.Environment ← if args.fileName?.isSome then
pure .none
else do
let env ← Lean.MonadEnv.getEnv
pure <| .some env
let (context, state) ← do Frontend.createContextStateFromFile file fileName env? {}
let frontendM := Frontend.mapCompilationSteps λ step => do
let boundary := (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
let invocations?: Option (List Protocol.InvokedTactic) ← if args.invocations then
let invocations ← Frontend.collectTacticsFromCompilationStep step
pure $ .some invocations
else
pure .none
let sorrys := if args.sorrys then
Frontend.collectSorrys step
else
[]
let messages ← step.messageStrings
return (step.before, boundary, invocations?, sorrys, messages)
let li ← frontendM.run context |>.run' state
let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
let (goalStateId?, goals) ← if sorrys.isEmpty then do
pure (.none, #[])
else do
let goalState ← runMetaInMainM $ Frontend.sorrysToGoalState sorrys
let stateId ← newGoalState goalState
let goals ← goalSerialize goalState options
pure (.some stateId, goals)
return {
boundary,
invocations?,
goalStateId?,
goals,
messages,
}
return .ok { units }
catch e =>
return .error $ errorI "frontend" (← e.toMessageData.toString)
end Pantograph.Repl

View File

@ -1,155 +0,0 @@
import Pantograph.Goal
import Pantograph.Library
import Pantograph.Protocol
import Pantograph.Condensed
import Lean
import LSpec
open Lean
namespace Pantograph
deriving instance Repr for Expr
-- Use strict equality check for expressions
instance : BEq Expr := ⟨Expr.equal⟩
def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
-- Auxiliary functions
namespace Protocol
def Goal.devolatilizeVars (goal: Goal): Goal :=
{
goal with
vars := goal.vars.map removeInternalAux,
}
where removeInternalAux (v: Variable): Variable :=
{
v with
name := ""
}
/-- Set internal names to "" -/
def Goal.devolatilize (goal: Goal): Goal :=
{
goal.devolatilizeVars with
name := "",
}
deriving instance DecidableEq, Repr for Name
deriving instance DecidableEq, Repr for Expression
deriving instance DecidableEq, Repr for Variable
deriving instance DecidableEq, Repr for Goal
deriving instance DecidableEq, Repr for ExprEchoResult
deriving instance DecidableEq, Repr for InteractionError
deriving instance DecidableEq, Repr for Option
end Protocol
namespace Condensed
deriving instance BEq, Repr for LocalDecl
deriving instance BEq, Repr for Goal
protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
{
decl with fvarId := { name := .anonymous }
}
protected def Goal.devolatilize (goal: Goal): Goal :=
{
goal with
mvarId := { name := .anonymous },
context := goal.context.map LocalDecl.devolatilize
}
end Condensed
def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
def TacticResult.toString : TacticResult → String
| .success state => s!".success ({state.goals.length} goals)"
| .failure messages =>
let messages := "\n".intercalate messages.toList
s!".failure {messages}"
| .parseError error => s!".parseError {error}"
| .invalidAction error => s!".invalidAction {error}"
namespace Test
def expectationFailure (desc: String) (error: String): LSpec.TestSeq := LSpec.test desc (LSpec.ExpectationFailure "ok _" error)
def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
def parseFailure (error: String) := expectationFailure "parse" error
def elabFailure (error: String) := expectationFailure "elab" error
def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array String := #[]): IO LSpec.TestSeq := do
let coreContext: Core.Context ← createCoreContext options
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 runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
runCoreMSeq env metaM.run'
def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
termElabM.run' (ctx := Condensed.elabContext)
def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
let .ok stx := Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := s)
(fileName := filename) | panic! s!"Failed to parse {s}"
return stx
def parseSentence (s: String): Elab.TermElabM Expr := do
let stx ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := s)
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
Elab.Term.elabTerm (stx := stx) .none
def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
return newGoals.goals
def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
let name := (← mvarId.getDecl).userName
let t ← exprToStr (← mvarId.getType)
return (name, t)
-- Monadic testing
abbrev TestT := StateT LSpec.TestSeq
def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
set $ (← get) ++ test
def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
Prod.snd <$> t.run LSpec.TestSeq.done
def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
IO LSpec.TestSeq :=
runTermElabMSeq env $ runTest t
def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
{ userName, type }
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
Protocol.Goal :=
{
userName?,
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := .some { pp? := .some x.snd },
})).toArray
}
end Test
end Pantograph

View File

@ -1,107 +0,0 @@
import LSpec
import Pantograph.Serial
import Pantograph.Environment
import Test.Common
import Lean
open Lean
namespace Pantograph.Test.Environment
open Pantograph
deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorRule
deriving instance DecidableEq, Repr for Protocol.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
def test_catalog: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let inner: CoreM LSpec.TestSeq := do
let catalogResult ← Environment.catalog {}
let symbolsWithNum := env.constants.fold (init := #[]) (λ acc name info =>
match (Environment.toFilteredSymbol name info).isSome && (name matches .num _ _) with
| false => acc
| true => acc.push name
)
return LSpec.check "No num symbols" (symbolsWithNum.size == 0)
runCoreMSeq env inner
def test_symbol_visibility: IO LSpec.TestSeq := do
let entries: List (Name × Bool) := [
("Nat.add_comm".toName, false),
("foo.bla.Init.Data.List.Basic.2.1.Init.Lean.Expr._hyg.4".toName, true),
("Init.Data.Nat.Basic._auxLemma.4".toName, true),
]
let suite := entries.foldl (λ suites (symbol, target) =>
let test := LSpec.check symbol.toString ((Environment.isNameInternal symbol) == target)
LSpec.TestSeq.append suites test) LSpec.TestSeq.done
return suite
inductive ConstantCat where
| induct (info: Protocol.InductInfo)
| ctor (info: Protocol.ConstructorInfo)
| recursor (info: Protocol.RecursorInfo)
def test_inspect: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let testCases: List (String × ConstantCat) := [
("Or", ConstantCat.induct {
numParams := 2,
numIndices := 0,
all := #["Or"],
ctors := #["Or.inl", "Or.inr"],
}),
("Except.ok", ConstantCat.ctor {
induct := "Except",
cidx := 1,
numParams := 2,
numFields := 1,
}),
("Eq.rec", ConstantCat.recursor {
all := #["Eq"],
numParams := 2,
numIndices := 1,
numMotives := 1,
numMinors := 1,
rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
k := true,
}),
("ForM.rec", ConstantCat.recursor {
all := #["ForM"],
numParams := 3,
numIndices := 0,
numMotives := 1,
numMinors := 1,
rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
k := false,
})
]
let inner: CoreM LSpec.TestSeq := do
testCases.foldlM (λ acc (name, cat) => do
let args: Protocol.EnvInspect := { name := name }
let result ← match ← Environment.inspect args (options := {}) with
| .ok result => pure $ result
| .error e => panic! s!"Error: {e.desc}"
let p := match cat with
| .induct info => LSpec.test name (result.inductInfo? == .some info)
| .ctor info => LSpec.test name (result.constructorInfo? == .some info)
| .recursor info => LSpec.test name (result.recursorInfo? == .some info)
return LSpec.TestSeq.append acc p
) LSpec.TestSeq.done
runCoreMSeq env inner
def suite: List (String × IO LSpec.TestSeq) :=
[
("Catalog", test_catalog),
("Symbol Visibility", test_symbol_visibility),
("Inspect", test_inspect),
]
end Pantograph.Test.Environment

View File

@ -1,191 +0,0 @@
import LSpec
import Pantograph
import Repl
import Test.Common
open Lean Pantograph
namespace Pantograph.Test.Frontend
def collectSorrysFromSource (source: String) : MetaM (List GoalState) := do
let filename := "<anonymous>"
let (context, state) ← do Frontend.createContextStateFromFile source filename (← getEnv) {}
let m := Frontend.mapCompilationSteps λ step => do
return (step.before, Frontend.collectSorrys step)
let li ← m.run context |>.run' state
let goalStates ← li.filterMapM λ (env, sorrys) => withEnv env do
if sorrys.isEmpty then
return .none
let goalState ← Frontend.sorrysToGoalState sorrys
return .some goalState
return goalStates
def test_multiple_sorrys_in_proof : TestT MetaM Unit := do
let sketch := "
theorem plus_n_Sm_proved_formal_sketch : ∀ n m : Nat, n + (m + 1) = (n + m) + 1 := by
have h_nat_add_succ: ∀ n m : Nat, n = m := sorry
sorry
"
let goalStates ← (collectSorrysFromSource sketch).run' {}
let [goalState] := goalStates | panic! "Incorrect number of states"
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
{
target := { pp? := "∀ (n m : Nat), n = m" },
vars := #[
]
},
{
target := { pp? := "∀ (n m : Nat), n + (m + 1) = n + m + 1" },
vars := #[{
userName := "h_nat_add_succ",
type? := .some { pp? := "∀ (n m : Nat), n = m" },
}],
}
])
def test_sorry_in_middle: TestT MetaM Unit := do
let sketch := "
example : ∀ (n m: Nat), n + m = m + n := by
intros n m
sorry
"
let goalStates ← (collectSorrysFromSource sketch).run' {}
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
{
target := { pp? := "n + m = m + n" },
vars := #[{
userName := "n",
type? := .some { pp? := "Nat" },
}, {
userName := "m",
type? := .some { pp? := "Nat" },
}
],
}
])
def test_sorry_in_induction : TestT MetaM Unit := do
let sketch := "
example : ∀ (n m: Nat), n + m = m + n := by
intros n m
induction n with
| zero =>
have h1 : 0 + m = m := sorry
sorry
| succ n ih =>
have h2 : n + m = m := sorry
sorry
"
let goalStates ← (collectSorrysFromSource sketch).run' {}
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
{
target := { pp? := "0 + m = m" },
vars := #[{
userName := "m",
type? := .some { pp? := "Nat" },
}]
},
{
userName? := .some "zero",
target := { pp? := "0 + m = m + 0" },
vars := #[{
userName := "m",
type? := .some { pp? := "Nat" },
}, {
userName := "h1",
type? := .some { pp? := "0 + m = m" },
}]
},
{
target := { pp? := "n + m = m" },
vars := #[{
userName := "m",
type? := .some { pp? := "Nat" },
}, {
userName := "n",
type? := .some { pp? := "Nat" },
}, {
userName := "ih",
type? := .some { pp? := "n + m = m + n" },
}]
},
{
userName? := .some "succ",
target := { pp? := "n + 1 + m = m + (n + 1)" },
vars := #[{
userName := "m",
type? := .some { pp? := "Nat" },
}, {
userName := "n",
type? := .some { pp? := "Nat" },
}, {
userName := "ih",
type? := .some { pp? := "n + m = m + n" },
}, {
userName := "h2",
type? := .some { pp? := "n + m = m" },
}]
}
])
def test_sorry_in_coupled: TestT MetaM Unit := do
let sketch := "
example : ∀ (y: Nat), ∃ (x: Nat), y + 1 = x := by
intro y
apply Exists.intro
case h => sorry
case w => sorry
"
let goalStates ← (collectSorrysFromSource sketch).run' {}
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
{
target := { pp? := "y + 1 = ?w" },
vars := #[{
userName := "y",
type? := .some { pp? := "Nat" },
}
],
},
{
userName? := .some "w",
target := { pp? := "Nat" },
vars := #[{
userName := "y",
type? := .some { pp? := "Nat" },
}
],
}
])
def test_environment_capture: TestT MetaM Unit := do
let sketch := "
def mystery (n: Nat) := n + 1
example (n: Nat) : mystery n + 1 = n + 2 := sorry
"
let goalStates ← (collectSorrysFromSource sketch).run' {}
let [goalState] := goalStates | panic! s!"Incorrect number of states: {goalStates.length}"
addTest $ LSpec.check "goals" ((← goalState.serializeGoals (options := {})).map (·.devolatilize) = #[
{
target := { pp? := "mystery n + 1 = n + 2" },
vars := #[{
userName := "n",
type? := .some { pp? := "Nat" },
}],
}
])
def suite (env : Environment): List (String × IO LSpec.TestSeq) :=
let tests := [
("multiple_sorrys_in_proof", test_multiple_sorrys_in_proof),
("sorry_in_middle", test_sorry_in_middle),
("sorry_in_induction", test_sorry_in_induction),
("sorry_in_coupled", test_sorry_in_coupled),
("environment_capture", test_environment_capture),
]
tests.map (fun (name, test) => (name, runMetaMSeq env $ runTest test))
end Pantograph.Test.Frontend

View File

@ -2,257 +2,92 @@
-/
import LSpec
import Pantograph
import Repl
import Test.Common
namespace Pantograph.Test
open Pantograph
namespace Pantograph.Test.Integration
open Pantograph.Repl
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
(expected: Lean.Json): MainM LSpec.TestSeq := do
let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload }
return LSpec.test name (toString result = toString expected)
def subroutine_step (cmd: String) (payload: List (String × Lean.Json))
(expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected
def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
(expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
let payload := Lean.Json.mkObj payload
let name := name?.getD s!"{cmd} {payload.compress}"
let result ← Repl.execute { cmd, payload }
return LSpec.test name (toString result = toString (Lean.toJson expected))
abbrev Test := List (MainM LSpec.TestSeq)
def test_elab : Test :=
[
step "expr.echo"
[("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
(Lean.toJson ({
type := { pp? := .some "{α : Type u} → Type u" },
expr := { pp? := .some "fun {α} => List α" }
}: Protocol.ExprEchoResult)),
]
def test_option_modify : Test :=
let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"
let module? := Option.some "Init.Data.Nat.Basic"
let options: Protocol.Options := {}
[
step "env.inspect" [("name", .str "Nat.add_one")]
({ type := { pp? }, module? }: Protocol.EnvInspectResult),
step "options.set" [("printExprAST", .bool true)]
({ }: Protocol.OptionsSetResult),
step "env.inspect" [("name", .str "Nat.add_one")]
({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
step "options.print" []
({ options with printExprAST := true }: Protocol.Options),
]
def test_malformed_command : Test :=
let invalid := "invalid"
[
step invalid [("name", .str "Nat.add_one")]
({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
(name? := .some "Invalid Command"),
step "expr.echo" [(invalid, .str "Random garbage data")]
({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
Protocol.InteractionError)
(name? := .some "JSON Deserialization")
]
def test_tactic : Test :=
let goal1: Protocol.Goal := {
name := "_uniq.11",
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }}],
}
let goal2: Protocol.Goal := {
name := "_uniq.17",
target := { pp? := .some "x y → y x" },
vars := #[
{ name := "_uniq.10", userName := "x", type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
],
}
[
step "goal.start" [("expr", .str "∀ (p q: Prop), p q → q p")]
({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
step "goal.print" [("stateId", .num 1)]
({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
]
def test_automatic_mode (automatic: Bool): Test :=
let varsPQ := #[
{ name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
{ name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }}
]
let goal1: Protocol.Goal := {
name := "_uniq.17",
target := { pp? := .some "q p" },
vars := varsPQ ++ #[
{ name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p q" }}
],
}
let goal2l: Protocol.Goal := {
name := "_uniq.59",
userName? := .some "inl",
target := { pp? := .some "q p" },
vars := varsPQ ++ #[
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
],
}
let goal2r: Protocol.Goal := {
name := "_uniq.72",
userName? := .some "inr",
target := { pp? := .some "q p" },
vars := varsPQ ++ #[
{ name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
],
}
let goal3l: Protocol.Goal := {
name := "_uniq.78",
userName? := .some "inl.h",
target := { pp? := .some "p" },
vars := varsPQ ++ #[
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
],
}
[
step "options.set" [("automaticMode", .bool automatic)]
({}: Protocol.OptionsSetResult),
step "goal.start" [("expr", .str "∀ (p q: Prop), p q → q p")]
({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
]
def test_env_add_inspect : Test :=
let name1 := "Pantograph.mystery"
let name2 := "Pantograph.mystery2"
[
step "env.add"
[
("name", .str name1),
("type", .str "Prop → Prop → Prop"),
("value", .str "λ (a b: Prop) => Or a b"),
("isTheorem", .bool false)
]
({}: Protocol.EnvAddResult),
step "env.inspect" [("name", .str name1)]
({
value? := .some { pp? := .some "fun a b => a b" },
type := { pp? := .some "Prop → Prop → Prop" },
}:
Protocol.EnvInspectResult),
step "env.add"
[
("name", .str name2),
("type", .str "Nat → Int"),
("value", .str "λ (a: Nat) => a + 1"),
("isTheorem", .bool false)
]
({}: Protocol.EnvAddResult),
step "env.inspect" [("name", .str name2)]
({
value? := .some { pp? := .some "fun a => ↑a + 1" },
type := { pp? := .some "Nat → Int" },
}:
Protocol.EnvInspectResult)
]
example : ∀ (p: Prop), p → p := by
intro p h
exact h
def test_frontend_process : Test :=
[
let file := "example : ∀ (p q: Prop), p → p q := by\n intro p q h\n exact Or.inl h"
let goal1 := "p q : Prop\nh : p\n⊢ p q"
step "frontend.process"
[
("file", .str file),
("invocations", .bool true),
("sorrys", .bool false),
]
({
units := [{
boundary := (0, file.utf8ByteSize),
invocations? := .some [
{
goalBefore := "⊢ ∀ (p q : Prop), p → p q",
goalAfter := goal1,
tactic := "intro p q h",
usedConstants := #[],
},
{
goalBefore := goal1 ,
goalAfter := "",
tactic := "exact Or.inl h",
usedConstants := #["Or.inl"],
},
]
}],
}: Protocol.FrontendProcessResult),
]
example : 1 + 2 = 3 := rfl
example (p: Prop): p → p := by simp
def test_frontend_process_sorry : Test :=
let solved := "example : 1 + 2 = 3 := rfl\n"
let withSorry := "example (p: Prop): p → p := sorry"
[
let file := s!"{solved}{withSorry}"
let goal1: Protocol.Goal := {
name := "_uniq.6",
target := { pp? := .some "p → p" },
vars := #[{ name := "_uniq.4", userName := "p", type? := .some { pp? := .some "Prop" }}],
}
step "frontend.process"
[
("file", .str file),
("invocations", .bool false),
("sorrys", .bool true),
]
({
units := [{
boundary := (0, solved.utf8ByteSize),
}, {
boundary := (solved.utf8ByteSize, solved.utf8ByteSize + withSorry.utf8ByteSize),
goalStateId? := .some 0,
goals := #[goal1],
messages := #["<anonymous>:2:0: warning: declaration uses 'sorry'\n"],
}],
}: Protocol.FrontendProcessResult),
]
def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do
-- Setup the environment for execution
let env ← Lean.importModules
(imports := [{module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
(opts := {})
(trustLevel := 1)
let context: Context := {
imports := ["Init"]
}
let coreContext: Lean.Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [],
fileName := "<Test>",
fileMap := { source := "", positions := #[0], lines := #[1] },
options := Lean.Options.empty
}
let commands: MainM LSpec.TestSeq :=
steps.foldlM (λ suite step => do
let result ← step
return suite ++ result) LSpec.TestSeq.done
runCoreMSeq env <| commands.run context |>.run' {}
try
let termElabM := 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 })
catch ex =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
let tests := [
("expr.echo", test_elab),
("options.set options.print", test_option_modify),
("Malformed command", test_malformed_command),
("Tactic", test_tactic),
("Manual Mode", test_automatic_mode false),
("Automatic Mode", test_automatic_mode true),
("env.add env.inspect", test_env_add_inspect),
("frontend.process invocation", test_frontend_process),
("frontend.process sorry", test_frontend_process_sorry),
def test_option_modify : IO LSpec.TestSeq :=
let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
let sexp? := Option.some "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"
let module? := Option.some "Init.Data.Nat.Basic"
let options: Commands.Options := {}
subroutine_runner [
subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp? }, module? }:
Commands.LibInspectResult)),
subroutine_step "options.set"
[("printExprAST", .bool true)]
(Lean.toJson ({ }:
Commands.OptionsSetResult)),
subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp?, sexp? }, module? }:
Commands.LibInspectResult)),
subroutine_step "options.print"
[]
(Lean.toJson ({ options with printExprAST := true }:
Commands.OptionsPrintResult))
]
tests.map (fun (name, test) => (name, runTest env test))
def test_malformed_command : IO LSpec.TestSeq :=
let invalid := "invalid"
subroutine_runner [
subroutine_named_step "Invalid command" invalid
[("name", .str "Nat.add_one")]
(Lean.toJson ({
error := "command", desc := s!"Unknown command {invalid}"}:
Commands.InteractionError)),
subroutine_named_step "JSON Deserialization" "expr.echo"
[(invalid, .str "Random garbage data")]
(Lean.toJson ({
error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}:
Commands.InteractionError))
]
def test_integration: IO LSpec.TestSeq := do
return LSpec.group "Integration" $
(LSpec.group "Option modify" (← test_option_modify)) ++
(LSpec.group "Malformed command" (← test_malformed_command))
end Pantograph.Test.Integration
end Pantograph.Test

View File

@ -1,38 +0,0 @@
import LSpec
import Lean
import Pantograph.Library
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Library
def test_expr_echo (env: Environment): IO LSpec.TestSeq := do
let inner: CoreM LSpec.TestSeq := do
let prop_and_proof := "⟨∀ (x: Prop), x → x, λ (x: Prop) (h: x) => h⟩"
let tests := LSpec.TestSeq.done
let echoResult ← exprEcho prop_and_proof (options := {})
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := { pp? := "?m.2" }, expr := { pp? := "?m.3" }
}))
let echoResult ← exprEcho prop_and_proof (expectedType? := .some "Σ' p:Prop, p") (options := { printExprAST := true })
let tests := tests.append (LSpec.test "fail" (echoResult.toOption == .some {
type := {
pp? := "(p : Prop) ×' p",
sexp? := "((:c PSigma) (:sort 0) (:lambda p (:sort 0) 0))",
},
expr := {
pp? := "⟨∀ (x : Prop), x → x, fun x h => h⟩",
sexp? := "((:c PSigma.mk) (:sort 0) (:lambda p (:sort 0) 0) (:forall x (:sort 0) (:forall _ 0 1)) (:lambda x (:sort 0) (:lambda h 0 0)))",
}
}))
return tests
runCoreMSeq env (options := #["pp.proofs.threshold=100"]) inner
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("expr_echo", test_expr_echo env),
]
end Pantograph.Test.Library

View File

@ -1,60 +1,18 @@
import LSpec
import Test.Environment
import Test.Frontend
import Test.Integration
import Test.Library
import Test.Metavar
import Test.Proofs
import Test.Serial
import Test.Tactic
-- Test running infrastructure
namespace Pantograph.Test
def addPrefix (pref: String) (tests: List (String × α)): List (String × α) :=
tests.map (λ (name, x) => (pref ++ "/" ++ name, x))
/-- Runs test in parallel. Filters test name if given -/
def runTestGroup (filter: Option String) (tests: List (String × IO LSpec.TestSeq)): IO LSpec.TestSeq := do
let tests: List (String × IO LSpec.TestSeq) := match filter with
| .some filter => tests.filter (λ (name, _) => filter.isPrefixOf name)
| .none => tests
let tasks: List (String × Task _) ← tests.mapM (λ (name, task) => do
return (name, ← EIO.asTask task))
let all := tasks.foldl (λ acc (name, task) =>
let v: Except IO.Error LSpec.TestSeq := Task.get task
match v with
| .ok case => acc ++ (LSpec.group name case)
| .error e => acc ++ (expectationFailure name e.toString)
) LSpec.TestSeq.done
return all
end Pantograph.Test
open Pantograph.Test
/-- Main entry of tests; Provide an argument to filter tests by prefix -/
def main (args: List String) := do
let name_filter := args.head?
unsafe def main := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot)
let env_default: Lean.Environment ← Lean.importModules
(imports := #[`Init])
(opts := {})
(trustLevel := 1)
let suites: List (String × List (String × IO LSpec.TestSeq)) := [
("Environment", Environment.suite),
("Frontend", Frontend.suite env_default),
("Integration", Integration.suite env_default),
("Library", Library.suite env_default),
("Metavar", Metavar.suite env_default),
("Proofs", Proofs.suite env_default),
("Serial", Serial.suite env_default),
("Tactic/Congruence", Tactic.Congruence.suite env_default),
("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default),
("Tactic/No Confuse", Tactic.NoConfuse.suite env_default),
("Tactic/Prograde", Tactic.Prograde.suite env_default),
let suites := [
test_integration,
test_proofs,
test_serial
]
let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) []
LSpec.lspecIO (← runTestGroup name_filter tests)
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
LSpec.lspecIO $ all

View File

@ -1,285 +0,0 @@
import LSpec
import Pantograph.Goal
import Pantograph.Serial
import Test.Common
import Lean
namespace Pantograph.Test.Metavar
open Pantograph
open Lean
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
def addTest (test: LSpec.TestSeq): TestM Unit := do
set $ (← get) ++ test
-- Tests that all delay assigned mvars are instantiated
def test_instantiate_mvar: TestM Unit := do
let env ← Lean.MonadEnv.getEnv
let value := "@Nat.le_trans 2 2 5 (@of_eq_true (@LE.le Nat instLENat 2 2) (@eq_true (@LE.le Nat instLENat 2 2) (@Nat.le_refl 2))) (@of_eq_true (@LE.le Nat instLENat 2 5) (@eq_true_of_decide (@LE.le Nat instLENat 2 5) (@Nat.decLe 2 5) (@Eq.refl Bool Bool.true)))"
let syn ← match parseTerm env value with
| .ok s => pure $ s
| .error e => do
addTest $ assertUnreachable e
return ()
let expr ← match ← elabTerm syn with
| .ok expr => pure $ expr
| .error e => do
addTest $ assertUnreachable e
return ()
let t ← Lean.Meta.inferType expr
addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
"((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
return ()
def startProof (expr: String): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
let syn? := parseTerm env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← elabType syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
return Option.none
| .ok expr =>
let goal ← GoalState.create (expr := expr)
return Option.some goal
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
{
userName?,
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := .some { pp? := .some x.snd },
})).toArray
}
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let coreContext: Lean.Core.Context ← createCoreContext #[]
let metaM := termElabM.run' (ctx := Condensed.elabContext)
let coreM := metaM.run'
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok (_, a) =>
return a
/-- M-coupled goals -/
def test_m_couple: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-- Set m to 3
let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state2.continue state1 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 3", .some "3 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
def test_m_couple_simp: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
#[#["_uniq.38"], #["_uniq.38"], #[]])
let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
let state1b ← match state2.continue state1 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 2", .some "2 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state4 ← match state3.continue state1b with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
state5.restoreMetaM
let root ← match state5.rootExpr? with
| .some e => pure e
| .none =>
addTest $ assertUnreachable "(5 root)"
return ()
let rootStr: String := toString (← Lean.Meta.ppExpr root)
addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
let unfoldedRoot ← unfoldAuxLemmas root
addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) =
"Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))")
return ()
def test_proposition_generation: TestM Unit := do
let state? ← startProof "Σ' p:Prop, p"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[
buildGoal [] "?fst" (userName? := .some "snd"),
buildGoal [] "Prop" (userName? := .some "fst")
])
if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then
addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "?m.29 x"])
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
let assign := "Eq.refl x"
let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
#[])
addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
return ()
def test_partial_continuation: TestM Unit := do
let state? ← startProof "(2: Nat) ≤ 5"
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "apply Nat.succ" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "Nat"])
-- Execute a partial continuation
let coupled_goals := state1.goals ++ state2.goals
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 ≤ ?m.succ", .some "?m.succ ≤ 5", .some "Nat"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
-- Roundtrip
--let coupled_goals := coupled_goals.map (λ g =>
-- { name := str_to_name $ serializeName g.name (sanitize := false)})
let coupled_goals := coupled_goals.map (λ g => serializeName 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 ≤ ?m.succ", .some "?m.succ ≤ 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 [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
-- Continuation should fail if some goals have not been solved
match state2.continue state1 with
| .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Target state has unresolved goals")
| .ok _ => addTest $ assertUnreachable "(continuation failure)"
return ()
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
let tests := [
("Instantiate", test_instantiate_mvar),
("2 < 5", test_m_couple),
("2 < 5", test_m_couple_simp),
("Proposition Generation", test_proposition_generation),
("Partial Continuation", test_partial_continuation)
]
tests.map (fun (name, test) => (name, proofRunner env test))
end Pantograph.Test.Metavar

View File

@ -1,12 +1,8 @@
/-
Tests pertaining to goals with no interdependencies
-/
import LSpec
import Pantograph.Goal
import Pantograph.Tactic
import Pantograph.Serial
import Test.Common
namespace Pantograph.Test.Proofs
namespace Pantograph.Test
open Pantograph
open Lean
@ -14,17 +10,21 @@ inductive Start where
| copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options Elab.TermElabM)
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
def addTest (test: LSpec.TestSeq): TestM Unit := do
deriving instance DecidableEq, Repr for Commands.Expression
deriving instance DecidableEq, Repr for Commands.Variable
deriving instance DecidableEq, Repr for Commands.Goal
def add_test (test: LSpec.TestSeq): TestM Unit := do
set $ (← get) ++ test
def startProof (start: Start): TestM (Option GoalState) := do
def start_proof (start: Start): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
match start with
| .copy name =>
let cInfo? := name.toName |> env.find?
addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
let cInfo? := str_to_name name |> env.find?
add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with
| .some cInfo =>
let goal ← GoalState.create (expr := cInfo.type)
@ -32,15 +32,15 @@ def startProof (start: Start): TestM (Option GoalState) := do
| .none =>
return Option.none
| .expr expr =>
let syn? := parseTerm env expr
addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
let syn? := syntax_from_str env expr
add_test $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with
| .error error =>
IO.println error
return Option.none
| .ok syn =>
let expr? ← elabType syn
addTest $ LSpec.check s!"Elaborating" expr?.isOk
let expr? ← syntax_to_expr syn
add_test $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with
| .error error =>
IO.println error
@ -49,169 +49,72 @@ def startProof (start: Start): TestM (Option GoalState) := do
let goal ← GoalState.create (expr := expr)
return Option.some goal
def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
(userName?: Option String := .none): Protocol.Goal :=
def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
{
name,
userName?,
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
name := x.fst,
type? := .some { pp? := .some x.snd },
isInaccessible? := .some false
})).toArray
}
def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
Protocol.Goal :=
-- Like `build_goal` but allow certain variables to be elided.
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
{
userName?,
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := .some { pp? := .some x.snd },
name := x.fst,
type? := x.snd.map (λ type => { pp? := type }),
isInaccessible? := x.snd.map (λ _ => false)
})).toArray
}
def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let coreContext: Lean.Core.Context ← createCoreContext #[]
let metaM := termElabM.run' (ctx := Condensed.elabContext)
let coreM := metaM.run'
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_identity: TestM Unit := do
let state? ← startProof (.expr "∀ (p: Prop), p → p")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro p h"
let state1 ← match ← state0.tacticOn 0 tactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let inner := "_uniq.12"
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) =
#[inner])
let state1parent ← state1.withParentContext do
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))")
-- Individual test cases
example: ∀ (a b: Nat), a + b = b + a := by
intro n m
rw [Nat.add_comm]
def test_nat_add_comm (manual: Bool): TestM Unit := do
let state? ← startProof <| match manual with
| false => .copy "Nat.add_comm"
| true => .expr "∀ (a b: Nat), a + b = b + a"
addTest $ LSpec.check "Start goal" state?.isSome
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
def proof_nat_add_comm: TestM Unit := do
let goal? ← start_proof (.copy "Nat.add_comm")
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
let state1 ← match ← state0.tacticOn 0 "intro n m" with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
if let .failure #[message] ← goal.execute "assumption" then
add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
else
add_test $ assert_unreachable "assumption"
match ← state1.tacticOn 0 "assumption" with
| .failure #[message] =>
addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
| other => do
addTest $ assertUnreachable $ other.toString
if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
return ()
else
add_test $ assert_unreachable "rw [Nat.add_comm]"
else
add_test $ assert_unreachable "intro n m"
def proof_nat_add_comm_manual: TestM Unit := do
let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then
let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
add_test $ LSpec.check "intro n m" (sGoal = sGoal1e)
let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "rw [Nat.add_comm]" state2.goals.isEmpty
if let .failure #[message] ← goal.execute "assumption" then
add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
else
add_test $ assert_unreachable "assumption"
if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
return ()
def test_delta_variable: TestM Unit := do
let options: Protocol.Options := { noRepeat := true }
let state? ← startProof <| .expr "∀ (a b: Nat), a + b = b + a"
addTest $ LSpec.check "Start goal" state?.isSome
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
else
add_test $ assert_unreachable "rw [Nat.add_comm]"
else
add_test $ assert_unreachable "intro n m"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
#[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intro m" ((← state2.serializeGoals (parent := state1) options).map (·.devolatilize) =
#[buildGoalSelective [("n", .none), ("m", .some "Nat")] "n + m = m + n"])
return ()
where
-- Like `buildGoal` but allow certain variables to be elided.
buildGoalSelective (nameType: List (String × Option String)) (target: String): Protocol.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
userName := x.fst,
type? := x.snd.map (λ type => { pp? := type }),
})).toArray
}
example (w x y z : Nat) (p : Nat → Prop)
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
assumption
def test_arith: TestM Unit := do
let state? ← startProof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intros"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic (state1.goals.length = 1)
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let tactic := "assumption"
let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test tactic state3.goals.isEmpty
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
return ()
-- Two ways to write the same theorem
example: ∀ (p q: Prop), p q → q p := by
@ -228,497 +131,122 @@ example: ∀ (p q: Prop), p q → q p := by
assumption
. apply Or.inl
assumption
def test_or_comm: TestM Unit := do
let state? ← startProof (.expr "∀ (p q: Prop), p q → q p")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
let tactic := "intro p q h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let fvP := "_uniq.10"
let fvQ := "_uniq.13"
let fvH := "_uniq.16"
let state1g0 := "_uniq.17"
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
#[{
name := state1g0,
def proof_or_comm: TestM Unit := do
let typeProp: Commands.Expression := { pp? := .some "Prop" }
let branchGoal (caseName name: String): Commands.Goal := {
caseName? := .some caseName,
target := { pp? := .some "q p" },
vars := #[
{ name := fvP, userName := "p", type? := .some { pp? := .some "Prop" } },
{ name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" } },
{ name := fvH, userName := "h", type? := .some { pp? := .some "p q" } }
]
}])
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
let state1parent ← state1.withParentContext do
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
let tactic := "cases h"
let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[branchGoal "inl" "p", branchGoal "inr" "q"])
let (caseL, caseR) := ("_uniq.64", "_uniq.77")
addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
#[caseL, caseR])
addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let state2parent ← state2.withParentContext do
serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))"
let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))"
let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))"
let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))"
addTest $ LSpec.test "(2 parent)" (state2parent ==
s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state3_1parent ← state3_1.withParentContext do
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_2.goals.isEmpty
addTest $ LSpec.check "(4_2 root)" state4_2.rootExpr?.isNone
-- Ensure the proof can continue from `state4_2`.
let state2b ← match state4_2.continue state2 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isSome
return ()
where
typeProp: Protocol.Expression := { pp? := .some "Prop" }
branchGoal (caseName varName: String): Protocol.Goal := {
userName? := .some caseName,
target := { pp? := .some "q p" },
vars := #[
{ userName := "p", type? := .some typeProp },
{ userName := "q", type? := .some typeProp },
{ userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible := true }
{ name := "p", type? := .some typeProp, isInaccessible? := .some false },
{ name := "q", type? := .some typeProp, isInaccessible? := .some false },
{ name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
]
}
let goal? ← start_proof (.expr "∀ (p q: Prop), p q → q p")
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
if let .success #[(goal, sGoal)] ← goal.execute "intro p q h" then
let sGoal1e := build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"
add_test $ LSpec.check "intro p q h" (sGoal = sGoal1e)
example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
intro a b c1 c2 h
conv =>
lhs
congr
. rw [Nat.add_comm]
. rfl
exact h
if let .success #[(goal1, sGoal1), (goal2, sGoal2)] ← goal.execute "cases h" then
add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p")
if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then
if let .success #[] ← goal.execute "assumption" then
return ()
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "apply Or.inr"
def test_conv: TestM Unit := do
let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro a b c1 c2 h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
add_test $ LSpec.check "cases h/2" (sGoal2 = branchGoal "inr" "q")
if let .success #[(goal, _)] ← goal2.execute "apply Or.inl" then
if let .success #[] ← goal.execute "assumption" then
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "a + b + c1 = b + a + c2"])
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "apply Or.inl"
let state2 ← match ← state1.conv (state1.get! 0) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
else
add_test $ assert_unreachable "cases h"
else
add_test $ assert_unreachable "intro p q h"
let convTactic := "rhs"
let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
example (w x y z : Nat) (p : Nat → Prop)
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
assumption
def proof_arith_1: TestM Unit := do
let goal? ← start_proof (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)")
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
if let .success #[(goal, _)] ← goal.execute "intros" then
if let .success #[(goal, _)] ← goal.execute "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *" then
if let .success #[] ← goal.execute "assumption" then
return ()
addTest $ LSpec.check s!" {convTactic} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
#[{ interiorGoal [] "b + a + c2" with isConversion := true }])
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "simp ..."
else
add_test $ assert_unreachable "intros"
let convTactic := "lhs"
let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
#[{ interiorGoal [] "a + b + c1" with isConversion := true }])
def proof_delta_variable: TestM Unit := withReader (fun _ => {proofVariableDelta := true}) do
let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a")
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
if let .success #[(goal, sGoal)] ← goal.execute "intro n" then
let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"
add_test $ LSpec.check "intro n" (sGoal = sGoal1e)
let convTactic := "congr"
let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
#[
{ interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
{ interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
])
if let .success #[(_, sGoal)] ← goal.execute "intro m" then
let sGoal2e: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n"
add_test $ LSpec.check "intro m" (sGoal = sGoal2e)
else
add_test $ assert_unreachable "intro m"
else
add_test $ assert_unreachable "intro n"
let convTactic := "rw [Nat.add_comm]"
let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
let convTactic := "rfl"
let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[])
let state4_1 ← match state6_1.continue state4 with
| .ok state => pure state
| .error e => do
addTest $ expectationFailure "continue" e
return ()
let convTactic := "rfl"
let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!" · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
#[])
let state1_1 ← match ← state6.convExit with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let tactic := "exact h"
let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) =
#[])
where
h := "b + a + c1 = b + a + c2"
interiorGoal (free: List (String × String)) (target: String) :=
let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
buildGoal free target
example : ∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d := by
intro a b c d h1 h2
calc a + b = b + c := by apply h1
_ = c + d := by apply h2
def test_calc: TestM Unit := do
let state? ← startProof (.expr "∀ (a b c d: Nat), a + b = b + c → b + c = c + d → a + b = c + d")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro a b c d h1 h2"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "a + b = c + d"])
let pred := "a + b = b + c"
let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[
interiorGoal [] "a + b = b + c" (.some "calc"),
interiorGoal [] "b + c = c + d"
])
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
let tactic := "apply h1"
let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state3 ← match state2m.continue state2 with
| .ok state => pure state
| .error e => do
addTest $ expectationFailure "continue" e
return ()
let pred := "_ = c + d"
let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"calc {pred} := _" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
#[
interiorGoal [] "b + c = c + d" (.some "calc")
])
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
let tactic := "apply h2"
let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(4m root)" state4m.rootExpr?.isSome
where
interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) :=
let free := [("a", "Nat"), ("b", "Nat"), ("c", "Nat"), ("d", "Nat"),
("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free
buildGoal free target userName?
def test_nat_zero_add: TestM Unit := do
let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro n"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat")] "n + 0 = n"])
let recursor := "@Nat.brecOn"
let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
])
let tactic := "exact n"
let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) =
#[])
let state2b ← match state3b.continue state2 with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
let tactic := "exact (λ x => x + 0 = x)"
let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) =
#[])
let state2c ← match state3c.continue state2b with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
let tactic := "intro t h"
let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
let tactic := "simp"
let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let state2d ← match state3d.continue state2c with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
let tactic := "rfl"
let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) =
#[])
let expr := stateF.mctx.eAssignment.find! stateF.root
let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr)
addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome
def test_nat_zero_add_alt: TestM Unit := do
let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n")
let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let tactic := "intro n"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat")] "n + 0 = n"])
let recursor := "@Nat.brecOn"
let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let major := "_uniq.68"
addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
#[
buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
buildNamedGoal major [("n", "Nat")] "Nat",
buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
])
let tactic := "intro x"
let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
let tactic := "apply Eq"
let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
let state2b ← match state3m2.resume [conduit] with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
let fvN := "_uniq.63"
let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
#[
{
name := "_uniq.70",
userName? := .some "conduit",
target := {
pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
},
vars := #[{
name := fvN,
userName := "n",
type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
}],
let coreContext: Lean.Core.Context := {
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
}
])
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
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 suite (env: Environment): List (String × IO LSpec.TestSeq) :=
def test_proofs : IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let tests := [
("identity", test_identity),
("Nat.add_comm", test_nat_add_comm false),
("Nat.add_comm manual", test_nat_add_comm true),
("Nat.add_comm delta", test_delta_variable),
("arithmetic", test_arith),
("Or.comm", test_or_comm),
("conv", test_conv),
("calc", test_calc),
("Nat.zero_add", test_nat_zero_add),
("Nat.zero_add alt", test_nat_zero_add_alt),
("Nat.add_comm", proof_nat_add_comm),
("nat.add_comm manual", proof_nat_add_comm_manual),
("Or.comm", proof_or_comm),
("arithmetic 1", proof_arith_1),
("delta variable", proof_delta_variable)
]
tests.map (fun (name, test) => (name, proofRunner env test))
let tests ← tests.foldlM (fun acc tests => do
let (name, tests) := tests
let tests ← proof_runner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Proofs" tests
end Pantograph.Test
end Pantograph.Test.Proofs

View File

@ -1,109 +1,76 @@
import LSpec
import Pantograph.Serial
import Test.Common
import Lean
import Pantograph.Symbols
open Lean
namespace Pantograph.Test.Serial
namespace Pantograph.Test
open Pantograph
open Lean
deriving instance Repr, DecidableEq for Protocol.BoundExpression
deriving instance Repr, DecidableEq for Commands.BoundExpression
def test_serializeName: LSpec.TestSeq :=
let quote := "\""
let escape := "\\"
LSpec.test "a.b.1" (serializeName (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
LSpec.test "seg.«a.b»" (serializeName (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
-- Pathological test case
LSpec.test s!"«̈{escape}{quote}»" (serializeName (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
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_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
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", "n.succ ≤ m")], target := "n ≤ m" })
let entries: List (String × Commands.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" })
]
runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do
let coreM := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := env.find? symbol |>.get! |>.type
let test := LSpec.check symbol.toString ((← typeExprToBound expr) = target)
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 := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph/Test>",
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_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [
-- This one contains unhygienic variable names which must be suppressed
("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
("Nat.add", "(:forall :anon (:c Nat) (:forall :anon (:c Nat) (:c Nat)))"),
-- These ones are normal and easy
("Nat.add_one", "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))"),
("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h ((:c LE.le) (:c Nat) (:c instLENat) ((:c Nat.succ) 1) 0) ((:c LE.le) (:c Nat) (:c instLENat) 2 1)) :implicit) :implicit)"),
("Nat.add_one", "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"),
("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)"),
-- Handling of higher order types
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
]
runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := env.find? symbol.toName |>.get! |>.type
let test := LSpec.check symbol ((← serializeExpressionSexp expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let expr := str_to_name symbol |> env.find? |>.get! |>.type
let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
let coreM := metaM.run'
let coreContext: Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva"
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph/Test>",
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_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × (List Name) × String) := [
("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"),
("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"),
]
entries.foldlM (λ suites (source, levels, target) =>
let termElabM := do
let env ← MonadEnv.getEnv
let s ← match parseTerm env source with
| .ok s => pure s
| .error e => return parseFailure e
let expr ← match (← elabTerm s) with
| .ok expr => pure expr
| .error e => return elabFailure e
return LSpec.check source ((← serializeExpressionSexp expr) = target)
let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
LSpec.TestSeq.done
def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
let entries: List (Expr × String) := [
(.lam `p (.sort .zero)
(.lam `q (.sort .zero)
(.lam `k (mkApp2 (.const `And []) (.bvar 1) (.bvar 0))
(.proj `And 1 (.bvar 0))
.default)
.implicit)
.implicit,
"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
),
]
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
let env ← MonadEnv.getEnv
let testCaseName := target.take 10
let test := LSpec.check testCaseName ((← serializeExpressionSexp expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)
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)
-- Instance parsing
def test_instance (env: Environment): IO LSpec.TestSeq :=
runMetaMSeq env do
let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
let s := parseTerm env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
return LSpec.TestSeq.done
return LSpec.group "Serialisation" $
(LSpec.group "str_to_name" test_str_to_name) ++
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("serializeName", do pure test_serializeName),
("Expression binder", test_expr_to_binder env),
("Sexp from symbol", test_sexp_of_symbol env),
("Sexp from elaborated expr", test_sexp_of_elab env),
("Sexp from expr", test_sexp_of_expr env),
("Instance", test_instance env),
]
end Pantograph.Test.Serial
end Pantograph.Test

View File

@ -1,4 +0,0 @@
import Test.Tactic.Congruence
import Test.Tactic.MotivatedApply
import Test.Tactic.NoConfuse
import Test.Tactic.Prograde

View File

@ -1,88 +0,0 @@
import LSpec
import Lean
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Tactic.Congruence
def test_congr_arg_list : TestT Elab.TermElabM Unit := do
let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[
(`α, "Sort ?u.30"),
(`a₁, "?α"),
(`a₂, "?α"),
(`f, "?α → List α"),
(`h, "?a₁ = ?a₂"),
(`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
])
let f := newGoals.get! 3
let h := newGoals.get! 4
let c := newGoals.get! 5
let results ← Meta.withAssignableSyntheticOpaque do f.apply (← parseSentence "List.reverse")
addTest $ LSpec.check "apply" (results.length = 0)
addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
def test_congr_arg : TestT Elab.TermElabM Unit := do
let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let newGoals ← runTacticOnMVar Tactic.evalCongruenceArg target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[
(`α, "Sort ?u.70"),
(`a₁, "?α"),
(`a₂, "?α"),
(`f, "?α → Nat"),
(`h, "?a₁ = ?a₂"),
(`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
])
def test_congr_fun : TestT Elab.TermElabM Unit := do
let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let newGoals ← runTacticOnMVar Tactic.evalCongruenceFun target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[
(`α, "Sort ?u.159"),
(`f₁, "?α → Nat"),
(`f₂, "?α → Nat"),
(`h, "?f₁ = ?f₂"),
(`a, "?α"),
(`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
])
def test_congr : TestT Elab.TermElabM Unit := do
let expr := "λ (a b: Nat) => a = b"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let newGoals ← runTacticOnMVar Tactic.evalCongruence target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[
(`α, "Sort ?u.10"),
(`f₁, "?α → Nat"),
(`f₂, "?α → Nat"),
(`a₁, "?α"),
(`a₂, "?α"),
(`h₁, "?f₁ = ?f₂"),
(`h₂, "?a₁ = ?a₂"),
(`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
])
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("congrArg List.reverse", test_congr_arg_list),
("congrArg", test_congr_arg),
("congrFun", test_congr_fun),
("congr", test_congr),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
end Pantograph.Test.Tactic.Congruence

View File

@ -1,113 +0,0 @@
import LSpec
import Lean
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Tactic.MotivatedApply
def test_type_extract : TestT Elab.TermElabM Unit := do
let recursor ← parseSentence "@Nat.brecOn"
let recursorType ← Meta.inferType recursor
addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
(← exprToStr recursorType))
let info ← match Tactic.getRecursorInformation recursorType with
| .some info => pure info
| .none => throwError "Failed to extract recursor info"
addTest $ LSpec.check "iMotive" (info.iMotive = 2)
let motiveType := info.getMotiveType
addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
(← exprToStr motiveType))
def test_nat_brec_on : TestT Elab.TermElabM Unit := do
let expr := "λ (n t: Nat) => n + 0 = n"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "@Nat.brecOn")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
-- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalMotivatedApply recursor
let newGoals ← runTacticOnMVar tactic target.mvarId!
let test := LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[
"Nat → Prop",
"Nat",
"∀ (t : Nat), Nat.below t → ?motive t",
"?motive ?m.67 = (n + 0 = n)",
])
addTest test
def test_list_brec_on : TestT Elab.TermElabM Unit := do
let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "@List.brecOn")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
-- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalMotivatedApply recursor
let newGoals ← runTacticOnMVar tactic target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[
"Type ?u.90",
"List ?m.92 → Prop",
"List ?m.92",
"∀ (t : List ?m.92), List.below t → ?motive t",
"?motive ?m.94 = (l ++ [] = [] ++ l)",
])
def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
let expr := "λ (n t: Nat) => n + 0 = n"
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "@Nat.brecOn")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
-- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalMotivatedApply recursor
let newGoals ← runTacticOnMVar tactic target.mvarId!
let majorId := 67
addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
[
"Nat → Prop",
"Nat",
"∀ (t : Nat), Nat.below t → ?motive t",
s!"?motive ?m.{majorId} = (n + 0 = n)",
]))
let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
-- Assign motive to `λ x => x + _`
let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
motive.assign motive_assign
addTest $ ← conduit.withContext do
let t := toString (← Meta.ppExpr $ ← conduit.getType)
return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("type_extract", test_type_extract),
("Nat.brecOn", test_nat_brec_on),
("List.brecOn", test_list_brec_on),
("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
end Pantograph.Test.Tactic.MotivatedApply

View File

@ -1,72 +0,0 @@
import LSpec
import Lean
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Tactic.NoConfuse
def test_nat : TestT Elab.TermElabM Unit := do
let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "h")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
-- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalNoConfuse recursor
let newGoals ← runTacticOnMVar tactic target.mvarId!
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
def test_nat_fail : TestT Elab.TermElabM Unit := do
let expr := "λ (n: Nat) (h: n = n) => False"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "h")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
-- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
try
let tactic := Tactic.evalNoConfuse recursor
let _ ← runTacticOnMVar tactic target.mvarId!
addTest $ assertUnreachable "Tactic should fail"
catch _ =>
addTest $ LSpec.check "Tactic should fail" true
def test_list : TestT Elab.TermElabM Unit := do
let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let recursor ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "h")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
-- Apply the tactic
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let tactic := Tactic.evalNoConfuse recursor
let newGoals ← runTacticOnMVar tactic target.mvarId!
addTest $ LSpec.check "goals"
((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("Nat", test_nat),
("Nat fail", test_nat_fail),
("List", test_list),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
end Pantograph.Test.Tactic.NoConfuse

View File

@ -1,300 +0,0 @@
import LSpec
import Lean
import Test.Common
open Lean
open Pantograph
namespace Pantograph.Test.Tactic.Prograde
def test_define : TestT Elab.TermElabM Unit := do
let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
let expr ← parseSentence expr
Meta.forallTelescope expr $ λ _ body => do
let e ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := "Or.inl h")
(fileName := filename) with
| .ok syn => pure syn
| .error error => throwError "Failed to parse: {error}"
-- Apply the tactic
let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
let target: Expr := mkAnd
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
let h := .fvar ⟨uniq 8⟩
addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
context := #[
cdeclOf `p (.sort 0),
cdeclOf `q (.sort 0),
cdeclOf `h h
],
target,
})
let tactic := Tactic.evalDefine `h2 e
let m := .mvar ⟨uniq 13⟩
let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
context := #[
cdeclOf `p (.sort 0),
cdeclOf `q (.sort 0),
cdeclOf `h h,
{
userName := `h2,
type := mkOr h m,
value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
}
],
target,
})
let .some e ← getExprMVarAssignment? goal.mvarId! | panic! "Tactic must assign"
addTest $ LSpec.test "assign" e.isLet
def test_define_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro p q h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"])
let expr := "Or.inl (Or.inl h)"
let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
#[])
let evalBind := "y"
let evalExpr := "Or.inl h"
let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"eval {evalBind} := {evalExpr}" ((← state2.serializeGoals).map (·.devolatilize) =
#[{
target := { pp? := .some "(p q) p q"},
vars := #[
{ userName := "p", type? := .some { pp? := .some "Prop" } },
{ userName := "q", type? := .some { pp? := .some "Prop" } },
{ userName := "h", type? := .some { pp? := .some "p" } },
{ userName := "y",
type? := .some { pp? := .some "p ?m.25" },
value? := .some { pp? := .some "Or.inl h" },
}
]
}])
let expr := "Or.inl y"
let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
#[])
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
intro p x
apply x.fst
exact 5
def test_define_root_expr : TestT Elab.TermElabM Unit := do
--let rootExpr ← parseSentence "Nat"
--let state0 ← GoalState.create rootExpr
--let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
--let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
--addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
let state0 ← GoalState.create rootExpr
let tactic := "intro p x"
let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
let binderName := `binder
let value := "x.fst"
let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
let tacticM := Tactic.evalDefine binderName expr
let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
let tactic := s!"apply {binderName}"
let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
let tactic := s!"exact 5"
let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5")
--set_option pp.all true
--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
--def test_define_root_expr : TestT Elab.TermElabM Unit := do
def test_have_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro p q h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"])
let expr := "Or.inl (Or.inl h)"
let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
#[])
let haveBind := "y"
let haveType := "p q"
let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) =
#[
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p q",
buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p q")] "(p q) p q"
])
let expr := "Or.inl h"
let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
#[])
let state2b ← match state3.continue state2 with
| .ok state => pure state
| .error e => do
addTest $ assertUnreachable e
return ()
let expr := "Or.inl y"
let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
#[])
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr
let tactic := "intro a p h"
let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
#[{
target := { pp? := .some mainTarget },
vars := interiorVars,
}])
let letType := "Nat"
let expr := s!"let b: {letType} := _; _"
let result2 ← match specialized with
| true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
| false => state1.tryAssign (state1.get! 0) (expr := expr)
let state2 ← match result2 with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
let serializedState2 ← state2.serializeGoals
let letBindName := if specialized then "b" else "_1"
addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) =
#[{
target := { pp? := .some letType },
vars := interiorVars,
userName? := .some letBindName
},
{
target := { pp? := .some mainTarget },
vars := interiorVars ++ #[{
userName := "b",
type? := .some { pp? := .some letType },
value? := .some { pp? := .some s!"?{letBindName}" },
}],
userName? := if specialized then .none else .some "_2",
}
])
let tactic := "exact 1"
let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[])
let state3r ← match state3.continue state2 with
| .error msg => do
addTest $ assertUnreachable $ msg
return ()
| .ok state => pure state
addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) =
#[
{
target := { pp? := .some mainTarget },
vars := interiorVars ++ #[{
userName := "b",
type? := .some { pp? := .some "Nat" },
value? := .some { pp? := .some "1" },
}],
userName? := if specialized then .none else .some "_2",
}
])
let tactic := "exact h"
match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
| .failure #[message] =>
addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop")
| other => do
addTest $ assertUnreachable $ other.toString
let tactic := "exact Or.inl (Or.inl h)"
let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome
where
mainTarget := "(a p) a p"
interiorVars: Array Protocol.Variable := #[
{ userName := "a", type? := .some { pp? := .some "Prop" }, },
{ userName := "p", type? := .some { pp? := .some "Prop" }, },
{ userName := "h", type? := .some { pp? := .some "a" }, }
]
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("define", test_define),
("define proof", test_define_proof),
("define root expr", test_define_root_expr),
("have proof", test_have_proof),
("let via assign", test_let false),
("let via tryLet", test_let true),
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
end Pantograph.Test.Tactic.Prograde

3
Test/all.sh Executable file
View File

@ -0,0 +1,3 @@
#!/bin/bash
lake build test && lake env build/bin/test

View File

@ -1,169 +0,0 @@
{
"nodes": {
"flake-parts": {
"inputs": {
"nixpkgs-lib": "nixpkgs-lib"
},
"locked": {
"lastModified": 1709336216,
"narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
"owner": "hercules-ci",
"repo": "flake-parts",
"rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
"type": "github"
},
"original": {
"owner": "hercules-ci",
"repo": "flake-parts",
"type": "github"
}
},
"flake-utils": {
"locked": {
"lastModified": 1656928814,
"narHash": "sha256-RIFfgBuKz6Hp89yRr7+NR5tzIAbn52h8vT6vXkYjZoM=",
"owner": "numtide",
"repo": "flake-utils",
"rev": "7e2a3b3dfd9af950a856d66b0a7d01e3c18aa249",
"type": "github"
},
"original": {
"owner": "numtide",
"repo": "flake-utils",
"type": "github"
}
},
"lean": {
"inputs": {
"flake-utils": "flake-utils",
"nixpkgs": "nixpkgs",
"nixpkgs-cadical": "nixpkgs-cadical",
"nixpkgs-old": "nixpkgs-old"
},
"locked": {
"lastModified": 1727749878,
"narHash": "sha256-O2Egyh2D0TfQWzQKfHUeAh7qAjMfeLVwXwGUw5QqcvE=",
"owner": "leanprover",
"repo": "lean4",
"rev": "dc2533473114eb8656439ff2b9335209784aa640",
"type": "github"
},
"original": {
"owner": "leanprover",
"ref": "v4.12.0",
"repo": "lean4",
"type": "github"
}
},
"lspec": {
"flake": false,
"locked": {
"lastModified": 1728279187,
"narHash": "sha256-ZMqbvCqR/gHXRuIkuo7b0Yp9N1vOQR7xnrcy/SeIBoQ=",
"owner": "argumentcomputer",
"repo": "LSpec",
"rev": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
"type": "github"
},
"original": {
"owner": "argumentcomputer",
"ref": "504a8cecf8da601b9466ac727aebb6b511aae4ab",
"repo": "LSpec",
"type": "github"
}
},
"nixpkgs": {
"locked": {
"lastModified": 1686089707,
"narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-cadical": {
"locked": {
"lastModified": 1722221733,
"narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
},
"original": {
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "12bf09802d77264e441f48e25459c10c93eada2e",
"type": "github"
}
},
"nixpkgs-lib": {
"locked": {
"dir": "lib",
"lastModified": 1709237383,
"narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
"type": "github"
},
"original": {
"dir": "lib",
"owner": "NixOS",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs-old": {
"flake": false,
"locked": {
"lastModified": 1581379743,
"narHash": "sha256-i1XCn9rKuLjvCdu2UeXKzGLF6IuQePQKFt4hEKRU5oc=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "34c7eb7545d155cc5b6f499b23a7cb1c96ab4d59",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixos-19.03",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs_2": {
"locked": {
"lastModified": 1711703276,
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
"owner": "nixos",
"repo": "nixpkgs",
"rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
"type": "github"
},
"original": {
"owner": "nixos",
"ref": "nixos-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"root": {
"inputs": {
"flake-parts": "flake-parts",
"lean": "lean",
"lspec": "lspec",
"nixpkgs": "nixpkgs_2"
}
}
},
"root": "root",
"version": 7
}

View File

@ -1,96 +0,0 @@
{
description = "Pantograph";
inputs = {
nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
flake-parts.url = "github:hercules-ci/flake-parts";
lean = {
# Do not follow input's nixpkgs since it could cause build failures
url = "github:leanprover/lean4?ref=v4.12.0";
};
lspec = {
url = "github:argumentcomputer/LSpec?ref=504a8cecf8da601b9466ac727aebb6b511aae4ab";
flake = false;
};
};
outputs = inputs @ {
self,
nixpkgs,
flake-parts,
lean,
lspec,
...
} : flake-parts.lib.mkFlake { inherit inputs; } {
flake = {
};
systems = [
"x86_64-linux"
"x86_64-darwin"
];
perSystem = { system, pkgs, ... }: let
leanPkgs = lean.packages.${system}.deprecated;
lspecLib = leanPkgs.buildLeanPackage {
name = "LSpec";
roots = [ "Main" "LSpec" ];
src = "${lspec}";
};
project = leanPkgs.buildLeanPackage {
name = "Pantograph";
roots = [ "Pantograph" ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path) &&
!(pkgs.lib.hasSuffix "Repl.lean" path);
});
};
repl = leanPkgs.buildLeanPackage {
name = "Repl";
roots = [ "Main" "Repl" ];
deps = [ project ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path);
});
};
test = leanPkgs.buildLeanPackage {
name = "Test";
# NOTE: The src directory must be ./. since that is where the import
# root begins (e.g. `import Test.Environment` and not `import
# Environment`) and thats where `lakefile.lean` resides.
roots = [ "Test.Main" ];
deps = [ lspecLib repl ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "Pantograph" path);
});
};
in rec {
packages = {
inherit (leanPkgs) lean lean-all;
inherit (project) sharedLib;
inherit (repl) executable;
default = repl.executable;
};
legacyPackages = {
inherit project leanPkgs;
};
checks = {
test = pkgs.runCommand "test" {
buildInputs = [ test.executable leanPkgs.lean-all ];
} ''
#export LEAN_SRC_PATH="${./.}"
${test.executable}/bin/test > $out
'';
};
devShells.default = pkgs.mkShell {
buildInputs = [ leanPkgs.lean-all leanPkgs.lean ];
};
};
};
}

View File

@ -1,15 +1,11 @@
{"version": "1.1.0",
"packagesDir": ".lake/packages",
{"version": 5,
"packagesDir": "lake-packages",
"packages":
[{"url": "https://github.com/lenianiva/LSpec.git",
"type": "git",
"subDir": null,
"scope": "",
"rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
[{"git":
{"url": "https://github.com/lurk-lab/LSpec.git",
"subDir?": null,
"rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
"opts": {},
"name": "LSpec",
"manifestFile": "lake-manifest.json",
"inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "pantograph",
"lakeDir": ".lake"}
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
"inherited": false}}]}

View File

@ -4,26 +4,21 @@ open Lake DSL
package pantograph
lean_lib Pantograph {
roots := #[`Pantograph]
defaultFacets := #[LeanLib.sharedFacet]
}
lean_lib Repl {
}
@[default_target]
lean_exe repl {
lean_exe pantograph {
root := `Main
-- Solves the native symbol not found problem
-- Somehow solves the native symbol not found problem
supportInterpreter := true
}
require LSpec from git
"https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
"https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
lean_lib Test {
}
@[test_driver]
lean_exe test {
root := `Test.Main
-- Solves the native symbol not found problem
-- Somehow solves the native symbol not found problem
supportInterpreter := true
}

View File

@ -1 +1 @@
leanprover/lean4:v4.12.0
leanprover/lean4:4.0.0