feat: Condensed interface

This commit is contained in:
Leni Aniva 2024-06-25 15:13:58 -04:00
parent 472cd54868
commit ffbea41f62
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 104 additions and 3 deletions

42
Pantograph/Condensed.lean Normal file
View File

@ -0,0 +1,42 @@
/- structures for FFI based interface -/
import Lean
open Lean
namespace Pantograph.Condensed
/-
These two functions are for user defiend names. For internal names such as
`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to
construct hash maps for Lean names.
-/
@[export pantograph_str_to_name]
def strToName (s: String) : Name := s.toName
@[export pantograph_name_to_str]
def nameToStr (s: String) : Name := s.toName
@[export pantograph_name_is_inaccessible]
def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
-- 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
end Pantograph.Condensed

View File

@ -4,10 +4,10 @@ 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.Protocol
import Pantograph.Goal
import Pantograph.Protocol
open Lean
@ -201,6 +201,55 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
dependentMVars?,
}
@[export pantograph_to_condensed_goal]
def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
let options: Protocol.Options := {}
let ppAuxDecls := options.printAuxDecls
let ppImplDetailHyps := options.printImplementationDetailHyps
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]
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)
/-- Adapted from ppGoal -/
def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
: MetaM Protocol.Goal := do
@ -214,7 +263,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
match localDecl with
| .cdecl _ fvarId userName _ _ _ =>
let userName := userName.simpMacroScopes
return {
name := ofName fvarId.name,
userName:= ofName userName.simpMacroScopes,

View File

@ -8,6 +8,17 @@ open Lean
namespace Pantograph
deriving instance Repr for Expr
-- Use strict equality check for expressions
--instance : BEq Expr := ⟨Expr.equal⟩
instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
if h : Expr.equal x y then
.isTrue h
else
.isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
-- Auxiliary functions
namespace Protocol
def Goal.devolatilizeVars (goal: Goal): Goal :=