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 25 additions and 8 deletions
Showing only changes of commit 3ca52517ab - Show all commits

View File

@ -4,6 +4,26 @@ open Lean
namespace Pantograph namespace Pantograph
structure ProjectionApplication where
projector: Name
numParams: Nat
inner: Expr
@[export pantograph_expr_proj_to_app]
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
let (typeName, idx, inner) := match e with
| .proj typeName idx inner => (typeName, idx, inner)
| _ => panic! "Argument must be proj"
let ctor := getStructureCtor env typeName
let fieldName := getStructureFields env typeName |>.get! idx
let projector := getProjFnForField? env typeName fieldName |>.get!
{
projector,
numParams := ctor.numParams,
inner,
}
def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/ /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/

View File

@ -168,15 +168,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
-- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
-- It may become necessary to incorporate the metadata. -- It may become necessary to incorporate the metadata.
self inner self inner
| .proj typeName idx inner => do | .proj _ _ _ => do
let env ← getEnv let env ← getEnv
let ctor := getStructureCtor env typeName let projApp := exprProjToApp env e
let fieldName := getStructureFields env typeName |>.get! idx let autos := String.intercalate " " (List.replicate projApp.numParams "_")
let projectorName := getProjFnForField? env typeName fieldName |>.get! let inner ← self projApp.inner
pure s!"((:c {projApp.projector}) {autos} {inner})"
let autos := String.intercalate " " (List.replicate ctor.numParams "_")
let inner ← self inner
pure s!"((:c {projectorName}) {autos} {inner})"
-- Elides all unhygenic names -- Elides all unhygenic names
binderInfoSexp : Lean.BinderInfo → String binderInfoSexp : Lean.BinderInfo → String
| .default => "" | .default => ""