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

Pantograph/Environment.lean

@@ -69,8 +69,8 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
       else pure (.none),
     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,
           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

Pantograph/Protocol.lean

@@ -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

Pantograph/Serial.lean

@@ -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 => ""

Test/Environment.lean

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

Test/Serial.lean

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