mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
tests: Update test results for new Kindex organization
This commit is contained in:
parent
69ea11eaa2
commit
bec7490b0d
@ -1,6 +1,6 @@
|
|||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: U60
|
* Hole: Data.U60
|
||||||
|
|
||||||
|
|
||||||
/--[suite/checker/Inspection.kind2:3:3]
|
/--[suite/checker/Inspection.kind2:3:3]
|
||||||
|
@ -1,13 +1,13 @@
|
|||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: U60
|
* Hole: Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* awoo : Type
|
* awoo : Type
|
||||||
* awoo = U60
|
* awoo = Data.U60
|
||||||
* uuuhuuul : (List awoo)
|
* uuuhuuul : (Data.List awoo)
|
||||||
* uuuhuuul = (List.nil awoo)
|
* uuuhuuul = (Data.List.nil awoo)
|
||||||
* ooooooo : (List U60)
|
* ooooooo : (Data.List Data.U60)
|
||||||
* ooooooo = uuuhuuul
|
* ooooooo = uuuhuuul
|
||||||
|
|
||||||
/--[suite/checker/Subst.kind2:11:5]
|
/--[suite/checker/Subst.kind2:11:5]
|
||||||
|
@ -2,14 +2,14 @@
|
|||||||
|
|
||||||
/--[suite/checker/derive/fail/RepeatedDef.kind2:2:5]
|
/--[suite/checker/derive/fail/RepeatedDef.kind2:2:5]
|
||||||
|
|
|
|
||||||
1 | type Nat {
|
1 | type Data.Nat {
|
||||||
2 | zero
|
2 | zero
|
||||||
| v---
|
| v---
|
||||||
| \The first ocorrence
|
| \The first ocorrence
|
||||||
3 | succ
|
3 | succ
|
||||||
:
|
:
|
||||||
6 | Nat.zero : U60
|
6 | Data.Nat.zero : Data.U60
|
||||||
| v-------
|
| v------------
|
||||||
| \Second occorrence here!
|
| \Second occorrence here!
|
||||||
|
|
||||||
Hint: Rename one of the definitions or remove and look at how names work in Kind at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md
|
Hint: Rename one of the definitions or remove and look at how names work in Kind at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
ERROR Type mismatch
|
ERROR Type mismatch
|
||||||
|
|
||||||
* Got : (Eq _ (U120.new 0 123) (U120.new 0 123))
|
* Got : (Eq _ (Data.U120.new 0 123) (Data.U120.new 0 123))
|
||||||
* Expected : (Eq _ (U120.new 0 123) (U120.new 0 124))
|
* Expected : (Eq _ (Data.U120.new 0 123) (Data.U120.new 0 124))
|
||||||
|
|
||||||
|
|
||||||
/--[suite/checker/derive/fail/WrongU120Eq.kind2:12:9]
|
/--[suite/checker/derive/fail/WrongU120Eq.kind2:12:9]
|
||||||
|
@ -1,14 +1,14 @@
|
|||||||
ERROR Type mismatch
|
ERROR Type mismatch
|
||||||
|
|
||||||
* Got : Type
|
* Got : Type
|
||||||
* Expected : U60
|
* Expected : Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* a : U60
|
* a : Data.U60
|
||||||
|
|
||||||
/--[suite/checker/fail/MismatchTwo.kind2:2:10]
|
/--[suite/checker/fail/MismatchTwo.kind2:2:10]
|
||||||
|
|
|
|
||||||
1 | Main (a: U60): U60
|
1 | Main (a: Data.U60): Data.U60
|
||||||
2 | Main a = Type
|
2 | Main a = Type
|
||||||
| v---
|
| v---
|
||||||
| \Here!
|
| \Here!
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
|
|
||||||
/--[suite/checker/fail/Unbound.kind2:2:7]
|
/--[suite/checker/fail/Unbound.kind2:2:7]
|
||||||
|
|
|
|
||||||
1 | Tew : U60
|
1 | Tew : Data.U60
|
||||||
2 | Tew = owo
|
2 | Tew = owo
|
||||||
| v--
|
| v--
|
||||||
| \Here!
|
| \Here!
|
||||||
|
@ -2,7 +2,7 @@
|
|||||||
|
|
||||||
/--[suite/erasure/fail/ShouldErr.kind2:2:9]
|
/--[suite/erasure/fail/ShouldErr.kind2:2:9]
|
||||||
|
|
|
|
||||||
1 | Kek <a: U60> : U60
|
1 | Kek <a: Data.U60> : Data.U60
|
||||||
2 | Kek a = a
|
2 | Kek a = a
|
||||||
| v
|
| v
|
||||||
| \It's in relevant position!
|
| \It's in relevant position!
|
||||||
|
@ -1,2 +1,2 @@
|
|||||||
(Maybe.some _ 1009)
|
(Data.Maybe.some _ 1009)
|
||||||
|
|
||||||
|
@ -1,2 +1,2 @@
|
|||||||
(Teste (List.nil _))
|
(Teste (Data.List.nil _))
|
||||||
|
|
||||||
|
@ -1,14 +1,14 @@
|
|||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: (Assert (Nat.count_layers n 1))
|
* Hole: (Assert (Data.Nat.count_layers n 1))
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* n : Nat
|
* n : Data.Nat
|
||||||
|
|
||||||
/--[suite/issues/checker/HvmReducesTooMuch.kind2:14:29]
|
/--[suite/issues/checker/HvmReducesTooMuch.kind2:14:34]
|
||||||
|
|
|
|
||||||
13 | Beq_nat_refl (n: Nat) : Assert (Nat.count_layers n 0)
|
13 | Beq_nat_refl (n: Data.Nat) : Assert (Data.Nat.count_layers n 0)
|
||||||
14 | Beq_nat_refl (Nat.succ n) = ?
|
14 | Beq_nat_refl (Data.Nat.succ n) = ?
|
||||||
| v
|
| v
|
||||||
| \Here!
|
| \Here!
|
||||||
|
|
||||||
|
@ -1,15 +1,15 @@
|
|||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: U60
|
* Hole: Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* n : (Pair U60 U60)
|
* n : (Data.Pair Data.U60 Data.U60)
|
||||||
* n.fst : U60
|
* n.fst : Data.U60
|
||||||
* n.snd : U60
|
* n.snd : Data.U60
|
||||||
|
|
||||||
/--[suite/issues/checker/ISSUE-457.kind2:10:16]
|
/--[suite/issues/checker/ISSUE-457.kind2:10:16]
|
||||||
|
|
|
|
||||||
9 | match Pair n {
|
9 | match Data.Pair n {
|
||||||
10 | new => ?
|
10 | new => ?
|
||||||
| v
|
| v
|
||||||
| \Here!
|
| \Here!
|
||||||
@ -18,16 +18,16 @@
|
|||||||
|
|
||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: U60
|
* Hole: Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* n : (Pair U60 U60)
|
* n : (Data.Pair Data.U60 Data.U60)
|
||||||
* n.fst : U60
|
* n.fst : Data.U60
|
||||||
* n.snd : U60
|
* n.snd : Data.U60
|
||||||
|
|
||||||
/--[suite/issues/checker/ISSUE-457.kind2:17:5]
|
/--[suite/issues/checker/ISSUE-457.kind2:17:5]
|
||||||
|
|
|
|
||||||
16 | open Pair n
|
16 | open Data.Pair n
|
||||||
17 | ?
|
17 | ?
|
||||||
| v
|
| v
|
||||||
| \Here!
|
| \Here!
|
||||||
@ -36,16 +36,16 @@
|
|||||||
|
|
||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: U60
|
* Hole: Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* n : (Pair U60 U60)
|
* n : (Data.Pair Data.U60 Data.U60)
|
||||||
* fst : U60
|
* fst : Data.U60
|
||||||
* snd : U60
|
* snd : Data.U60
|
||||||
|
|
||||||
/--[suite/issues/checker/ISSUE-457.kind2:22:5]
|
/--[suite/issues/checker/ISSUE-457.kind2:22:5]
|
||||||
|
|
|
|
||||||
21 | let Pair.new fst snd = n
|
21 | let Data.Pair.new fst snd = n
|
||||||
22 | ?
|
22 | ?
|
||||||
| v
|
| v
|
||||||
| \Here!
|
| \Here!
|
||||||
|
@ -1,13 +1,13 @@
|
|||||||
INFO Inspection
|
INFO Inspection
|
||||||
|
|
||||||
* Hole: U60
|
* Hole: Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* awoo : Type
|
* awoo : Type
|
||||||
* awoo = U60
|
* awoo = Data.U60
|
||||||
* uuuhuuul : (List awoo)
|
* uuuhuuul : (Data.List awoo)
|
||||||
* uuuhuuul = (List.nil awoo)
|
* uuuhuuul = (Data.List.nil awoo)
|
||||||
* ooooooo : (List U60)
|
* ooooooo : (Data.List Data.U60)
|
||||||
* ooooooo = uuuhuuul
|
* ooooooo = uuuhuuul
|
||||||
|
|
||||||
/--[suite/issues/checker/ISSUE-461.kind2:11:5]
|
/--[suite/issues/checker/ISSUE-461.kind2:11:5]
|
||||||
|
@ -3,8 +3,8 @@
|
|||||||
/--[suite/issues/checker/MatchDerivationWithAll.kind2:3:10]
|
/--[suite/issues/checker/MatchDerivationWithAll.kind2:3:10]
|
||||||
|
|
|
|
||||||
2 | type WithCtx (a: Type) {
|
2 | type WithCtx (a: Type) {
|
||||||
3 | new: U60 -> (WithCtx a)
|
3 | new: Data.U60 -> (WithCtx a)
|
||||||
| v-----------------
|
| v----------------------
|
||||||
| \Here!
|
| \Here!
|
||||||
4 | }
|
4 | }
|
||||||
|
|
||||||
@ -18,8 +18,8 @@
|
|||||||
| v------
|
| v------
|
||||||
| \This is the type that should be used instead
|
| \This is the type that should be used instead
|
||||||
:
|
:
|
||||||
3 | new: U60 -> (WithCtx a)
|
3 | new: Data.U60 -> (WithCtx a)
|
||||||
| v-----------------
|
| v----------------------
|
||||||
| \This is not the type that is being declared
|
| \This is not the type that is being declared
|
||||||
4 | }
|
4 | }
|
||||||
|
|
||||||
|
@ -1,17 +1,17 @@
|
|||||||
ERROR Type mismatch
|
ERROR Type mismatch
|
||||||
|
|
||||||
* Got : (Run n)
|
* Got : (Run n)
|
||||||
* Expected : U60
|
* Expected : Data.U60
|
||||||
|
|
||||||
* Context
|
* Context
|
||||||
* t1 : Type
|
* t1 : Type
|
||||||
* n : Nat
|
* n : Data.Nat
|
||||||
* f : (Run n)
|
* f : (Run n)
|
||||||
|
|
||||||
/--[suite/issues/checker/TestWith.kind2:14:22]
|
/--[suite/issues/checker/TestWith.kind2:14:27]
|
||||||
|
|
|
|
||||||
13 | Lero t1 n f =
|
13 | Lero t1 n f =
|
||||||
14 | match Nat n with f {
|
14 | match Data.Nat n with f {
|
||||||
| v
|
| v
|
||||||
| \Here!
|
| \Here!
|
||||||
15 | succ => (+ f 2)
|
15 | succ => (+ f 2)
|
||||||
|
@ -5,7 +5,7 @@
|
|||||||
|
|
||||||
/--[suite/issues/checker/U60ToNatDoesNotReduce.kind2:30:17]
|
/--[suite/issues/checker/U60ToNatDoesNotReduce.kind2:30:17]
|
||||||
|
|
|
|
||||||
29 | Test_anon_fun : (Equal (Nat.succ (Nat.succ (Nat.zero))) (U60.to_nat 5))
|
29 | Test_anon_fun : (Equal (Data.Nat.succ (Data.Nat.succ (Data.Nat.zero))) (Data.U60.to_nat 5))
|
||||||
30 | Test_anon_fun = ?
|
30 | Test_anon_fun = ?
|
||||||
| v
|
| v
|
||||||
| \Here!
|
| \Here!
|
||||||
|
@ -1,13 +1,13 @@
|
|||||||
WARN This function does not cover all the possibilities!
|
WARN This function does not cover all the possibilities!
|
||||||
|
|
||||||
* Missing case : (String.cons _ _)
|
* Missing case : (Data.String.cons _ _)
|
||||||
|
|
||||||
/--[suite/issues/coverage/ISSUE-463.kind2:8:1]
|
/--[suite/issues/coverage/ISSUE-463.kind2:8:1]
|
||||||
|
|
|
|
||||||
7 |
|
7 |
|
||||||
8 | Bits.from_hex (x: String) : U60
|
8 | Bits.from_hex (x: Data.String) : Data.U60
|
||||||
| v------------
|
| v------------
|
||||||
| \Here!
|
| \Here!
|
||||||
9 | Bits.from_hex (String.cons '0' xs) = 2
|
9 | Bits.from_hex (Data.String.cons '0' xs) = 2
|
||||||
|
|
||||||
|
|
||||||
|
@ -1,13 +1,13 @@
|
|||||||
WARN This function does not cover all the possibilities!
|
WARN This function does not cover all the possibilities!
|
||||||
|
|
||||||
* Missing case : Bool.false Bool.true
|
* Missing case : Data.Bool.false Data.Bool.true
|
||||||
|
|
||||||
/--[suite/issues/coverage/IncompleteBool.kind2:6:1]
|
/--[suite/issues/coverage/IncompleteBool.kind2:6:1]
|
||||||
|
|
|
|
||||||
5 |
|
5 |
|
||||||
6 | Or (b: Bool) (bo: Bool) : Bool
|
6 | Or (b: Data.Bool) (bo: Data.Bool) : Data.Bool
|
||||||
| v-
|
| v-
|
||||||
| \Here!
|
| \Here!
|
||||||
7 | Or Bool.true _ = Bool.true
|
7 | Or Data.Bool.true _ = Data.Bool.true
|
||||||
|
|
||||||
|
|
||||||
|
@ -1,3 +1,3 @@
|
|||||||
|
ctr {Ata}
|
||||||
ctr {Kek}
|
ctr {Kek}
|
||||||
ctr {Bee}
|
ctr {Bee}
|
||||||
ctr {Ata}
|
|
||||||
|
@ -1,17 +1,17 @@
|
|||||||
ctr {String.nil}
|
ctr {USaeFJLF9ugE head tail}
|
||||||
ctr {Pair.new fst snd}
|
ctr {elNhOG2o_j4N fst snd}
|
||||||
ctr {String.cons head tail}
|
ctr {QfIbR9TgcoZc}
|
||||||
|
|
||||||
fun (Test n) {
|
fun (Test n) {
|
||||||
(Test ~) = (!@x1 (!@x1.0 (Pair.match x1.0 @x2 (!@x2.0 @~ (String.match x2.0 #1 @~ @~ #2) x2)) x1) {Pair.new {String.cons #84 {String.cons #101 {String.cons #115 {String.cons #116 {String.cons #101 {String.nil}}}}}} #0})
|
(Test ~) = (!@x1 (!@x1.0 (T0Fu9pW_avGi x1.0 @x2 (!@x2.0 @~ (xNjG8UGUAGaO x2.0 #1 @~ @~ #2) x2)) x1) {elNhOG2o_j4N {USaeFJLF9ugE #84 {USaeFJLF9ugE #101 {USaeFJLF9ugE #115 {USaeFJLF9ugE #116 {USaeFJLF9ugE #101 {QfIbR9TgcoZc}}}}}} #0})
|
||||||
}
|
}
|
||||||
|
|
||||||
fun (Pair.match scrutinee new_) {
|
fun (T0Fu9pW_avGi scrutinee new_) {
|
||||||
(Pair.match {Pair.new x0 x1} x2) = (!@x2.0 (!@x1.0 (!@x0.0 (!(!x2.0 x0.0) x1.0) x0) x1) x2)
|
(T0Fu9pW_avGi {elNhOG2o_j4N x0 x1} x2) = (!@x2.0 (!@x1.0 (!@x0.0 (!(!x2.0 x0.0) x1.0) x0) x1) x2)
|
||||||
}
|
}
|
||||||
|
|
||||||
fun (String.match scrutinee nil_ cons_) {
|
fun (xNjG8UGUAGaO scrutinee nil_ cons_) {
|
||||||
(String.match {String.nil} x0 ~) = (!@x0.0 x0.0 x0)
|
(xNjG8UGUAGaO {QfIbR9TgcoZc} x0 ~) = (!@x0.0 x0.0 x0)
|
||||||
(String.match {String.cons x0 x1} ~ x3) = (!@x3.0 (!@x1.0 (!@x0.0 (!(!x3.0 x0.0) x1.0) x0) x1) x3)
|
(xNjG8UGUAGaO {USaeFJLF9ugE x0 x1} ~ x3) = (!@x3.0 (!@x1.0 (!@x0.0 (!(!x3.0 x0.0) x1.0) x0) x1) x3)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -1,10 +1,10 @@
|
|||||||
ctr {List.cons h t}
|
ctr {zsfQr6_MzW7G h t}
|
||||||
|
|
||||||
fun (U120.new hi lo) {
|
fun (9rVKCpdXApqm hi lo) {
|
||||||
(U120.new x0 x1) = (!@x1.0 (!@x0.0 (| (<< x0.0 #60) x1.0) x0) x1)
|
(9rVKCpdXApqm x0 x1) = (!@x1.0 (!@x0.0 (| (<< x0.0 #60) x1.0) x0) x1)
|
||||||
}
|
}
|
||||||
|
|
||||||
fun (TestFunc xs) {
|
fun (TestFunc xs) {
|
||||||
(TestFunc {List.cons ~ x1}) = (!@x1.0 (!@x2 dup c.0 x2.0 = x2; dup x2.1 x2.2 = c.0; (!@x3 (!@x3.0 (!@~ {List.cons {U120.add x2.0 x3.0} x1.0} #4) x3) {U120.add x2.1 x2.2}) #2) x1)
|
(TestFunc {zsfQr6_MzW7G ~ x1}) = (!@x1.0 (!@x2 dup c.0 x2.0 = x2; dup x2.1 x2.2 = c.0; (!@x3 (!@x3.0 (!@~ {zsfQr6_MzW7G {w4Xd4rma6YBa x2.0 x3.0} x1.0} #4) x3) {w4Xd4rma6YBa x2.1 x2.2}) #2) x1)
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -3,8 +3,8 @@
|
|||||||
/--[suite/kdl/NonInlineState.kind2:7:1]
|
/--[suite/kdl/NonInlineState.kind2:7:1]
|
||||||
|
|
|
|
||||||
6 |
|
6 |
|
||||||
7 | MyFn.state : U60
|
7 | MyFn.state : Data.U60
|
||||||
| v---------------
|
| v--------------------
|
||||||
| \Here!
|
| \Here!
|
||||||
|
|
||||||
|
|
||||||
|
@ -1 +1 @@
|
|||||||
(Maybe.some 1009)
|
(Data.Maybe.some 1009)
|
Loading…
Reference in New Issue
Block a user