Pretty Printing non-polymorphic instance

Stream: lean4

[Leni Aniva]

Is there a way to print polymorphic operators so they point to the exact instance being instantiated? e.g. In a context of n m : Nat, have n + m being prettyprinted as Nat.add n m?

I have this script for printing expressions: (It is a bit long but most of it deals with setting options)

import Lean

open Lean

def str_to_name (s: String): Name :=
  (s.splitOn ".").foldl Name.str Name.anonymous

def subroutine : Elab.TermElabM Unit := do
  let info? := (← MonadEnv.getEnv).find? (str_to_name "Nat.add_comm")
  match info? with
  | none => IO.println "Not found"
  | some info =>
    let format ← Lean.Meta.ppExpr info.toConstantVal.type
    IO.println <| toString format

def setOptionFromString' (opts : Options) (entry : String) : IO Options := do
  let ps := (entry.splitOn "=").map String.trim
  let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
  let key := str_to_name key
  let defValue ← getOptionDefaultValue key
  match defValue with
  | DataValue.ofString _ => pure $ opts.setString key val
  | DataValue.ofBool _   =>
    match val with
    | "true" => pure $ opts.setBool key true
    | "false" => pure $ opts.setBool key false
    | _ => throw $ IO.userError s!"invalid Bool option value '{val}'"
  | DataValue.ofName _   => pure $ opts.setName key val.toName
  | DataValue.ofNat _    =>
    match val.toNat? with
    | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
    | some v => pure $ opts.setNat key v
  | DataValue.ofInt _    =>
    match val.toInt? with
    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
    | some v => pure $ opts.setInt key v
  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")

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

When I run this with pp.explicit:

lean --run Examples/PrintExpr.lean pp.explicit=true

it gives

∀ (n m : Nat),
  @Eq Nat (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n m)
    (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) m n)

How can I make this print Nat.add m n instead of HAdd?

[Wojciech Nawrocki]

The operation there is HAdd.hAdd so it wouldn't really make sense to pretty-print it as anything else. You could either normalize the term so that definitional unfolding gets you Nat.add (but it might normalize further without stopping at that), or write some custom code to see through type class instances and find out that in this case the instance points to Nat.add.

[Max Nowak 🐉]

Maybe just beta-reducing @HAdd.hAdd Nat Nat Nat (instHAdd...) (without m and n) would be enough?

[Max Nowak 🐉]

A general heuristic would be to unfold TC instance projections, but I'm not sure if that might be overzealous.

[Wojciech Nawrocki]

(Another way to put it is that pretty printing sometimes works modulo alpha-equivalence but does not do general definitional computation.)

[Leni Aniva]

Wojciech Nawrocki said:

The operation there is HAdd.hAdd so it wouldn't really make sense to pretty-print it as anything else. You could either normalize the term so that definitional unfolding gets you Nat.add (but it might normalize further without stopping at that), or write some custom code to see through type class instances and find out that in this case the instance points to Nat.add.

which normalisation function should I call?

[Wojciech Nawrocki]

@Leni V. Aniva what are you trying to do that needs this? It sounds like a bit of an #xy problem. There is a function here in LeanSMT that does a similar thing.

[Leni Aniva]

Wojciech Nawrocki said:

Leni V. Aniva what are you trying to do that needs this? It sounds like a bit of an #xy problem. There is a function here in LeanSMT that does a similar thing.

I promise this isn't an xy problem. I need the concrete instantiated functions to train ML algorithms

[Mario Carneiro]

printing the instance itself would be sufficient to disambiguate it if that's what you want

[Leni Aniva]

Mario Carneiro said:

printing the instance itself would be sufficient to disambiguate it if that's what you want

Do you mean with pp.instances? Even with these options set:

--pp.instances=true --pp.notation=false --pp.instanceTypes=true      20:03:03

I get this for Nat.add_comm, which does not show the instances

∀ (n m : Nat), Eq (HAdd.hAdd n m) (HAdd.hAdd m n)

[Mario Carneiro]

pp.explicit should work

[Leni Aniva]

Mario Carneiro said:

pp.explicit should work

if this is the only solution I'll just settle for

@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) n m

[Mario Carneiro]

I think that in general it's not really well defined what the answer is if you want something else

[Leni Aniva]

Mario Carneiro said:

I think that in general it's not really well defined what the answer is if you want something else

I see. Thanks! I'll just have to have the ML model work harder