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

fix: Pass options by reference

This commit is contained in:
Leni Aniva 2024-03-11 21:31:59 -07:00
parent 285cf0416a
commit c83af044b4
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 9 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Pantograph/Environment.lean
View File

@ -37,7 +37,7 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do
| .some x => acc.push x | .some x => acc.push x
| .none => acc) | .none => acc)
return { symbols := names } return { symbols := names }
def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let name := args.name.toName let name := args.name.toName
let info? := env.find? name let info? := env.find? name

4
Pantograph/Library.lean
View File

@ -98,7 +98,7 @@ def mkOptions
} }
@[export pantograph_env_inspect_m] @[export pantograph_env_inspect_m]
def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) := Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
Environment.inspect ({ Environment.inspect ({
name, value? := .some value, dependency?:= .some dependency name, value? := .some value, dependency?:= .some dependency
@ -162,7 +162,7 @@ def goalResume (target: GoalState) (goals: Array String): Except String GoalStat
target.resume (goals.map (λ n => { name := n.toName }) |>.toList) target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
@[export pantograph_goal_serialize_m] @[export pantograph_goal_serialize_m]
def goalSerialize (state: GoalState) (options: Protocol.Options): Lean.CoreM (Array Protocol.Goal) := def goalSerialize (state: GoalState) (options: @&Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
runMetaM <| state.serializeGoals (parent := .none) options runMetaM <| state.serializeGoals (parent := .none) options

8
Pantograph/Serial.lean
View File

@ -172,7 +172,7 @@ def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol
} }
/-- Adapted from ppGoal -/ /-- Adapted from ppGoal -/
def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Protocol.Goal := do : MetaM Protocol.Goal := do
-- Options for printing; See Meta.ppGoal for details -- Options for printing; See Meta.ppGoal for details
let showLetValues := true let showLetValues := true
@ -242,7 +242,11 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar
where where
of_name (n: Name) := name_to_ast n (sanitize := false) of_name (n: Name) := name_to_ast n (sanitize := false)
protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalState := .none) (options: Protocol.Options := {}): MetaM (Array Protocol.Goal):= do protected def GoalState.serializeGoals
(state: GoalState)
(parent: Option GoalState := .none)
(options: @&Protocol.Options := {}):
MetaM (Array Protocol.Goal):= do
state.restoreMetaM state.restoreMetaM
let goals := state.goals.toArray let goals := state.goals.toArray
let parentDecl? := parent.bind (λ parentState => let parentDecl? := parent.bind (λ parentState =>