Zulip Chat Archive

Stream: general

Topic: graphs: tc hierarchy


view this post on Zulip Johan Commelin (May 28 2020 at 09:54):

@Floris van Doorn you had some scripts that generated graphs of the type class hierarchy. Is that right? Do you still have them somewhere?

view this post on Zulip Johan Commelin (May 28 2020 at 09:54):

If so, we can probably teach them to output json.

view this post on Zulip Floris van Doorn (May 29 2020 at 05:13):

Yes, and I put it here: https://gist.github.com/fpvandoorn/4d4c52322d7eb661e5154f9a732754d4

It currently produces output like this:

partial_order:
  File: C:\Users\Floris\.elan\toolchains\leanprover-community-lean-3.14.0\lib\lean\library\init\algebra\order.lean
  Line: 26
  Type: class
semilattice_inf_bot_of_bounded_lattice:
  File: d:\projects\mathlib\src\order\bounded_lattice.lean
  Line: 250
  Type: instance
  Source: bounded_lattice
  Target: semilattice_inf_bot
group.to_has_inv:
  File: d:\projects\mathlib\src\algebra\group\basic.lean
  Line: 219
  Type: instance
  Source: group
  Target: has_inv
order_bot:
  File: d:\projects\mathlib\src\order\bounded_lattice.lean
  Line: 94
  Type: class
[...]

It shouldn't be hard to modify the output.

It currently mostly prints "the algebraic hierarchy". This means instances and classes that have at most 1 argument that is not a type-class argument (within square brackets), and the instances can only be forgetful instances (where the conclusion is a class applied to a variable).

view this post on Zulip Floris van Doorn (May 29 2020 at 05:13):

What is the output you want, and how do you want to use it? Automatically generating a graph would be nice.

view this post on Zulip Johan Commelin (May 29 2020 at 06:37):

The idea would be to automatically generated an interactive graph using d3.js

view this post on Zulip Johan Commelin (May 29 2020 at 06:37):

So the output should probably be some sort of json, although Patrick also linked to a package that can convert .dot files into d3 graphs.

view this post on Zulip Johan Commelin (Jun 01 2020 at 08:29):

@Bryan Gin-ge Chen The output of the script by Floris (see above) is yaml... is that ok for you? I guess we can easily postprocess that into suitable json, right?

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 15:02):

Yes, it shouldn't be too hard to postprocess. I bet the script could be modified to output JSON pretty easily too though.

view this post on Zulip Johan Commelin (Jun 01 2020 at 15:30):

Right, that's what I thought. What kind of JSON format are we looking for?

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 15:47):

For experimentation we can just go with whatever's quickest to implement.

view this post on Zulip Johan Commelin (Jun 01 2020 at 16:10):

Should it look like

[ # a list of edges
{ source : 'group', target: 'monoid' },
{ blabbla },
]

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 16:14):

Yeah, I think that would work fine (modulo correct JSON syntax :wink: )

view this post on Zulip Johan Commelin (Jun 01 2020 at 16:24):

/me doesn't really know json

view this post on Zulip Johan Commelin (Jun 01 2020 at 16:24):

I'll try to hack the output into that form once my kids are in bed

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 16:30):

No worries, I probably won't have time to play around with graphs until the weekend, and I can probably quickly do this myself then.

view this post on Zulip Floris van Doorn (Jun 01 2020 at 18:22):

There's also the question what you want the content of the graph to be exactly. The algebraic hierarchy? All type-classes?
I think currently my script gives you a bit more than the algebraic hierarchy. It gives you all "unary type-classes" but I think there are also some typeclasses with argument m : Type u -> Type u which you might want to remove.

view this post on Zulip Johan Commelin (Jun 01 2020 at 19:03):

I was thinking initially just all type classes...

view this post on Zulip Johan Commelin (Jun 01 2020 at 19:03):

But maybe you get lots of junk then?

view this post on Zulip Floris van Doorn (Jun 01 2020 at 19:19):

Well, if your idea is to get a graph similar to the one in the mathlib paper, then I recommend just using the algebraic hierarchy + "forgetful" instances. For other classes/instances it's a lot less clear what arrows to draw.
What arrows represent group A -> group B -> group (A x B) or decidable_eq A -> decidable_eq (list A) or decidable_eq real?

view this post on Zulip Johan Commelin (Jun 01 2020 at 19:21):

Hmmm, I hadn't really thought about the edges, I think. Your suggestion sounds good to me.

view this post on Zulip Johan Commelin (Jul 06 2020 at 18:04):

I'm going to try to generate an update version of this graph for the workshop

view this post on Zulip Johan Commelin (Jul 06 2020 at 18:05):

Now it would be great if we could reuse some sphere eversion machinery (@Patrick Massot) to create a clickable version that takes you to the corresponding page in the docs.

view this post on Zulip Patrick Massot (Jul 06 2020 at 18:10):

That part is very easy. The tricky part is to have a meaningful manageable graph to display.

view this post on Zulip Johan Commelin (Jul 06 2020 at 18:21):

I just ran the script by Floris. It generates a graph with 120 edges.

view this post on Zulip Johan Commelin (Jul 06 2020 at 18:22):

Oops, that's wrong

view this post on Zulip Johan Commelin (Jul 06 2020 at 18:25):

My new count is about 520 nodes and 400 edges. Which still seems weird.

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:49):

I'm trying to make the script by Floris output two JSON lists, one with nodes, and one with edges. But I'm bad at meta stuff. Here is what I have so far:

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def file_to_topic : string  string :=
λ s, (s.split_on '/').head

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string := file_to_topic file)

structure node extends item.

namespace node

def jsonify : node  string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := jsonify

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge  string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := jsonify

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node  edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file  env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := olean_file,
        line := pos_line (env.decl_pos name) },
      is_c  tactic.has_attribute `class name,
      if is_c.1 then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i  tactic.has_attribute `instance name,
      if is_i.1 then do
        (l, tgt)  return decl.type.pi_binders,
        guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        guard (src  tgt),
        let E : edge := { name := to_string name, source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α)  list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α  β)  (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env  get_env,
   o  (curr_env.fold list.nil list.cons).mmap (parse_decl curr_env),
   trace (to_string o.remove_none.split_sum),
   skip

meta def test : tactic unit :=
do curr_env  get_env,
   d  get_decl `comm_monoid,
   trace (to_string d.to_name),
   o  parse_decl curr_env d,
   trace (to_string o),
   skip

run_cmd test

run_cmd print_content

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:49):

If someone could help, that would be awesome.

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:51):

The idea is to be able to generate interactive graphs that will link to the correct docs.
We might need to tweak the info that we save in the nodes and edges.
Also, I want items to have a "topic" so that you can easily hide all the nodes that come from the subdirectory src/algebra, and focus on src/topology, etc...

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:51):

(The full graph will be too large to be useful.)

view this post on Zulip Rob Lewis (Jul 07 2020 at 14:53):

tactic.has_attribute returns a bool and a nat. The bool isn't whether the attribute is there or not, it's whether the attribute is persistent (non-local). has_attribute will fail if the attribute isn't there.

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:54):

Aha... so what do I do now?

view this post on Zulip Rob Lewis (Jul 07 2020 at 14:54):

You can use succeeds if you don't actually need the output of has_attribute, which I don't think you do.

view this post on Zulip Johan Commelin (Jul 07 2020 at 14:54):

Is there some sort of success thing? That I should prepend?

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:06):

I now have, but it still doesn't seem to work

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def file_to_topic : string  string :=
λ s, (s.split_on '/').head

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string := file_to_topic file)

structure node extends item.

namespace node

def jsonify : node  string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := jsonify

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge  string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := jsonify

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node  edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file  env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := olean_file,
        line := pos_line (env.decl_pos name) },
      is_c  succeeds (tactic.has_attribute `class name),
      if is_c then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i  succeeds (tactic.has_attribute `instance name),
      if is_i then do
        (l, tgt)  return decl.type.pi_binders,
        guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        guard (src  tgt),
        let E : edge := { source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α)  list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α  β)  (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env  get_env,
   o  (curr_env.fold [] list.cons).mmap (parse_decl curr_env),
   trace (to_string o.remove_none.split_sum),
   skip

meta def test : tactic unit :=
do curr_env  get_env,
   d  get_decl `comm_monoid.to_comm_semigroup,
   trace (to_string d.to_name),
   o  parse_decl curr_env d,
   trace (to_string o),
   skip

run_cmd test

run_cmd print_content

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:18):

This bit

meta def print_content : tactic unit :=
do curr_env  get_env,
   o  (curr_env.fold [] list.cons).mmap (parse_decl curr_env),
   skip

gives an error

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:18):

failed
state:
 true

view this post on Zulip Anne Baanen (Jul 07 2020 at 15:20):

It looks like the line guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var), is the one that fails. What is the goal of that check?

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:21):

I don't know... it was there in Floris's version

view this post on Zulip Anne Baanen (Jul 07 2020 at 15:23):

I'm guessing then that it detects declarations that we don't want to process. In that case, the issue is that the first failing declaration aborts the whole command, so we want to wrap the command in a <|> return none. Let's see if it helps...

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:23):

Without the guards it works!

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:23):

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def file_to_topic : string  string :=
λ s, (s.split_on '/').head

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string := file_to_topic file)

structure node extends item.

namespace node

def jsonify : node  string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := jsonify

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge  string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := jsonify

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node  edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file  env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := olean_file,
        line := pos_line (env.decl_pos name) },
      is_c  succeeds (tactic.has_attribute `class name),
      if is_c then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i  succeeds (tactic.has_attribute `instance name),
      if is_i then do
        (l, tgt)  return decl.type.pi_binders,
        -- guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        -- guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        -- guard (src ≠ tgt),
        let E : edge := { source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α)  list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α  β)  (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env  get_env,
   o  (curr_env.fold [] list.cons).mmap (parse_decl curr_env),
   let (ns, es) := o.remove_none.split_sum,
   trace (to_string ns),
   trace (to_string es),
   skip

meta def test : tactic unit :=
do curr_env  get_env,
   d  get_decl `comm_monoid.to_comm_semigroup,
   trace (to_string d.to_name),
   o  parse_decl curr_env d,
   trace (to_string o),
   skip

run_cmd test

run_cmd print_content

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:24):

Anne Baanen said:

I'm guessing then that it detects declarations that we don't want to process. In that case, the issue is that the first failing declaration aborts the whole command, so we want to wrap the command in a <|> return none. Let's see if it helps...

Ooh, that makes sense. Because I do indeed get garbage output if I simply comment out the guard.

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:25):

I don't know exactly where to put the <|> return none. Would be delighted if you show me.

view this post on Zulip Anne Baanen (Jul 07 2020 at 15:25):

I tried to put it around the call to parse_decl:

meta def print_content : tactic unit :=
do curr_env  get_env,
   o  (curr_env.fold [] list.cons).mmap (λ x, parse_decl curr_env x <|> pure none),
   trace (to_string o.remove_none.split_sum),
   skip

view this post on Zulip Anne Baanen (Jul 07 2020 at 15:26):

Then I get output like:

([{ name : partial_order,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/order.lean,
line : 26 }
, { name : has_coe_t_aux,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/coe.lean,
line : 123 }
, { name : is_cond_left_inv,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/classes.lean,
line : 55 }
, { name : is_total,
topic : ,
file : /home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/classes.lean,
line : 95 }
, ...

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:27):

Yup, same here...

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:27):

Now, all we need is a way to turn a filename into a topic

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:28):

Probably split_on '/', end then take the first thing after src, or after library.

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:29):

And for nice links to docs#foobar we probably need to save more stuff, like the full name.

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:29):

Or maybe name is already the full name... I don't know.

view this post on Zulip Anne Baanen (Jul 07 2020 at 15:33):

Johan Commelin said:

Probably split_on '/', end then take the first thing after src, or after library.

def file_to_topic : string  string :=
λ xs, ".".intercalate ((xs.split_on '/').drop_while (λ x, x  "library"  x  "src")).tail.init

view this post on Zulip Anne Baanen (Jul 07 2020 at 15:34):

Maps "/home/arch/arb/.elan/toolchains/leanprover-community-lean-3.17.0/lib/lean/library/init/algebra/classes.lean" to init.algebra

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:35):

Cool!

view this post on Zulip Johan Commelin (Jul 07 2020 at 15:36):

We'll have to play a bit with the exact value of this function, I guess. But this is a good start.

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:29):

This script should not be run by people that have a username library or src :wink:

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:42):

I'm reasonably happy with this version:

import algebra.group.defs

open tactic declaration environment native

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

def prepare_filename₁ : string  list string :=
λ xs, ((xs.split_on '/').drop_while (λ x, x  "library"  x  "src"))

def prepare_filename₂ : list string  list string
| ("library" :: l) := ("core" :: l)
| ("src" :: l)     := l
| _                := []

def filename : string  string :=
"/".intercalate  prepare_filename₂  prepare_filename₁

def topic : string  string :=
list.head  prepare_filename₂  prepare_filename₁

structure item :=
(file : string)
(line : string)
(name : string)
(topic : string)

structure node extends item.

namespace node

def jsonify : node  string :=
λ n,
"{ name : " ++ n.name ++ ",\n" ++
  "topic : " ++ n.topic ++ ",\n" ++
  "file : " ++ n.file ++ ",\n" ++
  "line : " ++ n.line ++ " }\n"

instance : has_to_string node := jsonify

end node

structure edge extends item :=
(source : string)
(target : string)

namespace edge

def jsonify : edge  string :=
λ e,
"{ name : " ++ e.name ++ ",\n" ++
  "topic : " ++ e.topic ++ ",\n" ++
  "source : " ++ e.source ++ ",\n" ++
  "target : " ++ e.target ++ ",\n" ++
  "file : " ++ e.file ++ ",\n" ++
  "line : " ++ e.line ++ " }\n"

instance : has_to_string edge := jsonify

end edge

/- parses information about `decl` if it is an instance or a class. -/
meta def parse_decl (env : environment) (decl : declaration) :
  tactic (option (node  edge)) :=
let name := decl.to_name in
do
    if (env.decl_olean name).is_some
    then do
      olean_file  env.decl_olean name,
      let I : item :=
      { name := to_string name,
        file := filename olean_file,
        line := pos_line (env.decl_pos name),
        topic := topic olean_file },
      is_c  succeeds (tactic.has_attribute `class name),
      if is_c then
        let N : node := { .. I } in
        return (some (sum.inl N))
      else do
      is_i  succeeds (tactic.has_attribute `instance name),
      if is_i then do
        (l, tgt)  return decl.type.pi_binders,
        -- guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),
        -- guard (tgt.get_app_args.head.is_var && l.ilast.type.get_app_args.head.is_var),
        let src := to_string l.ilast.type.erase_annotations.get_app_fn.const_name,
        let tgt := to_string tgt.erase_annotations.get_app_fn.const_name,
        -- guard (src ≠ tgt),
        let E : edge := { source := src, target := tgt, .. I },
        return (some (sum.inr E))
      else do return none
    else do return none

variables {α β : Type*}

def list.remove_none : list (option α)  list α
| []            := []
| (none :: l)   := l.remove_none
| (some a :: l) := a :: l.remove_none

def list.split_sum : list (α  β)  (list α) × (list β)
| []  := ([], [])
| ((sum.inl a) :: l) := let L := l.split_sum in ((a :: L.1), L.2)
| ((sum.inr b) :: l) := let L := l.split_sum in (L.1, (b :: L.2))

/-- prints information about unary classes and forgetful instances in the environment.
  It only prints instances and classes that have at most 1 argument
  that is not a type-class argument (within square brackets),
  and the instances can only be forgetful instances
  (where the conclusion is a class applied to a variable) -/
meta def print_content : tactic unit :=
do curr_env  get_env,
   o  (curr_env.fold [] list.cons).mmap (λ x, parse_decl curr_env x <|> pure none),
   let (ns, es) := o.remove_none.split_sum,
   trace "{ nodes : \n",
   trace (to_string ns),
   trace ",\n  edges :\n",
   trace (to_string es),
   trace "}",
   skip

meta def test : tactic unit :=
do curr_env  get_env,
   d  get_decl `comm_monoid.to_comm_semigroup,
   trace (to_string d.to_name),
   o  parse_decl curr_env d,
   trace (to_string o),
   skip

-- run_cmd test

run_cmd print_content

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:44):

See https://gist.github.com/jcommelin/da4a87f4d7d87b6e11e3308b5ba97771 for the output

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:44):

@Bryan Gin-ge Chen Is this the type of json file that you could turn into a nice D3 graph?

view this post on Zulip Bryan Gin-ge Chen (Jul 07 2020 at 16:45):

Almost! Just add double quotes around the key names and any string values.

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:46):

Ok, cool! Let me try that.

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:51):

@Bryan Gin-ge Chen Voila: https://gist.github.com/cffe869fe6ba0f154b15d45a2e4a08f2

view this post on Zulip Bryan Gin-ge Chen (Jul 07 2020 at 16:54):

SyntaxError: JSON.parse: unexpected character at line 580 column 11 of the JSON data. Something is still wrong, let me check...

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:55):

#3307 contains the script that I'm using.

view this post on Zulip Bryan Gin-ge Chen (Jul 07 2020 at 16:55):

Ah, line 580 looks like this: "line" : }. Maybe if there's no line data you'll want to put null there? Or just skip the line field entirely?

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:56):

Aah, there is an empty "line"

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:56):

Hmm, whatever you think is best.

view this post on Zulip Bryan Gin-ge Chen (Jul 07 2020 at 16:56):

I haven't been following, what would an empty line mean?

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:57):

meta def pos_line (p : option pos) : string :=
match p with
| some x := to_string x.line
| _      := ""
end

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:57):

We can turn the "" into "null".

view this post on Zulip Bryan Gin-ge Chen (Jul 07 2020 at 16:57):

Yeah, that would work.

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:58):

I have no idea what it means that p is none...

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:58):

@Bryan Gin-ge Chen https://gist.github.com/6d9da8c35a91cacb4a70d5c390c1d17f

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:59):

Ooh, that's the script

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:59):

https://gist.github.com/6e16f71a163a1dd42a1f9b3ec23f6a9b

view this post on Zulip Johan Commelin (Jul 07 2020 at 16:59):

That's updated output

view this post on Zulip Bryan Gin-ge Chen (Jul 07 2020 at 17:01):

OK, it parsed! I'll see what I can do later (possibly the weekend). I might prioritize looking at the Live Share stuff first though.

view this post on Zulip Johan Commelin (Jul 07 2020 at 17:01):

Ooh, Live Share would be awesome!

view this post on Zulip Johan Commelin (Jul 07 2020 at 17:01):

(I still didn't get it to work on my setup, though. Stupid MS sign-in page.)

view this post on Zulip Johan Commelin (Jul 07 2020 at 17:12):

I imagine something like https://observablehq.com/@peatroot/interacting-with-directed-acyclic-graphs, where we can hide nodes and edges depending on which topics are selected as "visible".
(I got that link from Bryan, in another thread.)

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:25):

Johan Commelin said:

I don't know... it was there in Floris's version

The goal of my script was to only print unary type classes and forgetful instances between them.

These guards were there to filter out instances that did not fall into this category.
The way my script was setup was that failing means the declaration was skipped.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:29):

Is a class like src#is_idempotent a class you want to print in your graph?

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:30):

Or an instance like src#nat.has_mod?

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:38):

I think I don't really care about those

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:39):

I would prefer to get a graph containing things like group, field, topological_space, normed_space, metric_space, topological_monoid, etc...

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:39):

But exactly how to characterise those... I dunno

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:49):

That's what my script did, and what those guard expressions did.
I'll modify your script to filter them out.

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:50):

To filter what out?

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:50):

@Floris van Doorn I think I want basically what your script did. And it seemed that it's what I have now... after Anne debugged it for me.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:51):

But your script also outputs a bunch of "junk", like the class and instance I mentioned above.

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:51):

Aha... no idea why it does that

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:51):

because you removed those guard expressions.

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:51):

Ooh, lol... I forgot to uncomment the guards

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:52):

This is how it starts after uncommenting them

{ "nodes" :

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_coe_t_aux",
"topic" : "core",
"file" : "core/init/coe.lean",
"line" : 123 }
, { "name" : "is_cond_left_inv",
"topic" : "core",
"file" : "core/init/algebra/classes.lean",
"line" : 55 }
, { "name" : "is_total",
"topic" : "core",
"file" : "core/init/algebra/classes.lean",
"line" : 95 }
, { "name" : "has_ssubset",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 340 }
, { "name" : "has_andthen",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 334 }
, { "name" : "is_cond_right_inv",
"topic" : "core",
"file" : "core/init/algebra/classes.lean",
"line" : 58 }

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:53):

Is there a reasonable way to filter out has_coe_t_aux? Or does is quack too much like a group or a topological monoid?

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:53):

It shouldn't be there, since it has two arguments. I think my original script filtered those out.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:54):

Things like has_mul and the like will of course be printed.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:55):

Just checked, my original script doesn't print has_coe_t_aux.

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:56):

Ok... I clearly blundered.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 19:56):

The line

guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit),

was there for both instances and classes, you removed it for classes. You can probably put it back, and it should filter those out.

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:58):

thanks!

view this post on Zulip Johan Commelin (Jul 07 2020 at 19:59):

I pushed to the PR

view this post on Zulip Johan Commelin (Jul 07 2020 at 20:00):

Output now starts with

{ "nodes" :

[{ "name" : "partial_order",
"topic" : "core",
"file" : "core/init/algebra/order.lean",
"line" : 26 }
, { "name" : "has_ssubset",
"topic" : "core",
"file" : "core/init/core.lean",
"line" : 340 }
, { "name" : "add_comm_group",
"topic" : "algebra",
"file" : "algebra/group/defs.lean",
"line" : 301 }
, { "name" : "add_left_cancel_semigroup",
"topic" : "algebra",
"file" : "algebra/group/defs.lean",
"line" : 106 }
, { "name" : "comm_group",
"topic" : "algebra",
"file" : "algebra/group/defs.lean",
"line" : 298 }

view this post on Zulip Johan Commelin (Jul 07 2020 at 20:00):

That looks quite promising.

view this post on Zulip Floris van Doorn (Jul 07 2020 at 20:08):

If you add guard l.head.type.is_sort (for both instances and classes), that should filter out things like monad.

view this post on Zulip Johan Commelin (Jul 07 2020 at 20:11):

Aha... I'm not sure if we want that... would it kill too much?

view this post on Zulip Floris van Doorn (Jul 07 2020 at 20:50):

I don't think so, what class on Type* -> Type* do you want to include in your graph?

view this post on Zulip Johan Commelin (Jul 08 2020 at 04:48):

Well, maybe we want to allow all the monad and functor etc..., because if you can easily switch them off using the topic field, why not support them?


Last updated: May 15 2021 at 00:39 UTC