diff --git a/tests/lean/run/CompilerProbe.lean b/tests/lean/run/CompilerProbe.lean index 55f8242ed2..63011df5ae 100644 --- a/tests/lean/run/CompilerProbe.lean +++ b/tests/lean/run/CompilerProbe.lean @@ -32,19 +32,8 @@ def lambdaCounter : Probe Decl Nat := -- Find most commonly used function with threshold #eval Probe.runOnModule `Lean.Compiler.LCNF.JoinPoints (phase := .mono) <| - Probe.getExprs >=> - Probe.filter (fun e => return e.isApp && e.getAppFn.isConst) >=> - Probe.map (fun e => return s!"{e.getAppFn.constName!}") >=> + Probe.getLetExprs >=> + Probe.filter (fun e => return e matches .const ..) >=> + Probe.map (fun | .const declName .. => return s!"{declName}" | _ => unreachable!) >=> Probe.countUniqueSorted >=> Probe.filter (fun (_, count) => return count > 100) - --- To get that real shell feeling -infixr:55 " | " => Bind.kleisliRight - -#eval - Probe.runOnModule `Lean.Compiler.LCNF.JoinPoints (phase := .mono) <| - Probe.getExprs | - Probe.filter (fun e => return e.isApp && e.getAppFn.isConst) | - Probe.map (fun e => return s!"{e.getAppFn.constName!}") | - Probe.countUniqueSorted | - Probe.filter (fun (_, count) => return count > 100) diff --git a/tests/lean/seqToCodeIssue.lean.expected.out b/tests/lean/seqToCodeIssue.lean.expected.out index 12c139450f..c46df158c2 100644 --- a/tests/lean/seqToCodeIssue.lean.expected.out +++ b/tests/lean/seqToCodeIssue.lean.expected.out @@ -10,8 +10,8 @@ return _x.4; cases b : EStateM.Result IO.Error PUnit PUnit | Bool.false => - let a.10 := 1; - goto _jp.2 a.10 a.1 + let _x.10 := 1; + goto _jp.2 _x.10 a.1 | Bool.true => - let a.11 := 0; - goto _jp.2 a.11 a.1 + let _x.11 := 0; + goto _jp.2 _x.11 a.1 diff --git a/tests/lean/unhygienicCode.lean.expected.out b/tests/lean/unhygienicCode.lean.expected.out index 55e2d190f6..28ddf181d7 100644 --- a/tests/lean/unhygienicCode.lean.expected.out +++ b/tests/lean/unhygienicCode.lean.expected.out @@ -65,22 +65,22 @@ def foo (x_1 : obj) : obj := let x_9 : obj := Lean.Syntax.node3 x_5 x_6 x_7 x_8 x_4; ret x_9[Compiler.result] size: 18 def foo n : Syntax := - let fst.1 := Syntax.missing; - let fst.2 := 1; + let _x.1 := Syntax.missing; + let _x.2 := 1; let _x.3 := false; - let fst.4 := SourceInfo.fromRef fst.1 _x.3; + let _x.4 := SourceInfo.fromRef _x.1 _x.3; let _x.5 := "UnhygienicMain"; - let fst.6 := Name.mkStr1 _x.5; + let _x.6 := Name.mkStr1 _x.5; let _x.7 := "term_+_"; let _x.8 := Name.mkStr1 _x.7; let _x.9 := "a"; let _x.10 := String.toSubstring' _x.9; let _x.11 := Name.mkStr1 _x.9; - let _x.12 := addMacroScope fst.6 _x.11 fst.2; + let _x.12 := addMacroScope _x.6 _x.11 _x.2; let _x.13 := [] _; - let _x.14 := Syntax.ident fst.4 _x.10 _x.12 _x.13; + let _x.14 := Syntax.ident _x.4 _x.10 _x.12 _x.13; let _x.15 := "+"; - let _x.16 := Syntax.atom fst.4 _x.15; + let _x.16 := Syntax.atom _x.4 _x.15; let _x.17 := Lean.instQuoteNatNumLitKind._elam_0 n; - let _x.18 := Syntax.node3 fst.4 _x.8 _x.14 _x.16 _x.17; + let _x.18 := Syntax.node3 _x.4 _x.8 _x.14 _x.16 _x.17; return _x.18