diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index 1e4bc06..f954f0d 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -51,7 +51,7 @@ structure Variable where /-- The name displayed to the user -/ userName: String /-- Does the name contain a dagger -/ - isInaccessible?: Option Bool := .none + isInaccessible?: Option Bool := .some false type?: Option Expression := .none value?: Option Expression := .none deriving Lean.ToJson diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index b353785..9f54bbb 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -215,11 +215,13 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava return { name := ofName fvarId.name, userName:= ofName userName.simpMacroScopes, + isInaccessible? := .some userName.isInaccessibleUserName } | .ldecl _ fvarId userName _ _ _ _ => do return { name := ofName fvarId.name, userName := toString userName.simpMacroScopes, + isInaccessible? := .some userName.isInaccessibleUserName } let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do match localDecl with diff --git a/Pantograph/Tactic/Assign.lean b/Pantograph/Tactic/Assign.lean index af76bfd..ea08c48 100644 --- a/Pantograph/Tactic/Assign.lean +++ b/Pantograph/Tactic/Assign.lean @@ -19,9 +19,12 @@ def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do nextGoals.toList.filterM (not <$> ·.isAssigned) def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do - let goalType ← Elab.Tactic.getMainTarget - let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType) - let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr + let target ← Elab.Tactic.getMainTarget + let (expr, nextGoals) ← Elab.Tactic.elabTermWithHoles stx + (expectedType? := .some target) + (tagSuffix := .anonymous ) + (allowNaturalHoles := true) + (← Elab.Tactic.getMainGoal).assign expr Elab.Tactic.setGoals nextGoals diff --git a/Pantograph/Tactic/Prograde.lean b/Pantograph/Tactic/Prograde.lean index dd34684..c67102c 100644 --- a/Pantograph/Tactic/Prograde.lean +++ b/Pantograph/Tactic/Prograde.lean @@ -64,13 +64,14 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult let lctx ← MonadLCtx.getLCtx -- The branch goal inherits the same context, but with a different type - let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type + let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type (userName := binderName) assert! ¬ type.hasLooseBVars - let upstreamType := .letE binderName type mvarBranch (← mvarId.getType) false - let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) - upstreamType (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag) - mvarId.assign mvarUpstream + let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do + let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) + (type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag) + mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false) + pure mvarUpstream return { main := mvarUpstream.mvarId!, diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 3849b44..65e43a3 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -198,15 +198,16 @@ def test_proposition_generation: TestM Unit := do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) = - #[.some "∀ (x : Nat), ?m.29 x"]) + #[.some "?m.29 x"]) addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone - let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with + let assign := "Eq.refl x" + let state3 ← match ← state2.tryAssign (goalId := 0) (expr := assign) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check ":= Eq.refl" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = + addTest $ LSpec.check s!":= {assign}" ((← state3.serializeGoals (options := ← read)).map (·.target.pp?) = #[]) addTest $ LSpec.test "(3 root)" state3.rootExpr?.isSome diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 8e0f78d..d138e4c 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -175,7 +175,7 @@ def test_delta_variable: TestM Unit := do vars := (nameType.map fun x => ({ userName := x.fst, type? := x.snd.map (λ type => { pp? := type }), - isInaccessible? := x.snd.map (λ _ => false) + isInaccessible? := .some false, })).toArray } @@ -544,83 +544,6 @@ def test_calc: TestM Unit := do ("h1", "a + b = b + c"), ("h2", "b + c = c + d")] ++ free buildGoal free target userName? -def test_let (specialized: Bool): TestM Unit := do - let state? ← startProof (.expr "∀ (a: Nat) (p: Prop), p → p ∨ ¬p") - let state0 ← match state? with - | .some state => pure state - | .none => do - addTest $ assertUnreachable "Goal could not parse" - return () - let tactic := "intro a p h" - 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) = - #[interiorGoal [] "p ∨ ¬p"]) - - - let letType := "Nat" - let expr := s!"let b: {letType} := _; _" - let result2 ← match specialized with - | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) - | false => state1.tryAssign (goalId := 0) (expr := expr) - let state2 ← match result2 with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let serializedState2 ← state2.serializeGoals (options := ← read) - addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) = - #[ - interiorGoal [] letType, - interiorGoal [] "let b := ?m.20;\np ∨ ¬p" - ]) - -- Check that the goal mvar ids match up - 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 - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.check tactic ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) = #[]) - - let state3r ← match state3.continue state2 with - | .error msg => do - addTest $ assertUnreachable $ msg - return () - | .ok state => pure state - addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals (options := ← read)).map (·.devolatilize) = - #[interiorGoal [] "let b := a;\np ∨ ¬p"]) - - let tactic := "exact h" - match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with - | .failure #[message] => - addTest $ LSpec.check tactic (message = "type mismatch\n h\nhas type\n p : Prop\nbut is expected to have type\n let b := a;\n p ∨ ¬p : Prop") - | other => do - addTest $ assertUnreachable $ other.toString - - let tactic := "intro b" - let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - let tactic := "exact Or.inl h" - let state5 ← match ← state4.tryTactic (goalId := 0) (tactic := tactic) with - | .success state => pure state - | other => do - addTest $ assertUnreachable $ other.toString - return () - addTest $ LSpec.test "(5 root)" state5.rootExpr?.isSome - where - interiorGoal (free: List (String × String)) (target: String) (userName?: Option String := .none) := - 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 @@ -795,8 +718,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Or.comm", test_or_comm), ("conv", test_conv), ("calc", test_calc), - ("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), ] diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean index 6b7cd44..5b20011 100644 --- a/Test/Tactic/Prograde.lean +++ b/Test/Tactic/Prograde.lean @@ -162,12 +162,105 @@ def test_proof_have : TestT Elab.TermElabM Unit := do addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome +def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do + let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))" + let state0 ← GoalState.create rootExpr + let tactic := "intro a p h" + 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).map (·.devolatilize) = + #[{ + target := { pp? := .some mainTarget }, + vars := interiorVars, + }]) + + let letType := "Nat" + let expr := s!"let b: {letType} := _; _" + let result2 ← match specialized with + | true => state1.tryLet (goalId := 0) (binderName := "b") (type := letType) + | false => state1.tryAssign (goalId := 0) (expr := expr) + let state2 ← match result2 with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + let serializedState2 ← state2.serializeGoals + let letBindName := if specialized then "b" else "_1" + addTest $ LSpec.check expr (serializedState2.map (·.devolatilize) = + #[{ + target := { pp? := .some letType }, + vars := interiorVars, + userName? := .some letBindName + }, + { + target := { pp? := .some mainTarget }, + vars := interiorVars ++ #[{ + userName := "b", + type? := .some { pp? := .some letType }, + value? := .some { pp? := .some s!"?{letBindName}" }, + }], + userName? := if specialized then .none else .some "_2", + } + ]) + + let tactic := "exact 1" + let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check tactic ((← state3.serializeGoals).map (·.devolatilize) = #[]) + + let state3r ← match state3.continue state2 with + | .error msg => do + addTest $ assertUnreachable $ msg + return () + | .ok state => pure state + addTest $ LSpec.check "(continue)" ((← state3r.serializeGoals).map (·.devolatilize) = + #[ + { + target := { pp? := .some mainTarget }, + vars := interiorVars ++ #[{ + userName := "b", + type? := .some { pp? := .some "Nat" }, + value? := .some { pp? := .some "1" }, + }], + userName? := if specialized then .none else .some "_2", + } + ]) + + let tactic := "exact h" + match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .failure #[message] => + addTest $ LSpec.check tactic (message = s!"type mismatch\n h\nhas type\n a : Prop\nbut is expected to have type\n {mainTarget} : Prop") + | other => do + addTest $ assertUnreachable $ other.toString + + let tactic := "exact Or.inl (Or.inl h)" + let state4 ← match ← state3r.tryTactic (goalId := 0) (tactic := tactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.test "(4 root)" state4.rootExpr?.isSome + where + mainTarget := "(a ∨ p) ∨ a ∨ p" + interiorVars: Array Protocol.Variable := #[ + { userName := "a", type? := .some { pp? := .some "Prop" }, }, + { userName := "p", type? := .some { pp? := .some "Prop" }, }, + { userName := "h", type? := .some { pp? := .some "a" }, } + ] def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("eval", test_eval), ("Proof eval", test_proof_eval), ("Proof have", test_proof_have), + ("let via assign", test_let false), + ("let via tryLet", test_let true), ] |>.map (λ (name, t) => (name, runTestTermElabM env t)) end Pantograph.Test.Tactic.Prograde