feat: Automatic Mode #92
|
@ -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
|
||||||
|
|
207
Pantograph.lean
207
Pantograph.lean
|
@ -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
|
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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),
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
|
@ -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
|
||||||
|
|
30
flake.nix
30
flake.nix
|
@ -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;
|
||||||
|
|
|
@ -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
|
||||||
|
|
Loading…
Reference in New Issue