Merge branch 'dev' into goal/have-conv-calc

This commit is contained in:
Leni Aniva 2024-04-11 15:35:30 -07:00
commit a41b95e540
5 changed files with 55 additions and 17 deletions

View File

@ -69,8 +69,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
else pure (.none), else pure (.none),
module? := module? module? := module?
} }
let result := match info with let result match info with
| .inductInfo induct => { core with inductInfo? := .some { | .inductInfo induct => pure { core with inductInfo? := .some {
numParams := induct.numParams, numParams := induct.numParams,
numIndices := induct.numIndices, numIndices := induct.numIndices,
all := induct.all.toArray.map (·.toString), all := induct.all.toArray.map (·.toString),
@ -79,21 +79,27 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
isReflexive := induct.isReflexive, isReflexive := induct.isReflexive,
isNested := induct.isNested, isNested := induct.isNested,
} } } }
| .ctorInfo ctor => { core with constructorInfo? := .some { | .ctorInfo ctor => pure { core with constructorInfo? := .some {
induct := ctor.induct.toString, induct := ctor.induct.toString,
cidx := ctor.cidx, cidx := ctor.cidx,
numParams := ctor.numParams, numParams := ctor.numParams,
numFields := ctor.numFields, numFields := ctor.numFields,
} } } }
| .recInfo r => { core with recursorInfo? := .some { | .recInfo r => pure { core with recursorInfo? := .some {
all := r.all.toArray.map (·.toString), all := r.all.toArray.map (·.toString),
numParams := r.numParams, numParams := r.numParams,
numIndices := r.numIndices, numIndices := r.numIndices,
numMotives := r.numMotives, numMotives := r.numMotives,
numMinors := r.numMinors, numMinors := r.numMinors,
rules := ← r.rules.toArray.mapM (λ rule => do
pure {
ctor := rule.ctor.toString,
nFields := rule.nfields,
rhs := ← (serialize_expression options rule.rhs).run',
})
k := r.k, k := r.k,
} } } }
| _ => core | _ => pure core
return .ok result return .ok result
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv

View File

@ -138,12 +138,20 @@ structure ConstructorInfo where
numParams: Nat numParams: Nat
numFields: Nat numFields: Nat
deriving Lean.ToJson deriving Lean.ToJson
/-- See `Lean/Declaration.lean` -/
structure RecursorRule where
ctor: String
nFields: Nat
rhs: Expression
deriving Lean.ToJson
structure RecursorInfo where structure RecursorInfo where
all: Array String all: Array String
numParams: Nat numParams: Nat
numIndices: Nat numIndices: Nat
numMotives: Nat numMotives: Nat
numMinors: Nat numMinors: Nat
rules: Array RecursorRule
k: Bool k: Bool
deriving Lean.ToJson deriving Lean.ToJson
structure EnvInspectResult where structure EnvInspectResult where

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

@ -11,6 +11,7 @@ open Pantograph
deriving instance DecidableEq, Repr for Protocol.InductInfo deriving instance DecidableEq, Repr for Protocol.InductInfo
deriving instance DecidableEq, Repr for Protocol.ConstructorInfo deriving instance DecidableEq, Repr for Protocol.ConstructorInfo
deriving instance DecidableEq, Repr for Protocol.RecursorRule
deriving instance DecidableEq, Repr for Protocol.RecursorInfo deriving instance DecidableEq, Repr for Protocol.RecursorInfo
deriving instance DecidableEq, Repr for Protocol.EnvInspectResult deriving instance DecidableEq, Repr for Protocol.EnvInspectResult
@ -69,6 +70,7 @@ def test_inspect: IO LSpec.TestSeq := do
numIndices := 1, numIndices := 1,
numMotives := 1, numMotives := 1,
numMinors := 1, numMinors := 1,
rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
k := true, k := true,
}), }),
("ForM.rec", ConstantCat.recursor { ("ForM.rec", ConstantCat.recursor {
@ -77,6 +79,7 @@ def test_inspect: IO LSpec.TestSeq := do
numIndices := 0, numIndices := 0,
numMotives := 1, numMotives := 1,
numMinors := 1, numMinors := 1,
rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
k := false, k := false,
}) })
] ]

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),
] ]