max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix some tests

Browse source
This commit is contained in:
Leonardo de Moura 2022-11-07 17:40:49 -08:00
parent 9399164201
commit d11697cbf7
3 changed files with 15 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
tests/lean/run/CompilerProbe.lean
View file

@ -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)

8
tests/lean/seqToCodeIssue.lean.expected.out
View file

@ -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

16
tests/lean/unhygienicCode.lean.expected.out
View file

@ -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