From b954f12526eb6eca25d1f77c5b2729ad23b447a3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 13 Apr 2024 19:41:49 -0700 Subject: [PATCH 01/38] refactor: Move all tactic operations to the bottom --- Pantograph/Goal.lean | 127 ++++++++++++++++++++++--------------------- 1 file changed, 64 insertions(+), 63 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 484ff51..c6700b6 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -80,6 +80,70 @@ private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): acc.insert mvarId ) SSet.empty + +protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do + let goal ← state.savedState.tactic.goals.get? goalId + return { + state with + savedState := { + state.savedState with + tactic := { goals := [goal] }, + }, + calcPrevRhs? := .none, + } + +/-- +Brings into scope a list of goals +-/ +protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := + if ¬ (goals.all (λ goal => state.mvars.contains goal)) then + .error s!"Goals not in scope" + else + -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. + let unassigned := goals.filter (λ goal => + let mctx := state.mctx + ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) + .ok { + state with + savedState := { + term := state.savedState.term, + tactic := { goals := unassigned }, + }, + calcPrevRhs? := .none, + } +/-- +Brings into scope all goals from `branch` +-/ +protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState := + if !target.goals.isEmpty then + .error s!"Target state has unresolved goals" + else if target.root != branch.root then + .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}" + else + target.resume (goals := branch.goals) + +protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do + let expr ← goalState.mctx.eAssignment.find? goalState.root + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + if expr.hasMVar then + -- Must not assert that the goal state is empty here. We could be in a branch goal. + --assert! ¬goalState.goals.isEmpty + .none + else + assert! goalState.goals.isEmpty + return expr +protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do + let parent ← goalState.parentMVar? + let expr := goalState.mctx.eAssignment.find! parent + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + return expr +protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do + let expr ← goalState.mctx.eAssignment.find? mvar + let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) + return expr + +--- Tactic execution functions --- + /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do @@ -446,67 +510,4 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): catch exception => return .failure #[← exception.toMessageData.toString] - -protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState := do - let goal ← state.savedState.tactic.goals.get? goalId - return { - state with - savedState := { - state.savedState with - tactic := { goals := [goal] }, - }, - calcPrevRhs? := .none, - } - -/-- -Brings into scope a list of goals --/ -protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := - if ¬ (goals.all (λ goal => state.mvars.contains goal)) then - .error s!"Goals not in scope" - else - -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. - let unassigned := goals.filter (λ goal => - let mctx := state.mctx - ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal)) - .ok { - state with - savedState := { - term := state.savedState.term, - tactic := { goals := unassigned }, - }, - calcPrevRhs? := .none, - } -/-- -Brings into scope all goals from `branch` --/ -protected def GoalState.continue (target: GoalState) (branch: GoalState): Except String GoalState := - if !target.goals.isEmpty then - .error s!"Target state has unresolved goals" - else if target.root != branch.root then - .error s!"Roots of two continued goal states do not match: {target.root.name} != {branch.root.name}" - else - target.resume (goals := branch.goals) - -protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do - let expr ← goalState.mctx.eAssignment.find? goalState.root - let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) - if expr.hasMVar then - -- Must not assert that the goal state is empty here. We could be in a branch goal. - --assert! ¬goalState.goals.isEmpty - .none - else - assert! goalState.goals.isEmpty - return expr -protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do - let parent ← goalState.parentMVar? - let expr := goalState.mctx.eAssignment.find! parent - let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) - return expr -protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do - let expr ← goalState.mctx.eAssignment.find? mvar - let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) - return expr - - end Pantograph -- 2.44.1 From 75b4648ba9d53e7032c1196b55e92483ca761a24 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 14 Apr 2024 15:40:57 -0700 Subject: [PATCH 02/38] feat: mapply stub --- Pantograph/Goal.lean | 66 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index c6700b6..176e48e 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -252,6 +252,7 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.tryAssign let expr ← match Parser.runParserCategory (env := state.env) (catName := `term) @@ -275,6 +276,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.tryHave let type ← match Parser.runParserCategory (env := state.env) (catName := `term) @@ -324,6 +326,7 @@ protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: Str let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.tryLet let type ← match Parser.runParserCategory (env := state.env) (catName := `term) @@ -369,6 +372,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat): let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure goal | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.conv let tacticM : Elab.Tactic.TacticM (Elab.Tactic.SavedState × MVarId) := do state.restoreTacticM goal @@ -452,6 +456,7 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error + goal.checkNotAssigned `GoalState.tryCalc let calcPrevRhs? := state.calcPrevRhsOf? goalId let target ← instantiateMVars (← goal.getDecl).type let tag := (← goal.getDecl).userName @@ -510,4 +515,65 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): catch exception => return .failure #[← exception.toMessageData.toString] +def getForallArgsBody: Expr → List Expr × Expr + | .forallE _ d b _ => + let (innerArgs, innerBody) := getForallArgsBody b + (d :: innerArgs, innerBody) + | e => ([], e) +def collectMotiveArguments (forallBody: Expr): SSet Nat := + -- Get all de Bruijn indices + Id.run $ do + Expr.foldlM (λ acc subexpr => do + match subexpr with + | .app (.bvar i) _ => return acc.insert i + | _ => return acc + ) SSet.empty forallBody + +protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.tryMotivatedApply + + let recursor ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := recursor) + (fileName := filename) with + | .ok syn => pure syn + | .error error => return .parseError error + try + -- Implemented similarly to the intro tactic + let nextGoals: List MVarId ← goal.withContext do + let recursor ← Elab.Term.elabType (stx := recursor) + let recursorType ← Meta.inferType recursor + + let (forallArgs, forallBody) := getForallArgsBody recursorType + let motiveIndices := collectMotiveArguments forallBody + + let numArgs ← Meta.getExpectedNumArgs recursorType + + let rec go (i: Nat): MetaM (List MVarId × Expr) := do + let argType := forallArgs.get! i + sorry + let (newMVars, assign) ← go numArgs + + goal.assign assign + + pure newMVars + return .success { + root := state.root, + savedState := { + term := ← MonadBacktrack.saveState, + tactic := { goals := nextGoals } + }, + newMVars := nextGoals.toSSet, + parentMVar? := .some goal, + calcPrevRhs? := .none + } + catch exception => + return .failure #[← exception.toMessageData.toString] + end Pantograph -- 2.44.1 From dbd54f767938027c43427a0eb90245ccc420e26d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Apr 2024 12:47:02 -0700 Subject: [PATCH 03/38] feat: Implement the mapply tactic --- Pantograph/Goal.lean | 24 ++++++++---- Test/Common.lean | 11 ++++-- Test/Proofs.lean | 87 +++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 111 insertions(+), 11 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 176e48e..0fdf2e1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -547,7 +547,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu try -- Implemented similarly to the intro tactic let nextGoals: List MVarId ← goal.withContext do - let recursor ← Elab.Term.elabType (stx := recursor) + let recursor ← Elab.Term.elabTerm (stx := recursor) .none let recursorType ← Meta.inferType recursor let (forallArgs, forallBody) := getForallArgsBody recursorType @@ -555,14 +555,24 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu let numArgs ← Meta.getExpectedNumArgs recursorType - let rec go (i: Nat): MetaM (List MVarId × Expr) := do - let argType := forallArgs.get! i - sorry - let (newMVars, assign) ← go numArgs + let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do + if i ≥ numArgs then + return prev + else + let argType := forallArgs.get! i + -- If `argType` has motive references, its goal needs to be placed in it + let argType := argType.instantiateRev prev + -- Create the goal + let argGoal ← Meta.mkFreshExprMVar argType .natural .anonymous + let prev := prev ++ [argGoal] + go (i + 1) prev + termination_by numArgs - i + let newMVars ← go 0 #[] - goal.assign assign + -- Create the main goal for the return type of the recursor + goal.assign (mkAppN recursor newMVars) - pure newMVars + pure $ newMVars.toList.map (·.mvarId!) return .success { root := state.root, savedState := { diff --git a/Test/Common.lean b/Test/Common.lean index 8719ebd..8b8e977 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -10,11 +10,9 @@ namespace Pantograph -- Auxiliary functions namespace Protocol -/-- Set internal names to "" -/ -def Goal.devolatilize (goal: Goal): Goal := +def Goal.devolatilizeVars (goal: Goal): Goal := { goal with - name := "", vars := goal.vars.map removeInternalAux, } where removeInternalAux (v: Variable): Variable := @@ -22,6 +20,13 @@ def Goal.devolatilize (goal: Goal): Goal := v with name := "" } +/-- Set internal names to "" -/ +def Goal.devolatilize (goal: Goal): Goal := + { + goal.devolatilizeVars with + name := "", + } + deriving instance DecidableEq, Repr for Expression deriving instance DecidableEq, Repr for Variable deriving instance DecidableEq, Repr for Goal diff --git a/Test/Proofs.lean b/Test/Proofs.lean index e14ba4a..ae94054 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -49,6 +49,16 @@ def startProof (start: Start): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal +def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String): Protocol.Goal := + { + name, + target := { pp? := .some target}, + vars := (nameType.map fun x => ({ + userName := x.fst, + type? := .some { pp? := .some x.snd }, + isInaccessible? := .some false + })).toArray + } def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { userName?, @@ -582,7 +592,7 @@ def test_let (specialized: Bool): TestM Unit := do interiorGoal [] "let b := ?m.20;\np ∨ ¬p" ]) -- Check that the goal mvar ids match up - addTest $ LSpec.check expr ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20") + addTest $ LSpec.check "(mvarId)" ((serializedState2.map (·.name) |>.get! 0) = "_uniq.20") let tactic := "exact a" let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with @@ -625,6 +635,80 @@ def test_let (specialized: Bool): TestM Unit := do let free := [("a", "Nat"), ("p", "Prop"), ("h", "p")] ++ free buildGoal free target userName? +def test_nat_zero_add: TestM Unit := do + let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro n" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat")] "n + 0 = n"]) + let recursor := "@Nat.brecOn" + let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = + #[ + buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66", + buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat", + buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t" + ]) + + let tactic := "exact n" + let state3b ← match ← state2.tryTactic (goalId := 1) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3b.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + let state2b ← match state3b.continue state2 with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let tactic := "exact (λ x => x + 0 = x)" + let state3c ← match ← state2b.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3c.serializeGoals (options := ← read)).map (·.devolatilize) = + #[]) + let state2c ← match state3c.continue state2b with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let tactic := "intro t h" + let state3 ← match ← state2c.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) + + let tactic := "simp" + let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) = + #[]) + + addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Nat.add_comm", test_nat_add_comm false), @@ -637,6 +721,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("calc", test_calc), ("let via assign", test_let false), ("let via tryLet", test_let true), + ("Nat.zero_add", test_nat_zero_add), ] tests.map (fun (name, test) => (name, proofRunner env test)) -- 2.44.1 From 7aa7e6d7e948a22cec20a259c4f244f11711be65 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 15 Apr 2024 12:56:28 -0700 Subject: [PATCH 04/38] feat: Library interface for mapply --- Pantograph/Library.lean | 58 +++++++++++++++++++---------------------- 1 file changed, 27 insertions(+), 31 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6b8e2e2..01b5a42 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -158,37 +158,6 @@ def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := | .ok expr => pure $ expr return .ok $ ← GoalState.create expr -@[export pantograph_goal_tactic_m] -def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := - runTermElabM <| state.tryTactic goalId tactic - -@[export pantograph_goal_assign_m] -def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := - runTermElabM <| state.tryAssign goalId expr - -@[export pantograph_goal_have_m] -def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := - runTermElabM <| state.tryHave goalId binderName type -@[export pantograph_goal_let_m] -def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := - runTermElabM <| state.tryLet goalId binderName type - -@[export pantograph_goal_conv_m] -def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := - runTermElabM <| state.conv goalId - -@[export pantograph_goal_conv_exit_m] -def goalConvExit (state: GoalState): Lean.CoreM TacticResult := - runTermElabM <| state.convExit - -@[export pantograph_goal_calc_m] -def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult := - runTermElabM <| state.tryCalc goalId pred - -@[export pantograph_goal_focus] -def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := - state.focus goalId - @[export pantograph_goal_resume] def goalResume (target: GoalState) (goals: Array String): Except String GoalState := target.resume (goals.map (λ n => { name := n.toName }) |>.toList) @@ -212,5 +181,32 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto serializeExpression options (← unfoldAuxLemmas expr)), } +@[export pantograph_goal_tactic_m] +def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryTactic goalId tactic +@[export pantograph_goal_assign_m] +def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryAssign goalId expr +@[export pantograph_goal_have_m] +def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryHave goalId binderName type +@[export pantograph_goal_let_m] +def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryLet goalId binderName type +@[export pantograph_goal_conv_m] +def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := + runTermElabM <| state.conv goalId +@[export pantograph_goal_conv_exit_m] +def goalConvExit (state: GoalState): Lean.CoreM TacticResult := + runTermElabM <| state.convExit +@[export pantograph_goal_calc_m] +def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryCalc goalId pred +@[export pantograph_goal_focus] +def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := + state.focus goalId +@[export pantograph_goal_motivated_apply_m] +def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryMotivatedApply goalId recursor end Pantograph -- 2.44.1 From fec13ddb5176323a2878f00be197fa976c5c7e1e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 18 Apr 2024 14:19:25 -0700 Subject: [PATCH 05/38] chore: Code cleanup --- Pantograph/Goal.lean | 27 +++++++++++++++++---------- Pantograph/Library.lean | 2 +- Test/Proofs.lean | 11 +++++++---- 3 files changed, 25 insertions(+), 15 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0fdf2e1..5c6a583 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -232,7 +232,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): -- Generate a list of mvarIds that exist in the parent state; Also test the -- assertion that the types have not changed on any mvars. let newMVars := newMVarSet prevMCtx nextMCtx - let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned)) + let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned) return .success { root := state.root, savedState := { @@ -521,13 +521,9 @@ def getForallArgsBody: Expr → List Expr × Expr (d :: innerArgs, innerBody) | e => ([], e) def collectMotiveArguments (forallBody: Expr): SSet Nat := - -- Get all de Bruijn indices - Id.run $ do - Expr.foldlM (λ acc subexpr => do - match subexpr with - | .app (.bvar i) _ => return acc.insert i - | _ => return acc - ) SSet.empty forallBody + match forallBody with + | .app (.bvar i) _ => SSet.empty.insert i + | _ => SSet.empty protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Elab.TermElabM TacticResult := do @@ -552,6 +548,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu let (forallArgs, forallBody) := getForallArgsBody recursorType let motiveIndices := collectMotiveArguments forallBody + --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}" let numArgs ← Meta.getExpectedNumArgs recursorType @@ -563,16 +560,26 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu -- If `argType` has motive references, its goal needs to be placed in it let argType := argType.instantiateRev prev -- Create the goal - let argGoal ← Meta.mkFreshExprMVar argType .natural .anonymous + let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous + let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName) + IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}" let prev := prev ++ [argGoal] go (i + 1) prev termination_by numArgs - i let newMVars ← go 0 #[] + -- FIXME: Add an `Eq` target and swap out the motive type + + --let sourceType := forallBody.instantiateRev newMVars + --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $ + -- Meta.isDefEq sourceType (← goal.getType) do + -- throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" + -- Create the main goal for the return type of the recursor goal.assign (mkAppN recursor newMVars) - pure $ newMVars.toList.map (·.mvarId!) + let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) + pure nextGoals return .success { root := state.root, savedState := { diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 01b5a42..00b4bc7 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -38,7 +38,7 @@ namespace Pantograph def defaultTermElabMContext: Lean.Elab.Term.Context := { autoBoundImplicit := true, - declName? := some "_pantograph".toName, + declName? := .some `_pantograph, errToSorry := false } def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ae94054..1adc9d4 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -49,9 +49,11 @@ def startProof (start: Start): TestM (Option GoalState) := do let goal ← GoalState.create (expr := expr) return Option.some goal -def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String): Protocol.Goal := +def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String) + (userName?: Option String := .none): Protocol.Goal := { name, + userName?, target := { pp? := .some target}, vars := (nameType.map fun x => ({ userName := x.fst, @@ -59,7 +61,8 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S isInaccessible? := .some false })).toArray } -def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := +def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): + Protocol.Goal := { userName?, target := { pp? := .some target}, @@ -658,9 +661,9 @@ def test_nat_zero_add: TestM Unit := do return () addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ - buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66", + buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"), buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat", - buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t" + buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t" ]) let tactic := "exact n" -- 2.44.1 From 398b1c39edd070d4c14981201d630cfc30a19632 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 19 Apr 2024 12:37:17 -0700 Subject: [PATCH 06/38] refactor: Common tactic execute function --- Pantograph/Goal.lean | 127 ++++++-------------------- Pantograph/Tactic.lean | 2 + Pantograph/Tactic/MotivatedApply.lean | 59 ++++++++++++ 3 files changed, 89 insertions(+), 99 deletions(-) create mode 100644 Pantograph/Tactic.lean create mode 100644 Pantograph/Tactic/MotivatedApply.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 5c6a583..0b7e306 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -4,6 +4,7 @@ Functions for handling metavariables All the functions starting with `try` resume their inner monadic state. -/ import Pantograph.Protocol +import Pantograph.Tactic import Lean def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := @@ -144,24 +145,6 @@ protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): O --- Tactic execution functions --- -/-- Inner function for executing tactic on goal state -/ -def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : - Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do - let tacticM (stx: Syntax): Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do - state.restore - Elab.Tactic.setGoals [goal] - try - Elab.Tactic.evalTactic stx - if (← getThe Core.State).messages.hasErrors then - let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Message.data).mapM fun md => md.toString - return .error errors - else - return .ok (← MonadBacktrack.saveState) - catch exception => - return .error #[← exception.toMessageData.toString] - tacticM tactic { elaborator := .anonymous } |>.run' state.tactic - /-- Response for executing a tactic -/ inductive TacticResult where -- Goes to next state @@ -175,14 +158,35 @@ inductive TacticResult where -- The given action cannot be executed in the state | invalidAction (message: String) -/-- Execute tactic on given state -/ -protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): - Elab.TermElabM TacticResult := do +protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit): + Elab.TermElabM TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with | .some goal => pure $ goal | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryTactic + goal.checkNotAssigned `GoalState.execute + try + let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } + if (← getThe Core.State).messages.hasErrors then + let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray + let errors ← (messages.map Message.data).mapM fun md => md.toString + return .failure errors + let nextElabState ← MonadBacktrack.saveState + let nextMCtx := nextElabState.meta.meta.mctx + let prevMCtx := state.mctx + return .success { + state with + savedState := { term := nextElabState, tactic := newGoals }, + newMVars := newMVarSet prevMCtx nextMCtx, + parentMVar? := .some goal, + calcPrevRhs? := .none, + } + catch exception => + return .failure #[← exception.toMessageData.toString] + +/-- Execute tactic on given state -/ +protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String): + Elab.TermElabM TacticResult := do let tactic ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := if state.isConv then `conv else `tactic) @@ -190,22 +194,7 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri (fileName := filename) with | .ok stx => pure $ stx | .error error => return .parseError error - match ← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic) with - | .error errors => - return .failure errors - | .ok nextSavedState => - -- Assert that the definition of metavariables are the same - let nextMCtx := nextSavedState.term.meta.meta.mctx - let prevMCtx := state.mctx - -- Generate a list of mvarIds that exist in the parent state; Also test the - -- assertion that the types have not changed on any mvars. - return .success { - state with - savedState := nextSavedState - newMVars := newMVarSet prevMCtx nextMCtx, - parentMVar? := .some goal, - calcPrevRhs? := .none, - } + state.execute goalId $ Elab.Tactic.evalTactic tactic /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): @@ -515,15 +504,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): catch exception => return .failure #[← exception.toMessageData.toString] -def getForallArgsBody: Expr → List Expr × Expr - | .forallE _ d b _ => - let (innerArgs, innerBody) := getForallArgsBody b - (d :: innerArgs, innerBody) - | e => ([], e) -def collectMotiveArguments (forallBody: Expr): SSet Nat := - match forallBody with - | .app (.bvar i) _ => SSet.empty.insert i - | _ => SSet.empty protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Elab.TermElabM TacticResult := do @@ -540,57 +520,6 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu (fileName := filename) with | .ok syn => pure syn | .error error => return .parseError error - try - -- Implemented similarly to the intro tactic - let nextGoals: List MVarId ← goal.withContext do - let recursor ← Elab.Term.elabTerm (stx := recursor) .none - let recursorType ← Meta.inferType recursor - - let (forallArgs, forallBody) := getForallArgsBody recursorType - let motiveIndices := collectMotiveArguments forallBody - --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}" - - let numArgs ← Meta.getExpectedNumArgs recursorType - - let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do - if i ≥ numArgs then - return prev - else - let argType := forallArgs.get! i - -- If `argType` has motive references, its goal needs to be placed in it - let argType := argType.instantiateRev prev - -- Create the goal - let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous - let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName) - IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}" - let prev := prev ++ [argGoal] - go (i + 1) prev - termination_by numArgs - i - let newMVars ← go 0 #[] - - -- FIXME: Add an `Eq` target and swap out the motive type - - --let sourceType := forallBody.instantiateRev newMVars - --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $ - -- Meta.isDefEq sourceType (← goal.getType) do - -- throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" - - -- Create the main goal for the return type of the recursor - goal.assign (mkAppN recursor newMVars) - - let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) - pure nextGoals - return .success { - root := state.root, - savedState := { - term := ← MonadBacktrack.saveState, - tactic := { goals := nextGoals } - }, - newMVars := nextGoals.toSSet, - parentMVar? := .some goal, - calcPrevRhs? := .none - } - catch exception => - return .failure #[← exception.toMessageData.toString] + state.execute goalId (tacticM := Tactic.motivatedApply recursor) end Pantograph diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean new file mode 100644 index 0000000..0148548 --- /dev/null +++ b/Pantograph/Tactic.lean @@ -0,0 +1,2 @@ + +import Pantograph.Tactic.MotivatedApply diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean new file mode 100644 index 0000000..50a660f --- /dev/null +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -0,0 +1,59 @@ +import Lean + +open Lean + +namespace Pantograph.Tactic + +def getForallArgsBody: Expr → List Expr × Expr + | .forallE _ d b _ => + let (innerArgs, innerBody) := getForallArgsBody b + (d :: innerArgs, innerBody) + | e => ([], e) +def collectMotiveArguments (forallBody: Expr): SSet Nat := + match forallBody with + | .app (.bvar i) _ => SSet.empty.insert i + | _ => SSet.empty + +def motivatedApply: Elab.Tactic.Tactic := λ stx => do + let goal ← Elab.Tactic.getMainGoal + let nextGoals: List MVarId ← goal.withContext do + let recursor ← Elab.Term.elabTerm (stx := stx) .none + let recursorType ← Meta.inferType recursor + + let (forallArgs, forallBody) := getForallArgsBody recursorType + let motiveIndices := collectMotiveArguments forallBody + --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}" + + let numArgs ← Meta.getExpectedNumArgs recursorType + + let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do + if i ≥ numArgs then + return prev + else + let argType := forallArgs.get! i + -- If `argType` has motive references, its goal needs to be placed in it + let argType := argType.instantiateRev prev + -- Create the goal + let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous + let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName) + IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}" + let prev := prev ++ [argGoal] + go (i + 1) prev + termination_by numArgs - i + let newMVars ← go 0 #[] + + -- FIXME: Add an `Eq` target and swap out the motive type + + --let sourceType := forallBody.instantiateRev newMVars + --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $ + -- Meta.isDefEq sourceType (← goal.getType) do + -- throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" + + -- Create the main goal for the return type of the recursor + goal.assign (mkAppN recursor newMVars) + + let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) + pure nextGoals + Elab.Tactic.setGoals nextGoals + +end Pantograph.Tactic -- 2.44.1 From 4a92e655f6515d1c6eaaaa991721f5cfb2774154 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 20 Apr 2024 13:09:41 -0700 Subject: [PATCH 07/38] test: Tactic test stub --- Pantograph/Tactic/MotivatedApply.lean | 1 + Test/Main.lean | 2 ++ Test/Tactic.lean | 1 + Test/Tactic/MotivatedApply.lean | 11 +++++++++++ 4 files changed, 15 insertions(+) create mode 100644 Test/Tactic.lean create mode 100644 Test/Tactic/MotivatedApply.lean diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 50a660f..817942d 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -14,6 +14,7 @@ def collectMotiveArguments (forallBody: Expr): SSet Nat := | .app (.bvar i) _ => SSet.empty.insert i | _ => SSet.empty +/-- Applies a symbol of the type `∀ (motive: α → Sort u) (a: α)..., (motive α)` -/ def motivatedApply: Elab.Tactic.Tactic := λ stx => do let goal ← Elab.Tactic.getMainGoal let nextGoals: List MVarId ← goal.withContext do diff --git a/Test/Main.lean b/Test/Main.lean index 1aa1d3d..ae897d4 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -5,6 +5,7 @@ import Test.Library import Test.Metavar import Test.Proofs import Test.Serial +import Test.Tactic -- Test running infrastructure @@ -48,6 +49,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Serial", Serial.suite env_default), + ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ] let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) [] LSpec.lspecIO (← runTestGroup name_filter tests) diff --git a/Test/Tactic.lean b/Test/Tactic.lean new file mode 100644 index 0000000..4284a41 --- /dev/null +++ b/Test/Tactic.lean @@ -0,0 +1 @@ +import Test.Tactic.MotivatedApply diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean new file mode 100644 index 0000000..04d7825 --- /dev/null +++ b/Test/Tactic/MotivatedApply.lean @@ -0,0 +1,11 @@ +import LSpec +import Lean + +open Lean + +namespace Pantograph.Test.Tactic.MotivatedApply + +def suite (env: Environment): List (String × IO LSpec.TestSeq) := + [] + +end Pantograph.Test.Tactic.MotivatedApply -- 2.44.1 From 3812aa56ecb871a9531d3cabec61a51eab7acbde Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Apr 2024 00:11:41 -0700 Subject: [PATCH 08/38] feat: Phantom var in mapply --- Makefile | 4 +- Pantograph/Goal.lean | 2 +- Pantograph/Tactic/MotivatedApply.lean | 88 +++++++++++++++++++++------ Test/Common.lean | 6 ++ Test/Proofs.lean | 9 ++- Test/Tactic/MotivatedApply.lean | 65 +++++++++++++++++++- 6 files changed, 147 insertions(+), 27 deletions(-) diff --git a/Makefile b/Makefile index 5d4ad6b..86f9e5b 100644 --- a/Makefile +++ b/Makefile @@ -1,9 +1,9 @@ LIB := ./.lake/build/lib/Pantograph.olean EXE := ./.lake/build/bin/pantograph -SOURCE := $(wildcard Pantograph/*.lean) $(wildcard *.lean) lean-toolchain +SOURCE := $(wildcard *.lean Pantograph/*.lean Pantograph/**/*.lean) lean-toolchain TEST_EXE := ./.lake/build/bin/test -TEST_SOURCE := $(wildcard Test/*.lean) +TEST_SOURCE := $(wildcard Test/*.lean Test/**/*.lean) $(LIB) $(EXE): $(SOURCE) lake build pantograph diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 0b7e306..17d94c0 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -126,7 +126,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do let expr ← goalState.mctx.eAssignment.find? goalState.root let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) - if expr.hasMVar then + if expr.hasExprMVar then -- Must not assert that the goal state is empty here. We could be in a branch goal. --assert! ¬goalState.goals.isEmpty .none diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 817942d..9826e3d 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -9,6 +9,54 @@ def getForallArgsBody: Expr → List Expr × Expr let (innerArgs, innerBody) := getForallArgsBody b (d :: innerArgs, innerBody) | e => ([], e) + +def replaceForallBody: Expr → Expr → Expr + | .forallE param domain body binderInfo, target => + let body := replaceForallBody body target + .forallE param domain body binderInfo + | _, target => target + +structure RecursorWithMotive where + args: List Expr + body: Expr + + -- .bvar index for the motive and major from the body + iMotive: Nat + iMajor: Nat + +namespace RecursorWithMotive + +protected def nArgs (info: RecursorWithMotive): Nat := info.args.length + +protected def getMotiveType (info: RecursorWithMotive): Expr := + let level := info.nArgs - info.iMotive - 1 + let a := info.args.get! level + a + +protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): MetaM Expr := do + let motiveType := info.getMotiveType + let resultantType ← Meta.inferType resultant + return replaceForallBody motiveType resultantType + +protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do + let goalMotive := mvars.get! (info.nArgs - info.iMotive - 1) + let goalMajor := mvars.get! (info.nArgs - info.iMajor - 1) + Meta.mkEq (.app goalMotive goalMajor) resultant + +end RecursorWithMotive + +def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do + let (args, body) := getForallArgsBody recursorType + let (iMotive, iMajor) ← match body with + | .app (.bvar iMotive) (.bvar iMajor) => pure (iMotive, iMajor) + | _ => .none + return { + args, + body, + iMotive, + iMajor, + } + def collectMotiveArguments (forallBody: Expr): SSet Nat := match forallBody with | .app (.bvar i) _ => SSet.empty.insert i @@ -21,38 +69,38 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do let recursor ← Elab.Term.elabTerm (stx := stx) .none let recursorType ← Meta.inferType recursor - let (forallArgs, forallBody) := getForallArgsBody recursorType - let motiveIndices := collectMotiveArguments forallBody - --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}" + let resultant ← goal.getType - let numArgs ← Meta.getExpectedNumArgs recursorType + let info ← match getRecursorInformation recursorType with + | .some info => pure info + | .none => throwError "Recursor return type does not correspond with the invocation of a motive: {← Meta.ppExpr recursorType}" let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do - if i ≥ numArgs then + if i ≥ info.nArgs then return prev else - let argType := forallArgs.get! i + let argType := info.args.get! i -- If `argType` has motive references, its goal needs to be placed in it let argType := argType.instantiateRev prev - -- Create the goal - let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous - let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName) - IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}" + let bvarIndex := info.nArgs - i - 1 + let argGoal ← if bvarIndex = info.iMotive then + let surrogateMotiveType ← info.surrogateMotiveType resultant + Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) + else if bvarIndex = info.iMajor then + Meta.mkFreshExprMVar argType .syntheticOpaque (userName := `major) + else + Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) let prev := prev ++ [argGoal] go (i + 1) prev - termination_by numArgs - i - let newMVars ← go 0 #[] + termination_by info.nArgs - i + let mut newMVars ← go 0 #[] - -- FIXME: Add an `Eq` target and swap out the motive type - - --let sourceType := forallBody.instantiateRev newMVars - --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $ - -- Meta.isDefEq sourceType (← goal.getType) do - -- throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" - - -- Create the main goal for the return type of the recursor goal.assign (mkAppN recursor newMVars) + let phantomType ← info.phantomType newMVars resultant + let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom) + newMVars := newMVars ++ [goalPhantom] + let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) pure nextGoals Elab.Tactic.setGoals nextGoals diff --git a/Test/Common.lean b/Test/Common.lean index 8b8e977..6ea4fb2 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -63,6 +63,12 @@ def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSe def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := termElabM.run' (ctx := Pantograph.defaultTermElabMContext) +def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e + +def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do + let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } + return newGoals.goals + end Test end Pantograph diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 1adc9d4..43c346b 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -661,9 +661,10 @@ def test_nat_zero_add: TestM Unit := do return () addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ - buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"), - buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat", - buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t" + buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), + buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat" (.some "major"), + buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", + buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?major = (n + 0 = n)" (.some "phantom") ]) let tactic := "exact n" @@ -710,6 +711,8 @@ def test_nat_zero_add: TestM Unit := do addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)) = #[]) + let expr := stateF.mctx.eAssignment.find! stateF.root + let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr) addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome def suite (env: Environment): List (String × IO LSpec.TestSeq) := diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 04d7825..60ed7be 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -1,11 +1,74 @@ import LSpec import Lean +import Test.Common open Lean +open Pantograph namespace Pantograph.Test.Tactic.MotivatedApply +def valueAndType (recursor: String): MetaM (Expr × Expr) := do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := recursor) + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + runTermElabMInMeta do + let recursor ← Elab.Term.elabTerm (stx := recursor) .none + let recursorType ← Meta.inferType recursor + return (recursor, recursorType) + + +def test_type_extract (env: Environment): IO LSpec.TestSeq := + runMetaMSeq env do + let mut tests := LSpec.TestSeq.done + let (recursor, recursorType) ← valueAndType "@Nat.brecOn" + tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = + (← exprToStr recursorType)) + let info ← match Tactic.getRecursorInformation recursorType with + | .some info => pure info + | .none => throwError "Failed to extract recursor info" + tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2) + tests := tests ++ LSpec.check "iMajor" (info.iMajor = 1) + let motiveType := info.getMotiveType + tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" = + (← exprToStr motiveType)) + return tests + +def test_execute (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n t: Nat) => n + 0 = n" + runMetaMSeq env do + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@Nat.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar tactic target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Nat → Prop", + "Nat", + "∀ (t : Nat), Nat.below t → ?motive t", + "?motive ?major = (n + 0 = n)", + ]) + tests := tests ++ test + return tests + def suite (env: Environment): List (String × IO LSpec.TestSeq) := - [] + [ + ("type_extract", test_type_extract env), + ("execute", test_execute env), + ] end Pantograph.Test.Tactic.MotivatedApply -- 2.44.1 From feff62a3c53de6ba111cb6aa48371a2ae0effb7e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Apr 2024 09:52:13 -0700 Subject: [PATCH 09/38] fix: Remove determination of major --- Pantograph/Tactic/MotivatedApply.lean | 15 ++++++--------- Test/Proofs.lean | 4 ++-- Test/Tactic/MotivatedApply.lean | 3 +-- 3 files changed, 9 insertions(+), 13 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 9826e3d..1201174 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -22,7 +22,6 @@ structure RecursorWithMotive where -- .bvar index for the motive and major from the body iMotive: Nat - iMajor: Nat namespace RecursorWithMotive @@ -39,22 +38,22 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): return replaceForallBody motiveType resultantType protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do - let goalMotive := mvars.get! (info.nArgs - info.iMotive - 1) - let goalMajor := mvars.get! (info.nArgs - info.iMajor - 1) - Meta.mkEq (.app goalMotive goalMajor) resultant + let motiveCall := Expr.instantiateRev info.body mvars + Meta.mkEq motiveCall resultant end RecursorWithMotive def getRecursorInformation (recursorType: Expr): Option RecursorWithMotive := do let (args, body) := getForallArgsBody recursorType - let (iMotive, iMajor) ← match body with - | .app (.bvar iMotive) (.bvar iMajor) => pure (iMotive, iMajor) + if ¬ body.isApp then + .none + let iMotive ← match body.getAppFn with + | .bvar iMotive => pure iMotive | _ => .none return { args, body, iMotive, - iMajor, } def collectMotiveArguments (forallBody: Expr): SSet Nat := @@ -86,8 +85,6 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do let argGoal ← if bvarIndex = info.iMotive then let surrogateMotiveType ← info.surrogateMotiveType resultant Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) - else if bvarIndex = info.iMajor then - Meta.mkFreshExprMVar argType .syntheticOpaque (userName := `major) else Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) let prev := prev ++ [argGoal] diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 43c346b..2df0868 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -662,9 +662,9 @@ def test_nat_zero_add: TestM Unit := do addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), - buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat" (.some "major"), + buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", - buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?major = (n + 0 = n)" (.some "phantom") + buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "phantom") ]) let tactic := "exact n" diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 60ed7be..1f751ed 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -31,7 +31,6 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq := | .some info => pure info | .none => throwError "Failed to extract recursor info" tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2) - tests := tests ++ LSpec.check "iMajor" (info.iMajor = 1) let motiveType := info.getMotiveType tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" = (← exprToStr motiveType)) @@ -60,7 +59,7 @@ def test_execute (env: Environment): IO LSpec.TestSeq := "Nat → Prop", "Nat", "∀ (t : Nat), Nat.below t → ?motive t", - "?motive ?major = (n + 0 = n)", + "?motive ?m.69 = (n + 0 = n)", ]) tests := tests ++ test return tests -- 2.44.1 From 6ffb227cd641f77109c539152e0b38f6d2bfa125 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 22 Apr 2024 10:02:09 -0700 Subject: [PATCH 10/38] feat: Conduit modus ponens --- Pantograph/Tactic/MotivatedApply.lean | 12 ++++++------ Test/Proofs.lean | 15 +++++++++++++-- 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 1201174..821b681 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -37,7 +37,7 @@ protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): let resultantType ← Meta.inferType resultant return replaceForallBody motiveType resultantType -protected def phantomType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do +protected def conduitType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do let motiveCall := Expr.instantiateRev info.body mvars Meta.mkEq motiveCall resultant @@ -92,11 +92,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do termination_by info.nArgs - i let mut newMVars ← go 0 #[] - goal.assign (mkAppN recursor newMVars) - - let phantomType ← info.phantomType newMVars resultant - let goalPhantom ← Meta.mkFreshExprMVar phantomType .syntheticOpaque (userName := `phantom) - newMVars := newMVars ++ [goalPhantom] + -- Create the conduit type which proves the result of the motive is equal to the goal + let conduitType ← info.conduitType newMVars resultant + let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit) + goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) + newMVars := newMVars ++ [goalConduit] let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) pure nextGoals diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 2df0868..429d4d2 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -664,7 +664,7 @@ def test_nat_zero_add: TestM Unit := do buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", - buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "phantom") + buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit") ]) let tactic := "exact n" @@ -703,7 +703,18 @@ def test_nat_zero_add: TestM Unit := do #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) let tactic := "simp" - let stateF ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with + let state3d ← match ← state3.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state2d ← match state3d.continue state2c with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + let tactic := "rfl" + let stateF ← match ← state2d.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString -- 2.44.1 From 4cff6677d27a9629eb44d173c321977ac860e5e8 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 4 May 2024 23:36:42 -0700 Subject: [PATCH 11/38] chore: Lean version bump to 4.8.0-rc1 --- Pantograph.lean | 2 +- Pantograph/Goal.lean | 4 ++-- Pantograph/Protocol.lean | 1 - Test/Integration.lean | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- lean-toolchain | 2 +- 7 files changed, 10 insertions(+), 11 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index f59bc11..74289d6 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -87,7 +87,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do } } return .ok { } - options_print (_: Protocol.OptionsPrint): MainM (CR Protocol.OptionsPrintResult) := do + 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 diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 17d94c0..921f60b 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -169,7 +169,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab. let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Message.data).mapM fun md => md.toString + let errors ← (messages.map (·.data)).mapM fun md => md.toString return .failure errors let nextElabState ← MonadBacktrack.saveState let nextMCtx := nextElabState.meta.meta.mctx @@ -214,7 +214,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr): goal.assign expr if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray - let errors ← (messages.map Message.data).mapM fun md => md.toString + let errors ← (messages.map (·.data)).mapM fun md => md.toString return .failure errors let prevMCtx := state.savedState.term.meta.meta.mctx let nextMCtx ← getMCtx diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 17618fc..f73c3b0 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -193,7 +193,6 @@ structure OptionsSetResult where deriving Lean.ToJson structure OptionsPrint where deriving Lean.FromJson -abbrev OptionsPrintResult := Options structure GoalStart where -- Only one of the fields below may be populated. diff --git a/Test/Integration.lean b/Test/Integration.lean index 29cb82d..9bd5db6 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -65,7 +65,7 @@ def test_option_modify : IO LSpec.TestSeq := subroutine_step "options.print" [] (Lean.toJson ({ options with printExprAST := true }: - Protocol.OptionsPrintResult)) + Protocol.Options)) ] def test_malformed_command : IO LSpec.TestSeq := let invalid := "invalid" diff --git a/flake.lock b/flake.lock index 39888a8..1a50363 100644 --- a/flake.lock +++ b/flake.lock @@ -42,16 +42,16 @@ "nixpkgs-old": "nixpkgs-old" }, "locked": { - "lastModified": 1711508550, - "narHash": "sha256-UK4DnYmwXLcqHA316Zkn0cnujdYlxqUf+b6S4l56Q3s=", + "lastModified": 1714704934, + "narHash": "sha256-q0kLyIahUXolkSrBZSegPF+R99WAH1YC96JfKoFntDE=", "owner": "leanprover", "repo": "lean4", - "rev": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", + "rev": "dcccfb73cb247e9478220375ab7de03f7c67e505", "type": "github" }, "original": { "owner": "leanprover", - "ref": "b4caee80a3dfc5c9619d88b16c40cc3db90da4e2", + "ref": "v4.8.0-rc1", "repo": "lean4", "type": "github" } diff --git a/flake.nix b/flake.nix index 2458805..ad40a3f 100644 --- a/flake.nix +++ b/flake.nix @@ -5,8 +5,8 @@ nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable"; flake-parts.url = "github:hercules-ci/flake-parts"; lean = { - url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; # Do not follow input's nixpkgs since it could cause build failures + url = "github:leanprover/lean4?ref=v4.8.0-rc1"; }; lspec = { url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; diff --git a/lean-toolchain b/lean-toolchain index c630636..d8a6d7e 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-03-27 +leanprover/lean4:v4.8.0-rc1 -- 2.44.1 From 63417ef179066bfd847ff5efc5e74085268b1795 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 00:43:32 -0700 Subject: [PATCH 12/38] fix: Motive extra arguments not instiantiated --- Pantograph/Tactic/MotivatedApply.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index 821b681..a7b9a07 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -32,8 +32,8 @@ protected def getMotiveType (info: RecursorWithMotive): Expr := let a := info.args.get! level a -protected def surrogateMotiveType (info: RecursorWithMotive) (resultant: Expr): MetaM Expr := do - let motiveType := info.getMotiveType +protected def surrogateMotiveType (info: RecursorWithMotive) (mvars: Array Expr) (resultant: Expr): MetaM Expr := do + let motiveType := Expr.instantiateRev info.getMotiveType mvars let resultantType ← Meta.inferType resultant return replaceForallBody motiveType resultantType @@ -83,7 +83,7 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do let argType := argType.instantiateRev prev let bvarIndex := info.nArgs - i - 1 let argGoal ← if bvarIndex = info.iMotive then - let surrogateMotiveType ← info.surrogateMotiveType resultant + let surrogateMotiveType ← info.surrogateMotiveType prev resultant Meta.mkFreshExprMVar surrogateMotiveType .syntheticOpaque (userName := `motive) else Meta.mkFreshExprMVar argType .syntheticOpaque (userName := .anonymous) -- 2.44.1 From 1e1995255a91a738f3e1ce0dc2a8f8842acc4152 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 10:36:43 -0700 Subject: [PATCH 13/38] test: mapply captures dependent types --- Test/Tactic/MotivatedApply.lean | 35 +++++++++++++++++++++++++++++++-- 1 file changed, 33 insertions(+), 2 deletions(-) diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 1f751ed..84ca804 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -36,7 +36,7 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq := (← exprToStr motiveType)) return tests -def test_execute (env: Environment): IO LSpec.TestSeq := +def test_nat_brec_on (env: Environment): IO LSpec.TestSeq := let expr := "λ (n t: Nat) => n + 0 = n" runMetaMSeq env do let (expr, exprType) ← valueAndType expr @@ -64,10 +64,41 @@ def test_execute (env: Environment): IO LSpec.TestSeq := tests := tests ++ test return tests +def test_list_brec_on (env: Environment): IO LSpec.TestSeq := + let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l" + runMetaMSeq env do + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@List.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar tactic target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Type ?u.92", + "List ?m.94 → Prop", + "List ?m.94", + "∀ (t : List ?m.94), List.below t → ?motive t", + "?motive ?m.96 = (l ++ [] = [] ++ l)", + ]) + tests := tests ++ test + return tests + + def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("type_extract", test_type_extract env), - ("execute", test_execute env), + ("nat_brec_on", test_nat_brec_on env), + ("list_brec_on", test_list_brec_on env), ] end Pantograph.Test.Tactic.MotivatedApply -- 2.44.1 From cf1289f159ddddf85430fbdd04d47d4f3be6eeae Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 13:24:29 -0700 Subject: [PATCH 14/38] feat: NoConfuse tactic --- Pantograph/Goal.lean | 16 +++++ Pantograph/Tactic.lean | 1 + Pantograph/Tactic/NoConfuse.lean | 18 ++++++ Test/Main.lean | 1 + Test/Tactic.lean | 1 + Test/Tactic/NoConfuse.lean | 100 +++++++++++++++++++++++++++++++ 6 files changed, 137 insertions(+) create mode 100644 Pantograph/Tactic/NoConfuse.lean create mode 100644 Test/Tactic/NoConfuse.lean diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 921f60b..7ada190 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -521,5 +521,21 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.motivatedApply recursor) +protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: String): + Elab.TermElabM TacticResult := do + state.restoreElabM + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + goal.checkNotAssigned `GoalState.tryMotivatedApply + + let recursor ← match Parser.runParserCategory + (env := state.env) + (catName := `term) + (input := eq) + (fileName := filename) with + | .ok syn => pure syn + | .error error => return .parseError error + state.execute goalId (tacticM := Tactic.noConfuse recursor) end Pantograph diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index 0148548..5a7828c 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Tactic.lean @@ -1,2 +1,3 @@ import Pantograph.Tactic.MotivatedApply +import Pantograph.Tactic.NoConfuse diff --git a/Pantograph/Tactic/NoConfuse.lean b/Pantograph/Tactic/NoConfuse.lean new file mode 100644 index 0000000..b8bc84e --- /dev/null +++ b/Pantograph/Tactic/NoConfuse.lean @@ -0,0 +1,18 @@ +import Lean + +open Lean + +namespace Pantograph.Tactic + +def noConfuse: Elab.Tactic.Tactic := λ stx => do + let goal ← Elab.Tactic.getMainGoal + goal.withContext do + let absurd ← Elab.Term.elabTerm (stx := stx) .none + let noConfusion ← Meta.mkNoConfusion (target := ← goal.getType) (h := absurd) + + unless ← Meta.isDefEq (← Meta.inferType noConfusion) (← goal.getType) do + throwError "invalid noConfuse call: The resultant type {← Meta.ppExpr $ ← Meta.inferType noConfusion} cannot be unified with {← Meta.ppExpr $ ← goal.getType}" + goal.assign noConfusion + Elab.Tactic.setGoals [] + +end Pantograph.Tactic diff --git a/Test/Main.lean b/Test/Main.lean index ae897d4..4a1ca69 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -50,6 +50,7 @@ def main (args: List String) := do ("Proofs", Proofs.suite env_default), ("Serial", Serial.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), + ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), ] let tests: List (String × IO LSpec.TestSeq) := suites.foldl (λ acc (name, suite) => acc ++ (addPrefix name suite)) [] LSpec.lspecIO (← runTestGroup name_filter tests) diff --git a/Test/Tactic.lean b/Test/Tactic.lean index 4284a41..f1e2649 100644 --- a/Test/Tactic.lean +++ b/Test/Tactic.lean @@ -1 +1,2 @@ import Test.Tactic.MotivatedApply +import Test.Tactic.NoConfuse diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean new file mode 100644 index 0000000..54c2be7 --- /dev/null +++ b/Test/Tactic/NoConfuse.lean @@ -0,0 +1,100 @@ +import LSpec +import Lean +import Test.Common + +open Lean +open Pantograph + +namespace Pantograph.Test.Tactic.NoConfuse + +def valueAndType (recursor: String): MetaM (Expr × Expr) := do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := recursor) + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + runTermElabMInMeta do + let recursor ← Elab.Term.elabTerm (stx := recursor) .none + let recursorType ← Meta.inferType recursor + return (recursor, recursorType) + +def test_nat (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n: Nat) (h: 0 = n + 1) => False" + runMetaMSeq env do + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.noConfuse recursor + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar tactic target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + []) + tests := tests ++ test + return tests + +def test_nat_fail (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n: Nat) (h: n = n) => False" + runMetaMSeq env do + let (expr, _) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + try + let tactic := Tactic.noConfuse recursor + let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId! + tests := tests ++ assertUnreachable "Tactic should fail" + catch _ => + tests := tests ++ LSpec.check "Tactic should fail" true + return tests + return tests + +def test_list (env: Environment): IO LSpec.TestSeq := + let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False" + runMetaMSeq env do + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "h") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.noConfuse recursor + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar tactic target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + []) + tests := tests ++ test + return tests + +def suite (env: Environment): List (String × IO LSpec.TestSeq) := + [ + ("nat", test_nat env), + ("nat_fail", test_nat_fail env), + ("list", test_list env), + ] + +end Pantograph.Test.Tactic.NoConfuse -- 2.44.1 From 2937675044bcefe266a9c1d1116dbec53ee3942a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 13:25:48 -0700 Subject: [PATCH 15/38] feat: Library interface for calling no_confuse --- Pantograph/Goal.lean | 2 +- Pantograph/Library.lean | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 7ada190..11e5b20 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -521,7 +521,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu | .ok syn => pure syn | .error error => return .parseError error state.execute goalId (tacticM := Tactic.motivatedApply recursor) -protected def GoalState.tryNoConfusion (state: GoalState) (goalId: Nat) (eq: String): +protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM let goal ← match state.savedState.tactic.goals.get? goalId with diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 00b4bc7..608aeeb 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -208,5 +208,8 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := @[export pantograph_goal_motivated_apply_m] def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := runTermElabM <| state.tryMotivatedApply goalId recursor +@[export pantograph_goal_no_confuse_m] +def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryNoConfuse goalId recursor end Pantograph -- 2.44.1 From 679871cbc659ce9ff58e832d20f51f52ae3dc2f1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 5 May 2024 13:26:46 -0700 Subject: [PATCH 16/38] fix: NoConfuse arg name --- Pantograph/Library.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 608aeeb..6dda2f0 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -209,7 +209,7 @@ def goalFocus (state: GoalState) (goalId: Nat): Option GoalState := def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := runTermElabM <| state.tryMotivatedApply goalId recursor @[export pantograph_goal_no_confuse_m] -def goalNoConfuse (state: GoalState) (goalId: Nat) (recursor: String): Lean.CoreM TacticResult := - runTermElabM <| state.tryNoConfuse goalId recursor +def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := + runTermElabM <| state.tryNoConfuse goalId eq end Pantograph -- 2.44.1 From aa106f7591b8719ce91baa25e7434b808b62e0d6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 May 2024 22:20:20 -0700 Subject: [PATCH 17/38] feat: Do not filter mvars from mapply --- Pantograph/Tactic/MotivatedApply.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Tactic/MotivatedApply.lean b/Pantograph/Tactic/MotivatedApply.lean index a7b9a07..f570560 100644 --- a/Pantograph/Tactic/MotivatedApply.lean +++ b/Pantograph/Tactic/MotivatedApply.lean @@ -94,11 +94,11 @@ def motivatedApply: Elab.Tactic.Tactic := λ stx => do -- Create the conduit type which proves the result of the motive is equal to the goal let conduitType ← info.conduitType newMVars resultant - let goalConduit ← Meta.mkFreshExprMVar conduitType .syntheticOpaque (userName := `conduit) + let goalConduit ← Meta.mkFreshExprMVar conduitType .natural (userName := `conduit) goal.assign $ ← Meta.mkEqMP goalConduit (mkAppN recursor newMVars) newMVars := newMVars ++ [goalConduit] - let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned) + let nextGoals := newMVars.toList.map (·.mvarId!) pure nextGoals Elab.Tactic.setGoals nextGoals -- 2.44.1 From 69ec70ffbe7caec196c549bf30018c6433e4104b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 6 May 2024 22:39:17 -0700 Subject: [PATCH 18/38] feat: Do not explicitly show delay assigned mvar --- Pantograph/Serial.lean | 9 ++++++--- Test/Proofs.lean | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 950818e..26b0c9f 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -102,9 +102,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM | .fvar fvarId => let name := ofName fvarId.name pure s!"(:fv {name})" - | .mvar mvarId => - let name := ofName mvarId.name - pure s!"(:mv {name})" + | .mvar mvarId => do + if ← mvarId.isDelayedAssigned then + pure s!"(:mv)" + else + let name := ofName mvarId.name + pure s!"(:mv {name})" | .sort level => let level := serializeSortLevel level sanitize pure s!"(:sort {level})" diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 429d4d2..8e77227 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) -- This is due to delayed assignment addTest $ LSpec.test "(2 parent)" (state2parent == - "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state -- 2.44.1 From 66a5dfcf3c615a3f5d970acd624364d3dc5551d5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 8 May 2024 12:41:21 -0700 Subject: [PATCH 19/38] feat: Diagnostics command for FFI users --- Pantograph/Library.lean | 4 +++ Pantograph/Serial.lean | 63 ++++++++++++++++++++++------------------- 2 files changed, 38 insertions(+), 29 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6dda2f0..fa5d414 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -212,4 +212,8 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := runTermElabM <| state.tryNoConfuse goalId eq +@[export pantograph_goal_diag] +def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := + runMetaM $ state.diag diagOptions + end Pantograph diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 26b0c9f..b2a4529 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -270,51 +270,56 @@ protected def GoalState.serializeGoals | .none => throwError s!"Metavariable does not exist in context {goal.name}" /-- Print the metavariables in a readable format -/ -protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do +protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM String := do goalState.restoreMetaM let savedState := goalState.savedState let goals := savedState.tactic.goals let mctx ← getMCtx let root := goalState.root -- Print the root - match mctx.decls.find? root with - | .some decl => printMVar ">" root decl - | .none => IO.println s!">{root.name}: ??" - goals.forM (fun mvarId => do - if mvarId != root then - match mctx.decls.find? mvarId with - | .some decl => printMVar "⊢" mvarId decl - | .none => IO.println s!"⊢{mvarId.name}: ??" + let result: String ← match mctx.decls.find? root with + | .some decl => printMVar ">" root decl + | .none => pure s!">{root.name}: ??" + let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId => + match mctx.decls.find? mvarId with + | .some decl => printMVar "⊢" mvarId decl + | .none => pure s!"⊢{mvarId.name}: ??" ) let goals := goals.toSSet - mctx.decls.forM (fun mvarId decl => do - if goals.contains mvarId || mvarId == root then - pure () - -- Print the remainig ones that users don't see in Lean - else if options.printAll then + let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) => + !(goals.contains mvarId || mvarId == root) && options.printAll) + |>.mapM (fun (mvarId, decl) => do let pref := if goalState.newMVars.contains mvarId then "~" else " " printMVar pref mvarId decl - else - pure () - --IO.println s!" {mvarId.name}{userNameToString decl.userName}" ) + pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join) where - printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do - if options.printContext then - decl.lctx.fvarIdToDecl.forM printFVar + printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := do + let resultFVars: List String ← + if options.printContext then + decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) => + do pure $ (← printFVar fvarId decl) ++ "\n") + else + pure [] let type ← if options.instantiate then instantiateMVars decl.type else pure $ decl.type let type_sexp ← serializeExpressionSexp type (sanitize := false) - IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" - if options.printValue then - if let Option.some value := (← getMCtx).eAssignment.find? mvarId then - let value ← if options.instantiate - then instantiateMVars value - else pure $ value - IO.println s!" := {← Meta.ppExpr value}" - printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do - IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}" + let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" + let resultValue: String ← + if options.printValue then + if let Option.some value := (← getMCtx).eAssignment.find? mvarId then + let value ← if options.instantiate + then instantiateMVars value + else pure $ value + pure s!"\n := {← Meta.ppExpr value}" + else + pure "" + else + pure "" + pure $ (String.join resultFVars) ++ resultMain ++ resultValue + printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM String := do + pure s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}" userNameToString : Name → String | .anonymous => "" | other => s!"[{other}]" -- 2.44.1 From e58dbc66a92ef10b014a30745a542ec0dd9be6ef Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 8 May 2024 20:51:36 -0700 Subject: [PATCH 20/38] fix: Consistent naming in library functions --- Pantograph/Library.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index fa5d414..3ae852f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -180,6 +180,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto parent? := ← state.parentExpr?.mapM (λ expr => do serializeExpression options (← unfoldAuxLemmas expr)), } +@[export pantograph_goal_diag_m] +def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := + runMetaM $ state.diag diagOptions @[export pantograph_goal_tactic_m] def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := @@ -212,8 +215,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := runTermElabM <| state.tryNoConfuse goalId eq -@[export pantograph_goal_diag] -def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := - runMetaM $ state.diag diagOptions - end Pantograph -- 2.44.1 From 0b88f6708e299f0282f048364a885f7913525bc7 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 9 May 2024 14:02:43 -0700 Subject: [PATCH 21/38] test: Delayed mvar assignment for mapply --- Test/Proofs.lean | 52 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e77227..04fe79c 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -726,6 +726,57 @@ def test_nat_zero_add: TestM Unit := do let (expr, _) := instantiateMVarsCore (mctx := stateF.mctx) (e := expr) addTest $ LSpec.check "(F root)" stateF.rootExpr?.isSome +def test_nat_zero_add_alt: TestM Unit := do + let state? ← startProof (.expr "∀ (n: Nat), n + 0 = n") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + let tactic := "intro n" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat")] "n + 0 = n"]) + let recursor := "@Nat.brecOn" + let state2 ← match ← state1.tryMotivatedApply (goalId := 0) (recursor := recursor) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = + #[ + buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), + buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", + buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", + buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit") + ]) + + let tactic := "intro x" + let state3m ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3m.serializeGoals (options := ← read)).map (·.devolatilize) = + #[buildGoal [("n", "Nat"), ("x", "Nat")] "Prop" (.some "motive")]) + let tactic := "apply Eq" + let state3m2 ← match ← state3m.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with + | .ok state => pure state + | .error e => do + addTest $ assertUnreachable e + return () + addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) = + #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) + def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ ("Nat.add_comm", test_nat_add_comm false), @@ -739,6 +790,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("let via assign", test_let false), ("let via tryLet", test_let true), ("Nat.zero_add", test_nat_zero_add), + ("Nat.zero_add alt", test_nat_zero_add_alt), ] tests.map (fun (name, test) => (name, proofRunner env test)) -- 2.44.1 From 03ecb6cf19b7741a6bb20f2eb969374ac59b8643 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 11 May 2024 20:01:02 -0700 Subject: [PATCH 22/38] feat: Partial instantiate metavariables --- Pantograph/Library.lean | 4 ++-- Pantograph/Serial.lean | 32 ++++++++++++++++++------- Test/Integration.lean | 4 ++-- Test/Proofs.lean | 2 +- Test/Serial.lean | 1 + Test/Tactic/MotivatedApply.lean | 42 +++++++++++++++++++++++++++++++-- 6 files changed, 70 insertions(+), 15 deletions(-) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 3ae852f..59d7adc 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -176,9 +176,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto state.restoreMetaM return { root? := ← state.rootExpr?.mapM (λ expr => do - serializeExpression options (← unfoldAuxLemmas expr)), + serializeExpression options (← instantiateAll expr)), parent? := ← state.parentExpr?.mapM (λ expr => do - serializeExpression options (← unfoldAuxLemmas expr)), + serializeExpression options (← instantiateAll expr)), } @[export pantograph_goal_diag_m] def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index b2a4529..cdb35ce 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -18,6 +18,23 @@ namespace Pantograph def unfoldAuxLemmas (e : Expr) : CoreM Expr := do Lean.Meta.deltaExpand e Lean.Name.isAuxLemma +def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do + Meta.transform e + (pre := fun e => e.withApp fun f args => do + if let .mvar mvarId := f then + if let some decl ← getDelayedMVarAssignment? mvarId then + if args.size ≥ decl.fvars.size then + let pending ← instantiateMVars (.mvar decl.mvarIdPending) + if !pending.isMVar then + return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args + return .continue) + +def instantiateAll (e: Expr): MetaM Expr := do + let e ← instantiateMVars e + let e ← unfoldAuxLemmas e + let e ← instantiatePartialDelayedMVars e + return e + --- Input Functions --- /-- Read syntax object from string -/ @@ -103,11 +120,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM let name := ofName fvarId.name pure s!"(:fv {name})" | .mvar mvarId => do - if ← mvarId.isDelayedAssigned then - pure s!"(:mv)" - else + let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv" let name := ofName mvarId.name - pure s!"(:mv {name})" + pure s!"(:{pref} {name})" | .sort level => let level := serializeSortLevel level sanitize pure s!"(:sort {level})" @@ -210,7 +225,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava match localDecl with | .cdecl _ fvarId userName type _ _ => let userName := userName.simpMacroScopes - let type ← instantiateMVars type + let type ← instantiate type return { name := ofName fvarId.name, userName:= ofName userName, @@ -219,9 +234,9 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava } | .ldecl _ fvarId userName type val _ _ => do let userName := userName.simpMacroScopes - let type ← instantiateMVars type + let type ← instantiate type let value? ← if showLetValues then - let val ← instantiateMVars val + let val ← instantiate val pure $ .some (← serializeExpression options val) else pure $ .none @@ -248,10 +263,11 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava name := ofName goal.name, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, - target := (← serializeExpression options (← instantiateMVars mvarDecl.type)), + target := (← serializeExpression options (← instantiateAll mvarDecl.type)), vars := vars.reverse.toArray } where + instantiate := instantiateAll ofName (n: Name) := serializeName n (sanitize := false) protected def GoalState.serializeGoals diff --git a/Test/Integration.lean b/Test/Integration.lean index 9bd5db6..66b3637 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq := vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], } let goal2: Protocol.Goal := { - name := "_uniq.14", + name := "_uniq.17", target := { pp? := .some "x ∨ y → y ∨ x" }, vars := #[ { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, - { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} ], } subroutine_runner [ diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 04fe79c..496bcc8 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) -- This is due to delayed assignment addTest $ LSpec.test "(2 parent)" (state2parent == - "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + "((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state diff --git a/Test/Serial.lean b/Test/Serial.lean index f55c18f..093dd8b 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -52,6 +52,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), -- This tests `autoBoundImplicit` ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), + ("(2: Nat) <= (5: Nat)", "((:c LE.le) (:mv _uniq.37) (:mv _uniq.38) ((:c OfNat.ofNat) (:mv _uniq.23) (:lit 2) (:mv _uniq.24)) ((:c OfNat.ofNat) (:mv _uniq.33) (:lit 5) (:mv _uniq.34)))"), ] let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do let env ← MonadEnv.getEnv diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index 84ca804..ad8ebdc 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -93,12 +93,50 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq := tests := tests ++ test return tests +def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do + let expr := "λ (n t: Nat) => n + 0 = n" + runMetaMSeq env $ runTermElabMInMeta do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := "@Nat.brecOn") + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + let (expr, exprType) ← valueAndType expr + Meta.lambdaTelescope expr $ λ _ body => do + let mut tests := LSpec.TestSeq.done + -- Apply the tactic + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let tactic := Tactic.motivatedApply recursor + let newGoals ← runTacticOnMVar tactic target.mvarId! + tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = + [ + "Nat → Prop", + "Nat", + "∀ (t : Nat), Nat.below t → ?motive t", + "?motive ?m.69 = (n + 0 = n)", + ])) + let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" + tests := tests ++ (LSpec.check "goal name" (major.name.toString = "_uniq.69")) + + -- Assign motive to `λ x => x + _` + let (motive_assign, _) ← valueAndType "λ (x: Nat) => @Nat.add x + 0 = _" + motive.assign motive_assign + + let test ← conduit.withContext do + let t := toString (← Meta.ppExpr $ ← conduit.getType) + return LSpec.check "conduit" (t = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)") + tests := tests ++ test + + return tests def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("type_extract", test_type_extract env), - ("nat_brec_on", test_nat_brec_on env), - ("list_brec_on", test_list_brec_on env), + ("Nat.brecOn", test_nat_brec_on env), + ("List.brecOn", test_list_brec_on env), + ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env), ] end Pantograph.Test.Tactic.MotivatedApply -- 2.44.1 From c04b363de70611f68e45c938a03dfff0be4efc34 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 12 May 2024 22:33:38 -0700 Subject: [PATCH 23/38] feat: Handle delay assigned mvars --- Pantograph/Goal.lean | 3 ++- Pantograph/Serial.lean | 35 +++++++++++++++++++++++++++++++++-- Test/Integration.lean | 4 ++-- Test/Metavar.lean | 2 +- Test/Proofs.lean | 32 +++++++++++++++++++++++++++----- 5 files changed, 65 insertions(+), 11 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 11e5b20..e1d36b3 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -98,7 +98,8 @@ Brings into scope a list of goals -/ protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := if ¬ (goals.all (λ goal => state.mvars.contains goal)) then - .error s!"Goals not in scope" + let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString) + .error s!"Goals {invalid_goals} are not in scope" else -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic. let unassigned := goals.filter (λ goal => diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index cdb35ce..14a4002 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -32,7 +32,7 @@ def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do def instantiateAll (e: Expr): MetaM Expr := do let e ← instantiateMVars e let e ← unfoldAuxLemmas e - let e ← instantiatePartialDelayedMVars e + --let e ← instantiatePartialDelayedMVars e return e --- Input Functions --- @@ -101,6 +101,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String := | _, .zero => s!"{k}" | _, _ => s!"(+ {u_str} {k})" + /-- Completely serializes an expression tree. Json not used due to compactness @@ -109,7 +110,37 @@ A `_` symbol in the AST indicates automatic deductions not present in the origin partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do self expr where - self (e: Expr): MetaM String := + delayedMVarToSexp (e: Expr): MetaM (Option String) := do + let .mvar mvarId := e.getAppFn | return .none + let .some decl ← getDelayedMVarAssignment? mvarId | return .none + let mvarIdPending := decl.mvarIdPending + -- Print the function application e. See Lean's `withOverApp` + let args := e.getAppArgs + + -- Not enough arguments to instantiate this + if args.size < decl.fvars.size then + return .none + + let callee ← self $ ← instantiateMVars $ .mvar mvarIdPending + let sites ← + decl.fvars.zip args |>.mapM (λ (fvar, arg) => do + let fvarName := Expr.fvarId! fvar |>.name + return s!"({toString fvarName} {← self arg})" + ) + let tailArgs ← args.toList.drop decl.fvars.size |>.mapM self + + + let sites := " ".intercalate sites.toList + let result := if tailArgs.isEmpty then + s!"(:subst {callee} {sites})" + else + let tailArgs := " ".intercalate tailArgs + s!"((:subst {callee} {sites}) {tailArgs})" + return .some result + + self (e: Expr): MetaM String := do + if let .some result ← delayedMVarToSexp e then + return result match e with | .bvar deBruijnIndex => -- This is very common so the index alone is shown. Literals are handled below. diff --git a/Test/Integration.lean b/Test/Integration.lean index 66b3637..9bd5db6 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq := vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], } let goal2: Protocol.Goal := { - name := "_uniq.17", + name := "_uniq.14", target := { pp? := .some "x ∨ y → y ∨ x" }, vars := #[ { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, - { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} ], } subroutine_runner [ diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 33fe8cb..0818881 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -263,7 +263,7 @@ def test_partial_continuation: TestM Unit := do -- Continuation should fail if the state does not exist: match state0.resume coupled_goals with - | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope") + | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope") | .ok _ => addTest $ assertUnreachable "(continuation failure)" -- Continuation should fail if some goals have not been solved match state2.continue state1 with diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 496bcc8..0d31273 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -243,9 +243,10 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) - -- This is due to delayed assignment + let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (_uniq.54 (:fv _uniq.16)) (_uniq.55 (:fv _uniq.50))) (_uniq.50 0))) (_uniq.47 0))) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (_uniq.67 (:fv _uniq.16)) (_uniq.68 (:fv _uniq.63))) (_uniq.63 0))) (_uniq.60 0))))" + let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))" addTest $ LSpec.test "(2 parent)" (state2parent == - "((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))") + s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state @@ -769,13 +770,34 @@ def test_nat_zero_add_alt: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - let state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with + addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"] + let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" + let state2b ← match state3m2.resume [conduit] with | .ok state => pure state | .error e => do addTest $ assertUnreachable e return () - addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) = - #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"]) + + let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))" + let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))" + let fvN := "_uniq.63" + addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) = + #[ + { + name := "_uniq.70", + userName? := .some "conduit", + target := { + pp? := .some "?m.79 ?m.68 = (n + 0 = n)", + sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv _uniq.84) (:mv _uniq.85) (:mv _uniq.86)) (_uniq.77 (:mv _uniq.68))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", + }, + vars := #[{ + name := fvN, + userName := "n", + type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" }, + isInaccessible? := .some false + }], + } + ]) def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ -- 2.44.1 From f813d4a8dd201a01674917b18d1d39c7ec8138af Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 May 2024 13:49:05 -0700 Subject: [PATCH 24/38] refactor: Delayed mvar instantiation function --- Pantograph/Serial.lean | 43 +++++++++++++++++++++++++----------------- Test/Proofs.lean | 8 +++++--- 2 files changed, 31 insertions(+), 20 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 14a4002..a95180e 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -101,6 +101,26 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String := | _, .zero => s!"{k}" | _, _ => s!"(+ {u_str} {k})" +structure DelayedMVarInvocation where + mvarIdPending: MVarId + args: Array (FVarId × Expr) + tail: Array Expr + +def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do + let .mvar mvarId := e.getAppFn | return .none + let .some decl ← getDelayedMVarAssignment? mvarId | return .none + let mvarIdPending := decl.mvarIdPending + -- Print the function application e. See Lean's `withOverApp` + let args := e.getAppArgs + + assert! args.size >= decl.fvars.size + + return .some { + mvarIdPending, + args := decl.fvars.map (·.fvarId!) |>.zip args, + tail := args.toList.drop decl.fvars.size |>.toArray, + } + /-- Completely serializes an expression tree. Json not used due to compactness @@ -111,30 +131,19 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM self expr where delayedMVarToSexp (e: Expr): MetaM (Option String) := do - let .mvar mvarId := e.getAppFn | return .none - let .some decl ← getDelayedMVarAssignment? mvarId | return .none - let mvarIdPending := decl.mvarIdPending - -- Print the function application e. See Lean's `withOverApp` - let args := e.getAppArgs - - -- Not enough arguments to instantiate this - if args.size < decl.fvars.size then - return .none - - let callee ← self $ ← instantiateMVars $ .mvar mvarIdPending - let sites ← - decl.fvars.zip args |>.mapM (λ (fvar, arg) => do - let fvarName := Expr.fvarId! fvar |>.name - return s!"({toString fvarName} {← self arg})" + let .some invocation ← toDelayedMVarInvocation e | return .none + let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending + let sites ← invocation.args.mapM (λ (fvar, arg) => do + pure s!"({toString fvar.name} {← self arg})" ) - let tailArgs ← args.toList.drop decl.fvars.size |>.mapM self + let tailArgs ← invocation.tail.mapM self let sites := " ".intercalate sites.toList let result := if tailArgs.isEmpty then s!"(:subst {callee} {sites})" else - let tailArgs := " ".intercalate tailArgs + let tailArgs := " ".intercalate tailArgs.toList s!"((:subst {callee} {sites}) {tailArgs})" return .some result diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 0d31273..54b5016 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -748,10 +748,11 @@ def test_nat_zero_add_alt: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () + let major := "_uniq.68" addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) = #[ buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"), - buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat", + buildNamedGoal major [("n", "Nat")] "Nat", buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t", buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit") ]) @@ -770,7 +771,8 @@ def test_nat_zero_add_alt: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"] + let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84") + addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT] let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" let state2b ← match state3m2.resume [conduit] with | .ok state => pure state @@ -788,7 +790,7 @@ def test_nat_zero_add_alt: TestM Unit := do userName? := .some "conduit", target := { pp? := .some "?m.79 ?m.68 = (n + 0 = n)", - sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv _uniq.84) (:mv _uniq.85) (:mv _uniq.86)) (_uniq.77 (:mv _uniq.68))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", + sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (_uniq.77 (:mv {major}))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", }, vars := #[{ name := fvN, -- 2.44.1 From bc09f4a29df6e32a1b016b6b563d58b9a26f2411 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 13 May 2024 13:58:50 -0700 Subject: [PATCH 25/38] refactor: Expr related functions to Expr.lean --- Pantograph/Expr.lean | 52 +++++++++++++++++++++++++++++++++++++++++ Pantograph/Library.lean | 4 ++++ Pantograph/Serial.lean | 43 +--------------------------------- 3 files changed, 57 insertions(+), 42 deletions(-) create mode 100644 Pantograph/Expr.lean diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean new file mode 100644 index 0000000..14d063e --- /dev/null +++ b/Pantograph/Expr.lean @@ -0,0 +1,52 @@ +import Lean + +open Lean + +namespace Pantograph + +def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ + +/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ +def unfoldAuxLemmas (e : Expr) : CoreM Expr := do + Lean.Meta.deltaExpand e Lean.Name.isAuxLemma + +def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do + Meta.transform e + (pre := fun e => e.withApp fun f args => do + if let .mvar mvarId := f then + if let some decl ← getDelayedMVarAssignment? mvarId then + if args.size ≥ decl.fvars.size then + let pending ← instantiateMVars (.mvar decl.mvarIdPending) + if !pending.isMVar then + return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args + return .continue) + +@[export pantograph_instantiate_all_meta_m] +def instantiateAll (e: Expr): MetaM Expr := do + let e ← instantiateMVars e + let e ← unfoldAuxLemmas e + --let e ← instantiatePartialDelayedMVars e + return e + +structure DelayedMVarInvocation where + mvarIdPending: MVarId + args: Array (FVarId × Expr) + tail: Array Expr + +@[export pantograph_to_delayed_mvar_invocation_meta_m] +def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do + let .mvar mvarId := e.getAppFn | return .none + let .some decl ← getDelayedMVarAssignment? mvarId | return .none + let mvarIdPending := decl.mvarIdPending + -- Print the function application e. See Lean's `withOverApp` + let args := e.getAppArgs + + assert! args.size >= decl.fvars.size + + return .some { + mvarIdPending, + args := decl.fvars.map (·.fvarId!) |>.zip args, + tail := args.toList.drop decl.fvars.size |>.toArray, + } + +end Pantograph diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 59d7adc..9c64b69 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -78,6 +78,10 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do (trustLevel := 1) return { env := env } +@[export pantograph_create_meta_context] +def createMetaContext: IO Lean.Meta.Context := do + return {} + @[export pantograph_env_catalog_m] def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a95180e..58d4ea7 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -2,6 +2,7 @@ All serialisation functions -/ import Lean +import Pantograph.Expr import Pantograph.Protocol import Pantograph.Goal @@ -10,30 +11,8 @@ open Lean -- Symbol processing functions -- -def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ - namespace Pantograph -/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ -def unfoldAuxLemmas (e : Expr) : CoreM Expr := do - Lean.Meta.deltaExpand e Lean.Name.isAuxLemma - -def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do - Meta.transform e - (pre := fun e => e.withApp fun f args => do - if let .mvar mvarId := f then - if let some decl ← getDelayedMVarAssignment? mvarId then - if args.size ≥ decl.fvars.size then - let pending ← instantiateMVars (.mvar decl.mvarIdPending) - if !pending.isMVar then - return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args - return .continue) - -def instantiateAll (e: Expr): MetaM Expr := do - let e ← instantiateMVars e - let e ← unfoldAuxLemmas e - --let e ← instantiatePartialDelayedMVars e - return e --- Input Functions --- @@ -101,26 +80,6 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String := | _, .zero => s!"{k}" | _, _ => s!"(+ {u_str} {k})" -structure DelayedMVarInvocation where - mvarIdPending: MVarId - args: Array (FVarId × Expr) - tail: Array Expr - -def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do - let .mvar mvarId := e.getAppFn | return .none - let .some decl ← getDelayedMVarAssignment? mvarId | return .none - let mvarIdPending := decl.mvarIdPending - -- Print the function application e. See Lean's `withOverApp` - let args := e.getAppArgs - - assert! args.size >= decl.fvars.size - - return .some { - mvarIdPending, - args := decl.fvars.map (·.fvarId!) |>.zip args, - tail := args.toList.drop decl.fvars.size |>.toArray, - } - /-- Completely serializes an expression tree. Json not used due to compactness -- 2.44.1 From 5c7bb288b2914d5179fa117289e4455893b3ddd2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 14 May 2024 19:08:25 -0700 Subject: [PATCH 26/38] feat: Display full free variable list in subst --- Pantograph/Expr.lean | 12 ++++++++++-- Pantograph/Serial.lean | 8 +++++--- Test/Proofs.lean | 8 ++++---- 3 files changed, 19 insertions(+), 9 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 14d063e..7e691d5 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -30,7 +30,7 @@ def instantiateAll (e: Expr): MetaM Expr := do structure DelayedMVarInvocation where mvarIdPending: MVarId - args: Array (FVarId × Expr) + args: Array (FVarId × (Option Expr)) tail: Array Expr @[export pantograph_to_delayed_mvar_invocation_meta_m] @@ -38,14 +38,22 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d let .mvar mvarId := e.getAppFn | return .none let .some decl ← getDelayedMVarAssignment? mvarId | return .none let mvarIdPending := decl.mvarIdPending + let mvarDecl ← mvarIdPending.getDecl -- Print the function application e. See Lean's `withOverApp` let args := e.getAppArgs assert! args.size >= decl.fvars.size + let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList + let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do + let fvarId := localDecl.fvarId + let a := fvarArgMap.find? fvarId + return acc ++ [(fvarId, a)] + + assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome) return .some { mvarIdPending, - args := decl.fvars.map (·.fvarId!) |>.zip args, + args := subst.toArray, tail := args.toList.drop decl.fvars.size |>.toArray, } diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 58d4ea7..3d46ee2 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -92,12 +92,14 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM delayedMVarToSexp (e: Expr): MetaM (Option String) := do let .some invocation ← toDelayedMVarInvocation e | return .none let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending - let sites ← invocation.args.mapM (λ (fvar, arg) => do - pure s!"({toString fvar.name} {← self arg})" + let sites ← invocation.args.mapM (λ (fvarId, arg) => do + let arg := match arg with + | .some arg => arg + | .none => .fvar fvarId + self arg ) let tailArgs ← invocation.tail.mapM self - let sites := " ".intercalate sites.toList let result := if tailArgs.isEmpty then s!"(:subst {callee} {sites})" diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 54b5016..b09e403 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -243,10 +243,10 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) - let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (_uniq.54 (:fv _uniq.16)) (_uniq.55 (:fv _uniq.50))) (_uniq.50 0))) (_uniq.47 0))) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (_uniq.67 (:fv _uniq.16)) (_uniq.68 (:fv _uniq.63))) (_uniq.63 0))) (_uniq.60 0))))" - let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))" + let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))" + let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))" addTest $ LSpec.test "(2 parent)" (state2parent == - s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}") + s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state @@ -790,7 +790,7 @@ def test_nat_zero_add_alt: TestM Unit := do userName? := .some "conduit", target := { pp? := .some "?m.79 ?m.68 = (n + 0 = n)", - sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (_uniq.77 (:mv {major}))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", + sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (:fv {fvN}) (:mv {major})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", }, vars := #[{ name := fvN, -- 2.44.1 From cf174280014dcfa3533e15b85a455bd2146e2951 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 15 May 2024 21:34:15 -0700 Subject: [PATCH 27/38] fix: Panic in partial instantiation --- Pantograph/Expr.lean | 10 ++++++++-- Test/Integration.lean | 4 ++-- Test/Proofs.lean | 6 +++--- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 7e691d5..85c7f35 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -14,18 +14,24 @@ def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do Meta.transform e (pre := fun e => e.withApp fun f args => do if let .mvar mvarId := f then + if ← mvarId.isAssigned then + return .visit <| (← instantiateMVars e) if let some decl ← getDelayedMVarAssignment? mvarId then if args.size ≥ decl.fvars.size then + -- Do not use instantiateMVars here. Only one step of instantiation should happen. let pending ← instantiateMVars (.mvar decl.mvarIdPending) if !pending.isMVar then - return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args + let pending := pending.abstract decl.fvars + let pending := pending.instantiateRevRange 0 decl.fvars.size args + let pending := mkAppRange pending decl.fvars.size args.size args + return .visit <| pending return .continue) @[export pantograph_instantiate_all_meta_m] def instantiateAll (e: Expr): MetaM Expr := do let e ← instantiateMVars e + let e ← instantiatePartialDelayedMVars e let e ← unfoldAuxLemmas e - --let e ← instantiatePartialDelayedMVars e return e structure DelayedMVarInvocation where diff --git a/Test/Integration.lean b/Test/Integration.lean index 9bd5db6..66b3637 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq := vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], } let goal2: Protocol.Goal := { - name := "_uniq.14", + name := "_uniq.17", target := { pp? := .some "x ∨ y → y ∨ x" }, vars := #[ { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}, - { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} + { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }} ], } subroutine_runner [ diff --git a/Test/Proofs.lean b/Test/Proofs.lean index b09e403..ea6ff11 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -771,7 +771,7 @@ def test_nat_zero_add_alt: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84") + let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87") addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT] let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict" let state2b ← match state3m2.resume [conduit] with @@ -789,8 +789,8 @@ def test_nat_zero_add_alt: TestM Unit := do name := "_uniq.70", userName? := .some "conduit", target := { - pp? := .some "?m.79 ?m.68 = (n + 0 = n)", - sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (:fv {fvN}) (:mv {major})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", + pp? := .some "(?motive.a = ?motive.a) = (n + 0 = n)", + sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", }, vars := #[{ name := fvN, -- 2.44.1 From 6ad24b72d474f015543e425f148fb7a3dc7b81da Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Thu, 16 May 2024 10:31:38 -0700 Subject: [PATCH 28/38] fix: Nested delayed assignment instantiation --- Pantograph/Expr.lean | 93 ++++++++++++++++++++++++++++++++++-------- Pantograph/Serial.lean | 4 +- Test/Proofs.lean | 37 ++++++++++++----- 3 files changed, 106 insertions(+), 28 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 85c7f35..9f4b8d9 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -10,35 +10,94 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ def unfoldAuxLemmas (e : Expr) : CoreM Expr := do Lean.Meta.deltaExpand e Lean.Name.isAuxLemma -def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do - Meta.transform e +/-- +Force the instantiation of delayed metavariables even if they cannot be fully +instantiated. This is used during resumption. + +Since Lean 4 does not have an `Expr` constructor corresponding to delayed +metavariables, any delayed metavariables must be recursively handled by this +function to ensure that nested delayed metavariables can be properly processed. +The caveat is this recursive call will lead to infinite recursion if a loop +between metavariable assignment exists. + +This function ensures any metavariable in the result is either +1. Delayed assigned with its pending mvar not assigned in any form +2. Not assigned (delay or not) + -/ +partial def instantiateDelayedMVars (eOrig: Expr): MetaM Expr := do + --let padding := String.join $ List.replicate level " " + --IO.println s!"{padding}Starting {toString eOrig}" + let result ← Meta.transform (← instantiateMVars eOrig) (pre := fun e => e.withApp fun f args => do + --IO.println s!"{padding} V {toString e}" if let .mvar mvarId := f then if ← mvarId.isAssigned then - return .visit <| (← instantiateMVars e) - if let some decl ← getDelayedMVarAssignment? mvarId then - if args.size ≥ decl.fvars.size then - -- Do not use instantiateMVars here. Only one step of instantiation should happen. - let pending ← instantiateMVars (.mvar decl.mvarIdPending) - if !pending.isMVar then - let pending := pending.abstract decl.fvars - let pending := pending.instantiateRevRange 0 decl.fvars.size args - let pending := mkAppRange pending decl.fvars.size args.size args - return .visit <| pending - return .continue) + --IO.println s!"{padding} A ?{mvarId.name}" + return .continue <| .some (← self e) + if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + -- No progress can be made on this + if !(← mvarIdPending.isAssigned) then + --IO.println s!"{padding} D/T1: {toString e}" + let args ← args.mapM self + let result := mkAppN f args + return .done result + --IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}" + -- This asstion fails when a tactic or elaboration function is + -- implemented incorrectly. See `instantiateExprMVars` + if args.size < fvars.size then + --IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}" + throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" + assert! !(← mvarIdPending.isDelayedAssigned) + let pending ← self (.mvar mvarIdPending) + if pending == .mvar mvarIdPending then + -- No progress could be made on this case + --IO.println s!"{padding}D/N {toString e}" + assert! !(← mvarIdPending.isAssigned) + assert! !(← mvarIdPending.isDelayedAssigned) + --else if pending.isMVar then + -- assert! !(← pending.mvarId!.isAssigned) + -- assert! !(← pending.mvarId!.isDelayedAssigned) + -- -- Progress made, but this is now another delayed assigned mvar + -- let nextMVarId ← mkFreshMVarId + -- assignDelayedMVar nextMVarId fvars pending.mvarId! + -- let args ← args.mapM self + -- let result := mkAppN (.mvar nextMVarId) args + -- return .done result + else + -- Progress has been made on this mvar + let pending := pending.abstract fvars + let args ← args.mapM self + -- Craete the function call structure + let subst := pending.instantiateRevRange 0 fvars.size args + let result := mkAppRange subst fvars.size args.size args + --IO.println s!"{padding}D/T2 {toString result}" + return .done result + return .continue) + --IO.println s!"{padding}Result {toString result}" + return result + where + self e := instantiateDelayedMVars e + +/-- +Convert an expression to an equiavlent form with +1. No nested delayed assigned mvars +2. No aux lemmas +3. No assigned mvars + -/ @[export pantograph_instantiate_all_meta_m] def instantiateAll (e: Expr): MetaM Expr := do - let e ← instantiateMVars e - let e ← instantiatePartialDelayedMVars e + let e ← instantiateDelayedMVars e let e ← unfoldAuxLemmas e return e structure DelayedMVarInvocation where mvarIdPending: MVarId args: Array (FVarId × (Option Expr)) + -- Extra arguments applied to the result of this substitution tail: Array Expr +-- The pending mvar of any delayed assigned mvar must not be assigned in any way. @[export pantograph_to_delayed_mvar_invocation_meta_m] def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do let .mvar mvarId := e.getAppFn | return .none @@ -48,7 +107,9 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d -- Print the function application e. See Lean's `withOverApp` let args := e.getAppArgs - assert! args.size >= decl.fvars.size + assert! args.size ≥ decl.fvars.size + assert! !(← mvarIdPending.isAssigned) + assert! !(← mvarIdPending.isDelayedAssigned) let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do let fvarId := localDecl.fvarId diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 3d46ee2..17dee2d 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -91,7 +91,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM where delayedMVarToSexp (e: Expr): MetaM (Option String) := do let .some invocation ← toDelayedMVarInvocation e | return .none - let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending + let callee ← self $ .mvar invocation.mvarIdPending let sites ← invocation.args.mapM (λ (fvarId, arg) => do let arg := match arg with | .some arg => arg @@ -264,7 +264,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava name := ofName goal.name, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, - target := (← serializeExpression options (← instantiateAll mvarDecl.type)), + target := (← serializeExpression options (← instantiate mvarDecl.type)), vars := vars.reverse.toArray } where diff --git a/Test/Proofs.lean b/Test/Proofs.lean index ea6ff11..aa730ba 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -226,11 +226,25 @@ def test_or_comm: TestM Unit := do | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = - #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"]) + let fvP := "_uniq.10" + let fvQ := "_uniq.13" + let fvH := "_uniq.16" + let state1g0 := "_uniq.17" + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) = + #[{ + name := state1g0, + target := { pp? := .some "q ∨ p" }, + vars := #[ + { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, + { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false }, + { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false } + ] + }]) addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone + let state1parent ← 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}) (:fv {fvP}) (:fv {fvQ}) 0))))") let tactic := "cases h" let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state @@ -239,22 +253,25 @@ def test_or_comm: TestM Unit := do return () addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[branchGoal "inl" "p", branchGoal "inr" "q"]) + let (caseL, caseR) := ("_uniq.62", "_uniq.75") + addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) = + #[caseL, caseR]) addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false) - let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))" - let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))" + let state2parent ← serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) + let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" + let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" addTest $ LSpec.test "(2 parent)" (state2parent == - s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})") + s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))") let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))") + let state3_1parent ← 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.87))") addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state @@ -262,8 +279,8 @@ def test_or_comm: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check " assumption" state4_1.goals.isEmpty - let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false) - addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)") + let state4_1parent ← instantiateAll state4_1.parentExpr?.get! + addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with | .success state => pure state -- 2.44.1 From 2f951c8fefcf3566fd5f2b38c508db96ef5cba00 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 19 May 2024 15:43:10 -0700 Subject: [PATCH 29/38] fix: Decoupling of mvars during instantiation --- Pantograph/Expr.lean | 114 ++++++++++++++++++++++------------------ Pantograph/Goal.lean | 10 ++++ Pantograph/Library.lean | 10 ++-- Pantograph/Serial.lean | 2 +- Test/Proofs.lean | 51 ++++++++++++++---- 5 files changed, 122 insertions(+), 65 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 9f4b8d9..8f890e3 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -12,7 +12,8 @@ def unfoldAuxLemmas (e : Expr) : CoreM Expr := do /-- Force the instantiation of delayed metavariables even if they cannot be fully -instantiated. This is used during resumption. +instantiated. This is used during resumption to provide diagnostic data about +the current goal. Since Lean 4 does not have an `Expr` constructor corresponding to delayed metavariables, any delayed metavariables must be recursively handled by this @@ -24,60 +25,73 @@ This function ensures any metavariable in the result is either 1. Delayed assigned with its pending mvar not assigned in any form 2. Not assigned (delay or not) -/ -partial def instantiateDelayedMVars (eOrig: Expr): MetaM Expr := do - --let padding := String.join $ List.replicate level " " +partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do + --let padding := String.join $ List.replicate level "│ " --IO.println s!"{padding}Starting {toString eOrig}" - let result ← Meta.transform (← instantiateMVars eOrig) + let mut result ← Meta.transform (← instantiateMVars eOrig) (pre := fun e => e.withApp fun f args => do - --IO.println s!"{padding} V {toString e}" - if let .mvar mvarId := f then - if ← mvarId.isAssigned then - --IO.println s!"{padding} A ?{mvarId.name}" - return .continue <| .some (← self e) - if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then - -- No progress can be made on this - if !(← mvarIdPending.isAssigned) then - --IO.println s!"{padding} D/T1: {toString e}" - let args ← args.mapM self - let result := mkAppN f args - return .done result + let .mvar mvarId := f | return .continue + --IO.println s!"{padding}├V {e}" + let mvarDecl ← mvarId.getDecl - --IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}" - -- This asstion fails when a tactic or elaboration function is - -- implemented incorrectly. See `instantiateExprMVars` - if args.size < fvars.size then - --IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}" - throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" - assert! !(← mvarIdPending.isDelayedAssigned) - let pending ← self (.mvar mvarIdPending) - if pending == .mvar mvarIdPending then - -- No progress could be made on this case - --IO.println s!"{padding}D/N {toString e}" - assert! !(← mvarIdPending.isAssigned) - assert! !(← mvarIdPending.isDelayedAssigned) - --else if pending.isMVar then - -- assert! !(← pending.mvarId!.isAssigned) - -- assert! !(← pending.mvarId!.isDelayedAssigned) - -- -- Progress made, but this is now another delayed assigned mvar - -- let nextMVarId ← mkFreshMVarId - -- assignDelayedMVar nextMVarId fvars pending.mvarId! - -- let args ← args.mapM self - -- let result := mkAppN (.mvar nextMVarId) args - -- return .done result - else - -- Progress has been made on this mvar - let pending := pending.abstract fvars - let args ← args.mapM self - -- Craete the function call structure - let subst := pending.instantiateRevRange 0 fvars.size args - let result := mkAppRange subst fvars.size args.size args - --IO.println s!"{padding}D/T2 {toString result}" - return .done result - return .continue) - --IO.println s!"{padding}Result {toString result}" + -- This is critical to maintaining the interdependency of metavariables. + -- Without setting `.syntheticOpaque`, Lean's metavariable elimination + -- system will not make the necessary delayed assigned mvars in case of + -- nested mvars. + mvarId.setKind .syntheticOpaque + + let lctx ← MonadLCtx.getLCtx + if mvarDecl.lctx.any (λ decl => !lctx.contains decl.fvarId) then + let violations := mvarDecl.lctx.decls.foldl (λ acc decl? => match decl? with + | .some decl => if lctx.contains decl.fvarId then acc else acc ++ [decl.fvarId.name] + | .none => acc) [] + panic! s!"Local context variable violation: {violations}" + + if let .some assign ← getExprMVarAssignment? mvarId then + --IO.println s!"{padding}├A ?{mvarId.name}" + assert! !(← mvarId.isDelayedAssigned) + return .visit (mkAppN assign args) + else if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then + --let substTableStr := String.intercalate ", " $ Array.zipWith fvars args (λ fvar assign => s!"{fvar.fvarId!.name} := {assign}") |>.toList + --IO.println s!"{padding}├MD ?{mvarId.name} := ?{mvarIdPending.name} [{substTableStr}]" + + if args.size < fvars.size then + throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}" + --if !args.isEmpty then + --IO.println s!"{padding}├── Arguments Begin" + let args ← args.mapM self + --if !args.isEmpty then + --IO.println s!"{padding}├── Arguments End" + if !(← mvarIdPending.isAssignedOrDelayedAssigned) then + --IO.println s!"{padding}├T1" + let result := mkAppN f args + return .done result + + let pending ← mvarIdPending.withContext do + let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1) + --IO.println s!"{padding}├Pre: {inner}" + let r := (← Expr.abstractM inner fvars).instantiateRev args + pure r + + -- Tail arguments + let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray) + --IO.println s!"{padding}├MD {result}" + return .done result + else + assert! !(← mvarId.isAssigned) + assert! !(← mvarId.isDelayedAssigned) + --if !args.isEmpty then + -- IO.println s!"{padding}├── Arguments Begin" + let args ← args.mapM self + --if !args.isEmpty then + -- IO.println s!"{padding}├── Arguments End" + + --IO.println s!"{padding}├M ?{mvarId.name}" + return .done (mkAppN f args)) + --IO.println s!"{padding}└Result {result}" return result where - self e := instantiateDelayedMVars e + self e := instantiateDelayedMVars e --(level := level + 1) /-- Convert an expression to an equiavlent form with diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index e1d36b3..8efc20f 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -62,6 +62,16 @@ protected def GoalState.mctx (state: GoalState): MetavarContext := state.savedState.term.meta.meta.mctx protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env + +protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do + let metaM := mvarId.withContext m + metaM.run' (← read) state.savedState.term.meta.meta + +protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do + state.withContext state.parentMVar?.get! m +protected def GoalState.withRootContext (state: GoalState) (m: MetaM α): MetaM α := do + state.withContext state.root m + private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 9c64b69..34e1ecc 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -179,10 +179,12 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto runMetaM do state.restoreMetaM return { - root? := ← state.rootExpr?.mapM (λ expr => do - serializeExpression options (← instantiateAll expr)), - parent? := ← state.parentExpr?.mapM (λ expr => do - serializeExpression options (← instantiateAll expr)), + root? := ← state.rootExpr?.mapM (λ expr => + state.withRootContext do + serializeExpression options (← instantiateAll expr)), + parent? := ← state.parentExpr?.mapM (λ expr => + state.withParentContext do + serializeExpression options (← instantiateAll expr)), } @[export pantograph_goal_diag_m] def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String := diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 17dee2d..a6c0ece 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -264,7 +264,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava name := ofName goal.name, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, - target := (← serializeExpression options (← instantiate mvarDecl.type)), + target := (← serializeExpression options (← instantiateMVars (← instantiate mvarDecl.type))), vars := vars.reverse.toArray } where diff --git a/Test/Proofs.lean b/Test/Proofs.lean index aa730ba..9c45138 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -84,6 +84,27 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq := | .ok (_, a) => return a +def test_identity: TestM Unit := do + let state? ← startProof (.expr "∀ (p: Prop), p → p") + let state0 ← match state? with + | .some state => pure state + | .none => do + addTest $ assertUnreachable "Goal could not parse" + return () + + let tactic := "intro p h" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let inner := "_uniq.12" + addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.name) = + #[inner]) + let state1parent ← state1.withParentContext do + serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false) + addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda h 0 (:subst (:mv {inner}) 1 0)))") + -- Individual test cases example: ∀ (a b: Nat), a + b = b + a := by intro n m @@ -243,8 +264,9 @@ def test_or_comm: TestM Unit := do addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone - let state1parent ← 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}) (:fv {fvP}) (:fv {fvQ}) 0))))") + let state1parent ← state1.withParentContext do + 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))))") let tactic := "cases h" let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state @@ -253,25 +275,31 @@ def test_or_comm: TestM Unit := do return () addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[branchGoal "inl" "p", branchGoal "inr" "q"]) - let (caseL, caseR) := ("_uniq.62", "_uniq.75") + let (caseL, caseR) := ("_uniq.64", "_uniq.77") addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) = #[caseL, caseR]) - addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome + addTest $ LSpec.check "(2 parent exists)" state2.parentExpr?.isSome addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state2parent ← serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) + let state2parent ← state2.withParentContext do + serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false) let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))" let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))" + let motive := s!"(:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) ((:c Or) (:fv {fvP}) (:fv {fvQ})) (:fv {fvH}) 0) {orQP}))" + let caseL := s!"(:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseL}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let caseR := s!"(:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:subst (:mv {caseR}) (:fv {fvP}) (:fv {fvQ}) 1)))" + let conduit := s!"((:c Eq.refl) {orPQ} (:fv {fvH}))" addTest $ LSpec.test "(2 parent)" (state2parent == - s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))") + 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 | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - let state3_1parent ← 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.87))") + let state3_1parent ← state3_1.withParentContext do + 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.check "· apply Or.inr" (state3_1.goals.length = 1) let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with | .success state => pure state @@ -800,14 +828,16 @@ def test_nat_zero_add_alt: TestM Unit := do let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))" let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))" let fvN := "_uniq.63" + let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))" + let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))" addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) = #[ { name := "_uniq.70", userName? := .some "conduit", target := { - pp? := .some "(?motive.a = ?motive.a) = (n + 0 = n)", - sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))", + pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)", + sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})", }, vars := #[{ name := fvN, @@ -820,6 +850,7 @@ def test_nat_zero_add_alt: TestM Unit := do def suite (env: Environment): List (String × IO LSpec.TestSeq) := let tests := [ + ("identity", test_identity), ("Nat.add_comm", test_nat_add_comm false), ("Nat.add_comm manual", test_nat_add_comm true), ("Nat.add_comm delta", test_delta_variable), -- 2.44.1 From cc74d41b150343215f40f391b52f308adc14a65c Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 20 May 2024 10:55:52 -0700 Subject: [PATCH 30/38] feat: Congruence tactics --- Pantograph/Tactic.lean | 1 + Pantograph/Tactic/Congruence.lean | 78 +++++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 Pantograph/Tactic/Congruence.lean diff --git a/Pantograph/Tactic.lean b/Pantograph/Tactic.lean index 5a7828c..225ad31 100644 --- a/Pantograph/Tactic.lean +++ b/Pantograph/Tactic.lean @@ -1,3 +1,4 @@ +import Pantograph.Tactic.Congruence import Pantograph.Tactic.MotivatedApply import Pantograph.Tactic.NoConfuse diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean new file mode 100644 index 0000000..3de904f --- /dev/null +++ b/Pantograph/Tactic/Congruence.lean @@ -0,0 +1,78 @@ +import Lean + +open Lean + +namespace Pantograph.Tactic + +def congruenceArg: Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + -- Create the descendant goals + + let nextGoals ← goal.withContext do + let u ← Meta.mkFreshLevelMVar + let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous + let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous alpha beta .default) + .synthetic (userName := goal.name ++ `f) + let a₁ ← Meta.mkFreshExprMVar (.some alpha) + .synthetic (userName := goal.name ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some alpha) + .synthetic (userName := goal.name ++ `a₂) + let h ← Meta.mkEq a₁ a₂ + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType) + let conduit ← Meta.mkFreshExprMVar conduitType + .synthetic (userName := goal.name ++ `conduit) + goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) + return [alpha, a₁, a₂, f, h, conduit] + Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) + +def congruenceFun: Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + -- Create the descendant goals + + let nextGoals ← goal.withContext do + let u ← Meta.mkFreshLevelMVar + let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous + let fType := .forallE .anonymous alpha beta .default + let f₁ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := goal.name ++ `f₁) + let f₂ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := goal.name ++ `f₂) + let a ← Meta.mkFreshExprMVar (.some alpha) + .synthetic (userName := goal.name ++ `a) + let h ← Meta.mkEq f₁ f₂ + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType) + let conduit ← Meta.mkFreshExprMVar conduitType + .synthetic (userName := goal.name ++ `conduit) + goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) + return [alpha, f₁, f₂, h, a, conduit] + Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) + +def congruence: Elab.Tactic.TacticM Unit := do + let goal ← Elab.Tactic.getMainGoal + let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + -- Create the descendant goals + + let nextGoals ← goal.withContext do + let u ← Meta.mkFreshLevelMVar + let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous + let fType := .forallE .anonymous alpha beta .default + let f₁ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := goal.name ++ `f₁) + let f₂ ← Meta.mkFreshExprMVar (.some fType) + .synthetic (userName := goal.name ++ `f₂) + let a₁ ← Meta.mkFreshExprMVar (.some alpha) + .synthetic (userName := goal.name ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some alpha) + .synthetic (userName := goal.name ++ `a₂) + let h₁ ← Meta.mkEq f₁ f₂ + let h₂ ← Meta.mkEq a₁ a₂ + let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType) + let conduit ← Meta.mkFreshExprMVar conduitType + .synthetic (userName := goal.name ++ `conduit) + goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) + return [alpha, f₁, f₂, a₁, a₂, h₁, h₂, conduit] + Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) + +end Pantograph.Tactic -- 2.44.1 From 92acf7782c66f9efc6026a5896be35b84b202f5d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 20 May 2024 11:51:35 -0700 Subject: [PATCH 31/38] test: CongruenceArg tactic --- Pantograph/Tactic/Congruence.lean | 81 +++++++++++++++++-------------- Test/Common.lean | 15 ++++++ Test/Main.lean | 1 + Test/Tactic.lean | 1 + Test/Tactic/Congruence.lean | 36 ++++++++++++++ Test/Tactic/NoConfuse.lean | 6 +-- 6 files changed, 100 insertions(+), 40 deletions(-) create mode 100644 Test/Tactic/Congruence.lean diff --git a/Pantograph/Tactic/Congruence.lean b/Pantograph/Tactic/Congruence.lean index 3de904f..bbb9d75 100644 --- a/Pantograph/Tactic/Congruence.lean +++ b/Pantograph/Tactic/Congruence.lean @@ -6,73 +6,80 @@ namespace Pantograph.Tactic def congruenceArg: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - -- Create the descendant goals + let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + let userName := (← goal.getDecl).userName let nextGoals ← goal.withContext do let u ← Meta.mkFreshLevelMVar - let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous - let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous alpha beta .default) - .synthetic (userName := goal.name ++ `f) - let a₁ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₂) - let h ← Meta.mkEq a₁ a₂ + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let f ← Meta.mkFreshExprMVar (.some <| .forallE .anonymous α β .default) + .synthetic (userName := userName ++ `f) + let a₁ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₂) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) + .synthetic (userName := userName ++ `h) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f a₁) (.app f a₂)) (← goal.getType) let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := goal.name ++ `conduit) + .synthetic (userName := userName ++ `conduit) goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrArg f h) - return [alpha, a₁, a₂, f, h, conduit] + return [α, a₁, a₂, f, h, conduit] Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) def congruenceFun: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - -- Create the descendant goals + let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + let userName := (← goal.getDecl).userName let nextGoals ← goal.withContext do let u ← Meta.mkFreshLevelMVar - let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous - let fType := .forallE .anonymous alpha beta .default + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let fType := .forallE .anonymous α β .default let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₁) + .synthetic (userName := userName ++ `f₁) let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₂) - let a ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a) - let h ← Meta.mkEq f₁ f₂ + .synthetic (userName := userName ++ `f₂) + let a ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a) + let h ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a) (.app f₂ a)) (← goal.getType) let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := goal.name ++ `conduit) + .synthetic (userName := userName ++ `conduit) goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongrFun h a) - return [alpha, f₁, f₂, h, a, conduit] + return [α, f₁, f₂, h, a, conduit] Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) def congruence: Elab.Tactic.TacticM Unit := do let goal ← Elab.Tactic.getMainGoal - let .some (beta, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" - -- Create the descendant goals + let .some (β, _, _) := (← goal.getType).eq? | throwError "Goal is not an Eq" + let userName := (← goal.getDecl).userName let nextGoals ← goal.withContext do let u ← Meta.mkFreshLevelMVar - let alpha ← Meta.mkFreshExprMVar (.some $ mkSort u) .natural .anonymous - let fType := .forallE .anonymous alpha beta .default + let α ← Meta.mkFreshExprMVar (.some $ mkSort u) + .natural (userName := userName ++ `α) + let fType := .forallE .anonymous α β .default let f₁ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₁) + .synthetic (userName := userName ++ `f₁) let f₂ ← Meta.mkFreshExprMVar (.some fType) - .synthetic (userName := goal.name ++ `f₂) - let a₁ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₁) - let a₂ ← Meta.mkFreshExprMVar (.some alpha) - .synthetic (userName := goal.name ++ `a₂) - let h₁ ← Meta.mkEq f₁ f₂ - let h₂ ← Meta.mkEq a₁ a₂ + .synthetic (userName := userName ++ `f₂) + let a₁ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₁) + let a₂ ← Meta.mkFreshExprMVar (.some α) + .synthetic (userName := userName ++ `a₂) + let h₁ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq f₁ f₂) + .synthetic (userName := userName ++ `h₁) + let h₂ ← Meta.mkFreshExprMVar (.some $ ← Meta.mkEq a₁ a₂) + .synthetic (userName := userName ++ `h₂) let conduitType ← Meta.mkEq (← Meta.mkEq (.app f₁ a₁) (.app f₂ a₂)) (← goal.getType) let conduit ← Meta.mkFreshExprMVar conduitType - .synthetic (userName := goal.name ++ `conduit) + .synthetic (userName := userName ++ `conduit) goal.assign $ ← Meta.mkEqMP conduit (← Meta.mkCongr h₁ h₂) - return [alpha, f₁, f₂, a₁, a₂, h₁, h₂, conduit] + return [α, f₁, f₂, a₁, a₂, h₁, h₂, conduit] Elab.Tactic.setGoals <| nextGoals.map (·.mvarId!) end Pantograph.Tactic diff --git a/Test/Common.lean b/Test/Common.lean index 6ea4fb2..c656309 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -27,6 +27,7 @@ def Goal.devolatilize (goal: Goal): Goal := name := "", } +deriving instance DecidableEq, Repr for Name deriving instance DecidableEq, Repr for Expression deriving instance DecidableEq, Repr for Variable deriving instance DecidableEq, Repr for Goal @@ -65,9 +66,23 @@ def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e +def parseSentence (s: String): MetaM Expr := do + let recursor ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `term) + (input := s) + (fileName := filename) with + | .ok syn => pure syn + | .error error => throwError "Failed to parse: {error}" + runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none + def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] } return newGoals.goals +def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do + let name := (← mvarId.getDecl).userName + let t ← exprToStr (← mvarId.getType) + return (name, t) end Test diff --git a/Test/Main.lean b/Test/Main.lean index 4a1ca69..31042c5 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -49,6 +49,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Serial", Serial.suite env_default), + ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), ] diff --git a/Test/Tactic.lean b/Test/Tactic.lean index f1e2649..5863ec0 100644 --- a/Test/Tactic.lean +++ b/Test/Tactic.lean @@ -1,2 +1,3 @@ +import Test.Tactic.Congruence import Test.Tactic.MotivatedApply import Test.Tactic.NoConfuse diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean new file mode 100644 index 0000000..7ef358a --- /dev/null +++ b/Test/Tactic/Congruence.lean @@ -0,0 +1,36 @@ +import LSpec +import Lean +import Test.Common + +open Lean +open Pantograph + +namespace Pantograph.Test.Tactic.Congruence + +def test_congr_arg (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m" + runMetaMSeq env do + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let mut tests := LSpec.TestSeq.done + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.70"), + (`a₁, "?α"), + (`a₂, "?α"), + (`f, "?α → Nat"), + (`h, "?a₁ = ?a₂"), + (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"), + ]) + tests := tests ++ test + return tests + +def suite (env: Environment): List (String × IO LSpec.TestSeq) := + [ + ("congrArg", test_congr_arg env), + ] + +end Pantograph.Test.Tactic.Congruence diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index 54c2be7..442e2ca 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -92,9 +92,9 @@ def test_list (env: Environment): IO LSpec.TestSeq := def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ - ("nat", test_nat env), - ("nat_fail", test_nat_fail env), - ("list", test_list env), + ("Nat", test_nat env), + ("Nat fail", test_nat_fail env), + ("List", test_list env), ] end Pantograph.Test.Tactic.NoConfuse -- 2.44.1 From 75df7268c5c229769c606963b2ef2bb178810bdd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 20 May 2024 11:55:38 -0700 Subject: [PATCH 32/38] test: Simplify testing structure for tactics --- Test/Tactic/MotivatedApply.lean | 44 ++++++++++++--------------------- Test/Tactic/NoConfuse.lean | 19 +++----------- 2 files changed, 19 insertions(+), 44 deletions(-) diff --git a/Test/Tactic/MotivatedApply.lean b/Test/Tactic/MotivatedApply.lean index ad8ebdc..154e34c 100644 --- a/Test/Tactic/MotivatedApply.lean +++ b/Test/Tactic/MotivatedApply.lean @@ -7,24 +7,11 @@ open Pantograph namespace Pantograph.Test.Tactic.MotivatedApply -def valueAndType (recursor: String): MetaM (Expr × Expr) := do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := recursor) - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - runTermElabMInMeta do - let recursor ← Elab.Term.elabTerm (stx := recursor) .none - let recursorType ← Meta.inferType recursor - return (recursor, recursorType) - - def test_type_extract (env: Environment): IO LSpec.TestSeq := runMetaMSeq env do let mut tests := LSpec.TestSeq.done - let (recursor, recursorType) ← valueAndType "@Nat.brecOn" + let recursor ← parseSentence "@Nat.brecOn" + let recursorType ← Meta.inferType recursor tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" = (← exprToStr recursorType)) let info ← match Tactic.getRecursorInformation recursorType with @@ -39,7 +26,7 @@ def test_type_extract (env: Environment): IO LSpec.TestSeq := def test_nat_brec_on (env: Environment): IO LSpec.TestSeq := let expr := "λ (n t: Nat) => n + 0 = n" runMetaMSeq env do - let (expr, exprType) ← valueAndType expr + let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) @@ -59,7 +46,7 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq := "Nat → Prop", "Nat", "∀ (t : Nat), Nat.below t → ?motive t", - "?motive ?m.69 = (n + 0 = n)", + "?motive ?m.67 = (n + 0 = n)", ]) tests := tests ++ test return tests @@ -67,7 +54,7 @@ def test_nat_brec_on (env: Environment): IO LSpec.TestSeq := def test_list_brec_on (env: Environment): IO LSpec.TestSeq := let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l" runMetaMSeq env do - let (expr, exprType) ← valueAndType expr + let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) @@ -84,11 +71,11 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq := let newGoals ← runTacticOnMVar tactic target.mvarId! pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [ - "Type ?u.92", - "List ?m.94 → Prop", - "List ?m.94", - "∀ (t : List ?m.94), List.below t → ?motive t", - "?motive ?m.96 = (l ++ [] = [] ++ l)", + "Type ?u.90", + "List ?m.92 → Prop", + "List ?m.92", + "∀ (t : List ?m.92), List.below t → ?motive t", + "?motive ?m.94 = (l ++ [] = [] ++ l)", ]) tests := tests ++ test return tests @@ -103,30 +90,31 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do (fileName := filename) with | .ok syn => pure syn | .error error => throwError "Failed to parse: {error}" - let (expr, exprType) ← valueAndType expr + let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let mut tests := LSpec.TestSeq.done -- Apply the tactic let target ← Meta.mkFreshExprSyntheticOpaqueMVar body let tactic := Tactic.motivatedApply recursor let newGoals ← runTacticOnMVar tactic target.mvarId! + let majorId := 67 tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [ "Nat → Prop", "Nat", "∀ (t : Nat), Nat.below t → ?motive t", - "?motive ?m.69 = (n + 0 = n)", + s!"?motive ?m.{majorId} = (n + 0 = n)", ])) let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number" - tests := tests ++ (LSpec.check "goal name" (major.name.toString = "_uniq.69")) + tests := tests ++ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}")) -- Assign motive to `λ x => x + _` - let (motive_assign, _) ← valueAndType "λ (x: Nat) => @Nat.add x + 0 = _" + let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _" motive.assign motive_assign let test ← conduit.withContext do let t := toString (← Meta.ppExpr $ ← conduit.getType) - return LSpec.check "conduit" (t = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)") + return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)") tests := tests ++ test return tests diff --git a/Test/Tactic/NoConfuse.lean b/Test/Tactic/NoConfuse.lean index 442e2ca..c672a0b 100644 --- a/Test/Tactic/NoConfuse.lean +++ b/Test/Tactic/NoConfuse.lean @@ -7,23 +7,10 @@ open Pantograph namespace Pantograph.Test.Tactic.NoConfuse -def valueAndType (recursor: String): MetaM (Expr × Expr) := do - let recursor ← match Parser.runParserCategory - (env := ← MonadEnv.getEnv) - (catName := `term) - (input := recursor) - (fileName := filename) with - | .ok syn => pure syn - | .error error => throwError "Failed to parse: {error}" - runTermElabMInMeta do - let recursor ← Elab.Term.elabTerm (stx := recursor) .none - let recursorType ← Meta.inferType recursor - return (recursor, recursorType) - def test_nat (env: Environment): IO LSpec.TestSeq := let expr := "λ (n: Nat) (h: 0 = n + 1) => False" runMetaMSeq env do - let (expr, exprType) ← valueAndType expr + let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) @@ -46,7 +33,7 @@ def test_nat (env: Environment): IO LSpec.TestSeq := def test_nat_fail (env: Environment): IO LSpec.TestSeq := let expr := "λ (n: Nat) (h: n = n) => False" runMetaMSeq env do - let (expr, _) ← valueAndType expr + let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) @@ -70,7 +57,7 @@ def test_nat_fail (env: Environment): IO LSpec.TestSeq := def test_list (env: Environment): IO LSpec.TestSeq := let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False" runMetaMSeq env do - let (expr, exprType) ← valueAndType expr + let expr ← parseSentence expr Meta.lambdaTelescope expr $ λ _ body => do let recursor ← match Parser.runParserCategory (env := ← MonadEnv.getEnv) -- 2.44.1 From bbc00cbbb80748a53c2741bd2e4ee1415ba92f8d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 20 May 2024 14:00:04 -0700 Subject: [PATCH 33/38] feat: Congruence tactic FFI interface and tests --- Pantograph/Goal.lean | 12 +--------- Pantograph/Library.lean | 16 ++++++++++++++ Test/Tactic/Congruence.lean | 44 +++++++++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+), 11 deletions(-) diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 3a8e2fe..46888e7 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -76,7 +76,7 @@ private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := state.savedState.term.meta.restore -private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := +protected def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := state.savedState.term.restore private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do state.savedState.restore @@ -518,11 +518,6 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String): protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Elab.TermElabM TacticResult := do state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryMotivatedApply - let recursor ← match Parser.runParserCategory (env := state.env) (catName := `term) @@ -534,11 +529,6 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Elab.TermElabM TacticResult := do state.restoreElabM - let goal ← match state.savedState.tactic.goals.get? goalId with - | .some goal => pure goal - | .none => return .indexError goalId - goal.checkNotAssigned `GoalState.tryMotivatedApply - let recursor ← match Parser.runParserCategory (env := state.env) (catName := `term) diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 20eaa34..e0625e8 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -204,4 +204,20 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Lean def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): Lean.CoreM TacticResult := runTermElabM <| state.tryNoConfuse goalId eq +inductive TacticExecute where + | congruenceArg + | congruenceFun + | congruence +@[export pantograph_goal_tactic_execute_m] +def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult := + runTermElabM do + state.restoreElabM + let tactic := match tacticExecute with + | .congruenceArg => Tactic.congruenceArg + | .congruenceFun => Tactic.congruenceFun + | .congruence => Tactic.congruence + state.execute goalId tactic + + + end Pantograph diff --git a/Test/Tactic/Congruence.lean b/Test/Tactic/Congruence.lean index 7ef358a..1421263 100644 --- a/Test/Tactic/Congruence.lean +++ b/Test/Tactic/Congruence.lean @@ -27,10 +27,54 @@ def test_congr_arg (env: Environment): IO LSpec.TestSeq := ]) tests := tests ++ test return tests +def test_congr_fun (env: Environment): IO LSpec.TestSeq := + let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2" + runMetaMSeq env do + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let mut tests := LSpec.TestSeq.done + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.159"), + (`f₁, "?α → Nat"), + (`f₂, "?α → Nat"), + (`h, "?f₁ = ?f₂"), + (`a, "?α"), + (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"), + ]) + tests := tests ++ test + return tests +def test_congr (env: Environment): IO LSpec.TestSeq := + let expr := "λ (a b: Nat) => a = b" + runMetaMSeq env do + let expr ← parseSentence expr + Meta.lambdaTelescope expr $ λ _ body => do + let mut tests := LSpec.TestSeq.done + let target ← Meta.mkFreshExprSyntheticOpaqueMVar body + let test ← runTermElabMInMeta do + let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId! + pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) = + [ + (`α, "Sort ?u.10"), + (`f₁, "?α → Nat"), + (`f₂, "?α → Nat"), + (`a₁, "?α"), + (`a₂, "?α"), + (`h₁, "?f₁ = ?f₂"), + (`h₂, "?a₁ = ?a₂"), + (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"), + ]) + tests := tests ++ test + return tests def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("congrArg", test_congr_arg env), + ("congrFun", test_congr_fun env), + ("congr", test_congr env), ] end Pantograph.Test.Tactic.Congruence -- 2.44.1 From bd42c396d71097b100852aa1f25d3759f76edfe0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 20 May 2024 14:19:10 -0700 Subject: [PATCH 34/38] chore: Code cleanup --- Pantograph/Expr.lean | 5 ++--- Pantograph/Library.lean | 3 +-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/Pantograph/Expr.lean b/Pantograph/Expr.lean index 8f890e3..63331af 100644 --- a/Pantograph/Expr.lean +++ b/Pantograph/Expr.lean @@ -70,11 +70,10 @@ partial def instantiateDelayedMVars (eOrig: Expr) : MetaM Expr := do let pending ← mvarIdPending.withContext do let inner ← instantiateDelayedMVars (.mvar mvarIdPending) --(level := level + 1) --IO.println s!"{padding}├Pre: {inner}" - let r := (← Expr.abstractM inner fvars).instantiateRev args - pure r + pure <| (← inner.abstractM fvars).instantiateRev args -- Tail arguments - let result := mkAppN pending (List.drop fvars.size args.toList |>.toArray) + let result := mkAppRange pending fvars.size args.size args --IO.println s!"{padding}├MD {result}" return .done result else diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index e0625e8..d3df45f 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -212,11 +212,10 @@ inductive TacticExecute where def goalTacticExecute (state: GoalState) (goalId: Nat) (tacticExecute: TacticExecute): Lean.CoreM TacticResult := runTermElabM do state.restoreElabM - let tactic := match tacticExecute with + state.execute goalId $ match tacticExecute with | .congruenceArg => Tactic.congruenceArg | .congruenceFun => Tactic.congruenceFun | .congruence => Tactic.congruence - state.execute goalId tactic -- 2.44.1 From 3c90c94645eca5b8ecdc50773180a3543943d2bd Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 5 Jun 2024 13:45:13 -0700 Subject: [PATCH 35/38] fix: Execute instantiateAll in goal state diag --- Pantograph/Serial.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a6c0ece..e12bb7a 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -264,7 +264,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava name := ofName goal.name, userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, - target := (← serializeExpression options (← instantiateMVars (← instantiate mvarDecl.type))), + target := (← serializeExpression options (← instantiate mvarDecl.type)), vars := vars.reverse.toArray } where @@ -319,7 +319,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag else pure [] let type ← if options.instantiate - then instantiateMVars decl.type + then instantiateAll decl.type else pure $ decl.type let type_sexp ← serializeExpressionSexp type (sanitize := false) let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" @@ -327,7 +327,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag if options.printValue then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then let value ← if options.instantiate - then instantiateMVars value + then instantiateAll value else pure $ value pure s!"\n := {← Meta.ppExpr value}" else -- 2.44.1 From 6dcff8b1518f8f6fa42095065398b879254fae09 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 5 Jun 2024 15:56:20 -0700 Subject: [PATCH 36/38] fix: Print diag in mvar context --- Pantograph/Protocol.lean | 1 + Pantograph/Serial.lean | 10 +++++++--- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index f73c3b0..271d4b7 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -273,6 +273,7 @@ structure GoalDiag where -- Print all mvars printAll: Bool := false instantiate: Bool := true + printSexp: Bool := false abbrev CR α := Except InteractionError α diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index e12bb7a..8f56468 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -311,7 +311,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag ) pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join) where - printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := do + printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do let resultFVars: List String ← if options.printContext then decl.lctx.fvarIdToDecl.toList.mapM (λ (fvarId, decl) => @@ -321,8 +321,12 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag let type ← if options.instantiate then instantiateAll decl.type else pure $ decl.type - let type_sexp ← serializeExpressionSexp type (sanitize := false) - let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}" + let type_sexp ← if options.printSexp then + let sexp ← serializeExpressionSexp type (sanitize := false) + pure <| " " ++ sexp + else + pure "" + let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}" let resultValue: String ← if options.printValue then if let Option.some value := (← getMCtx).eAssignment.find? mvarId then -- 2.44.1 From 3a534930894490d12248c4335d42cdf3e2baca56 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 5 Jun 2024 16:14:52 -0700 Subject: [PATCH 37/38] feat: Show delayed assignment in goal diag --- Pantograph/Serial.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 8f56468..5cccb4e 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -329,11 +329,13 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag let resultMain: String := s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}{type_sexp}" let resultValue: String ← if options.printValue then - if let Option.some value := (← getMCtx).eAssignment.find? mvarId then + if let .some value ← getExprMVarAssignment? mvarId then let value ← if options.instantiate then instantiateAll value else pure $ value pure s!"\n := {← Meta.ppExpr value}" + else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then + pure s!"\n := $ {mvarIdPending.name}" else pure "" else -- 2.44.1 From 773a0afbd8a354093c9576df7be19f60f75d57df Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 11 Jun 2024 12:44:42 -0700 Subject: [PATCH 38/38] feat: Handling of universe level names in elab --- Pantograph.lean | 4 +-- Pantograph/Library.lean | 66 ++++++++++++++++++++-------------------- Pantograph/Protocol.lean | 4 +++ Pantograph/Serial.lean | 4 ++- README.md | 6 ++-- Test/Integration.lean | 2 +- Test/Serial.lean | 33 +++++++++++--------- 7 files changed, 64 insertions(+), 55 deletions(-) diff --git a/Pantograph.lean b/Pantograph.lean index c637303..e34e8e4 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -71,7 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do let state ← get - exprEcho args.expr args.type? state.options + 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 @@ -94,7 +94,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := 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 + | .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}" diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 6505fec..f14d8ea 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -34,16 +34,16 @@ def setOptionFromString' (opts : Options) (entry : String) : ExceptT String IO O end Lean +open Lean + namespace Pantograph -def defaultTermElabMContext: Lean.Elab.Term.Context := { - autoBoundImplicit := true, - declName? := some "_pantograph".toName, +def defaultTermElabMContext: Elab.Term.Context := { errToSorry := false } -def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α := +def runMetaM { α } (metaM: MetaM α): CoreM α := metaM.run' -def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α := +def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α := termElabM.run' (ctx := defaultTermElabMContext) |>.run' def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc } @@ -56,13 +56,13 @@ unsafe def initSearch (sp: String): IO Unit := do /-- Creates a Core.Context object needed to run all monads -/ @[export pantograph_create_core_context] -def createCoreContext (options: Array String): IO Lean.Core.Context := do - let options? ← options.foldlM Lean.setOptionFromString' Lean.Options.empty |>.run +def createCoreContext (options: Array String): IO Core.Context := do + let options? ← options.foldlM setOptionFromString' Options.empty |>.run let options ← match options? with | .ok options => pure options | .error e => throw $ IO.userError s!"Options cannot be parsed: {e}" return { - currNamespace := Lean.Name.str .anonymous "Aniva" + currNamespace := Name.str .anonymous "Aniva" openDecls := [], -- No 'open' directives needed fileName := "", fileMap := { source := "", positions := #[0] }, @@ -71,7 +71,7 @@ def createCoreContext (options: Array String): IO Lean.Core.Context := do /-- Creates a Core.State object needed to run all monads -/ @[export pantograph_create_core_state] -def createCoreState (imports: Array String): IO Lean.Core.State := do +def createCoreState (imports: Array String): IO Core.State := do let env ← Lean.importModules (imports := imports.map (λ str => { module := str.toName, runtimeOnly := false })) (opts := {}) @@ -79,33 +79,33 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do return { env := env } @[export pantograph_env_catalog_m] -def envCatalog: Lean.CoreM Protocol.EnvCatalogResult := +def envCatalog: CoreM Protocol.EnvCatalogResult := Environment.catalog ({}: Protocol.EnvCatalog) @[export pantograph_env_inspect_m] def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options): - Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := + CoreM (Protocol.CR Protocol.EnvInspectResult) := Environment.inspect ({ name, value? := .some value, dependency?:= .some dependency }: Protocol.EnvInspect) options @[export pantograph_env_add_m] def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool): - Lean.CoreM (Protocol.CR Protocol.EnvAddResult) := + CoreM (Protocol.CR Protocol.EnvAddResult) := Environment.addDecl { name, type, value, isTheorem } -def parseElabType (type: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do - let env ← Lean.MonadEnv.getEnv +def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do + let env ← MonadEnv.getEnv let syn ← match parseTerm env type with | .error str => return .error $ errorI "parsing" str | .ok syn => pure syn match ← elabType syn with | .error str => return .error $ errorI "elab" str - | .ok expr => return .ok (← Lean.instantiateMVars expr) + | .ok expr => return .ok (← instantiateMVars expr) /-- This must be a TermElabM since the parsed expr contains extra information -/ -def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do - let env ← Lean.MonadEnv.getEnv +def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do + let env ← MonadEnv.getEnv let expectedType? ← match ← expectedType?.mapM parseElabType with | .none => pure $ .none | .some (.ok t) => pure $ .some t @@ -115,17 +115,17 @@ def parseElabExpr (expr: String) (expectedType?: Option String := .none): Lean.E | .ok syn => pure syn match ← elabTerm syn expectedType? with | .error str => return .error $ errorI "elab" str - | .ok expr => return .ok (← Lean.instantiateMVars expr) + | .ok expr => return .ok (← instantiateMVars expr) @[export pantograph_expr_echo_m] -def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&Protocol.Options): - Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := - runTermElabM do +def exprEcho (expr: String) (expectedType?: Option String := .none) (levels: Array String := #[]) (options: @&Protocol.Options := {}): + CoreM (Protocol.CR Protocol.ExprEchoResult) := + runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do let expr ← match ← parseElabExpr expr expectedType? with | .error e => return .error e | .ok expr => pure expr try - let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr) + let type ← unfoldAuxLemmas (← Meta.inferType expr) return .ok { type := (← serializeExpression options type), expr := (← serializeExpression options expr) @@ -134,38 +134,38 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @& return .error $ errorI "typing" (← exception.toMessageData.toString) @[export pantograph_goal_start_expr_m] -def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) := - runTermElabM do +def goalStartExpr (expr: String) (levels: Array String): CoreM (Protocol.CR GoalState) := + runTermElabM $ Elab.Term.withLevelNames (levels.toList.map (·.toName)) do let expr ← match ← parseElabType expr with | .error e => return .error e | .ok expr => pure $ expr return .ok $ ← GoalState.create expr @[export pantograph_goal_tactic_m] -def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult := +def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult := runTermElabM <| state.tryTactic goalId tactic @[export pantograph_goal_assign_m] -def goalAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult := +def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := runTermElabM <| state.tryAssign goalId expr @[export pantograph_goal_have_m] -def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := +def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryHave goalId binderName type @[export pantograph_goal_let_m] -def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): Lean.CoreM TacticResult := +def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := runTermElabM <| state.tryLet goalId binderName type @[export pantograph_goal_conv_m] -def goalConv (state: GoalState) (goalId: Nat): Lean.CoreM TacticResult := +def goalConv (state: GoalState) (goalId: Nat): CoreM TacticResult := runTermElabM <| state.conv goalId @[export pantograph_goal_conv_exit_m] -def goalConvExit (state: GoalState): Lean.CoreM TacticResult := +def goalConvExit (state: GoalState): CoreM TacticResult := runTermElabM <| state.convExit @[export pantograph_goal_calc_m] -def goalCalc (state: GoalState) (goalId: Nat) (pred: String): Lean.CoreM TacticResult := +def goalCalc (state: GoalState) (goalId: Nat) (pred: String): CoreM TacticResult := runTermElabM <| state.tryCalc goalId pred @[export pantograph_goal_focus] @@ -181,11 +181,11 @@ def goalContinue (target: GoalState) (branch: GoalState): Except String GoalStat target.continue branch @[export pantograph_goal_serialize_m] -def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) := +def goalSerialize (state: GoalState) (options: @&Protocol.Options): CoreM (Array Protocol.Goal) := runMetaM <| state.serializeGoals (parent := .none) options @[export pantograph_goal_print_m] -def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Protocol.GoalPrintResult := +def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.GoalPrintResult := runMetaM do state.restoreMetaM return { diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 17618fc..0d5da7e 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -101,6 +101,8 @@ structure StatResult where structure ExprEcho where expr: String type?: Option String + -- universe levels + levels: Option (Array String) := .none deriving Lean.FromJson structure ExprEchoResult where expr: Expression @@ -198,6 +200,8 @@ abbrev OptionsPrintResult := Options structure GoalStart where -- Only one of the fields below may be populated. expr: Option String -- Directly parse in an expression + -- universe levels + levels: Option (Array String) := .none copyFrom: Option String -- Copy the type from a theorem in the environment deriving Lean.FromJson structure GoalStartResult where diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 950818e..8c16a01 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -1,5 +1,7 @@ /- -All serialisation functions +All serialisation functions; +This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without +using `Scope`s. -/ import Lean diff --git a/README.md b/README.md index 508d026..c136337 100644 --- a/README.md +++ b/README.md @@ -82,8 +82,8 @@ where the application of `assumption` should lead to a failure. See `Pantograph/Protocol.lean` for a description of the parameters and return values in JSON. * `reset`: Delete all cached expressions and proof trees * `stat`: Display resource usage -* `expr.echo {"expr": , "type": }`: Determine the - type of an expression and format it +* `expr.echo {"expr": , "type": , ["levels": []]}`: Determine the + type of an expression and format it. * `env.catalog`: Display a list of all safe Lean symbols in the current environment * `env.inspect {"name": , "value": }`: Show the type and package of a given symbol; If value flag is set, the value is printed or hidden. By default @@ -91,7 +91,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va * `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` * `options.print`: Display the current set of options -* `goal.start {["name": ], ["expr": ], ["copyFrom": ]}`: +* `goal.start {["name": ], ["expr": ], ["levels": []], ["copyFrom": ]}`: Start a new proof from a given expression or symbol * `goal.tactic {"stateId": , "goalId": , ...}`: Execute a tactic string on a given goal. The tactic is supplied as additional key-value pairs in one of the following formats: diff --git a/Test/Integration.lean b/Test/Integration.lean index 29cb82d..a9ced23 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -35,7 +35,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d def test_elab : IO LSpec.TestSeq := subroutine_runner [ subroutine_step "expr.echo" - [("expr", .str "λ {α : Sort (u + 1)} => List α")] + [("expr", .str "λ {α : Sort (u + 1)} => List α"), ("levels", .arr #["u"])] (Lean.toJson ({ type := { pp? := .some "{α : Type u} → Type u" }, expr := { pp? := .some "fun {α} => List α" } diff --git a/Test/Serial.lean b/Test/Serial.lean index f55c18f..8819378 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -47,23 +47,26 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do return LSpec.TestSeq.append suites test) LSpec.TestSeq.done def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do - let entries: List (String × String) := [ - ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), - ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), + let entries: List (String × (List Name) × String) := [ + ("λ x: Nat × Bool => x.1", [], "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), + ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), -- This tests `autoBoundImplicit` - ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), + ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"), + ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :implicit)"), ] - let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do - let env ← MonadEnv.getEnv - let s ← match parseTerm env source with - | .ok s => pure s - | .error e => return parseFailure e - let expr ← match (← elabTerm s) with - | .ok expr => pure expr - | .error e => return elabFailure e - let test := LSpec.check source ((← serializeExpressionSexp expr) = target) - return LSpec.TestSeq.append suites test) LSpec.TestSeq.done - runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext) + entries.foldlM (λ suites (source, levels, target) => + let termElabM := do + let env ← MonadEnv.getEnv + let s ← match parseTerm env source with + | .ok s => pure s + | .error e => return parseFailure e + let expr ← match (← elabTerm s) with + | .ok expr => pure expr + | .error e => return elabFailure e + return LSpec.check source ((← serializeExpressionSexp expr) = target) + let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext) + return LSpec.TestSeq.append suites (← runMetaMSeq env metaM)) + LSpec.TestSeq.done def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do let entries: List (Expr × String) := [ -- 2.44.1