feat: Instantiation tests #52

Merged
aniva merged 2 commits from io/serial into dev 2024-03-30 00:08:33 -07:00
5 changed files with 39 additions and 15 deletions
Showing only changes of commit 90f7f251e9 - Show all commits

View File

@ -225,6 +225,10 @@ protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
let expr := goalState.mctx.eAssignment.find! parent let expr := goalState.mctx.eAssignment.find! parent
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr) let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
return 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 end Pantograph

View File

@ -243,7 +243,7 @@ structure GoalPrintResult where
-- The root expression -- The root expression
root?: Option Expression := .none root?: Option Expression := .none
-- The filling expression of the parent goal -- The filling expression of the parent goal
parent?: Option Expression := .none parent?: Option Expression
deriving Lean.ToJson deriving Lean.ToJson
-- Diagnostic Options, not available in REPL -- Diagnostic Options, not available in REPL

View File

@ -97,6 +97,12 @@ def test_tactic : IO LSpec.TestSeq :=
goals? := #[goal1], goals? := #[goal1],
}: }:
Protocol.GoalTacticResult)), Protocol.GoalTacticResult)),
subroutine_step "goal.print"
[("stateId", .num 1)]
(Lean.toJson ({
parent? := .some { pp? := .some "fun x => ?m.11 x" },
}:
Protocol.GoalPrintResult)),
subroutine_step "goal.tactic" subroutine_step "goal.tactic"
[("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")] [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
(Lean.toJson ({ (Lean.toJson ({

View File

@ -5,11 +5,11 @@
"nixpkgs-lib": "nixpkgs-lib" "nixpkgs-lib": "nixpkgs-lib"
}, },
"locked": { "locked": {
"lastModified": 1696343447, "lastModified": 1709336216,
"narHash": "sha256-B2xAZKLkkeRFG5XcHHSXXcP7To9Xzr59KXeZiRf4vdQ=", "narHash": "sha256-Dt/wOWeW6Sqm11Yh+2+t0dfEWxoMxGBvv3JpIocFl9E=",
"owner": "hercules-ci", "owner": "hercules-ci",
"repo": "flake-parts", "repo": "flake-parts",
"rev": "c9afaba3dfa4085dbd2ccb38dfade5141e33d9d4", "rev": "f7b3c975cf067e56e7cda6cb098ebe3fb4d74ca2",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -38,9 +38,7 @@
"flake-utils": "flake-utils", "flake-utils": "flake-utils",
"lean4-mode": "lean4-mode", "lean4-mode": "lean4-mode",
"nix": "nix", "nix": "nix",
"nixpkgs": [ "nixpkgs": "nixpkgs_2",
"nixpkgs"
],
"nixpkgs-old": "nixpkgs-old" "nixpkgs-old": "nixpkgs-old"
}, },
"locked": { "locked": {
@ -146,11 +144,11 @@
"nixpkgs-lib": { "nixpkgs-lib": {
"locked": { "locked": {
"dir": "lib", "dir": "lib",
"lastModified": 1696019113, "lastModified": 1709237383,
"narHash": "sha256-X3+DKYWJm93DRSdC5M6K5hLqzSya9BjibtBsuARoPco=", "narHash": "sha256-cy6ArO4k5qTx+l5o+0mL9f5fa86tYUX3ozE1S+Txlds=",
"owner": "NixOS", "owner": "NixOS",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "f5892ddac112a1e9b3612c39af1b72987ee5783a", "rev": "1536926ef5621b09bba54035ae2bb6d806d72ac8",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -196,11 +194,27 @@
}, },
"nixpkgs_2": { "nixpkgs_2": {
"locked": { "locked": {
"lastModified": 1697456312, "lastModified": 1686089707,
"narHash": "sha256-roiSnrqb5r+ehnKCauPLugoU8S36KgmWraHgRqVYndo=", "narHash": "sha256-LTNlJcru2qJ0XhlhG9Acp5KyjB774Pza3tRH0pKIb3o=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "af21c31b2a1ec5d361ed8050edd0303c31306397",
"type": "github"
},
"original": {
"owner": "NixOS",
"ref": "nixpkgs-unstable",
"repo": "nixpkgs",
"type": "github"
}
},
"nixpkgs_3": {
"locked": {
"lastModified": 1711703276,
"narHash": "sha256-iMUFArF0WCatKK6RzfUJknjem0H9m4KgorO/p3Dopkk=",
"owner": "nixos", "owner": "nixos",
"repo": "nixpkgs", "repo": "nixpkgs",
"rev": "ca012a02bf8327be9e488546faecae5e05d7d749", "rev": "d8fe5e6c92d0d190646fb9f1056741a229980089",
"type": "github" "type": "github"
}, },
"original": { "original": {
@ -215,7 +229,7 @@
"flake-parts": "flake-parts", "flake-parts": "flake-parts",
"lean": "lean", "lean": "lean",
"lspec": "lspec", "lspec": "lspec",
"nixpkgs": "nixpkgs_2" "nixpkgs": "nixpkgs_3"
} }
} }
}, },

View File

@ -6,7 +6,7 @@
flake-parts.url = "github:hercules-ci/flake-parts"; flake-parts.url = "github:hercules-ci/flake-parts";
lean = { lean = {
url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2"; url = "github:leanprover/lean4?ref=b4caee80a3dfc5c9619d88b16c40cc3db90da4e2";
inputs.nixpkgs.follows = "nixpkgs"; # Do not follow input's nixpkgs since it could cause build failures
}; };
lspec = { lspec = {
url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114"; url = "github:lurk-lab/LSpec?ref=3388be5a1d1390594a74ec469fd54a5d84ff6114";