addAndCompile a structure?

Stream: lean4

[James Gallicchio]

I have a list of field names and elaborated Exprs for the field types. How do I turn that into a structure declaration to compile? I can't seem to find any relevant functions... :(

To slightly un-XY: I want a syntax for defining structures as

object Name {
  "key1" : something
}

where something : SchemaM ?type (SchemaM is a monad). Idea is I want to generate a structure with field key1 : <type>. Then I can define other stuff that makes use of the actual something value.

So in order to find what <type> is, I'm elaborating something to an expression with expected type SchemaM ?type and then instantiating the ?type expression.

But now I've no idea how to get this into a structure (.. an inductive I know how to do. but not a structure).

Is there a different way I should be going about it?

[James Gallicchio]

One thing I've tried is to just build the syntax for a structure and then elabCommand it. But I think I am encountering issues where liftTermElabM throws out (?) the metavariable assignments:

import Lean
import Std

def SchemaM : Type → Type := Id

open Lean Macro Elab Meta Term Command in
elab "object " name:ident "{" keyStx:( str ":" "required "? term ),* "}" : command => do
  -- name, required, (Lean) type, schema
  let keys : Array (String × Bool × TSyntax `term × TSyntax `term) ←
    liftTermElabM <| keyStx.getElems.mapM (fun s =>
      -- unsure if this is actually necessary
      -- but we use the mvar identifier `type` so /shrug
      withFreshMacroScope do
      let key := s.raw[0].isStrLit?.get!
      let isReq := s.raw[2].hasArgs
      let val : Term := .mk s.raw[3]
      -- make a new metavariable for the type
      let type : Term ← `(?type)
      let typeExpr : Expr ← elabTermEnsuringType type (some (.sort (Level.ofNat 1)))
      let elabVal ← elabTermEnsuringType val (some (.app (.const ``SchemaM []) typeExpr))
      return (key, isReq, type, ← elabVal.toSyntax)
    )
  let typeId := mkIdent (name.getId ++ "type")
  let fields : TSyntaxArray _ ← keys.mapM (fun (name, _req, type, _schema) =>
    `(Lean.Parser.Command.structExplicitBinder| ($(mkIdent name) : $type))
  )
  elabCommand <| ← `(
    structure $typeId where
      $fields:structExplicitBinder*
  )

def string : SchemaM Unit := ()

set_option pp.rawOnError true
object Hi { -- don't know how to synthesize placeholder
            -- context:
            -- case type
            -- ⊢ Sort ?u.12896-/
  "hi" : string
}

[James Gallicchio]

(sidenote: it lists that ?type : Sort ?u.12896 there, but I quite clearly call ensureHasType with Sort 1. Why is that information not reflected in the error?)

[James Gallicchio]

Another option would be to use the delaborator instead of metavariables. But it feels like a bad idea to rely on the delaborator...

[Tomas Skrivan]

I'm not sitting in front of a computer so I can't check but isn't structure just an inductive with some flag? Now I'm guessing, maybe create an inductive and then call some function that generates all the projection functions?

[James Gallicchio]

That is what I am hoping. But I can't seem to find a function to generate the right stuff. The Declaration itself has a few flags that are related to being a structure, but nothing labelled as being a structure.

[Tomas Skrivan]

I think you have to register structure with registerStructure https://github.com/leanprover/lean4/blob/dceed634a05e1d62588f89b9f1d7b7b4cf79f676/src/Lean/Structure.lean#L57 but there has to be a streamlined function that generates StructureDescr from struct like inductive

[Tomas Skrivan]

Maybe this one https://github.com/leanprover/lean4/blob/dceed634a05e1d62588f89b9f1d7b7b4cf79f676/src/Lean/Elab/Structure.lean#L699

[Tomas Skrivan]

I think this is the crucial line, just above it you create projections
https://github.com/leanprover/lean4/blob/dceed634a05e1d62588f89b9f1d7b7b4cf79f676/src/Lean/Elab/Structure.lean#L835

[Tomas Skrivan]

But I'm very confused why is it sooo complicated. Maybe the extends business is really complicated. It would be definitely nice to have a nice streamlined API that creates a simple structure given a set of field names, types and structure parameters.

I'm thinking about implementing "struct of arrays" support and such API would be useful for that.

[Tomas Skrivan]

Wow, the function mkProjections is opaque, what is going on? Is it because the kernel needs to know about projections such that it can deal with Expr.proj?

[James Gallicchio]

oof