Merge branch 'dev' into library/catalog

Pantograph/Serial.lean

@@ -84,67 +84,70 @@ partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
 /--
  Completely serializes an expression tree. Json not used due to compactness
 -/
-partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
+partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
   self expr
   where
-  self (e: Expr): String :=
+  self (e: Expr): MetaM String :=
     match e with
     | .bvar deBruijnIndex =>
       -- This is very common so the index alone is shown. Literals are handled below.
       -- The raw de Bruijn index should never appear in an unbound setting. In
       -- Lean these are handled using a `#` prefix.
-      s!"{deBruijnIndex}"
+      pure s!"{deBruijnIndex}"
     | .fvar fvarId =>
       let name := of_name fvarId.name
-      s!"(:fv {name})"
+      pure s!"(:fv {name})"
     | .mvar mvarId =>
       let name := of_name mvarId.name
-      s!"(:mv {name})"
+      pure s!"(:mv {name})"
     | .sort level =>
       let level := serialize_sort_level_ast level sanitize
-      s!"(:sort {level})"
+      pure s!"(:sort {level})"
     | .const declName _ =>
       -- The universe level of the const expression is elided since it should be
       -- inferrable from surrounding expression
-      s!"(:c {declName})"
+      pure s!"(:c {declName})"
-    | .app _ _ =>
+    | .app _ _ => do
-      let fn' := self e.getAppFn
+      let fn' ← self e.getAppFn
-      let args := e.getAppArgs.map self |>.toList
+      let args := (← e.getAppArgs.mapM self) |>.toList
       let args := " ".intercalate args
-      s!"({fn'} {args})"
+      pure s!"({fn'} {args})"
-    | .lam binderName binderType body binderInfo =>
+    | .lam binderName binderType body binderInfo => do
       let binderName' := of_name binderName
-      let binderType' := self binderType
+      let binderType' ← self binderType
-      let body' := self body
+      let body' ← self body
       let binderInfo' := binder_info_to_ast binderInfo
-      s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
+      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
-    | .forallE binderName binderType body binderInfo =>
+    | .forallE binderName binderType body binderInfo => do
       let binderName' := of_name binderName
-      let binderType' := self binderType
+      let binderType' ← self binderType
-      let body' := self body
+      let body' ← self body
       let binderInfo' := binder_info_to_ast binderInfo
-      s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
+      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
-    | .letE name type value body _ =>
+    | .letE name type value body _ => do
       -- Dependent boolean flag diacarded
       let name' := name_to_ast name
-      let type' := self type
+      let type' ← self type
-      let value' := self value
+      let value' ← self value
-      let body' := self body
+      let body' ← self body
-      s!"(:let {name'} {type'} {value'} {body'})"
+      pure s!"(:let {name'} {type'} {value'} {body'})"
     | .lit v =>
       -- To not burden the downstream parser who needs to handle this, the literal
       -- is wrapped in a :lit sexp.
       let v' := match v with
         | .natVal val => toString val
         | .strVal val => s!"\"{val}\""
-      s!"(:lit {v'})"
+      pure s!"(:lit {v'})"
     | .mdata _ inner =>
       -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
       -- It may become necessary to incorporate the metadata.
       self inner
-    | .proj typeName idx struct =>
+    | .proj typeName idx inner => do
-      let struct' := self struct
+      let env ← getEnv
-      s!"(:proj {typeName} {idx} {struct'})"
+      let fieldName := getStructureFields env typeName |>.get! idx
+      let inner ← Meta.mkProjection inner fieldName
+      assert! !inner.isProj
+      self inner
   -- Elides all unhygenic names
   binder_info_to_ast : Lean.BinderInfo → String
     | .default => ""
@@ -158,7 +161,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E
   let pp?: Option String := match options.printExprPretty with
     | true => .some pp
     | false => .none
-  let sexp: String := serialize_expression_ast e
+  let sexp: String ← serialize_expression_ast e
   let sexp?: Option String := match options.printExprAST with
     | true => .some sexp
     | false => .none
@@ -287,7 +290,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
     printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
       if options.printContext then
         decl.lctx.fvarIdToDecl.forM printFVar
-      let type_sexp := serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
+      let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
       IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
       if options.printValue then
         if let Option.some value := (← getMCtx).eAssignment.find? mvarId then

Test/Serial.lean

@@ -52,7 +52,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   let metaM: MetaM LSpec.TestSeq := 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)
+    let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   let coreM := metaM.run'
   let coreContext: Core.Context := {
@@ -66,6 +66,32 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
     return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
   | .ok a            => return a
 
+def test_sexp_of_expr (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))")
+  ]
+  let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
+    let env ← MonadEnv.getEnv
+    let s := syntax_from_str env source |>.toOption |>.get!
+    let expr := (← syntax_to_expr s) |>.toOption |>.get!
+    let test := LSpec.check source ((← serialize_expression_ast expr) = target)
+    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
+  let metaM := termElabM.run' (ctx := {
+    declName? := some "_pantograph",
+    errToSorry := false
+  })
+  let coreM := metaM.run'
+  let coreContext: Core.Context := {
+    currNamespace := Lean.Name.str .anonymous "Aniva"
+    openDecls := [],     -- No 'open' directives needed
+    fileName := "<Pantograph/Test>",
+    fileMap := { source := "", positions := #[0], lines := #[1] }
+  }
+  match ← (coreM.run' coreContext { env := env }).toBaseIO with
+  | .error exception =>
+    return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
+  | .ok a            => return a
 
 def suite: IO LSpec.TestSeq := do
   let env: Environment ← importModules
@@ -76,6 +102,7 @@ def suite: IO LSpec.TestSeq := do
   return LSpec.group "Serialization" $
     (LSpec.group "name_to_ast" test_name_to_ast) ++
     (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
-    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))
+    (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) ++
+    (LSpec.group "Sexp from expr" (← test_sexp_of_expr env))
 
 end Pantograph.Test.Serial