fix: Serialization of projection operators #64

Merged
aniva merged 2 commits from serial/projection into dev 2024-04-09 21:28:53 -07:00
2 changed files with 33 additions and 12 deletions

View File

@ -86,6 +86,8 @@ partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
/-- /--
Completely serializes an expression tree. Json not used due to compactness Completely serializes an expression tree. Json not used due to compactness
A `_` symbol in the AST indicates automatic deductions not present in the original expression.
-/ -/
partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
self expr self expr
@ -147,10 +149,13 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
self inner self inner
| .proj typeName idx inner => do | .proj typeName idx inner => do
let env ← getEnv let env ← getEnv
let ctor := getStructureCtor env typeName
let fieldName := getStructureFields env typeName |>.get! idx let fieldName := getStructureFields env typeName |>.get! idx
let projectorName := getProjFnForField? env typeName fieldName |>.get! let projectorName := getProjFnForField? env typeName fieldName |>.get!
let e := Expr.app (.const projectorName []) inner
self e 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
binder_info_to_ast : Lean.BinderInfo → String binder_info_to_ast : Lean.BinderInfo → String
| .default => "" | .default => ""

View File

@ -23,12 +23,11 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), ("Nat.add_comm".toName, { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" }) ("Nat.le_of_succ_le".toName, { binders := #[("n", "Nat"), ("m", "Nat"), ("h", "n.succ ≤ m")], target := "n ≤ m" })
] ]
let coreM: CoreM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let expr := env.find? symbol |>.get! |>.type let expr := env.find? symbol |>.get! |>.type
let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target) let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run' return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
runCoreMSeq env coreM
def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [ let entries: List (String × String) := [
@ -41,14 +40,13 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"), ("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))") ("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")
] ]
let metaM: MetaM LSpec.TestSeq := entries.foldlM (λ suites (symbol, target) => do runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let expr := env.find? symbol.toName |>.get! |>.type let expr := env.find? symbol.toName |>.get! |>.type
let test := LSpec.check symbol ((← serialize_expression_ast expr) = target) let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
runMetaMSeq env metaM
def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [ let entries: List (String × String) := [
("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"), ("λ x: Nat × Bool => x.1", "(:lambda x ((:c Prod) (:c Nat) (:c Bool)) ((:c Prod.fst) (:c Nat) (:c Bool) 0))"),
("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
@ -65,24 +63,42 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
| .error e => return elabFailure e | .error e => return elabFailure e
let test := LSpec.check source ((← serialize_expression_ast expr) = target) let test := LSpec.check source ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let metaM := termElabM.run' (ctx := defaultTermElabMContext) runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
runMetaMSeq env metaM
def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
let entries: List (Expr × String) := [
(.lam `p (.sort .zero)
(.lam `q (.sort .zero)
(.lam `k (mkApp2 (.const `And []) (.bvar 1) (.bvar 0))
(.proj `And 1 (.bvar 0))
.default)
.implicit)
.implicit,
"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
),
]
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
let env ← MonadEnv.getEnv
let testCaseName := target.take 10
let test := LSpec.check testCaseName ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
-- Instance parsing -- Instance parsing
def test_instance (env: Environment): IO LSpec.TestSeq := do def test_instance (env: Environment): IO LSpec.TestSeq :=
let metaM: MetaM LSpec.TestSeq := do runMetaMSeq env do
let env ← MonadEnv.getEnv let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y" let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
let s := parseTerm env source |>.toOption |>.get! let s := parseTerm env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get! let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
return LSpec.TestSeq.done return LSpec.TestSeq.done
runMetaMSeq env metaM
def suite (env: Environment): List (String × IO LSpec.TestSeq) := def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[ [
("name_to_ast", do pure test_name_to_ast), ("name_to_ast", do pure test_name_to_ast),
("Expression binder", test_expr_to_binder env), ("Expression binder", test_expr_to_binder env),
("Sexp from symbol", test_sexp_of_symbol env), ("Sexp from symbol", test_sexp_of_symbol 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),
] ]