diff --git a/.gitignore b/.gitignore index 4bf016557dd..f52bf6e7a76 100644 --- a/.gitignore +++ b/.gitignore @@ -6,3 +6,5 @@ **/_build **/_output /result* + +/samples/**/*.txt diff --git a/samples/app/main.txt b/samples/app/main.txt deleted file mode 100644 index d5ae2f746fd..00000000000 --- a/samples/app/main.txt +++ /dev/null @@ -1,205 +0,0 @@ --- Parsing list.as: --- Parsing types.as: --- Parsing server.as: --- Parsing client.as: --- Parsing main.as: --- Checking all: -type Client = actor {go : shared (Text, Server) -> (); send : shared Text -> ()} -type ClientData = {client : Client; id : Nat; revoked : var Bool} -type List = ?{head : T; tail : var List} -type Server = actor {subscribe : shared Client -> async Subscription} -type Subscription = shared {cancel : shared () -> (); post : shared Text -> ()} -let Client : () -> Client -let Server : () -> Server -let alice : actor {go : shared (Text, Server) -> (); send : shared Text -> ()} -let bob : actor {go : shared (Text, Server) -> (); send : shared Text -> ()} -let charlie : actor {go : shared (Text, Server) -> (); send : shared Text -> ()} -let server : actor {subscribe : shared Client -> async Subscription} --- Interpreting all: -Server() - <= {subscribe = func} -Client() - <= {go = func; send = func} -Client() - <= {go = func; send = func} -Client() - <= {go = func; send = func} --> message go("bob", {subscribe = func}) --> message go("alice", {subscribe = func}) --> message go("charlie", {subscribe = func}) -<- message go("bob", {subscribe = func}) - go("bob", {subscribe = func}) - -> async client.as:9.12-14.6 - ignore(async _) - <= () - <= () -<- message go("alice", {subscribe = func}) - go("alice", {subscribe = func}) - -> async client.as:9.12-14.6 - ignore(async _) - <= () - <= () -<- message go("charlie", {subscribe = func}) - go("charlie", {subscribe = func}) - -> async client.as:9.12-14.6 - ignore(async _) - <= () - <= () -<- async client.as:9.12-14.6 - -> message subscribe({go = func; send = func}) - => await client.as:10.17-10.40 -<- async client.as:9.12-14.6 - -> message subscribe({go = func; send = func}) - => await client.as:10.17-10.40 -<- async client.as:9.12-14.6 - -> message subscribe({go = func; send = func}) - => await client.as:10.17-10.40 -<- message subscribe({go = func; send = func}) - subscribe({go = func; send = func}) - -> async server.as:18.52-29.4 - <= async _ -<- message subscribe({go = func; send = func}) - subscribe({go = func; send = func}) - -> async server.as:18.52-29.4 - <= async _ -<- message subscribe({go = func; send = func}) - subscribe({go = func; send = func}) - -> async server.as:18.52-29.4 - <= async _ -<- async server.as:18.52-29.4 - <= {cancel = func; post = func} -<- async server.as:18.52-29.4 - <= {cancel = func; post = func} -<- async server.as:18.52-29.4 - <= {cancel = func; post = func} -<- await client.as:10.17-10.40({cancel = func; post = func}) - -> message anon-func-24.14("hello from bob") - -> message anon-func-24.14("goodbye from bob") - -> message anon-func-27.16() - <= () -<- await client.as:10.17-10.40({cancel = func; post = func}) - -> message anon-func-24.14("hello from alice") - -> message anon-func-24.14("goodbye from alice") - -> message anon-func-27.16() - <= () -<- await client.as:10.17-10.40({cancel = func; post = func}) - -> message anon-func-24.14("hello from charlie") - -> message anon-func-24.14("goodbye from charlie") - -> message anon-func-27.16() - <= () -<- message anon-func-24.14("hello from bob") - anon-func-24.14("hello from bob") - broadcast(0, "hello from bob") - -> message send("hello from bob") - -> message send("hello from bob") - <= () - <= () -<- message anon-func-24.14("goodbye from bob") - anon-func-24.14("goodbye from bob") - broadcast(0, "goodbye from bob") - -> message send("goodbye from bob") - -> message send("goodbye from bob") - <= () - <= () -<- message anon-func-27.16() - anon-func-27.16() - unsubscribe(0) - print("(unsubscribe ") -(unsubscribe <= () - printInt(0) -0 <= () - print(")\n") -) - <= () - <= () - <= () -<- message anon-func-24.14("hello from alice") - anon-func-24.14("hello from alice") - broadcast(1, "hello from alice") - -> message send("hello from alice") - <= () - <= () -<- message anon-func-24.14("goodbye from alice") - anon-func-24.14("goodbye from alice") - broadcast(1, "goodbye from alice") - -> message send("goodbye from alice") - <= () - <= () -<- message anon-func-27.16() - anon-func-27.16() - unsubscribe(1) - print("(unsubscribe ") -(unsubscribe <= () - printInt(1) -1 <= () - print(")\n") -) - <= () - <= () - <= () -<- message anon-func-24.14("hello from charlie") - anon-func-24.14("hello from charlie") - broadcast(2, "hello from charlie") - <= () - <= () -<- message anon-func-24.14("goodbye from charlie") - anon-func-24.14("goodbye from charlie") - broadcast(2, "goodbye from charlie") - <= () - <= () -<- message anon-func-27.16() - anon-func-27.16() - unsubscribe(2) - print("(unsubscribe ") -(unsubscribe <= () - printInt(2) -2 <= () - print(")\n") -) - <= () - <= () - <= () -<- message send("hello from bob") - send("hello from bob") - print("charlie received hello from bob\n") -charlie received hello from bob - <= () - <= () -<- message send("hello from bob") - send("hello from bob") - print("alice received hello from bob\n") -alice received hello from bob - <= () - <= () -<- message send("goodbye from bob") - send("goodbye from bob") - print("charlie received goodbye from bob\n") -charlie received goodbye from bob - <= () - <= () -<- message send("goodbye from bob") - send("goodbye from bob") - print("alice received goodbye from bob\n") -alice received goodbye from bob - <= () - <= () -<- message send("hello from alice") - send("hello from alice") - print("charlie received hello from alice\n") -charlie received hello from alice - <= () - <= () -<- message send("goodbye from alice") - send("goodbye from alice") - print("charlie received goodbye from alice\n") -charlie received goodbye from alice - <= () - <= () --- Finished all: -let Client : () -> Client = func -let Server : () -> Server = func -let alice : actor {go : shared (Text, Server) -> (); send : shared Text -> ()} = {go = func; send = func} -let bob : actor {go : shared (Text, Server) -> (); send : shared Text -> ()} = {go = func; send = func} -let charlie : actor {go : shared (Text, Server) -> (); send : shared Text -> ()} = {go = func; send = func} -let server : actor {subscribe : shared Client -> async Subscription} = {subscribe = func} - diff --git a/samples/counter.txt b/samples/counter.txt deleted file mode 100644 index e576aa7adc3..00000000000 --- a/samples/counter.txt +++ /dev/null @@ -1,297 +0,0 @@ --- Parsing counter.as: --- Checking all: -type Counter = actor {dec : shared () -> (); read : shared () -> async Int} -let Counter : Int -> Counter -let c : actor {dec : shared () -> (); read : shared () -> async Int} -let show : (Text, Int) -> () -let showAsync : (Text, async Int) -> () -let testDec : () -> () -let testRead : () -> () --- Interpreting all: -Counter(10) - <= {dec = func; read = func} -testDec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - -> message dec() - <= () -testRead() - -> async counter.as:37.11-46.4 - <= async _ -<- message dec() - dec() - show("dec", 10) - <= () - <= () -<- message dec() - dec() - show("dec", 9) - <= () - <= () -<- message dec() - dec() - show("dec", 8) - <= () - <= () -<- message dec() - dec() - show("dec", 7) - <= () - <= () -<- message dec() - dec() - show("dec", 6) - <= () - <= () -<- message dec() - dec() - show("dec", 5) - <= () - <= () -<- message dec() - dec() - show("dec", 4) - <= () - <= () -<- message dec() - dec() - show("dec", 3) - <= () - <= () -<- message dec() - dec() - show("dec", 2) - <= () - <= () -<- message dec() - dec() - show("dec", 1) - <= () - <= () -<- async counter.as:37.11-46.4 - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", 0) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -1 -<- await counter.as:42.21-42.28(-1) - show("await", -1) - <= () - showAsync("after", async -1) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -1) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -2 -<- await counter.as:42.21-42.28(-2) - show("await", -2) - <= () - showAsync("after", async -2) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -2) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -3 -<- await counter.as:42.21-42.28(-3) - show("await", -3) - <= () - showAsync("after", async -3) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -3) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -4 -<- await counter.as:42.21-42.28(-4) - show("await", -4) - <= () - showAsync("after", async -4) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -4) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -5 -<- await counter.as:42.21-42.28(-5) - show("await", -5) - <= () - showAsync("after", async -5) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -5) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -6 -<- await counter.as:42.21-42.28(-6) - show("await", -6) - <= () - showAsync("after", async -6) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -6) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -7 -<- await counter.as:42.21-42.28(-7) - show("await", -7) - <= () - showAsync("after", async -7) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -7) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -8 -<- await counter.as:42.21-42.28(-8) - show("await", -8) - <= () - showAsync("after", async -8) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -8) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -9 -<- await counter.as:42.21-42.28(-9) - show("await", -9) - <= () - showAsync("after", async -9) - <= () - -> message dec() - -> message read() - showAsync("before", async _) - <= () - => await counter.as:42.21-42.28 -<- message dec() - dec() - show("dec", -9) - <= () - <= () -<- message read() - read() - -> async counter.as:13.22-13.27 - <= async _ -<- async counter.as:13.22-13.27 - <= -10 -<- await counter.as:42.21-42.28(-10) - show("await", -10) - <= () - showAsync("after", async -10) - <= () - <= () --- Finished all: -let Counter : Int -> Counter = func -let c : actor {dec : shared () -> (); read : shared () -> async Int} = {dec = func; read = func} -let show : (Text, Int) -> () = func -let showAsync : (Text, async Int) -> () = func -let testDec : () -> () = func -let testRead : () -> () = func - diff --git a/samples/hoare.txt b/samples/hoare.txt deleted file mode 100644 index 00aa11e6ec0..00000000000 --- a/samples/hoare.txt +++ /dev/null @@ -1,45 +0,0 @@ --- Parsing hoare.as: --- Checking all: -let a : [var Int] -let partition : ([var Int], Nat, Nat) -> Nat -let quicksort : ([var Int], Nat, Nat) -> () -let swap : ([var Int], Nat, Nat) -> () --- Interpreting all: -quicksort([8, 3, 9, 5, 2], 0, 4) - partition([8, 3, 9, 5, 2], 0, 4) - swap([8, 3, 9, 5, 2], 0, 4) - <= () - swap([2, 3, 9, 5, 8], 2, 4) - <= () - swap([2, 3, 8, 5, 9], 2, 3) - <= () - <= 3 - quicksort([2, 3, 5, 8, 9], 0, 3) - partition([2, 3, 5, 8, 9], 0, 3) - <= 0 - quicksort([2, 3, 5, 8, 9], 0, 0) - <= () - quicksort([2, 3, 5, 8, 9], 1, 3) - partition([2, 3, 5, 8, 9], 1, 3) - <= 1 - quicksort([2, 3, 5, 8, 9], 1, 1) - <= () - quicksort([2, 3, 5, 8, 9], 2, 3) - partition([2, 3, 5, 8, 9], 2, 3) - <= 2 - quicksort([2, 3, 5, 8, 9], 2, 2) - <= () - quicksort([2, 3, 5, 8, 9], 3, 3) - <= () - <= () - <= () - <= () - quicksort([2, 3, 5, 8, 9], 4, 4) - <= () - <= () --- Finished all: -let a : [var Int] = [2, 3, 5, 8, 9] -let partition : ([var Int], Nat, Nat) -> Nat = func -let quicksort : ([var Int], Nat, Nat) -> () = func -let swap : ([var Int], Nat, Nat) -> () = func - diff --git a/samples/quicksort.txt b/samples/quicksort.txt deleted file mode 100644 index 9325ad21b31..00000000000 --- a/samples/quicksort.txt +++ /dev/null @@ -1,105 +0,0 @@ --- Parsing quicksort.as: --- Checking all: -type Array = [var T] -type QS = {quicksort : (Array, Nat, Nat) -> ()} -let QS : ((T, T) -> Int) -> QS -let a : [var Int] -let cmpi : (Int, Int) -> Int -let qs : {quicksort : (Array, Nat, Nat) -> ()} --- Interpreting all: -QS(func) - <= {quicksort = func} -quicksort([8, 3, 9, 5, 2], 0, 4) - partition([8, 3, 9, 5, 2], 0, 4) - trace([8, 3, 9, 5, 2]) - <= () - cmpi(8, 8) - <= 0 - cmpi(2, 8) - <= -6 - swap([8, 3, 9, 5, 2], 0, 4) - <= () - cmpi(2, 8) - <= -6 - cmpi(3, 8) - <= -5 - cmpi(9, 8) - <= 1 - cmpi(8, 8) - <= 0 - swap([2, 3, 9, 5, 8], 2, 4) - <= () - cmpi(8, 8) - <= 0 - cmpi(9, 8) - <= 1 - cmpi(5, 8) - <= -3 - swap([2, 3, 8, 5, 9], 2, 3) - <= () - cmpi(5, 8) - <= -3 - cmpi(8, 8) - <= 0 - cmpi(8, 8) - <= 0 - <= 3 - quicksort([2, 3, 5, 8, 9], 0, 3) - partition([2, 3, 5, 8, 9], 0, 3) - trace([2, 3, 5, 8, 9]) - <= () - cmpi(2, 2) - <= 0 - cmpi(8, 2) - <= 6 - cmpi(5, 2) - <= 3 - cmpi(3, 2) - <= 1 - cmpi(2, 2) - <= 0 - <= 0 - quicksort([2, 3, 5, 8, 9], 0, 0) - <= () - quicksort([2, 3, 5, 8, 9], 1, 3) - partition([2, 3, 5, 8, 9], 1, 3) - trace([2, 3, 5, 8, 9]) - <= () - cmpi(3, 3) - <= 0 - cmpi(8, 3) - <= 5 - cmpi(5, 3) - <= 2 - cmpi(3, 3) - <= 0 - <= 1 - quicksort([2, 3, 5, 8, 9], 1, 1) - <= () - quicksort([2, 3, 5, 8, 9], 2, 3) - partition([2, 3, 5, 8, 9], 2, 3) - trace([2, 3, 5, 8, 9]) - <= () - cmpi(5, 5) - <= 0 - cmpi(8, 5) - <= 3 - cmpi(5, 5) - <= 0 - <= 2 - quicksort([2, 3, 5, 8, 9], 2, 2) - <= () - quicksort([2, 3, 5, 8, 9], 3, 3) - <= () - <= () - <= () - <= () - quicksort([2, 3, 5, 8, 9], 4, 4) - <= () - <= () --- Finished all: -let QS : ((T, T) -> Int) -> QS = func -let a : [var Int] = [2, 3, 5, 8, 9] -let cmpi : (Int, Int) -> Int = func -let qs : {quicksort : (Array, Nat, Nat) -> ()} = {quicksort = func} -