From daa4e18ea70cf1800870cdf6634bb3388322a8be Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 7 Jul 2020 12:48:34 +0000 Subject: [PATCH 1/7] Add script by Floris --- scripts/typeclass_stats.lean | 60 ++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 scripts/typeclass_stats.lean diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean new file mode 100644 index 0000000000000..fec7e8669adb9 --- /dev/null +++ b/scripts/typeclass_stats.lean @@ -0,0 +1,60 @@ +import all + +open tactic declaration environment native + +meta def pos_line (p : option pos) : string := +match p with +| some x := to_string x.line +| _ := "" +end + +/- prints information about `decl` if it is an instance or a class. If `print_args` is true, it also prints + arguments of the class as "instances" (like `topological_monoid -> monoid`). -/ +meta def print_item_yaml (env : environment) (print_args : bool) (decl : declaration) + : tactic unit := +let name := decl.to_name in +do + when (env.decl_olean name).is_some $ do + olean_file ← env.decl_olean name, + let s:= ":\n File: " ++ olean_file ++ "\n Line: " ++ + pos_line (env.decl_pos name), + tactic.has_attribute `instance name >> (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), + trace $ to_string decl.to_name ++ s, + trace " Type: instance", + trace $ " Source: " ++ src, + trace $ " Target: " ++ tgt) <|> + tactic.has_attribute `class name >> (do + (l, tgt) ← return decl.type.pi_binders, + guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit), + trace $ to_string decl.to_name ++ s, + trace " Type: class", + when print_args $ l.tail.mmap' (λ arg, do + let nm := arg.type.erase_annotations.get_app_fn.const_name.to_string, + trace $ "arg_of_" ++ decl.to_name.to_string ++ "_" ++ nm ++ s, + trace " Type: instance", + trace $ " Source: " ++ decl.to_name.to_string, + trace $ " Target: " ++ nm) + ) <|> + skip + +/-- 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, + (curr_env.fold list.nil list.cons).mmap' (print_item_yaml curr_env tt) + +meta def test : tactic unit := +do curr_env ← get_env, + d ← get_decl `topological_monoid, + trace (to_string d.to_name), + print_item_yaml curr_env tt d + +-- run_cmd test +run_cmd print_content + From 2f49c7526dfcd937476e3084c055288de983a661 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 7 Jul 2020 16:52:46 +0000 Subject: [PATCH 2/7] jsonify the output --- scripts/typeclass_stats.lean | 148 ++++++++++++++++++++++++++--------- 1 file changed, 111 insertions(+), 37 deletions(-) diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean index fec7e8669adb9..850f90cc283fe 100644 --- a/scripts/typeclass_stats.lean +++ b/scripts/typeclass_stats.lean @@ -1,4 +1,4 @@ -import all +import algebra.group.defs open tactic declaration environment native @@ -8,53 +8,127 @@ match p with | _ := "" end -/- prints information about `decl` if it is an instance or a class. If `print_args` is true, it also prints - arguments of the class as "instances" (like `topological_monoid -> monoid`). -/ -meta def print_item_yaml (env : environment) (print_args : bool) (decl : declaration) - : tactic unit := +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 - when (env.decl_olean name).is_some $ do + if (env.decl_olean name).is_some + then do olean_file ← env.decl_olean name, - let s:= ":\n File: " ++ olean_file ++ "\n Line: " ++ - pos_line (env.decl_pos name), - tactic.has_attribute `instance name >> (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), - trace $ to_string decl.to_name ++ s, - trace " Type: instance", - trace $ " Source: " ++ src, - trace $ " Target: " ++ tgt) <|> - tactic.has_attribute `class name >> (do - (l, tgt) ← return decl.type.pi_binders, - guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit), - trace $ to_string decl.to_name ++ s, - trace " Type: class", - when print_args $ l.tail.mmap' (λ arg, do - let nm := arg.type.erase_annotations.get_app_fn.const_name.to_string, - trace $ "arg_of_" ++ decl.to_name.to_string ++ "_" ++ nm ++ s, - trace " Type: instance", - trace $ " Source: " ++ decl.to_name.to_string, - trace $ " Target: " ++ nm) - ) <|> - skip + 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) -/ + 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, - (curr_env.fold list.nil list.cons).mmap' (print_item_yaml curr_env tt) + 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 `topological_monoid, + d ← get_decl `comm_monoid.to_comm_semigroup, trace (to_string d.to_name), - print_item_yaml curr_env tt d + o ← parse_decl curr_env d, + trace (to_string o), + skip -- run_cmd test -run_cmd print_content +run_cmd print_content From ff0aa017226a65de0e42cd395a9ac769b34dbd78 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 7 Jul 2020 17:00:56 +0000 Subject: [PATCH 3/7] If line data is missing, return null --- scripts/typeclass_stats.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean index 850f90cc283fe..310adb264f267 100644 --- a/scripts/typeclass_stats.lean +++ b/scripts/typeclass_stats.lean @@ -5,7 +5,7 @@ open tactic declaration environment native meta def pos_line (p : option pos) : string := match p with | some x := to_string x.line -| _ := "" +| _ := "null" end def prepare_filename₁ : string → list string := From 10308ebf37a115ec624b0bfdc48ef930b6616eef Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 7 Jul 2020 19:45:07 +0000 Subject: [PATCH 4/7] golf code, thanks Kyle and Rob --- scripts/typeclass_stats.lean | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean index 310adb264f267..c19c15e3239e3 100644 --- a/scripts/typeclass_stats.lean +++ b/scripts/typeclass_stats.lean @@ -93,18 +93,6 @@ do 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), @@ -113,7 +101,7 @@ def list.split_sum : list (α ⊕ β) → (list α) × (list β) 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, + let (ns, es) := o.reduce_option.partition_map id, trace "{ \"nodes\" : \n", trace (to_string ns), trace ",\n \"edges\" :\n", From 4203a9db32ebc8ebf5d08c1ddb1fc465aa0d32fc Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 7 Jul 2020 19:53:30 +0000 Subject: [PATCH 5/7] uncomment guards --- scripts/typeclass_stats.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean index c19c15e3239e3..9bf8881b5325f 100644 --- a/scripts/typeclass_stats.lean +++ b/scripts/typeclass_stats.lean @@ -83,11 +83,11 @@ 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), + 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), + guard (src ≠ tgt), let E : edge := { source := src, target := tgt, .. I }, return (some (sum.inr E)) else do return none From eb41da46917d9e884e680668d1b63ce20c8f58a7 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 7 Jul 2020 19:59:44 +0000 Subject: [PATCH 6/7] Fix another guard mistake, thanks Floris --- scripts/typeclass_stats.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean index 9bf8881b5325f..6cebfc0f2c205 100644 --- a/scripts/typeclass_stats.lean +++ b/scripts/typeclass_stats.lean @@ -75,15 +75,15 @@ do file := filename olean_file, line := pos_line (env.decl_pos name), topic := topic olean_file }, + (l, tgt) ← return decl.type.pi_binders, + guard (l.tail.all $ λ b, b.info = binder_info.inst_implicit), is_c ← succeeds (tactic.has_attribute `class name), - if is_c then - let N : node := { .. I } in + if is_c then do + let N : node := { .. I }, 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, From dc23da19e917d9d20d32f28ebe9065a6b4416960 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Wed, 8 Jul 2020 07:10:22 +0200 Subject: [PATCH 7/7] Update scripts/typeclass_stats.lean Co-authored-by: Floris van Doorn --- scripts/typeclass_stats.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/typeclass_stats.lean b/scripts/typeclass_stats.lean index 6cebfc0f2c205..55e63e25a9cfd 100644 --- a/scripts/typeclass_stats.lean +++ b/scripts/typeclass_stats.lean @@ -100,8 +100,8 @@ do (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.reduce_option.partition_map id, + o ← (curr_env.fold [] list.cons).mmap_filter (λ x, parse_decl curr_env x <|> pure none), + let (ns, es) := o.partition_map id, trace "{ \"nodes\" : \n", trace (to_string ns), trace ",\n \"edges\" :\n",