mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-16 10:40:42 +03:00
merge: master with experimental
This commit is contained in:
commit
8941530426
27
.github/workflows/cargo.yml
vendored
27
.github/workflows/cargo.yml
vendored
@ -41,33 +41,6 @@ jobs:
|
||||
- uses: actions-rs/cargo@v1
|
||||
with:
|
||||
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:
|
||||
# name: 💅 Cargo Fmt
|
||||
# continue-on-error: true
|
||||
|
31
Cargo.lock
generated
31
Cargo.lock
generated
@ -387,12 +387,6 @@ dependencies = [
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "exitcode"
|
||||
version = "1.1.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "de853764b47027c2e862a995c34978ffa63c1501f2e15f987ba11bd4f9bba193"
|
||||
|
||||
[[package]]
|
||||
name = "fixed-hash"
|
||||
version = "0.7.0"
|
||||
@ -666,19 +660,6 @@ dependencies = [
|
||||
"kind-tree",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind-cli"
|
||||
version = "0.3.3"
|
||||
dependencies = [
|
||||
"anyhow",
|
||||
"clap 4.0.29",
|
||||
"exitcode",
|
||||
"kind-checker",
|
||||
"kind-driver",
|
||||
"kind-query",
|
||||
"kind-report",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind-derive"
|
||||
version = "0.1.0"
|
||||
@ -817,6 +798,18 @@ dependencies = [
|
||||
"linked-hash-map",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind2"
|
||||
version = "0.3.7"
|
||||
dependencies = [
|
||||
"anyhow",
|
||||
"clap 4.0.29",
|
||||
"kind-checker",
|
||||
"kind-driver",
|
||||
"kind-query",
|
||||
"kind-report",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kindelia_common"
|
||||
version = "0.1.5"
|
||||
|
@ -38,7 +38,7 @@ Main : IO (Result () String) {
|
||||
}
|
||||
```
|
||||
|
||||
Theorems can be proved inductivelly, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
||||
Theorems can be proved inductively, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
||||
|
||||
```javascript
|
||||
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
|
||||
|
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()));
|
||||
*expr = inlinable.body.clone();
|
||||
subst_on_expr(expr, subst);
|
||||
self.inline_expr(expr)
|
||||
} else {
|
||||
for arg in args {
|
||||
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,6 +1,6 @@
|
||||
WARN This function does not cover all the possibilities!
|
||||
|
||||
* Missing case : Bool.true Bool.true Bool.true Bool.true Bool.true Bool.true Bool.true Bool.true _ Bool.true _ Bool.true Bool.false Bool.true Bool.true
|
||||
* Missing case : Bool.true Bool.true Bool.true Bool.true Bool.true Bool.true Bool.true Bool.true _ Bool.true _ Bool.true Bool.false _ _
|
||||
|
||||
/--[suite/issues/coverage/Bool-2.kind2:6:1]
|
||||
|
|
||||
|
@ -1 +1,13 @@
|
||||
Ok!
|
||||
WARN This function does not cover all the possibilities!
|
||||
|
||||
* Missing case :
|
||||
|
||||
/--[suite/issues/coverage/ISSUE-463-3.kind2:13:1]
|
||||
|
|
||||
12 |
|
||||
13 | Complete (m: Assert Bool.true) (e: Empty) : Type
|
||||
| v-------
|
||||
| \Here!
|
||||
14 |
|
||||
|
||||
|
||||
|
@ -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.
|
||||
|
||||
/--[suite/eval/NoMatch.kind2:3:5]
|
||||
/--[suite/run/NoMatch.kind2:3:5]
|
||||
|
|
||||
| /
|
||||
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]
|
||||
#[timeout(15000)]
|
||||
fn test_eval() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./suite/eval"), |path, session| {
|
||||
fn test_run() -> Result<(), Error> {
|
||||
test_kind2(Path::new("./suite/run"), |path, session| {
|
||||
let entrypoints = vec!["Main".to_string()];
|
||||
let check = driver::erase_book(session, path, entrypoints)
|
||||
.map(|file| driver::compile_book_to_hvm(file, false))
|
||||
@ -99,10 +99,34 @@ fn test_eval() -> Result<(), Error> {
|
||||
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]
|
||||
#[timeout(15000)]
|
||||
fn test_eval_issues() -> Result<(), Error> {
|
||||
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 check = driver::erase_book(session, path, entrypoints)
|
||||
.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