aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

chore: Version 0.3 #136

Open
aniva wants to merge 487 commits from dev into main
pull from: dev
merge into: aniva:main
Conversation 0 Commits 487 Files Changed 52 +34 -26
7 changed files with 34 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit c3076cbb7d - Show all commits

5
Pantograph/Expr.lean
View File

@ -1,4 +1,5 @@
import Lean
import Std.Data.HashMap
open Lean
@ -144,10 +145,10 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
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 fvarArgMap: Std.HashMap FVarId Expr := Std.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
let a := fvarArgMap[fvarId]?
return acc ++ [(fvarId, a)]
assert! decl.fvars.all (λ fvar => mvarDecl.lctx.findFVar? fvar |>.isSome)

13
Pantograph/Frontend/MetaTranslate.lean
View File

@ -1,4 +1,5 @@
import Lean.Meta
import Std.Data.HashMap
open Lean
@ -10,12 +11,12 @@ structure Context where
sourceMCtx : MetavarContext := {}
sourceLCtx : LocalContext := {}
abbrev FVarMap := HashMap FVarId FVarId
abbrev FVarMap := Std.HashMap FVarId FVarId
structure State where
-- Stores mapping from old to new mvar/fvars
mvarMap: HashMap MVarId MVarId := {}
fvarMap: HashMap FVarId FVarId := {}
mvarMap: Std.HashMap MVarId MVarId := {}
fvarMap: Std.HashMap FVarId FVarId := {}
/-
Monadic state for translating a frozen meta state. The underlying `MetaM`
@ -46,13 +47,13 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
let state ← get
match e with
| .fvar fvarId =>
let .some fvarId' := state.fvarMap.find? fvarId | panic! s!"FVar id not registered: {fvarId.name}"
let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}"
assert! (← getLCtx).contains fvarId'
return .done $ .fvar fvarId'
| .mvar mvarId => do
assert! !(sourceMCtx.dAssignment.contains mvarId)
assert! !(sourceMCtx.eAssignment.contains mvarId)
match state.mvarMap.find? mvarId with
match state.mvarMap[mvarId]? with
| .some mvarId' => do
return .done $ .mvar mvarId'
| .none => do
@ -92,7 +93,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
) lctx
partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
if let .some mvarId' := (← get).mvarMap.find? srcMVarId then
if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
return mvarId'
let mvar ← Meta.withLCtx .empty #[] do
let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!

25
Repl.lean
View File

@ -1,4 +1,4 @@
import Lean.Data.HashMap
import Std.Data.HashMap
import Pantograph
namespace Pantograph.Repl
@ -10,7 +10,7 @@ structure Context where
structure State where
options: Protocol.Options := {}
nextId: Nat := 0
goalStates: Lean.HashMap Nat GoalState := Lean.HashMap.empty
goalStates: Std.HashMap Nat GoalState := Std.HashMap.empty
/-- Main state monad for executing commands -/
abbrev MainM := ReaderT Context (StateT State Lean.CoreM)
@ -66,7 +66,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
let state ← get
let nGoals := state.goalStates.size
set { state with nextId := 0, goalStates := Lean.HashMap.empty }
set { state with nextId := 0, goalStates := .empty }
return .ok { nGoals }
stat (_: Protocol.Stat): MainM (CR Protocol.StatResult) := do
let state ← get
@ -119,7 +119,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { stateId, root := goalState.root.name.toString }
goal_tactic (args: Protocol.GoalTactic): MainM (CR Protocol.GoalTacticResult) := do
let state ← get
let .some goalState := state.goalStates.find? args.stateId |
let .some goalState := state.goalStates[args.stateId]? |
return .error $ errorIndex s!"Invalid state index {args.stateId}"
let .some goal := goalState.goals.get? args.goalId |
return .error $ errorIndex s!"Invalid goal index {args.goalId}"
@ -146,12 +146,15 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .ok (.success nextGoalState) => do
let nextGoalState ← match state.options.automaticMode, args.conv? with
| true, .none => do
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) | throwError "Resuming known goals"
let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
throwError "Resuming known goals"
pure result
| true, .some true => pure nextGoalState
| true, .some false => do
let .some (_, _, dormantGoals) := goalState.convMVar? | throwError "If conv exit succeeded this should not fail"
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) | throwError "Resuming known goals"
let .some (_, _, dormantGoals) := goalState.convMVar? |
throwError "If conv exit succeeded this should not fail"
let .ok result := nextGoalState.resume (nextGoalState.goals ++ dormantGoals) |
throwError "Resuming known goals"
pure result
| false, _ => pure nextGoalState
let nextStateId ← newGoalState nextGoalState
@ -168,10 +171,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok { tacticErrors? := .some messages }
goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do
let state ← get
let .some target := state.goalStates.find? args.target | return .error $ errorIndex s!"Invalid state index {args.target}"
let .some target := state.goalStates[args.target]? |
return .error $ errorIndex s!"Invalid state index {args.target}"
let nextState? ← match args.branch?, args.goals? with
| .some branchId, .none => do
match state.goalStates.find? branchId with
match state.goalStates[branchId]? with
| .none => return .error $ errorIndex s!"Invalid state index {branchId}"
| .some branch => pure $ target.continue branch
| .none, .some goals =>
@ -197,7 +201,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
return .ok {}
goal_print (args: Protocol.GoalPrint): MainM (CR Protocol.GoalPrintResult) := do
let state ← get
let .some goalState := state.goalStates.find? args.stateId | return .error $ errorIndex s!"Invalid state index {args.stateId}"
let .some goalState := state.goalStates[args.stateId]? |
return .error $ errorIndex s!"Invalid state index {args.stateId}"
let result ← runMetaInMainM <| goalPrint goalState state.options
return .ok result
frontend_process (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do

4
flake.nix
View File

@ -6,10 +6,10 @@
flake-parts.url = "github:hercules-ci/flake-parts";
lean = {
# Do not follow input's nixpkgs since it could cause build failures
url = "github:leanprover/lean4?ref=v4.10.0-rc1";
url = "github:leanprover/lean4?ref=v4.12.0";
};
lspec = {
url = "github:lurk-lab/LSpec?ref=8a51034d049c6a229d88dd62f490778a377eec06";
url = "github:lenianiva/LSpec?ref=c492cecd0bc473e2f9c8b94d545d02cc0056034f";
flake = false;
};
};

9
lake-manifest.json
View File

@ -1,13 +1,14 @@
{"version": 7,
{"version": "1.1.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/lurk-lab/LSpec.git",
[{"url": "https://github.com/lenianiva/LSpec.git",
"type": "git",
"subDir": null,
"rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"scope": "",
"rev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
"name": "LSpec",
"manifestFile": "lake-manifest.json",
"inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114",
"inputRev": "c492cecd0bc473e2f9c8b94d545d02cc0056034f",
"inherited": false,
"configFile": "lakefile.lean"}],
"name": "pantograph",

2
lakefile.lean
View File

@ -18,7 +18,7 @@ lean_exe repl {
}
require LSpec from git
"https://github.com/lurk-lab/LSpec.git" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114"
"https://github.com/lenianiva/LSpec.git" @ "c492cecd0bc473e2f9c8b94d545d02cc0056034f"
lean_lib Test {
}
@[test_driver]

2
lean-toolchain
View File

@ -1 +1 @@
leanprover/lean4:v4.10.0-rc1
leanprover/lean4:v4.12.0