From 5994f0ddf03b71b9b1c6fbb80a7a8e153a24e17d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 17 Jan 2025 23:10:03 -0800 Subject: [PATCH 1/4] fix: Conditional handling of `.proj` --- Pantograph/Delate.lean | 17 +++++++++-------- Test/Delate.lean | 15 ++++++++++++++- 2 files changed, 23 insertions(+), 9 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 38d8bda..a404fba 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -17,15 +17,18 @@ structure ProjectionApplication where numParams: Nat inner: Expr +/-- Converts a `.proj` expression to a function application if possible. Not all +such expressions are convertible. -/ @[export pantograph_expr_proj_to_app] -def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication := +def exprProjToApp (env: Environment) (e: Expr): Option ProjectionApplication := do let (typeName, idx, inner) := match e with | .proj typeName idx inner => (typeName, idx, inner) | _ => panic! "Argument must be proj" + let _ ← getStructureInfo? env typeName let ctor := getStructureCtor env typeName let fieldName := getStructureFields env typeName |>.get! idx let projector := getProjFnForField? env typeName fieldName |>.get! - { + return { projector, numParams := ctor.numParams, inner, @@ -375,12 +378,10 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- It may become necessary to incorporate the metadata. self inner - | .proj _ _ _ => do - let env ← getEnv - let projApp := exprProjToApp env e - let autos := String.intercalate " " (List.replicate projApp.numParams "_") - let inner ← self projApp.inner - pure s!"((:c {projApp.projector}) {autos} {inner})" + | .proj typeName idx e => do + let typeName' := serializeName typeName (sanitize := false) + let e' ← self e + pure s!"(:proj {typeName'} {idx} {e'})" -- Elides all unhygenic names binderInfoSexp : Lean.BinderInfo → String | .default => "" diff --git a/Test/Delate.lean b/Test/Delate.lean index 013be73..7b449bf 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do .default) .implicit) .implicit, - "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)" + "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) (:proj And 1 0)) :i) :i)" ), ] let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do @@ -96,6 +96,18 @@ def test_instance (env: Environment): IO LSpec.TestSeq := let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get! return LSpec.TestSeq.done +def test_projection (env: Environment) : IO LSpec.TestSeq:= runTest do + let prod := .app (.bvar 1) (.bvar 0) + let expr := .proj `Prod 1 prod + let .some { projector, numParams, inner }:= exprProjToApp env expr | + fail "`Prod should have projection function" + checkEq "projector" projector `Prod.snd + checkEq "numParams" numParams 2 + checkTrue "inner" $ inner.equal prod + + let expr := .proj `Exists 1 prod + checkTrue "Exists" (exprProjToApp env expr).isNone + def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ ("serializeName", do pure test_serializeName), @@ -104,6 +116,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Sexp from elaborated expr", test_sexp_of_elab env), ("Sexp from expr", test_sexp_of_expr env), ("Instance", test_instance env), + ("Projection", test_projection env), ] end Pantograph.Test.Delate From 3a26bb19249c89d16dd0b105c147c120c795200a Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 22 Jan 2025 12:49:33 -0800 Subject: [PATCH 2/4] fix: Analyze projection application --- Pantograph/Delate.lean | 38 +++++++++++++++++++------------------- Test/Delate.lean | 25 ++++++++++++++++--------- 2 files changed, 35 insertions(+), 28 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index a404fba..18eaaf1 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -12,27 +12,27 @@ open Lean namespace Pantograph -structure ProjectionApplication where - projector: Name - numParams: Nat - inner: Expr +inductive Projection where + -- Normal field case + | field (projector : Name) (numParams : Nat) (struct : Expr) + -- Singular inductive case + | singular (recursor : Name) (numParams : Nat) (struct : Expr) -/-- Converts a `.proj` expression to a function application if possible. Not all -such expressions are convertible. -/ -@[export pantograph_expr_proj_to_app] -def exprProjToApp (env: Environment) (e: Expr): Option ProjectionApplication := do - let (typeName, idx, inner) := match e with - | .proj typeName idx inner => (typeName, idx, inner) +/-- 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, struct) := match e with + | .proj typeName idx struct => (typeName, idx, struct) | _ => panic! "Argument must be proj" - let _ ← getStructureInfo? env typeName - let ctor := getStructureCtor env typeName - let fieldName := getStructureFields env typeName |>.get! idx - let projector := getProjFnForField? env typeName fieldName |>.get! - return { - projector, - numParams := ctor.numParams, - inner, - } + 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 struct + else + let recursor := mkRecOnName typeName + let ctor := getStructureCtor env typeName + .singular recursor ctor.numParams struct def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ diff --git a/Test/Delate.lean b/Test/Delate.lean index 7b449bf..aa5ea7c 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -96,17 +96,23 @@ def test_instance (env: Environment): IO LSpec.TestSeq := let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get! return LSpec.TestSeq.done -def test_projection (env: Environment) : IO LSpec.TestSeq:= runTest do - let prod := .app (.bvar 1) (.bvar 0) - let expr := .proj `Prod 1 prod - let .some { projector, numParams, inner }:= exprProjToApp env expr | - fail "`Prod should have projection function" +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 struct' := analyzeProjection env expr | + fail "`Prod has fields" checkEq "projector" projector `Prod.snd checkEq "numParams" numParams 2 - checkTrue "inner" $ inner.equal prod + checkTrue "struct" $ struct.equal struct' - let expr := .proj `Exists 1 prod - checkTrue "Exists" (exprProjToApp env expr).isNone +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 struct' := analyzeProjection env expr | + fail "`Exists has no projectors" + checkEq "recursor" recursor `Exists.recOn + checkEq "numParams" numParams 2 + checkTrue "struct" $ struct.equal struct' def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ @@ -116,7 +122,8 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) := ("Sexp from elaborated expr", test_sexp_of_elab env), ("Sexp from expr", test_sexp_of_expr env), ("Instance", test_instance env), - ("Projection", test_projection env), + ("Projection Prod", test_projection_prod env), + ("Projection Exists", test_projection_exists env), ] end Pantograph.Test.Delate From 8ce4cbdcf55e73589f3eca3052fadfa1843589d0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 22 Jan 2025 13:01:47 -0800 Subject: [PATCH 3/4] feat: Printing field projection in sexp --- Pantograph/Delate.lean | 27 +++++++++++++++++---------- Test/Delate.lean | 8 +++----- 2 files changed, 20 insertions(+), 15 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 18eaaf1..28f4851 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -14,25 +14,25 @@ namespace Pantograph inductive Projection where -- Normal field case - | field (projector : Name) (numParams : Nat) (struct : Expr) + | field (projector : Name) (numParams : Nat) -- Singular inductive case - | singular (recursor : Name) (numParams : Nat) (struct : Expr) + | singular (recursor : Name) (numParams : 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, struct) := match e with + 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 struct + .field projector ctor.numParams else let recursor := mkRecOnName typeName let ctor := getStructureCtor env typeName - .singular recursor ctor.numParams struct + .singular recursor ctor.numParams def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _ @@ -291,7 +291,7 @@ partial def serializeSortLevel (level: Level) : String := | _, .zero => s!"{k}" | _, _ => s!"(+ {u_str} {k})" - +#check Exists.recOn /-- Completely serializes an expression tree. Json not used due to compactness @@ -378,10 +378,17 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter -- It may become necessary to incorporate the metadata. self inner - | .proj typeName idx e => do - let typeName' := serializeName typeName (sanitize := false) - let e' ← self e - pure s!"(:proj {typeName'} {idx} {e'})" + | .proj typeName idx inner => do + let env ← getEnv + match analyzeProjection env e with + | .field projector numParams => + let autos := String.intercalate " " (List.replicate numParams "_") + 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 binderInfoSexp : Lean.BinderInfo → String | .default => "" diff --git a/Test/Delate.lean b/Test/Delate.lean index aa5ea7c..befc60b 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -77,7 +77,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do .default) .implicit) .implicit, - "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) (:proj And 1 0)) :i) :i)" + "(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :i) :i)" ), ] let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do @@ -99,20 +99,18 @@ def test_instance (env: Environment): IO LSpec.TestSeq := 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 struct' := analyzeProjection env expr | + let .field projector numParams := analyzeProjection env expr | fail "`Prod has fields" checkEq "projector" projector `Prod.snd checkEq "numParams" numParams 2 - checkTrue "struct" $ struct.equal struct' 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 struct' := analyzeProjection env expr | + let .singular recursor numParams := analyzeProjection env expr | fail "`Exists has no projectors" checkEq "recursor" recursor `Exists.recOn checkEq "numParams" numParams 2 - checkTrue "struct" $ struct.equal struct' def suite (env: Environment): List (String × IO LSpec.TestSeq) := [ From 5c1e7599c0ea85301d859f94052d1b9f4251119d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 24 Jan 2025 14:44:09 -0800 Subject: [PATCH 4/4] feat: Projection export function --- Pantograph/Delate.lean | 36 ++++++++++++++++++++++++++++++++---- Test/Delate.lean | 3 ++- 2 files changed, 34 insertions(+), 5 deletions(-) diff --git a/Pantograph/Delate.lean b/Pantograph/Delate.lean index 28f4851..ad923aa 100644 --- a/Pantograph/Delate.lean +++ b/Pantograph/Delate.lean @@ -16,7 +16,7 @@ inductive Projection where -- Normal field case | field (projector : Name) (numParams : Nat) -- Singular inductive case - | singular (recursor : Name) (numParams : Nat) + | singular (recursor : Name) (numParams : Nat) (numFields : Nat) /-- Converts a `.proj` expression to a form suitable for exporting/transpilation -/ @[export pantograph_analyze_projection] @@ -32,7 +32,36 @@ def analyzeProjection (env: Environment) (e: Expr): Projection := else let recursor := mkRecOnName typeName let ctor := getStructureCtor env typeName - .singular recursor ctor.numParams + .singular recursor ctor.numParams ctor.numFields + +def anonymousLevel : Level := .mvar ⟨.anonymous⟩ + +@[export pantograph_expr_proj_to_app] +def exprProjToApp (env: Environment) (e: Expr): Expr := + let anon : Expr := .mvar ⟨.anonymous⟩ + match analyzeProjection env e with + | .field projector numParams => + let info := match env.find? projector with + | .some info => info + | _ => panic! "Illegal projector" + let callee := .const projector $ List.replicate info.numLevelParams anonymousLevel + let args := (List.replicate numParams anon) ++ [e.projExpr!] + mkAppN callee args.toArray + | .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") _ @@ -291,7 +320,6 @@ partial def serializeSortLevel (level: Level) : String := | _, .zero => s!"{k}" | _, _ => s!"(+ {u_str} {k})" -#check Exists.recOn /-- Completely serializes an expression tree. Json not used due to compactness @@ -385,7 +413,7 @@ partial def serializeExpressionSexp (expr: Expr) : MetaM String := do let autos := String.intercalate " " (List.replicate numParams "_") let inner' ← self inner pure s!"((:c {projector}) {autos} {inner'})" - | .singular _ _ => + | .singular _ _ _ => let typeName' := serializeName typeName (sanitize := false) let e' ← self e pure s!"(:proj {typeName'} {idx} {e'})" diff --git a/Test/Delate.lean b/Test/Delate.lean index befc60b..517a394 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -107,10 +107,11 @@ def test_projection_prod (env: Environment) : IO LSpec.TestSeq:= runTest do 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 := analyzeProjection env expr | + 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) := [