From 0d570276816185df141518e66a74b5f9292975c3 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 8 Nov 2024 13:05:48 -0800 Subject: [PATCH] refactor: Merge Condensed into Delate --- Pantograph.lean | 1 - Pantograph/Condensed.lean | 95 --------------------------------------- Pantograph/Delate.lean | 85 ++++++++++++++++++++++++++++++++++- Pantograph/Library.lean | 1 - Test/Common.lean | 1 - 5 files changed, 84 insertions(+), 99 deletions(-) delete mode 100644 Pantograph/Condensed.lean diff --git a/Pantograph.lean b/Pantograph.lean index 72c4906..bad5f2a 100644 --- a/Pantograph.lean +++ b/Pantograph.lean @@ -1,4 +1,3 @@ -import Pantograph.Condensed import Pantograph.Environment import Pantograph.Frontend import Pantograph.Goal diff --git a/Pantograph/Condensed.lean b/Pantograph/Condensed.lean deleted file mode 100644 index 125b69c..0000000 --- a/Pantograph/Condensed.lean +++ /dev/null @@ -1,95 +0,0 @@ -/- structures for FFI based interface -/ -import Lean -import Pantograph.Goal -import Pantograph.Expr - -open Lean - -namespace Pantograph -namespace Condensed - --- Mirrors Lean's LocalDecl -structure LocalDecl where - -- Default value is for testing - fvarId: FVarId := { name := .anonymous } - userName: Name - - -- Normalized expression - type : Expr - value? : Option Expr := .none - -structure Goal where - mvarId: MVarId := { name := .anonymous } - userName: Name := .anonymous - context: Array LocalDecl - target: Expr - -@[export pantograph_goal_is_lhs] -def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome - --- Functions for creating contexts and states -@[export pantograph_elab_context] -def elabContext: Elab.Term.Context := { - errToSorry := false - } - -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] -def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do - let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions) - let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions) - let mvarDecl ← mvarId.getDecl - let lctx := mvarDecl.lctx - let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } - Meta.withLCtx lctx mvarDecl.localInstances do - let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do - match localDecl with - | .cdecl _ fvarId userName type _ _ => - let type ← instantiate type - return { fvarId, userName, type } - | .ldecl _ fvarId userName type value _ _ => do - let userName := userName.simpMacroScopes - let type ← instantiate type - let value ← instantiate value - return { fvarId, userName, type, value? := .some value } - let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do - let skip := !ppAuxDecls && localDecl.isAuxDecl || - !ppImplDetailHyps && localDecl.isImplementationDetail - if skip then - return acc - else - let var ← ppVar localDecl - return var::acc - return { - mvarId, - userName := mvarDecl.userName, - context := vars.reverse.toArray, - target := ← instantiate mvarDecl.type - } - where - instantiate := instantiateAll - -@[export pantograph_goal_state_to_condensed_m] -protected def GoalState.toCondensed (state: GoalState): - CoreM (Array Condensed.Goal):= do - let metaM := do - let goals := state.goals.toArray - goals.mapM fun goal => do - match state.mctx.findDecl? goal with - | .some _ => - let serializedGoal ← toCondensedGoal goal - pure serializedGoal - | .none => throwError s!"Metavariable does not exist in context {goal.name}" - metaM.run' (s := state.savedState.term.meta.meta) - -end Pantograph diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 3a9efa4..c5954f0 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -4,7 +4,6 @@ This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without using `Scope`s. -/ import Lean -import Pantograph.Condensed import Pantograph.Expr import Pantograph.Goal import Pantograph.Protocol @@ -14,7 +13,91 @@ open Lean -- Symbol processing functions -- namespace Pantograph +namespace Condensed +-- Mirrors Lean's LocalDecl +structure LocalDecl where + -- Default value is for testing + fvarId: FVarId := { name := .anonymous } + userName: Name + + -- Normalized expression + type : Expr + value? : Option Expr := .none + +structure Goal where + mvarId: MVarId := { name := .anonymous } + userName: Name := .anonymous + context: Array LocalDecl + target: Expr + +@[export pantograph_goal_is_lhs] +def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome + +-- Functions for creating contexts and states +@[export pantograph_elab_context] +def elabContext: Elab.Term.Context := { + errToSorry := false + } + +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] +def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do + let ppAuxDecls := Meta.pp.auxDecls.get (← getOptions) + let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions) + let mvarDecl ← mvarId.getDecl + let lctx := mvarDecl.lctx + let lctx := lctx.sanitizeNames.run' { options := (← getOptions) } + Meta.withLCtx lctx mvarDecl.localInstances do + let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do + match localDecl with + | .cdecl _ fvarId userName type _ _ => + let type ← instantiate type + return { fvarId, userName, type } + | .ldecl _ fvarId userName type value _ _ => do + let userName := userName.simpMacroScopes + let type ← instantiate type + let value ← instantiate value + return { fvarId, userName, type, value? := .some value } + let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do + let skip := !ppAuxDecls && localDecl.isAuxDecl || + !ppImplDetailHyps && localDecl.isImplementationDetail + if skip then + return acc + else + let var ← ppVar localDecl + return var::acc + return { + mvarId, + userName := mvarDecl.userName, + context := vars.reverse.toArray, + target := ← instantiate mvarDecl.type + } + where + instantiate := instantiateAll + +@[export pantograph_goal_state_to_condensed_m] +protected def GoalState.toCondensed (state: GoalState): + CoreM (Array Condensed.Goal):= do + let metaM := do + let goals := state.goals.toArray + goals.mapM fun goal => do + match state.mctx.findDecl? goal with + | .some _ => + let serializedGoal ← toCondensedGoal goal + pure serializedGoal + | .none => throwError s!"Metavariable does not exist in context {goal.name}" + metaM.run' (s := state.savedState.term.meta.meta) --- Input Functions --- diff --git a/Pantograph/Library.lean b/Pantograph/Library.lean index 8a5db24..a082f4b 100644 --- a/Pantograph/Library.lean +++ b/Pantograph/Library.lean @@ -1,4 +1,3 @@ -import Pantograph.Condensed import Pantograph.Environment import Pantograph.Goal import Pantograph.Protocol diff --git a/Test/Common.lean b/Test/Common.lean index 2d98aca..3670cba 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -1,7 +1,6 @@ import Pantograph.Goal import Pantograph.Library import Pantograph.Protocol -import Pantograph.Condensed import Lean import LSpec