proj to app

Stream: lean4

[Leni Aniva]

Is there a function that can convert Expr.proj to the equivalent Expr.app?

For example .proj Prod 0 x is x.0, and I want to transform it to the equivalent Prod.fst x`

The documentation says

When exporting Lean developments to other systems, proj can be replaced with typeName.rec
applications.
but how can this be done since Prod.rec relies on the motive?

[Kyle Miller]

I think you use docs#Lean.getStructureFields to get the field names, and then use docs#Lean.getFieldInfo? to get a structure that contains the projFn field.

It looks like there's docs#Lean.Meta.mkProjection, to create the Expr.app. It can also handle field names that are subfields (fields from a structure it extends)

[Leni Aniva]

Kyle Miller said:

I think you use docs#Lean.getStructureFields to get the field names, and then use docs#Lean.getFieldInfo? to get a structure that contains the projFn field.

It looks like there's docs#Lean.Meta.mkProjection, to create the Expr.app. It can also handle field names that are subfields (fields from a structure it extends)

is there a way to get the list of all structures for this?

[Notification Bot]

Leni Aniva has marked this topic as resolved.

[Leni Aniva]

Kyle Miller said:

I think you use docs#Lean.getStructureFields to get the field names, and then use docs#Lean.getFieldInfo? to get a structure that contains the projFn field.

It looks like there's docs#Lean.Meta.mkProjection, to create the Expr.app. It can also handle field names that are subfields (fields from a structure it extends)

I tried using this function and I found this symbol that causes it to crash: ULift.down. The value of this function is fun α self => self.1, which seems to be ok on the surface. However when I invoke Meta.mkProjection on the operand self.1, I get

unexpected bound variable #0

The full example is here:

import Lean
open Lean
partial def serialize_expression_ast (expr: Expr): MetaM String := do
  self expr
  where
  self (e: Expr): MetaM String :=
    match e with
    | .bvar deBruijnIndex =>
      pure s!"{deBruijnIndex}"
    | .fvar fvarId =>
      let name := fvarId.name.toString
      pure s!"(:fv {name})"
    | .mvar mvarId =>
      let name := mvarId.name.toString
      pure s!"(:mv {name})"
    | .sort _ =>
      pure s!"(:sort)"
    | .const declName _ =>
      -- The universe level of the const expression is elided since it should be
      -- inferrable from surrounding expression
      pure s!"(:c {declName})"
    | .app _ _ => do
      let fn' ← self e.getAppFn
      let args := (← e.getAppArgs.mapM self) |>.toList
      let args := " ".intercalate args
      pure s!"({fn'} {args})"
    | .lam binderName binderType body binderInfo => do
      let binderName' := binderName.toString
      let binderType' ← self binderType
      let body' ← self body
      let binderInfo' := binder_info_to_ast binderInfo
      pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
    | .forallE binderName binderType body binderInfo => do
      let binderName' := binderName.toString
      let binderType' ← self binderType
      let body' ← self body
      let binderInfo' := binder_info_to_ast binderInfo
      pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
    | .letE name type value body _ => do
      -- Dependent boolean flag diacarded
      let name' := name.toString
      let type' ← self type
      let value' ← self value
      let body' ← self 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}\""
      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 inner => do
      let env ← getEnv
      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 => ""
    | .implicit => " :implicit"
    | .strictImplicit => " :strictImplicit"
    | .instImplicit => " :instImplicit"

def metaM: MetaM Unit := do
  let env ← getEnv
  let symbol := "ULift.down".toName
  IO.println "Finding symbol"
  let info := env.find? symbol |>.get!
  IO.println "Finding value"
  let value := info.value? |>.get!
  IO.println "Printing"
  let expr := toString (← serialize_expression_ast value)
  IO.println s!"{expr}"

def main : IO Unit := do
  let env: Environment ← importModules
    (imports := #["Init"].map (λ str => { module := str.toName, runtimeOnly := false }))
    (opts := {})
    (trustLevel := 1)
  let coreM := Meta.MetaM.run' metaM
  let coreContext: Lean.Core.Context := {
    currNamespace := "PrintExpr".toName,
    openDecls := [],     -- No 'open' directives needed
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0], lines := #[1] }
    options := Lean.Options.empty
  }
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
    IO.println s!"{← exception.toMessageData.toString}"
  | .ok _            =>
    IO.println "Finished"

[Notification Bot]

Leni Aniva has marked this topic as unresolved.

[Notification Bot]

Leni Aniva has marked this topic as unresolved.

[Notification Bot]

Leni Aniva has marked this topic as resolved.

[Notification Bot]

Leni Aniva has marked this topic as unresolved.

[Leni Aniva]

Kyle Miller said:

I think you use docs#Lean.getStructureFields to get the field names, and then use docs#Lean.getFieldInfo? to get a structure that contains the projFn field.

It looks like there's docs#Lean.Meta.mkProjection, to create the Expr.app. It can also handle field names that are subfields (fields from a structure it extends)

Is there a function that doesn't require telescoping? Meta.mkProjection requires telescoping into the local context where the projection takes place. I feel like the projected type should be recoverable from the fields of Expr.proj

I'm currently using a structure like this:

| .proj typeName idx inner => do
      let env ← getEnv
      let fieldName := getStructureFields env typeName |>.get! idx
      let projectorName := getProjFnForField? env typeName fieldName |>.get!
      let e := Expr.app (.const  projectorName []) inner
      -- e is now a projection in `.app` form