mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-10-26 08:09:22 +03:00
commit
49cb04522f
27
.github/workflows/cargo.yml
vendored
27
.github/workflows/cargo.yml
vendored
@ -41,33 +41,6 @@ jobs:
|
|||||||
- uses: actions-rs/cargo@v1
|
- uses: actions-rs/cargo@v1
|
||||||
with:
|
with:
|
||||||
command: test
|
command: test
|
||||||
|
|
||||||
wikind_test:
|
|
||||||
name: ⚗️ Wikind Test
|
|
||||||
runs-on: ${{ matrix.os }}
|
|
||||||
timeout-minutes: 20
|
|
||||||
strategy:
|
|
||||||
matrix:
|
|
||||||
os: [ubuntu-latest]
|
|
||||||
steps:
|
|
||||||
- uses: actions/checkout@v2
|
|
||||||
- uses: actions-rs/toolchain@v1
|
|
||||||
with:
|
|
||||||
profile: minimal
|
|
||||||
toolchain: nightly
|
|
||||||
override: true
|
|
||||||
|
|
||||||
- uses: Swatinem/rust-cache@v2
|
|
||||||
- uses: actions-rs/cargo@v1
|
|
||||||
with:
|
|
||||||
command: build
|
|
||||||
|
|
||||||
- name: Run wikind
|
|
||||||
run: |
|
|
||||||
chmod +x ./tests/test_wikind.sh
|
|
||||||
./tests/test_wikind.sh
|
|
||||||
shell: bash
|
|
||||||
|
|
||||||
# cargo_fmt:
|
# cargo_fmt:
|
||||||
# name: 💅 Cargo Fmt
|
# name: 💅 Cargo Fmt
|
||||||
# continue-on-error: true
|
# continue-on-error: true
|
||||||
|
File diff suppressed because it is too large
Load Diff
@ -78,6 +78,7 @@ impl InlineState {
|
|||||||
FxHashMap::from_iter(inlinable.names.iter().cloned().zip(args.clone()));
|
FxHashMap::from_iter(inlinable.names.iter().cloned().zip(args.clone()));
|
||||||
*expr = inlinable.body.clone();
|
*expr = inlinable.body.clone();
|
||||||
subst_on_expr(expr, subst);
|
subst_on_expr(expr, subst);
|
||||||
|
self.inline_expr(expr)
|
||||||
} else {
|
} else {
|
||||||
for arg in args {
|
for arg in args {
|
||||||
self.inline_expr(arg);
|
self.inline_expr(arg);
|
||||||
|
@ -1 +1,2 @@
|
|||||||
500
|
500
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
(Maybe.some 1009)
|
(Maybe.some _ 1009)
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
300
|
300
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
3
|
3
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
65
|
65
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
700
|
700
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
2
|
2
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
3
|
3
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
(Teste [])
|
(Teste (List.nil _))
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
3
|
3
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
17
|
17
|
||||||
|
|
||||||
|
@ -1 +1,2 @@
|
|||||||
"ata"
|
'ata'
|
||||||
|
|
||||||
|
3
crates/kind-tests/suite/issues/eval/ISSUE-472.golden
Normal file
3
crates/kind-tests/suite/issues/eval/ISSUE-472.golden
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
'
|
||||||
|
'
|
||||||
|
|
23
crates/kind-tests/suite/issues/eval/ISSUE-472.kind2
Normal file
23
crates/kind-tests/suite/issues/eval/ISSUE-472.kind2
Normal file
@ -0,0 +1,23 @@
|
|||||||
|
Char : Type
|
||||||
|
Char = U60
|
||||||
|
|
||||||
|
#inline
|
||||||
|
String.new_line : (String)
|
||||||
|
String.new_line = (String.pure (Char.newline))
|
||||||
|
|
||||||
|
Main : _
|
||||||
|
Main = String.new_line
|
||||||
|
|
||||||
|
#inline
|
||||||
|
Char.newline : (Char)
|
||||||
|
Char.newline = 10
|
||||||
|
|
||||||
|
#derive[match]
|
||||||
|
type String {
|
||||||
|
nil
|
||||||
|
cons (head: (Char)) (tail: (String))
|
||||||
|
}
|
||||||
|
|
||||||
|
#inline
|
||||||
|
String.pure (x: (Char)) : (String)
|
||||||
|
String.pure x = (String.cons x (String.nil))
|
1
crates/kind-tests/suite/issues/run/CallStr.golden
Normal file
1
crates/kind-tests/suite/issues/run/CallStr.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
"ata"
|
3
crates/kind-tests/suite/issues/run/CallStr.kind2
Normal file
3
crates/kind-tests/suite/issues/run/CallStr.kind2
Normal file
@ -0,0 +1,3 @@
|
|||||||
|
Main : U60 {
|
||||||
|
"ata"
|
||||||
|
}
|
2
crates/kind-tests/suite/issues/run/ISSUE-472.golden
Normal file
2
crates/kind-tests/suite/issues/run/ISSUE-472.golden
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
"
|
||||||
|
"
|
23
crates/kind-tests/suite/issues/run/ISSUE-472.kind2
Normal file
23
crates/kind-tests/suite/issues/run/ISSUE-472.kind2
Normal file
@ -0,0 +1,23 @@
|
|||||||
|
Char : Type
|
||||||
|
Char = U60
|
||||||
|
|
||||||
|
#inline
|
||||||
|
String.new_line : (String)
|
||||||
|
String.new_line = (String.pure (Char.newline))
|
||||||
|
|
||||||
|
Main : _
|
||||||
|
Main = String.new_line
|
||||||
|
|
||||||
|
#inline
|
||||||
|
Char.newline : (Char)
|
||||||
|
Char.newline = 10
|
||||||
|
|
||||||
|
#derive[match]
|
||||||
|
type String {
|
||||||
|
nil
|
||||||
|
cons (head: (Char)) (tail: (String))
|
||||||
|
}
|
||||||
|
|
||||||
|
#inline
|
||||||
|
String.pure (x: (Char)) : (String)
|
||||||
|
String.pure x = (String.cons x (String.nil))
|
1
crates/kind-tests/suite/run/AllFieldsDestruct.golden
Normal file
1
crates/kind-tests/suite/run/AllFieldsDestruct.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
500
|
10
crates/kind-tests/suite/run/AllFieldsDestruct.kind2
Normal file
10
crates/kind-tests/suite/run/AllFieldsDestruct.kind2
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
#derive[match]
|
||||||
|
record Pudim {
|
||||||
|
owo : U60
|
||||||
|
uwu : U60
|
||||||
|
}
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main =
|
||||||
|
let Pudim.new owo uwu .. = Pudim.new (uwu = 300) (owo = 200)
|
||||||
|
(+ owo uwu)
|
1
crates/kind-tests/suite/run/DoNotation.golden
Normal file
1
crates/kind-tests/suite/run/DoNotation.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
(Maybe.some 1009)
|
12
crates/kind-tests/suite/run/DoNotation.kind2
Normal file
12
crates/kind-tests/suite/run/DoNotation.kind2
Normal file
@ -0,0 +1,12 @@
|
|||||||
|
Main : Maybe U60
|
||||||
|
Main =
|
||||||
|
do Maybe {
|
||||||
|
Maybe.some 3
|
||||||
|
Maybe.pure 2
|
||||||
|
ask res = Maybe.pure 2
|
||||||
|
ask res2 = Maybe.pure 3
|
||||||
|
match Maybe t = (Maybe.some 4) {
|
||||||
|
some val => Maybe.pure (+ 1000 (+ val (+ res res2)))
|
||||||
|
none => Maybe.none
|
||||||
|
}
|
||||||
|
}
|
1
crates/kind-tests/suite/run/Getters.golden
Normal file
1
crates/kind-tests/suite/run/Getters.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
300
|
10
crates/kind-tests/suite/run/Getters.kind2
Normal file
10
crates/kind-tests/suite/run/Getters.kind2
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
#derive[getters]
|
||||||
|
record Pair (a: Type) (b: Type) {
|
||||||
|
fst : a
|
||||||
|
snd : b
|
||||||
|
}
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main =
|
||||||
|
let a = (Pair.new 100 200 :: Pair U60 U60)
|
||||||
|
(+ (Pair.fst.get a) (Pair.snd.get a))
|
1
crates/kind-tests/suite/run/MatchMotive.golden
Normal file
1
crates/kind-tests/suite/run/MatchMotive.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
3
|
19
crates/kind-tests/suite/run/MatchMotive.kind2
Normal file
19
crates/kind-tests/suite/run/MatchMotive.kind2
Normal file
@ -0,0 +1,19 @@
|
|||||||
|
#derive[match]
|
||||||
|
type Maybe (a: Type) {
|
||||||
|
some (val: a)
|
||||||
|
none
|
||||||
|
}
|
||||||
|
|
||||||
|
Str : Type
|
||||||
|
Str.nil : Str
|
||||||
|
|
||||||
|
MotiveGen (n: Maybe U60) : Type
|
||||||
|
MotiveGen (Maybe.some _) = U60
|
||||||
|
MotiveGen Maybe.none = Str
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main =
|
||||||
|
match Maybe t = Maybe.some 3 {
|
||||||
|
some => t.val
|
||||||
|
none => Str.nil
|
||||||
|
} : (x => MotiveGen x)
|
@ -1,6 +1,6 @@
|
|||||||
ERROR Required functions are not implemented for this type.
|
ERROR Required functions are not implemented for this type.
|
||||||
|
|
||||||
/--[suite/eval/NoMatch.kind2:3:5]
|
/--[suite/run/NoMatch.kind2:3:5]
|
||||||
|
|
|
|
||||||
| /
|
| /
|
||||||
3 | | match NoMatch t = NoMatch.pudding {
|
3 | | match NoMatch t = NoMatch.pudding {
|
1
crates/kind-tests/suite/run/PatChar.golden
Normal file
1
crates/kind-tests/suite/run/PatChar.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
65
|
6
crates/kind-tests/suite/run/PatChar.kind2
Normal file
6
crates/kind-tests/suite/run/PatChar.kind2
Normal file
@ -0,0 +1,6 @@
|
|||||||
|
Lol (n: U60) : U60
|
||||||
|
Lol 'A' = 'A'
|
||||||
|
Lol _ = 0
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main = (Lol 'A')
|
1
crates/kind-tests/suite/run/Setters.golden
Normal file
1
crates/kind-tests/suite/run/Setters.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
700
|
12
crates/kind-tests/suite/run/Setters.kind2
Normal file
12
crates/kind-tests/suite/run/Setters.kind2
Normal file
@ -0,0 +1,12 @@
|
|||||||
|
#derive[getters, setters]
|
||||||
|
record Pair (a: Type) (b: Type) {
|
||||||
|
fst : a
|
||||||
|
snd : b
|
||||||
|
}
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main =
|
||||||
|
let a = (Pair.new 100 200 :: Pair U60 U60)
|
||||||
|
let b = Pair.fst.set a 500
|
||||||
|
let c = Pair.snd.set a (+ (Pair.fst.get b) (Pair.snd.get b))
|
||||||
|
Pair.snd.get c
|
1
crates/kind-tests/suite/run/SimpleOpen.golden
Normal file
1
crates/kind-tests/suite/run/SimpleOpen.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
2
|
16
crates/kind-tests/suite/run/SimpleOpen.kind2
Normal file
16
crates/kind-tests/suite/run/SimpleOpen.kind2
Normal file
@ -0,0 +1,16 @@
|
|||||||
|
#derive[match]
|
||||||
|
record Pudim {
|
||||||
|
owo : U60
|
||||||
|
uwu : U60
|
||||||
|
}
|
||||||
|
|
||||||
|
#keep
|
||||||
|
Ok (n: Pudim) : U60
|
||||||
|
Ok n =
|
||||||
|
open Pudim n
|
||||||
|
(+ n.owo n.uwu)
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main =
|
||||||
|
let Pudim.new owo .. = Pudim.new (uwu = 300) (owo = 200)
|
||||||
|
2
|
1
crates/kind-tests/suite/run/TestWith.golden
Normal file
1
crates/kind-tests/suite/run/TestWith.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
3
|
19
crates/kind-tests/suite/run/TestWith.kind2
Normal file
19
crates/kind-tests/suite/run/TestWith.kind2
Normal file
@ -0,0 +1,19 @@
|
|||||||
|
#derive[match]
|
||||||
|
type Nat {
|
||||||
|
succ (pred: Nat)
|
||||||
|
zero
|
||||||
|
}
|
||||||
|
|
||||||
|
Run (n: Nat) : Type
|
||||||
|
Run (Nat.succ n) = U60
|
||||||
|
Run (Nat.zero) = U60
|
||||||
|
|
||||||
|
Lero <t> (n: Nat) (f: Run n) : U60
|
||||||
|
Lero t1 n f =
|
||||||
|
match Nat n with (f : Run n) {
|
||||||
|
succ => (+ f 2)
|
||||||
|
zero => (+ f 1)
|
||||||
|
}
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main = Lero (Nat.succ Nat.zero) 1
|
1
crates/kind-tests/suite/run/User.golden
Normal file
1
crates/kind-tests/suite/run/User.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
(Teste [])
|
12
crates/kind-tests/suite/run/User.kind2
Normal file
12
crates/kind-tests/suite/run/User.kind2
Normal file
@ -0,0 +1,12 @@
|
|||||||
|
|
||||||
|
#kdl_run
|
||||||
|
Main : U60
|
||||||
|
Main = Teste List.nil
|
||||||
|
|
||||||
|
type List (t: Type) {
|
||||||
|
cons (x: t) (xs: List t)
|
||||||
|
nil
|
||||||
|
}
|
||||||
|
|
||||||
|
Teste (n: List U60) : U60
|
||||||
|
Teste (List.cons 2 xs) = 2
|
1
crates/kind-tests/suite/run/VecMatch.golden
Normal file
1
crates/kind-tests/suite/run/VecMatch.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
3
|
20
crates/kind-tests/suite/run/VecMatch.kind2
Normal file
20
crates/kind-tests/suite/run/VecMatch.kind2
Normal file
@ -0,0 +1,20 @@
|
|||||||
|
type Nat {
|
||||||
|
succ (pred : Nat)
|
||||||
|
zero
|
||||||
|
}
|
||||||
|
|
||||||
|
#derive[match]
|
||||||
|
type Vec (t: Type) ~ (n: Nat) {
|
||||||
|
cons <size : Nat> (x : t) (xs : Vec t size) : Vec t (Nat.succ size)
|
||||||
|
nil : Vec t Nat.zero
|
||||||
|
}
|
||||||
|
|
||||||
|
Vec.count <t> <n: Nat> (v: Vec t n) : U60
|
||||||
|
Vec.count vec =
|
||||||
|
match Vec vec {
|
||||||
|
cons xs .. => (+ 1 (Vec.count xs))
|
||||||
|
nil => 0
|
||||||
|
}
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main = Vec.count (Vec.cons 10 (Vec.cons 20 (Vec.cons 30 Vec.nil)))
|
1
crates/kind-tests/suite/run/With.golden
Normal file
1
crates/kind-tests/suite/run/With.golden
Normal file
@ -0,0 +1 @@
|
|||||||
|
17
|
16
crates/kind-tests/suite/run/With.kind2
Normal file
16
crates/kind-tests/suite/run/With.kind2
Normal file
@ -0,0 +1,16 @@
|
|||||||
|
#derive[match]
|
||||||
|
type Maybe (t: Type) {
|
||||||
|
some (val: t)
|
||||||
|
none
|
||||||
|
}
|
||||||
|
|
||||||
|
Main : U60
|
||||||
|
Main =
|
||||||
|
let t = Maybe.some 3
|
||||||
|
let e = 4
|
||||||
|
let f = 10
|
||||||
|
match Maybe t with e f {
|
||||||
|
some val => (+ val (+ e f))
|
||||||
|
none => (* e f)
|
||||||
|
}
|
||||||
|
|
@ -86,8 +86,8 @@ fn test_checker_issues() -> Result<(), Error> {
|
|||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
#[timeout(15000)]
|
#[timeout(15000)]
|
||||||
fn test_eval() -> Result<(), Error> {
|
fn test_run() -> Result<(), Error> {
|
||||||
test_kind2(Path::new("./suite/eval"), |path, session| {
|
test_kind2(Path::new("./suite/run"), |path, session| {
|
||||||
let entrypoints = vec!["Main".to_string()];
|
let entrypoints = vec!["Main".to_string()];
|
||||||
let check = driver::erase_book(session, path, entrypoints)
|
let check = driver::erase_book(session, path, entrypoints)
|
||||||
.map(|file| driver::compile_book_to_hvm(file, false))
|
.map(|file| driver::compile_book_to_hvm(file, false))
|
||||||
@ -99,10 +99,34 @@ fn test_eval() -> Result<(), Error> {
|
|||||||
Ok(())
|
Ok(())
|
||||||
}
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
#[timeout(15000)]
|
||||||
|
fn test_eval() -> Result<(), Error> {
|
||||||
|
test_kind2(Path::new("./suite/eval"), |path, session| {
|
||||||
|
let check = driver::desugar_book(session, path)
|
||||||
|
.map(|file| driver::eval_in_checker(&file));
|
||||||
|
|
||||||
|
check.ok().map(|x| x.0)
|
||||||
|
})?;
|
||||||
|
Ok(())
|
||||||
|
}
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
#[timeout(15000)]
|
#[timeout(15000)]
|
||||||
fn test_eval_issues() -> Result<(), Error> {
|
fn test_eval_issues() -> Result<(), Error> {
|
||||||
test_kind2(Path::new("./suite/issues/eval"), |path, session| {
|
test_kind2(Path::new("./suite/issues/eval"), |path, session| {
|
||||||
|
let check = driver::desugar_book(session, path)
|
||||||
|
.map(|file| driver::eval_in_checker(&file));
|
||||||
|
|
||||||
|
check.ok().map(|x| x.0)
|
||||||
|
})?;
|
||||||
|
Ok(())
|
||||||
|
}
|
||||||
|
|
||||||
|
#[test]
|
||||||
|
#[timeout(15000)]
|
||||||
|
fn test_run_issues() -> Result<(), Error> {
|
||||||
|
test_kind2(Path::new("./suite/issues/run"), |path, session| {
|
||||||
let entrypoints = vec!["Main".to_string()];
|
let entrypoints = vec!["Main".to_string()];
|
||||||
let check = driver::erase_book(session, path, entrypoints)
|
let check = driver::erase_book(session, path, entrypoints)
|
||||||
.map(|file| driver::compile_book_to_hvm(file, false))
|
.map(|file| driver::compile_book_to_hvm(file, false))
|
||||||
|
@ -1,9 +0,0 @@
|
|||||||
set -e
|
|
||||||
|
|
||||||
git clone https://github.com/Kindelia/Wikind.git
|
|
||||||
|
|
||||||
for file in ./Wikind/**/*.kind2; do
|
|
||||||
cargo run --release -- --root=Wikind check $file
|
|
||||||
done
|
|
||||||
|
|
||||||
rm Wikind
|
|
Loading…
Reference in New Issue
Block a user