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

chore: fix and disable some LCNF tests

Browse source 
We still need to port code to the new architecture
This commit is contained in:
Leonardo de Moura 2022-08-24 14:11:57 -07:00
parent 9b28878615
commit 85866fc238
7 changed files with 5 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/casesOnCases.lean
View file

@ -12,5 +12,5 @@ def isZero (x : Nat) :=
#eval Lean.Compiler.compile #[``isZero]
set_option trace.Compiler.simp true
-- set_option trace.Compiler.simp true -- TODO: uncomment
#eval Lean.Compiler.compile #[``isZero]

3
tests/lean/casesOnCases.lean.expected.out
View file

@ -1,3 +1,2 @@
[Compiler.simp] isZero : Nat → Bool :=
fun x => Nat.casesOn x true fun n => false

2
tests/lean/inlineIssue.lean
View file

@ -15,5 +15,5 @@ def f (x : Nat) :=
#eval Lean.Compiler.compile #[``f]
set_option trace.Compiler.simp true
-- set_option trace.Compiler.simp true -- TODO: uncomment
#eval Lean.Compiler.compile #[``f]

45
tests/lean/inlineIssue.lean.expected.out
View file

@ -1,45 +1,2 @@
[Compiler.simp] f : Nat → Nat :=
fun x =>
let h.14 := fun x_1 =>
Nat.casesOn x_1
(let _x.82 := Nat.mul x x_1;
let _x.85 := Nat.mul _x.82 x;
let _x.88 := Nat.mul _x.85 x_1;
Nat.mul _x.88 x_1)
fun n => Nat.add n x_1;
let _x.15 := 1;
let _x.95 := Nat.add x _x.15;
let _x.19 := h.14 _x.95;
let _x.20 := 2;
let _x.98 := Nat.add x _x.20;
let _x.24 := h.14 _x.98;
let _x.101 := Nat.add _x.19 _x.24;
let _x.26 := 3;
let _x.104 := Nat.add x _x.26;
let _x.30 := h.14 _x.104;
let _x.107 := Nat.add _x.101 _x.30;
let _x.32 := 4;
let _x.110 := Nat.add x _x.32;
let _x.36 := h.14 _x.110;
let _x.113 := Nat.add _x.107 _x.36;
let _x.38 := 5;
let _x.116 := Nat.add x _x.38;
let _x.42 := h.14 _x.116;
let _x.119 := Nat.add _x.113 _x.42;
let _x.44 := 6;
let _x.122 := Nat.add x _x.44;
let _x.48 := h.14 _x.122;
let _x.125 := Nat.add _x.119 _x.48;
let _x.50 := 7;
let _x.128 := Nat.add x _x.50;
let _x.54 := h.14 _x.128;
let _x.131 := Nat.add _x.125 _x.54;
let _x.56 := 8;
let _x.134 := Nat.add x _x.56;
let _x.60 := h.14 _x.134;
let _x.137 := Nat.add _x.131 _x.60;
let _x.62 := 9;
let _x.140 := Nat.add x _x.62;
let _x.66 := h.14 _x.140;
Nat.add _x.137 _x.66

24
tests/lean/interactive/completionOption.lean.expected.out
View file

@ -210,18 +210,6 @@
"kind": 10,
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"textEdit":
{"replace":
{"start": {"line": 10, "character": 11},
"end": {"line": 10, "character": 18}},
"newText": "trace.Compiler.pullLocalDecls.candidate",
"insert":
{"start": {"line": 10, "character": 11},
"end": {"line": 10, "character": 18}}},
"label": "trace.Compiler.pullLocalDecls.candidate",
"kind": 10,
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"textEdit":
{"replace":
{"start": {"line": 10, "character": 11},
@ -234,18 +222,6 @@
"kind": 10,
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"textEdit":
{"replace":
{"start": {"line": 10, "character": 11},
"end": {"line": 10, "character": 18}},
"newText": "trace.Compiler.simp.projInst",
"insert":
{"start": {"line": 10, "character": 11},
"end": {"line": 10, "character": 18}}},
"label": "trace.Compiler.simp.projInst",
"kind": 10,
"detail":
"(false), enable/disable tracing for the given module and submodules"},
{"textEdit":
{"replace":
{"start": {"line": 10, "character": 11},

2
tests/lean/lcnfTypes.lean
View file

@ -3,7 +3,7 @@ import Lean
notation "◾" => lcErased
notation "⊤" => lcAny
open Lean Compiler Meta
open Lean Compiler LCNF Meta
def test (declName : Name) : MetaM Unit := do
IO.println s!"{declName} : {← ppExpr (← getDeclLCNFType declName)}"

4
tests/lean/run/lcnf1.lean
View file

@ -106,7 +106,3 @@ def gebner2 (x : UInt64) := x &&& ((1 : UInt64) <<< 5 : UInt64)
#eval Compiler.compile #[``instMonadEIO]
-- set_option pp.explicit true in
#eval Compiler.compile #[``EStateM.instMonadEStateM]
#eval do
let some decl ← Compiler.getStage1Decl? ``List.length | throwError "not found"
IO.println (← decl.toString)