tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-10-04 15:17:34 +03:00
Code Issues Projects Releases Wiki Activity

Officially restore the syntax for enum types

Browse Source 
The enum types synax was temporary and somehow hidden. For v0.2.0, we
make it visible again. This commits also changes the syntax such that
alternatives must be prefixed with a backtick `, as for enum tags, for
more visual consistency.

This commit also updates the manual sections accordingly.
This commit is contained in:
Yann Hamdaoui 2022-07-28 19:07:48 +02:00
parent 33f2007ec1
commit 05375af534
14 changed files with 112 additions and 188 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
doc/manual/syntax.md
View File

@ -214,8 +214,9 @@ While it's technically possible to just use strings in place of enum tags, using
an enum tag insists on the fact that only a finite number of alternatives can be
used for the corresponding value.
Enum will also be handled more finely by the typechecker, however, as of the
version 0.1 of Nickel, enum types are not yet supported.
Additionally, the typechecker is aware of enums and can for example statically
enforce that only valid tags are passed to a function within a typed block. See
[the manual section on typing](./typing.md) for more details.
## Equality

30
doc/manual/typing.md
View File

@ -193,21 +193,21 @@ The following type constructors are available:
record.map (fun char count => count + 1) occurrences : {_ : Num}
```
<!-- - **Enum**: `<tag1, .., tagn>`: an enumeration comprised of alternatives `tag1`, -->
<!-- .., `tagn`. An enumeration literal is prefixed with a backtick and serialized -->
<!-- as a string. It is useful to encode finite alternatives. The advantage over -->
<!-- strings is that the typechecker handles them more finely: it is able to detect -->
<!-- incomplete matches, for example. -->
<!-- -->
<!-- Example: -->
<!-- ```nickel -->
<!-- let protocol : <http, ftp, sftp> = `http in -->
<!-- (switch { -->
<!-- `http => 1, -->
<!-- `ftp => 2, -->
<!-- `sftp => 3 -->
<!-- } protocol) : Num -->
<!-- ``` -->
- **Enum**: ``[| `tag1, .., `tagn |]``: an enumeration comprised of alternatives
`tag1`, .., `tagn`. An enumeration literal is prefixed with a backtick and
serialized as a string. It is useful to encode finite alternatives. The
advantage over strings is that the typechecker handles them more finely: it is
able to detect incomplete matches, for example.
Example:
```nickel
let protocol : [| `http, `ftp, `sftp |] = `http in
(switch {
`http => 1,
`ftp => 2,
`sftp => 3
} protocol) : Num
```
- **Arrow (function)**: `S -> T`. A function taking arguments of type `S` and returning a value of
type `T`. For multi-parameters functions, just iterate the arrow constructor.

2
examples/record-contract/record-contract.ncl
View File

@ -22,7 +22,7 @@ let Container = {
} in
let KubernetesConfig = {
kind | [| ReplicationController, ReplicaSet, Pod |]
kind | [| `ReplicationController, `ReplicaSet, `Pod |]
| doc "The kind of the element being configured."
| default = `Pod,

81
src/grammar.lalrpop
View File

@ -316,7 +316,7 @@ Atom: UniTerm = {
AsUniTerm<StrChunks>,
Ident => UniTerm::from(UniTermNode::Var(<>)),
UniRecord => UniTerm::from(UniTermNode::Record(<>)),
"`" <EnumTag> => UniTerm::from(Term::Enum(<>)),
<EnumTag> => UniTerm::from(Term::Enum(<>)),
"[" <terms: (<Term> ",")*> <last: Term?> "]" => {
let terms : Vec<RichTerm> = terms.into_iter()
.chain(last.into_iter()).collect();
@ -384,47 +384,50 @@ Pattern: (Option<Ident>,Destruct) = {
Destruct: Destruct = {
<start: @L> "{" <mut matches: (<Match> ",")*> <last:LastMatch?> "}" <end: @R> => {
let (open, rest) = match last {
Some(LastMatch::Match(m)) => {
matches.push(*m);
(false,None)
},
Some(LastMatch::Ellipsis(rest)) => (true, rest),
_ => (false, None),
};
let span = mk_span(src_id, start, end);
Destruct::Record{matches, open, rest, span}
Some(LastMatch::Match(m)) => {
matches.push(*m);
(false,None)
},
Some(LastMatch::Ellipsis(rest)) => (true, rest),
_ => (false, None),
};
let span = mk_span(src_id, start, end);
Destruct::Record{matches, open, rest, span}
},
};
// A binding `ident = <pattern>` inside a destructuring pattern.
Match: Match = {
<left:Ident> <anns: Annot<FixedType>?> <default: DefaultAnnot?> "=" <right: Pattern> => {
let meta = match (default, anns) {
(Some(d), Some(m)) => MetaValue::flatten(d,m),
(Some(m),_) | (_,Some(m)) => m,
_ => MetaValue {
contracts: vec![Contract{
types: Types(AbsType::Dyn().into()),
label: Label{span: left.pos.unwrap(), ..Default::default()},
}],
..Default::default()
},
};
Match::Assign(left, meta, right)
let meta = match (default, anns) {
(Some(d), Some(m)) => MetaValue::flatten(d,m),
(Some(m),_) | (_,Some(m)) => m,
_ => MetaValue {
contracts: vec![Contract{
types: Types(AbsType::Dyn().into()),
label: Label{span: left.pos.unwrap(), ..Default::default()},
}],
..Default::default()
},
};
Match::Assign(left, meta, right)
},
<id:Ident> <anns: Annot<FixedType>?> <default: DefaultAnnot?> => {
let meta = match (default, anns) {
(Some(d), Some(m)) => MetaValue::flatten(d,m),
(Some(m),_) | (_,Some(m)) => m,
_ => MetaValue {
contracts: vec![Contract{
types: Types(AbsType::Dyn().into()),
label: Label{span: id.pos.unwrap(), ..Default::default()},
}],
..Default::default()
},
};
Match::Simple(id, meta)
let meta = match (default, anns) {
(Some(d), Some(m)) => MetaValue::flatten(d,m),
(Some(m),_) | (_,Some(m)) => m,
_ => MetaValue {
contracts: vec![Contract{
types: Types(AbsType::Dyn().into()),
label: Label{span: id.pos.unwrap(), ..Default::default()},
}],
..Default::default()
},
};
Match::Simple(id, meta)
},
};
@ -499,7 +502,9 @@ Interpolation = { "%{", "multstr %{" };
StaticString: String = StringStart <s: ChunkLiteral?> StringEnd => s.unwrap_or_default();
EnumTag: Ident = {
EnumTag: Ident = "`" <EnumTagContent> => <>;
EnumTagContent: Ident = {
<Ident>,
<StaticString> => <>.into(),
// Allow tags of the form `Str, `Bool, etc. This is ad-hoc and should
@ -554,7 +559,7 @@ UOp: UnaryOp = {
};
SwitchCase: SwitchCase = {
"`" <id: EnumTag> "=>" <t: Term> => SwitchCase::Normal(id, t),
"`" <id: EnumTagContent> "=>" <t: Term> => SwitchCase::Normal(id, t),
"_" "=>" <t: Term> => SwitchCase::Default(<>),
}
@ -750,7 +755,7 @@ TypeBuiltin: Types = {
TypeAtom: Types = {
<TypeBuiltin>,
"[|" <rows:(<EnumTag> ",")*> <last: (<EnumTag>)?> <tail: (";" <EnumTag>)?> "|]" => {
"[|" <rows:(<EnumTag> ",")*> <last: (<EnumTag>)?> <tail: (";" <Ident>)?> "|]" => {
let ty = rows.into_iter()
.chain(last.into_iter())
// As we build row types as a linked list via a fold on the original
@ -794,7 +799,7 @@ extern {
"forall" => Token::Normal(NormalToken::Forall),
"in" => Token::Normal(NormalToken::In),
"let" => Token::Normal(NormalToken::Let),
"rec" => Token::Normal(NormalToken::Rec),
"rec" => Token::Normal(NormalToken::Rec),
"switch" => Token::Normal(NormalToken::Switch),
"null" => Token::Normal(NormalToken::Null),

9
src/pretty.rs
View File

@ -772,15 +772,14 @@ where
.braces(),
RowEmpty() => allocator.nil(),
RowExtend(id, ty_opt, tail) => {
let mut builder = allocator.quote_if_needed(&id);
builder = if let Some(ty) = ty_opt {
builder
let builder = if let Some(ty) = ty_opt {
allocator
.quote_if_needed(&id)
.append(allocator.text(":"))
.append(allocator.space())
.append(ty.pretty(allocator))
} else {
builder
allocator.text("`").append(allocator.quote_if_needed(&id))
};
match tail.0 {

8
src/typecheck/error.rs
View File

@ -1,12 +1,8 @@
//! Internal error types for typechecking.
use super::{reporting, State, TypeWrapper};
use crate::{
error::TypecheckError,
identifier::Ident,
label::ty_path,
position::TermPos,
term::RichTerm,
types::{AbsType, Types},
error::TypecheckError, identifier::Ident, label::ty_path, position::TermPos, term::RichTerm,
types::AbsType,
};
/// Error during the unification of two row types.

2
src/typecheck/operation.rs
View File

@ -22,7 +22,7 @@ pub fn get_uop_type(
mk_tyw_arrow!(branches.clone(), branches.clone(), branches),
)
}
// Dyn -> [| Num, Bool, Str, Enum, Fun, Array, Record, Lbl, Other |]
// Dyn -> [| `Num, `Bool, `Str, `Enum, `Fun, `Array, `Record, `Lbl, `Other |]
UnaryOp::Typeof() => (
mk_typewrapper::dynamic(),
mk_tyw_enum!("Num", "Bool", "Str", "Enum", "Fun", "Array", "Record", "Lbl", "Other"),

10
src/types.rs
View File

@ -477,10 +477,10 @@ impl fmt::Display for Types {
AbsType::DynRecord(ty) => write!(f, "{{_: {}}}", ty),
AbsType::RowEmpty() => Ok(()),
AbsType::RowExtend(id, ty_opt, tail) => {
write!(f, "{}", id)?;
if let Some(ty) = ty_opt {
write!(f, ": {}", ty)?;
write!(f, "{}: {}", id, ty)?;
} else {
write!(f, "`{}", id)?;
}
match tail.0 {
@ -553,8 +553,8 @@ mod test {
assert_format_eq("forall r. {x: Bool, y: Bool, z: Bool ; r}");
assert_format_eq("{x: Bool, y: Bool, z: Bool}");
assert_format_eq("[|a, b, c, d|]");
assert_format_eq("forall r. [|tag1, tag2, tag3 ; r|]");
assert_format_eq("[|`a, `b, `c, `d|]");
assert_format_eq("forall r. [|`tag1, `tag2, `tag3 ; r|]");
assert_format_eq("Array Num");
assert_format_eq("Array (Array Num)");

19
stdlib/array.ncl
View File

@ -1,22 +1,5 @@
{
array = {
ComparisonResult
| doc m%"
The result of a comparison. Must be one of the tags:
```
`Less
`Equal
`Greater
```
"%m
= fun label =>
label
|> contract.tag "must be one of `Less, `Equal, or `Greater"
# The enum type syntax [| ... |] is not stable. Do not rely on it in
# your own Nickel programs.
|> contract.apply [| Less, Equal, Greater |],
NonEmpty
| doc m%"
Contract to ensure the given array is not empty.
@ -271,7 +254,7 @@
"%m
= fun f n => %generate% n f,
sort | forall a. (a -> a -> ComparisonResult) -> Array a -> Array a
sort | forall a. (a -> a -> [| `Lesser, `Equal, `Greater |]) -> Array a -> Array a
| doc m%"
Sorts the given arrays based on the provided comparison operator.

88
stdlib/builtin.ncl
View File

@ -1,75 +1,5 @@
{
builtin = {
ValueType
| doc m%"
Possible dynamic type for a value. Must be one of the tags:
```
`Num
`Bool
`Str
`Enum
`Fun
`Array
`Record
`Lbl
`Other
```
"%m
= fun label =>
label
|> contract.tag m%"
must be one of `Num, `Bool, `Str, `Enum, `Fun, `Array`, `Record, `Lbl or `Other
"%m
# The enum type syntax [| ... |] is not stable. Do not rely on it in
# your own Nickel programs.
|> contract.apply [|
Num,
Bool,
Str,
Enum,
Lbl,
Fun,
Array,
Record,
Other
|],
HashAlgorithm
| doc m%"
Supportd hash algorithm. Must be one of the tag:
```
`Md5
`Sha1
`Sha256
`Sha512
```
"%m
= fun label =>
label
|> contract.tag "must be one of `Md5, `Sha1, `Sha256, `Sha512"
# The enum type syntax [| ... |] is not stable. Do not rely on it in
# your own Nickel programs.
|> contract.apply [| Md5, Sha1, Sha256, Sha512 |],
ExportFormat
| doc m%"
Supported import and export format. Must be one of the tag:
```
`Json
`Toml
`Yaml
```
"%m
= fun label =>
label
|> contract.tag "must be one of `Json, `Toml or `Yaml"
# The enum type syntax [| ... |] is not stable. Do not rely on it in
# your own Nickel programs.
|> contract.apply [| Json, Toml, Yaml |],
is_num : Dyn -> Bool
| doc m%"
Checks if the given value is a number.
@ -169,7 +99,17 @@
"%m
= fun x => %typeof% x == `Record,
typeof | Dyn -> ValueType
typeof : Dyn -> [|
`Num,
`Bool,
`Str,
`Enum,
`Lbl,
`Fun,
`Array,
`Record,
`Other
|]
| doc m%"
Results in a value representing the type of the typed value.
@ -215,7 +155,7 @@
"%m
= fun x y => %deep_seq% x y,
hash | HashAlgorithm -> Str -> Str
hash : [| `Md5, `Sha1, `Sha256, `Sha512 |] -> Str -> Str
| doc m%"
Hashes the given string provided the desired hash algorithm.
@ -227,7 +167,7 @@
"%m
= fun type s => %hash% type s,
serialize | ExportFormat -> Dyn -> Str
serialize : [| `Json, `Toml, `Yaml |] -> Dyn -> Str
| doc m%"
Serializes the given value to the desired representation.
@ -242,7 +182,7 @@
"%m
= fun format x => %serialize% format (%deep_seq% x x),
deserialize | ExportFormat -> Str -> Dyn
deserialize : [| `Json, `Toml, `Yaml |] -> Str -> Dyn
| doc m%"
Deserializes the given string to a nickel value given the encoding of the string.

4
tests/contracts_fail.rs
View File

@ -32,8 +32,8 @@ fn id_fail() {
#[test]
fn enum_simple() {
assert_raise_blame!("`far | [|foo, bar|]");
assert_raise_blame!("123 | [|foo, bar|]");
assert_raise_blame!("`far | [|`foo, `bar|]");
assert_raise_blame!("123 | [|`foo, `bar|]");
assert_raise_blame!("`foo | [| |]");
}

18
tests/pass/contracts.ncl
View File

@ -28,34 +28,34 @@ let Assert = fun l x => x || %blame% l in
("hello" ++ " world" | Str) == "hello world",
# enums_simple
(`foo | [| foo, bar |]) == `foo,
(`bar | forall r. [| foo, bar ; r|]) == `bar,
(`foo | [| `foo, `bar |]) == `foo,
(`bar | forall r. [| `foo, `bar ; r|]) == `bar,
# enums_escaped
(`"foo:baz" | [| "foo:baz", "bar:baz" |]) == `"foo:baz",
(`"bar:baz" | forall r. [| "foo:baz", "bar:baz" ; r |]) == `"bar:baz",
(`"foo:baz" | [| `"foo:baz", `"bar:baz" |]) == `"foo:baz",
(`"bar:baz" | forall r. [| `"foo:baz", `"bar:baz" ; r |]) == `"bar:baz",
# enums_complex
let f : forall r. [| foo, bar ; r |] -> Num =
let f : forall r. [| `foo, `bar ; r |] -> Num =
fun x => switch { `foo => 1, `bar => 2, _ => 3, } x in
f `bar == 2,
let f : forall r. [| foo, bar ; r |] -> Num =
let f : forall r. [| `foo, `bar ; r |] -> Num =
fun x => switch { `foo => 1, `bar => 2, _ => 3, } x in
f `boo == 3,
let f : forall r. [| foo, "bar:baz" ; r |] -> Num =
let f : forall r. [| `foo, `"bar:baz" ; r |] -> Num =
fun x => switch { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
f `"bar:baz" == 2,
let f : forall r. [| foo, "bar:baz" ; r |] -> Num =
let f : forall r. [| `foo, `"bar:baz" ; r |] -> Num =
fun x => switch { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
f `"boo,grr" == 3,
# enums_applied
# Regression test for enum types converted to contracts outside of annotations
# causing issues wrt typechecking
let Wrapper = contract.apply [| Foo, Bar |] in
let Wrapper = contract.apply [| `Foo, `Bar |] in
(`Foo | Wrapper) == `Foo,
# records_simple

16
tests/pass/typechecking.ncl
View File

@ -50,28 +50,28 @@ let typecheck = [
((if (f true) then (f 2) else 3) : Num),
# enums_simple
(`bla : [|bla |]),
(`blo : [|bla, blo |]),
(`bla : forall r. [|bla ; r |]),
(`bla : forall r. [|bla, blo ; r |]),
(`bla : [|`bla |]),
(`blo : [|`bla, `blo |]),
(`bla : forall r. [|`bla ; r |]),
(`bla : forall r. [|`bla, `blo ; r |]),
((switch {`bla => 3} `bla) : Num),
((switch {`bla => 3, _ => 2} `blo) : Num),
# enums_complex
((fun x => switch {`bla => 1, `ble => 2} x) : [|bla, ble |] -> Num),
((fun x => switch {`bla => 1, `ble => 2} x) : [|`bla, `ble |] -> Num),
((fun x => switch {`bla => 1, `ble => 2, `bli => 4} (%embed% bli x))
: [|bla, ble |] -> Num),
: [|`bla, `ble |] -> Num),
((fun x =>
(switch {`bla => 3, `bli => 2} x)
+ (switch {`bli => 6, `bla => 20} x))
`bla
: Num),
let f : forall r. [|blo, ble ; r |] -> Num = fun x =>
let f : forall r. [|`blo, `ble ; r |] -> Num = fun x =>
switch {`blo => 1, `ble => 2, _ => 3} x in
(f `bli : Num),
let f : forall r. (forall p. [|blo, ble ; r |] -> [|bla, bli ; p |]) =
let f : forall r. (forall p. [|`blo, `ble ; r |] -> [|`bla, `bli ; p |]) =
fun x => switch {`blo => `bla, `ble => `bli, _ => `bla} x in
f `bli,

8
tests/typecheck_fail.rs
View File

@ -77,7 +77,7 @@ fn simple_forall() {
#[test]
fn enum_simple() {
assert_typecheck_fails!("`foo : [| bar |]");
assert_typecheck_fails!("`foo : [| `bar |]");
assert_typecheck_fails!("switch { `foo => 3} `bar : Num");
assert_typecheck_fails!("switch { `foo => 3, `bar => true} `bar : Num");
}
@ -85,7 +85,7 @@ fn enum_simple() {
#[test]
fn enum_complex() {
assert_typecheck_fails!(
"(fun x => switch {`bla => 1, `ble => 2, `bli => 4} x) : [| bla, ble |] -> Num"
"(fun x => switch {`bla => 1, `ble => 2, `bli => 4} x) : [| `bla, `ble |] -> Num"
);
// TODO typecheck this, I'm not sure how to do it with row variables
// LATER NOTE: this requires row subtyping, not easy
@ -95,12 +95,12 @@ fn enum_complex() {
(switch {`bla => 6, `blo => 20} x)) `bla : Num"
);
assert_typecheck_fails!(
"let f : forall r. [| blo, ble ; r |] -> Num =
"let f : forall r. [| `blo, `ble ; r |] -> Num =
fun x => (switch {`blo => 1, `ble => 2, `bli => 3} x) in
f"
);
assert_typecheck_fails!(
"let f : forall r. (forall p. [| blo, ble ; r |] -> [| bla, bli ; p |]) =
"let f : forall r. (forall p. [| `blo, `ble ; r |] -> [| `bla, `bli ; p |]) =
fun x => (switch {`blo => `bla, `ble => `bli, _ => `blo} x) in
f `bli"
);