Merge pull request 'fix: Panic in `exprProjToApp`' (#161) from bug/expr-proj-to-app-panic into dev

Reviewed-on: #161
This commit is contained in:
Leni Aniva 2025-01-24 15:05:04 -08:00
commit b67d3eccc4
2 changed files with 77 additions and 22 deletions

View File

@ -12,24 +12,56 @@ open Lean
namespace Pantograph namespace Pantograph
structure ProjectionApplication where inductive Projection where
projector: Name -- Normal field case
numParams: Nat | field (projector : Name) (numParams : Nat)
inner: Expr -- Singular inductive case
| singular (recursor : Name) (numParams : Nat) (numFields : Nat)
/-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/
@[export pantograph_analyze_projection]
def analyzeProjection (env: Environment) (e: Expr): Projection :=
let (typeName, idx, _) := match e with
| .proj typeName idx struct => (typeName, idx, struct)
| _ => panic! "Argument must be proj"
if (getStructureInfo? env typeName).isSome then
let ctor := getStructureCtor env typeName
let fieldName := getStructureFields env typeName |>.get! idx
let projector := getProjFnForField? env typeName fieldName |>.get!
.field projector ctor.numParams
else
let recursor := mkRecOnName typeName
let ctor := getStructureCtor env typeName
.singular recursor ctor.numParams ctor.numFields
def anonymousLevel : Level := .mvar ⟨.anonymous⟩
@[export pantograph_expr_proj_to_app] @[export pantograph_expr_proj_to_app]
def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication := def exprProjToApp (env: Environment) (e: Expr): Expr :=
let (typeName, idx, inner) := match e with let anon : Expr := .mvar ⟨.anonymous⟩
| .proj typeName idx inner => (typeName, idx, inner) match analyzeProjection env e with
| _ => panic! "Argument must be proj" | .field projector numParams =>
let ctor := getStructureCtor env typeName let info := match env.find? projector with
let fieldName := getStructureFields env typeName |>.get! idx | .some info => info
let projector := getProjFnForField? env typeName fieldName |>.get! | _ => panic! "Illegal projector"
{ let callee := .const projector $ List.replicate info.numLevelParams anonymousLevel
projector, let args := (List.replicate numParams anon) ++ [e.projExpr!]
numParams := ctor.numParams, mkAppN callee args.toArray
inner, | .singular recursor numParams numFields =>
} let info := match env.find? recursor with
| .some info => info
| _ => panic! "Illegal recursor"
let callee := .const recursor $ List.replicate info.numLevelParams anonymousLevel
let typeArgs := List.replicate numParams anon
-- Motive type can be inferred directly
let motive := .lam .anonymous anon anon .default
let major := e.projExpr!
-- Generate a lambda of `numFields` parameters, and returns the `e.projIdx!` one.
let induct := List.foldl
(λ acc _ => .lam .anonymous anon acc .default)
(.bvar $ (numFields - e.projIdx! - 1))
(List.range numFields)
mkAppN callee (typeArgs ++ [motive, major, induct]).toArray
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") _
@ -288,7 +320,6 @@ partial def serializeSortLevel (level: Level) : String :=
| _, .zero => s!"{k}" | _, .zero => s!"{k}"
| _, _ => s!"(+ {u_str} {k})" | _, _ => s!"(+ {u_str} {k})"
/-- /--
Completely serializes an expression tree. Json not used due to compactness Completely serializes an expression tree. Json not used due to compactness
@ -375,12 +406,17 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do
-- 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 _ _ _ => do | .proj typeName idx inner => do
let env ← getEnv let env ← getEnv
let projApp := exprProjToApp env e match analyzeProjection env e with
let autos := String.intercalate " " (List.replicate projApp.numParams "_") | .field projector numParams =>
let inner ← self projApp.inner let autos := String.intercalate " " (List.replicate numParams "_")
pure s!"((:c {projApp.projector}) {autos} {inner})" let inner' ← self inner
pure s!"((:c {projector}) {autos} {inner'})"
| .singular _ _ _ =>
let typeName' := serializeName typeName (sanitize := false)
let e' ← self e
pure s!"(:proj {typeName'} {idx} {e'})"
-- Elides all unhygenic names -- Elides all unhygenic names
binderInfoSexp : Lean.BinderInfo → String binderInfoSexp : Lean.BinderInfo → String
| .default => "" | .default => ""

View File

@ -96,6 +96,23 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get! let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
return LSpec.TestSeq.done return LSpec.TestSeq.done
def test_projection_prod (env: Environment) : IO LSpec.TestSeq:= runTest do
let struct := .app (.bvar 1) (.bvar 0)
let expr := .proj `Prod 1 struct
let .field projector numParams := analyzeProjection env expr |
fail "`Prod has fields"
checkEq "projector" projector `Prod.snd
checkEq "numParams" numParams 2
def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
let struct := .app (.bvar 1) (.bvar 0)
let expr := .proj `Exists 1 struct
let .singular recursor numParams numFields := analyzeProjection env expr |
fail "`Exists has no projectors"
checkEq "recursor" recursor `Exists.recOn
checkEq "numParams" numParams 2
checkEq "numFields" numFields 2
def suite (env: Environment): List (String × IO LSpec.TestSeq) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[ [
("serializeName", do pure test_serializeName), ("serializeName", do pure test_serializeName),
@ -104,6 +121,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
("Sexp from elaborated expr", test_sexp_of_elab env), ("Sexp from elaborated expr", test_sexp_of_elab env),
("Sexp from expr", test_sexp_of_expr env), ("Sexp from expr", test_sexp_of_expr env),
("Instance", test_instance env), ("Instance", test_instance env),
("Projection Prod", test_projection_prod env),
("Projection Exists", test_projection_exists env),
] ]
end Pantograph.Test.Delate end Pantograph.Test.Delate