Enable handling of m-Coupled goals #20

Merged
aniva merged 11 commits from goal/dependency into dev 2023-10-27 19:30:21 -07:00
6 changed files with 68 additions and 36 deletions
Showing only changes of commit 0ecfa9fc26 - Show all commits

View File

@ -143,7 +143,12 @@ protected def GoalState.continue (target: GoalState) (graftee: GoalState): Excep
} }
protected def GoalState.rootExpr (goalState: GoalState): Option Expr := protected def GoalState.rootExpr (goalState: GoalState): Option Expr :=
goalState.mctx.eAssignment.find? goalState.root |>.filter (λ e => ¬ e.hasMVar) let expr := goalState.mctx.eAssignment.find! goalState.root
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
if expr.hasMVar then
.none
else
.some expr
-- Diagnostics functions -- Diagnostics functions
@ -183,7 +188,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalPrin
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): Elab.TermElabM Unit := do
if options.printContext then if options.printContext then
decl.lctx.fvarIdToDecl.forM printFVar decl.lctx.fvarIdToDecl.forM printFVar
let type_sexp serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false) let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
if options.printValue then if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then

View File

@ -43,7 +43,10 @@ structure Expression where
deriving Lean.ToJson deriving Lean.ToJson
structure Variable where structure Variable where
name: String /-- The internal name used in raw expressions -/
name: String := ""
/-- The name displayed to the user -/
userName: String
/-- Does the name contain a dagger -/ /-- Does the name contain a dagger -/
isInaccessible?: Option Bool := .none isInaccessible?: Option Bool := .none
type?: Option Expression := .none type?: Option Expression := .none

View File

@ -102,8 +102,8 @@ def serialize_sort_level_ast (level: Level): String :=
/-- /--
Completely serializes an expression tree. Json not used due to compactness Completely serializes an expression tree. Json not used due to compactness
-/ -/
def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
return self expr self expr
where where
self (e: Expr): String := self (e: Expr): String :=
match e with match e with
@ -175,7 +175,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
let pp?: Option String := match options.printExprPretty with let pp?: Option String := match options.printExprPretty with
| true => .some pp | true => .some pp
| false => .none | false => .none
let sexp: String := (← serialize_expression_ast e) let sexp: String := serialize_expression_ast e
let sexp?: Option String := match options.printExprAST with let sexp?: Option String := match options.printExprAST with
| true => .some sexp | true => .some sexp
| false => .none | false => .none
@ -196,27 +196,30 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
Meta.withLCtx lctx mvarDecl.localInstances do Meta.withLCtx lctx mvarDecl.localInstances do
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
match localDecl with match localDecl with
| .cdecl _ _ varName _ _ _ => | .cdecl _ fvarId userName _ _ _ =>
let varName := varName.simpMacroScopes let userName := userName.simpMacroScopes
return { return {
name := toString varName, name := of_name fvarId.name,
userName:= of_name userName.simpMacroScopes,
} }
| .ldecl _ _ varName _ _ _ _ => do | .ldecl _ fvarId userName _ _ _ _ => do
return { return {
name := toString varName, name := of_name fvarId.name,
userName := toString userName.simpMacroScopes,
} }
let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
match localDecl with match localDecl with
| .cdecl _ _ varName type _ _ => | .cdecl _ fvarId userName type _ _ =>
let varName := varName.simpMacroScopes let userName := userName.simpMacroScopes
let type ← instantiateMVars type let type ← instantiateMVars type
return { return {
name := toString varName, name := of_name fvarId.name,
isInaccessible? := .some varName.isInaccessibleUserName userName:= of_name userName,
isInaccessible? := .some userName.isInaccessibleUserName
type? := .some (← serialize_expression options type) type? := .some (← serialize_expression options type)
} }
| .ldecl _ _ varName type val _ _ => do | .ldecl _ fvarId userName type val _ _ => do
let varName := varName.simpMacroScopes let userName := userName.simpMacroScopes
let type ← instantiateMVars type let type ← instantiateMVars type
let value? ← if showLetValues then let value? ← if showLetValues then
let val ← instantiateMVars val let val ← instantiateMVars val
@ -224,8 +227,9 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
else else
pure $ .none pure $ .none
return { return {
name := toString varName, name := of_name fvarId.name,
isInaccessible? := .some varName.isInaccessibleUserName userName:= of_name userName,
isInaccessible? := .some userName.isInaccessibleUserName
type? := .some (← serialize_expression options type) type? := .some (← serialize_expression options type)
value? := value? value? := value?
} }
@ -242,13 +246,13 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe
| false => ppVar localDecl | false => ppVar localDecl
return var::acc return var::acc
return { return {
caseName? := match mvarDecl.userName with caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
| Name.anonymous => .none
| name => .some <| toString name,
isConversion := isLHSGoal? mvarDecl.type |>.isSome, isConversion := isLHSGoal? mvarDecl.type |>.isSome,
target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
vars := vars.reverse.toArray vars := vars.reverse.toArray
} }
where
of_name (n: Name) := name_to_ast n (sanitize := false)

19
Test/Common.lean Normal file
View File

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

View File

@ -4,6 +4,7 @@ Tests pertaining to goals with no interdependencies
import LSpec import LSpec
import Pantograph.Goal import Pantograph.Goal
import Pantograph.Serial import Pantograph.Serial
import Test.Common
namespace Pantograph namespace Pantograph
@ -69,7 +70,7 @@ def buildGoal (nameType: List (String × String)) (target: String): Protocol.Goa
{ {
target := { pp? := .some target}, target := { pp? := .some target},
vars := (nameType.map fun x => ({ vars := (nameType.map fun x => ({
name := x.fst, userName := x.fst,
type? := .some { pp? := .some x.snd }, type? := .some { pp? := .some x.snd },
isInaccessible? := .some false isInaccessible? := .some false
})).toArray })).toArray
@ -79,7 +80,7 @@ def buildGoalSelective (nameType: List (String × Option String)) (target: Strin
{ {
target := { pp? := .some target}, target := { pp? := .some target},
vars := (nameType.map fun x => ({ vars := (nameType.map fun x => ({
name := x.fst, userName := x.fst,
type? := x.snd.map (λ type => { pp? := type }), type? := x.snd.map (λ type => { pp? := type }),
isInaccessible? := x.snd.map (λ _ => false) isInaccessible? := x.snd.map (λ _ => false)
})).toArray })).toArray
@ -104,7 +105,6 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
| .ok (_, a) => | .ok (_, a) =>
return a return a
-- Individual test cases -- Individual test cases
example: ∀ (a b: Nat), a + b = b + a := by example: ∀ (a b: Nat), a + b = b + a := by
intro n m intro n m
@ -125,7 +125,7 @@ def proof_nat_add_comm (manual: Bool): TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "intro n m" (goal1 = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n") addTest $ LSpec.check "intro n m" (goal1.devolatilize = buildGoal [("n", "Nat"), ("m", "Nat")] "n + m = m + n")
match ← state1.execute (goalId := 0) (tactic := "assumption") with match ← state1.execute (goalId := 0) (tactic := "assumption") with
| .failure #[message] => | .failure #[message] =>
@ -170,14 +170,14 @@ def proof_or_comm: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "p q h" (goal1 = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p") addTest $ LSpec.check "p q h" (goal1.devolatilize = buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p")
let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with let (state2, goal1, goal2) ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
| .success state #[goal1, goal2] => pure (state, goal1, goal2) | .success state #[goal1, goal2] => pure (state, goal1, goal2)
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "cases h/1" (goal1 = branchGoal "inl" "p") addTest $ LSpec.check "cases h/1" (goal1.devolatilize = branchGoal "inl" "p")
addTest $ LSpec.check "cases h/2" (goal2 = branchGoal "inr" "q") addTest $ LSpec.check "cases h/2" (goal2.devolatilize = branchGoal "inr" "q")
let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with let (state3_1, _goal) ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
| .success state #[goal] => pure (state, goal) | .success state #[goal] => pure (state, goal)
@ -200,6 +200,7 @@ def proof_or_comm: TestM Unit := do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
addTest $ LSpec.check "4_2 root" state4_2.rootExpr.isNone
-- Ensure the proof can continue from `state4_2`. -- Ensure the proof can continue from `state4_2`.
let state2b ← match state2.continue state4_2 with let state2b ← match state2.continue state4_2 with
| .error msg => do | .error msg => do
@ -217,8 +218,8 @@ def proof_or_comm: TestM Unit := do
| other => do | other => do
addTest $ assertUnreachable $ other.toString addTest $ assertUnreachable $ other.toString
return () return ()
IO.println "===== 4_1 =====" state4_1.print
state4_1.print ({ printNonVisible := false }) addTest $ LSpec.check "4_1 root" state4_1.rootExpr.isSome
return () return ()
where where
@ -227,9 +228,9 @@ def proof_or_comm: TestM Unit := do
caseName? := .some caseName, caseName? := .some caseName,
target := { pp? := .some "q p" }, target := { pp? := .some "q p" },
vars := #[ vars := #[
{ name := "p", type? := .some typeProp, isInaccessible? := .some false }, { userName := "p", type? := .some typeProp, isInaccessible? := .some false },
{ name := "q", type? := .some typeProp, isInaccessible? := .some false }, { userName := "q", type? := .some typeProp, isInaccessible? := .some false },
{ name := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true }
] ]
} }

View File

@ -47,8 +47,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let expr := str_to_name symbol |> env.find? |>.get! |>.type let expr := str_to_name symbol |> env.find? |>.get! |>.type
let test := LSpec.check symbol ((serialize_expression_ast expr) = target) let test := LSpec.check symbol ((serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let coreM := metaM.run' let coreM := metaM.run'
let coreContext: Core.Context := { let coreContext: Core.Context := {
currNamespace := Lean.Name.str .anonymous "Aniva" currNamespace := Lean.Name.str .anonymous "Aniva"