From c83af044b4627eda5a12135b1ba197bea5ff3da2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 11 Mar 2024 21:31:59 -0700 Subject: [PATCH] fix: Pass options by reference --- Pantograph/Environment.lean | 2 +- Pantograph/Library.lean | 4 ++-- Pantograph/Serial.lean | 8 ++++++-- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index df0bc7f..f37225f 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -37,7 +37,7 @@ def catalog (_: Protocol.EnvCatalog): CoreM Protocol.EnvCatalogResult := do | .some x => acc.push x | .none => acc) 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 name := args.name.toName let info? := env.find? name diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index b731fb3..d72fd3a 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -98,7 +98,7 @@ def mkOptions } @[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) := Environment.inspect ({ 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) @[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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 547b3dc..213ae6d 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -172,7 +172,7 @@ def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol } /-- 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 -- Options for printing; See Meta.ppGoal for details let showLetValues := true @@ -242,7 +242,11 @@ def serialize_goal (options: Protocol.Options) (goal: MVarId) (mvarDecl: Metavar where 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 let goals := state.goals.toArray let parentDecl? := parent.bind (λ parentState =>