Enable handling of m-Coupled goals #20

Merged
aniva merged 11 commits from goal/dependency into dev 2023-10-27 19:30:21 -07:00
16 changed files with 950 additions and 457 deletions

View File

@ -8,7 +8,7 @@ import Pantograph
open Pantograph open Pantograph
/-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/ /-- Parse a command either in `{ "cmd": ..., "payload": ... }` form or `cmd { ... }` form. -/
def parse_command (s: String): Except String Commands.Command := do def parseCommand (s: String): Except String Protocol.Command := do
let s := s.trim let s := s.trim
match s.get? 0 with match s.get? 0 with
| .some '{' => -- Parse in Json mode | .some '{' => -- Parse in Json mode
@ -26,9 +26,9 @@ unsafe def loop : MainM Unit := do
let state ← get let state ← get
let command ← (← IO.getStdin).getLine let command ← (← IO.getStdin).getLine
if command.trim.length = 0 then return () if command.trim.length = 0 then return ()
match parse_command command with match parseCommand command with
| .error error => | .error error =>
let error := Lean.toJson ({ error := "command", desc := error }: Commands.InteractionError) let error := Lean.toJson ({ error := "command", desc := error }: Protocol.InteractionError)
-- Using `Lean.Json.compress` here to prevent newline -- Using `Lean.Json.compress` here to prevent newline
IO.println error.compress IO.println error.compress
| .ok command => | .ok command =>

View File

@ -6,7 +6,7 @@ TEST_EXE := build/bin/test
TEST_SOURCE := $(wildcard Test/*.lean) TEST_SOURCE := $(wildcard Test/*.lean)
$(LIB) $(EXE): $(SOURCE) $(LIB) $(EXE): $(SOURCE)
lake build lake build pantograph
$(TEST_EXE): $(LIB) $(TEST_SOURCE) $(TEST_EXE): $(LIB) $(TEST_SOURCE)
lake build test lake build test
@ -14,4 +14,7 @@ $(TEST_EXE): $(LIB) $(TEST_SOURCE)
test: $(TEST_EXE) test: $(TEST_EXE)
lake env $(TEST_EXE) lake env $(TEST_EXE)
.PHONY: test clean:
lake clean
.PHONY: test clean

View File

@ -1,8 +1,8 @@
import Pantograph.Commands import Pantograph.Goal
import Pantograph.Serial import Pantograph.Protocol
import Pantograph.Symbols
import Pantograph.Tactic
import Pantograph.SemihashMap import Pantograph.SemihashMap
import Pantograph.Serial
import Pantograph.Symbol
namespace Pantograph namespace Pantograph
@ -11,16 +11,16 @@ structure Context where
/-- Stores state of the REPL -/ /-- Stores state of the REPL -/
structure State where structure State where
options: Commands.Options := {} options: Protocol.Options := {}
goalStates: SemihashMap GoalState := SemihashMap.empty goalStates: SemihashMap GoalState := SemihashMap.empty
-- State monad /-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM) abbrev MainM := ReaderT Context (StateT State Lean.Elab.TermElabM)
-- For some reason writing `CommandM α := MainM (Except ... α)` disables certain -- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- monadic features in `MainM` -- certain monadic features in `MainM`
abbrev CR α := Except Commands.InteractionError α abbrev CR α := Except Protocol.InteractionError α
def execute (command: Commands.Command): MainM Lean.Json := do def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json := let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with
| .ok args => do | .ok args => do
@ -39,32 +39,33 @@ def execute (command: Commands.Command): MainM Lean.Json := do
| "goal.start" => run goal_start | "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic | "goal.tactic" => run goal_tactic
| "goal.delete" => run goal_delete | "goal.delete" => run goal_delete
| "goal.print" => run goal_print
| cmd => | cmd =>
let error: Commands.InteractionError := let error: Protocol.InteractionError :=
errorCommand s!"Unknown command {cmd}" errorCommand s!"Unknown command {cmd}"
return Lean.toJson error return Lean.toJson error
where where
errorI (type desc: String): Commands.InteractionError := { error := type, desc := desc } errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
errorCommand := errorI "command" errorCommand := errorI "command"
errorIndex := errorI "index" errorIndex := errorI "index"
-- Command Functions -- Command Functions
reset (_: Commands.Reset): MainM (CR Commands.StatResult) := do reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
set { state with goalStates := SemihashMap.empty } set { state with goalStates := SemihashMap.empty }
return .ok { nGoals } return .ok { nGoals }
stat (_: Commands.Stat): MainM (CR Commands.StatResult) := do stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get let state ← get
let nGoals := state.goalStates.size let nGoals := state.goalStates.size
return .ok { nGoals } return .ok { nGoals }
lib_catalog (_: Commands.LibCatalog): MainM (CR Commands.LibCatalogResult) := do lib_catalog (_: Protocol.LibCatalog): MainM (CR Protocol.LibCatalogResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := #[]) (λ acc name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => acc.push x | .some x => acc.push x
| .none => acc) | .none => acc)
return .ok { symbols := names } return .ok { symbols := names }
lib_inspect (args: Commands.LibInspect): MainM (CR Commands.LibInspectResult) := do lib_inspect (args: Protocol.LibInspect): MainM (CR Protocol.LibInspectResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let name := str_to_name args.name let name := str_to_name args.name
@ -84,7 +85,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
value? := ← value?.mapM (λ v => serialize_expression state.options v), value? := ← value?.mapM (λ v => serialize_expression state.options v),
module? := module? module? := module?
} }
expr_echo (args: Commands.ExprEcho): MainM (CR Commands.ExprEchoResult) := do expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
match syntax_from_str env args.expr with match syntax_from_str env args.expr with
@ -101,7 +102,7 @@ def execute (command: Commands.Command): MainM Lean.Json := do
} }
catch exception => catch exception =>
return .error $ errorI "typing" (← exception.toMessageData.toString) return .error $ errorI "typing" (← exception.toMessageData.toString)
options_set (args: Commands.OptionsSet): MainM (CR Commands.OptionsSetResult) := do options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get let state ← get
let options := state.options let options := state.options
set { state with set { state with
@ -110,15 +111,15 @@ def execute (command: Commands.Command): MainM Lean.Json := do
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty, printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty, printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST, printExprAST := args.printExprAST?.getD options.printExprAST,
proofVariableDelta := args.proofVariableDelta?.getD options.proofVariableDelta, noRepeat := args.noRepeat?.getD options.noRepeat,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls, printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
} }
} }
return .ok { } return .ok { }
options_print (_: Commands.OptionsPrint): MainM (CR Commands.OptionsPrintResult) := do options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do
return .ok (← get).options return .ok (← get).options
goal_start (args: Commands.GoalStart): MainM (CR Commands.GoalStartResult) := do goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get let state ← get
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with let expr?: Except _ Lean.Expr ← (match args.expr, args.copyFrom with
@ -133,42 +134,55 @@ def execute (command: Commands.Command): MainM Lean.Json := do
(match env.find? <| str_to_name copyFrom with (match env.find? <| str_to_name copyFrom with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}" | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok cInfo.type) | .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" "Exactly one of {expr, copyFrom} must be supplied")
| _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
match expr? with match expr? with
| .error error => return .error error | .error error => return .error error
| .ok expr => | .ok expr =>
let goalState ← GoalState.create expr let goalState ← GoalState.create expr
let (goalStates, goalId) := state.goalStates.insert goalState let (goalStates, stateId) := state.goalStates.insert goalState
set { state with goalStates } set { state with goalStates }
return .ok { goalId } return .ok { stateId }
goal_tactic (args: Commands.GoalTactic): MainM (CR Commands.GoalTacticResult) := do goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get let state ← get
match state.goalStates.get? args.goalId with match state.goalStates.get? args.stateId with
| .none => return .error $ errorIndex s!"Invalid goal index {args.goalId}" | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => | .some goalState => do
let result ← GoalState.execute goalState args.tactic |>.run state.options let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
match result with | .some tactic, .none => do
| .success goals => pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
if goals.isEmpty then | .none, .some expr => do
return .ok {} pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
else | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
-- Append all goals match nextGoalState? with
let (goalStates, goalIds, sGoals) := Array.foldl (λ acc itr => | .error error => return .error error
let (map, indices, serializedGoals) := acc | .ok (.success nextGoalState) =>
let (goalState, sGoal) := itr let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
let (map, index) := map.insert goalState
(map, index :: indices, sGoal :: serializedGoals)
) (state.goalStates, [], []) goals
set { state with goalStates } set { state with goalStates }
return .ok { goals? := .some sGoals.reverse.toArray, goalIds? := .some goalIds.reverse.toArray } let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
| .failure messages => return .ok {
nextStateId? := .some nextStateId,
goals? := .some goals,
}
| .ok (.parseError message) =>
return .ok { parseError? := .some message }
| .ok (.indexError goalId) =>
return .error $ errorIndex s!"Invalid goal id index {goalId}"
| .ok (.failure messages) =>
return .ok { tacticErrors? := .some messages } return .ok { tacticErrors? := .some messages }
goal_delete (args: Commands.GoalDelete): MainM (CR Commands.GoalDeleteResult) := do goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get let state ← get
let goalStates := args.goalIds.foldl (λ map id => map.remove id) state.goalStates let goalStates := args.stateIds.foldl (λ map id => map.remove id) state.goalStates
set { state with goalStates } set { state with goalStates }
return .ok {} return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
match state.goalStates.get? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
return .ok {
root?,
}
end Pantograph end Pantograph

204
Pantograph/Goal.lean Normal file
View File

@ -0,0 +1,204 @@
import Lean
import Pantograph.Symbol
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
savedState : Elab.Tactic.SavedState
-- The root hole which is the search target
root: MVarId
-- New metavariables acquired in this state
newMVars: SSet MVarId
-- The id of the goal in the parent
parentGoalId: Nat := 0
abbrev M := Elab.TermElabM
protected def GoalState.create (expr: Expr): M 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 goal := (← Meta.mkFreshExprMVar expr (kind := MetavarKind.synthetic) (userName := .anonymous))
let savedStateMonad: Elab.Tactic.TacticM Elab.Tactic.SavedState := MonadBacktrack.saveState
let root := goal.mvarId!
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [root]}
return {
savedState,
root,
newMVars := SSet.insert .empty root,
}
protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
protected def GoalState.runM {α: Type} (state: GoalState) (m: Elab.TermElabM α) : M α := do
state.savedState.term.restore
m
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
private def GoalState.mvars (state: GoalState): SSet MVarId :=
state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k
/-- Inner function for executing tactic on goal state -/
def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
M (Except (Array String) Elab.Tactic.SavedState):= do
let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := 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)
catch exception =>
return .error #[← exception.toMessageData.toString]
tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
/-- 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 goal index is out of bounds
| indexError (goalId: Nat)
/-- Execute tactic on given state -/
protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String):
M TacticResult := do
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure $ goal
| .none => return .indexError goalId
let tactic ← match Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `tactic)
(input := tactic)
(fileName := "<stdin>") with
| .ok stx => pure $ stx
| .error error => return .parseError error
match (← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
| .error errors =>
return .failure errors
| .ok nextSavedState =>
-- Assert that the definition of metavariables are the same
let nextMCtx := nextSavedState.term.meta.meta.mctx
let prevMCtx := state.savedState.term.meta.meta.mctx
-- Generate a list of mvarIds that exist in the parent state; Also test the
-- assertion that the types have not changed on any mvars.
let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
assert! prevMVarDecl.type == mvarDecl.type
return acc
else
return acc.insert mvarId
) SSet.empty
return .success {
state with
savedState := nextSavedState
newMVars,
parentGoalId := goalId,
}
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
let expr ← match Parser.runParserCategory
(env := state.env)
(catName := `term)
(input := expr)
(fileName := "<stdin>") with
| .ok syn => pure syn
| .error error => return .parseError error
let tacticM: Elab.Tactic.TacticM TacticResult := do
state.savedState.restore
Elab.Tactic.setGoals [goal]
try
let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
-- Attempt to unify the expression
let goalType ← goal.getType
let exprType ← Meta.inferType expr
if !(← Meta.isDefEq goalType exprType) then
return .failure #["Type unification failed", toString (← Meta.ppExpr goalType), toString (← Meta.ppExpr exprType)]
goal.checkNotAssigned `GoalState.tryAssign
goal.assign expr
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 .failure errors
else
let prevMCtx := state.savedState.term.meta.meta.mctx
let nextMCtx ← getMCtx
-- Generate a list of mvarIds that exist in the parent state; Also test the
-- assertion that the types have not changed on any mvars.
let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
assert! prevMVarDecl.type == mvarDecl.type
return acc
else
return mvarId :: acc
) []
-- The new goals are the newMVars that lack an assignment
Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
let nextSavedState ← MonadBacktrack.saveState
return .success {
state with
savedState := nextSavedState,
newMVars := newMVars.toSSet,
parentGoalId := goalId,
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
/-- After finishing one branch of a proof (`graftee`), pick up from the point where the proof was left off (`target`) -/
protected def GoalState.continue (target: GoalState) (graftee: GoalState): Except String GoalState :=
if target.root != graftee.root then
.error s!"Roots of two continued goal states do not match: {target.root.name} != {graftee.root.name}"
-- Ensure goals are not dangling
else if ¬ (target.goals.all (λ goal => graftee.mvars.contains goal)) then
.error s!"Some goals in target are not present in the graftee"
else
-- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
let unassigned := target.goals.filter (λ goal =>
let mctx := graftee.mctx
¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
.ok {
savedState := {
term := graftee.savedState.term,
tactic := { goals := unassigned },
},
root := target.root,
newMVars := graftee.newMVars,
}
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
let expr := goalState.mctx.eAssignment.find! goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasMVar 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
.some expr
end Pantograph

View File

@ -6,7 +6,7 @@ its field names to avoid confusion with error messages generated by the REPL.
-/ -/
import Lean.Data.Json import Lean.Data.Json
namespace Pantograph.Commands namespace Pantograph.Protocol
/-- Main Option structure, placed here to avoid name collision -/ /-- Main Option structure, placed here to avoid name collision -/
@ -18,9 +18,10 @@ structure Options where
printExprPretty: Bool := true printExprPretty: Bool := true
-- When enabled, print the raw AST of expressions -- When enabled, print the raw AST of expressions
printExprAST: Bool := false printExprAST: Bool := false
-- When enabled, the types and values of persistent variables in a proof goal -- 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 -- are not shown unless they are new to the proof step. Reduces overhead.
proofVariableDelta: Bool := false -- NOTE: that this assumes the type and assignment of variables can never change.
noRepeat: Bool := false
-- See `pp.auxDecls` -- See `pp.auxDecls`
printAuxDecls: Bool := false printAuxDecls: Bool := false
-- See `pp.implementationDetailHyps` -- See `pp.implementationDetailHyps`
@ -43,7 +44,10 @@ structure Expression where
deriving Lean.ToJson deriving Lean.ToJson
structure Variable where structure Variable where
name: String /-- The internal name used in raw expressions -/
name: String := ""
/-- The name displayed to the user -/
userName: String
/-- Does the name contain a dagger -/ /-- Does the name contain a dagger -/
isInaccessible?: Option Bool := .none isInaccessible?: Option Bool := .none
type?: Option Expression := .none type?: Option Expression := .none
@ -120,7 +124,7 @@ structure OptionsSet where
printJsonPretty?: Option Bool printJsonPretty?: Option Bool
printExprPretty?: Option Bool printExprPretty?: Option Bool
printExprAST?: Option Bool printExprAST?: Option Bool
proofVariableDelta?: Option Bool noRepeat?: Option Bool
printAuxDecls?: Option Bool printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool printImplementationDetailHyps?: Option Bool
deriving Lean.FromJson deriving Lean.FromJson
@ -132,32 +136,55 @@ abbrev OptionsPrintResult := Options
structure GoalStart where structure GoalStart where
-- Only one of the fields below may be populated. -- Only one of the fields below may be populated.
expr: Option String -- Proof expression expr: Option String -- Directly parse in an expression
copyFrom: Option String -- Theorem name copyFrom: Option String -- Copy the type from a theorem in the environment
deriving Lean.FromJson deriving Lean.FromJson
structure GoalStartResult where structure GoalStartResult where
goalId: Nat := 0 -- Proof tree id stateId: Nat := 0
deriving Lean.ToJson deriving Lean.ToJson
structure GoalTactic where structure GoalTactic where
-- Identifiers for tree, state, and goal -- Identifiers for tree, state, and goal
goalId: Nat stateId: Nat
tactic: String goalId: Nat := 0
-- One of the fields here must be filled
tactic?: Option String := .none
expr?: Option String := .none
deriving Lean.FromJson deriving Lean.FromJson
structure GoalTacticResult where structure GoalTacticResult where
-- Existence of this field shows success -- 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 goals?: Option (Array Goal) := .none
-- Next proof state id, if successful
goalIds?: Option (Array Nat) := .none -- Existence of this field shows tactic execution failure
-- Existence of this field shows failure
tacticErrors?: Option (Array String) := .none tacticErrors?: Option (Array String) := .none
-- Existence of this field shows the tactic parsing has failed
parseError?: Option String := .none
deriving Lean.ToJson deriving Lean.ToJson
-- Remove a bunch of goals. -- Remove goal states
structure GoalDelete where structure GoalDelete where
goalIds: List Nat stateIds: List Nat
deriving Lean.FromJson deriving Lean.FromJson
structure GoalDeleteResult where structure GoalDeleteResult where
deriving Lean.ToJson deriving Lean.ToJson
structure GoalPrint where
stateId: Nat
deriving Lean.FromJson
structure GoalPrintResult where
-- The root expression
root?: Option Expression
deriving Lean.ToJson
end Pantograph.Commands -- Diagnostic Options, not available in REPL
structure GoalDiag where
printContext: Bool := true
printValue: Bool := true
printNewMVars: Bool := false
-- Print all mvars
printAll: Bool := false
end Pantograph.Protocol

View File

@ -3,7 +3,8 @@ All serialisation functions
-/ -/
import Lean import Lean
import Pantograph.Commands import Pantograph.Protocol
import Pantograph.Goal
namespace Pantograph namespace Pantograph
open Lean open Lean
@ -28,34 +29,28 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax :=
def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try try
let expr ← Elab.Term.elabType syn 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 return .ok expr
catch ex => return .error (← ex.toMessageData.toString) catch ex => return .error (← ex.toMessageData.toString)
def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do def syntax_to_expr (syn: Syntax): Elab.TermElabM (Except String Expr) := do
try try
let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .none) 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 return .ok expr
catch ex => return .error (← ex.toMessageData.toString) catch ex => return .error (← ex.toMessageData.toString)
--- Output Functions --- --- Output Functions ---
def type_expr_to_bound (expr: Expr): MetaM Commands.BoundExpression := do def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
Meta.forallTelescope expr fun arr body => do Meta.forallTelescope expr fun arr body => do
let binders ← arr.mapM fun fvar => do let binders ← arr.mapM fun fvar => do
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType))) return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
return { binders, target := toString (← Meta.ppExpr body) } return { binders, target := toString (← Meta.ppExpr body) }
private def name_to_ast: Lean.Name → String private def name_to_ast (name: Lean.Name) (sanitize: Bool := true): String := match name with
| .anonymous | .anonymous => ":anon"
| .num _ _ => ":anon" | .num n i => match sanitize with
| false => s!"{toString n} {i}"
| true => ":anon"
| n@(.str _ _) => toString n | n@(.str _ _) => toString n
private def level_depth: Level → Nat private def level_depth: Level → Nat
@ -108,78 +103,80 @@ def serialize_sort_level_ast (level: Level): String :=
/-- /--
Completely serializes an expression tree. Json not used due to compactness Completely serializes an expression tree. Json not used due to compactness
-/ -/
def serialize_expression_ast (expr: Expr): MetaM String := do def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
match expr with self expr
where
self (e: Expr): String :=
match e with
| .bvar deBruijnIndex => | .bvar deBruijnIndex =>
-- This is very common so the index alone is shown. Literals are handled below. -- 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 -- The raw de Bruijn index should never appear in an unbound setting. In
-- Lean these are handled using a `#` prefix. -- Lean these are handled using a `#` prefix.
return s!"{deBruijnIndex}" s!"{deBruijnIndex}"
| .fvar fvarId => | .fvar fvarId =>
let name := (← fvarId.getDecl).userName let name := of_name fvarId.name
return s!"(:fv {name})" s!"(:fv {name})"
| .mvar mvarId => | .mvar mvarId =>
let name := name_to_ast mvarId.name let name := of_name mvarId.name
return s!"(:mv {name})" s!"(:mv {name})"
| .sort level => | .sort level =>
let level := serialize_sort_level_ast level let level := serialize_sort_level_ast level
return s!"(:sort {level})" s!"(:sort {level})"
| .const declName _ => | .const declName _ =>
-- The universe level of the const expression is elided since it should be -- The universe level of the const expression is elided since it should be
-- inferrable from surrounding expression -- inferrable from surrounding expression
return s!"(:c {declName})" s!"(:c {declName})"
| .app fn arg => | .app fn arg =>
let fn' ← serialize_expression_ast fn let fn' := self fn
let arg' ← serialize_expression_ast arg let arg' := self arg
return s!"({fn'} {arg'})" s!"({fn'} {arg'})"
| .lam binderName binderType body binderInfo => | .lam binderName binderType body binderInfo =>
let binderName' := name_to_ast binderName let binderName' := of_name binderName
let binderType' ← serialize_expression_ast binderType let binderType' := self binderType
let body' ← serialize_expression_ast body let body' := self body
let binderInfo' := binder_info_to_ast binderInfo let binderInfo' := binder_info_to_ast binderInfo
return s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})" s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
| .forallE binderName binderType body binderInfo => | .forallE binderName binderType body binderInfo =>
let binderName' := name_to_ast binderName let binderName' := of_name binderName
let binderType' ← serialize_expression_ast binderType let binderType' := self binderType
let body' ← serialize_expression_ast body let body' := self body
let binderInfo' := binder_info_to_ast binderInfo let binderInfo' := binder_info_to_ast binderInfo
return s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})" s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
| .letE name type value body _ => | .letE name type value body _ =>
-- Dependent boolean flag diacarded -- Dependent boolean flag diacarded
let name' := name_to_ast name let name' := name_to_ast name
let type' ← serialize_expression_ast type let type' := self type
let value' ← serialize_expression_ast value let value' := self value
let body' ← serialize_expression_ast body let body' := self body
return s!"(:let {name'} {type'} {value'} {body'})" s!"(:let {name'} {type'} {value'} {body'})"
| .lit v => | .lit v =>
-- To not burden the downstream parser who needs to handle this, the literal -- To not burden the downstream parser who needs to handle this, the literal
-- is wrapped in a :lit sexp. -- is wrapped in a :lit sexp.
let v' := match v with let v' := match v with
| .natVal val => toString val | .natVal val => toString val
| .strVal val => s!"\"{val}\"" | .strVal val => s!"\"{val}\""
return s!"(:lit {v'})" s!"(:lit {v'})"
| .mdata _ expr => | .mdata _ inner =>
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-- It may become necessary to incorporate the metadata. -- It may become necessary to incorporate the metadata.
return (← serialize_expression_ast expr) self inner
| .proj typeName idx struct => | .proj typeName idx struct =>
let struct' ← serialize_expression_ast struct let struct' := self struct
return s!"(:proj {typeName} {idx} {struct'})" s!"(:proj {typeName} {idx} {struct'})"
where
-- Elides all unhygenic names -- Elides all unhygenic names
binder_info_to_ast : Lean.BinderInfo → String binder_info_to_ast : Lean.BinderInfo → String
| .default => "" | .default => ""
| .implicit => " :implicit" | .implicit => " :implicit"
| .strictImplicit => " :strictImplicit" | .strictImplicit => " :strictImplicit"
| .instImplicit => " :instImplicit" | .instImplicit => " :instImplicit"
of_name (name: Name) := name_to_ast name sanitize
def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.Expression := do def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
let pp := toString (← Meta.ppExpr e) let pp := toString (← Meta.ppExpr e)
let pp?: Option String := match options.printExprPretty with let pp?: Option String := match options.printExprPretty with
| true => .some pp | true => .some pp
| false => .none | false => .none
let sexp: String := (← serialize_expression_ast e) let sexp: String := serialize_expression_ast e
let sexp?: Option String := match options.printExprAST with let sexp?: Option String := match options.printExprAST with
| true => .some sexp | true => .some sexp
| false => .none | false => .none
@ -189,8 +186,8 @@ def serialize_expression (options: Commands.Options) (e: Expr): MetaM Commands.E
} }
/-- Adapted from ppGoal -/ /-- Adapted from ppGoal -/
def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Commands.Goal := do : MetaM Protocol.Goal := do
-- Options for printing; See Meta.ppGoal for details -- Options for printing; See Meta.ppGoal for details
let showLetValues := true let showLetValues := true
let ppAuxDecls := options.printAuxDecls let ppAuxDecls := options.printAuxDecls
@ -198,29 +195,32 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
let lctx := mvarDecl.lctx let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
Meta.withLCtx lctx mvarDecl.localInstances do Meta.withLCtx lctx mvarDecl.localInstances do
let ppVarNameOnly (localDecl: LocalDecl): MetaM Commands.Variable := do let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
match localDecl with match localDecl with
| .cdecl _ _ varName _ _ _ => | .cdecl _ fvarId userName _ _ _ =>
let varName := varName.simpMacroScopes let userName := userName.simpMacroScopes
return { return {
name := toString varName, name := of_name fvarId.name,
userName:= of_name userName.simpMacroScopes,
} }
| .ldecl _ _ varName _ _ _ _ => do | .ldecl _ fvarId userName _ _ _ _ => do
return { return {
name := toString varName, name := of_name fvarId.name,
userName := toString userName.simpMacroScopes,
} }
let ppVar (localDecl : LocalDecl) : MetaM Commands.Variable := do let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
match localDecl with match localDecl with
| .cdecl _ _ varName type _ _ => | .cdecl _ fvarId userName type _ _ =>
let varName := varName.simpMacroScopes let userName := userName.simpMacroScopes
let type ← instantiateMVars type let type ← instantiateMVars type
return { return {
name := toString varName, name := of_name fvarId.name,
isInaccessible? := .some varName.isInaccessibleUserName userName:= of_name userName,
isInaccessible? := .some userName.isInaccessibleUserName
type? := .some (← serialize_expression options type) type? := .some (← serialize_expression options type)
} }
| .ldecl _ _ varName type val _ _ => do | .ldecl _ fvarId userName type val _ _ => do
let varName := varName.simpMacroScopes let userName := userName.simpMacroScopes
let type ← instantiateMVars type let type ← instantiateMVars type
let value? ← if showLetValues then let value? ← if showLetValues then
let val ← instantiateMVars val let val ← instantiateMVars val
@ -228,8 +228,9 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
else else
pure $ .none pure $ .none
return { return {
name := toString varName, name := of_name fvarId.name,
isInaccessible? := .some varName.isInaccessibleUserName userName:= of_name userName,
isInaccessible? := .some userName.isInaccessibleUserName
type? := .some (← serialize_expression options type) type? := .some (← serialize_expression options type)
value? := value? value? := value?
} }
@ -239,21 +240,79 @@ def serialize_goal (options: Commands.Options) (mvarDecl: MetavarDecl) (parentDe
if skip then if skip then
return acc return acc
else else
let nameOnly := options.proofVariableDelta && (parentDecl?.map let nameOnly := options.noRepeat && (parentDecl?.map
(λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false) (λ decl => decl.lctx.find? localDecl.fvarId |>.isSome) |>.getD false)
let var ← match nameOnly with let var ← match nameOnly with
| true => ppVarNameOnly localDecl | true => ppVarNameOnly localDecl
| false => ppVar localDecl | false => ppVar localDecl
return var::acc return var::acc
return { return {
caseName? := match mvarDecl.userName with caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
| Name.anonymous => .none isConversion := isLHSGoal? mvarDecl.type |>.isSome,
| name => .some <| toString name,
isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
vars := vars.reverse.toArray vars := vars.reverse.toArray
} }
where
of_name (n: Name) := name_to_ast n (sanitize := false)
protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do
let goals := state.goals.toArray
state.savedState.term.meta.restore
let parentDecl? := parent.bind (λ parentState =>
let parentGoal := parentState.goals.get! state.parentGoalId
parentState.mctx.findDecl? parentGoal)
goals.mapM fun goal => do
match state.mctx.findDecl? goal with
| .some mvarDecl =>
let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?)
pure serializedGoal
| .none => throwError s!"Metavariable does not exist in context {goal.name}"
/-- Print the metavariables in a readable format -/
protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
let savedState := goalState.savedState
savedState.term.meta.restore
let goals := savedState.tactic.goals
let mctx ← getMCtx
let root := goalState.root
-- Print the root
match mctx.decls.find? root with
| .some decl => printMVar ">" root decl
| .none => IO.println s!">{root.name}: ??"
goals.forM (fun mvarId => do
if mvarId != root then
match mctx.decls.find? mvarId with
| .some decl => printMVar "⊢" mvarId decl
| .none => IO.println s!"⊢{mvarId.name}: ??"
)
let goals := goals.toSSet
mctx.decls.forM (fun mvarId decl => do
if goals.contains mvarId || mvarId == root then
pure ()
-- Always print the root goal
else if mvarId == goalState.root then
printMVar (pref := ">") mvarId decl
-- Print the remainig ones that users don't see in Lean
else if options.printAll then
let pref := if goalState.newMVars.contains mvarId then "~" else " "
printMVar pref mvarId decl
else
pure ()
--IO.println s!" {mvarId.name}{userNameToString decl.userName}"
)
where
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
if options.printContext then
decl.lctx.fvarIdToDecl.forM printFVar
let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
IO.println s!" = {← Meta.ppExpr value}"
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
userNameToString : Name → String
| .anonymous => ""
| other => s!"[{other}]"
end Pantograph end Pantograph

View File

@ -1,10 +1,8 @@
/-
- Manages the visibility status of symbols
-/
import Lean.Declaration import Lean.Declaration
namespace Pantograph namespace Pantograph
/-- Converts a symbol of the form `aa.bb.cc` to a name -/
def str_to_name (s: String): Lean.Name := def str_to_name (s: String): Lean.Name :=
(s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous

View File

@ -1,102 +0,0 @@
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,5 +1,5 @@
namespace Pantograph namespace Pantograph
def version := "0.2.5" def version := "0.2.6"
end Pantograph end Pantograph

View File

@ -76,8 +76,9 @@ See `Pantograph/Commands.lean` for a description of the parameters and return va
have to be set via command line arguments.), for options, see `Pantograph/Commands.lean` have to be set via command line arguments.), for options, see `Pantograph/Commands.lean`
- `options.print`: Display the current set of options - `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.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.tactic {"stateId": <id>, "goalId": <id>, ["tactic": <tactic>], ["expr": <expr>]}`: Execute a tactic string on a given goal
- `goal.remove {"goalIds": [<id>]}"`: Remove a bunch of stored goals. - `goal.remove {"stateIds": [<id>]}"`: Remove a bunch of stored goals.
- `goal.print {"stateId": <id>}"`: Print a goal state
- `stat`: Display resource usage - `stat`: Display resource usage
## Errors ## Errors

19
Test/Common.lean Normal file
View File

@ -0,0 +1,19 @@
import Pantograph.Protocol
namespace Pantograph
namespace Protocol
/-- Set internal names to "" -/
def Goal.devolatilize (goal: Goal): Goal :=
{
goal with
vars := goal.vars.map removeInternalAux,
}
where removeInternalAux (v: Variable): Variable :=
{
v with
name := ""
}
end Protocol
end Pantograph

101
Test/Holes.lean Normal file
View File

@ -0,0 +1,101 @@
import LSpec
import Pantograph.Goal
import Pantograph.Serial
namespace Pantograph.Test.Holes
open Pantograph
open Lean
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_goal (hole: String): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv
let syn? := syntax_from_str env hole
add_test $ LSpec.check s!"Parsing {hole}" (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
}
def construct_sigma: TestM Unit := do
let goal? ← start_goal "∀ (n m: Nat), n + m = m + n"
add_test $ LSpec.check "Start goal" goal?.isSome
if let .some goal := goal? then
return ()
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 suite: 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 := [
("Σ'", construct_sigma)
]
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 "Holes" tests
end Pantograph.Test.Holes

View File

@ -2,7 +2,7 @@
-/ -/
import LSpec import LSpec
import Pantograph import Pantograph
namespace Pantograph.Test namespace Pantograph.Test.Integration
open Pantograph open Pantograph
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json)) def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json))
@ -47,26 +47,26 @@ def test_option_modify : IO LSpec.TestSeq :=
let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n" 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 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 module? := Option.some "Init.Data.Nat.Basic"
let options: Commands.Options := {} let options: Protocol.Options := {}
subroutine_runner [ subroutine_runner [
subroutine_step "lib.inspect" subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")] [("name", .str "Nat.add_one")]
(Lean.toJson ({ (Lean.toJson ({
type := { pp? }, module? }: type := { pp? }, module? }:
Commands.LibInspectResult)), Protocol.LibInspectResult)),
subroutine_step "options.set" subroutine_step "options.set"
[("printExprAST", .bool true)] [("printExprAST", .bool true)]
(Lean.toJson ({ }: (Lean.toJson ({ }:
Commands.OptionsSetResult)), Protocol.OptionsSetResult)),
subroutine_step "lib.inspect" subroutine_step "lib.inspect"
[("name", .str "Nat.add_one")] [("name", .str "Nat.add_one")]
(Lean.toJson ({ (Lean.toJson ({
type := { pp?, sexp? }, module? }: type := { pp?, sexp? }, module? }:
Commands.LibInspectResult)), Protocol.LibInspectResult)),
subroutine_step "options.print" subroutine_step "options.print"
[] []
(Lean.toJson ({ options with printExprAST := true }: (Lean.toJson ({ options with printExprAST := true }:
Commands.OptionsPrintResult)) Protocol.OptionsPrintResult))
] ]
def test_malformed_command : IO LSpec.TestSeq := def test_malformed_command : IO LSpec.TestSeq :=
let invalid := "invalid" let invalid := "invalid"
@ -75,19 +75,38 @@ def test_malformed_command : IO LSpec.TestSeq :=
[("name", .str "Nat.add_one")] [("name", .str "Nat.add_one")]
(Lean.toJson ({ (Lean.toJson ({
error := "command", desc := s!"Unknown command {invalid}"}: error := "command", desc := s!"Unknown command {invalid}"}:
Commands.InteractionError)), Protocol.InteractionError)),
subroutine_named_step "JSON Deserialization" "expr.echo" subroutine_named_step "JSON Deserialization" "expr.echo"
[(invalid, .str "Random garbage data")] [(invalid, .str "Random garbage data")]
(Lean.toJson ({ (Lean.toJson ({
error := "command", desc := s!"Unable to parse json: Pantograph.Commands.ExprEcho.expr: String expected"}: error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
Commands.InteractionError)) Protocol.InteractionError))
]
def test_tactic : IO LSpec.TestSeq :=
let goal: Protocol.Goal := {
target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
}
subroutine_runner [
subroutine_step "goal.start"
[("expr", .str "∀ (p q: Prop), p q → q p")]
(Lean.toJson ({stateId := 0}:
Protocol.GoalStartResult)),
subroutine_step "goal.tactic"
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
(Lean.toJson ({
nextStateId? := .some 1,
goals? := #[goal],
}:
Protocol.GoalTacticResult))
] ]
def test_integration: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
return LSpec.group "Integration" $ return LSpec.group "Integration" $
(LSpec.group "Option modify" (← test_option_modify)) ++ (LSpec.group "Option modify" (← test_option_modify)) ++
(LSpec.group "Malformed command" (← test_malformed_command)) (LSpec.group "Malformed command" (← test_malformed_command)) ++
(LSpec.group "Tactic" (← test_tactic))
end Pantograph.Test end Pantograph.Test.Integration

View File

@ -1,4 +1,5 @@
import LSpec import LSpec
--import Test.Holes
import Test.Integration import Test.Integration
import Test.Proofs import Test.Proofs
import Test.Serial import Test.Serial
@ -10,9 +11,10 @@ unsafe def main := do
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
let suites := [ let suites := [
test_integration, --Holes.suite,
test_proofs, Integration.suite,
test_serial Proofs.suite,
Serial.suite
] ]
let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done let all ← suites.foldlM (λ acc m => do pure $ acc ++ (← m)) LSpec.TestSeq.done
LSpec.lspecIO $ all LSpec.lspecIO $ all

View File

@ -1,8 +1,23 @@
/-
Tests pertaining to goals with no interdependencies
-/
import LSpec import LSpec
import Pantograph.Tactic import Pantograph.Goal
import Pantograph.Serial import Pantograph.Serial
import Test.Common
namespace Pantograph.Test namespace Pantograph
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}"
| .indexError index => s!".indexError {index}"
end Pantograph
namespace Pantograph.Test.Proofs
open Pantograph open Pantograph
open Lean open Lean
@ -10,21 +25,21 @@ inductive Start where
| copy (name: String) -- Start from some name in the environment | copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression | expr (expr: String) -- Start from some expression
abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Commands.Options M) abbrev TestM := StateRefT LSpec.TestSeq (ReaderT Protocol.Options M)
deriving instance DecidableEq, Repr for Commands.Expression deriving instance DecidableEq, Repr for Protocol.Expression
deriving instance DecidableEq, Repr for Commands.Variable deriving instance DecidableEq, Repr for Protocol.Variable
deriving instance DecidableEq, Repr for Commands.Goal deriving instance DecidableEq, Repr for Protocol.Goal
def add_test (test: LSpec.TestSeq): TestM Unit := do def addTest (test: LSpec.TestSeq): TestM Unit := do
set $ (← get) ++ test set $ (← get) ++ test
def start_proof (start: Start): TestM (Option GoalState) := do def startProof (start: Start): TestM (Option GoalState) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
match start with match start with
| .copy name => | .copy name =>
let cInfo? := str_to_name name |> env.find? let cInfo? := str_to_name name |> env.find?
add_test $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome addTest $ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with match cInfo? with
| .some cInfo => | .some cInfo =>
let goal ← GoalState.create (expr := cInfo.type) let goal ← GoalState.create (expr := cInfo.type)
@ -33,14 +48,14 @@ def start_proof (start: Start): TestM (Option GoalState) := do
return Option.none return Option.none
| .expr expr => | .expr expr =>
let syn? := syntax_from_str env expr let syn? := syntax_from_str env expr
add_test $ LSpec.check s!"Parsing {expr}" (syn?.isOk) addTest $ LSpec.check s!"Parsing {expr}" (syn?.isOk)
match syn? with match syn? with
| .error error => | .error error =>
IO.println error IO.println error
return Option.none return Option.none
| .ok syn => | .ok syn =>
let expr? ← syntax_to_expr syn let expr? ← syntax_to_expr_type syn
add_test $ LSpec.check s!"Elaborating" expr?.isOk addTest $ LSpec.check s!"Elaborating" expr?.isOk
match expr? with match expr? with
| .error error => | .error error =>
IO.println error IO.println error
@ -49,72 +64,146 @@ def start_proof (start: Start): TestM (Option GoalState) := do
let goal ← GoalState.create (expr := expr) let goal ← GoalState.create (expr := expr)
return Option.some goal return Option.some goal
def assert_unreachable (message: String): LSpec.TestSeq := LSpec.check message false def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false
def build_goal (nameType: List (String × String)) (target: String): Commands.Goal := def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal :=
{ {
caseName?,
target := { pp? := .some target}, target := { pp? := .some target},
vars := (nameType.map fun x => ({ vars := (nameType.map fun x => ({
name := x.fst, userName := x.fst,
type? := .some { pp? := .some x.snd }, type? := .some { pp? := .some x.snd },
isInaccessible? := .some false isInaccessible? := .some false
})).toArray })).toArray
} }
-- Like `build_goal` but allow certain variables to be elided. def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do
def build_goal_selective (nameType: List (String × Option String)) (target: String): Commands.Goal := let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options
{
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
}
let coreContext: Lean.Core.Context := {
currNamespace := Name.append .anonymous "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
-- Individual test cases -- Individual test cases
example: ∀ (a b: Nat), a + b = b + a := by example: ∀ (a b: Nat), a + b = b + a := by
intro n m intro n m
rw [Nat.add_comm] rw [Nat.add_comm]
def proof_nat_add_comm: TestM Unit := do def proof_nat_add_comm (manual: Bool): TestM Unit := do
let goal? ← start_proof (.copy "Nat.add_comm") let state? ← startProof <| match manual with
add_test $ LSpec.check "Start goal" goal?.isSome | false => .copy "Nat.add_comm"
if let .some goal := goal? then | true => .expr "∀ (a b: Nat), a + b = b + a"
if let .success #[(goal, sGoal)] ← goal.execute "intro n m" then addTest $ LSpec.check "Start goal" state?.isSome
let sGoal1e: Commands.Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n" let state0 ← match state? with
add_test $ LSpec.check "intro n m" (sGoal = sGoal1e) | .some state => pure state
| .none => do
if let .failure #[message] ← goal.execute "assumption" then addTest $ assertUnreachable "Goal could not parse"
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 () 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 let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro n m") with
add_test $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") | .success state => pure state
else | other => do
add_test $ assert_unreachable "assumption" addTest $ assertUnreachable $ other.toString
if let .success #[] ← goal.execute "rw [Nat.add_comm]" then
return () return ()
else addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
add_test $ assert_unreachable "rw [Nat.add_comm]" #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
else
add_test $ assert_unreachable "intro n m"
match ← state1.execute (goalId := 0) (tactic := "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
let state2 ← match ← state1.execute (goalId := 0) (tactic := "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
return ()
def proof_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 ()
let state1 ← match ← state0.execute (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.execute (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 }),
isInaccessible? := x.snd.map (λ _ => false)
})).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 proof_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 state1 ← match ← state0.execute (goalId := 0) (tactic := "intros") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "intros" (state1.goals.length = 1)
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.execute (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 state3 ← match ← state2.execute (goalId := 0) (tactic := "assumption") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.test "assumption" state3.goals.isEmpty
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
return ()
-- Two ways to write the same theorem -- Two ways to write the same theorem
example: ∀ (p q: Prop), p q → q p := by example: ∀ (p q: Prop), p q → q p := by
@ -132,121 +221,180 @@ example: ∀ (p q: Prop), p q → q p := by
. apply Or.inl . apply Or.inl
assumption assumption
def proof_or_comm: TestM Unit := do def proof_or_comm: TestM Unit := do
let typeProp: Commands.Expression := { pp? := .some "Prop" } let state? ← startProof (.expr "∀ (p q: Prop), p q → q p")
let branchGoal (caseName name: String): Commands.Goal := { let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return ()
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") 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 [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"])
let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
| .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
#[branchGoal "inl" "p", branchGoal "inr" "q"])
let state3_1 ← match ← state2.execute (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.execute (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?.isNone
let state3_2 ← match ← state2.execute (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.execute (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 state2.continue state4_2 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.execute (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.execute (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 name: String): Protocol.Goal := {
caseName? := .some caseName, caseName? := .some caseName,
target := { pp? := .some "q p" }, target := { pp? := .some "q p" },
vars := #[ vars := #[
{ name := "p", type? := .some typeProp, isInaccessible? := .some false }, { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
{ name := "q", type? := .some typeProp, isInaccessible? := .some false }, { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
{ name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } { userName := "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 /-- M-coupled goals -/
add_test $ LSpec.check "cases h/1" (sGoal1 = branchGoal "inl" "p") def proof_m_couple: TestM Unit := do
if let .success #[(goal, _)] ← goal1.execute "apply Or.inr" then let state? ← startProof (.expr "(2: Nat) ≤ 5")
if let .success #[] ← goal.execute "assumption" then let state0 ← match state? with
| .some state => pure state
| .none => do
addTest $ assertUnreachable "Goal could not parse"
return () return ()
else
add_test $ assert_unreachable "assumption"
else
add_test $ assert_unreachable "apply Or.inr"
let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply Nat.le_trans") with
add_test $ LSpec.check "cases h/2" (sGoal2 = branchGoal "inr" "q") | .success state => pure state
if let .success #[(goal, _)] ← goal2.execute "apply Or.inl" then | other => do
if let .success #[] ← goal.execute "assumption" then addTest $ assertUnreachable $ other.toString
return () return ()
else addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
add_test $ assert_unreachable "assumption" #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
else addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
add_test $ assert_unreachable "apply Or.inl" -- Set m to 3
let state2 ← match ← state1.execute (goalId := 2) (tactic := "exact 3") with
else | .success state => pure state
add_test $ assert_unreachable "cases h" | other => do
else addTest $ assertUnreachable $ other.toString
add_test $ assert_unreachable "intro p q h" return ()
addTest $ LSpec.test "(1b root)" state2.rootExpr?.isNone
example (w x y z : Nat) (p : Nat → Prop) let state1b ← match state1.continue state2 with
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by | .error msg => do
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at * addTest $ assertUnreachable $ msg
assumption return ()
def proof_arith_1: TestM Unit := do | .ok state => pure state
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)") addTest $ LSpec.check "exact 3" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
add_test $ LSpec.check "Start goal" goal?.isSome #[.some "2 ≤ 3", .some "3 ≤ 5"])
if let .some goal := goal? then addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
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 () 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 def proof_proposition_generation: TestM Unit := do
let goal? ← start_proof (.expr "∀ (a b: Nat), a + b = b + a") let state? ← startProof (.expr "Σ' p:Prop, p")
add_test $ LSpec.check "Start goal" goal?.isSome let state0 ← match state? with
if let .some goal := goal? then | .some state => pure state
if let .success #[(goal, sGoal)] ← goal.execute "intro n" then | .none => do
let sGoal1e: Commands.Goal := build_goal_selective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n" addTest $ assertUnreachable "Goal could not parse"
add_test $ LSpec.check "intro n" (sGoal = sGoal1e) return ()
if let .success #[(_, sGoal)] ← goal.execute "intro m" then let state1 ← match ← state0.execute (goalId := 0) (tactic := "apply PSigma.mk") with
let sGoal2e: Commands.Goal := build_goal_selective [("n", .none), ("m", .some "Nat")] "n + m = m + n" | .success state => pure state
add_test $ LSpec.check "intro m" (sGoal = sGoal2e) | other => do
else addTest $ assertUnreachable $ other.toString
add_test $ assert_unreachable "intro m" return ()
else addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
add_test $ assert_unreachable "intro n" #[
buildGoal [] "?fst" (caseName? := .some "snd"),
buildGoal [] "Prop" (caseName? := .some "fst")
])
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
def proof_runner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := do let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with
let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options | .success state => pure state
| other => do
addTest $ assertUnreachable $ other.toString
return ()
addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
let coreContext: Lean.Core.Context := { let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
currNamespace := str_to_name "Aniva", | .success state => pure state
openDecls := [], -- No 'open' directives needed | other => do
fileName := "<Pantograph>", addTest $ assertUnreachable $ other.toString
fileMap := { source := "", positions := #[0], lines := #[1] } return ()
} addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) =
let metaM := termElabM.run' (ctx := { #[])
declName? := some "_pantograph", addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome
errToSorry := false return ()
})
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 def suite: IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules let env: Lean.Environment ← Lean.importModules
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (imports := #[{ module := Name.append .anonymous "Init", runtimeOnly := false}])
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
let tests := [ let tests := [
("Nat.add_comm", proof_nat_add_comm), ("Nat.add_comm", proof_nat_add_comm false),
("nat.add_comm manual", proof_nat_add_comm_manual), ("Nat.add_comm manual", proof_nat_add_comm true),
("Nat.add_comm delta", proof_delta_variable),
("arithmetic", proof_arith),
("Or.comm", proof_or_comm), ("Or.comm", proof_or_comm),
("arithmetic 1", proof_arith_1), ("2 < 5", proof_m_couple),
("delta variable", proof_delta_variable) ("Proposition Generation", proof_proposition_generation)
] ]
let tests ← tests.foldlM (fun acc tests => do let tests ← tests.foldlM (fun acc tests => do
let (name, tests) := tests let (name, tests) := tests
let tests ← proof_runner env tests let tests ← proofRunner env tests
return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done return acc ++ (LSpec.group name tests)) LSpec.TestSeq.done
return LSpec.group "Proofs" tests return LSpec.group "Proofs" tests
end Pantograph.Test end Pantograph.Test.Proofs

View File

@ -1,19 +1,19 @@
import LSpec import LSpec
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Symbols import Pantograph.Symbol
namespace Pantograph.Test namespace Pantograph.Test.Serial
open Pantograph open Pantograph
open Lean open Lean
deriving instance Repr, DecidableEq for Commands.BoundExpression deriving instance Repr, DecidableEq for Protocol.BoundExpression
def test_str_to_name: LSpec.TestSeq := 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") 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 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × Commands.BoundExpression) := [ let entries: List (String × Protocol.BoundExpression) := [
("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), ("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" }) ("Nat.le_of_succ_le", { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "Nat.succ n ≤ m")], target := "n ≤ m" })
] ]
@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let expr := str_to_name symbol |> env.find? |>.get! |>.type let expr := str_to_name symbol |> env.find? |>.get! |>.type
let test := LSpec.check symbol ((serialize_expression_ast expr) = target) let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let coreM := metaM.run' let coreM := metaM.run'
let coreContext: Core.Context := { let coreContext: Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva" currNamespace := Lean.Name.str .anonymous "Aniva"
@ -62,15 +62,15 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
| .ok a => return a | .ok a => return a
def test_serial: IO LSpec.TestSeq := do def suite: IO LSpec.TestSeq := do
let env: Environment ← importModules let env: Environment ← importModules
(imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false })) (imports := #["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {}) (opts := {})
(trustLevel := 1) (trustLevel := 1)
return LSpec.group "Serialisation" $ return LSpec.group "Serialization" $
(LSpec.group "str_to_name" test_str_to_name) ++ (LSpec.group "str_to_name" test_str_to_name) ++
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++ (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
end Pantograph.Test end Pantograph.Test.Serial