feat: Condensed interface #85

Merged
aniva merged 27 commits from serial/expr into dev 2024-08-15 22:41:59 -07:00
2 changed files with 18 additions and 6 deletions
Showing only changes of commit 651afa75f4 - Show all commits

View File

@ -66,11 +66,19 @@ def elabState (levelNames: Array Name): Elab.Term.State := {
end Condensed end Condensed
-- Get the list of visible (by default) free variables from a goal
@[export pantograph_visible_fvars_of_mvar]
protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
let mvarDecl ← mctx.findDecl? mvarId
let lctx := mvarDecl.lctx
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
| some decl => if decl.isAuxDecl decl.isImplementationDetail then r else r.push decl.fvarId
| none => r
@[export pantograph_to_condensed_goal_m] @[export pantograph_to_condensed_goal_m]
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
let options : Protocol.Options := {} let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions)
let ppAuxDecls := options.printAuxDecls let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
let ppImplDetailHyps := options.printImplementationDetailHyps
let mvarDecl ← mvarId.getDecl let mvarDecl ← mvarId.getDecl
let lctx := mvarDecl.lctx let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }

View File

@ -69,10 +69,14 @@ protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): O
protected def GoalState.metaState (state: GoalState): Meta.State := protected def GoalState.metaState (state: GoalState): Meta.State :=
state.savedState.term.meta.meta state.savedState.term.meta.meta
@[export pantograph_goal_state_fvar_names_of_goal] -- Get the list of visible free variables from a goal
protected def GoalState.fvarNamesOfGoal (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do @[export pantograph_goal_state_visible_fvars]
protected def GoalState.visibleFVars (state: GoalState) (mvarId: MVarId): Option (Array FVarId) := do
let mvarDecl ← state.mctx.findDecl? mvarId let mvarDecl ← state.mctx.findDecl? mvarId
return mvarDecl.lctx.getFVarIds let lctx := mvarDecl.lctx
return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
| some decl => if decl.isAuxDecl decl.isImplementationDetail then r else r.push decl.fvarId
| none => r
protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
mvarId.withContext m |>.run' (← read) state.metaState mvarId.withContext m |>.run' (← read) state.metaState