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
19 changed files with 1656 additions and 12 deletions

3
.gitignore vendored
View File

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

115
Main.lean
View File

@ -1,4 +1,115 @@
import Lean.Data.Json
import Lean.Environment
import Pantograph.Version
import Pantograph
def main : IO Unit :=
IO.println s!"Hello, {hello}!"
-- Main IO functions
open Pantograph
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
def parse_command (s: String): Except String Commands.Command := do
let s := s.trim
match s.get? 0 with
| .some '{' => -- Parse in Json mode
Lean.fromJson? (← Lean.Json.parse s)
| .some _ => -- Parse in line mode
let offset := s.posOf ' ' |> s.offsetOfPos
if offset = s.length then
return { cmd := s.take offset, payload := Lean.Json.null }
else
let payload ← s.drop offset |> Lean.Json.parse
return { cmd := s.take offset, payload := payload }
| .none => throw "Command is empty"
unsafe def loop : MainM Unit := do
let state ← get
let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return ()
match parse_command command with
| .error error =>
let error := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError)
-- Using `Lean.Json.compress` here to prevent newline
IO.println error.compress
| .ok command =>
let ret ← execute command
let str := match state.options.printJsonPretty with
| true => ret.pretty
| false => ret.compress
IO.println str
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
println! s!"{version}"
return
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot)
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 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 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 { env := env }
catch ex =>
IO.println "Uncaught IO exception"
IO.println ex.toString

View File

@ -1 +1,174 @@
def hello := "world"
import Pantograph.Commands
import Pantograph.Serial
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

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

259
Pantograph/Serial.lean Normal file
View File

@ -0,0 +1,259 @@
/-
All serialisation functions
-/
import Lean
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 syntax_from_str (env: Environment) (s: String): Except String Syntax :=
Parser.runParserCategory
(env := env)
(catName := `term)
(input := s)
(fileName := "<stdin>")
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 syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try
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 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) }
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)` -/
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 := serialize_sort_level_ast v
let w := serialize_sort_level_ast w
s!"(:max {v} {w})"
| .imax v w =>
let v := serialize_sort_level_ast v
let w := serialize_sort_level_ast w
s!"(:imax {v} {w})"
| .param name =>
let name := name_to_ast name
s!"{name}"
| .mvar id =>
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
-/
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.
return s!"{deBruijnIndex}"
| .fvar fvarId =>
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 := 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
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' := 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}\""
return s!"(:lit {v'})"
| .mdata _ expr =>
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-- It may become necessary to incorporate the metadata.
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
binder_info_to_ast : Lean.BinderInfo → String
| .default => ""
| .implicit => " :implicit"
| .strictImplicit => " :strictImplicit"
| .instImplicit => " :instImplicit"
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?
}
/-- Adapted from ppGoal -/
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
let ppImplDetailHyps := options.printImplementationDetailHyps
let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
Meta.withLCtx lctx mvarDecl.localInstances do
let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do
match localDecl with
| .cdecl _ _ varName _ _ _ =>
let varName := varName.simpMacroScopes
return {
name := toString varName,
}
| .ldecl _ _ varName _ _ _ _ => do
return {
name := toString varName,
}
let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do
match localDecl with
| .cdecl _ _ varName type _ _ =>
let varName := varName.simpMacroScopes
let type ← instantiateMVars type
return {
name := toString varName,
isInaccessible? := .some varName.isInaccessibleUserName
type? := .some (← serialize_expression options type)
}
| .ldecl _ _ varName type val _ _ => do
let varName := varName.simpMacroScopes
let type ← instantiateMVars type
let value? ← if showLetValues then
let val ← instantiateMVars val
pure $ .some (← serialize_expression options val)
else
pure $ .none
return {
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
let skip := !ppAuxDecls && localDecl.isAuxDecl ||
!ppImplDetailHyps && localDecl.isImplementationDetail
if skip then
return acc
else
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 {
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
}
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

102
Pantograph/Tactic.lean Normal file
View File

@ -0,0 +1,102 @@
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

5
Pantograph/Version.lean Normal file
View File

@ -0,0 +1,5 @@
namespace Pantograph
def version := "0.2.5"
end Pantograph

110
README.md Normal file
View File

@ -0,0 +1,110 @@
# Pantograph
An interaction system for Lean 4.
![Pantograph](doc/icon.svg)
## Installation
Install `elan` and `lean4`. Then, execute
``` sh
lake build
```
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"
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
build/bin/pantograph MODULES|LEAN_OPTIONS
```
The REPL loop accepts commands as single-line JSON inputs and outputs either an
`Error:` (indicating malformed command) or a JSON return value indicating the
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/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
also accept lean options of the form `--key=value` e.g. `--pp.raw=true`.
Example: (~5k symbols)
```
$ build/bin/Pantograph Init
lib.catalog
lib.inspect {"name": "Nat.le_add_left"}
```
Example with `mathlib4` (~90k symbols, may stack overflow, see troubleshooting)
```
$ 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
```
$ env build/bin/Pantograph Init
goal.start {"expr": "∀ (n m : Nat), n + m = m + n"}
goal.tactic {"goalId": 0, "tactic": "intro n m"}
goal.tactic {"goalId": 1, "tactic": "assumption"}
goal.delete {"goalIds": [0]}
stat {}
goal.tactic {"goalId": 1, "tactic": "rw [Nat.add_comm]"}
stat
```
where the application of `assumption` should lead to a failure.
## Commands
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/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
## Errors
When an error pertaining to the execution of a command happens, the returning JSON structure is
``` json
{ error: "type", desc: "description" }
```
Common error forms:
* `command`: Indicates malformed command structure which results from either
invalid command or a malformed JSON structure that cannot be fed to an
individual command.
* `index`: Indicates an invariant maintained by the output of one command and
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.
## Troubleshooting
If lean encounters stack overflow problems when printing catalog, execute this before running lean:
```sh
ulimit -s unlimited
```
## Testing
The tests are based on `LSpec`. To run tests,
``` sh
test/all.sh
```

93
Test/Integration.lean Normal file
View File

@ -0,0 +1,93 @@
/- Integration test for the REPL
-/
import LSpec
import Pantograph
namespace Pantograph.Test
open Pantograph
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 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
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 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))
]
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

18
Test/Main.lean Normal file
View File

@ -0,0 +1,18 @@
import LSpec
import Test.Integration
import Test.Proofs
import Test.Serial
open Pantograph.Test
unsafe def main := do
Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot)
let suites := [
test_integration,
test_proofs,
test_serial
]
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
LSpec.lspecIO $ all

252
Test/Proofs.lean Normal file
View File

@ -0,0 +1,252 @@
import LSpec
import Pantograph.Tactic
import Pantograph.Serial
namespace Pantograph.Test
open Pantograph
open Lean
inductive Start where
| copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M)
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 start_proof (start: Start): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
match start with
| .copy name =>
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)
return Option.some goal
| .none =>
return Option.none
| .expr expr =>
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? ← syntax_to_expr syn
add_test $ 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 assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false
def build_goal (nameType: List (String × String)) (target: String): Commands.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
name := x.fst,
type? := .some { pp? := .some x.snd },
isInaccessible? := .some false
})).toArray
}
-- Like `build_goal` but allow certain variables to be elided.
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal :=
{
target := { pp? := .some target},
vars := (nameType.map fun x => ({
name := x.fst,
type? := x.snd.map (λ type => { pp? := type }),
isInaccessible? := x.snd.map (λ _ => false)
})).toArray
}
-- Individual test cases
example: ∀ (a b: Nat), a + b = b + a := by
intro n m
rw [Nat.add_comm]
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)
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 ()
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)
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 ()
else
add_test $ assert_unreachable "rw [Nat.add_comm]"
else
add_test $ assert_unreachable "intro n m"
-- Two ways to write the same theorem
example: ∀ (p q: Prop), p q → q p := by
intro p q h
cases h
apply Or.inr
assumption
apply Or.inl
assumption
example: ∀ (p q: Prop), p q → q p := by
intro p q h
cases h
. apply Or.inr
assumption
. apply Or.inl
assumption
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 := "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)
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"
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 ()
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "apply Or.inl"
else
add_test $ assert_unreachable "cases h"
else
add_test $ assert_unreachable "intro p q h"
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 ()
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "simp ..."
else
add_test $ assert_unreachable "intros"
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)
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"
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 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 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 := [
("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)
]
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

76
Test/Serial.lean Normal file
View File

@ -0,0 +1,76 @@
import LSpec
import Pantograph.Serial
import Pantograph.Symbols
namespace Pantograph.Test
open Pantograph
open Lean
deriving instance Repr, DecidableEq for Commands.BoundExpression
def test_str_to_name: LSpec.TestSeq :=
LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run")
def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
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" })
]
let coreM := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := str_to_name symbol |> env.find? |>.get! |>.type
let test := LSpec.check symbol ((← type_expr_to_bound expr) = target)
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 :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)"),
-- Handling of higher order types
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
]
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv
let expr := str_to_name symbol |> env.find? |>.get! |>.type
let 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_serial: IO LSpec.TestSeq := do
let env: Environment ← importModules
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return LSpec.group "Serialisation" $
(LSpec.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))
end Pantograph.Test

3
Test/all.sh Executable file
View File

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

73
doc/icon.svg Normal file
View File

@ -0,0 +1,73 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- Created with Inkscape (http://www.inkscape.org/) -->
<svg
width="256"
height="256"
viewBox="0 0 55.900957 55.900957"
version="1.1"
id="svg21534"
xml:space="preserve"
inkscape:version="1.2.2 (b0a8486541, 2022-12-01)"
sodipodi:docname="icon.svg"
xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
xmlns="http://www.w3.org/2000/svg"
xmlns:svg="http://www.w3.org/2000/svg"><sodipodi:namedview
id="namedview21536"
pagecolor="#ffffff"
bordercolor="#111111"
borderopacity="1"
inkscape:showpageshadow="0"
inkscape:pageopacity="0"
inkscape:pagecheckerboard="1"
inkscape:deskcolor="#d1d1d1"
inkscape:document-units="px"
showgrid="true"
inkscape:zoom="5.1754899"
inkscape:cx="158.82554"
inkscape:cy="91.682142"
inkscape:window-width="3777"
inkscape:window-height="2093"
inkscape:window-x="0"
inkscape:window-y="0"
inkscape:window-maximized="1"
inkscape:current-layer="layer1"><inkscape:grid
type="xygrid"
id="grid23833"
spacingx="3.4938098"
spacingy="3.4938098"
empspacing="4" /></sodipodi:namedview><defs
id="defs21531" /><g
inkscape:label="Layer 1"
inkscape:groupmode="layer"
id="layer1"><rect
style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:1.78013;stroke-miterlimit:3.4;stroke-dasharray:none"
id="rect26805"
width="11.502316"
height="2.2512667"
x="33.344425"
y="7.6690259"
ry="0.28140834"
rx="0.47926313" /><path
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
d="m 35.764667,9.9513013 c 0,0 -26.8581417,13.7987337 -28.0863506,14.9501437 -1.250042,1.171878 3.2347846,3.945325 3.2347846,3.945325 l 21.34979,14.934062 6.624567,0.453105 -27.599216,-17.304358 c 0,0 -0.603209,-0.08927 -0.600411,-0.762283 0.0028,-0.673015 27.32022,-16.4227356 27.32022,-16.4227356 z"
id="path27381"
sodipodi:nodetypes="csccccscc" /><path
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
d="M 10.97848,26.985751 40.537772,9.7943227 41.921795,9.7005084 11.210626,27.421377 Z"
id="path27479" /><path
style="fill:#3e3e3e;stroke:none;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;fill-opacity:1"
d="m 7.0509847,25.522367 c -0.8266141,1.386819 -2.4011783,4.48805 -2.4706357,4.90223 -0.069458,0.414182 0.4434324,0.513474 0.8491061,0.757041 C 5.835129,31.425204 19.33424,43.917182 19.33424,43.917182 l 0.324562,-0.539228 c 0,0 -14.2055729,-12.369493 -14.0644435,-12.868167 0.1411292,-0.498672 3.544896,-3.777392 3.544896,-3.777392 L 7.4596884,25.117508 Z"
id="path27481" /><rect
style="fill:#3e3e3e;fill-opacity:1;fill-rule:evenodd;stroke:none;stroke-width:2.11692;stroke-miterlimit:3.4;stroke-dasharray:none;stroke-opacity:1"
id="rect27483"
width="36.38942"
height="3.6217353"
x="13.953447"
y="43.009739"
rx="0.43672624"
ry="0.43672624" /><path
style="fill:none;stroke:#000000;stroke-width:0.218363px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
d="M -2.1119274,7.666599 H 64.179192"
id="path27487" /></g></svg>

After

Width:  |  Height:  |  Size: 3.5 KiB

11
lake-manifest.json Normal file
View File

@ -0,0 +1,11 @@
{"version": 5,
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/lurk-lab/LSpec.git",
"subDir?": null,
"rev": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
"opts": {},
"name": "LSpec",
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
"inherited": false}}]}

View File

@ -1,19 +1,24 @@
import Lake
open Lake DSL
package pantograph {
-- add package configuration options here
}
require mathlib from git
"https://github.com/leanprover-community/mathlib4.git" @ "8e5a00a8afc8913c0584cb85f37951995275fd87"
package pantograph
lean_lib Pantograph {
-- add library configuration options here
}
@[default_target]
lean_exe pantograph {
root := `Main
-- Somehow solves the native symbol not found problem
supportInterpreter := true
}
require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "88f7d23e56a061d32c7173cea5befa4b2c248b41"
lean_lib Test {
}
lean_exe test {
root := `Test.Main
-- Somehow solves the native symbol not found problem
supportInterpreter := true
}

View File

@ -1 +1 @@
leanprover/lean4:nightly-2023-05-06
leanprover/lean4:4.0.0