feat: Automatic Mode #92

Merged
aniva merged 9 commits from goal/automatic into dev 2024-09-08 12:25:07 -07:00
16 changed files with 528 additions and 463 deletions

View File

@ -4,6 +4,7 @@ import Lean.Environment
import Pantograph.Version import Pantograph.Version
import Pantograph.Library import Pantograph.Library
import Pantograph import Pantograph
import Repl
-- Main IO functions -- Main IO functions
open Pantograph open Pantograph

View File

@ -1,211 +1,8 @@
import Lean.Data.HashMap
import Pantograph.Compile import Pantograph.Compile
import Pantograph.Condensed
import Pantograph.Environment import Pantograph.Environment
import Pantograph.Goal import Pantograph.Goal
import Pantograph.Library import Pantograph.Library
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Serial import Pantograph.Serial
import Pantograph.Version
namespace Pantograph
structure Context where
imports: List String
/-- Stores state of the REPL -/
structure State where
options: Protocol.Options := {}
nextId: Nat := 0
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
/-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
-- HACK: For some reason writing `CommandM α := MainM (Except ... α)` disables
-- certain monadic features in `MainM`
abbrev CR α := Except Protocol.InteractionError α
def execute (command: Protocol.Command): MainM Lean.Json := do
let run { α β: Type } [Lean.FromJson α] [Lean.ToJson β] (comm: α → MainM (CR β)): MainM Lean.Json :=
match Lean.fromJson? command.payload with
| .ok args => do
match (← comm args) with
| .ok result => return Lean.toJson result
| .error ierror => return Lean.toJson ierror
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with
| "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo
| "env.catalog" => run env_catalog
| "env.inspect" => run env_inspect
| "env.add" => run env_add
| "options.set" => run options_set
| "options.print" => run options_print
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete
| "goal.print" => run goal_print
| "compile.unit" => run compile_unit
| cmd =>
let error: Protocol.InteractionError :=
errorCommand s!"Unknown command {cmd}"
return Lean.toJson error
where
errorCommand := errorI "command"
errorIndex := errorI "index"
-- Command Functions
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
return .ok { nGoals }
env_catalog (args: Protocol.EnvCatalog): MainM (CR Protocol.EnvCatalogResult) := do
let result ← Environment.catalog args
return .ok result
env_inspect (args: Protocol.EnvInspect): MainM (CR Protocol.EnvInspectResult) := do
let state ← get
Environment.inspect args state.options
env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
Environment.addDecl args
expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
let state ← get
exprEcho args.expr (expectedType? := args.type?) (levels := args.levels.getD #[]) (options := state.options)
options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
let state ← get
let options := state.options
set { state with
options := {
-- FIXME: This should be replaced with something more elegant
printJsonPretty := args.printJsonPretty?.getD options.printJsonPretty,
printExprPretty := args.printExprPretty?.getD options.printExprPretty,
printExprAST := args.printExprAST?.getD options.printExprAST,
printDependentMVars := args.printDependentMVars?.getD options.printDependentMVars,
noRepeat := args.noRepeat?.getD options.noRepeat,
printAuxDecls := args.printAuxDecls?.getD options.printAuxDecls,
printImplementationDetailHyps := args.printImplementationDetailHyps?.getD options.printImplementationDetailHyps
}
}
return .ok { }
options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.Options) := do
return .ok (← get).options
goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
let state ← get
let env ← Lean.MonadEnv.getEnv
let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
| .some expr, .none => goalStartExpr expr (args.levels.getD #[])
| .none, .some copyFrom =>
(match env.find? <| copyFrom.toName with
| .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
| .some cInfo => return .ok (← GoalState.create cInfo.type))
| _, _ =>
return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
match expr? with
| .error error => return .error error
| .ok goalState =>
let stateId := state.nextId
set { state with
goalStates := state.goalStates.insert stateId goalState,
nextId := state.nextId + 1
}
return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => do
let nextGoalState?: Except _ GoalState ←
match args.tactic?, args.expr?, args.have?, args.calc?, args.conv? with
| .some tactic, .none, .none, .none, .none => do
pure ( Except.ok (← goalTactic goalState args.goalId tactic))
| .none, .some expr, .none, .none, .none => do
pure ( Except.ok (← goalAssign goalState args.goalId expr))
| .none, .none, .some type, .none, .none => do
let binderName := args.binderName?.getD ""
pure ( Except.ok (← goalState.tryHave args.goalId binderName type))
| .none, .none, .none, .some pred, .none => do
pure ( Except.ok (← goalCalc goalState args.goalId pred))
| .none, .none, .none, .none, .some true => do
pure ( Except.ok (← goalConv goalState args.goalId))
| .none, .none, .none, .none, .some false => do
pure ( Except.ok (← goalConvExit goalState))
| _, _, _, _, _ => pure (Except.error <|
errorI "arguments" "Exactly one of {tactic, expr, have, calc, conv} must be supplied")
match nextGoalState? with
| .error error => return .error error
| .ok (.success nextGoalState) =>
let nextStateId := state.nextId
set { state with
goalStates := state.goalStates.insert state.nextId nextGoalState,
nextId := state.nextId + 1,
}
let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options) |>.run'
return .ok {
nextStateId? := .some nextStateId,
goals? := .some goals,
}
| .ok (.parseError message) =>
return .ok { parseError? := .some message }
| .ok (.indexError goalId) =>
return .error $ errorIndex s!"Invalid goal id index {goalId}"
| .ok (.invalidAction message) =>
return .error $ errorI "invalid" message
| .ok (.failure messages) =>
return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
match state.goalStates.find? args.target with
| .none => return .error $ errorIndex s!"Invalid state index {args.target}"
| .some target => do
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates.find? branchId with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
pure $ goalResume target goals
| _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
match nextState? with
| .error error => return .error <| errorI "structure" error
| .ok nextGoalState =>
let nextStateId := state.nextId
set { state with
goalStates := state.goalStates.insert nextStateId nextGoalState,
nextId := state.nextId + 1
}
let goals ← goalSerialize nextGoalState (options := state.options)
return .ok {
nextStateId,
goals,
}
goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
let state ← get
let goalStates := args.stateIds.foldl (λ map id => map.erase id) state.goalStates
set { state with goalStates }
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
match state.goalStates.find? args.stateId with
| .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
| .some goalState => runMetaM <| do
return .ok (← goalPrint goalState state.options)
compile_unit (args: Protocol.CompileUnit): MainM (CR Protocol.CompileUnitResult) := do
let module := args.module.toName
try
let steps ← Compile.processSource module
let units? := if args.compilationUnits then
.some $ steps.map λ step => (step.src.startPos.byteIdx, step.src.stopPos.byteIdx)
else
.none
let invocations? ← if args.invocations then
pure $ .some (← Compile.collectTacticsFromCompilation steps)
else
pure .none
return .ok { units?, invocations? }
catch e =>
return .error $ errorI "compile" (← e.toMessageData.toString)
end Pantograph

View File

@ -27,10 +27,11 @@ structure GoalState where
parentMVar?: Option MVarId parentMVar?: Option MVarId
-- Existence of this field shows that we are currently in `conv` mode. -- Existence of this field shows that we are currently in `conv` mode.
convMVar?: Option (MVarId × MVarId) := .none -- (convRhs, goal, dormant)
convMVar?: Option (MVarId × MVarId × List MVarId) := .none
-- Previous RHS for calc, so we don't have to repeat it every time -- Previous RHS for calc, so we don't have to repeat it every time
-- WARNING: If using `state with` outside of `calc`, this must be set to `.none` -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
calcPrevRhs?: Option Expr := .none calcPrevRhs?: Option (MVarId × Expr) := .none
@[export pantograph_goal_state_create_m] @[export pantograph_goal_state_create_m]
protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
@ -96,6 +97,20 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
calcPrevRhs? := .none, calcPrevRhs? := .none,
} }
/-- Immediately bring all parent goals back into scope. Used in automatic mode -/
@[export pantograph_goal_state_immediate_resume_parent]
protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
-- Prune parents solved goals
let mctx := state.mctx
let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
{
state with
savedState := {
state.savedState with
tactic := { goals := state.goals ++ parentGoals },
},
}
/-- /--
Brings into scope a list of goals Brings into scope a list of goals
-/ -/
@ -115,7 +130,6 @@ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except S
term := state.savedState.term, term := state.savedState.term,
tactic := { goals := unassigned }, tactic := { goals := unassigned },
}, },
calcPrevRhs? := .none,
} }
/-- /--
Brings into scope all goals from `branch` Brings into scope all goals from `branch`
@ -147,24 +161,24 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr return expr
@[export pantograph_goal_state_get_mvar_e_assignment] @[export pantograph_goal_state_get_mvar_e_assignment]
protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvarId: MVarId): Option Expr := do
let expr ← goalState.mctx.eAssignment.find? mvar let expr ← goalState.mctx.eAssignment.find? mvarId
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return expr return expr
--- Tactic execution functions --- --- Tactic execution functions ---
protected def GoalState.step (state: GoalState) (mvarId: MVarId) (tacticM: Elab.Tactic.TacticM Unit) protected def GoalState.step (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit)
: Elab.TermElabM GoalState := do : Elab.TermElabM GoalState := do
unless (← getMCtx).decls.contains mvarId do unless (← getMCtx).decls.contains goal do
throwError s!"MVarId is not in context: {mvarId.name}" throwError s!"Goal is not in context: {goal.name}"
mvarId.checkNotAssigned `GoalState.step goal.checkNotAssigned `GoalState.step
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [mvarId] } let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
let nextElabState ← MonadBacktrack.saveState let nextElabState ← MonadBacktrack.saveState
return { return {
state with state with
savedState := { term := nextElabState, tactic := newGoals }, savedState := { term := nextElabState, tactic := newGoals },
parentMVar? := .some mvarId, parentMVar? := .some goal,
calcPrevRhs? := .none, calcPrevRhs? := .none,
} }
@ -176,25 +190,20 @@ inductive TacticResult where
| failure (messages: Array String) | failure (messages: Array String)
-- Could not parse tactic -- Could not parse tactic
| parseError (message: String) | parseError (message: String)
-- The goal index is out of bounds
| indexError (goalId: Nat)
-- The given action cannot be executed in the state -- The given action cannot be executed in the state
| invalidAction (message: String) | invalidAction (message: String)
/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/ /-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit): protected def GoalState.tryTacticM (state: GoalState) (goal: MVarId) (tacticM: Elab.Tactic.TacticM Unit):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
let mvarId ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure $ goal
| .none => return .indexError goalId
try try
let nextState ← state.step mvarId tacticM let nextState ← state.step goal tacticM
return .success nextState return .success nextState
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
/-- Execute a string tactic on given state -/ /-- Execute a string tactic on given state. Restores TermElabM -/
protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): protected def GoalState.tryTactic (state: GoalState) (goal: MVarId) (tactic: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let tactic ← match Parser.runParserCategory let tactic ← match Parser.runParserCategory
@ -204,9 +213,9 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
(fileName := filename) with (fileName := filename) with
| .ok stx => pure $ stx | .ok stx => pure $ stx
| .error error => return .parseError error | .error error => return .parseError error
state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic state.tryTacticM goal $ Elab.Tactic.evalTactic tactic
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): protected def GoalState.tryAssign (state: GoalState) (goal: MVarId) (expr: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let expr ← match Parser.runParserCategory let expr ← match Parser.runParserCategory
@ -216,11 +225,11 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
(fileName := filename) with (fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.tryTacticM goalId $ Tactic.evalAssign expr state.tryTacticM goal $ Tactic.evalAssign expr
-- Specialized Tactics -- Specialized Tactics
protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): protected def GoalState.tryLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let type ← match Parser.runParserCategory let type ← match Parser.runParserCategory
@ -230,17 +239,13 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str
(fileName := filename) with (fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.tryTacticM goalId $ Tactic.evalLet binderName.toName type state.tryTacticM goal $ Tactic.evalLet binderName.toName type
/-- Enter conv tactic mode -/ /-- Enter conv tactic mode -/
@[export pantograph_goal_state_conv_m] protected def GoalState.conv (state: GoalState) (goal: MVarId):
protected def GoalState.conv (state: GoalState) (goalId: Nat):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
if state.convMVar?.isSome then if state.convMVar?.isSome then
return .invalidAction "Already in conv state" return .invalidAction "Already in conv state"
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
goal.checkNotAssigned `GoalState.conv goal.checkNotAssigned `GoalState.conv
let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do
state.restoreTacticM goal state.restoreTacticM goal
@ -253,11 +258,13 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
return (← MonadBacktrack.saveState, convMVar) return (← MonadBacktrack.saveState, convMVar)
try try
let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-- Other goals are now dormant
let otherGoals := state.goals.filter $ λ g => g != goal
return .success { return .success {
root := state.root, root := state.root,
savedState := nextSavedState savedState := nextSavedState
parentMVar? := .some goal, parentMVar? := .some goal,
convMVar? := .some (convRhs, goal), convMVar? := .some (convRhs, goal, otherGoals),
calcPrevRhs? := .none calcPrevRhs? := .none
} }
catch exception => catch exception =>
@ -267,7 +274,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
@[export pantograph_goal_state_conv_exit_m] @[export pantograph_goal_state_conv_exit_m]
protected def GoalState.convExit (state: GoalState): protected def GoalState.convExit (state: GoalState):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
let (convRhs, convGoal) ← match state.convMVar? with let (convRhs, convGoal, _) ← match state.convMVar? with
| .some mvar => pure mvar | .some mvar => pure mvar
| .none => return .invalidAction "Not in conv state" | .none => return .invalidAction "Not in conv state"
let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
@ -300,21 +307,18 @@ protected def GoalState.convExit (state: GoalState):
catch exception => catch exception =>
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
protected def GoalState.calcPrevRhsOf? (state: GoalState) (goalId: Nat) := protected def GoalState.calcPrevRhsOf? (state: GoalState) (goal: MVarId): Option Expr := do
if goalId == 1 then let (mvarId, rhs) ← state.calcPrevRhs?
state.calcPrevRhs? if mvarId == goal then
.some rhs
else else
.none .none
@[export pantograph_goal_state_try_calc_m] @[export pantograph_goal_state_try_calc_m]
protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): protected def GoalState.tryCalc (state: GoalState) (goal: MVarId) (pred: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
if state.convMVar?.isSome then if state.convMVar?.isSome then
return .invalidAction "Cannot initiate `calc` while in `conv` state" return .invalidAction "Cannot initiate `calc` while in `conv` state"
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
let `(term|$pred) ← match Parser.runParserCategory let `(term|$pred) ← match Parser.runParserCategory
(env := state.env) (env := state.env)
(catName := `term) (catName := `term)
@ -323,9 +327,10 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
goal.checkNotAssigned `GoalState.tryCalc goal.checkNotAssigned `GoalState.tryCalc
let calcPrevRhs? := state.calcPrevRhsOf? goalId let calcPrevRhs? := state.calcPrevRhsOf? goal
let target ← instantiateMVars (← goal.getDecl).type let decl ← goal.getDecl
let tag := (← goal.getDecl).userName let target ← instantiateMVars decl.type
let tag := decl.userName
try try
goal.withContext do goal.withContext do
@ -349,9 +354,8 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
(userName := tag ++ `calc) (userName := tag ++ `calc)
let mvarBranch := proof.mvarId! let mvarBranch := proof.mvarId!
let calcPrevRhs? := Option.some rhs
let mut proofType ← Meta.inferType proof let mut proofType ← Meta.inferType proof
let mut remainder := Option.none let mut remainder? := Option.none
-- The calc tactic either solves the main goal or leaves another relation. -- The calc tactic either solves the main goal or leaves another relation.
-- Replace the main goal, and save the new goal if necessary -- Replace the main goal, and save the new goal if necessary
@ -364,10 +368,11 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag let lastStepGoal ← Meta.mkFreshExprSyntheticOpaqueMVar lastStep tag
(proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep (proof, proofType) ← Elab.Term.mkCalcTrans proof proofType lastStepGoal lastStep
unless ← Meta.isDefEq proofType target do throwFailed unless ← Meta.isDefEq proofType target do throwFailed
remainder := .some lastStepGoal.mvarId! remainder? := .some lastStepGoal.mvarId!
goal.assign proof goal.assign proof
let goals := [ mvarBranch ] ++ remainder.toList let goals := [ mvarBranch ] ++ remainder?.toList
let calcPrevRhs? := remainder?.map $ λ g => (g, rhs)
return .success { return .success {
root := state.root, root := state.root,
savedState := { savedState := {
@ -381,19 +386,19 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
return .failure #[← exception.toMessageData.toString] return .failure #[← exception.toMessageData.toString]
protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): protected def GoalState.tryMotivatedApply (state: GoalState) (goal: MVarId) (recursor: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let recursor ← match (← Compile.parseTermM recursor) with let recursor ← match (← Compile.parseTermM recursor) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.tryTacticM goalId (tacticM := Tactic.evalMotivatedApply recursor) state.tryTacticM goal (tacticM := Tactic.evalMotivatedApply recursor)
protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): protected def GoalState.tryNoConfuse (state: GoalState) (goal: MVarId) (eq: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let eq ← match (← Compile.parseTermM eq) with let eq ← match (← Compile.parseTermM eq) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.tryTacticM goalId (tacticM := Tactic.evalNoConfuse eq) state.tryTacticM goal (tacticM := Tactic.evalNoConfuse eq)
end Pantograph end Pantograph

View File

@ -152,38 +152,38 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G
} }
@[export pantograph_goal_tactic_m] @[export pantograph_goal_tactic_m]
def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult := def goalTactic (state: GoalState) (goal: MVarId) (tactic: String): CoreM TacticResult :=
runTermElabM <| state.tryTactic goalId tactic runTermElabM <| state.tryTactic goal tactic
@[export pantograph_goal_assign_m] @[export pantograph_goal_assign_m]
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := def goalAssign (state: GoalState) (goal: MVarId) (expr: String): CoreM TacticResult :=
runTermElabM <| state.tryAssign goalId expr runTermElabM <| state.tryAssign goal expr
@[export pantograph_goal_have_m] @[export pantograph_goal_have_m]
protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do protected def GoalState.tryHave (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult := do
let type ← match (← Compile.parseTermM type) with let type ← match (← Compile.parseTermM type) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
runTermElabM do runTermElabM do
state.restoreElabM state.restoreElabM
state.tryTacticM goalId $ Tactic.evalHave binderName.toName type state.tryTacticM goal $ Tactic.evalHave binderName.toName type
@[export pantograph_goal_try_define_m] @[export pantograph_goal_try_define_m]
protected def GoalState.tryDefine (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do protected def GoalState.tryDefine (state: GoalState) (goal: MVarId) (binderName: String) (expr: String): CoreM TacticResult := do
let expr ← match (← Compile.parseTermM expr) with let expr ← match (← Compile.parseTermM expr) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
runTermElabM do runTermElabM do
state.restoreElabM state.restoreElabM
state.tryTacticM goalId (Tactic.evalDefine binderName.toName expr) state.tryTacticM goal (Tactic.evalDefine binderName.toName expr)
@[export pantograph_goal_let_m] @[export pantograph_goal_let_m]
def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := def goalLet (state: GoalState) (goal: MVarId) (binderName: String) (type: String): CoreM TacticResult :=
runTermElabM <| state.tryLet goalId binderName type runTermElabM <| state.tryLet goal binderName type
@[export pantograph_goal_conv_m] @[export pantograph_goal_conv_m]
def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult := def goalConv (state: GoalState) (goal: MVarId): CoreM TacticResult :=
runTermElabM <| state.conv goalId runTermElabM <| state.conv goal
@[export pantograph_goal_conv_exit_m] @[export pantograph_goal_conv_exit_m]
def goalConvExit (state: GoalState): CoreM TacticResult := def goalConvExit (state: GoalState): CoreM TacticResult :=
runTermElabM <| state.convExit runTermElabM <| state.convExit
@[export pantograph_goal_calc_m] @[export pantograph_goal_calc_m]
def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult := def goalCalc (state: GoalState) (goal: MVarId) (pred: String): CoreM TacticResult :=
runTermElabM <| state.tryCalc goalId pred runTermElabM <| state.tryCalc goal pred
end Pantograph end Pantograph

View File

@ -27,6 +27,8 @@ structure Options where
printAuxDecls: Bool := false printAuxDecls: Bool := false
-- See `pp.implementationDetailHyps` -- See `pp.implementationDetailHyps`
printImplementationDetailHyps: Bool := false printImplementationDetailHyps: Bool := false
-- If this is set to `true`, goals will never go dormant, so you don't have to manage resumption
automaticMode: Bool := false
deriving Lean.ToJson deriving Lean.ToJson
abbrev OptionsT := ReaderT Options abbrev OptionsT := ReaderT Options
@ -190,6 +192,7 @@ structure OptionsSet where
noRepeat?: Option Bool noRepeat?: Option Bool
printAuxDecls?: Option Bool printAuxDecls?: Option Bool
printImplementationDetailHyps?: Option Bool printImplementationDetailHyps?: Option Bool
automaticMode?: Option Bool
deriving Lean.FromJson deriving Lean.FromJson
structure OptionsSetResult where structure OptionsSetResult where
deriving Lean.ToJson deriving Lean.ToJson

View File

@ -1,6 +1,6 @@
namespace Pantograph namespace Pantograph
@[export pantograph_version] @[export pantograph_version]
def version := "0.2.17" def version := "0.2.18"
end Pantograph end Pantograph

View File

@ -90,6 +90,10 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
only the values of definitions are printed. only the values of definitions are printed.
* `options.set { key: value, ... }`: Set one or more options (not Lean options; those * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean` have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
One particular option for interest for machine learning researchers is the automatic mode.
`options.set { "automaticMode": true }`. This makes Pantograph act like
LeanDojo, with no resumption necessary to manage your goals.
* `options.print`: Display the current set of options * `options.print`: Display the current set of options
* `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`: * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
Start a new proof from a given expression or symbol Start a new proof from a given expression or symbol

220
Repl.lean Normal file
View File

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

View File

@ -62,13 +62,15 @@ protected def Goal.devolatilize (goal: Goal): Goal :=
end Condensed end Condensed
def GoalState.get! (state: GoalState) (i: Nat): MVarId := state.goals.get! i
def GoalState.tacticOn (state: GoalState) (goalId: Nat) (tactic: String) := state.tryTactic (state.goals.get! goalId) tactic
def TacticResult.toString : TacticResult → String def TacticResult.toString : TacticResult → String
| .success state => s!".success ({state.goals.length} goals)" | .success state => s!".success ({state.goals.length} goals)"
| .failure messages => | .failure messages =>
let messages := "\n".intercalate messages.toList let messages := "\n".intercalate messages.toList
s!".failure {messages}" s!".failure {messages}"
| .parseError error => s!".parseError {error}" | .parseError error => s!".parseError {error}"
| .indexError index => s!".indexError {index}"
| .invalidAction error => s!".invalidAction {error}" | .invalidAction error => s!".invalidAction {error}"
namespace Test namespace Test

View File

@ -2,39 +2,24 @@
-/ -/
import LSpec import LSpec
import Pantograph import Pantograph
import Repl
import Test.Common
namespace Pantograph.Test.Integration namespace Pantograph.Test.Integration
open Pantograph open Pantograph
def subroutine_named_step (name cmd: String) (payload: List (String × Lean.Json)) def step { α } [Lean.ToJson α] (cmd: String) (payload: List (String × Lean.Json))
(expected: Lean.Json): MainM LSpec.TestSeq := do (expected: α) (name? : Option String := .none): MainM LSpec.TestSeq := do
let result ← execute { cmd := cmd, payload := Lean.Json.mkObj payload } let payload := Lean.Json.mkObj payload
return LSpec.test name (toString result = toString expected) let name := name?.getD s!"{cmd} {payload.compress}"
def subroutine_step (cmd: String) (payload: List (String × Lean.Json)) let result ← execute { cmd, payload }
(expected: Lean.Json): MainM LSpec.TestSeq := subroutine_named_step cmd cmd payload expected return LSpec.test name (toString result = toString (Lean.toJson expected))
def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := do abbrev Test := List (MainM LSpec.TestSeq)
-- 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 ← createCoreContext #[]
let commands: MainM LSpec.TestSeq :=
steps.foldlM (λ suite step => do
let result ← step
return suite ++ result) LSpec.TestSeq.done
try
let coreM := commands.run context |>.run' {}
return Prod.fst $ (← coreM.toIO coreContext { env := env })
catch ex =>
return LSpec.check s!"Uncaught IO exception: {ex.toString}" false
def test_elab : IO LSpec.TestSeq := def test_elab : Test :=
subroutine_runner [ [
subroutine_step "expr.echo" step "expr.echo"
[("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])] [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])]
(Lean.toJson ({ (Lean.toJson ({
type := { pp? := .some "{α : Type u} → Type u" }, type := { pp? := .some "{α : Type u} → Type u" },
@ -42,46 +27,33 @@ def test_elab : IO LSpec.TestSeq :=
}: Protocol.ExprEchoResult)), }: Protocol.ExprEchoResult)),
] ]
def test_option_modify : IO LSpec.TestSeq := def test_option_modify : Test :=
let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ" let pp? := Option.some "∀ (n : Nat), n + 1 = n.succ"
let sexp? := Option.some "(:forall n (:c Nat) ((:c Eq) (:c Nat) ((:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat)) 0 ((:c OfNat.ofNat) (:c Nat) (:lit 1) ((:c instOfNatNat) (:lit 1)))) ((:c Nat.succ) 0)))" let 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: Protocol.Options := {} let options: Protocol.Options := {}
subroutine_runner [ [
subroutine_step "env.inspect" step "env.inspect" [("name", .str "Nat.add_one")]
[("name", .str "Nat.add_one")] ({ type := { pp? }, module? }: Protocol.EnvInspectResult),
(Lean.toJson ({ step "options.set" [("printExprAST", .bool true)]
type := { pp? }, module? }: ({ }: Protocol.OptionsSetResult),
Protocol.EnvInspectResult)), step "env.inspect" [("name", .str "Nat.add_one")]
subroutine_step "options.set" ({ type := { pp?, sexp? }, module? }: Protocol.EnvInspectResult),
[("printExprAST", .bool true)] step "options.print" []
(Lean.toJson ({ }: ({ options with printExprAST := true }: Protocol.Options),
Protocol.OptionsSetResult)),
subroutine_step "env.inspect"
[("name", .str "Nat.add_one")]
(Lean.toJson ({
type := { pp?, sexp? }, module? }:
Protocol.EnvInspectResult)),
subroutine_step "options.print"
[]
(Lean.toJson ({ options with printExprAST := true }:
Protocol.Options))
] ]
def test_malformed_command : IO LSpec.TestSeq := def test_malformed_command : Test :=
let invalid := "invalid" let invalid := "invalid"
subroutine_runner [ [
subroutine_named_step "Invalid command" invalid step invalid [("name", .str "Nat.add_one")]
[("name", .str "Nat.add_one")] ({ error := "command", desc := s!"Unknown command {invalid}" }: Protocol.InteractionError)
(Lean.toJson ({ (name? := .some "Invalid Command"),
error := "command", desc := s!"Unknown command {invalid}"}: step "expr.echo" [(invalid, .str "Random garbage data")]
Protocol.InteractionError)), ({ error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected" }:
subroutine_named_step "JSON Deserialization" "expr.echo" Protocol.InteractionError)
[(invalid, .str "Random garbage data")] (name? := .some "JSON Deserialization")
(Lean.toJson ({
error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
Protocol.InteractionError))
] ]
def test_tactic : IO LSpec.TestSeq := def test_tactic : Test :=
let goal1: Protocol.Goal := { let goal1: Protocol.Goal := {
name := "_uniq.11", name := "_uniq.11",
target := { pp? := .some "∀ (q : Prop), x q → q x" }, target := { pp? := .some "∀ (q : Prop), x q → q x" },
@ -95,77 +67,123 @@ def test_tactic : IO LSpec.TestSeq :=
{ name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }} { name := "_uniq.16", userName := "y", type? := .some { pp? := .some "Prop" }}
], ],
} }
subroutine_runner [ [
subroutine_step "goal.start" step "goal.start" [("expr", .str "∀ (p q: Prop), p q → q p")]
[("expr", .str "∀ (p q: Prop), p q → q p")] ({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
(Lean.toJson ({stateId := 0, root := "_uniq.9"}: step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
Protocol.GoalStartResult)), ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
subroutine_step "goal.tactic" step "goal.print" [("stateId", .num 1)]
[("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")] ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
(Lean.toJson ({ step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
nextStateId? := .some 1, ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
goals? := #[goal1], ]
}: def test_automatic_mode (automatic: Bool): Test :=
Protocol.GoalTacticResult)), let varsPQ := #[
subroutine_step "goal.print" { name := "_uniq.10", userName := "p", type? := .some { pp? := .some "Prop" }},
[("stateId", .num 1)] { name := "_uniq.13", userName := "q", type? := .some { pp? := .some "Prop" }}
(Lean.toJson ({ ]
parent? := .some { pp? := .some "fun x => ?m.12 x" }, let goal1: Protocol.Goal := {
}: name := "_uniq.17",
Protocol.GoalPrintResult)), target := { pp? := .some "q p" },
subroutine_step "goal.tactic" vars := varsPQ ++ #[
[("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] { name := "_uniq.16", userName := "h", type? := .some { pp? := .some "p q" }}
(Lean.toJson ({ ],
nextStateId? := .some 2, }
goals? := #[goal2], let goal2l: Protocol.Goal := {
}: name := "_uniq.59",
Protocol.GoalTacticResult)) userName? := .some "inl",
target := { pp? := .some "q p" },
vars := varsPQ ++ #[
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
],
}
let goal2r: Protocol.Goal := {
name := "_uniq.72",
userName? := .some "inr",
target := { pp? := .some "q p" },
vars := varsPQ ++ #[
{ name := "_uniq.60", userName := "h✝", type? := .some { pp? := .some "q" }, isInaccessible := true}
],
}
let goal3l: Protocol.Goal := {
name := "_uniq.78",
userName? := .some "inl.h",
target := { pp? := .some "p" },
vars := varsPQ ++ #[
{ name := "_uniq.47", userName := "h✝", type? := .some { pp? := .some "p" }, isInaccessible := true}
],
}
[
step "options.set" [("automaticMode", .bool automatic)]
({}: Protocol.OptionsSetResult),
step "goal.start" [("expr", .str "∀ (p q: Prop), p q → q p")]
({ stateId := 0, root := "_uniq.9" }: Protocol.GoalStartResult),
step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro p q h")]
({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "cases h")]
({ nextStateId? := .some 2, goals? := #[goal2l, goal2r], }: Protocol.GoalTacticResult),
let goals? := if automatic then #[goal3l, goal2r] else #[goal3l]
step "goal.tactic" [("stateId", .num 2), ("goalId", .num 0), ("tactic", .str "apply Or.inr")]
({ nextStateId? := .some 3, goals?, }: Protocol.GoalTacticResult),
] ]
def test_env_add_inspect : IO LSpec.TestSeq := def test_env_add_inspect : Test :=
let name1 := "Pantograph.mystery" let name1 := "Pantograph.mystery"
let name2 := "Pantograph.mystery2" let name2 := "Pantograph.mystery2"
subroutine_runner [ [
subroutine_step "env.add" step "env.add"
[ [
("name", .str name1), ("name", .str name1),
("type", .str "Prop → Prop → Prop"), ("type", .str "Prop → Prop → Prop"),
("value", .str "λ (a b: Prop) => Or a b"), ("value", .str "λ (a b: Prop) => Or a b"),
("isTheorem", .bool false) ("isTheorem", .bool false)
] ]
(Lean.toJson ({}: Protocol.EnvAddResult)), ({}: Protocol.EnvAddResult),
subroutine_step "env.inspect" step "env.inspect" [("name", .str name1)]
[("name", .str name1)] ({
(Lean.toJson ({
value? := .some { pp? := .some "fun a b => a b" }, value? := .some { pp? := .some "fun a b => a b" },
type := { pp? := .some "Prop → Prop → Prop" }, type := { pp? := .some "Prop → Prop → Prop" },
}: }:
Protocol.EnvInspectResult)), Protocol.EnvInspectResult),
subroutine_step "env.add" step "env.add"
[ [
("name", .str name2), ("name", .str name2),
("type", .str "Nat → Int"), ("type", .str "Nat → Int"),
("value", .str "λ (a: Nat) => a + 1"), ("value", .str "λ (a: Nat) => a + 1"),
("isTheorem", .bool false) ("isTheorem", .bool false)
] ]
(Lean.toJson ({}: Protocol.EnvAddResult)), ({}: Protocol.EnvAddResult),
subroutine_step "env.inspect" step "env.inspect" [("name", .str name2)]
[("name", .str name2)] ({
(Lean.toJson ({
value? := .some { pp? := .some "fun a => ↑a + 1" }, value? := .some { pp? := .some "fun a => ↑a + 1" },
type := { pp? := .some "Nat → Int" }, type := { pp? := .some "Nat → Int" },
}: }:
Protocol.EnvInspectResult)) Protocol.EnvInspectResult)
] ]
def suite: List (String × IO LSpec.TestSeq) := def runTest (env: Lean.Environment) (steps: Test): IO LSpec.TestSeq := do
[ -- Setup the environment for execution
("Elab", test_elab), let context: Context := {
("Option modify", test_option_modify), imports := ["Init"]
}
let commands: MainM LSpec.TestSeq :=
steps.foldlM (λ suite step => do
let result ← step
return suite ++ result) LSpec.TestSeq.done
runCoreMSeq env <| commands.run context |>.run' {}
def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) :=
let tests := [
("expr.echo", test_elab),
("options.set options.print", test_option_modify),
("Malformed command", test_malformed_command), ("Malformed command", test_malformed_command),
("Tactic", test_tactic), ("Tactic", test_tactic),
("Manual Mode", test_automatic_mode false),
("Automatic Mode", test_automatic_mode true),
("env.add env.inspect", test_env_add_inspect), ("env.add env.inspect", test_env_add_inspect),
] ]
tests.map (fun (name, test) => (name, runTest env test))
end Pantograph.Test.Integration end Pantograph.Test.Integration

View File

@ -44,7 +44,7 @@ def main (args: List String) := do
let suites: List (String × List (String × IO LSpec.TestSeq)) := [ let suites: List (String × List (String × IO LSpec.TestSeq)) := [
("Environment", Environment.suite), ("Environment", Environment.suite),
("Integration", Integration.suite), ("Integration", Integration.suite env_default),
("Library", Library.suite env_default), ("Library", Library.suite env_default),
("Metavar", Metavar.suite env_default), ("Metavar", Metavar.suite env_default),
("Proofs", Proofs.suite env_default), ("Proofs", Proofs.suite env_default),

View File

@ -83,7 +83,7 @@ def test_m_couple: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -92,7 +92,7 @@ def test_m_couple: TestM Unit := do
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
-- Set m to 3 -- Set m to 3
let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 3") with let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 3") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -115,7 +115,7 @@ def test_m_couple_simp: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -126,7 +126,7 @@ def test_m_couple_simp: TestM Unit := do
addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) = addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
#[#["_uniq.38"], #["_uniq.38"], #[]]) #[#["_uniq.38"], #["_uniq.38"], #[]])
let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -140,7 +140,7 @@ def test_m_couple_simp: TestM Unit := do
addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) = addTest $ LSpec.check "exact 2" ((← state1b.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ 2", .some "2 ≤ 5"]) #[.some "2 ≤ 2", .some "2 ≤ 5"])
addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone addTest $ LSpec.test "(2 root)" state1b.rootExpr?.isNone
let state3 ← match ← state1b.tryTactic (goalId := 0) (tactic := "simp") with let state3 ← match ← state1b.tacticOn (goalId := 0) (tactic := "simp") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -150,7 +150,7 @@ def test_m_couple_simp: TestM Unit := do
addTest $ assertUnreachable $ msg addTest $ assertUnreachable $ msg
return () return ()
| .ok state => pure state | .ok state => pure state
let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := "simp") with let state5 ← match ← state4.tacticOn (goalId := 0) (tactic := "simp") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -177,7 +177,7 @@ def test_proposition_generation: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply PSigma.mk") with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply PSigma.mk") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -191,7 +191,7 @@ def test_proposition_generation: TestM Unit := do
addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})")
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := "λ (x: Nat) => _") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -201,7 +201,7 @@ def test_proposition_generation: TestM Unit := do
addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
let assign := "Eq.refl x" let assign := "Eq.refl x"
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := assign) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -220,7 +220,7 @@ def test_partial_continuation: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "apply Nat.le_trans") with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "apply Nat.le_trans") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -228,7 +228,7 @@ def test_partial_continuation: TestM Unit := do
addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) = addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
#[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "apply Nat.succ") with let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "apply Nat.succ") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString

View File

@ -91,7 +91,7 @@ def test_identity: TestM Unit := do
return () return ()
let tactic := "intro p h" let tactic := "intro p h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn 0 tactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -118,7 +118,7 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n m") with let state1 ← match ← state0.tacticOn 0 "intro n m" with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -126,13 +126,13 @@ def test_nat_add_comm (manual: Bool): TestM Unit := do
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"]) #[buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"])
match ← state1.tryTactic (goalId := 0) (tactic := "assumption") with match ← state1.tacticOn 0 "assumption" with
| .failure #[message] => | .failure #[message] =>
addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n") addTest $ LSpec.check "assumption" (message = "tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n")
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "rw [Nat.add_comm]") with let state2 ← match ← state1.tacticOn 0 "rw [Nat.add_comm]" with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -150,14 +150,14 @@ def test_delta_variable: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro n") with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := "intro n") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) = addTest $ LSpec.check "intro n" ((← state1.serializeGoals (parent := state0) options).map (·.devolatilize) =
#[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"]) #[buildGoalSelective [("n", .some "Nat")] "∀ (b : Nat), n + b = b + n"])
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "intro m") with let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "intro m") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -189,14 +189,14 @@ def test_arith: TestM Unit := do
return () return ()
let tactic := "intros" let tactic := "intros"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check tactic (state1.goals.length = 1) addTest $ LSpec.check tactic (state1.goals.length = 1)
addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone
let state2 ← match ← state1.tryTactic (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 let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -204,7 +204,7 @@ def test_arith: TestM Unit := do
addTest $ LSpec.check "simp ..." (state2.goals.length = 1) addTest $ LSpec.check "simp ..." (state2.goals.length = 1)
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
let tactic := "assumption" let tactic := "assumption"
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -239,7 +239,7 @@ def test_or_comm: TestM Unit := do
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
let tactic := "intro p q h" let tactic := "intro p q h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -265,7 +265,7 @@ def test_or_comm: TestM Unit := do
serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false) serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))") addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) 2 1 0))))")
let tactic := "cases h" let tactic := "cases h"
let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with let state2 ← match ← state1.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -289,7 +289,7 @@ def test_or_comm: TestM Unit := do
addTest $ LSpec.test "(2 parent)" (state2parent == addTest $ LSpec.test "(2 parent)" (state2parent ==
s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})") s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) {motive} (:fv {fvH}) {caseL} {caseR} {conduit})")
let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with let state3_1 ← match ← state2.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -298,7 +298,7 @@ def test_or_comm: TestM Unit := do
serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false) serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))") addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.91))")
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -307,13 +307,13 @@ def test_or_comm: TestM Unit := do
let state4_1parent ← instantiateAll state4_1.parentExpr?.get! let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with let state3_2 ← match ← state2.tacticOn (goalId := 1) (tactic := "apply Or.inl") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1) addTest $ LSpec.check "· apply Or.inl" (state3_2.goals.length = 1)
let state4_2 ← match ← state3_2.tryTactic (goalId := 0) (tactic := "assumption") with let state4_2 ← match ← state3_2.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -327,13 +327,13 @@ def test_or_comm: TestM Unit := do
return () return ()
| .ok state => pure state | .ok state => pure state
addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0]) addTest $ LSpec.test "(resume)" (state2b.goals == [state2.goals.get! 0])
let state3_1 ← match ← state2b.tryTactic (goalId := 0) (tactic := "apply Or.inr") with let state3_1 ← match ← state2b.tacticOn (goalId := 0) (tactic := "apply Or.inr") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with let state4_1 ← match ← state3_1.tacticOn (goalId := 0) (tactic := "assumption") with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -372,7 +372,7 @@ def test_conv: TestM Unit := do
return () return ()
let tactic := "intro a b c1 c2 h" let tactic := "intro a b c1 c2 h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -380,7 +380,7 @@ def test_conv: TestM Unit := do
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "a + b + c1 = b + a + c2"]) #[interiorGoal [] "a + b + c1 = b + a + c2"])
let state2 ← match ← state1.conv (goalId := 0) with let state2 ← match ← state1.conv (state1.get! 0) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -389,7 +389,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }]) #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
let convTactic := "rhs" let convTactic := "rhs"
let state3R ← match ← state2.tryTactic (goalId := 0) convTactic with let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -398,7 +398,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "b + a + c2" with isConversion := true }]) #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
let convTactic := "lhs" let convTactic := "lhs"
let state3L ← match ← state2.tryTactic (goalId := 0) convTactic with let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -407,7 +407,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "a + b + c1" with isConversion := true }]) #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
let convTactic := "congr" let convTactic := "congr"
let state4 ← match ← state3L.tryTactic (goalId := 0) convTactic with let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -419,7 +419,7 @@ def test_conv: TestM Unit := do
]) ])
let convTactic := "rw [Nat.add_comm]" let convTactic := "rw [Nat.add_comm]"
let state5_1 ← match ← state4.tryTactic (goalId := 0) convTactic with let state5_1 ← match ← state4.tacticOn (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -428,7 +428,7 @@ def test_conv: TestM Unit := do
#[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }]) #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
let convTactic := "rfl" let convTactic := "rfl"
let state6_1 ← match ← state5_1.tryTactic (goalId := 0) convTactic with let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -443,7 +443,7 @@ def test_conv: TestM Unit := do
return () return ()
let convTactic := "rfl" let convTactic := "rfl"
let state6 ← match ← state4_1.tryTactic (goalId := 0) convTactic with let state6 ← match ← state4_1.tacticOn (goalId := 0) convTactic with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -458,7 +458,7 @@ def test_conv: TestM Unit := do
return () return ()
let tactic := "exact h" let tactic := "exact h"
let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with let stateF ← match ← state1_1.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -485,7 +485,7 @@ def test_calc: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let tactic := "intro a b c d h1 h2" let tactic := "intro a b c d h1 h2"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -493,7 +493,7 @@ def test_calc: TestM Unit := do
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[interiorGoal [] "a + b = c + d"]) #[interiorGoal [] "a + b = c + d"])
let pred := "a + b = b + c" let pred := "a + b = b + c"
let state2 ← match ← state1.tryCalc (goalId := 0) (pred := pred) with let state2 ← match ← state1.tryCalc (state1.get! 0) (pred := pred) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -503,11 +503,11 @@ def test_calc: TestM Unit := do
interiorGoal [] "a + b = b + c" (.some "calc"), interiorGoal [] "a + b = b + c" (.some "calc"),
interiorGoal [] "b + c = c + d" interiorGoal [] "b + c = c + d"
]) ])
addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? 0 |>.isNone) addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? 1 |>.isSome) addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)
let tactic := "apply h1" let tactic := "apply h1"
let state2m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with let state2m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -518,7 +518,7 @@ def test_calc: TestM Unit := do
addTest $ expectationFailure "continue" e addTest $ expectationFailure "continue" e
return () return ()
let pred := "_ = c + d" let pred := "_ = c + d"
let state4 ← match ← state3.tryCalc (goalId := 0) (pred := pred) with let state4 ← match ← state3.tryCalc (state3.get! 0) (pred := pred) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -527,9 +527,9 @@ def test_calc: TestM Unit := do
#[ #[
interiorGoal [] "b + c = c + d" (.some "calc") interiorGoal [] "b + c = c + d" (.some "calc")
]) ])
addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? 0 |>.isNone) addTest $ LSpec.test "(4.0 prev rhs)" (state4.calcPrevRhsOf? (state4.get! 0) |>.isNone)
let tactic := "apply h2" let tactic := "apply h2"
let state4m ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with let state4m ← match ← state4.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -549,7 +549,7 @@ def test_nat_zero_add: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let tactic := "intro n" let tactic := "intro n"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -557,7 +557,7 @@ def test_nat_zero_add: TestM Unit := do
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat")] "n + 0 = n"]) #[buildGoal [("n", "Nat")] "n + 0 = n"])
let recursor := "@Nat.brecOn" let recursor := "@Nat.brecOn"
let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -571,7 +571,7 @@ def test_nat_zero_add: TestM Unit := do
]) ])
let tactic := "exact n" let tactic := "exact n"
let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with let state3b ← match ← state2.tacticOn (goalId := 1) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -584,7 +584,7 @@ def test_nat_zero_add: TestM Unit := do
addTest $ assertUnreachable e addTest $ assertUnreachable e
return () return ()
let tactic := "exact (λ x => x + 0 = x)" let tactic := "exact (λ x => x + 0 = x)"
let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with let state3c ← match ← state2b.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -597,7 +597,7 @@ def test_nat_zero_add: TestM Unit := do
addTest $ assertUnreachable e addTest $ assertUnreachable e
return () return ()
let tactic := "intro t h" let tactic := "intro t h"
let state3 ← match ← state2c.tryTactic (goalId := 0) (tactic := tactic) with let state3 ← match ← state2c.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -606,7 +606,7 @@ def test_nat_zero_add: TestM Unit := do
#[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
let tactic := "simp" let tactic := "simp"
let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with let state3d ← match ← state3.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -617,7 +617,7 @@ def test_nat_zero_add: TestM Unit := do
addTest $ assertUnreachable e addTest $ assertUnreachable e
return () return ()
let tactic := "rfl" let tactic := "rfl"
let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with let stateF ← match ← state2d.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -637,7 +637,7 @@ def test_nat_zero_add_alt: TestM Unit := do
addTest $ assertUnreachable "Goal could not parse" addTest $ assertUnreachable "Goal could not parse"
return () return ()
let tactic := "intro n" let tactic := "intro n"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -645,7 +645,7 @@ def test_nat_zero_add_alt: TestM Unit := do
addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat")] "n + 0 = n"]) #[buildGoal [("n", "Nat")] "n + 0 = n"])
let recursor := "@Nat.brecOn" let recursor := "@Nat.brecOn"
let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with let state2 ← match ← state1.tryMotivatedApply (state1.get! 0) (recursor := recursor) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -660,7 +660,7 @@ def test_nat_zero_add_alt: TestM Unit := do
]) ])
let tactic := "intro x" let tactic := "intro x"
let state3m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with let state3m ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -668,7 +668,7 @@ def test_nat_zero_add_alt: TestM Unit := do
addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) = addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) =
#[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")]) #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")])
let tactic := "apply Eq" let tactic := "apply Eq"
let state3m2 ← match ← state3m.tryTactic (goalId := 0) (tactic := tactic) with let state3m2 ← match ← state3m.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString

View File

@ -55,7 +55,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))" let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr let state0 ← GoalState.create rootExpr
let tactic := "intro p q h" let tactic := "intro p q h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -64,7 +64,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"]) #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"])
let expr := "Or.inl (Or.inl h)" let expr := "Or.inl (Or.inl h)"
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -74,7 +74,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
let evalBind := "y" let evalBind := "y"
let evalExpr := "Or.inl h" let evalExpr := "Or.inl h"
let state2 ← match ← state1.tryDefine (goalId := 0) (binderName := evalBind) (expr := evalExpr) with let state2 ← match ← state1.tryDefine (state1.get! 0) (binderName := evalBind) (expr := evalExpr) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -94,7 +94,7 @@ def test_define_proof : TestT Elab.TermElabM Unit := do
}]) }])
let expr := "Or.inl y" let expr := "Or.inl y"
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -112,22 +112,22 @@ def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
def test_define_root_expr : TestT Elab.TermElabM Unit := do def test_define_root_expr : TestT Elab.TermElabM Unit := do
--let rootExpr ← parseSentence "Nat" --let rootExpr ← parseSentence "Nat"
--let state0 ← GoalState.create rootExpr --let state0 ← GoalState.create rootExpr
--let .success state1 ← state0.tryTactic (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5" --let .success state1 ← state0.tacticOn (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
--let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr" --let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
--addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5") --addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p" let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
let state0 ← GoalState.create rootExpr let state0 ← GoalState.create rootExpr
let tactic := "intro p x" let tactic := "intro p x"
let .success state1 ← state0.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic let .success state1 ← state0.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
let binderName := `binder let binderName := `binder
let value := "x.fst" let value := "x.fst"
let expr ← state1.goals[0]!.withContext $ strToTermSyntax value let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
let tacticM := Tactic.evalDefine binderName expr let tacticM := Tactic.evalDefine binderName expr
let .success state2 ← state1.tryTacticM (goalId := 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}" let .success state2 ← state1.tryTacticM (state1.get! 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
let tactic := s!"apply {binderName}" let tactic := s!"apply {binderName}"
let .success state3 ← state2.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic let .success state3 ← state2.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
let tactic := s!"exact 5" let tactic := s!"exact 5"
let .success state4 ← state3.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic let .success state4 ← state3.tacticOn (goalId := 0) tactic | addTest $ assertUnreachable tactic
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr" let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5") addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5")
@ -139,7 +139,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))" let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr let state0 ← GoalState.create rootExpr
let tactic := "intro p q h" let tactic := "intro p q h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -148,7 +148,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"]) #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p q) p q"])
let expr := "Or.inl (Or.inl h)" let expr := "Or.inl (Or.inl h)"
let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with let state2 ← match ← state1.tryAssign (state1.get! 0) (expr := expr) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -158,7 +158,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
let haveBind := "y" let haveBind := "y"
let haveType := "p q" let haveType := "p q"
let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with let state2 ← match ← state1.tryHave (state1.get! 0) (binderName := haveBind) (type := haveType) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -170,7 +170,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
]) ])
let expr := "Or.inl h" let expr := "Or.inl h"
let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with let state3 ← match ← state2.tryAssign (state2.get! 0) (expr := expr) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -184,7 +184,7 @@ def test_have_proof : TestT Elab.TermElabM Unit := do
addTest $ assertUnreachable e addTest $ assertUnreachable e
return () return ()
let expr := "Or.inl y" let expr := "Or.inl y"
let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with let state4 ← match ← state2b.tryAssign (state2b.get! 0) (expr := expr) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -199,7 +199,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))" let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p q) (p q))"
let state0 ← GoalState.create rootExpr let state0 ← GoalState.create rootExpr
let tactic := "intro a p h" let tactic := "intro a p h"
let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with let state1 ← match ← state0.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -213,8 +213,8 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
let letType := "Nat" let letType := "Nat"
let expr := s!"let b: {letType} := _; _" let expr := s!"let b: {letType} := _; _"
let result2 ← match specialized with let result2 ← match specialized with
| true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) | true => state1.tryLet (state1.get! 0) (binderName := "b") (type := letType)
| false => state1.tryAssign (goalId := 0) (expr := expr) | false => state1.tryAssign (state1.get! 0) (expr := expr)
let state2 ← match result2 with let state2 ← match result2 with
| .success state => pure state | .success state => pure state
| other => do | other => do
@ -240,7 +240,7 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
]) ])
let tactic := "exact 1" let tactic := "exact 1"
let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with let state3 ← match ← state2.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
@ -266,14 +266,14 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
]) ])
let tactic := "exact h" let tactic := "exact h"
match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
| .failure #[message] => | .failure #[message] =>
addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop") addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop")
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
let tactic := "exact Or.inl (Or.inl h)" let tactic := "exact Or.inl (Or.inl h)"
let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with let state4 ← match ← state3r.tacticOn (goalId := 0) (tactic := tactic) with
| .success state => pure state | .success state => pure state
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString

View File

@ -37,14 +37,25 @@
}; };
project = leanPkgs.buildLeanPackage { project = leanPkgs.buildLeanPackage {
name = "Pantograph"; name = "Pantograph";
roots = [ "Main" "Pantograph" ]; roots = [ "Pantograph" ];
src = pkgs.lib.cleanSourceWith { src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.; src = ./.;
filter = path: type: filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) && !(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path) && !(pkgs.lib.hasSuffix ".md" path) &&
!(pkgs.lib.hasSuffix "Makefile" path); !(pkgs.lib.hasSuffix "Repl.lean" path);
}; });
};
repl = leanPkgs.buildLeanPackage {
name = "Repl";
roots = [ "Main" "Repl" ];
deps = [ project ];
src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.;
filter = path: type:
!(pkgs.lib.hasInfix "/Test/" path) &&
!(pkgs.lib.hasSuffix ".md" path);
});
}; };
test = leanPkgs.buildLeanPackage { test = leanPkgs.buildLeanPackage {
name = "Test"; name = "Test";
@ -52,18 +63,19 @@
# root begins (e.g. `import Test.Environment` and not `import # root begins (e.g. `import Test.Environment` and not `import
# Environment`) and thats where `lakefile.lean` resides. # Environment`) and thats where `lakefile.lean` resides.
roots = [ "Test.Main" ]; roots = [ "Test.Main" ];
deps = [ lspecLib project ]; deps = [ lspecLib repl ];
src = pkgs.lib.cleanSourceWith { src = pkgs.lib.cleanSource (pkgs.lib.cleanSourceWith {
src = ./.; src = ./.;
filter = path: type: filter = path: type:
!(pkgs.lib.hasInfix "Pantograph" path); !(pkgs.lib.hasInfix "Pantograph" path);
}; });
}; };
in rec { in rec {
packages = { packages = {
inherit (leanPkgs) lean lean-all; inherit (leanPkgs) lean lean-all;
inherit (project) sharedLib executable; inherit (project) sharedLib;
default = project.executable; inherit (repl) executable;
default = repl.executable;
}; };
legacyPackages = { legacyPackages = {
inherit project leanPkgs; inherit project leanPkgs;

View File

@ -4,11 +4,14 @@ open Lake DSL
package pantograph package pantograph
lean_lib Pantograph { lean_lib Pantograph {
roots := #[`Pantograph]
defaultFacets := #[LeanLib.sharedFacet] defaultFacets := #[LeanLib.sharedFacet]
} }
lean_lib Repl {
}
@[default_target] @[default_target]
lean_exe pantograph { lean_exe repl {
root := `Main root := `Main
-- Solves the native symbol not found problem -- Solves the native symbol not found problem
supportInterpreter := true supportInterpreter := true