Merge pull request 'fix: `env.add` Declarations with universe levels' (#181) from bug/env-add-level into dev

Reviewed-on: #181

Pantograph/Environment.lean

@@ -144,31 +144,38 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): Protocol.
     else
       .pure result
   return result
+/-- Elaborates and adds a declaration to the `CoreM` environment. -/
 @[export pantograph_env_add_m]
-def addDecl (name: String) (levels: Array String := #[]) (type: String) (value: String) (isTheorem: Bool)
+def addDecl (name: String) (levels: Array String := #[]) (type?: Option String) (value: String) (isTheorem: Bool)
     : Protocol.FallibleT CoreM Protocol.EnvAddResult := do
   let env ← Lean.MonadEnv.getEnv
-  let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
-    let type ← match parseTerm env type with
-      | .ok syn => do
-        match ← elabTerm syn with
-        | .error e => return .error e
-        | .ok expr => pure expr
+  let levelParams := levels.toList.map (·.toName)
+  let tvM: Elab.TermElabM (Except String (Expr × Expr)) :=
+    Elab.Term.withLevelNames levelParams do do
+    let expectedType?? : Except String (Option Expr) ← ExceptT.run $ type?.mapM λ type => do
+      match parseTerm env type with
+      | .ok syn => elabTerm syn
+      | .error e => MonadExceptOf.throw e
+    let expectedType? ← match expectedType?? with
+      | .ok t? => pure t?
       | .error e => return .error e
     let value ← match parseTerm env value with
       | .ok syn => do
         try
-          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
+          let expr ← Elab.Term.elabTerm (stx := syn) (expectedType? := expectedType?)
           Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
           let expr ← instantiateMVars expr
           pure $ expr
         catch ex => return .error (← ex.toMessageData.toString)
       | .error e => return .error e
-    pure $ .ok (type, value)
+    Elab.Term.synthesizeSyntheticMVarsNoPostponing
+    let type ← match expectedType? with
+      | .some t => pure t
+      | .none => Meta.inferType value
+    pure $ .ok (← instantiateMVars type, ← instantiateMVars value)
   let (type, value) ← match ← tvM.run' (ctx := {}) |>.run' with
     | .ok t => pure t
     | .error e => Protocol.throw $ Protocol.errorExpr e
-  let levelParams := levels.toList.map (·.toName)
   let decl := if isTheorem then
     Lean.Declaration.thmDecl <| Lean.mkTheoremValEx
       (name := name.toName)

Pantograph/Protocol.lean

@@ -205,7 +205,7 @@ structure EnvInspectResult where
 structure EnvAdd where
   name: String
   levels: Array String := #[]
-  type: String
+  type?: Option String := .none
   value: String
   isTheorem: Bool := false
   deriving Lean.FromJson

Repl.lean

@@ -227,7 +227,7 @@ def execute (command: Protocol.Command): MainM Json := do
     let state ← getMainState
     runCoreM' $ Environment.inspect args state.options
   env_add (args: Protocol.EnvAdd): EMainM Protocol.EnvAddResult := do
-    runCoreM' $ Environment.addDecl args.name args.levels args.type args.value args.isTheorem
+    runCoreM' $ Environment.addDecl args.name args.levels args.type? args.value args.isTheorem
   env_save (args: Protocol.EnvSaveLoad): EMainM Protocol.EnvSaveLoadResult := do
     let env ← MonadEnv.getEnv
     environmentPickle env args.path

Test/Integration.lean

@@ -162,11 +162,11 @@ def test_automatic_mode (automatic: Bool): Test :=
 def test_env_add_inspect : Test :=
   let name1 := "Pantograph.mystery"
   let name2 := "Pantograph.mystery2"
+  let name3 := "Pantograph.mystery3"
   [
     step "env.add"
       ({
         name := name1,
-        type := "Prop → Prop → Prop",
         value := "λ (a b: Prop) => Or a b",
         isTheorem := false
       }: Protocol.EnvAdd)
@@ -180,7 +180,7 @@ def test_env_add_inspect : Test :=
     step "env.add"
       ({
         name := name2,
-        type := "Nat → Int",
+        type? := "Nat → Int",
         value := "λ (a: Nat) => a + 1",
         isTheorem := false
       }: Protocol.EnvAdd)
@@ -190,7 +190,21 @@ def test_env_add_inspect : Test :=
        value? := .some { pp? := .some "fun a => ↑a + 1" },
        type := { pp? := .some "Nat → Int" },
      }:
-      Protocol.EnvInspectResult)
+      Protocol.EnvInspectResult),
+    step "env.add"
+      ({
+        name := name3,
+        levels := #["u"]
+        type? := "(α : Type u) → α → (α × α)",
+        value := "λ (α : Type u) (x : α) => (x, x)",
+        isTheorem := false
+      }: Protocol.EnvAdd)
+     ({}: Protocol.EnvAddResult),
+    step "env.inspect" ({name := name3} : Protocol.EnvInspect)
+     ({
+       type := { pp? := .some "(α : Type u) → α → α × α" },
+     }:
+      Protocol.EnvInspectResult),
   ]
 
 example : ∀ (p: Prop), p → p := by