diff --git a/crates/kind-tests/suite/checker/Inspection.golden b/crates/kind-tests/suite/checker/Inspection.golden index f2a0352f..322e2e00 100644 --- a/crates/kind-tests/suite/checker/Inspection.golden +++ b/crates/kind-tests/suite/checker/Inspection.golden @@ -1,6 +1,6 @@ INFO Inspection - * Hole: U60 + * Hole: Data.U60 /--[suite/checker/Inspection.kind2:3:3] diff --git a/crates/kind-tests/suite/checker/Subst.golden b/crates/kind-tests/suite/checker/Subst.golden index 81c0fed6..9f7bb471 100644 --- a/crates/kind-tests/suite/checker/Subst.golden +++ b/crates/kind-tests/suite/checker/Subst.golden @@ -1,13 +1,13 @@ INFO Inspection - * Hole: U60 + * Hole: Data.U60 * Context * awoo : Type - * awoo = U60 - * uuuhuuul : (List awoo) - * uuuhuuul = (List.nil awoo) - * ooooooo : (List U60) + * awoo = Data.U60 + * uuuhuuul : (Data.List awoo) + * uuuhuuul = (Data.List.nil awoo) + * ooooooo : (Data.List Data.U60) * ooooooo = uuuhuuul /--[suite/checker/Subst.kind2:11:5] diff --git a/crates/kind-tests/suite/checker/derive/fail/RepeatedDef.golden b/crates/kind-tests/suite/checker/derive/fail/RepeatedDef.golden index 69a19e9a..5c3139fb 100644 --- a/crates/kind-tests/suite/checker/derive/fail/RepeatedDef.golden +++ b/crates/kind-tests/suite/checker/derive/fail/RepeatedDef.golden @@ -2,14 +2,14 @@ /--[suite/checker/derive/fail/RepeatedDef.kind2:2:5] | - 1 | type Nat { + 1 | type Data.Nat { 2 | zero | v--- | \The first ocorrence 3 | succ : - 6 | Nat.zero : U60 - | v------- + 6 | Data.Nat.zero : Data.U60 + | v------------ | \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 diff --git a/crates/kind-tests/suite/checker/derive/fail/WrongU120Eq.golden b/crates/kind-tests/suite/checker/derive/fail/WrongU120Eq.golden index b1877534..cca1babe 100644 --- a/crates/kind-tests/suite/checker/derive/fail/WrongU120Eq.golden +++ b/crates/kind-tests/suite/checker/derive/fail/WrongU120Eq.golden @@ -1,7 +1,7 @@ ERROR Type mismatch - * Got : (Eq _ (U120.new 0 123) (U120.new 0 123)) - * Expected : (Eq _ (U120.new 0 123) (U120.new 0 124)) + * Got : (Eq _ (Data.U120.new 0 123) (Data.U120.new 0 123)) + * Expected : (Eq _ (Data.U120.new 0 123) (Data.U120.new 0 124)) /--[suite/checker/derive/fail/WrongU120Eq.kind2:12:9] diff --git a/crates/kind-tests/suite/checker/fail/MismatchTwo.golden b/crates/kind-tests/suite/checker/fail/MismatchTwo.golden index 680d9a98..2fd30701 100644 --- a/crates/kind-tests/suite/checker/fail/MismatchTwo.golden +++ b/crates/kind-tests/suite/checker/fail/MismatchTwo.golden @@ -1,14 +1,14 @@ ERROR Type mismatch * Got : Type - * Expected : U60 + * Expected : Data.U60 * Context - * a : U60 + * a : Data.U60 /--[suite/checker/fail/MismatchTwo.kind2:2:10] | - 1 | Main (a: U60): U60 + 1 | Main (a: Data.U60): Data.U60 2 | Main a = Type | v--- | \Here! diff --git a/crates/kind-tests/suite/checker/fail/Unbound.golden b/crates/kind-tests/suite/checker/fail/Unbound.golden index a8169aa4..52b1585f 100644 --- a/crates/kind-tests/suite/checker/fail/Unbound.golden +++ b/crates/kind-tests/suite/checker/fail/Unbound.golden @@ -2,7 +2,7 @@ /--[suite/checker/fail/Unbound.kind2:2:7] | - 1 | Tew : U60 + 1 | Tew : Data.U60 2 | Tew = owo | v-- | \Here! diff --git a/crates/kind-tests/suite/erasure/fail/ShouldErr.golden b/crates/kind-tests/suite/erasure/fail/ShouldErr.golden index 13f76cad..fb739858 100644 --- a/crates/kind-tests/suite/erasure/fail/ShouldErr.golden +++ b/crates/kind-tests/suite/erasure/fail/ShouldErr.golden @@ -2,7 +2,7 @@ /--[suite/erasure/fail/ShouldErr.kind2:2:9] | - 1 | Kek : U60 + 1 | Kek : Data.U60 2 | Kek a = a | v | \It's in relevant position! diff --git a/crates/kind-tests/suite/eval/DoNotation.golden b/crates/kind-tests/suite/eval/DoNotation.golden index 71df2d14..e8c13992 100644 --- a/crates/kind-tests/suite/eval/DoNotation.golden +++ b/crates/kind-tests/suite/eval/DoNotation.golden @@ -1,2 +1,2 @@ -(Maybe.some _ 1009) +(Data.Maybe.some _ 1009) diff --git a/crates/kind-tests/suite/eval/User.golden b/crates/kind-tests/suite/eval/User.golden index 3454a946..5f94e2e1 100644 --- a/crates/kind-tests/suite/eval/User.golden +++ b/crates/kind-tests/suite/eval/User.golden @@ -1,2 +1,2 @@ -(Teste (List.nil _)) +(Teste (Data.List.nil _)) diff --git a/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden b/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden index 0ba2c139..c5389554 100644 --- a/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden +++ b/crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden @@ -1,15 +1,15 @@ INFO Inspection - * Hole: (Assert (Nat.count_layers n 1)) + * Hole: (Assert (Data.Nat.count_layers n 1)) * 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) - 14 | Beq_nat_refl (Nat.succ n) = ? - | v - | \Here! + 13 | Beq_nat_refl (n: Data.Nat) : Assert (Data.Nat.count_layers n 0) + 14 | Beq_nat_refl (Data.Nat.succ n) = ? + | v + | \Here! diff --git a/crates/kind-tests/suite/issues/checker/ISSUE-457.golden b/crates/kind-tests/suite/issues/checker/ISSUE-457.golden index 1828cf50..491a7eba 100644 --- a/crates/kind-tests/suite/issues/checker/ISSUE-457.golden +++ b/crates/kind-tests/suite/issues/checker/ISSUE-457.golden @@ -1,15 +1,15 @@ INFO Inspection - * Hole: U60 + * Hole: Data.U60 * Context - * n : (Pair U60 U60) - * n.fst : U60 - * n.snd : U60 + * n : (Data.Pair Data.U60 Data.U60) + * n.fst : Data.U60 + * n.snd : Data.U60 /--[suite/issues/checker/ISSUE-457.kind2:10:16] | - 9 | match Pair n { + 9 | match Data.Pair n { 10 | new => ? | v | \Here! @@ -18,16 +18,16 @@ INFO Inspection - * Hole: U60 + * Hole: Data.U60 * Context - * n : (Pair U60 U60) - * n.fst : U60 - * n.snd : U60 + * n : (Data.Pair Data.U60 Data.U60) + * n.fst : Data.U60 + * n.snd : Data.U60 /--[suite/issues/checker/ISSUE-457.kind2:17:5] | - 16 | open Pair n + 16 | open Data.Pair n 17 | ? | v | \Here! @@ -36,16 +36,16 @@ INFO Inspection - * Hole: U60 + * Hole: Data.U60 * Context - * n : (Pair U60 U60) - * fst : U60 - * snd : U60 + * n : (Data.Pair Data.U60 Data.U60) + * fst : Data.U60 + * snd : Data.U60 /--[suite/issues/checker/ISSUE-457.kind2:22:5] | - 21 | let Pair.new fst snd = n + 21 | let Data.Pair.new fst snd = n 22 | ? | v | \Here! diff --git a/crates/kind-tests/suite/issues/checker/ISSUE-461.golden b/crates/kind-tests/suite/issues/checker/ISSUE-461.golden index 2dd4698b..18a3aca2 100644 --- a/crates/kind-tests/suite/issues/checker/ISSUE-461.golden +++ b/crates/kind-tests/suite/issues/checker/ISSUE-461.golden @@ -1,13 +1,13 @@ INFO Inspection - * Hole: U60 + * Hole: Data.U60 * Context * awoo : Type - * awoo = U60 - * uuuhuuul : (List awoo) - * uuuhuuul = (List.nil awoo) - * ooooooo : (List U60) + * awoo = Data.U60 + * uuuhuuul : (Data.List awoo) + * uuuhuuul = (Data.List.nil awoo) + * ooooooo : (Data.List Data.U60) * ooooooo = uuuhuuul /--[suite/issues/checker/ISSUE-461.kind2:11:5] diff --git a/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden b/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden index b225f210..08b4610c 100644 --- a/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden +++ b/crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden @@ -3,8 +3,8 @@ /--[suite/issues/checker/MatchDerivationWithAll.kind2:3:10] | 2 | type WithCtx (a: Type) { - 3 | new: U60 -> (WithCtx a) - | v----------------- + 3 | new: Data.U60 -> (WithCtx a) + | v---------------------- | \Here! 4 | } @@ -18,8 +18,8 @@ | v------ | \This is the type that should be used instead : - 3 | new: U60 -> (WithCtx a) - | v----------------- + 3 | new: Data.U60 -> (WithCtx a) + | v---------------------- | \This is not the type that is being declared 4 | } diff --git a/crates/kind-tests/suite/issues/checker/TestWith.golden b/crates/kind-tests/suite/issues/checker/TestWith.golden index 98559664..5ba62cbb 100644 --- a/crates/kind-tests/suite/issues/checker/TestWith.golden +++ b/crates/kind-tests/suite/issues/checker/TestWith.golden @@ -1,19 +1,19 @@ ERROR Type mismatch * Got : (Run n) - * Expected : U60 + * Expected : Data.U60 * Context * t1 : Type - * n : Nat + * n : Data.Nat * f : (Run n) - /--[suite/issues/checker/TestWith.kind2:14:22] + /--[suite/issues/checker/TestWith.kind2:14:27] | 13 | Lero t1 n f = - 14 | match Nat n with f { - | v - | \Here! + 14 | match Data.Nat n with f { + | v + | \Here! 15 | succ => (+ f 2) diff --git a/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden b/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden index 454bec01..16b80d11 100644 --- a/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden +++ b/crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden @@ -5,7 +5,7 @@ /--[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 = ? | v | \Here! diff --git a/crates/kind-tests/suite/issues/coverage/ISSUE-463.golden b/crates/kind-tests/suite/issues/coverage/ISSUE-463.golden index 908b104a..fd974644 100644 --- a/crates/kind-tests/suite/issues/coverage/ISSUE-463.golden +++ b/crates/kind-tests/suite/issues/coverage/ISSUE-463.golden @@ -1,13 +1,13 @@ 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] | 7 | - 8 | Bits.from_hex (x: String) : U60 + 8 | Bits.from_hex (x: Data.String) : Data.U60 | v------------ | \Here! - 9 | Bits.from_hex (String.cons '0' xs) = 2 + 9 | Bits.from_hex (Data.String.cons '0' xs) = 2 diff --git a/crates/kind-tests/suite/issues/coverage/IncompleteBool.golden b/crates/kind-tests/suite/issues/coverage/IncompleteBool.golden index 598c0885..6133400e 100644 --- a/crates/kind-tests/suite/issues/coverage/IncompleteBool.golden +++ b/crates/kind-tests/suite/issues/coverage/IncompleteBool.golden @@ -1,13 +1,13 @@ 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] | 5 | - 6 | Or (b: Bool) (bo: Bool) : Bool + 6 | Or (b: Data.Bool) (bo: Data.Bool) : Data.Bool | v- | \Here! - 7 | Or Bool.true _ = Bool.true + 7 | Or Data.Bool.true _ = Data.Bool.true diff --git a/crates/kind-tests/suite/kdl/Constructor.golden b/crates/kind-tests/suite/kdl/Constructor.golden index b158b785..ba0d812e 100644 --- a/crates/kind-tests/suite/kdl/Constructor.golden +++ b/crates/kind-tests/suite/kdl/Constructor.golden @@ -1,3 +1,3 @@ +ctr {Ata} ctr {Kek} ctr {Bee} -ctr {Ata} diff --git a/crates/kind-tests/suite/kdl/ISSUE-491-2.golden b/crates/kind-tests/suite/kdl/ISSUE-491-2.golden index 3feed11d..fb62f53f 100644 --- a/crates/kind-tests/suite/kdl/ISSUE-491-2.golden +++ b/crates/kind-tests/suite/kdl/ISSUE-491-2.golden @@ -1,17 +1,17 @@ -ctr {String.nil} -ctr {Pair.new fst snd} -ctr {String.cons head tail} +ctr {USaeFJLF9ugE head tail} +ctr {elNhOG2o_j4N fst snd} +ctr {QfIbR9TgcoZc} 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_) { - (Pair.match {Pair.new x0 x1} x2) = (!@x2.0 (!@x1.0 (!@x0.0 (!(!x2.0 x0.0) x1.0) x0) x1) x2) +fun (T0Fu9pW_avGi scrutinee new_) { + (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_) { - (String.match {String.nil} 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) +fun (xNjG8UGUAGaO scrutinee nil_ cons_) { + (xNjG8UGUAGaO {QfIbR9TgcoZc} x0 ~) = (!@x0.0 x0.0 x0) + (xNjG8UGUAGaO {USaeFJLF9ugE x0 x1} ~ x3) = (!@x3.0 (!@x1.0 (!@x0.0 (!(!x3.0 x0.0) x1.0) x0) x1) x3) } diff --git a/crates/kind-tests/suite/kdl/LinearizeVars.golden b/crates/kind-tests/suite/kdl/LinearizeVars.golden index 637a6994..ef7cda43 100644 --- a/crates/kind-tests/suite/kdl/LinearizeVars.golden +++ b/crates/kind-tests/suite/kdl/LinearizeVars.golden @@ -1,10 +1,10 @@ -ctr {List.cons h t} +ctr {zsfQr6_MzW7G h t} -fun (U120.new hi lo) { - (U120.new x0 x1) = (!@x1.0 (!@x0.0 (| (<< x0.0 #60) x1.0) x0) x1) +fun (9rVKCpdXApqm hi lo) { + (9rVKCpdXApqm x0 x1) = (!@x1.0 (!@x0.0 (| (<< x0.0 #60) x1.0) x0) x1) } 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) } diff --git a/crates/kind-tests/suite/kdl/NonInlineState.golden b/crates/kind-tests/suite/kdl/NonInlineState.golden index 9a62a26c..f7477589 100644 --- a/crates/kind-tests/suite/kdl/NonInlineState.golden +++ b/crates/kind-tests/suite/kdl/NonInlineState.golden @@ -3,8 +3,8 @@ /--[suite/kdl/NonInlineState.kind2:7:1] | 6 | - 7 | MyFn.state : U60 - | v--------------- + 7 | MyFn.state : Data.U60 + | v-------------------- | \Here! diff --git a/crates/kind-tests/suite/lib/Maybe/_.kind2 b/crates/kind-tests/suite/lib/Data/Maybe/_.kind2 similarity index 100% rename from crates/kind-tests/suite/lib/Maybe/_.kind2 rename to crates/kind-tests/suite/lib/Data/Maybe/_.kind2 diff --git a/crates/kind-tests/suite/lib/Maybe/bind.kind2 b/crates/kind-tests/suite/lib/Data/Maybe/bind.kind2 similarity index 100% rename from crates/kind-tests/suite/lib/Maybe/bind.kind2 rename to crates/kind-tests/suite/lib/Data/Maybe/bind.kind2 diff --git a/crates/kind-tests/suite/lib/Maybe/pure.kind2 b/crates/kind-tests/suite/lib/Data/Maybe/pure.kind2 similarity index 100% rename from crates/kind-tests/suite/lib/Maybe/pure.kind2 rename to crates/kind-tests/suite/lib/Data/Maybe/pure.kind2 diff --git a/crates/kind-tests/suite/lib/String.kind2 b/crates/kind-tests/suite/lib/Data/String.kind2 similarity index 100% rename from crates/kind-tests/suite/lib/String.kind2 rename to crates/kind-tests/suite/lib/Data/String.kind2 diff --git a/crates/kind-tests/suite/run/DoNotation.golden b/crates/kind-tests/suite/run/DoNotation.golden index 6d072348..8d16c59b 100644 --- a/crates/kind-tests/suite/run/DoNotation.golden +++ b/crates/kind-tests/suite/run/DoNotation.golden @@ -1 +1 @@ -(Maybe.some 1009) \ No newline at end of file +(Data.Maybe.some 1009) \ No newline at end of file