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

This commit is contained in:
Leni Aniva 2024-04-11 15:35:30 -07:00
commit 440cc1c920
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
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),
module? := module?
}
let result := match info with
| .inductInfo induct => { core with inductInfo? := .some {
let result match info with
| .inductInfo induct => pure { core with inductInfo? := .some {
numParams := induct.numParams,
numIndices := induct.numIndices,
all := induct.all.toArray.map (·.toString),
@ -79,21 +79,27 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
isReflexive := induct.isReflexive,
isNested := induct.isNested,
} }
| .ctorInfo ctor => { core with constructorInfo? := .some {
| .ctorInfo ctor => pure { core with constructorInfo? := .some {
induct := ctor.induct.toString,
cidx := ctor.cidx,
numParams := ctor.numParams,
numFields := ctor.numFields,
} }
| .recInfo r => { core with recursorInfo? := .some {
| .recInfo r => pure { core with recursorInfo? := .some {
all := r.all.toArray.map (·.toString),
numParams := r.numParams,
numIndices := r.numIndices,
numMotives := r.numMotives,
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,
} }
| _ => core
| _ => pure core
return .ok result
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
let env ← Lean.MonadEnv.getEnv

View File

@ -138,12 +138,20 @@ structure ConstructorInfo where
numParams: Nat
numFields: Nat
deriving Lean.ToJson
/-- See `Lean/Declaration.lean` -/
structure RecursorRule where
ctor: String
nFields: Nat
rhs: Expression
deriving Lean.ToJson
structure RecursorInfo where
all: Array String
numParams: Nat
numIndices: Nat
numMotives: Nat
numMinors: Nat
rules: Array RecursorRule
k: Bool
deriving Lean.ToJson
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
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
self expr
@ -147,10 +149,13 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
self inner
| .proj typeName idx inner => do
let env ← getEnv
let ctor := getStructureCtor env typeName
let fieldName := getStructureFields env typeName |>.get! idx
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
binder_info_to_ast : Lean.BinderInfo → String
| .default => ""

View File

@ -11,6 +11,7 @@ open Pantograph
deriving instance DecidableEq, Repr for Protocol.InductInfo
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.EnvInspectResult
@ -69,6 +70,7 @@ def test_inspect: IO LSpec.TestSeq := do
numIndices := 1,
numMotives := 1,
numMinors := 1,
rules := #[{ ctor := "Eq.refl", nFields := 0, rhs := { pp? := .some "fun {α} a motive refl => refl" } }]
k := true,
}),
("ForM.rec", ConstantCat.recursor {
@ -77,6 +79,7 @@ def test_inspect: IO LSpec.TestSeq := do
numIndices := 0,
numMotives := 1,
numMinors := 1,
rules := #[{ ctor := "ForM.mk", nFields := 1, rhs := { pp? := .some "fun m γ α motive mk forM => mk forM" } }]
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.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 expr := env.find? symbol |>.get! |>.type
let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
runCoreMSeq env coreM
def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
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)))"),
("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 expr := env.find? symbol.toName |>.get! |>.type
let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
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) := [
("λ 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))"),
@ -65,24 +63,42 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
| .error e => return elabFailure e
let test := LSpec.check source ((← serialize_expression_ast expr) = target)
return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
let metaM := termElabM.run' (ctx := defaultTermElabMContext)
runMetaMSeq env metaM
runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
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
def test_instance (env: Environment): IO LSpec.TestSeq := do
let metaM: MetaM LSpec.TestSeq := do
def test_instance (env: Environment): IO LSpec.TestSeq :=
runMetaMSeq env do
let env ← MonadEnv.getEnv
let source := "λ x y: Nat => HAdd.hAdd Nat Nat Nat (instHAdd Nat instAddNat) x y"
let s := parseTerm env source |>.toOption |>.get!
let _expr := (← runTermElabMInMeta <| elabTerm s) |>.toOption |>.get!
return LSpec.TestSeq.done
runMetaMSeq env metaM
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("name_to_ast", do pure test_name_to_ast),
("Expression binder", test_expr_to_binder 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),
("Instance", test_instance env),
]