diff --git a/examples/pil-fun/tests/gens/scala3/expected b/examples/pil-fun/tests/gens/scala3/expected new file mode 100644 index 000000000..7e594f27c --- /dev/null +++ b/examples/pil-fun/tests/gens/scala3/expected @@ -0,0 +1,167 @@ +------------------- + + +@main +def tvlt(): Unit = { + if (5.+(0)) < (2.+(2)) then { + var lybokfpr = (4.+(5)).+(4.+(5)) + lybokfpr = lybokfpr + lybokfpr = 4.+(lybokfpr + 1) + lybokfpr = lybokfpr + var uo: Boolean = (lybokfpr + lybokfpr).==(3 + 0) + + } else { + val qemiujv = (jjh: Int, gxdtmng: Int, zdkvk: Int, n: Int, zadrbgu: Boolean) => { + if (jjh + n) == zdkvk then + extension (cuohsl: Int) + def zmuqm(lnevjvz: Boolean, ssl: Int, ltiv: Int): Int = { + if (true.&&(true)).||(zadrbgu) then + if lnevjvz.&&(false && (!(zadrbgu))) then + {} + + else + if (ltiv.==(zdkvk)) || (ssl.<(4)) then + {} + else + {} + + (ssl.+(5)) + (n.+(6)) + } : Int + + else + extension (r: Int) + def mrew(nbasrya: Int, jqaak: Boolean, jpinulqg: Boolean, kazmm: Boolean) = + {} + def qsokaogqmr() = { } + + val mbn = jjh.+(1) + val ltpicdael: Int = 6 + var woyvgazf: Int = (4 + 0).+(6 + n) + + } : Unit + if (3 == 1) && (0.==(4)) then + if (2 + 1).==(1 + 2) then + extension (r: Int) def naqxvjgxmb() = { 4 <= (r + 1) } + qemiujv(1, 6, 5.+(4), 4.+(0), (1.naqxvjgxmb()).||(false.||(true))) + + else + if false then + {} + else + if true.||(false && false) then { + + } + + var wf: Boolean = (2.+(2)).<(2 + 2) + + extension (xmfo: Boolean) + def qnog(jg: Boolean, tzmk: Int, ogkzgnyugn: Int, bzyegcnug: Int) = { + qemiujv(3, 0, 0, tzmk.+(6), 5 < (tzmk + 6)) + + } + + else + var yqavod = false && true + qemiujv(6, 0, 0.+(4), 4.+(1), yqavod || (yqavod && yqavod)) + val sxfdzhrrh = (zbdd: Boolean, acoykh: Boolean, cbde: Boolean, dngc: Boolean, bqf: Boolean, drzqpmieuq: Boolean) => + {} + + if false || (2 <= 4) then + val obaztbbz: Boolean = (1.+(2)).==(2 + 6) + + else + val ji: Boolean = (2 + 4).==(0.+(1)) + val xsjzzhjk = (rbjd: Boolean, msoanazo: Int, dbbygddcsy: Boolean, j: Int, ots: Boolean, axwjjdtw: Boolean) => { } + + + } + val jrqa: Boolean = !(false) + extension (yannoshffy: Int) + def kwc(qnbouij: Int, mtsapbnquq: Int): Unit = + var k: Boolean = true + k = !(!(!(jrqa))) + + val llqkzrga = (deszncso: Boolean, dtwbodm: Boolean, wvqqvju: Boolean) => { + var x = (wvqqvju.&&(true)).||(4 == 5) + x = true + (6.+(3)).+(0.+(1)) + } + +} +------------------- + +val kwyflaeizb = (0.+(5)).+(3.+(5)) +val wfjunn = kwyflaeizb.+(kwyflaeizb + kwyflaeizb) +var lisrdrrgc: Int = 4.+(1) +val bh = (agieo: Boolean, qazggfrct: Int) => + if (0.<=(3)) && (!(false)) then { + var fwiklya = lisrdrrgc + + } else { + extension (psmyvssee: Int) def kmcysd(mc: Boolean, m: Int, kpwfobj: Int, g: Boolean, sk: Boolean) = { } + + } + lisrdrrgc = (kwyflaeizb + qazggfrct).+(kwyflaeizb.+(5)) + 6 +val qrnqnfy = (yovn: Boolean, t: Boolean) => { + if (true.||(yovn)) || yovn then { + + } + yovn +} + +@main +def chojxe(): Unit = { + if 1 < (kwyflaeizb.+(5)) then + {} + else + {} + +} +------------------- + +extension (xirzqm: Boolean) + def efqu(): Unit = + val tmxsbu = (5 == 6) && (!(false)) + var xnzeyxyo: Boolean = 4 == (3 + 4) + extension (kg: Boolean) + def doxdnly() = { + if (1.+(5)).<=(5 + 4) then { + xnzeyxyo = true + + } + if true then + {} + else + {} + + } + var drjp: Boolean = (0 == 0).||(xirzqm && false) + if tmxsbu && (tmxsbu && false) then { + + } + +var cstczqacp = (0 + 3) == (5 + 5) + +@main +def japky(): Unit = { + if cstczqacp then { + (4 < (0.+(1))).efqu() + extension (faco: Boolean) + def f(vunluob: Int, xgriaerel: Boolean, rhn: Boolean, ffmlvduuc: Boolean, l: Boolean): Unit = { + (5.==(vunluob)).efqu() + + } : Unit + val tkhyrdnc = () => { (0.+(0)).==(3) } : Boolean + + } else { + var gfknyi: Int = (1.+(3)) + (5.+(6)) + var quusqeb = (4 + 4) + (gfknyi.+(2)) + cstczqacp.efqu() + + } + var cyopq: Int = (0 + 2) + (3 + 2) + cstczqacp = cstczqacp && (true.&&(cstczqacp)) + val ycchap: Boolean = false + +} diff --git a/examples/pil-fun/tests/gens/scala3/run b/examples/pil-fun/tests/gens/scala3/run new file mode 100755 index 000000000..7307aaedb --- /dev/null +++ b/examples/pil-fun/tests/gens/scala3/run @@ -0,0 +1,6 @@ +rm -rf build + +flock "$1" pack -q install-deps pil-fun && \ +pack run pil-fun scala3 --seed 0,3 --tests 3 --model-fuel 6 + +rm -rf build diff --git a/tests/derivation/core/big con 001/DerivedGen.idr b/tests/derivation/core/big con 001/DerivedGen.idr new file mode 100644 index 000000000..da85e783f --- /dev/null +++ b/tests/derivation/core/big con 001/DerivedGen.idr @@ -0,0 +1,28 @@ +module DerivedGen + +import RunDerivedGen + +import Deriving.Show + +%default total + +%language ElabReflection + +record X where + constructor MkX + field1 : Nat + field2 : Nat + field3 : Nat + field4 : Nat + field5 : Nat + field6 : Nat + field7 : Nat + field8 : Nat + +%hint ShowX : Show X; ShowX = %runElab derive + +checkedGen : Fuel -> Gen MaybeEmpty X +checkedGen = deriveGen + +main : IO () +main = runGs [ G checkedGen ] diff --git a/tests/derivation/core/big con 001/RunDerivedGen.idr b/tests/derivation/core/big con 001/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/core/big con 001/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/core/big con 001/derive.ipkg b/tests/derivation/core/big con 001/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/core/big con 001/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/core/big con 001/expected b/tests/derivation/core/big con 001/expected new file mode 100644 index 000000000..699cbef9a --- /dev/null +++ b/tests/derivation/core/big con 001/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkX 16 4 17 10 10 17 5 4 +----- +MkX 12 11 8 15 4 14 7 4 +----- +MkX 10 1 15 20 0 17 13 17 +----- +MkX 17 12 2 18 13 10 14 16 +----- +MkX 16 11 1 3 3 10 12 17 +----- +MkX 19 7 3 16 6 12 18 2 +----- +MkX 8 1 18 15 1 7 0 5 +----- +MkX 15 19 3 19 9 6 4 0 +----- +MkX 3 13 19 5 20 3 1 13 +----- +MkX 9 5 0 7 4 7 6 16 diff --git a/tests/derivation/core/big con 001/run b/tests/derivation/core/big con 001/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/core/big con 001/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/core/big con 002/DerivedGen.idr b/tests/derivation/core/big con 002/DerivedGen.idr new file mode 100644 index 000000000..5db00aa16 --- /dev/null +++ b/tests/derivation/core/big con 002/DerivedGen.idr @@ -0,0 +1,32 @@ +module DerivedGen + +import RunDerivedGen + +import Deriving.Show + +%default total + +%language ElabReflection + +record X where + constructor MkX + field0 : Nat + field1 : Nat + field2 : Nat + field3 : Nat + field4 : Nat + field5 : Nat + field6 : Nat + field7 : Nat + field8 : Nat + field9 : Nat + field10 : Nat + field11 : Nat + +%hint ShowX : Show X; ShowX = %runElab derive + +checkedGen : Fuel -> Gen MaybeEmpty X +checkedGen = deriveGen + +main : IO () +main = runGs [ G checkedGen ] diff --git a/tests/derivation/core/big con 002/RunDerivedGen.idr b/tests/derivation/core/big con 002/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/core/big con 002/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/core/big con 002/derive.ipkg b/tests/derivation/core/big con 002/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/core/big con 002/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/core/big con 002/expected b/tests/derivation/core/big con 002/expected new file mode 100644 index 000000000..7cb77e0d7 --- /dev/null +++ b/tests/derivation/core/big con 002/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +MkX 16 4 17 10 10 17 5 4 12 11 8 15 +----- +MkX 4 14 7 4 10 1 15 20 0 17 13 17 +----- +MkX 17 12 2 18 13 10 14 16 16 11 1 3 +----- +MkX 3 10 12 17 19 7 3 16 6 12 18 2 +----- +MkX 8 1 18 15 1 7 0 5 15 19 3 19 +----- +MkX 9 6 4 0 3 13 19 5 20 3 1 13 +----- +MkX 9 5 0 7 4 7 6 16 3 6 4 5 +----- +MkX 10 11 2 11 12 13 19 15 5 7 10 18 +----- +MkX 2 14 9 7 20 13 3 10 17 7 6 20 +----- +MkX 19 13 5 1 20 12 19 17 2 12 20 14 diff --git a/tests/derivation/core/big con 002/run b/tests/derivation/core/big con 002/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/core/big con 002/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file