tweag/nickel
1
1
Fork 0
mirror of https://github.com/tweag/nickel.git synced 2024-07-07 08:26:29 +03:00
Code Issues Projects Releases Wiki Activity

Use long names for string and numbers

Browse Source 
Rename the builtin `Num` and `Str` types to `Number` and `String`, and
use long names on a number of related functions and stdlib modules for
consistency. This is a breaking syntax change.
This commit is contained in:
Yann Hamdaoui 2023-03-07 10:52:26 +01:00
parent 44f722267b
commit 030c71eed7
No known key found for this signature in database
GPG Key ID: 96305DE11214ABE6
85 changed files with 920 additions and 904 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
HACKING.md
View File

@ -165,12 +165,12 @@ with a comment declaring the expected behaviour. For example
# test: blame
let Even = fun label value =>
if builtin.is_num value && value % 2 == 0 then
if builtin.is_number value && value % 2 == 0 then
value
else
contract.blame label in
let DivBy3 = fun label value =>
if builtin.is_num value && value % 3 == 0 then
if builtin.is_number value && value % 3 == 0 then
value
else
contract.blame label in

2
benches/arrays/fold.ncl
View File

@ -1,4 +1,4 @@
let letter | Num -> string.CharLiteral = fun n =>
let letter | Number -> string.CharLiteral = fun n =>
string.code "a" + (n % 26)
|> string.from_code in

2
benches/arrays/generate.ncl
View File

@ -8,7 +8,7 @@ let g = fun n => n*2 + 5 in
run = fun n => generate n g,
},
checked = {
generate_with_contract | forall a. Num -> (Num -> a) -> Array a = fun n g =>
generate_with_contract | forall a. Number -> (Number -> a) -> Array a = fun n g =>
if n == 0 then []
else generate_with_contract (n - 1) g @ [g n],

6
benches/arrays/primes.ncl
View File

@ -1,6 +1,6 @@
let range
| doc "Generate an array of integers in the range [`start`, `end`)."
| Num -> Num -> Array Num
| Number -> Number -> Array Number
= fun start end =>
if end <= start then
[]
@ -17,9 +17,9 @@ let Prime = contract.from_predicate is_prime in
let primes
| doc "Generate `max` primes using Sieve of Eratosthenes."
| Num -> Array Prime
| Number -> Array Prime
= fun max =>
let limit = num.pow max (1 / 2) in # sqrt(max)
let limit = number.pow max (1 / 2) in # sqrt(max)
let drop_multiples = fun x xs =>
let to_drop = max
|> array.generate (fun y => (y + 2) * x)

4
benches/arrays/random.ncl
View File

@ -6,10 +6,10 @@ let mgc
# of the 2021 paper "Computationally Easy, Spectrally Good Multipliers for
# Congruential Pseudorandom Number Generators", by Guy Steele and Sebastiano Vigna.
# But, they cannot be used because they require bit-shifting to select the 32 MSBs.
# let params = { m = num.pow 2 32, a = 2480367069 } in
# let params = { m = number.pow 2 32, a = 2480367069 } in
# These parameters are from the "Numerical Recipes" book.
let params = { m = num.pow 2 32, a = 1664525, c = 1013904223 } in
let params = { m = number.pow 2 32, a = 1664525, c = 1013904223 } in
let rec array_random = fun init n =>
if n == 0 then [init]

2
benches/arrays/sum.ncl
View File

@ -1,5 +1,5 @@
let rec sum
| Array Num -> Num
| Array Number -> Number
= fun xs =>
if array.length xs == 0 then 0
else array.first xs + sum (array.drop_first xs)

2
benches/mantis/deploy.ncl
View File

@ -46,7 +46,7 @@ fun vars =>
"eu-west-2"])
| default = ["eu-central-1", "us-east-2"],
fqdn = "mantis.ws",
networkConfig | Str
networkConfig | String
| default = m%"
mantis.blockchains.testnet-internal-nomad.bootstrap-nodes = [
%{string.join ",\n" bootstrapNodes."%{vars.namespace}"})

18
benches/mantis/jobs/mantis.ncl
View File

@ -7,26 +7,26 @@ let lib = import "../lib.ncl" in
let baseTags = [""] in
let Params = {
count | num.Nat
count | number.Nat
| default = 5,
role | [| `passive, `miner, `backup |],
datacenters | Dyn,
job | Dyn,
namespace | Str,
logLevel | Str,
mantisRev | Str,
fqdn | Str,
loggers | {_: Str},
namespace | String,
logLevel | String,
mantisRev | String,
fqdn | String,
loggers | {_: String},
network | lib.contracts.OneOf ["testnet-internal-nomad", "etc"]
| default = "testnet-internal-nomad",
networkConfig | Str,
networkConfig | String,
fastSync | Bool
| default = false,
reschedule | {..}
#{_ : lib.contracts.PseudoOr [
# lib.contracts.OrableFromPred builtin.is_str,
# lib.contracts.OrableFromPred builtin.is_num,
# lib.contracts.OrableFromPred builtin.is_string,
# lib.contracts.OrableFromPred builtin.is_number,
# lib.contracts.OrableFromPred builtin.is_bool,
# {
# pred = builtin.is_record,

2
benches/mantis/lib.ncl
View File

@ -15,7 +15,7 @@
SmallerEq = fun x => contract.from_predicate (fun y => y <= x),
MatchRegexp = fun regex label value =>
let str_match = string.is_match regex in
if builtin.is_str value then
if builtin.is_string value then
if str_match value then
value
else

332
benches/mantis/schemas/nomad/types.ncl
View File

@ -2,7 +2,7 @@ let lib = import "../../lib.ncl" in
# DUMMY
let time = {
parseDurationSecond = fun arg => 0 | Str,
parseDurationSecond = fun arg => 0 | String,
} in
# DUMMY
@ -11,11 +11,11 @@ let time = {
{
json = {
Job = {
Namespace | Str,
Namespace | String,
Id | Name,
Name | Str,
Name | String,
Type | [| `service, `system, `batch |],
Priority | num.Nat,
Priority | number.Nat,
Datacenters | array.NonEmpty,
TaskGroups | Array TaskGroup
| default = [],
@ -25,8 +25,8 @@ let time = {
| default = [],
Spreads | Array Spread
| default = [],
ConsulToken | lib.contracts.Nullable Str,
VaultToken | lib.contracts.Nullable Str,
ConsulToken | lib.contracts.Nullable String,
VaultToken | lib.contracts.Nullable String,
Vault | lib.contracts.Nullable json.Vault
| default = null,
Update | lib.contracts.Nullable json.Update
@ -38,30 +38,30 @@ let time = {
},
Affinity = {
LTarget | Str,
RTargety | Str,
LTarget | String,
RTargety | String,
Operand | (lib.contracts.OneOf [
"regexp", "set_contains_all", "set_contains", "set_contains_any", "=",
"==", "is", "!=", "not", ">", ">=", "<", "<=", "version"]),
Weight | num.Nat
Weight | number.Nat
| lib.contracts.NotEq 0
| lib.contracts.GreaterEq -100
| lib.contracts.SmallerEq 100,
},
Constraint = {
LTarget | lib.contracts.Nullable Str
LTarget | lib.contracts.Nullable String
| default = null,
RTarget | Str,
RTarget | String,
Operand | (lib.contracts.OneOf [
"regexp", "set_contains", "distinct_hosts", "distinct_property", "=",
"==", "is", "!=", "not", ">", ">=", "<", "<="]),
},
Spread = {
Attribute | Str,
Attribute | String,
Weight | lib.contracts.Nullable (lib.contracts.AllOf [
num.Nat,
number.Nat,
lib.contracts.GreaterEq -100,
lib.contracts.LesserEq 100])
| default = null,
@ -70,49 +70,49 @@ let time = {
},
SpreadTargetElem = {
Value | Str,
Value | String,
Percent | lib.contracts.Nullable (lib.contracts.AllOf [
num.PosNat,
number.PosNat,
lib.contracts.LesserEq 100])
| default = null,
},
RestartPolicy = {
Attempts | num.Nat,
Interval | num.Nat,
Delay | num.Nat,
Attempts | number.Nat,
Interval | number.Nat,
Delay | number.Nat,
Mode | (lib.contracts.OneOf ["delay", "fail"]),
},
Volume = {
Name | Str,
Name | String,
Type | (lib.contracts.OneOf [null, "host", "csi"]),
Source | Str,
Source | String,
ReadOnly | Bool
| default = false,
MountOptions
| lib.contracts.Nullable {
FsType | lib.contracts.Nullable Str
FsType | lib.contracts.Nullable String
| default = null,
mountFlags | lib.contracts.Nullable Str
mountFlags | lib.contracts.Nullable String
| default = null
}
| default = null,
},
ReschedulePolicy = {
Attempts | lib.contracts.Nullable num.Nat
Attempts | lib.contracts.Nullable number.Nat
| default = null,
DelayFunction | lib.contracts.Nullable (lib.contracts.OneOf [
"constant", "exponential", "fibonacci"])
| default = null,
Delay | lib.contracts.Nullable (lib.contracts.AllOf [
num.Nat,
number.Nat,
lib.contracts.GreaterEq 5*1000]) # >=time.ParseDuration("5s")
| default = null,
Interval | lib.contracts.Nullable num.Nat
Interval | lib.contracts.Nullable number.Nat
| default = null,
MaxDelay | lib.contracts.Nullable num.Nat
MaxDelay | lib.contracts.Nullable number.Nat
| default = null,
Unlimited | lib.contracts.Nullable Bool
| default = null,
@ -121,21 +121,21 @@ let time = {
Migrate = {
HealthCheck | [| `checks, `task_states |]
| default = `checks,
HealthyDeadline | num.Nat
HealthyDeadline | number.Nat
| default = 500000000000,
MaxParallel | num.Nat
MaxParallel | number.Nat
| default = 1,
MinHealthyTime | num.Nat
MinHealthyTime | number.Nat
| default = 10000000000,
},
Periodic = {
Enabled | Bool
| default = false,
TimeZone | Str
TimeZone | String
| default = "UTC",
SpecType = "cron",
Spec | Str,
Spec | String,
ProhibitOverlap | Bool
| default = false,
},
@ -143,14 +143,14 @@ let time = {
Update = {
AutoPromote | Bool | default = false,
AutoRevert | Bool | default = false,
Canary | num.Nat | default = 0,
Canary | number.Nat | default = 0,
HealthCheck | [| `checks, `task_states, `manual |]
| default = `checks,
HealthyDeadline | lib.contracts.Nullable num.Nat | default = null,
MaxParallel | num.Nat | default = 1,
MinHealthyTime | lib.contracts.Nullable num.Nat | default = null,
ProgressDeadline | lib.contracts.Nullable num.Nat | default = null,
Stagger | lib.contracts.Nullable num.Nat | default = null,
HealthyDeadline | lib.contracts.Nullable number.Nat | default = null,
MaxParallel | number.Nat | default = 1,
MinHealthyTime | lib.contracts.Nullable number.Nat | default = null,
ProgressDeadline | lib.contracts.Nullable number.Nat | default = null,
Stagger | lib.contracts.Nullable number.Nat | default = null,
},
TaskGroup = {
@ -160,15 +160,15 @@ let time = {
| default = [],
Spreads | Array Spread
| default = [],
Count | num.Nat
Count | number.Nat
| lib.contracts.Greater 0,
# TODO: Meta [string] string
Name | Str,
Name | String,
RestartPolicy | lib.contracts.Nullable json.RestartPolicy
| default = null,
Services | Array Service
| default = [],
ShutdownDelay | num.Nat | default = 0,
ShutdownDelay | number.Nat | default = 0,
Tasks | Array Task
| default = [],
# TODO Volumes: [string]: #json.Volume
@ -176,7 +176,7 @@ let time = {
EphemeralDisk
| lib.contracts.Nullable {
Migrate | Bool,
SizeMB | num.Nat,
SizeMB | number.Nat,
Sticky | Bool,
}
| default = null,
@ -186,7 +186,7 @@ let time = {
| default = null,
Networks | Array json.Network
| default = [],
StopAfterClientDisconnect | lib.contracts.Nullable num.Nat
StopAfterClientDisconnect | lib.contracts.Nullable number.Nat
| default = null,
Scaling = null,
Vault | lib.contracts.Nullable json.Vault
@ -194,17 +194,17 @@ let time = {
},
Port = {
Label | Str,
Value | lib.contracts.Nullable num.Nat | default = null, # used for static ports
To | lib.contracts.Nullable num.Nat | default = null,
HostNetwork | Str | default = "",
Label | String,
Value | lib.contracts.Nullable number.Nat | default = null, # used for static ports
To | lib.contracts.Nullable number.Nat | default = null,
HostNetwork | String | default = "",
},
Network = {
Mode | [| `host, `bridge |] | default = `host,
Device | Str | default = "",
CIDR | Str | default = "",
IP | Str | default = "",
Device | String | default = "",
CIDR | String | default = "",
IP | String | default = "",
DNS = null,
ReservedPorts | lib.contracts.Nullable (Array json.Port) | default = null,
DynamicPorts | lib.contracts.Nullable (Array json.Port) | default = null,
@ -213,31 +213,31 @@ let time = {
ServiceCheck = {
AddressMode | [| `alloc, `driver, `host |],
Args | lib.contracts.Nullable (Array Str) | default = null,
Args | lib.contracts.Nullable (Array String) | default = null,
CheckRestart | json.CheckRestart,
Command | Str | default = "",
Command | String | default = "",
Expose = false,
FailuresBeforeCritical | num.Nat | default = 0,
Id | Str | default = "",
InitialStatus | Str | default = "",
Interval | num.Nat | default = 10000000000,
Method | Str | default = "",
Name | Str | default = "",
Path | Str | default = "",
PortLabel | Str,
Protocol | Str | default = "",
SuccessBeforePassing | num.Nat | default = 0,
TaskName | Str | default = "",
Timeout | num.Nat,
FailuresBeforeCritical | number.Nat | default = 0,
Id | String | default = "",
InitialStatus | String | default = "",
Interval | number.Nat | default = 10000000000,
Method | String | default = "",
Name | String | default = "",
Path | String | default = "",
PortLabel | String,
Protocol | String | default = "",
SuccessBeforePassing | number.Nat | default = 0,
TaskName | String | default = "",
Timeout | number.Nat,
TLSSkipVerify | Bool | default = false,
Type | [| `http, `tcp, `script, `grpc |],
Body | lib.contracts.Nullable Str | default = null,
Body | lib.contracts.Nullable String | default = null,
# TODO Header [string] [...string]
},
CheckRestart | lib.contracts.Nullable {
Limit | num.Nat | default = 0,
Grace | num.Nat | default = 10000000000,
Limit | number.Nat | default = 0,
Grace | number.Nat | default = 10000000000,
IgnoreWarnings | Bool | default = false,
},
@ -247,31 +247,31 @@ let time = {
},
LogConfig | lib.contracts.Nullable {
MaxFiles | num.PosNat,
MaxFileSizeMB | num.PosNat,
MaxFiles | number.PosNat,
MaxFileSizeMB | number.PosNat,
},
Service = {
Id | Str | default = "",
Name | Str,
Tags | Array Str
Id | String | default = "",
Name | String,
Tags | Array String
| default = [],
CanaryTags | Array Str
CanaryTags | Array String
| default = [],
EnableTagOverride | Bool
| default = false,
PortLabel | Str,
PortLabel | String,
AddressMode | [| `alloc, `auto, `driver, `host |],
Checks | Array ServiceCheck
| default = [],
CheckRestart | json.CheckRestart,
Connect = null,
# TODO Meta: [string]: string
TaskName | Str | default = "",
TaskName | String | default = "",
},
Task = {
Name | Str,
Name | String,
Driver | [| `exec, `docker, `nspawn |],
Config | stanza.taskConfig
| {driver | Driver},
@ -283,21 +283,21 @@ let time = {
Services | Array Service
| default = [],
Resources = {
CPU | num.Nat
CPU | number.Nat
| lib.contracts.GreaterEq 100
| default = 100,
MemoryMB | num.Nat
MemoryMB | number.Nat
| lib.contracts.GreaterEq 32
| default = 300,
DiskMB | lib.contracts.Nullable num.Nat
DiskMB | lib.contracts.Nullable number.Nat
| default = null,
},
Meta = {},
RestartPolicy | lib.contracts.Nullable json.RestartPolicy | default = null,
ShutdownDelay | num.Nat | default = 0,
User | Str | default = "",
ShutdownDelay | number.Nat | default = 0,
User | String | default = "",
Lifecycle | lib.contracts.Nullable json.Lifecycle | default = null,
KillTimeout | lib.contracts.Nullable num.Nat | default = null,
KillTimeout | lib.contracts.Nullable number.Nat | default = null,
LogConfig | json.LogConfig,
Artifacts | Array json.Artifact
| default = [],
@ -307,44 +307,44 @@ let time = {
VolumeMounts | Array json.VolumeMount
| default = [],
Leader | Bool | default = false,
KillSignal | Str,
KillSignal | String,
ScalingPolicies = null,
Vault | lib.contracts.Nullable json.Vault | default = null,
},
VolumeMount = {
Destination | Str,
PropagationMode | Str,
Destination | String,
PropagationMode | String,
ReadOnly | Bool,
Volume | Str,
Volume | String,
},
Artifact = {
GetterSource | Str,
GetterSource | String,
# TODO GetterOptions: [string]: string
# TODO GetterHeaders: [string]: string
GetterMode | [| `any, `file, `dir |] | default = `any,
RelativeDest | Str,
RelativeDest | String,
},
Template = {
SourcePath | Str | default = "",
DestPath | Str,
EmbeddedTmpl | Str,
SourcePath | String | default = "",
DestPath | String,
EmbeddedTmpl | String,
ChangeMode | [| `restart, `noop, `signal |] | default = `restart,
ChangeSignal | Str | default = "",
Splay | num.Nat | default = 5000000000,
ChangeSignal | String | default = "",
Splay | number.Nat | default = 5000000000,
Perms | lib.contracts.MatchRegexp "^[0-7]{4}$" | default = "0644",
LeftDelim | Str,
RightDelim | Str,
LeftDelim | String,
RightDelim | String,
Envvars | Bool,
},
Vault = {
ChangeMode | [| `noop, `restart, `signal |] | default = `restart,
ChangeSignal | Str | default = "",
ChangeSignal | String | default = "",
Env | Bool | default = true,
Namespace | Str | default = "",
Namespace | String | default = "",
Policies | array.NonEmpty,
}
},
@ -356,7 +356,7 @@ let time = {
toJson = json.Job & {
job = stanza.job,
jobName | Str,
jobName | String,
Name = jobName,
Datacenters = job.datacenters,
Namespace = job.namespace,
@ -683,7 +683,7 @@ let time = {
stanza = {
job = let type_schema = [| `batch, `service, `system |] in {
datacenters | array.NonEmpty,
namespace | Str,
namespace | String,
type | type_schema
| default = `service,
affinities | Array stanza.affinity
@ -698,7 +698,7 @@ let time = {
| default = null,
vaultc | lib.contracts.Nullable stanza.vault
| default = null,
priority_ | num.Nat
priority_ | number.Nat
| default = 50,
periodic | lib.contracts.Nullable stanza.periodic
| default = null,
@ -709,40 +709,40 @@ let time = {
migrate = {
health_check | [| `checks, `task_states |]
| default = `checks,
healthy_deadline | num.Nat
healthy_deadline | number.Nat
| default = 500000000000,
max_parallel | num.Nat
max_parallel | number.Nat
| default = 1,
min_healthy_time | num.Nat
min_healthy_time | number.Nat
| default = 10000000000,
},
periodic = {
time_zone | Str
time_zone | String
| default = "UTC",
prohibit_overlap | Bool
| default = false,
cron | Str,
cron | String,
},
affinity = {
LTarget | Str
LTarget | String
| default = null,
RTarget | Str,
RTarget | String,
Operand | lib.contracts.OneOf
["regexp", "set_contains_all", "set_contains", "set_contains_any", "=",
"==", "is", "!=", "not", ">", ">=", "<", "<=", "version"]
| default = "=",
Weight | num.Nat
Weight | number.Nat
| lib.contracts.NotEq 0
| lib.contracts.GreaterEq -100
| lib.contracts.SmallerEq 100,
},
constraint = {
attribute | Str
attribute | String
| default = null,
value | Str,
value | String,
operator | lib.contracts.OneOf
["=", "!=", ">", ">=", "<", "<=", "distinct_hosts", "distinct_property",
"regexp", "set_contains", "version", "semver", "is_set",
@ -751,10 +751,10 @@ let time = {
},
spread = {
attribute | lib.contracts.Nullable Str
attribute | lib.contracts.Nullable String
| default = null,
weight | lib.contracts.Nullable (lib.contracts.AllOf
[num.Nat,
[number.Nat,
lib.contracts.GreaterEq -100,
lib.contracts.SmallerEq 100])
| default = null,
@ -763,10 +763,10 @@ let time = {
},
targetElem = {
value | lib.contracts.Nullable Str
value | lib.contracts.Nullable String
| default = null,
percent | lib.contracts.Nullable (lib.contracts.AllOf [
num.Nat,
number.Nat,
lib.contracts.GreaterEq -100,
lib.contracts.SmallerEq 100])
| default = null,
@ -774,7 +774,7 @@ let time = {
ephemeral_disk =
lib.contracts.Nullable {
size | num.PosNat,
size | number.PosNat,
migrate | Bool | default = false,
sticky | Bool | default = false,
},
@ -792,7 +792,7 @@ let time = {
| default = null,
service | {_: stanza.service},
task | {_: stanza.task},
count | num.Nat,
count | number.Nat,
volume | {_: stanza.volume} | default = {},
vault | lib.contracts.Nullable stanza.vault
| default = null,
@ -831,23 +831,23 @@ let time = {
network = {
mode | [| `host, `bridge |],
dns | lib.contracts.Nullable {
servers | Array Str
servers | Array String
| default = []
}
| default = null,
port | {_: {
static | lib.contracts.Nullable num.Nat
static | lib.contracts.Nullable number.Nat
| default = null,
to | lib.contracts.Nullable num.Nat
to | lib.contracts.Nullable number.Nat
| default = null,
host_network | Str
host_network | String
| default = "",
}
},
},
check_restart = {
limit | num.PosNat,
limit | number.PosNat,
grace | Duration,
ignore_warnings | Bool
| default = false,
@ -856,34 +856,34 @@ let time = {
service = {
check_restart | lib.contracts.Nullable stanza.check_restart
| default = null,
port | Str,
port | String,
address_mode | [| `alloc, `driver, `auto, `host |]
| default = `auto,
tags | Array Str
tags | Array String
| default = [],
task | Str
task | String
| default = "",
check | {_: stanza.check} | default = {},
meta | {_: Str} | default = {},
meta | {_: String} | default = {},
},
check = {
address_mode | [| `alloc, `driver, `host |]
| default = `driver,
type | [| `http, `tcp, `script, `grpc |],
port | Str,
port | String,
interval | Duration,
timeout | Duration,
check_restart | lib.contracts.Nullable stanza.check_restart
| default = null,
header | {_: Array Str} | default = {},
body | lib.contracts.Nullable Str
header | {_: Array String} | default = {},
body | lib.contracts.Nullable String
| default = null,
initial_status | (lib.contracts.OneOf ["passing", "warning", "critical", ""])
| default = "",
success_before_passing | num.Nat
success_before_passing | number.Nat
| default = 0,
failures_before_critical | num.Nat
failures_before_critical | number.Nat
| default = 0,
tls_skip_verify | Bool
| default = false,
@ -903,30 +903,30 @@ let time = {
# path: ""
# protocol: ""
#}
path | Str | default = "",
method | Str | default = "",
protocol | Str | default = "",
path | String | default = "",
method | String | default = "",
protocol | String | default = "",
},
#Hmm... actual union :( hard to do
#taskConfig: dockerConfig | execConfig
execConfig = {
flake | Str,
command | Str,
args | Array Str
flake | String,
command | String,
args | Array String
| default = [],
},
label = {_: Str},
label = {_: String},
dockerConfig = {
image | Str,
command | lib.contracts.Nullable Str
image | String,
command | lib.contracts.Nullable String
| default = null,
args | Array Str
args | Array String
| default = [],
ports | Array Str
ports | Array String
| default = [],
labels | Array label
| default = [],
@ -940,8 +940,8 @@ let time = {
},
dockerConfigLoggingConfig = {
tag | Str,
labels | Str,
tag | String,
labels | String,
},
lifecycle = {
@ -951,8 +951,8 @@ let time = {
},
logs = {
max_files | num.PosNat,
max_file_size | num.PosNat,
max_files | number.PosNat,
max_file_size | number.PosNat,
},
task = {
@ -966,11 +966,11 @@ let time = {
artifact | {_: {
# actually, the key must be the destination
# destination | Destination,
headers | {_: Str},
headers | {_: String},
mode | [| `any, `file, `dir |]
| default = `any,
options | {_: Str},
source | Str,
options | {_: String},
source | String,
}
} | default = {},
@ -988,10 +988,10 @@ let time = {
driver | [| `exec, `docker, `nspawn |],
env | {_: Str}
env | {_: String}
| default = {},
kill_signal | Str
kill_signal | String
| default = "SIGINT",
#TODO
@ -1009,10 +1009,10 @@ let time = {
| default = null,
resources = {
cpu | num.Nat
cpu | number.Nat
| lib.contracts.GreaterEq 100,
memory
| num.Nat
| number.Nat
| lib.contracts.GreaterEq 32,
},
@ -1022,21 +1022,21 @@ let time = {
# Actually, the key must be a destination, there is no
# destination field
# destination | Destination,
data | Str
data | String
| default = "",
source | Str
source | String
| default = "",
env | Bool
| default = false,
change_mode | [| `restart, `noop, `signal |]
| default = `restart,
change_signal | Str
change_signal | String
| default = "",
perms | (lib.contracts.MatchRegexp "^[0-7]{4}$")
| default = "0644",
left_delimiter | Str
left_delimiter | String
| default = "{{",
right_delimiter | Str
right_delimiter | String
| default = "}}",
splay | Duration
| default = "3s",
@ -1058,7 +1058,7 @@ let time = {
restart = {
interval | Duration,
attempts | num.PosNat,
attempts | number.PosNat,
delay | Duration,
mode | [| `delay, `fail |],
},
@ -1068,13 +1068,13 @@ let time = {
| default = false,
auto_revert | Bool
| default = false,
canary | num.Nat
canary | number.Nat
| default = 0,
health_check | [| `checks, `task_states, `manual |]
| default = `checks,
healthy_deadline | Duration
| default = "5m",
max_parallel | num.Nat
max_parallel | number.Nat
| default = 1,
min_healthy_time | Duration
| default = "10s",
@ -1087,19 +1087,19 @@ let time = {
vault = {
change_mode | [| `noop, `restart, `signal |]
| default = `restart,
change_signal | Str
change_signal | String
| default = "",
env | Bool
| default = true,
namespace | Str
namespace | String
| default = "",
policies | Array Str
policies | Array String
| default = [],
},
volume = {
type | [| `host, `csi |],
source | Str,
source | String,
read_only | Bool
| default = false,
#TODO: dependent if
@ -1113,14 +1113,14 @@ let time = {
volume_mount = {
# Specifies the group volume that the mount is going to access.
volume | Str
volume | String
| default = "",
# Specifies where the volume should be mounted inside the task's
# allocation.
destination | Str
destination | String
| default = "",
foo : Str = destination ++ volume,
foo : String = destination ++ volume,
# When a group volume is writeable, you may specify that it is read_only
# on a per mount level using the read_only option here.

4
benches/mantis/tasks/telegraf.ncl
View File

@ -1,8 +1,8 @@
let types = import "../schemas/nomad/types.ncl" in
{
prometheusPort | Str,
clientId | Str
prometheusPort | String,
clientId | String
| default = "{{ env \"NOMAD_JOB_NAME\" }}-{{ env \"NOMAD_ALLOC_INDEX\" }}",
driver = `exec,

30
benches/nixpkgs/lists.ncl
View File

@ -87,7 +87,7 @@
"%
= fun op nul list => array.fold_left op nul list,
imap0: forall a b. (Num -> a -> b) -> (Array a) -> (Array b)
imap0: forall a b. (Number -> a -> b) -> (Array a) -> (Array b)
| doc m%%"
Map with index starting from 0
@ -97,7 +97,7 @@
"%%
= fun f list => array.generate (fun n => f n (array.at n list)) (array.length list),
imap1: forall a b. (Num -> a -> b) -> (Array a) -> (Array b)
imap1: forall a b. (Number -> a -> b) -> (Array a) -> (Array b)
| doc m%%"
Map with index starting from 1
@ -200,9 +200,9 @@
element of `list`.
Example:
any builtin.is_str [ 1, "a", { } ]
any builtin.is_string [ 1, "a", { } ]
>> true
any builtin.is_str [ 1, { } ]
any builtin.is_string [ 1, { } ]
>> false
"%
= fun pred => foldr (fun x y => if pred x then true else y) false,
@ -220,7 +220,7 @@
"%
= fun pred => foldr (fun x y => if pred x then y else false) true,
count: forall a. (a -> Bool) -> Array a -> Num
count: forall a. (a -> Bool) -> Array a -> Number
| doc m%"
Count how many elements of `list` match the supplied predicate
function.
@ -279,7 +279,7 @@
"%
= fun x => if builtin.is_array x then (x | Array Dyn) else [x],
range: Num -> Num -> Array Num
range: Number -> Number -> Array Number
| doc m%"
Return a list of integers from `first' up to and including `last'.
@ -316,7 +316,7 @@
) { right = [], wrong = [] },
# can not be staticaly checked (see issue #423)
groupBy | forall a. (a -> Str) -> Array a -> { _: Array a}
groupBy | forall a. (a -> String) -> Array a -> { _: Array a}
| doc m%"
Splits the elements of a list into many lists, using the return value of a predicate.
Predicate should return a string which becomes keys of attrset `groupBy' returns.
@ -340,7 +340,7 @@
{ "%{key}" = (r."%{key}" @ [e]) } & (record.remove key r)
) {},
groupBy_ : forall a b. (b -> a -> b) -> b -> (a -> Str) -> Array a -> { _: b}
groupBy_ : forall a b. (b -> a -> b) -> b -> (a -> String) -> Array a -> { _: b}
| doc m%"
as `groupBy` and allows to customise the combining function and initial value
@ -367,7 +367,7 @@
fst
# Second list
snd
=> array.generate (fun n => f (array.at n fst) (array.at n snd)) (num.min (array.length fst) (array.length snd)),
=> array.generate (fun n => f (array.at n fst) (array.at n snd)) (number.min (array.length fst) (array.length snd)),
zipLists: forall a b. Array a -> Array b -> Array { fst: a, snd: b}
| doc m%"
@ -498,7 +498,7 @@
if len < 2 then list
else (sort strictLess pivot.left) @ [ first ] @ (sort strictLess pivot.right),
compareLists: forall a. (a -> a -> Num) -> Array a -> Array a -> Num
compareLists: forall a. (a -> a -> Number) -> Array a -> Array a -> Number
| doc m%"
Compare two lists element-by-element.
@ -524,7 +524,7 @@
then compareLists cmp (array.drop_first a) (array.drop_first b)
else rel,
# naturalSort: Array Str -> Array Str
# naturalSort: Array String -> Array String
# | doc m%"
# Sort list using "Natural sorting".
# Numeric portions of strings are sorted in numeric order.
@ -539,13 +539,13 @@
# "%
# # TODO: broken. how to implement it in nickel?
# = fun lst =>
# let vectorise = fun s => array.map (fun x => if builtin.is_array x then (array.first x) | Num else x | Num) (string.split "(0|[1-9][0-9]*)" s) | Array Dyn
# let vectorise = fun s => array.map (fun x => if builtin.is_array x then (array.first x) | Number else x | Number) (string.split "(0|[1-9][0-9]*)" s) | Array Dyn
# in
# let prepared = array.map (fun x => [ (vectorise x), x ]) lst in # remember vectorised version for O(n) regex splits
# let less = fun a b => (compareLists compare (array.first a) (array.first b)) < 0 in
# array.map (fun x => array.at 1 x) (sort less prepared),
take: forall a. Num -> Array a -> Array a
take: forall a. Number -> Array a -> Array a
| doc m%"
Return the first (at most) N elements of a list.
@ -560,7 +560,7 @@
# Number of elements to take
count => sublist 0 count,
drop: forall a. Num -> Array a -> Array a
drop: forall a. Number -> Array a -> Array a
| doc m%"
Remove the first (at most) N elements of a list.
@ -577,7 +577,7 @@
# Input list
lst => sublist count (array.length lst) lst,
sublist: forall a. Num -> Num -> Array a -> Array a
sublist: forall a. Number -> Number -> Array a -> Array a
| doc m%"
Return a list consisting of at most `count` elements of `list`,
starting at index `start`.

91
doc/manual/contracts.md
View File

@ -13,20 +13,20 @@ normally. Otherwise, an error is raised. In Nickel, you can apply a contract
using the `|` operator:
```nickel
let x = (1 + 1 | Num) in x
let x = (1 + 1 | Number) in x
```
Contract can also be attached to identifiers in a definition:
```nickel
# let-binding: equivalent to the previous example
let x | Num = 1 + 1 in x
let x | Number = 1 + 1 in x
# on a record field
{x | Num = 1 + 1}
{x | Number = 1 + 1}
```
Here, `x` is bound to a `Num` contract. When evaluating `x`, the following steps
Here, `x` is bound to a `Number` contract. When evaluating `x`, the following steps
are performed:
1. Evaluate `1 + 1`.
@ -35,15 +35,14 @@ are performed:
```text
$ nickel repl
nickel>1 + 1 | Num
nickel>1 + 1 | Number
2
nickel>"a" | Num
nickel>"a" | Number
error: contract broken by a value.
[..]
```
Contracts corresponding to the basic types `Num`, `Str`, `Bool` and `Dyn` are
Contracts corresponding to the basic types `Number`, `String`, `Bool` and `Dyn` are
available. `Dyn` is a contract that never fails.
## User-defined contracts
@ -57,7 +56,7 @@ properties. Let us see how to define our very own contract. We start the REPL
```nickel
let IsFoo = fun label value =>
if builtin.is_str value then
if builtin.is_string value then
if value == "foo" then
value
else
@ -122,8 +121,8 @@ Here is an example of a port number contract:
```nickel
let Port = contract.from_predicate (fun value =>
builtin.is_num value &&
num.is_int value &&
builtin.is_number value &&
number.is_int value &&
value >= 0 &&
value <= 65535)
```
@ -134,7 +133,7 @@ Let us consider a contract for bound checking:
```nickel
let Between5And10 = contract.from_predicate (fun value =>
builtin.is_num value &&
builtin.is_number value &&
value >= 5 &&
value <= 10) in
let MyConfig = {
@ -146,11 +145,11 @@ Now, we add a new field to our schema, that must be between `0` and `1`:
```nickel
let Between5And10 = contract.from_predicate (fun value =>
builtin.is_num value &&
builtin.is_number value &&
value >= 5 &&
value <= 10) in
let Between0And1 = contract.from_predicate (fun value =>
builtin.is_num value &&
builtin.is_number value &&
value >= 0 &&
value <= 1) in
let MyConfig = {
@ -171,7 +170,7 @@ let Between = fun min max =>
value <= max) in
# alternative without from_predicate
let BetweenAlt = fun min max label value =>
if builtin.is_num value &&
if builtin.is_number value &&
value >= min &&
value <= max then
value
@ -202,9 +201,9 @@ let Nullable = fun contract label value =>
else
contract.apply contract label value in
# succeeds
null | Nullable Num
null | Nullable Number
# succeeds too
1 | Nullable Num
1 | Nullable Number
```
## Compound contracts
@ -221,11 +220,11 @@ missing:
```nickel
let MyConfig = {
path | Str,
path | String,
connection | {
server_port | Port,
host | Str,
host | String,
}
} in
@ -306,9 +305,9 @@ or default value:
```text
nickel>let MyConfig = {
foo | doc "This documentation will propagate to the final value!"
| Str
| String
| default = "foo",
bar | Num,
bar | Number,
}
nickel>let config | MyConfig = {bar = 2}
nickel> builtin.serialize `Json config
@ -318,7 +317,7 @@ nickel> builtin.serialize `Json config
}"
nickel>
nickel>:query config.foo
* contract: Str
* contract: String
* default: "foo"
* documentation: This documentation will propagate to the final value!
```
@ -328,7 +327,7 @@ nickel>:query config.foo
By default, record contracts are closed, meaning that additional fields are forbidden:
```text
nickel>let Contract = {foo | Str}
nickel>let Contract = {foo | String}
nickel>{foo = "a", bar = 1} | Contract
error: contract broken by a value [extra field `bar`].
[..]
@ -338,7 +337,7 @@ If you want to allow additional fields, append `, ..` after the last field
definition to define an open contract:
```text
nickel>let Contract = {foo | Str, ..}
nickel>let Contract = {foo | String, ..}
nickel>{foo = "a", bar = 1} | Contract
{ foo = <contract,value="a">, bar = 1}
```
@ -354,7 +353,7 @@ example:
```text
nickel>let Secure = {
must_be_very_secure | Bool = true,
data | Str,
data | String,
}
nickel>builtin.serialize `Json ({data = ""} | Secure)
"{
@ -378,23 +377,23 @@ error: Non mergeable terms
**Warning: `=` vs `|`**
It may be tempting to use `=` instead of `|` to attach a record contract to a
field. That is, writing `Contract = {foo = {bar | Str}}` instead of
`Contract = {foo | {bar | Str}}`. When applying this contract, the merging
operator will apply the `Str` contract to the field `foo` of the checked value.
field. That is, writing `Contract = {foo = {bar | String}}` instead of
`Contract = {foo | {bar | String}}`. When applying this contract, the merging
operator will apply the `String` contract to the field `foo` of the checked value.
At first sight, `=` also fits the bill. However, there are a number of subtle
but potentially surprising differences.
One concerns open contracts. Merging never requires the presence of specific
fields: thus, the contract `{bar | Str}` attached to `foo` will actually behave
fields: thus, the contract `{bar | String}` attached to `foo` will actually behave
as an open contract, even if you didn't use `..`. This is usually not what you
want:
```text
nickel>let ContractPipe = {
sub_field | {foo | Str}
sub_field | {foo | String}
}
nickel>let ContractEq = {
sub_field = {foo | Str}
sub_field = {foo | String}
}
nickel>{sub_field.foo = "a", sub_field.bar = "b"} | ContractPipe
error: contract broken by a value [extra field `bar`].
@ -410,7 +409,7 @@ in mind, **you should use `|` instead of `=` when attaching record contracts**.
### Types constructors for contracts
We've already seen that the primitive types `Num`, `Str` and `Bool` can be used
We've already seen that the primitive types `Number`, `String` and `Bool` can be used
as contracts. In fact, any type constructor of the
[static type system](./typing.md) can be used to combine contracts.
@ -421,7 +420,7 @@ contract to each element:
```text
nickel>let VeryBig = contract.from_predicate (fun value =>
builtin.is_num value
builtin.is_number value
&& value >= 1000)
nickel>[1000, 10001, 2] | Array VeryBig
error: contract broken by a value.
@ -447,14 +446,14 @@ that must hold about the return value of the function.
##### Caller vs callee
Function contracts, as opposed to a contract like `Num`, have the peculiarity of
Function contracts, as opposed to a contract like `Number`, have the peculiarity of
involving two parties in the contract checking. For example:
```nickel
let add_semi | Str -> Str = fun x => x ++ ";" in
let add_semi | String -> String = fun x => x ++ ";" in
add_semi 1
let wrong | Str -> Str = fun x => 0 in
let wrong | String -> String = fun x => 0 in
wrong "a"
```
@ -476,12 +475,12 @@ The interpreter automatically performs book-keeping for functions contracts in
order to make this caller/callee distinction:
```text
nickel>let add_semi | Str -> Str = fun x => x ++ ";" in
nickel>let add_semi | String -> String = fun x => x ++ ";" in
add_semi 1
error: contract broken by the caller.
[..]
nickel>let wrong | Str -> Str = fun x => 0 in
nickel>let wrong | String -> String = fun x => 0 in
wrong "a"
error: contract broken by a function.
[..]
@ -494,12 +493,12 @@ functions as well. Higher-order functions are functions that take other
functions as parameters. Here is an example:
```text
nickel>let apply_fun | (Num -> Num) -> Num = fun f => f 0 in
nickel>let apply_fun | (Number -> Number) -> Number = fun f => f 0 in
apply_fun (fun x => "a")
error: contract broken by the caller.
┌─ :1:9
│
1 │ (Num -> Num) -> Num
1 │ (Number -> Number) -> Number
│ --- expected return type of a function provided by the caller
│
┌─ repl-input-17:2:21
@ -518,7 +517,7 @@ records as an extensible dictionary, that is a key/value store, where keys are
strings and values respect `Contract`. Example:
```nickel
let occurrences | {_: Num} = {a = 2, b = 3, "!" = 5, "^" = 1} in
let occurrences | {_: Number} = {a = 2, b = 3, "!" = 5, "^" = 1} in
occurrences."!"
```
@ -578,7 +577,7 @@ value, which is wrapping the original value with delayed checks inside**. This
is the rationale behind contracts returning a value. Let us see:
```nickel
let NumBoolDict = fun label value =>
let NumberBoolDict = fun label value =>
if builtin.is_record value then
let check_fields = value
|> record.fields
@ -631,7 +630,7 @@ value and continues with the second argument (here, our wrapped `value`).
Let us see if we indeed preserved laziness:
```text
nickel>let config | NumBoolDict = {
nickel>let config | NumberBoolDict = {
"1" = 1 + "a", # Same as our previous "fail"
"0" | doc "Some information" = true,
}
@ -644,7 +643,7 @@ Yes! Our contract doesn't unduly cause the evaluation of the field `"1"`. Does
it check anything, though?
```text
nickel>let config | NumBoolDict = {
nickel>let config | NumberBoolDict = {
not_a_number = false,
"0" | doc "Some information" = false,
}
@ -652,7 +651,7 @@ nickel>:q config."0"
error: contract broken by a value [field name `not_a_number` is not a number].
[..]
nickel>let config | NumBoolDict = {
nickel>let config | NumberBoolDict = {
"0" | doc "Some information" = "not a boolean",
}
nickel>:q config."0"
@ -675,7 +674,7 @@ prefer to report this error as soon as possible.
#### Conclusion
Our `NumToBool` contract doesn't perform all the checks needed right away.
Our `NumberBoolDict` contract doesn't perform all the checks needed right away.
Instead, **it returns a new value, which is wrapping the original value with
delayed checks inside**. Doing so preserves laziness of the language and only
triggers the checks when the values are used or exported in a configuration.

8
doc/manual/cookbook.md
View File

@ -22,8 +22,8 @@ DON'T
```nickel
{
foo : Num -> Num = fun x => x + 1,
bar : Num -> Num = foo,
foo : Number -> Number = fun x => x + 1,
bar : Number -> Number = foo,
}
```
@ -34,8 +34,8 @@ BUT DO
foo = fun x => x + 1,
bar = foo,
} : {
foo : Num -> Num,
bar : Num -> Num,
foo : Number -> Number,
bar : Number -> Number,
}
```

36
doc/manual/correctness.md
View File

@ -81,14 +81,14 @@ Type annotations are introduced with `:`. For example:
```text
$ nickel repl
nickel> 1 + 1.5 : Num
nickel> 1 + 1.5 : Number
2.5
nickel> let f : Num -> Num = fun x => x + 1
nickel> let f : Number -> Number = fun x => x + 1
nickel> f 0
1
nickel> "not a Num" : Num
nickel> "not a Number" : Number
error: incompatible types
[..]
```
@ -176,8 +176,8 @@ An idiomatic way to express these properties in Nickel is to use the following
annotation:
```nickel
forall a. Array {key: Str, value: a}
-> {keys: Array Str, values: Array a}
forall a. Array {key: String, value: a}
-> {keys: Array String, values: Array a}
```
Where `forall a.` means that `a` can be any type, but that the `a` in the input
@ -191,7 +191,7 @@ using contract and type annotations.
`split` can be given a contract annotation as follows:
```nickel
split | forall a. Array {key: Str, value: a} -> {keys: Array Str, values: Array a} = # etc.
split | forall a. Array {key: String, value: a} -> {keys: Array String, values: Array a} = # etc.
```
Contract annotations are checked at runtime. At this point functions are
@ -199,8 +199,8 @@ essentially opaque values which must be passed an argument in order to evaluate
further. As a result, `split`'s contract will only be checked when the function
is actually applied to an argument. When this happens, the contract checks that:
1. the provided argument satisfies the `Array {key: Str, value: a}` contract,
2. the return value satisfies the `{keys: Array Str, values: Array a}` contract.
1. the provided argument satisfies the `Array {key: String, value: a}` contract,
2. the return value satisfies the `{keys: Array String, values: Array a}` contract.
Those checks produce useful error message when the caller passes arguments of
the wrong type, or if function were to return a value of the wrong type. But the
@ -220,7 +220,7 @@ function contract for `split` has the following limitations:
┌─ /path/to/lib.ncl:6:27
│
6 │ keys = acc.keys @ pair.key,
│ ^^^^^^^^ this expression has type Str, but Array was expected
│ ^^^^^^^^ this expression has type String, but Array was expected
│
┌─ /path/to/config.ncl:2:41
│
@ -251,7 +251,7 @@ that:
`split` can be given a type annotation as follows:
```nickel
split : forall a. Array {key: Str, value: a} -> {keys: Array Str, values: Array a} = # etc.
split : forall a. Array {key: String, value: a} -> {keys: Array String, values: Array a} = # etc.
```
Type annotations also give rise to contracts, which means that even if `split`'s
@ -271,8 +271,8 @@ error: incompatible rows declaration
│
[..]
error: While typing field `key`: incompatible types
= The type of the expression was expected to be `Array Str`
= The type of the expression was inferred to be `Str`
= The type of the expression was expected to be `Array String`
= The type of the expression was inferred to be `String`
= These types are not compatible
```
@ -325,7 +325,7 @@ If we write:
let {OptLevel} = import "lib.ncl" in
let level = 1 in
{
opt_level : OptLevel = "A" ++ string.from_num level,
opt_level : OptLevel = "A" ++ string.from_number level,
}
```
@ -335,16 +335,16 @@ We get:
error: incompatible types
┌─ /path/to/config.ncl:4:26
│
4 │ opt_level : OptLevel = "A" ++ string.from_num level,
4 │ opt_level : OptLevel = "A" ++ string.from_number level,
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ this expression
│
= The type of the expression was expected to be `OptLevel`
= The type of the expression was inferred to be `Str`
= The type of the expression was inferred to be `String`
= These types are not compatible
```
Because `OptLevel` is a custom predicate, the typechecker is unable to check
whether `"A"` concatenated with `string.from_num 1"` is a valid value. For that
whether `"A"` concatenated with `string.from_number 1"` is a valid value. For that
matter, even `"O1" : OptLevel` doesn't typecheck.
It *is* possible to build values which the typechecker will accept as valid
@ -364,7 +364,7 @@ go:
let {OptLevel} = import "lib.ncl" in
let level = 4 in
{
opt_level | OptLevel = "A" ++ string.from_num level,
opt_level | OptLevel = "A" ++ string.from_number level,
}
```
@ -379,7 +379,7 @@ error: contract broken by a value.
│
┌─ /path/to/config.ncl:4:26
│
3 │ opt_level | OptLevel = "A" ++ string.from_num level,
3 │ opt_level | OptLevel = "A" ++ string.from_number level,
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^ applied to this expression
│
┌─ <unknown> (generated by evaluation):1:1

18
doc/manual/merging.md
View File

@ -159,7 +159,7 @@ Evaluates to the record:
When one or both of the common fields are not records, the merge will fail
unless one of the following condition hold:
- They are both of a primitive data type `Num`, `Bool`, `Enum`, `String` and
- They are both of a primitive data type `Number`, `Bool`, `Enum`, `String` and
they are equal
- They are both null
@ -209,7 +209,7 @@ Then the merge `left & right` evaluates to the record:
For two values `v1` and `v2`, if at least one value is not a record, then
```text
v1 & v2 = v1 if (type_of(v1) is Num, Bool, Str, Enum or v1 == null)
v1 & v2 = v1 if (type_of(v1) is Number, Bool, String, Enum or v1 == null)
AND v1 == v2
_|_ otherwise (indicates failure)
```
@ -458,15 +458,15 @@ This evaluates to:
[contracts section](./contracts.md) for a thorough introduction to contracts in
Nickel.
Fields may have contracts attached, either directly, as in `{foo | Num = 1}`, or
propagated from an annotation higher up, as in `{foo = 1} | {foo | Num}`. In
both cases, `foo` must satisfy the contract `Num`. What happens if the value of
Fields may have contracts attached, either directly, as in `{foo | Number = 1}`, or
propagated from an annotation higher up, as in `{foo = 1} | {foo | Number}`. In
both cases, `foo` must satisfy the contract `Number`. What happens if the value of
`foo` is altered in a subsequent merge? For example:
- Should `{foo | default | Num = 1} & {foo = "bar"}` succeed, although `foo`
- Should `{foo | default | Number = 1} & {foo = "bar"}` succeed, although `foo`
would be a string in the final result?
- Should `{foo | {subfield | Str} = {subfield = "a"}} & {foo.other_subfield = 1}`
succeed, although a closed contract `{subfield | Str}` is attached to `foo`,
- Should `{foo | {subfield | String} = {subfield = "a"}} & {foo.other_subfield = 1}`
succeed, although a closed contract `{subfield | String}` is attached to `foo`,
and the final result would have an additional field `other_subfield` ?
Nickel chooses to answer **no** to both. In general, when a contract is attached
@ -508,7 +508,7 @@ Leftn, Right1, .., Rightk`. Here, we ignore the case of type annotations such as
let Port
| doc "A valid port number"
= contract.from_predicate (fun value =>
builtin.is_num value &&
builtin.is_number value &&
value % 1 == 0 &&
value >= 0 &&
value <= 65535) in

30
doc/manual/syntax.md
View File

@ -120,7 +120,7 @@ Yes it is, indeed it is"
> let n = 5 in "The number %{n}."
error: Type error
> let n = 5 in "The number %{string.from_num n}."
> let n = 5 in "The number %{string.from_number n}."
"The number 5."
```
@ -473,17 +473,17 @@ information on typing in the [relevant document](./typing.md).
Examples:
```nickel
5 : Num
"Hello" : Str
5 : Number
"Hello" : String
(fun a b => a + b) : Num -> Num -> Num
let add : Num -> Num -> Num = fun a b => a + b
(fun a b => a + b) : Number -> Number -> Number
let add : Number -> Number -> Number = fun a b => a + b
{a: Num = 1, b: Bool = true, c : Array Num = [ 1 ]}
let r : {a : Num, b : Bool, c : Array Num} = { a = 1, b = true, c = [ 1 ] }
{a: Number = 1, b: Bool = true, c : Array Number = [ 1 ]}
let r : {a : Number, b : Bool, c : Array Number} = { a = 1, b = true, c = [ 1 ] }
{ a = 1, b = 2 } : { _ : Num }
let r : { _ : Num } = { a = 1, b = 2 }
{ a = 1, b = 2 } : { _ : Number }
let r : { _ : Number } = { a = 1, b = 2 }
```
## Metadata
@ -495,23 +495,23 @@ with the syntax `<value> | <metadata>`. Multiple metadata can be chained.
Examples:
```text
> 5 | Num
> 5 | Number
5
> 5 | Bool
error: Blame error: contract broken by a value.
> let SmallNum = contract.from_predicate (fun x => x < 5) in
> let SmallNumber = contract.from_predicate (fun x => x < 5) in
1 | SmallNum
1
> let SmallNum = contract.from_predicate (fun x => x < 5) in
> let SmallNumber = contract.from_predicate (fun x => x < 5) in
10 | SmallNum
error: Blame error: contract broken by a value.
> let SmallNum = contract.from_predicate (fun x => x < 5) in
let NotTooSmallNum = contract.from_predicate (fun x => x >= 2) in
3 | Num
> let SmallNumber = contract.from_predicate (fun x => x < 5) in
let NotTooSmallNumber = contract.from_predicate (fun x => x >= 2) in
3 | Number
| SmallNum
| NotTooSmallNum
3

16
doc/manual/tuto.md
View File

@ -34,11 +34,11 @@ We can spot fields such as `name`, `ssh-keys`, `is-admin` or
the shape of this data, we need to think about the type needed for
each attribute.
For example, the field `name` is a string, which translates to `Str`
For example, the field `name` is a string, which translates to `String`
in Nickel. Meanwhile, `ssh-keys` must allow multiple keys, so this is a
list of strings, written as `Array Str` in Nickel. The field `is-admin`
list of strings, written as `Array String` in Nickel. The field `is-admin`
is a boolean, written as `Bool`. Finally, `extra-groups` is a list of
group names, so we need `Array Str`, the same type used for `ssh-keys`.
group names, so we need `Array String`, the same type used for `ssh-keys`.
We can also mark fields as `optional` so you won't have to explicitly
write them if they don't have any value. In the example,`extra-groups`
@ -65,15 +65,15 @@ but it will allow you to validate your input data
{
UserSchema =
{
name | Str,
name | String,
ssh-keys
| Array Str
| Array String
| optional,
is-admin
| Bool
| default = false,
extra-groups
| Array Str
| Array String
| optional,
},
}
@ -175,7 +175,7 @@ error: missing definition for `name`
note:
┌─ /tmp/example/users-contract.ncl:5:12
│
5 │ name | Str,
5 │ name | String,
│ ^^^ bound here
```
@ -184,5 +184,5 @@ the attribute `name` has no value while it should have one. This is to
be expected as we removed it earlier.
The second part shows the contract attribute that produced the error.
In this case it's showing that `name` should be a `Str`, and as there
In this case it's showing that `name` should be a `String`, and as there
is no `optional` keyword, this attribute must be set.

10
doc/manual/types-vs-contracts.md
View File

@ -31,7 +31,7 @@ What to do depends on the context:
local to a file, if your function is bound to a variable, it can be
potentially reused in different places.
Example: `let append_tm: Str -> Str = fun s => s ++ "(TM)" in ...`
Example: `let append_tm: String -> String = fun s => s ++ "(TM)" in ...`
- *Let-bound function inside a typed block: nothing or type annotation*. Inside a
typed block, types are inferred, so it is OK for simple functions to not be
annotated. However, you are required to annotate it if it is polymorphic,
@ -42,13 +42,13 @@ What to do depends on the context:
Example:
```nickel
let foo : Num =
let foo : Number =
let addTwo = fun x => x + 2 in
addTwo 4
in ...
let foo : Num =
let ev : ((Num -> Num) -> Num) -> Num -> Num
let foo : Number =
let ev : ((Number -> Number) -> Number) -> Number -> Number
= fun f x => f (function.const x) in
ev (fun f => f 0) 1
in ...
@ -64,7 +64,7 @@ Example:
```nickel
let Schema = {
name | Str
name | String
| doc "Name of the package",
version | PkgVersion
| doc "The semantic version of the package",

128
doc/manual/typing.md
View File

@ -18,8 +18,8 @@ By default, Nickel code is dynamically typed. For example:
name = "hello",
version = "0.1.1",
fullname =
if builtin.is_num version then
"hello-v%{string.from_num version}"
if builtin.is_number version then
"hello-v%{string.from_number version}"
else
"hello-%{version}",
}
@ -34,8 +34,8 @@ example:
name = "hello",
version = "0.1.1",
fullname =
if builtin.is_num version then
"hello-v%{string.from_num version}"
if builtin.is_number version then
"hello-v%{string.from_number version}"
else
"hello-%{version + 1}",
}
@ -52,7 +52,7 @@ error: Type error
│ ------- evaluated to this
·
8 │ "hello-%{version + 1}",
│ ^^^^^^^ This expression has type Str, but Num was expected
│ ^^^^^^^ This expression has type String, but Number was expected
│
= +, 1st argument
@ -74,7 +74,7 @@ error: Type error
┌─ repl-input-11:2:32
│
2 │ array.fold_left (fun acc x => if pred x then acc @ [x] else acc) [] l in
│ ^^^^^^ This expression has type Num, but Bool was expected
│ ^^^^^^ This expression has type Number, but Bool was expected
3 │ filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]
│ - evaluated to this
│
@ -106,15 +106,15 @@ Example:
```nickel
# Let binding
let f : Num -> Bool = fun x => x % 2 == 0 in
let f : Number -> Bool = fun x => x % 2 == 0 in
# Record field
let r = {
count : Num = 2354.45 * 4 + 100,
count : Number = 2354.45 * 4 + 100,
} in
# Inline
1 + ((if f 10 then 1 else 0) : Num)
1 + ((if f 10 then 1 else 0) : Number)
```
Let us try on the filter example. We want the call to be inside the statically
@ -124,7 +124,7 @@ a type annotation at the top-level:
```nickel
(let filter = fun pred l =>
array.fold_left (fun acc x => if pred x then acc @ [x] else acc) [] l in
filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]) : Array Num
filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]) : Array Number
```
Result:
@ -133,17 +133,17 @@ Result:
error: Incompatible types
┌─ repl-input-12:3:37
│
3 │ filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]) : Array Num
3 │ filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6]) : Array Number
│ ^ this expression
│
= The type of the expression was expected to be `Bool`
= The type of the expression was inferred to be `Num`
= The type of the expression was inferred to be `Number`
= These types are not compatible
```
This is already better! The error now points at the call site, and inside our
anonymous function, telling us it is expected to return a boolean instead of a
number. Notice how we just had to give the top-level annotation `Array Num`.
number. Notice how we just had to give the top-level annotation `Array Number`.
Nickel performs type inference, so that you don't have to write the type for
`filter`, the filtering function nor the array.
@ -162,8 +162,8 @@ Let us now have a quick tour of the type system. The basic types are:
- `Dyn`: the dynamic type. This is the type given to most expressions outside of
a typed block. A value of type `Dyn` can be pretty much anything.
- `Num`: the only number type. Currently implemented as a 64bits float.
- `Str`: a string, which must always be valid UTF8.
- `Number`: the only number type. Currently implemented as a 64bits float.
- `String`: a string, which must always be valid UTF8.
- `Bool`: a boolean, that is either `true` or `false`.
<!-- - `Lbl`: a contract label. You usually don't need to use it or worry about it,-->
<!-- it is more of an internal thing. -->
@ -175,8 +175,8 @@ The following type constructors are available:
Example:
```nickel
let x : Array (Array Num) = [[1,2], [3,4]] in
array.flatten x : Array Num
let x : Array (Array Number) = [[1,2], [3,4]] in
array.flatten x : Array Number
```
- **Record**: `{field1: T1, .., fieldn: Tn}`. A record whose field
@ -186,8 +186,8 @@ The following type constructors are available:
Example:
```nickel
let pair : {fst: Num, snd: Str} = {fst = 1, snd = "a"} in
pair.fst : Num
let pair : {fst: Number, snd: String} = {fst = 1, snd = "a"} in
pair.fst : Number
```
- **Dictionary**: `{_: T}`. A record whose field
@ -197,8 +197,8 @@ The following type constructors are available:
Example:
```nickel
let occurrences : {_: Num} = {a = 1, b = 3, c = 0} in
record.map (fun char count => count + 1) occurrences : {_ : Num}
let occurrences : {_: Number} = {a = 1, b = 3, c = 0} in
record.map (fun char count => count + 1) occurrences : {_ : Number}
```
- **Enum**: ``[| `tag1, .., `tagn |]``: an enumeration comprised of alternatives
@ -215,7 +215,7 @@ The following type constructors are available:
`http => 1,
`ftp => 2,
`sftp => 3
}) : Num
}) : Number
```
- **Arrow (function)**: `S -> T`. A function taking arguments of type `S` and
@ -226,8 +226,8 @@ The following type constructors are available:
```nickel
{
incr : Num -> Num = fun x => x + 1,
mkPath : Str -> Str -> Str -> Str = fun basepath filename ext =>
incr : Number -> Number = fun x => x + 1,
mkPath : String -> String -> String -> String = fun basepath filename ext =>
"%{basepath}/%{filename}.%{ext}",
}
```
@ -259,8 +259,8 @@ well:
```nickel
{
foo : Array Str = filter (fun s => string.length s > 2) ["a","ab","abcd"],
bar : Array Num = filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6],
foo : Array String = filter (fun s => string.length s > 2) ["a","ab","abcd"],
bar : Array Number = filter (fun x => if x % 2 == 0 then x else null) [1,2,3,4,5,6],
}
```
@ -269,7 +269,7 @@ You can use as many parameters as you need:
```nickel
let fst : forall a b. a -> b -> a = fun x y => x in
let snd : forall a b. a -> b -> b = fun x y => y in
{ n = fst 1 "a", s = snd 1 "a" } : {n: Num, s: Str}
{ n = fst 1 "a", s = snd 1 "a" } : {n: Number, s: String}
```
Or even nest them:
@ -279,7 +279,7 @@ let higherRankId : forall a. (forall b. b -> b) -> a -> a
= fun id x => id x in
let id : forall a. a -> a
= fun x => x in
higherRankId id 0 : Num
higherRankId id 0 : Number
```
#### Type inference and polymorphism
@ -292,7 +292,7 @@ the typechecker surprisingly rejects our code:
(let filter = ... in
let result = filter (fun x => x % 2 == 0) [1,2,3,4,5,6] in
let dummy = filter (fun s => string.length s > 2) ["a","ab","abcd"] in
result) : Array Num
result) : Array Number
```
Result:
@ -304,15 +304,15 @@ error: Incompatible types
2 │ let dummy = filter (fun s => string.length s > 2) ["a","ab","abcd"] in
│ ^ this expression
│
= The type of the expression was expected to be `Str`
= The type of the expression was inferred to be `Num`
= The type of the expression was expected to be `String`
= The type of the expression was inferred to be `Number`
= These types are not compatible
```
The reason is that **without an explicit polymorphic annotation, the typechecker
will always infer non-polymorphic types**. If you need polymorphism, you have to
write a type annotation. Here, `filter` is inferred to be of type `(Num -> Bool)
-> Array Num -> Array Num`, guessed from the application in the right hand side of
write a type annotation. Here, `filter` is inferred to be of type `(Number -> Bool)
-> Array Number -> Array Number`, guessed from the application in the right hand side of
`result`.
**Note**:
@ -333,7 +333,7 @@ In a configuration language, you will often find yourself handling records of
various kinds. In a simple type system, you can hit the following issue:
```nickel
(let addTotal: {total: Num} -> {total: Num} -> Num
(let addTotal: {total: Number} -> {total: Number} -> Number
= fun r1 r2 => r1.total + r2.total in
let r1 = {jan = 200, feb = 300, march = 10, total = jan + feb} in
let r2 = {aug = 50, sept = 20, total = aug + sept} in
@ -341,7 +341,7 @@ let r3 = {may = 1300, june = 400, total = may + june} in
{
partial1 = addTotal r1 r2,
partial2 = addTotal r2 r3,
}) : {partial1: Num, partial2: Num}
}) : {partial1: Number, partial2: Number}
```
```text
@ -351,15 +351,15 @@ error: Type error: extra row `sept`
8 │ partial2 = addTotal r2 r3,
│ ^^ this expression
│
= The type of the expression was expected to be `{total: Num}`, which does not contain the field `sept`
= The type of the expression was inferred to be `{total: Num, sept: Num, aug: Num}`, which contains the extra field `sept`
= The type of the expression was expected to be `{total: Number}`, which does not contain the field `sept`
= The type of the expression was inferred to be `{total: Number, sept: Number, aug: Number}`, which contains the extra field `sept`
```
The problem here is that for this code to run fine, the requirement of
`addTotal` should be that both arguments have a field `total: Num`, but could
`addTotal` should be that both arguments have a field `total: Number`, but could
very well have other fields, for all we care. Unfortunately, we don't know right
now how to express this constraint. The current annotation is too restrictive,
because it imposes that arguments have exactly one field `total: Num`, and
because it imposes that arguments have exactly one field `total: Number`, and
nothing more.
To express such constraints, Nickel features *row polymorphism*. The idea is
@ -368,7 +368,7 @@ we can substitute a parameter for a whole sequence of field declarations, also
referred to as rows:
```nickel
(let addTotal: forall a b. {total: Num ; a} -> {total: Num ; b} -> Num
(let addTotal: forall a b. {total: Number ; a} -> {total: Number ; b} -> Number
= fun r1 r2 => r1.total + r2.total in
let r1 = {jan = 200, feb = 300, march = 10, total = jan + feb} in
let r2 = {aug = 50, sept = 20, total = aug + sept} in
@ -376,7 +376,7 @@ let r3 = {may = 1300, june = 400, total = may + june} in
{
partial1 = addTotal r1 r2,
partial2 = addTotal r2 r3,
}) : {partial1: Num, partial2: Num}
}) : {partial1: Number, partial2: Number}
```
Result:
@ -385,24 +385,24 @@ Result:
{partial1 = 570, partial2 = 1770}
```
In the type of `addTotal`, the part `{total: Num ; a}` expresses exactly what we
wanted: the argument must have a field `total: Num`, but the *tail* (the rest of
In the type of `addTotal`, the part `{total: Number ; a}` expresses exactly what we
wanted: the argument must have a field `total: Number`, but the *tail* (the rest of
the record type) is polymorphic, and `a` may be substituted for arbitrary fields
(such as `jan: Num, feb: Num`). We used two different generic parameters `a` and
(such as `jan: Number, feb: Number`). We used two different generic parameters `a` and
`b`, to express that the tails of the arguments may differ. If we used `a` in
both places, as in `forall a. {total: Num ; a} -> {total: Num ; a} -> Num`, we
both places, as in `forall a. {total: Number ; a} -> {total: Number ; a} -> Number`, we
could still write `addTotal {total = 1, foo = 1} {total = 2, foo = 2}` but not
`addTotal {total = 1, foo = 1} {total = 2, bar = 2}`. Using distinct parameters
`a` and `b` gives us maximum flexibility.
What comes before the tail may include several fields, is in e.g. `forall a.
{total: Num, subtotal: Num ; a} -> Num`.
{total: Number, subtotal: Number ; a} -> Number`.
Note that row polymorphism also works with enums, with the same intuition of a
tail that can be substituted for something else. For example:
```nickel
let port_of : forall a. [| `http, `ftp; a |] -> Num =
let port_of : forall a. [| `http, `ftp; a |] -> Number =
match {
`http => 80,
`ftp => 21,
@ -416,7 +416,7 @@ type.
### Take-away
The type system of Nickel has usual basic types (`Dyn`, `Num`, `Str`, and
The type system of Nickel has usual basic types (`Dyn`, `Number`, `String`, and
`Bool`) and type constructors for arrays, records and functions. Nickel
features generics via polymorphism, introduced by the `forall` keyword. A type
can not only be generic in other types, but records types can also be
@ -465,7 +465,7 @@ error: Blame error: contract broken by the caller.
│ - evaluated to this expression
│
= This error may happen in the following situation:
1. A function `f` is bound by a contract: e.g. `(Num -> Num) -> Num`.
1. A function `f` is bound by a contract: e.g. `(Number -> Number) -> Number`.
2. `f` takes another function `g` as an argument: e.g. `f = fun g => g 0`.
3. `f` is called by with an argument `g` that does not respect the contract: e.g. `f (fun x => false)`.
= Either change the contract accordingly, or call `f` with a function that returns a value of the right type.
@ -506,7 +506,7 @@ dynamically typed value inside a statically typed block directly:
```nickel
let x = 0 + 1 in
(1 + x : Num)
(1 + x : Number)
```
Result:
@ -515,10 +515,10 @@ Result:
error: Incompatible types
┌─ repl-input-6:1:6
│
1 │ (1 + x : Num)
1 │ (1 + x : Number)
│ ^ this expression
│
= The type of the expression was expected to be `Num`
= The type of the expression was expected to be `Number`
= The type of the expression was inferred to be `Dyn`
= These types are not compatible
```
@ -531,8 +531,8 @@ idioms. In this case, we can trade a type annotation for a contract application:
Example:
```nickel
let x | Num = if true then 0 else "a" in
(1 + x : Num)
let x | Number = if true then 0 else "a" in
(1 + x : Number)
```
Here, `x` is clearly always a number, but it is not well-typed (the `then` and
@ -549,14 +549,14 @@ typed block, a contract application can thus serve to embed dynamically typed
code that you know is correct but wouldn't typecheck:
```nickel
(1 + ((if true then 0 else "a" | Num)) : Num
(1 + ((if true then 0 else "a" | Number)) : Number
```
The code above is accepted, while a fully statically typed version is rejected
because of the type mismatch between the if branches:
```nickel
(1 + (if true then 0 else "a")) : Num
(1 + (if true then 0 else "a")) : Number
```
Result:
@ -565,11 +565,11 @@ Result:
error: Incompatible types
┌─ repl-input-46:1:27
│
1 │ (1 + (if true then 0 else "a")) : Num
1 │ (1 + (if true then 0 else "a")) : Number
│ ^^^ this expression
│
= The type of the expression was expected to be `Num`
= The type of the expression was inferred to be `Str`
= The type of the expression was expected to be `Number`
= The type of the expression was inferred to be `String`
= These types are not compatible
```
@ -579,7 +579,7 @@ accepted:
```nickel
let x = 1 in
(1 + x : Num)
(1 + x : Number)
```
The typechecker tries to respect the intent of the programmer. If one doesn't
@ -587,7 +587,7 @@ use annotations, then the code shouldn't be typechecked, whatever the reason is.
If you want `x` to be statically typed, you should annotate it.
That being said, the typechecker still avoids being too rigid: it is obvious in
the previous example case that `1` is of type `Num`. This information is cheap
the previous example case that `1` is of type `Number`. This information is cheap
to gather. When encountering a binding outside of a typed block, the typechecker
determines the *apparent type* of the definition. The rationale is that
determining the apparent type shouldn't recurse arbitrarily inside the
@ -627,7 +627,7 @@ annotation.
```nickel
let Port = contract.from_predicate (fun value =>
builtin.is_num value
builtin.is_number value
&& value % 1 == 0
&& value >= 0
&& value <= 65535) in
@ -647,7 +647,7 @@ error: Incompatible types
│ ^^ this expression
│
= The type of the expression was expected to be `Port`
= The type of the expression was inferred to be `Num`
= The type of the expression was inferred to be `Number`
= These types are not compatible
```
@ -670,7 +670,7 @@ A custom contract hence acts like an opaque type (sometimes called abstract type
as well) for the typechecker. The typechecker doesn't really know much about it
except that the only way to construct a value of type `Port` is to use contract
application. You also need an explicit contract application to cast back a
`Port` to a `Num`: `(p | Num) + 1 : Num`.
`Port` to a `Number`: `(p | Number) + 1 : Number`.
Because of the rigidity of opaque types, using custom contracts inside static
type annotations is not very useful right now. We just had to give them a

8
examples/config-gcc/config-gcc.ncl
View File

@ -6,7 +6,7 @@ let GccFlag =
# We only allow the following flags
let available = ["W", "c", "S", "e", "o"] in
fun label value =>
if builtin.is_str value then
if builtin.is_string value then
if string.length value > 0 &&
array.any (fun x => x == string.substring 0 1 value) available then
value
@ -29,7 +29,7 @@ let GccFlag =
let Path =
let pattern = m%"^(.+)/([^/]+)$"% in
fun label value =>
if builtin.is_str value then
if builtin.is_string value then
if string.is_match pattern value then
value
else
@ -38,7 +38,7 @@ let Path =
contract.blame_with_message "not a string" label in
let SharedObjectFile = fun label value =>
if builtin.is_str value then
if builtin.is_string value then
if string.is_match m%"\.so$"% value then
value
else
@ -60,7 +60,7 @@ let Contract = {
flags | doc "
Additional flags to pass to GCC. Either provide a string without the
leading `-`, or a structured value `{flag : Str, arg: Str}`.
leading `-`, or a structured value `{flag : String, arg: String}`.
"
| Array GccFlag
| default = [],

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

@ -7,7 +7,7 @@
let Port
| doc "A contract for a port number"
= contract.from_predicate (fun value =>
builtin.is_num value &&
builtin.is_number value &&
value % 1 == 0 &&
value >= 0 &&
value <= 65535) in
@ -15,13 +15,13 @@ let Port
let PortElt
| doc "A contract for a port element of a Kubernetes configuration"
= {
name | Str,
name | String,
containerPort | Port,
} in
let Container = {
name | Str,
image | Str,
name | String,
image | String,
ports | Array PortElt,
} in
@ -30,22 +30,22 @@ let KubernetesConfig = {
| doc "The kind of the element being configured."
| default = `Pod,
apiVersion | Str,
apiVersion | String,
metadata = {
name | Str,
labels.app | Str,
name | String,
labels.app | String,
},
spec = {
replicas | num.PosNat
replicas | number.PosNat
| doc "The number of replicas"
| default = 1,
selector.matchLabels.app | Str,
selector.matchLabels.app | String,
template = {
metadata.labels.app | Str,
metadata.labels.app | String,
spec.containers | Array Container,
},
},

4
examples/simple-contracts/simple-contract-div.ncl
View File

@ -3,12 +3,12 @@
# /!\ THIS EXAMPLE IS EXPECTED TO FAIL
# Illustrates a basic contract violation.
let Even = fun label value =>
if builtin.is_num value && value % 2 == 0 then
if builtin.is_number value && value % 2 == 0 then
value
else
contract.blame label in
let DivBy3 = fun label value =>
if builtin.is_num value && value % 3 == 0 then
if builtin.is_number value && value % 3 == 0 then
value
else
contract.blame label in

2
lsp/nls/src/requests/completion.rs
View File

@ -824,7 +824,7 @@ mod tests {
use std::convert::TryInto;
// Representing the type: {a: {b : {c1 : Num, c2: Num}}}
let c_record_type = mk_uty_record!(("c1", TypeF::Num), ("c2", TypeF::Num));
let c_record_type = mk_uty_record!(("c1", TypeF::Number), ("c2", TypeF::Number));
let b_record_type = mk_uty_record!(("b", c_record_type));
let a_record_type = mk_uty_row!(("a", b_record_type));

14
notes/standardization-meeting-07.12.21.md
View File

@ -80,7 +80,7 @@ Current syntax: `nickel let f = fun x y z => body in`
**In-meeting notes**
`fun` is fine. In favor of second Ocaml-style function definition `let f x y z =
...`. What about partial annotations (what is the semantics of `f (x :
Num) y z =` outside of a typed block) ? The problem is already there with or
Number) y z =` outside of a typed block) ? The problem is already there with or
without the OCaml-style function definitions. We should also have an Haskell-style annotation "by pieces" consistent with the let-block syntax:
```nickel
@ -106,7 +106,7 @@ are substituted for `Dyn`.
- typing libraries:
```nickel
{
bar : Num -> Num = fun x => x + 1,
bar : Number -> Number = fun x => x + 1,
foo : forall a. a -> -a = fun x => x,
} : _
```
@ -169,9 +169,9 @@ But it introduces dynamic scoping, which is bad.
- add it nevertheless
- force the definition of an interface:
```nickel
{foo = bar + 1, bar | Num} & {bar}
{foo = bar + 1, bar | Number} & {bar}
// For more complex/dynamic interfaces
let Interface = {bar | Num} in
let Interface = {bar | Number} in
{foo = bar + 1, ..Interface}
```
@ -181,7 +181,7 @@ interfaces in one way or another. We can also already currently put the merged
content in a subfield as in:
```nickel
let Interface = {bar | Num} in
let Interface = {bar | Number} in
{foo = params.bar + 1, params | #Interface}
```
@ -189,7 +189,7 @@ Later, if mandated by e.g. NixOS modules, we could add the `..Interface` syntax
to "inline" one record inside the other:
```nickel
let Interface = {bar | Num} in
let Interface = {bar | Number} in
{foo = bar + 1, ..Interface}
```
@ -224,7 +224,7 @@ open_contract(#(open_contract(T))) = open_contract(T)
else contract label value in
//cannot do
foo | #Nullable (Num -> Num)
foo | #Nullable (Number -> Number)
```
- `#` is verbose: should we remove it? But in current situation, it is nice to
embed value syntax in the type syntax as in

2
notes/sum-as-dependent-records.md
View File

@ -15,7 +15,7 @@ For this, we'd need to implement two new kind of contracts:
Ideas/problems around this:
* We may be good enough with a Pi indexed only by simple types (Bool, Num, enums), I think this would simplify some of the concerns regarding strictness. Dually, some similar restriction might be helpful for Sigma. If we also drop Num, type checking might become much easier.
* We may be good enough with a Pi indexed only by simple types (Bool, Number, enums), I think this would simplify some of the concerns regarding strictness. Dually, some similar restriction might be helpful for Sigma. If we also drop Number, type checking might become much easier.
* Maybe we can get rid of Sigma, and construct them with `Pi b: Bool, (if b then A else B) -> (Pi c: Bool, if c then Bool else if b then A else B)`, where `c` is the accessor for the pair (`true == fst`, `false == snd`).
* A big question is what to do with type checking for these types.
* [4] talks about some problems with dependent function contracts, I'll try to understand in more detail what they're saying and check whether it makes any difference for us.

4
notes/typechecking.md
View File

@ -31,7 +31,7 @@ Whenever we want to tell the compiler, trust me here, we use `Assume(Type, Term)
Our types A, B can be variables (s, t, ...) (_unused_), base types (Num, Bool, Dyn) function types (A -> B) or flat types (#e), a contract used as a type.
Our types A, B can be variables (s, t, ...) (_unused_), base types (Number, Bool, Dyn) function types (A -> B) or flat types (#e), a contract used as a type.
Our expressions (e, f, ...) can be variables (x, y, ...), non recursive lets (let x = e in f), lambdas (fun x => e), application (e f), constants (true, false, 1, 2, ...), primitive operations (ite, isZero, isNum, isBool, isFun, blame, +, ...), promises (Promise(A, e)) and assumes (Assume(A, e)).
@ -65,7 +65,7 @@ G, x: A |s- f: B G |s- e: C unify(s, A, C) unify(s, B, D)
G |s- e f: C
----------------- ----------------
G |s- t/f: Bool G |s- n: Num
G |s- t/f: Bool G |s- n: Number
Operations as expected....

38
spec/type-system/notes/examples.md
View File

@ -13,7 +13,7 @@ case, we compute the max of the lower bounds or fail.
```nickel
f : forall a. a -> a -> a
x : {foo : {bar: Num}, bar: {baz2: Dyn}}
x : {foo : {bar: Number}, bar: {baz2: Dyn}}
y : {_: {_: Dyn}}
f x y
@ -21,7 +21,7 @@ f x y
# constraints
e: ?a
a: ?a
?a >: {foo : {baz: Num}, bar: {baz2: Dyn}}
?a >: {foo : {baz: Number}, bar: {baz2: Dyn}}
?a >: {_ : {_ : Dyn}}
# expected
@ -39,18 +39,18 @@ Q: what is the rule for `if-then-else` ?
```nickel
fun x =>
if builtin.is_num x then x + 1 else x
if builtin.is_number x then x + 1 else x
e: ?a -> ?b
x: ?a
?a <: Dyn
?a <: Num
?a <: Number
?b >: ?a
?b >: Num
?b >: Number
# expected
works
x: Num
x: Number
```
### incompatible if
@ -61,13 +61,13 @@ fun x =>
e: ?a -> ?b
x: ?a
?a <: Num
?a <: Number
?a <: Bool
?b >: Num
?b >: Number
# expected
fails
Num <> Bool
Number <> Bool
```
### record.insert with subtyping
@ -84,7 +84,7 @@ x: ?x
?a2 snd instantiation of record.insert
# fst call gives
Num <: ?a1
Number <: ?a1
?x <: {_: ?a1}
# snd call gives
@ -100,30 +100,30 @@ Dyn <: ?a2 => a2 := Dyn
?x1 <: Dyn
# state
Num <: ?a1
Number <: ?a1
?x1 <: ?a1
?x1 <: Dyn
# what do we do? unify? what if ?x1 <: ?a3 ?
# Or we do ?a1 >: max (Num, ?x1), setting ?x1 to Num
# Or we do ?a1 >: max (Number, ?x1), setting ?x1 to Number
# ... ?
# Would it be possible to have ?x1 <: ?a1, ?x2 <: ?a2, ?a1 <: Num, ?a2 <: Dyn
# Would it be possible to have ?x1 <: ?a1, ?x2 <: ?a2, ?a1 <: Number, ?a2 <: Dyn
# plus other bounds preventing from doing substitution?
# expected
works
{_: Num} -> {_: Dyn}
{_: Number} -> {_: Dyn}
```
Questions on this: what constraint do we pick? Do max of lower bound should
always provoke unification, like `max ?a Num`?
always provoke unification, like `max ?a Number`?
### record.insert with subtyping and multiple variables
```nickel
fun x =>
let var = "foo" ++ "bar" in
let f = fun u => builtin.is_num u."%{var}" in
let f = fun u => builtin.is_number u."%{var}" in
let y : Dyn = null in
let _ign = record.insert 1 "foo" x in
let _ign2 = f x in
@ -138,7 +138,7 @@ x: ?x
?a2 snd instantiation of record.insert
# fst call gives
Num <: ?a1
Number <: ?a1
?x <: {_: ?a1}
# snd call gives
@ -162,7 +162,7 @@ Dyn <: ?a2 => a2 := Dyn
?x1 <: Dyn
# state
Num <: ?a1
Number <: ?a1
?x1 <: ?a1
?x1 <: Dyn
?x1 <: ?u1
@ -171,7 +171,7 @@ Num <: ?a1
# expected
works
{_: Num} -> {_: Dyn}
{_: Number} -> {_: Dyn}
```
## Both lower and upper bounds

6
src/deserialize.rs
View File

@ -22,7 +22,7 @@ macro_rules! deserialize_number {
match unwrap_term(self)? {
Term::Num(n) => visitor.$visit(n as $type),
other => Err(RustDeserializationError::InvalidType {
expected: "Num".to_string(),
expected: "Number".to_string(),
occurred: RichTerm::from(other).to_string(),
}),
}
@ -39,7 +39,7 @@ macro_rules! deserialize_number_round {
match unwrap_term(self)? {
Term::Num(n) => visitor.$visit(n.round() as $type),
other => Err(RustDeserializationError::InvalidType {
expected: "Num".to_string(),
expected: "Number".to_string(),
occurred: RichTerm::from(other).to_string(),
}),
}
@ -708,7 +708,7 @@ mod tests {
assert_eq!(
A::deserialize(
TestProgram::new_from_source(
Cursor::new(br#"{ a = (10 | Num) }"#.to_vec()),
Cursor::new(br#"{ a = (10 | Number) }"#.to_vec()),
"source"
)
.expect("program shouldn't fail")

8
src/error.rs
View File

@ -1195,7 +1195,7 @@ mod blame_error {
String::from(
"This error may happen in the following situation:
1. A function `f` is bound by a contract: e.g. `Bool -> Num`.
2. `f` returns a value of the wrong type: e.g. `f = fun c => \"string\"` while `Num` is expected.",
2. `f` returns a value of the wrong type: e.g. `f = fun c => \"string\"` while `Number` is expected.",
),
String::from(
"Either change the contract accordingly, or change the return value of `f`",
@ -1231,8 +1231,8 @@ mod blame_error {
1. A function `f` is bound by a contract: e.g. `((Num -> Num) -> Num) -> Num)`.
2. `f` take another function `g` as an argument: e.g. `f = fun g => g (fun x => true)`.
3. `g` itself takes a function as an argument.
4. `f` passes a function that does not respect the contract to `g`: e.g. `g (fun x => true)` (expected to be of type `Num -> Num`)."),
String::from("Either change the contract accordingly, or call `g` with a function that returns a value of type `Num`."),
4. `f` passes a function that does not respect the contract to `g`: e.g. `g (fun x => true)` (expected to be of type `Number -> Number`)."),
String::from("Either change the contract accordingly, or call `g` with a function that returns a value of type `Number`."),
end_note,
],
)
@ -1245,7 +1245,7 @@ mod blame_error {
String::from("expected type of the argument provided by the caller"),
vec![
String::from("This error may happen in the following situation:
1. A function `f` is bound by a contract: e.g. `Num -> Num`.
1. A function `f` is bound by a contract: e.g. `Number -> Number`.
2. `f` is called with an argument of the wrong type: e.g. `f false`."),
String::from("Either change the contract accordingly, or call `f` with an argument of the right type."),
end_note,

4
src/eval/fixpoint.rs
View File

@ -153,8 +153,8 @@ pub fn patch_field<C: Cache>(
//
// ```
// let Variant = match {
// `num => Num,
// `str => Str,
// `num => Number,
// `str => String,
// `any => Dyn,
// } in
//

10
src/eval/operation.rs
View File

@ -43,7 +43,7 @@ generate_counter!(FreshVariableCounter, usize);
/// Result of the equality of two terms.
///
/// The equality of two terms can either be computed directly for base types (`Num`, `Str`, etc.),
/// The equality of two terms can either be computed directly for base types (`Number`, `String`, etc.),
/// in which case `Bool` is returned. Otherwise, composite values such as arrays or records generate
/// new subequalities, as represented by the last variant as a vector of pairs of terms. This list
/// should be non-empty (it if was empty, `eq` should have returned `Bool(true)` directly). The
@ -193,14 +193,14 @@ impl<R: ImportResolver, C: Cache> VirtualMachine<R, C> {
}
UnaryOp::Typeof() => {
let result = match *t {
Term::Num(_) => "Num",
Term::Num(_) => "Number",
Term::Bool(_) => "Bool",
Term::Str(_) => "Str",
Term::Str(_) => "String",
Term::Enum(_) => "Enum",
Term::Fun(..) | Term::Match { .. } => "Fun",
Term::Fun(..) | Term::Match { .. } => "Function",
Term::Array(..) => "Array",
Term::Record(..) | Term::RecRecord(..) => "Record",
Term::Lbl(..) => "Lbl",
Term::Lbl(..) => "Label",
_ => "Other",
};
Ok(Closure::atomic_closure(RichTerm::new(

4
src/eval/tests.rs
View File

@ -92,7 +92,7 @@ fn simple_plus() {
#[test]
fn asking_for_various_types() {
let num = mk_term::op1(UnaryOp::Typeof(), Term::Num(45.3));
assert_eq!(Ok(Term::Enum("Num".into())), eval_no_import(num));
assert_eq!(Ok(Term::Enum("Number".into())), eval_no_import(num));
let boolean = mk_term::op1(UnaryOp::Typeof(), Term::Bool(true));
assert_eq!(Ok(Term::Enum("Bool".into())), eval_no_import(boolean));
@ -101,7 +101,7 @@ fn asking_for_various_types() {
UnaryOp::Typeof(),
mk_fun!("x", mk_app!(mk_term::var("x"), mk_term::var("x"))),
);
assert_eq!(Ok(Term::Enum("Fun".into())), eval_no_import(lambda));
assert_eq!(Ok(Term::Enum("Function".into())), eval_no_import(lambda));
}
#[test]

43
src/label.rs
View File

@ -19,19 +19,19 @@ pub mod ty_path {
//! Checking higher-order contracts can involve a good share of intermediate contract checking.
//! Take the following example:
//! ```text
//! Assume((Num -> Num) -> Num) -> Num -> Num, fun ev => fun cst => ev (fun x => cst))
//! Assume((Number -> Number) -> Number) -> Number -> Number, fun ev => fun cst => ev (fun x => cst))
//! ```
//! Once called, various checks will be performed on the arguments of functions and their return
//! values:
//! 1. Check that `ev` provides a `Num` to `(fun x => cst)`
//! 2. Check that `(fun x => cst)` returns a `Num`
//! 3. Check that `ev (fun x => cst)` return a `Num`
//! 1. Check that `ev` provides a `Number` to `(fun x => cst)`
//! 2. Check that `(fun x => cst)` returns a `Number`
//! 3. Check that `ev (fun x => cst)` return a `Number`
//! 4. etc.
//!
//! Each check can be linked to a base type occurrence (here, a `Num`) in the original type:
//! Each check can be linked to a base type occurrence (here, a `Number`) in the original type:
//! ```text
//! (Num -> Num) -> Num) -> Num -> Num
//! ^^^1 ^^^2 ^^^3 etc.
//! (Number -> Number) -> Number) -> Number -> Number
//! ^^^^^1 ^^^^^^2 ^^^^^^3 etc.
//! ```
//!
//! This is the information encoded by a type path: what part of the original type is currently
@ -318,31 +318,32 @@ but this field doesn't exist in {}",
/// are types with arrows in it. Consider the simplest example:
///
/// ```text
/// f | Num -> Num
/// f | Number -> Number
/// ```
///
/// This does not entail that `f` returns a `Num` in *every* situation. The identity function `id
/// = fun x => x` can certainly be given the type `Num -> Num`, but `id "a" = "a"` is not a `Num`.
/// This does not entail that `f` returns a `Number` in *every* situation. The identity function
/// `id = fun x => x` can certainly be given the type `Number -> Number`, but `id "a" = "a"` is not
/// a `Number`.
///
/// To satisfy the contract `Num -> Num` for `f` is to satisfy the predicate "if you give me a
/// `Num` as an argument, I give you a `Num` as a result". There is an additional contract to be
/// checked, which is not the responsibility of `f`, but the caller's (or context)
/// one.
/// To satisfy the contract `Number -> Number` for `f` is to satisfy the predicate "if you give me
/// a `Number` as an argument, I give you a `Number` as a result". There is an additional contract
/// to be checked, which is not the responsibility of `f`, but the caller's (or context) one.
///
/// `f | Num -> Num` should thus be evaluated as `fun arg => ((f (arg | Num)) | Num)`, but we want
/// to report the failures of the two introduced subcontracts in a different way:
/// `f | Number -> Number` should thus be evaluated as `fun arg => ((f (arg | Number)) | Number)`,
/// but we want to report the failures of the two introduced subcontracts in a different way:
///
/// - The inner one (on the argument) says that `f` has been misused: it has been applied to
/// something that is not a `Num`.
/// something that is not a `Number`.
/// - The outer one says that `f` failed to satisfy its contract, as it has been provided with a
/// `Num` (otherwise the inner contracts would have failed before) but failed to deliver a `Num`.
/// `Number` (otherwise the inner contracts would have failed before) but failed to deliver a
/// `Number`.
///
/// This duality caller/callee or function/context is indicated by the polarity: the outer
/// corresponds to a *positive* polarity (the contract is on the term), while the inner corresponds
/// to a *negative* one (the contact is on the context). The polarity always starts as `true` in
/// user-written contracts, but is toggled in the argument contract when the interpreter decomposes
/// an higher order-contract. This also generalizes to higher types such as `((Num -> Num) -> Num)
/// -> Num` where the polarity alternates each time.
/// an higher order-contract. This also generalizes to higher types such as `((Number -> Number) ->
/// Number) -> Number` where the polarity alternates each time.
#[derive(Debug, Clone, PartialEq)]
pub struct Label {
/// The type checked by the original contract.
@ -411,7 +412,7 @@ impl Label {
/// Generate a dummy label for testing purpose.
pub fn dummy() -> Label {
Label {
types: Rc::new(Types::from(TypeF::Num)),
types: Rc::new(Types::from(TypeF::Number)),
diagnostics: vec![ContractDiagnostic::new().with_message(String::from("testing"))],
span: RawSpan {
src_id: Files::new().add("<test>", String::from("empty")),

8
src/parser/grammar.lalrpop
View File

@ -870,9 +870,9 @@ NOpPre<ArgRule>: UniTerm = {
TypeBuiltin: Types = {
"Dyn" => Types::from(TypeF::Dyn),
"Num" => Types::from(TypeF::Num),
"Number" => Types::from(TypeF::Number),
"Bool" => Types::from(TypeF::Bool),
"Str" => Types::from(TypeF::Str),
"String" => Types::from(TypeF::String),
}
TypeAtom: Types = {
@ -979,9 +979,9 @@ extern {
"symbolic string start" => Token::Normal(NormalToken::SymbolicStringStart(
SymbolicStringStart{prefix: <&'input str>, length: <usize>})),
"Num" => Token::Normal(NormalToken::Num),
"Number" => Token::Normal(NormalToken::Number),
"Dyn" => Token::Normal(NormalToken::Dyn),
"Str" => Token::Normal(NormalToken::Str),
"String" => Token::Normal(NormalToken::String),
"Bool" => Token::Normal(NormalToken::Bool),
"Array" => Token::Normal(NormalToken::Array),

8
src/parser/lexer.rs
View File

@ -77,12 +77,12 @@ pub enum NormalToken<'input> {
#[token("Dyn")]
Dyn,
#[token("Num")]
Num,
#[token("Number")]
Number,
#[token("Bool")]
Bool,
#[token("Str")]
Str,
#[token("String")]
String,
#[token("Array")]
Array,

6
src/parser/uniterm.rs
View File

@ -515,10 +515,10 @@ impl FixTypeVars for Types {
) -> Result<(), ParseError> {
match self.types {
TypeF::Dyn
| TypeF::Num
| TypeF::Number
| TypeF::Bool
| TypeF::Str
| TypeF::Sym
| TypeF::String
| TypeF::Symbol
| TypeF::Flat(_)
| TypeF::Wildcard(_) => Ok(()),
TypeF::Arrow(ref mut s, ref mut t) => {

6
src/pretty.rs
View File

@ -798,9 +798,9 @@ where
use TypeF::*;
match self.types {
Dyn => allocator.text("Dyn"),
Num => allocator.text("Num"),
Number => allocator.text("Number"),
Bool => allocator.text("Bool"),
Str => allocator.text("Str"),
String => allocator.text("String"),
Array(ty) => allocator
.text("Array")
.group()
@ -810,7 +810,7 @@ where
} else {
ty.pretty(allocator).nest(2).parens()
}),
Sym => allocator.text("Sym"),
Symbol => allocator.text("Symbol"),
Flat(t) => t.pretty(allocator),
Var(var) => allocator.as_string(var),
Forall { var, ref body, .. } => {

12
src/stdlib.rs
View File

@ -12,7 +12,7 @@ pub fn modules() -> [StdlibModule; 8] {
StdlibModule::Array,
StdlibModule::Record,
StdlibModule::String,
StdlibModule::Num,
StdlibModule::Number,
StdlibModule::Function,
StdlibModule::Internals,
]
@ -26,7 +26,7 @@ pub enum StdlibModule {
Array,
Record,
String,
Num,
Number,
Function,
Internals,
}
@ -39,7 +39,7 @@ impl StdlibModule {
StdlibModule::Array => "<stdlib/array.ncl>",
StdlibModule::Record => "<stdlib/record.ncl>",
StdlibModule::String => "<stdlib/string.ncl>",
StdlibModule::Num => "<stdlib/num.ncl>",
StdlibModule::Number => "<stdlib/number.ncl>",
StdlibModule::Function => "<stdlib/function.ncl>",
StdlibModule::Internals => "<stdlib/internals.ncl>",
}
@ -52,7 +52,7 @@ impl StdlibModule {
StdlibModule::Array => include_str!("../stdlib/array.ncl"),
StdlibModule::Record => include_str!("../stdlib/record.ncl"),
StdlibModule::String => include_str!("../stdlib/string.ncl"),
StdlibModule::Num => include_str!("../stdlib/num.ncl"),
StdlibModule::Number => include_str!("../stdlib/number.ncl"),
StdlibModule::Function => include_str!("../stdlib/function.ncl"),
StdlibModule::Internals => include_str!("../stdlib/internals.ncl"),
}
@ -71,7 +71,7 @@ impl TryFrom<Ident> for StdlibModule {
"array" => StdlibModule::Array,
"record" => StdlibModule::Record,
"string" => StdlibModule::String,
"num" => StdlibModule::Num,
"num" => StdlibModule::Number,
"function" => StdlibModule::Function,
"internals" => StdlibModule::Internals,
_ => return Err(UnknownStdlibModule),
@ -88,7 +88,7 @@ impl From<StdlibModule> for Ident {
StdlibModule::Array => "array",
StdlibModule::Record => "record",
StdlibModule::String => "string",
StdlibModule::Num => "num",
StdlibModule::Number => "num",
StdlibModule::Function => "function",
StdlibModule::Internals => "internals",
};

2
src/term/mod.rs
View File

@ -1978,7 +1978,7 @@ mod tests {
let inner = TypeAnnotation {
types: Some(LabeledType {
types: Types::from(TypeF::Num),
types: Types::from(TypeF::Number),
label: Label::dummy(),
}),
..Default::default()

6
src/transform/free_vars.rs
View File

@ -180,10 +180,10 @@ impl CollectFreeVars for Types {
fn collect_free_vars(&mut self, set: &mut HashSet<Ident>) {
match &mut self.types {
TypeF::Dyn
| TypeF::Num
| TypeF::Number
| TypeF::Bool
| TypeF::Str
| TypeF::Sym
| TypeF::String
| TypeF::Symbol
| TypeF::Var(_)
| TypeF::Wildcard(_) => (),
TypeF::Forall { body: ty, .. } | TypeF::Dict(ty) | TypeF::Array(ty) => {

6
src/typecheck/eq.rs
View File

@ -441,10 +441,10 @@ fn type_eq_bounded<E: TermEnvironment>(
(GenericUnifType::Concrete(s1), GenericUnifType::Concrete(s2)) => match (s1, s2) {
(TypeF::Wildcard(id1), TypeF::Wildcard(id2)) => id1 == id2,
(TypeF::Dyn, TypeF::Dyn)
| (TypeF::Num, TypeF::Num)
| (TypeF::Number, TypeF::Number)
| (TypeF::Bool, TypeF::Bool)
| (TypeF::Sym, TypeF::Sym)
| (TypeF::Str, TypeF::Str) => true,
| (TypeF::Symbol, TypeF::Symbol)
| (TypeF::String, TypeF::String) => true,
(TypeF::Dict(uty1), TypeF::Dict(uty2)) | (TypeF::Array(uty1), TypeF::Array(uty2)) => {
type_eq_bounded(state, uty1, env1, uty2, env2)
}

6
src/typecheck/mk_uniftype.rs
View File

@ -110,7 +110,7 @@ where
// dyn is a reserved keyword
generate_builder!(dynamic, Dyn);
generate_builder!(str, Str);
generate_builder!(num, Num);
generate_builder!(str, String);
generate_builder!(num, Number);
generate_builder!(bool, Bool);
generate_builder!(sym, Sym);
generate_builder!(sym, Symbol);

32
src/typecheck/mod.rs
View File

@ -123,7 +123,7 @@ pub enum UnifEnumRows {
/// representation, hence the parametrization.
#[derive(Clone, PartialEq, Debug)]
pub enum GenericUnifType<E: TermEnvironment> {
/// A concrete type (like `Num` or `Str -> Str`).
/// A concrete type (like `Number` or `String -> String`).
Concrete(TypeF<Box<GenericUnifType<E>>, GenericUnifRecordRows<E>, UnifEnumRows>),
/// A contract, seen as an opaque type. In order to compute type equality between contracts or
/// between a contract and a type, we need to carry an additional environment. This is why we
@ -970,10 +970,10 @@ fn walk_type<L: Linearizer>(
) -> Result<(), TypecheckError> {
match &ty.types {
TypeF::Dyn
| TypeF::Num
| TypeF::Number
| TypeF::Bool
| TypeF::Str
| TypeF::Sym
| TypeF::String
| TypeF::Symbol
// Currently, the parser can't generate unbound type variables by construction. Thus we
// don't check here for unbound type variables again.
| TypeF::Var(_)
@ -1773,10 +1773,10 @@ pub fn apparent_type(
.first()
.map(|labeled_ty| ApparentType::Annotated(labeled_ty.types.clone()))
.unwrap_or_else(|| apparent_type(value.as_ref(), env, resolver)),
Term::Num(_) => ApparentType::Inferred(Types::from(TypeF::Num)),
Term::Num(_) => ApparentType::Inferred(Types::from(TypeF::Number)),
Term::Bool(_) => ApparentType::Inferred(Types::from(TypeF::Bool)),
Term::SealingKey(_) => ApparentType::Inferred(Types::from(TypeF::Sym)),
Term::Str(_) | Term::StrChunks(_) => ApparentType::Inferred(Types::from(TypeF::Str)),
Term::SealingKey(_) => ApparentType::Inferred(Types::from(TypeF::Symbol)),
Term::Str(_) | Term::StrChunks(_) => ApparentType::Inferred(Types::from(TypeF::String)),
Term::Array(..) => ApparentType::Approximated(Types::from(TypeF::Array(Box::new(
Types::from(TypeF::Dyn),
)))),
@ -1995,10 +1995,10 @@ pub fn unify(
}
(UnifType::Concrete(s1), UnifType::Concrete(s2)) => match (s1, s2) {
(TypeF::Dyn, TypeF::Dyn)
| (TypeF::Num, TypeF::Num)
| (TypeF::Number, TypeF::Number)
| (TypeF::Bool, TypeF::Bool)
| (TypeF::Str, TypeF::Str)
| (TypeF::Sym, TypeF::Sym) => Ok(()),
| (TypeF::String, TypeF::String)
| (TypeF::Symbol, TypeF::Symbol) => Ok(()),
(TypeF::Array(uty1), TypeF::Array(uty2)) => unify(state, ctxt, *uty1, *uty2),
(TypeF::Arrow(s1s, s1t), TypeF::Arrow(s2s, s2t)) => {
unify(state, ctxt, (*s1s).clone(), (*s2s).clone()).map_err(|err| {
@ -2530,10 +2530,10 @@ impl ConstrainFreshRRowsVar for UnifType {
}
TypeF::Forall {body, ..} => body.constrain_fresh_rrows_var(state, var_id),
TypeF::Dyn
| TypeF::Num
| TypeF::Number
| TypeF::Bool
| TypeF::Str
| TypeF::Sym
| TypeF::String
| TypeF::Symbol
| TypeF::Flat(_)
| TypeF::Var(_)
// There can be no record rows unification variable inside an enum type
@ -2594,10 +2594,10 @@ impl ConstrainFreshERowsVar for UnifType {
}
TypeF::Forall { body, .. } => body.constrain_fresh_erows_var(state, var_id),
TypeF::Dyn
| TypeF::Num
| TypeF::Number
| TypeF::Bool
| TypeF::Str
| TypeF::Sym
| TypeF::String
| TypeF::Symbol
| TypeF::Flat(_)
| TypeF::Var(_)
| TypeF::Wildcard(_) => (),

26
src/typecheck/operation.rs
View File

@ -22,10 +22,12 @@ pub fn get_uop_type(
mk_uty_arrow!(branches.clone(), branches.clone(), branches),
)
}
// Dyn -> [| `Num, `Bool, `Str, `Enum, `Fun, `Array, `Record, `Lbl, `Other |]
// Dyn -> [| `Number, `Bool, `String, `Enum, `Function, `Array, `Record, `Label, `Other |]
UnaryOp::Typeof() => (
mk_uniftype::dynamic(),
mk_uty_enum!("Num", "Bool", "Str", "Enum", "Fun", "Array", "Record", "Lbl", "Other"),
mk_uty_enum!(
"Number", "Bool", "String", "Enum", "Function", "Array", "Record", "Label", "Other"
),
),
// Bool -> Bool -> Bool
UnaryOp::BoolAnd() | UnaryOp::BoolOr() => {
@ -85,7 +87,7 @@ pub fn get_uop_type(
UnaryOp::ArrayGen() => {
let a = UnifType::UnifVar(state.table.fresh_type_var_id());
let f_type = mk_uty_arrow!(TypeF::Num, a.clone());
let f_type = mk_uty_arrow!(TypeF::Number, a.clone());
(
mk_uniftype::num(),
mk_uty_arrow!(f_type, mk_uniftype::array(a)),
@ -99,7 +101,7 @@ pub fn get_uop_type(
let a = UnifType::UnifVar(state.table.fresh_type_var_id());
let b = UnifType::UnifVar(state.table.fresh_type_var_id());
let f_type = mk_uty_arrow!(TypeF::Str, a.clone(), b.clone());
let f_type = mk_uty_arrow!(TypeF::String, a.clone(), b.clone());
(
mk_uniftype::dyn_record(a),
mk_uty_arrow!(f_type, mk_uniftype::dyn_record(b)),
@ -184,9 +186,9 @@ pub fn get_uop_type(
mk_uty_arrow!(
mk_uniftype::str(),
mk_uty_record!(
("matched", TypeF::Str),
("index", TypeF::Num),
("groups", mk_uniftype::array(TypeF::Str))
("matched", TypeF::String),
("index", TypeF::Number),
("groups", mk_uniftype::array(TypeF::String))
)
),
),
@ -196,9 +198,9 @@ pub fn get_uop_type(
UnaryOp::StrFindCompiled(_) => (
mk_uniftype::str(),
mk_uty_record!(
("matched", TypeF::Str),
("index", TypeF::Num),
("groups", mk_uniftype::array(TypeF::Str))
("matched", TypeF::String),
("index", TypeF::Number),
("groups", mk_uniftype::array(TypeF::String))
),
),
// Dyn -> Dyn
@ -378,7 +380,7 @@ pub fn get_bop_type(
BinaryOp::StrSplit() => (
mk_uniftype::str(),
mk_uniftype::str(),
mk_uniftype::array(TypeF::Str),
mk_uniftype::array(TypeF::String),
),
// The first argument is a contract, the second is a label.
// forall a. Dyn -> Dyn -> Array a -> Array a
@ -412,7 +414,7 @@ pub fn get_bop_type(
// Morally: Array Str -> Lbl -> Lbl
// Actual: Array Str -> Dyn -> Dyn
BinaryOp::LabelWithNotes() => (
mk_uniftype::array(TypeF::Str),
mk_uniftype::array(TypeF::String),
mk_uniftype::dynamic(),
mk_uniftype::dynamic(),
),

84
src/types.rs
View File

@ -2,9 +2,9 @@
//!
//! # Base types
//!
//! - Num: a floating-point number
//! - Number: a floating-point number
//! - Bool: a boolean
//! - Str: a string literal
//! - String: a string literal
//! - Sym: a symbol, used by contracts when checking polymorphic types
//! - Array: an (heterogeneous) array
//!
@ -26,11 +26,11 @@
//! example is field access:
//!
//! ```text
//! let f = Promise(forall a. { myField : Num, a} -> Num, fun rec => rec.myField)
//! let f = Promise(forall a. { myField : Number, a} -> Number, fun rec => rec.myField)
//! ```
//!
//! The type `{ myField : Num, a }` indicates that any argument must have at least the field
//! `myField` of type `Num`, but may contain any other fields (or no additional field at all).
//! The type `{ myField : Number, a }` indicates that any argument must have at least the field
//! `myField` of type `Number`, but may contain any other fields (or no additional field at all).
//!
//! ## Dictionaries
//!
@ -124,7 +124,7 @@ pub enum EnumRowsF<ERows> {
/// The kind of a quantified type variable.
///
/// Nickel uses several forms of polymorphism. A type variable can be substituted for a type, as in
/// `id : forall a. a -> a`, for record rows as in `access_foo : forall a . {foo : Num; a} -> Num}`,
/// `id : forall a. a -> a`, for record rows as in `access_foo : forall a . {foo : Number; a} -> Number}`,
/// or for enum rows. This information is implicit in the source syntax: we don't require users to
/// write e.g. `forall a :: Type` or `forall a :: Rows`. But the kind of a variable is required for
/// the typechecker. It is thus determined during parsing and stored as `VarKind` where type
@ -213,15 +213,15 @@ pub enum TypeF<Ty, RRows, ERows> {
/// or checked.
Dyn,
/// A floating point number.
Num,
Number,
/// A boolean.
Bool,
/// A string literal.
Str,
String,
/// A symbol.
///
/// See [`crate::term::Term::Sealed`].
Sym,
Symbol,
/// A type created from a user-defined contract.
Flat(RichTerm),
/// A function.
@ -438,11 +438,11 @@ impl<Ty, RRows, ERows> TypeF<Ty, RRows, ERows> {
/// `TypeF` a functor (of arity 3). As hinted by the type signature, this function just
/// maps on "one-level" of recursion, so to speak.
///
/// Take the instantiated version `Types`, and a type of the form `(Dyn -> Dyn) -> (Num ->
/// Take the instantiated version `Types`, and a type of the form `(Dyn -> Dyn) -> (Number ->
/// Dyn)`. Then, calling `try_map_state(f_ty, ..)` on this type rows will map `f_ty` onto `(Dyn
/// -> Dyn)` and `Num -> Dyn` because they are direct children of the root `Arrow` node.
/// -> Dyn)` and `Number -> Dyn` because they are direct children of the root `Arrow` node.
///
/// Note that `f_ty` isn't mapped onto `Dyn` and `Num` recursively: map isn't a recursive
/// Note that `f_ty` isn't mapped onto `Dyn` and `Number` recursively: map isn't a recursive
/// operation. It's however a building block to express recursive operations: as an example,
/// see [RecordRows::traverse].
///
@ -462,10 +462,10 @@ impl<Ty, RRows, ERows> TypeF<Ty, RRows, ERows> {
{
match self {
TypeF::Dyn => Ok(TypeF::Dyn),
TypeF::Num => Ok(TypeF::Num),
TypeF::Number => Ok(TypeF::Number),
TypeF::Bool => Ok(TypeF::Bool),
TypeF::Str => Ok(TypeF::Str),
TypeF::Sym => Ok(TypeF::Sym),
TypeF::String => Ok(TypeF::String),
TypeF::Symbol => Ok(TypeF::Symbol),
TypeF::Flat(t) => Ok(TypeF::Flat(t)),
TypeF::Arrow(dom, codom) => Ok(TypeF::Arrow(f(dom, state)?, f(codom, state)?)),
TypeF::Var(i) => Ok(TypeF::Var(i)),
@ -794,9 +794,9 @@ impl RecordRows {
///
/// # Example
///
/// - self: ` {a : {b : Num }}`
/// - self: ` {a : {b : Number }}`
/// - path: `["a", "b"]`
/// - result: `Some(Num)`
/// - result: `Some(Number)`
pub fn row_find_path(&self, path: &[Ident]) -> Option<Types> {
if path.is_empty() {
return None;
@ -875,13 +875,13 @@ impl Types {
let ctr = match self.types {
TypeF::Dyn => contract::dynamic(),
TypeF::Num => contract::num(),
TypeF::Number => contract::num(),
TypeF::Bool => contract::bool(),
TypeF::Str => contract::string(),
TypeF::String => contract::string(),
//TODO: optimization: have a specialized contract for `Array Dyn`, to avoid mapping an
//always successful contract on each element.
TypeF::Array(ref ty) => mk_app!(contract::array(), ty.subcontract(h, pol, sy)?),
TypeF::Sym => panic!("Are you trying to check a Sym at runtime?"),
TypeF::Symbol => panic!("Are you trying to check a Sym at runtime?"),
TypeF::Arrow(ref s, ref t) => mk_app!(
contract::func(),
s.subcontract(h.clone(), !pol, sy)?,
@ -919,15 +919,19 @@ impl Types {
Ok(ctr)
}
/// Determine if a type is an atom, that is a either a primitive type (`Dyn`, `Num`, etc.) or a
/// Determine if a type is an atom, that is a either a primitive type (`Dyn`, `Number`, etc.) or a
/// type delimited by specific markers (such as a row type). Used in formatting to decide if
/// parentheses need to be inserted during pretty pretting.
pub fn fmt_is_atom(&self) -> bool {
use TypeF::*;
match &self.types {
Dyn | Num | Bool | Str | Var(_) | Record(_) | Enum(_) => true,
Flat(rt) if matches!(*rt.term, Term::Var(_)) => true,
TypeF::Dyn
| TypeF::Number
| TypeF::Bool
| TypeF::String
| TypeF::Var(_)
| TypeF::Record(_)
| TypeF::Enum(_) => true,
TypeF::Flat(rt) if matches!(*rt.term, Term::Var(_)) => true,
_ => false,
}
}
@ -1016,9 +1020,9 @@ impl Display for Types {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
match &self.types {
TypeF::Dyn => write!(f, "Dyn"),
TypeF::Num => write!(f, "Num"),
TypeF::Number => write!(f, "Number"),
TypeF::Bool => write!(f, "Bool"),
TypeF::Str => write!(f, "Str"),
TypeF::String => write!(f, "String"),
TypeF::Array(ty) => {
write!(f, "Array ")?;
@ -1028,7 +1032,7 @@ impl Display for Types {
write!(f, "({ty})")
}
}
TypeF::Sym => write!(f, "Sym"),
TypeF::Symbol => write!(f, "Sym"),
TypeF::Flat(ref t) => write!(f, "{}", t.pretty_print_cap(32)),
TypeF::Var(var) => write!(f, "{var}"),
TypeF::Forall { var, ref body, .. } => {
@ -1098,14 +1102,14 @@ mod test {
#[test]
fn types_pretty_printing() {
assert_format_eq("Num");
assert_format_eq("Num -> Num");
assert_format_eq("(Num -> Num) -> (Num -> Num) -> Num -> Num");
assert_format_eq("((Num -> Num) -> Num) -> Num");
assert_format_eq("Num -> (forall a. a -> Str) -> Str");
assert_format_eq("Number");
assert_format_eq("Number -> Number");
assert_format_eq("(Number -> Number) -> (Number -> Number) -> Number -> Number");
assert_format_eq("((Number -> Number) -> Number) -> Number");
assert_format_eq("Number -> (forall a. a -> String) -> String");
assert_format_eq("{_: Str}");
assert_format_eq("{_: (Str -> Str) -> Str}");
assert_format_eq("{_: String}");
assert_format_eq("{_: (String -> String) -> String}");
assert_format_eq("{x: (Bool -> Bool) -> Bool, y: Bool}");
assert_format_eq("forall r. {x: Bool, y: Bool, z: Bool ; r}");
@ -1114,11 +1118,11 @@ mod test {
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)");
assert_format_eq("Num -> Array (Array Str) -> Num");
assert_format_eq("Array (Num -> Num)");
assert_format_eq("Array (Array (Array Dyn) -> Num)");
assert_format_eq("Array Number");
assert_format_eq("Array (Array Number)");
assert_format_eq("Number -> Array (Array String) -> Number");
assert_format_eq("Array (Number -> Number)");
assert_format_eq("Array (Array (Array Dyn) -> Number)");
assert_format_eq("_");
assert_format_eq("_ -> _");

6
stdlib/array.ncl
View File

@ -65,7 +65,7 @@
|> drop_first
|> reverse,
length : forall a. Array a -> Num
length : forall a. Array a -> Number
| doc m%"
Results in a number representing the length of the given array.
@ -90,7 +90,7 @@
"%
= fun f l => %map% l f,
at : forall a. Num -> Array a -> a
at : forall a. Number -> Array a -> a
| doc m%"
Retrieves the n'th element from a array (0-indexed).
@ -283,7 +283,7 @@
in
fold_left aux {right = [], wrong = []} l,
generate : forall a. (Num -> a) -> Num -> Array a
generate : forall a. (Number -> a) -> Number -> Array a
| doc m%"
`generate f n` produces a array of length `n` by applying `f` on increasing numbers:
`[ f 0, f 1, ..., f (n - 1) ]`.

40
stdlib/builtin.ncl
View File

@ -1,18 +1,18 @@
{
builtin = {
is_num : Dyn -> Bool
is_number : Dyn -> Bool
| doc m%"
Checks if the given value is a number.
For example:
```nickel
is_num 1 =>
is_number 1 =>
true
is_num "Hello, World!" =>
is_number "Hello, World!" =>
false
```
"%
= fun x => %typeof% x == `Num,
= fun x => %typeof% x == `Number,
is_bool : Dyn -> Bool
| doc m%"
@ -28,19 +28,19 @@
"%
= fun x => %typeof% x == `Bool,
is_str : Dyn -> Bool
is_string : Dyn -> Bool
| doc m%"
Checks if the given value is a string.
For example:
```nickel
is_str true =>
is_string true =>
false
is_str "Hello, World!" =>
is_string "Hello, World!" =>
true
```
"%
= fun x => %typeof% x == `Str,
= fun x => %typeof% x == `String,
is_enum : Dyn -> Bool
| doc m%"
@ -69,7 +69,7 @@
false
```
"%
= fun x => %typeof% x == `Fun,
= fun x => %typeof% x == `Function,
is_array : Dyn -> Bool
| doc m%"
@ -100,12 +100,12 @@
= fun x => %typeof% x == `Record,
typeof : Dyn -> [|
`Num,
`Number,
`Bool,
`Str,
`String,
`Enum,
`Lbl,
`Fun,
`Label,
`Function,
`Array,
`Record,
`Other
@ -118,7 +118,7 @@
typeof [ 1, 2 ] =>
`Array
typeof (fun x => x) =>
`Fun
`Function
```
"%
= fun x => %typeof% x,
@ -155,7 +155,7 @@
"%
= fun x y => %deep_seq% x y,
hash : [| `Md5, `Sha1, `Sha256, `Sha512 |] -> Str -> Str
hash : [| `Md5, `Sha1, `Sha256, `Sha512 |] -> String -> String
| doc m%"
Hashes the given string provided the desired hash algorithm.
@ -167,7 +167,7 @@
"%
= fun type s => %hash% type s,
serialize : [| `Json, `Toml, `Yaml |] -> Dyn -> Str
serialize : [| `Json, `Toml, `Yaml |] -> Dyn -> String
| doc m%"
Serializes the given value to the desired representation.
@ -182,7 +182,7 @@
"%
= fun format x => %serialize% format (%force% x),
deserialize : [| `Json, `Toml, `Yaml |] -> Str -> Dyn
deserialize : [| `Json, `Toml, `Yaml |] -> String -> Dyn
| doc m%"
Deserializes the given string to a nickel value given the encoding of the string.
@ -194,7 +194,7 @@
"%
= fun format x => %deserialize% format x,
to_str | string.Stringable -> Str
to_string | string.Stringingable -> String
| doc m%"
Converts a stringable value to a string representation. Same as
`string.from`.
@ -211,7 +211,7 @@
"%
= fun x => %to_str% x,
trace : forall a. Str -> a -> a
trace : forall a. String -> a -> a
| doc m%"
`builtin.trace msg x` prints `msg` to standard output when encountered by the evaluator,
and proceed with the evaluation of `x`.
@ -246,7 +246,7 @@
"%
= fun msg label value => contract.blame_with_message msg label,
fail_with | Str -> Dyn
fail_with | String -> Dyn
| doc m%"
Unconditionally abort evaluation with the given message.

14
stdlib/contract.ncl
View File

@ -27,7 +27,7 @@
| doc m%"
Raise blame with respect to a given label and a custom error message.
Type: `forall a. Str -> Lbl -> a`
Type: `forall a. String -> Lbl -> a`
(for technical reasons, this function isn't actually statically typed)
Same as `blame`, but take an additional custom error message that will be
@ -97,7 +97,7 @@
Attach a custom error message to the current error diagnostic of a
label.
Type: `Str -> Lbl -> Lbl`
Type: `String -> Lbl -> Lbl`
(for technical reasons, this function isn't actually statically typed)
If a custom error message was previously set, there are two
@ -116,7 +116,7 @@
let ContractNum = contract.from_predicate (fun x => x > 0 && x < 50) in
let Contract = fun label value =>
if builtin.is_num value then
if builtin.is_number value then
contract.apply
ContractNum
(contract.label.with_message
@ -138,7 +138,7 @@
Attach custom error notes to the current error diagnostic of a
label.
Type: `Array Str -> Lbl -> Lbl`
Type: `Array String -> Lbl -> Lbl`
(for technical reasons, this function isn't actually statically typed)
If custom error notes were previously set, there are two
@ -157,7 +157,7 @@
let ContractNum = contract.from_predicate (fun x => x > 0 && x < 50) in
let Contract = fun label value =>
if builtin.is_num value then
if builtin.is_number value then
contract.apply
ContractNum
(label
@ -183,7 +183,7 @@
| doc m%"
Append a note to the notes of the current diagnostic of a label.
Type: `Str -> Lbl -> Lbl`
Type: `String -> Lbl -> Lbl`
(for technical reasons, this function isn't actually statically typed)
"%
= fun note label => %label_append_note% note label,
@ -209,7 +209,7 @@
if value == null then null
else contract.apply param_contract label value
in
let Contract = Nullable {foo | Num} in
let Contract = Nullable {foo | Number} in
({foo = 1} | Contract)
```

6
stdlib/internals.ncl
View File

@ -5,11 +5,11 @@
# Contract implementations
"$dyn" = fun l t => t,
"$num" = fun l t => if %typeof% t == `Num then t else %blame% l,
"$num" = fun l t => if %typeof% t == `Number then t else %blame% l,
"$bool" = fun l t => if %typeof% t == `Bool then t else %blame% l,
"$string" = fun l t => if %typeof% t == `Str then t else %blame% l,
"$string" = fun l t => if %typeof% t == `String then t else %blame% l,
"$fail" = fun l t => %blame% l,
@ -20,7 +20,7 @@
%blame% l,
"$func" = fun s t l e =>
if %typeof% e == `Fun then
if %typeof% e == `Function then
(fun x => %assume% t (%go_codom% l) (e (%assume% s (%chng_pol% (%go_dom% l)) x)))
else
%blame% l,

26
stdlib/num.ncl → stdlib/number.ncl
View File

@ -1,5 +1,5 @@
{
num = {
number = {
Integer
| doc m%"
Contract to enforce a number is an integer.
@ -13,7 +13,7 @@
```
"%
= fun label value =>
if %typeof% value == `Num then
if %typeof% value == `Number then
if value % 1 == 0 then
value
else
@ -36,7 +36,7 @@
```
"%
= fun label value =>
if %typeof% value == `Num then
if %typeof% value == `Number then
if value % 1 == 0 && value >= 0 then
value
else
@ -59,7 +59,7 @@
```
"%
= fun label value =>
if %typeof% value == `Num then
if %typeof% value == `Number then
if value % 1 == 0 && value > 0 then
value
else
@ -80,7 +80,7 @@
```
"%
= fun label value =>
if %typeof% value == `Num then
if %typeof% value == `Number then
if value != 0 then
value
else
@ -88,7 +88,7 @@
else
%blame% (%label_with_message% "not a number" label),
is_integer : Num -> Bool
is_integer : Number -> Bool
| doc m%"
Checks if the given number is an integer.
@ -102,7 +102,7 @@
"%
= fun x => x % 1 == 0,
min : Num -> Num -> Num
min : Number -> Number -> Number
| doc m%"
Results in the lowest of the given two numbers.
@ -114,7 +114,7 @@
"%
= fun x y => if x <= y then x else y,
max : Num -> Num -> Num
max : Number -> Number -> Number
| doc m%"
Results in the highest of the given two numbers.
@ -126,7 +126,7 @@
"%
= fun x y => if x >= y then x else y,
floor : Num -> Num
floor : Number -> Number
| doc m%"
Rounds the number down to the next integer.
@ -141,7 +141,7 @@
then x - (x % 1)
else x - 1 - (x % 1),
abs : Num -> Num
abs : Number -> Number
| doc m%"
Results in the absolute value of the given number.
@ -155,7 +155,7 @@
"%
= fun x => if x < 0 then -x else x,
fract : Num -> Num
fract : Number -> Number
| doc m%"
Results in the fractional part of the given number.
@ -169,7 +169,7 @@
"%
= fun x => x % 1,
truncate : Num -> Num
truncate : Number -> Number
| doc m%"
Truncates the given number.
@ -183,7 +183,7 @@
"%
= fun x => x - (x % 1),
pow : Num -> Num -> Num
pow : Number -> Number -> Number
| doc m%"
`pow x y` results in `x` to the power of `y`.

18
stdlib/record.ncl
View File

@ -1,6 +1,6 @@
{
record = {
map : forall a b. (Str -> a -> b) -> {_: a} -> {_: b}
map : forall a b. (String -> a -> b) -> {_: a} -> {_: b}
| doc m%"
Maps a function on every field of a record. The string argument of the function argument is the name of the
field.
@ -15,7 +15,7 @@
"%
= fun f r => %record_map% r f,
fields : forall a. { _: a } -> Array Str
fields : forall a. { _: a } -> Array String
| doc m%"
Given a record, results in a array of the string representation of all fields in the record.
@ -37,7 +37,7 @@
"%
= fun r => %values% r,
has_field : forall a. Str -> {_ : a} -> Bool
has_field : forall a. String -> {_ : a} -> Bool
| doc m%"
Given the name of a field and a record, checks if the record contains the given field.
@ -50,7 +50,7 @@
"%
= fun field r => %has_field% field r,
insert : forall a. Str -> a -> {_: a} -> {_: a}
insert : forall a. String -> a -> {_: a} -> {_: a}
| doc m%%"
Insert a new field in a record. `insert` doesn't mutate the original
record but returns a new one instead.
@ -67,7 +67,7 @@
"%%
= fun field content r => %record_insert% field r content,
remove : forall a. Str -> {_: a} -> {_: a}
remove : forall a. String -> {_: a} -> {_: a}
| doc m%"
Remove a field from a record. `remove` doesn't mutate the original
record but returns a new one instead.
@ -79,7 +79,7 @@
"%
= fun field r => %record_remove% field r,
update : forall a. Str -> a -> {_: a} -> {_: a}
update : forall a. String -> a -> {_: a} -> {_: a}
| doc m%"
Update a field of a record with a new value. `update` doesn't mutate the
original record but returns a new one instead. If the field to update is absent
@ -122,7 +122,7 @@
"%
= fun f => map (fun _field value => f value),
to_array : forall a. {_: a} -> Array {field: Str, value: a}
to_array : forall a. {_: a} -> Array {field: String, value: a}
| doc m%"
Converts a record to an array of key-value pairs.
@ -139,7 +139,7 @@
|> fields
|> array.map (fun field' => {field = field', value = record."%{field'}"}),
from_array : forall a. Array { field: Str, value: a} -> {_: a}
from_array : forall a. Array { field: String, value: a} -> {_: a}
| doc m%"
Convert an array of key-value pairs into a record.
@ -179,7 +179,7 @@
"%
= array.fold_left (&) {},
filter : forall a. (Str -> a -> Bool) -> {_: a} -> {_: a}
filter : forall a. (String -> a -> Bool) -> {_: a} -> {_: a}
| doc m%"
Filter a record using the given function, which is passed the name and
value for each key to make a decision.

70
stdlib/string.ncl
View File

@ -16,7 +16,7 @@
```
"%
= fun l s =>
if %typeof% s == `Str then
if %typeof% s == `String then
if s == "true" || s == "True" then
"true"
else if s == "false" || s == "False" then
@ -43,7 +43,7 @@
= let pattern = m%"^[+-]?(\d+(\.\d*)?(e[+-]?\d+)?|\.\d+(e[+-]?\d+)?)$"% in
let is_num_literal = %str_is_match% pattern in
fun l s =>
if %typeof% s == `Str then
if %typeof% s == `String then
if is_num_literal s then
s
else
@ -68,7 +68,7 @@
```
"%
= fun l s =>
if %typeof% s == `Str then
if %typeof% s == `String then
if length s == 1 then
s
else
@ -118,9 +118,9 @@
= contract.from_predicate (fun value =>
let type = builtin.typeof value in
value == null
|| type == `Num
|| type == `Number
|| type == `Bool
|| type == `Str
|| type == `String
|| type == `Enum),
NonEmpty
@ -138,7 +138,7 @@
```
"%
= fun l s =>
if %typeof% s == `Str then
if %typeof% s == `String then
if %str_length% s > 0 then
s
else
@ -146,7 +146,7 @@
else
%blame% (%label_with_message% "not a string" l),
join : Str -> Array Str -> Str
join : String -> Array String -> String
| doc m%"
Joins a array of strings given a separator.
@ -162,7 +162,7 @@
else
%head% l ++ array.fold_left (fun acc s => acc ++ sep ++ s) "" (%tail% l),
split : Str -> Str -> Array Str
split : String -> String -> Array String
| doc m%"
Splits a string based on a separator string. The separator string is not included in any string.
@ -176,7 +176,7 @@
"%
= fun sep s => %str_split% s sep,
trim : Str -> Str
trim : String -> String
| doc m%"
Trims whitespace from the start and end of the string.
@ -190,7 +190,7 @@
"%
= fun s => %str_trim% s,
characters : Str -> Array Str
characters : String -> Array String
| doc m%"
Separates a string into its individual characters.
@ -202,7 +202,7 @@
"%
= fun s => %str_chars% s,
codepoint | Character -> Num
codepoint | Character -> Number
| doc m%%"
Results in the unicode codepoint of the given character if it fits into a single codepoint.
@ -218,7 +218,7 @@
"%%
= fun s => %char_code% s,
from_codepoint | Num -> Character
from_codepoint | Number -> Character
| doc m%%"
Results in the character for a given unicode codepoint.
@ -234,7 +234,7 @@
"%%
= fun s => %char_from_code% s,
uppercase : Str -> Str
uppercase : String -> String
| doc m%"
Results in the uppercase version of the given character (including non-ascii characters) if it exists, the same
character if not.
@ -251,7 +251,7 @@
"%
= fun s => %str_uppercase% s,
lowercase : Str -> Str
lowercase : String -> String
| doc m%"
Results in the lowercase version of the given character (including non-ascii characters) if it exists, the same
character if not.
@ -268,7 +268,7 @@
"%
= fun s => %str_lowercase% s,
contains: Str -> Str -> Bool
contains: String -> String -> Bool
| doc m%"
Checks if the first string is part of the second string.
@ -284,9 +284,9 @@
"%
= fun subs s => %str_contains% s subs,
replace: Str -> Str -> Str -> Str
replace: String -> String -> String -> String
| doc m%"
`replace sub repl str` replaces every occurrence of `sub` in `str` with `repl`.
`replace sub repl String` replaces every occurrence of `sub` in `String` with `repl`.
For example:
```nickel
@ -299,9 +299,9 @@
= fun pattern replace s =>
%str_replace% s pattern replace,
replace_regex: Str -> Str -> Str -> Str
replace_regex: String -> String -> String -> String
| doc m%"
`replace_regex regex repl str` replaces every match of `regex` in `str` with `repl`.
`replace_regex regex repl String` replaces every match of `regex` in `String` with `repl`.
For example:
```nickel
@ -314,9 +314,9 @@
= fun pattern replace s =>
%str_replace_regex% s pattern replace,
is_match : Str -> Str -> Bool
is_match : String -> String -> Bool
| doc m%"
`is_match regex str` checks if `str` matches `regex`.
`is_match regex String` checks if `String` matches `regex`.
For example:
```nickel
@ -349,10 +349,10 @@
"%
= fun regex => %str_is_match% regex,
find : Str -> Str -> {matched: Str, index: Num, groups: Array Str}
find : String -> String -> {matched: String, index: Number, groups: Array String}
| doc m%"
`find regex str` matches `str` given `regex`. Results in the part of `str` that matched, the index of the
first character that was part of the match in `str`, and a arrays of all capture groups if any.
`find regex String` matches `String` given `regex`. Results in the part of `String` that matched, the index of the
first character that was part of the match in `String`, and a arrays of all capture groups if any.
For example:
```nickel
@ -368,7 +368,7 @@
"%
= fun regex => %str_find% regex,
length : Str -> Num
length : String -> Number
| doc m%"
Returns the length of the string, as measured by the number of UTF-8
[extended grapheme clusters](https://unicode.org/glossary/#extended_grapheme_cluster).
@ -389,7 +389,7 @@
"%
= fun s => %str_length% s,
substring: Num -> Num -> Str -> Str
substring: Number -> Number -> String -> String
| doc m%"
Takes a slice from the string. Errors if either index is out of range.
@ -405,10 +405,10 @@
"%
= fun start end s => %str_substr% s start end,
from | Stringable -> Str
from | Stringable -> String
| doc m%"
Converts a correct value to a string representation. Same as
`builtin.to_str`.
`builtin.to_string`.
For example:
```nickel
@ -421,7 +421,7 @@
"%
= fun x => %to_str% x,
from_num | Num -> Str
from_num | Number -> String
| doc m%"
Converts a number to its string representation.
@ -433,8 +433,8 @@
"%
= from,
# from_enum | < | Dyn> -> Str = fun tag => %to_str% tag,
from_enum | EnumTag -> Str
# from_enum | < | Dyn> -> String = fun tag => %to_str% tag,
from_enum | EnumTag -> String
| doc m%"
Converts an enum variant to its string representation.
@ -446,7 +446,7 @@
"%
= from,
from_bool | Bool -> Str
from_bool | Bool -> String
| doc m%"
Converts a boolean value to its string representation.
@ -458,7 +458,7 @@
"%
= from,
to_num | NumLiteral -> Num
to_num | NumLiteral -> Number
| doc m%"
Converts a string that represents an integer to that integer.
@ -486,8 +486,8 @@
"%
= fun s => s == "true",
# to_enum | Str -> < | Dyn> = fun s => %enum_from_str% s,
to_enum | Str -> EnumTag
# to_enum | String -> < | Dyn> = fun s => %enum_from_str% s,
to_enum | String -> EnumTag
| doc m%"
Converts any string that represents an enum variant to that enum variant.

70
tests/integration/contracts_fail.rs
View File

@ -62,7 +62,7 @@ fn enum_simple() {
#[test]
fn metavalue_contract_default_fail() {
assert_raise_blame!("{val | default | Num = true}.val");
assert_raise_blame!("{val | default | Number = true}.val");
}
#[test]
@ -72,7 +72,7 @@ fn merge_contract() {
#[test]
fn merge_default_contract() {
assert_raise_blame!("({a=2} & {b | Num} & {b | default = true}).b");
assert_raise_blame!("({a=2} & {b | Number} & {b | default = true}).b");
}
#[test]
@ -97,21 +97,23 @@ fn merge_compose_contract() {
fn records_contracts_simple() {
assert_raise_blame!("{a=1} | {}");
assert_raise_blame!("let x | {a: Num, s: Str} = {a = 1, s = 2} in %deep_seq% x x");
assert_raise_blame!("let x | {a: Num, s: Str} = {a = \"a\", s = \"b\"} in %deep_seq% x x");
assert_raise_blame!("let x | {a: Num, s: Str} = {a = 1} in %deep_seq% x x");
assert_raise_blame!("let x | {a: Num, s: Str} = {s = \"a\"} in %deep_seq% x x");
assert_raise_blame!("let x | {a: Number, s: String} = {a = 1, s = 2} in %deep_seq% x x");
assert_raise_blame!(
"let x | {a: Num, s: Str} = {a = 1, s = \"a\", extra = 1} in %deep_seq% x x"
"let x | {a: Number, s: String} = {a = \"a\", s = \"b\"} in %deep_seq% x x"
);
assert_raise_blame!("let x | {a: Number, s: String} = {a = 1} in %deep_seq% x x");
assert_raise_blame!("let x | {a: Number, s: String} = {s = \"a\"} in %deep_seq% x x");
assert_raise_blame!(
"let x | {a: Number, s: String} = {a = 1, s = \"a\", extra = 1} in %deep_seq% x x"
);
assert_raise_blame!(
"let x | {a: Num, s: {foo: Bool}} = {a = 1, s = {foo = 2}} in %deep_seq% x x"
"let x | {a: Number, s: {foo: Bool}} = {a = 1, s = {foo = 2}} in %deep_seq% x x"
);
assert_raise_blame!(
"let x | {a: Num, s: {foo: Bool}} = {a = 1, s = {foo = true, extra = 1}} in %deep_seq% x x"
"let x | {a: Number, s: {foo: Bool}} = {a = 1, s = {foo = true, extra = 1}} in %deep_seq% x x"
);
assert_raise_blame!("let x | {a: Num, s: {foo: Bool}} = {a = 1, s = {}} in %deep_seq% x x");
assert_raise_blame!("let x | {a: Number, s: {foo: Bool}} = {a = 1, s = {}} in %deep_seq% x x");
}
#[test]
@ -120,14 +122,14 @@ fn records_contracts_poly() {
(
"record argument missing all required fields",
r#"
let f | forall a. { foo: Num; a } -> Num = fun r => r.foo in
let f | forall a. { foo: Number; a } -> Number = fun r => r.foo in
f { }
"#,
),
(
"record argument missing one required field",
r#"
let f | forall r. { x: Num, y: Num; r } -> { x: Num, y: Num; r } =
let f | forall r. { x: Number, y: Number; r } -> { x: Number, y: Number; r } =
fun r => r
in
f { x = 1 }
@ -136,7 +138,8 @@ fn records_contracts_poly() {
(
"function arg which does not satisfy higher-order contract",
r#"
let f | (forall r. { x: Num; r } -> { ; r }) -> { x: Num, y: Num } -> { y : Num } =
let f | (forall r. { x: Number; r } -> { ; r })
-> { x: Number, y: Number } -> { y : Number } =
fun g r => g r
in
f (fun r => r) { x = 1, y = 2 }
@ -145,7 +148,8 @@ fn records_contracts_poly() {
(
"invalid record argument to function arg",
r#"
let f | (forall r. { x: Num; r } -> { x: Num ; r }) -> { x: Str, y: Num } -> { x: Num, y: Num } =
let f | (forall r. { x: Number; r } -> { x: Number ; r })
-> { x: String, y: Number } -> { x: Number, y: Number } =
fun g r => g r
in
# We need to evaluate x here to cause the error.
@ -155,7 +159,7 @@ fn records_contracts_poly() {
(
"return value without tail",
r#"
let f | forall r. { foo: Num; r } -> { foo: Num; r } =
let f | forall r. { foo: Number; r } -> { foo: Number; r } =
fun r => { foo = 1 }
in
f { foo = 1, other = 2 }
@ -164,7 +168,9 @@ fn records_contracts_poly() {
(
"return value with wrong tail",
r#"
let f | forall r r'. { a: Num; r } -> { a: Num; r' } -> { a: Num; r } =
let f | forall r r'. { a: Number; r }
-> { a: Number; r' }
-> { a: Number; r } =
fun r r' => r'
in
f { a = 1, b = "yes" } { a = 1, b = "no" }
@ -180,7 +186,7 @@ fn records_contracts_poly() {
(
"mapping over a record violates parametricity",
r#"
let f | forall r. { a: Num; r } -> { a: Str; r } =
let f | forall r. { a: Number; r } -> { a: String; r } =
fun r => %record_map% r (fun x => %to_str% x)
in
f { a = 1, b = 2 }
@ -189,7 +195,7 @@ fn records_contracts_poly() {
(
"merging a record violates parametricity, lhs arg",
r#"
let f | forall r. { a : Num; r } -> { a: Num; r } =
let f | forall r. { a : Number; r } -> { a: Number; r } =
fun r => { a | force = 0 } & r
in
f { a | default = 100, b = 1 }
@ -198,7 +204,7 @@ fn records_contracts_poly() {
(
"merging a record violates parametricity, rhs arg",
r#"
let f | forall r. { a : Num; r } -> { a: Num; r } =
let f | forall r. { a : Number; r } -> { a: Number; r } =
fun r => r & { a | force = 0 }
in
f { a | default = 100, b = 1 }
@ -233,7 +239,7 @@ fn lists_contracts() {
use nickel_lang::label::ty_path::Elem;
assert_matches!(
eval("%force% ([1, \"a\"] | Array Num) 0"),
eval("%force% ([1, \"a\"] | Array Number) 0"),
Err(Error::EvalError(EvalError::BlameError { .. }))
);
assert_matches!(
@ -245,7 +251,7 @@ fn lists_contracts() {
Err(Error::EvalError(EvalError::BlameError { .. }))
);
let res = eval("%force% ([{a = [1]}] | Array {a: Array Str}) false");
let res = eval("%force% ([{a = [1]}] | Array {a: Array String}) false");
match &res {
Err(Error::EvalError(EvalError::BlameError {
evaluated_arg: _,
@ -262,7 +268,7 @@ fn lists_contracts() {
res.unwrap_err().into_diagnostics(&mut files, None);
let res = eval(
"(%elem_at% (({foo = [(fun x => \"a\")]} | {foo: Array (forall a. a -> Num)}).foo) 0) false",
"(%elem_at% (({foo = [(fun x => \"a\")]} | {foo: Array (forall a. a -> Number)}).foo) 0) false",
);
match &res {
Err(Error::EvalError(EvalError::BlameError {
@ -280,17 +286,19 @@ fn lists_contracts() {
#[test]
fn records_contracts_closed() {
assert_raise_blame!("{a=1} | {}");
assert_raise_blame!("{a=1, b=2} | {a | Num}");
assert_raise_blame!("let Contract = {a | Num} & {b | Num} in ({a=1, b=2, c=3} | Contract)");
assert_raise_blame!("{a=1, b=2} | {a | Number}");
assert_raise_blame!(
"let Contract = {a | Number} & {b | Number} in ({a=1, b=2, c=3} | Contract)"
);
}
#[test]
fn dictionary_contracts() {
use nickel_lang::label::ty_path::Elem;
assert_raise_blame!("%force% (({foo} | {_: Num}) & {foo = \"string\"}) true");
assert_raise_blame!("%force% (({foo} | {_: Number}) & {foo = \"string\"}) true");
let res = eval("%force% ({foo = 1} | {_: Str}) false");
let res = eval("%force% ({foo = 1} | {_: String}) false");
match &res {
Err(Error::EvalError(EvalError::BlameError {
evaluated_arg: _,
@ -306,7 +314,7 @@ fn dictionary_contracts() {
#[test]
fn enum_complex() {
eval(
"let f : [| `foo, `bar |] -> Num = match { `foo => 1, `bar => 2, } in
"let f : [| `foo, `bar |] -> Number = match { `foo => 1, `bar => 2, } in
f `boo",
)
.unwrap_err();
@ -324,10 +332,10 @@ fn type_path_with_aliases() {
p.report(result.unwrap_err());
}
assert_blame_dont_panic("let Foo = Array Num in %force% ([\"a\"] | Foo)");
assert_blame_dont_panic("let Foo = Num -> Num in ((fun x => \"a\") | Foo) 0");
assert_blame_dont_panic("let Foo = Num -> Num in ((fun x => x) | Foo) \"a\"");
assert_blame_dont_panic("let Foo = Array Number in %force% ([\"a\"] | Foo)");
assert_blame_dont_panic("let Foo = Number -> Number in ((fun x => \"a\") | Foo) 0");
assert_blame_dont_panic("let Foo = Number -> Number in ((fun x => x) | Foo) \"a\"");
assert_blame_dont_panic(
"let Foo = {foo: Num} in %force% (((fun x => {foo = \"a\"}) | Dyn -> Foo) null)",
"let Foo = {foo: Number} in %force% (((fun x => {foo = \"a\"}) | Dyn -> Foo) null)",
);
}

2
tests/integration/destructuring/nonexistent_idents.ncl
View File

@ -1,4 +1,4 @@
(
let { a, b } = { a = 1, c = 2 } in
a: Num
a: Number
): _

40
tests/integration/destructuring/pass/preserves_types.ncl
View File

@ -1,51 +1,51 @@
let test_cases : _ = {
"destructuring let binding preserves types" =
let some_record: { a : Num, b : Str, c : Num -> Num } = { a = 1, b = "test", c = fun n => n } in
let some_record: { a : Number, b : String, c : Number -> Number } = { a = 1, b = "test", c = fun n => n } in
let { a, b, c } = some_record in
{ a_num = a, a_str = b, the_id_fn = c } : { a_num : Num, a_str : Str, the_id_fn : Num -> Num },
{ a_num = a, a_str = b, the_id_fn = c } : { a_num : Number, a_str : String, the_id_fn : Number -> Number },
"destructuring let binding infers types" =
let some_record = { a = 1, b = "test", c = fun n => n } in
let { a, b, c } = some_record in
{ a_num = a, a_str = b, the_id_fn = c } : { a_num : Num, a_str : Str, the_id_fn : Num -> Num },
{ a_num = a, a_str = b, the_id_fn = c } : { a_num : Number, a_str : String, the_id_fn : Number -> Number },
"destructuring function args preserves types" =
let dstrct : { a : Num, b : Str } -> { num : Num, str : Str } =
let dstrct : { a : Number, b : String } -> { num : Number, str : String } =
fun { a, b } => { num = a, str = b }
in
let r : { a : Num, b : Str } = { a = 1, b = "" } in
dstrct r : { num : Num, str : Str },
let r : { a : Number, b : String } = { a = 1, b = "" } in
dstrct r : { num : Number, str : String },
"destructuring function args infers types" =
let dstrct = fun { a, b } => { num = a, str = b } in
let r = { a = 1, b = "" } in
dstrct r : { num : Num, str: Str },
dstrct r : { num : Number, str: String },
"nested destructuring preserves types" =
let { a = { b, c }} = { a = { b : Num = 1, c : Str = "" }} in
{ num = b, str = c } : { num : Num, str : Str },
let { a = { b, c }} = { a = { b : Number = 1, c : String = "" }} in
{ num = b, str = c } : { num : Number, str : String },
"nested destructuring infers types" =
(let { a = { b, c }} = { a = { b = 1, c = "" }} in
{ num = b, str = c }) : { num : Num, str : Str },
{ num = b, str = c }) : { num : Number, str : String },
"destructuring rest pattern removes matched rows" =
let some_record : { a : Num, b : Str, c : Bool } = { a = 1, b = "", c = true } in
let some_record : { a : Number, b : String, c : Bool } = { a = 1, b = "", c = true } in
let { b, ..ac } = some_record in
ac : { a: Num, c: Bool },
ac : { a: Number, c: Bool },
"destructuring rest pattern infers correct type" =
let some_record = { a = 1, b = "", c = fun x => x + 1 } in
let { b, ..ac } = some_record in
ac : { a : Num, c : Num -> Num },
ac : { a : Number, c : Number -> Number },
"destructuring rest pattern preserves tail type" =
let f : forall z. { x: Num, y: Num; z } -> { y: Num; z } = fun { x, ..rest } => rest in
(f { x = 1, y = 2, z = 3 }): { y : Num, z: Num },
let f : forall z. { x: Number, y: Number; z } -> { y: Number; z } = fun { x, ..rest } => rest in
(f { x = 1, y = 2, z = 3 }): { y : Number, z: Number },
"destructuring rest pattern infers tail type" =
let f = fun { x, ..rest } => rest in
(f { x = "a", y = "b", z = 105}) : { y : Str, z : Num },
(f { x = "a", y = "b", z = 105}) : { y : String, z : Number },
# Note: we need to annotate `a` on the right-hand side of the binding
# because we don't currently have a subtyping rule like:
@ -54,10 +54,10 @@ let test_cases : _ = {
# (e.g. after RFC003 has been implemented) then it should be
# safe to remove that type annotation from this test case.
"destructuring with explicit types" =
let { a : { _ : Num } } = { a: { _ : Num } = { b = 1 } } in
a : { _ : Num },
let { a : { _ : Number } } = { a: { _ : Number } = { b = 1 } } in
a : { _ : Number },
"destructuring with contracts" =
let { a | { _ : Num } } = { a = 1 } in
a : Num,
let { a | { _ : Number } } = { a = 1 } in
a : Number,
} in true

2
tests/integration/destructuring/pass/typecontract.ncl
View File

@ -1,2 +1,2 @@
let {a | Num, b | Num} = {a=1, b=2} in
let {a | Number, b | Number} = {a=1, b=2} in
a + b == 3

2
tests/integration/destructuring/repeated_ident.ncl
View File

@ -2,5 +2,5 @@
# we're in typechecking mode. there's an open issue for this (#1098)
(
let { a, a, .. } = { a = 1, b = 2 } in
a : Num
a : Number
): _

4
tests/integration/destructuring/type_mismatch_fail.ncl
View File

@ -1,2 +1,2 @@
let { a : Num } = { a = "hi" } in
a : _
let { a : Number } = { a = "hi" } in
a : _

2
tests/integration/destructuring/typecontract_fail.ncl
View File

@ -1,2 +1,2 @@
let {a | Str} = {a=1} in
let {a | String} = {a=1} in
a

2
tests/integration/imports.rs
View File

@ -73,7 +73,7 @@ fn typecheck_fail() {
#[test]
fn static_typing_fail() {
let mut prog = TestProgram::new_from_source(
BufReader::new(format!("(let x = {} in x) : Str", mk_import("two.ncl")).as_bytes()),
BufReader::new(format!("(let x = {} in x) : String", mk_import("two.ncl")).as_bytes()),
"should_fail",
)
.unwrap();

2
tests/integration/imports/contract-fail.ncl
View File

@ -1 +1 @@
1 | Str
1 | String

2
tests/integration/imports/two.ncl
View File

@ -1 +1 @@
1 + 1 : Num
1 + 1 : Number

2
tests/integration/imports/typecheck-fail.ncl
View File

@ -1 +1 @@
false : Num
false : Number

8
tests/integration/pass/complete.ncl
View File

@ -1,10 +1,10 @@
let {Assert, ..} = import "lib/assert.ncl" in
let Y | ((Num -> Num) -> Num -> Num) -> Num -> Num = fun f => (fun x => f (x x)) (fun x => f (x x)) in
let dec : Num -> Num = fun x => x + (-1) in
let Y | ((Number -> Number) -> Number -> Number) -> Number -> Number = fun f => (fun x => f (x x)) (fun x => f (x x)) in
let dec : Number -> Number = fun x => x + (-1) in
let or : Bool -> Bool -> Bool = fun x => fun y => if x then x else y in
let fibo : Num -> Num = Y (fun fibo =>
let fibo : Number -> Number = Y (fun fibo =>
(fun x => if or (x == 0) (dec x == 0) then 1 else (fibo (dec x)) + (fibo (dec (dec x))))) in
let val : Num = 4 in
let val : Number = 4 in
(fibo val == 5 | Assert)

46
tests/integration/pass/contracts.ncl
View File

@ -24,8 +24,8 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
twice (fun x => x + 1) 3 == 5,
# strings
("hello" | Str) == "hello",
("hello" ++ " world" | Str) == "hello world",
("hello" | String) == "hello",
("hello" ++ " world" | String) == "hello world",
# enums_simple
(`foo | [| `foo, `bar |]) == `foo,
@ -36,19 +36,19 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
(`"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 |] -> Number =
match { `foo => 1, `bar => 2, _ => 3, } in
f `bar == 2,
let f : forall r. [| `foo, `bar ; r |] -> Num =
let f : forall r. [| `foo, `bar ; r |] -> Number =
match { `foo => 1, `bar => 2, _ => 3, } in
f `boo == 3,
let f : forall r. [| `foo, `"bar:baz" ; r |] -> Num =
let f : forall r. [| `foo, `"bar:baz" ; r |] -> Number =
fun x => match { `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 |] -> Number =
fun x => match { `foo => 1, `"bar:baz" => 2, _ => 3, } x in
f `"boo,grr" == 3,
@ -60,10 +60,10 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
# records_simple
({} | {}) == {},
let x | {a: Num, s: Str} = {a = 1, s = "a"} in
let x | {a: Number, s: String} = {a = 1, s = "a"} in
%deep_seq% x x == {a = 1, s = "a"},
let x | {a: Num, s: {foo: Bool}} = {a = 1, s = { foo = true}} in
let x | {a: Number, s: {foo: Bool}} = {a = 1, s = { foo = true}} in
%deep_seq% x x == {a = 1, s = { foo = true}},
# polymorphism
@ -72,8 +72,8 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
# `record.insert` and `record.remove` enforce the `$dyn_record` contract on
# their record arguments. `$dyn_record` uses `%record_map%` internally, and
# mapping over a sealed record is currently forbidden.
let extend | forall a. { ; a} -> {foo: Num ; a} = fun x => %record_insert% "foo" x 1 in
let remove | forall a. {foo: Num ; a} -> { ; a} = fun x => %record_remove% "foo" x in
let extend | forall a. { ; a} -> {foo: Number ; a} = fun x => %record_insert% "foo" x 1 in
let remove | forall a. {foo: Number ; a} -> { ; a} = fun x => %record_remove% "foo" x in
(id {} == {} | Assert) &&
(id {a = 1, b = false} == {a = 1, b = false} | Assert) &&
@ -91,24 +91,24 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
),
# records_dynamic_tail
({a = 1, b = "b"} | {a: Num, b: Str ; Dyn}) == {a = 1, b = "b"},
({a = 1, b = "b", c = false} | {a: Num, b: Str ; Dyn})
({a = 1, b = "b"} | {a: Number, b: String ; Dyn}) == {a = 1, b = "b"},
({a = 1, b = "b", c = false} | {a: Number, b: String ; Dyn})
== {a = 1, b = "b", c = false},
((fun r => r.b) | {a: Num ; Dyn} -> Dyn) {a = 1, b = 2} == 2,
((fun r => r.b) | {a: Number ; Dyn} -> Dyn) {a = 1, b = 2} == 2,
# records_open_contracts
({a = 0, b = 0} | {a | Num, ..}) == {a = 0, b = 0},
let Contract = {a | Num} & {..} in
({a = 0, b = 0} | {a | Number, ..}) == {a = 0, b = 0},
let Contract = {a | Number} & {..} in
({a = 0, b = 0} | Contract) == {a = 0, b = 0},
let Contract = {..} & {b | Num} in
let Contract = {..} & {b | Number} in
({a = 0, b = 0} | Contract) == {a = 0, b = 0},
let Contract = {a | Num, ..} & {b | Num, ..} in
let Contract = {a | Number, ..} & {b | Number, ..} in
({a = 0, b = 0, c = 0} | Contract) == {a = 0, b = 0, c = 0},
# arrays
([1, "2", false] | Array Dyn) == [1, "2", false],
([1, 2, 3] | Array Num) == [1, 2, 3],
(["1", "2", "false"] | Array Str) == ["1", "2", "false"],
([1, 2, 3] | Array Number) == [1, 2, 3],
(["1", "2", "false"] | Array String) == ["1", "2", "false"],
# full_annotations
# Check that the contract introduced by the type annotation doesn't interact
@ -117,24 +117,24 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
# nested_metavalues
# Regression test for #402
let MyContract = { x | Str } in
let MyContract = { x | String } in
{
foo | MyContract | default = { x = "From foo" },
bar | {..} | default = foo
} == { foo.x = "From foo", bar.x = "From foo"},
# mixing type and record contracts
let f | {foo | Num} -> {bar | Num} = fun r =>
let f | {foo | Number} -> {bar | Number} = fun r =>
{bar = r.foo} in
(f {foo = 1}).bar == 1,
# user-written contract application
let Extend = fun base label value =>
let derived = if builtin.is_record base then
(base & {foo | Num})
(base & {foo | Number})
else
base in
contract.apply derived label value in
let Contract = Extend {bar | Num, ..} in
let Contract = Extend {bar | Number, ..} in
let Id = Extend (fun label value => value) in
({bar = 1, foo = 1} | Contract)
& ({baz = 1} | Id)

10
tests/integration/pass/lazy-propagation.ncl
View File

@ -6,8 +6,8 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
# first example from RFC005
({
foo | {
bar : Num,
baz : Str
bar : Number,
baz : String
}
}
& {foo = {}}
@ -16,8 +16,8 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
== { foo.bar = 1, foo.baz = "a" },
# Nixel-inspired example from RFC005
let Drv = { out_path | Str, ..} in
let Package = { name | Str, drv | Drv, .. } in
let Drv = { out_path | String, ..} in
let Package = { name | String, drv | Drv, .. } in
({
build_inputs | {_: Package} = {
foo,
@ -39,7 +39,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
},
# "Outer-cross application doesn't make sense" example
(({foo = 5} | {foo | Num})
(({foo = 5} | {foo | Number})
& {bar = "bar"})
== {foo = 5, bar = "bar"},
]

2
tests/integration/pass/lib/typed-import.ncl
View File

@ -1 +1 @@
1 + 1 : Num
1 + 1 : Number

24
tests/integration/pass/metavalues.ncl
View File

@ -1,23 +1,23 @@
let {check, Assert, ..} = import "lib/assert.ncl" in
[
{val | default | Num = 10}.val == 10,
{val | default | Number = 10}.val == 10,
# merge_default
({a = 2} & {a | default = 0, b | default = true}) == {a = 2, b = true},
{a | default = {x = 1}} & {a | default = {y = "y"}} == {a = {x = 1, y = "y"}},
# merge_contract
{a = 2, b | Bool} & {a | Num, b | default = true}
{a = 2, b | Bool} & {a | Number, b | default = true}
== {a = 2, b = true},
# merge_default_contract
{a = 2} & {a | default | Num = 0, b | default = true}
{a = 2} & {a | default | Number = 0, b | default = true}
== {a = 2, b = true},
{a=2} & {a | Num} & {a | default = 3} == {a = 2},
{a=2} & {b | Num} & {b | default = 3} == {a = 2, b = 3},
({a | default = 1} & {b | Num} & {a | default = 1}).a
{a=2} & {a | Number} & {a | default = 3} == {a = 2},
{a=2} & {b | Number} & {b | default = 3} == {a = 2, b = 3},
({a | default = 1} & {b | Number} & {a | default = 1}).a
== 1,
# composed
@ -29,7 +29,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
# Check that the environments of contracts are correctly saved and restored when merging. See
# issue [#117](https://github.com/tweag/nickel/issues/117)
(let ctr_num = let x = Num in {a | x} in
(let ctr_num = let x = Number in {a | x} in
let ctr_id = let x = fun l x => x in {a | x} in
let val = let x = 1 in {a = x} in
let def = let x = 2 in {a | default = x} in
@ -48,7 +48,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
((val & (ctr_num & def)).a == 1 | Assert)),
# optionals
let Contract = {foo | Num, opt | Str | optional} in
let Contract = {foo | Number, opt | String | optional} in
let value | Contract = {foo = 1} in
(
(value == {foo = 1} | Assert) &&
@ -66,7 +66,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
# 2. Repeat foo in `{foo = 1, baz = false}` with the same value
# All of this because of #710 (https://github.com/tweag/nickel/issues/710). We
# may get rid of both once the merge semantics is clarified.
let Contract = {foo | Num, opt | Str | optional, ..} in
let Contract = {foo | Number, opt | String | optional, ..} in
let with_ctr | Contract = {foo = 1} in
let value | Contract = with_ctr & {foo = 1, baz = false} in
(
@ -81,7 +81,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
(record.fields value == ["baz", "foo"] | Assert)
),
let Contract = {foo | Num, opt | Str | optional} in
let Contract = {foo | Number, opt | String | optional} in
let value | Contract = {foo = 1 + 0, opt = "a" ++ "b"} in
(
(value == {foo = 1, opt = "ab"} | Assert) &&
@ -94,7 +94,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
(record.fields value == ["foo", "opt"] | Assert)
),
let Contract = {foo | Num, opt | Str | optional} in
let Contract = {foo | Number, opt | String | optional} in
let with_ctr | Contract = {foo = 0.5 + 0.5} in
# Same as above: we have to repeat `foo` with the same value because of #710
let value = with_ctr & {foo = 1, opt = "a" ++ "b"} in
@ -109,7 +109,7 @@ let {check, Assert, ..} = import "lib/assert.ncl" in
(record.fields value == ["foo", "opt"] | Assert)
),
let Contract = {foo | Num, opt | Str | optional} in
let Contract = {foo | Number, opt | String | optional} in
let with_ctr | Contract = {foo = 0.5 + 0.5} in
# Same as above: we have to repeat `foo` with the same value because of #710
# repeating `opt` without an `optional` attribute makes it required, but as

16
tests/integration/pass/multiple-overrides.ncl
View File

@ -6,12 +6,12 @@ let {check, ..} = import "lib/assert.ncl" in
let schema = {
config | {
output | {
value | Str,
value | String,
}
},
} in
let data = {
foo | Str
foo | String
| default = "original",
config.output.value = foo,
@ -29,12 +29,12 @@ let {check, ..} = import "lib/assert.ncl" in
let schema = {
config | {
output | {
value | Str,
value | String,
}
},
} in
let data = {
foo | Str
foo | String
| default = "original",
config.output.value = foo,
@ -51,13 +51,13 @@ let {check, ..} = import "lib/assert.ncl" in
let schema = {
config | {
output | {
value | Str,
value | String,
..
}
},
} in
let fst_data = {
foo | Str
foo | String
| default = "original",
config.output.value = foo,
@ -79,13 +79,13 @@ let {check, ..} = import "lib/assert.ncl" in
let parent = {
fst_data = {
common.fst = snd_data ++ "_data",
snd_data | Str
snd_data | String
| default = "",
fst_data = "fst",
},
snd_data = {
common.snd = fst_data ++ "_data",
fst_data | Str
fst_data | String
| default = "",
snd_data = "snd",
},

12
tests/integration/pass/records.ncl
View File

@ -29,7 +29,7 @@ let {check, ..} = import "lib/assert.ncl" in
== 2,
let r = record.map
(fun y x => if %typeof% x == `Num then x + 1 else 0)
(fun y x => if %typeof% x == `Number then x + 1 else 0)
{foo = 1, bar = "it's lazy"} in
(r.foo) + (r.bar) == 2,
@ -90,16 +90,16 @@ let {check, ..} = import "lib/assert.ncl" in
# piecewise signatures
{
foo : Num,
foo : Number,
bar = 3,
foo = 5
}.foo == 5,
{
foo : Num,
foo : Number,
foo = 1,
bar : Num = foo,
bar : Number = foo,
}.bar == 1,
let {foo : Num} = {foo = 1} in foo == 1,
let {foo : Number} = {foo = 1} in foo == 1,
# recursive overriding with common fields
# regression tests for [#579](https://github.com/tweag/nickel/issues/579)
@ -118,7 +118,7 @@ let {check, ..} = import "lib/assert.ncl" in
# recursive overriding with dictionaries
# regression tests for [#892](https://github.com/tweag/nickel/issues/892)
(({a = 1, b = a} | {_: Num}) & { a | force = 2}).b == 2,
(({a = 1, b = a} | {_: Number}) & { a | force = 2}).b == 2,
({
b = { foo = c.foo },

6
tests/integration/pass/serialize-package.ncl
View File

@ -7,7 +7,7 @@ let ctr = {
name | doc m%"
The package name.
"%
| Str,
| String,
buildInputs | doc m%"
The list of inputs for this package, specified as a
@ -39,12 +39,12 @@ let ctr = {
}
```"%
= {
package | Str
package | String
| doc m%"
The package name, given as a string. Dot-separated paths are not yet
supported"%,
input | Str
input | String
| doc m%"
The inputs where to fetch the package from. Must be a variable name
that is in scope on the Nix side."%

140
tests/integration/pass/typechecking.ncl
View File

@ -2,17 +2,17 @@ let typecheck = [
# basics
true : Bool,
false : Bool,
0 : Num,
45 : Num,
0 : Number,
45 : Number,
(fun x => x) : forall a. a -> a,
let x = 3 in (x : Num),
let x = 3 in (x : Number),
4 + false,
(true | Num) : Num,
"hello" : Str,
(true | Number) : Number,
"hello" : String,
# functions
(fun x => if x then x + 1 else 34) false,
let id : Num -> Num = fun x => x in (id 4 : Num),
let id : Number -> Number = fun x => x in (id 4 : Number),
# contracts are opaque types
# TODO: restore the following tests once type equality for contracts is
@ -24,10 +24,10 @@ let typecheck = [
# simple_polymorphism
let f : forall a. a -> a = fun x => x in
((if (f true) then (f 2) else 3) : Num),
((if (f true) then (f 2) else 3) : Number),
let f : forall a. (forall b. a -> b -> a) = fun x y => x in
((if (f true 3) then (f 2 false) else 3) : Num),
((if (f true 3) then (f 2 false) else 3) : Number),
let f : forall a. (forall b. b -> b) -> a -> a = fun f x => f x in
f ((fun z => z) : forall y. y -> y),
@ -36,78 +36,78 @@ let typecheck = [
let f : forall a. a -> a =
let g | forall a. (a -> a) = fun x => x in
g in
((if (f true) then (f 2) else 3) : Num),
((if (f true) then (f 2) else 3) : Number),
let f : forall a. a -> a =
let g | forall a. (a -> a) = fun x => x in
g g in
((if (f true) then (f 2) else 3) : Num),
((if (f true) then (f 2) else 3) : Number),
let f : forall a. a -> a =
let g : forall a. (forall b. (b -> (a -> a))) = fun y x => x in
g 0 in
((if (f true) then (f 2) else 3) : Num),
((if (f true) then (f 2) else 3) : Number),
# enums_simple
(`bla : [|`bla |]),
(`blo : [|`bla, `blo |]),
(`bla : forall r. [|`bla ; r |]),
(`bla : forall r. [|`bla, `blo ; r |]),
((`bla |> match {`bla => 3}) : Num),
((`blo |> match {`bla => 3, _ => 2}) : Num),
((`bla |> match {`bla => 3}) : Number),
((`blo |> match {`bla => 3, _ => 2}) : Number),
# enums_complex
((fun x => x |> match {`bla => 1, `ble => 2}) : [|`bla, `ble |] -> Num),
((fun x => x |> match {`bla => 1, `ble => 2}) : [|`bla, `ble |] -> Number),
((fun x => %embed% bli x |> match {`bla => 1, `ble => 2, `bli => 4})
: [|`bla, `ble |] -> Num),
: [|`bla, `ble |] -> Number),
((fun x =>
(x |> match {`bla => 3, `bli => 2})
+ (x |> match {`bli => 6, `bla => 20}))
`bla
: Num),
: Number),
let f : forall r. [|`blo, `ble ; r |] -> Num =
let f : forall r. [|`blo, `ble ; r |] -> Number =
match {`blo => 1, `ble => 2, _ => 3} in
(f `bli : Num),
(f `bli : Number),
let f : forall r. (forall p. [|`blo, `ble ; r |] -> [|`bla, `bli ; p |]) =
match {`blo => `bla, `ble => `bli, _ => `bla} in
f `bli,
# recursive let bindings
let rec f : forall a. a -> Num -> a = fun x n =>
let rec f : forall a. a -> Number -> a = fun x n =>
if n == 0 then x else if f "0" n == "1" then f x (n - 1) else f x (f 1 n) in
(f "0" 2 : Str),
let rec f : Num -> Num = fun x => if x == 0 then x else f (x - 1) in
(f 10 : Num),
let rec repeat : forall a. Num -> a -> Array a = fun n x =>
if n <= 0 then [] else repeat (n - 1) x @ [x] in (repeat 3 "foo" : Array Str),
(f "0" 2 : String),
let rec f : Number -> Number = fun x => if x == 0 then x else f (x - 1) in
(f 10 : Number),
let rec repeat : forall a. Number -> a -> Array a = fun n x =>
if n <= 0 then [] else repeat (n - 1) x @ [x] in (repeat 3 "foo" : Array String),
# static records
({bla = 1} : {bla : Num}),
({blo = true, bla = 1} : {bla : Num, blo : Bool}),
({blo = 1}.blo : Num),
({bla = true, blo = 1}.blo : Num),
let r : {bla : Bool, blo : Num} = {blo = 1, bla = true} in
((if r.bla then r.blo else 2) : Num),
({bla = 1} : {bla : Number}),
({blo = true, bla = 1} : {bla : Number, blo : Bool}),
({blo = 1}.blo : Number),
({bla = true, blo = 1}.blo : Number),
let r : {bla : Bool, blo : Number} = {blo = 1, bla = true} in
((if r.bla then r.blo else 2) : Number),
# Regression tests for https://github.com/tweag/nickel/issues/888
{"fo京o" = "bar"} : {"fo京o" : Str},
{foo = 1} : { "foo" : Num},
{"fo京o" = "bar"} : {"fo京o" : String},
{foo = 1} : { "foo" : Number},
let f : forall a r. {bla : Bool, blo : a, ble : a ; r} -> a =
fun r => if r.bla then r.blo else r.ble in
(if (f {bla = true, blo = false, ble = true, blip = 1, }) then
(f {bla = true, blo = 1, ble = 2, blip = `blip, })
else
(f {bla = true, blo = 3, ble = 4, bloppo = `bloppop, }) : Num),
(f {bla = true, blo = 3, ble = 4, bloppo = `bloppop, }) : Number),
({ "%{if true then "foo" else "bar"}" = 2, } : {_ : Num}),
({ "%{if true then "foo" else "bar"}" = 2, }."%{"bl" ++ "a"}" : Num),
({ foo = 3, bar = 4, } : {_ : Num}),
({ "%{if true then "foo" else "bar"}" = 2, } : {_ : Number}),
({ "%{if true then "foo" else "bar"}" = 2, }."%{"bl" ++ "a"}" : Number),
({ foo = 3, bar = 4, } : {_ : Number}),
# seq
(%seq% false 1 : Num),
(%seq% false 1 : Number),
((fun x y => %seq% x y) : forall a. (forall b. a -> b -> b)),
let xDyn = if false then true else false in
let yDyn = 1 + 1 in (%seq% xDyn yDyn : Dyn),
@ -116,8 +116,8 @@ let typecheck = [
[1, "2", false],
#TODO: the type system may accept the following test at some point.
#([1, "2", false] : Array Dyn),
["a", "b", "c"] : Array Str,
[1, 2, 3] : Array Num,
["a", "b", "c"] : Array String,
[1, 2, 3] : Array Number,
(fun x => [x]) : forall a. a -> Array a,
# arrays_ops
@ -125,30 +125,30 @@ let typecheck = [
(fun l => %head% l) : forall a. Array a -> a,
(fun f l => %map% l f) : forall a b. (a -> b) -> Array a -> Array b,
(fun l1 => fun l2 => l1 @ l2) : forall a. Array a -> Array a -> Array a,
(fun i l => %elem_at% l i) : forall a. Num -> Array a -> a,
(fun i l => %elem_at% l i) : forall a. Number -> Array a -> a,
# recursive_records
{a : Num = 1, b = a + 1} : {a : Num, b : Num},
{a : Num = 1 + a} : {a : Num},
{a : Num = 1 + a} : {a : Num},
{a : Number = 1, b = a + 1} : {a : Number, b : Number},
{a : Number = 1 + a} : {a : Number},
{a : Number = 1 + a} : {a : Number},
# let_inference
(let x = 1 + 2 in let f = fun x => x + 1 in f x) : Num,
# (let x = 1 + 2 in let f = fun x => x ++ "a" in f x) : Num,
{a = 1, b = 1 + a} : {a : Num, b : Num},
(let x = 1 + 2 in let f = fun x => x + 1 in f x) : Number,
# (let x = 1 + 2 in let f = fun x => x ++ "a" in f x) : Number,
{a = 1, b = 1 + a} : {a : Number, b : Number},
{f = fun x => if x == 0 then 1 else 1 + (f (x + (-1))),}
: {f : Num -> Num},
: {f : Number -> Number},
{ f = fun x => if x == 0 then 1 else 1 + (f (x + (-1))),}
: {f : Num -> Num},
: {f : Number -> Number},
# polymorphic_row_constraints
let extend | forall c. { ; c} -> {a: Str ; c} = 0 in
let remove | forall c. {a: Str ; c} -> { ; c} = 0 in
(let good = remove (extend {}) in 0) : Num,
let extend | forall c. { ; c} -> {a: String ; c} = 0 in
let remove | forall c. {a: String ; c} -> { ; c} = 0 in
(let good = remove (extend {}) in 0) : Number,
let r | {a: Num ; Dyn} = {a = 1, b = 2} in (r.a : Num),
({a = 1, b = 2} | {a: Num ; Dyn}) : {a: Num ; Dyn},
let r | {a: Number ; Dyn} = {a = 1, b = 2} in (r.a : Number),
({a = 1, b = 2} | {a: Number ; Dyn}) : {a: Number ; Dyn},
#Regression test following [#270](https://github.com/tweag/nickel/issues/270). Check that
#unifying a variable with itself doesn't introduce a loop. The failure of this test results
@ -159,54 +159,54 @@ let typecheck = [
else
gen_ (acc @ [x]) (x - 1)
}.gen_
: Array Num -> Num -> Array Num,
: Array Number -> Number -> Array Number,
{f = fun x => f x}.f : forall a. a -> a,
# shallow_inference
let x = 1 in (x + 1 : Num),
let x = "a" in (x ++ "a" : Str),
let x = "a%{"some str inside"}" in (x ++ "a" : Str),
let x = 1 in (x + 1 : Number),
let x = "a" in (x ++ "a" : String),
let x = "a%{"some str inside"}" in (x ++ "a" : String),
let x = false in (x || true : Bool),
let x = false in let y = x in let z = y in (z : Bool),
# Regression test following, see [#297](https://github.com/tweag/nickel/pull/297). Check that
# [apparent_type](../fn.apparent_type.html) doesn't silently convert array literals from `Array
# T` (for `T` a type or a type variable) to `Array Dyn`.
{foo = [1]} : {foo : Array Num},
{foo = [1]} : {foo : Array Number},
(let y = [] in y) : forall a. Array a,
# full_annotations
(let x = {val : Num | doc "some" | default = 1}.val in x + 1) : Num,
(let x = {val : Number | doc "some" | default = 1}.val in x + 1) : Number,
# Typed import
import "lib/typed-import.ncl" : Num,
import "lib/typed-import.ncl" : Number,
# Regression test for #430 (https://github.com/tweag/nickel/issues/430)
let x = import "lib/typed-import.ncl"
in x : Num,
in x : Number,
# recursive_records_quoted
{"foo" = 1} : {foo : Num},
{"foo" = 1} : {foo : Number},
# stdlib typechecking:
string.length : Str -> Num,
(string.length "Ok") : Num,
string.length : String -> Number,
(string.length "Ok") : Number,
(string.length "Ok" == 2) : Bool,
# partial application
(string.split ".") : Str -> Array Str,
(string.split ".") : String -> Array String,
(array.length [] == 0) : Bool,
(array.map (fun x => x ++ "1") ["a", "b", "c"]) : Array Str,
(array.map (fun x => x ++ "1") ["a", "b", "c"]) : Array String,
# wildcards
("hello" : _) : Str,
((fun x => x + 1) : _ -> Num) : Num -> Num,
({"foo" = 1} : {foo : _}) : {foo: Num},
("hello" : _) : String,
((fun x => x + 1) : _ -> Number) : Number -> Number,
({"foo" = 1} : {foo : _}) : {foo: Number},
# Regression test for #700 (https://github.com/tweag/nickel/issues/700)
# The (| ExportFormat) cast is only temporary, and can be removed once #671
# (https://github.com/tweag/nickel/issues/671) is closed
(record.update "foo" 5 {foo = 1}) : {_: Num},
(record.update "foo" 5 {foo = 1}) : {_: Number},
# contracts_equality
let lib = {

4
tests/integration/pass/types.ncl
View File

@ -1,4 +1,4 @@
let {Assert, ..} = import "lib/assert.ncl" in
(let plus : Num -> Num -> Num = fun x => fun y => x + y in
plus (54 : Num) (6 : Num) == 60 | Assert)
(let plus : Number -> Number -> Number = fun x => fun y => x + y in
plus (54 : Number) (6 : Number) == 60 | Assert)

2
tests/integration/pretty.rs
View File

@ -77,7 +77,7 @@ fn functions() {
fn arrays() {
check_file("arrays.ncl");
}
// TODO: Maybe fix the issue with transformation of `let A = Num` form
// TODO: Maybe fix the issue with transformation of `let A = Number` form
// in `let A = $num` which is not parsable.
//#[test]
//fn metavalues() {

8
tests/integration/query.rs
View File

@ -87,20 +87,20 @@ pub fn test_query_with_wildcard() {
}
));
// With a wildcard, there is a type annotation, inferred to be Num
assert_types_eq("{value : _ = 10}", "{value : Num = 10}", path.clone());
// With a wildcard, there is a type annotation, inferred to be Number
assert_types_eq("{value : _ = 10}", "{value : Number = 10}", path.clone());
// Wildcard infers record type
assert_types_eq(
r#"{value : _ = {foo = "quux"}}"#,
r#"{value : {foo: Str} = {foo = "quux"}}"#,
r#"{value : {foo: String} = {foo = "quux"}}"#,
path.clone(),
);
// Wildcard infers function type, infers inside `let`
assert_types_eq(
r#"{value : _ = let f = fun x => x + 1 in f}"#,
r#"{value : Num -> Num = (fun x => x + 1)}"#,
r#"{value : Number -> Number = (fun x => x + 1)}"#,
path,
);
}

4
tests/integration/records_fail.rs
View File

@ -69,11 +69,11 @@ fn dynamic_not_recursive() {
#[test]
fn missing_field() {
assert_matches!(
eval("{foo | Num, bar = foo + 1}.foo"),
eval("{foo | Number, bar = foo + 1}.foo"),
Err(Error::EvalError(EvalError::MissingFieldDef { id, ..})) if id.to_string() == "foo"
);
assert_matches!(
eval("{foo : Num, bar = foo + 1}.foo"),
eval("{foo : Number, bar = foo + 1}.foo"),
Err(Error::EvalError(EvalError::MissingFieldDef {id, ..})) if id.to_string() == "foo"
);
assert_matches!(

78
tests/integration/typecheck_fail.rs
View File

@ -38,20 +38,20 @@ fn unbound_variable_always_throws() {
#[test]
fn promise_simple_checks() {
assert_typecheck_fails!("true : Num");
assert_typecheck_fails!("true : Number");
assert_typecheck_fails!("34.5 : Bool");
assert_typecheck_fails!("(34 | Bool) : Num");
assert_typecheck_fails!("\"hello\" : Num");
assert_typecheck_fails!("(34 | Bool) : Number");
assert_typecheck_fails!("\"hello\" : Number");
}
#[test]
fn promise_complicated() {
// Inside Promises we typecheck strictly
assert_typecheck_fails!("let f : Bool -> Num = fun x => if x then x + 1 else 34 in f false");
assert_typecheck_fails!("let f : Bool -> Number = fun x => if x then x + 1 else 34 in f false");
// not annotated, non trivial let bindings type to Dyn
assert_typecheck_fails!("let id = fun x => x in (id 4 : Num)");
assert_typecheck_fails!("let id = fun x => x in (id 4 : Number)");
// no implicit polymorphism
assert_typecheck_fails!("(fun id => (id 4 : Num) + (id true : Bool)) (fun x => x)");
assert_typecheck_fails!("(fun id => (id 4 : Number) + (id true : Bool)) (fun x => x)");
// contract equality (to be fair, the current implementation is full of issues: to be reworked)
assert_typecheck_fails!("(fun x => x) : (fun l t => t) -> (fun l t => t)");
}
@ -66,11 +66,11 @@ fn simple_forall() {
"((fun f =>
let g : forall b. b -> b = fun y => y in
f g)
: ((forall a. a -> a) -> Num) -> Num)
: ((forall a. a -> a) -> Number) -> Number)
(fun x => 3)"
);
assert_typecheck_fails!(
"let g : Num -> Num = fun x => x in
"let g : Number -> Number = fun x => x in
let f : forall a. a -> a = fun x => g x in
f"
);
@ -79,22 +79,24 @@ fn simple_forall() {
#[test]
fn enum_simple() {
assert_typecheck_fails!("`foo : [| `bar |]");
assert_typecheck_fails!("match { `foo => 3} `bar : Num");
assert_typecheck_fails!("match { `foo => 3, `bar => true} `bar : Num");
assert_typecheck_fails!("match { `foo => 3} `bar : Number");
assert_typecheck_fails!("match { `foo => 3, `bar => true} `bar : Number");
}
#[test]
fn enum_complex() {
assert_typecheck_fails!("(match {`bla => 1, `ble => 2, `bli => 4}) : [| `bla, `ble |] -> Num");
assert_typecheck_fails!(
"(match {`bla => 1, `ble => 2, `bli => 4}) : [| `bla, `ble |] -> Number"
);
// TODO typecheck this, I'm not sure how to do it with row variables
// LATER NOTE: this requires row subtyping, not easy
assert_typecheck_fails!(
"(fun x =>
(x |> match {`bla => 3, `bli => 2}) +
(x |> match {`bla => 6, `blo => 20})) `bla : Num"
(x |> match {`bla => 6, `blo => 20})) `bla : Number"
);
assert_typecheck_fails!(
"let f : forall r. [| `blo, `ble ; r |] -> Num =
"let f : forall r. [| `blo, `ble ; r |] -> Number =
match {`blo => 1, `ble => 2, `bli => 3} in
f"
);
@ -107,35 +109,35 @@ fn enum_complex() {
#[test]
fn static_record_simple() {
assert_typecheck_fails!("{bla = true} : {bla : Num}");
assert_typecheck_fails!("{blo = 1} : {bla : Num}");
assert_typecheck_fails!("{bla = true} : {bla : Number}");
assert_typecheck_fails!("{blo = 1} : {bla : Number}");
assert_typecheck_fails!("{blo = 1}.blo : Bool");
assert_typecheck_fails!(
"let f : forall a. (forall r. {bla : Bool, blo : a, ble : a ; r} -> a) =
fun r => if r.bla then r.blo else r.ble in
(f {bla = true, blo = 1, ble = true, blip = `blip} : Num)"
(f {bla = true, blo = 1, ble = true, blip = `blip} : Number)"
);
assert_typecheck_fails!(
"let f : forall a. (forall r. {bla : Bool, blo : a, ble : a ; r} -> a) =
fun r => if r.bla then (r.blo + 1) else r.ble in
(f {bla = true, blo = 1, ble = 2, blip = `blip} : Num)"
(f {bla = true, blo = 1, ble = 2, blip = `blip} : Number)"
);
}
#[test]
fn dynamic_record_simple() {
assert_typecheck_fails!(
"({ \"%{if true then \"foo\" else \"bar\"}\" = 2, \"foo\" = true, }.\"bla\") : Num"
"({ \"%{if true then \"foo\" else \"bar\"}\" = 2, \"foo\" = true, }.\"bla\") : Number"
);
}
#[test]
fn simple_array() {
assert_typecheck_fails!("[1, 2, false] : Array Num");
assert_typecheck_fails!("[(1 : Str), true, \"b\"] : Array Dyn");
assert_typecheck_fails!("[1, 2, \"3\"] : Array Str");
assert_typecheck_fails!("[1, 2, false] : Array Number");
assert_typecheck_fails!("[(1 : String), true, \"b\"] : Array Dyn");
assert_typecheck_fails!("[1, 2, \"3\"] : Array String");
}
#[test]
@ -148,17 +150,17 @@ fn arrays_operations() {
#[test]
fn recursive_records() {
assert_typecheck_fails!("{a : Num = true, b = a + 1} : {a : Num, b : Num}");
assert_typecheck_fails!("{a = 1, b : Bool = a} : {a : Num, b : Bool}");
assert_typecheck_fails!("{a : Number = true, b = a + 1} : {a : Number, b : Number}");
assert_typecheck_fails!("{a = 1, b : Bool = a} : {a : Number, b : Bool}");
}
#[test]
fn let_inference() {
assert_typecheck_fails!("(let x = 1 + 2 in let f = fun x => x ++ \"a\" in f x) : Num");
assert_typecheck_fails!("(let x = 1 + 2 in let f = fun x => x ++ \"a\" in f x) : Number");
// Fields in recursive records are treated in the type environment in the same way as let-bound expressions
assert_typecheck_fails!(
"{ f = fun x => if x == 0 then false else 1 + (f (x + (-1)))} : {f : Num -> Num}"
"{ f = fun x => if x == 0 then false else 1 + (f (x + (-1)))} : {f : Number -> Number}"
);
}
@ -183,14 +185,14 @@ fn polymorphic_row_constraints() {
}
let mut res = type_check_expr(
"let extend | forall c. { ; c} -> {a: Str ; c} = null in
(let bad = extend {a = 1} in 0) : Num",
"let extend | forall c. { ; c} -> {a: String ; c} = null in
(let bad = extend {a = 1} in 0) : Number",
);
assert_row_conflict(res);
res = type_check_expr(
"let remove | forall c. {a: Str ; c} -> { ; c} = nul in
(let bad = remove (remove {a = \"a\"}) in 0) : Num",
"let remove | forall c. {a: String ; c} -> { ; c} = nul in
(let bad = remove (remove {a = \"a\"}) in 0) : Number",
);
assert_row_conflict(res);
}
@ -217,16 +219,16 @@ fn row_type_unification_variable_mismatch() {
fn dynamic_row_tail() {
// Currently, typechecking is conservative wrt the dynamic row type, meaning it can't
// convert to a less precise type with a dynamic tail.
assert_typecheck_fails!("{a = 1, b = 2} : {a: Num ; Dyn}");
assert_typecheck_fails!("{a = 1} : {a: Num ; Dyn}");
assert_typecheck_fails!("({a = 1} | {a: Num ; Dyn}) : {a: Num}");
assert_typecheck_fails!("{a = 1} : {a: Num ; Dyn}");
assert_typecheck_fails!("{a = 1, b = 2} : {a: Number ; Dyn}");
assert_typecheck_fails!("{a = 1} : {a: Number ; Dyn}");
assert_typecheck_fails!("({a = 1} | {a: Number ; Dyn}) : {a: Number}");
assert_typecheck_fails!("{a = 1} : {a: Number ; Dyn}");
}
#[test]
fn shallow_type_inference() {
assert_matches!(
type_check_expr("let x = (1 + 1) in (x + 1 : Num)"),
type_check_expr("let x = (1 + 1) in (x + 1 : Number)"),
Err(TypecheckError::TypeMismatch(..))
);
}
@ -234,7 +236,7 @@ fn shallow_type_inference() {
#[test]
fn dynamic_record_field() {
assert_matches!(
type_check_expr("let x = \"foo\" in {\"%{x}\" = 1} : {foo: Num}"),
type_check_expr("let x = \"foo\" in {\"%{x}\" = 1} : {foo: Number}"),
Err(TypecheckError::TypeMismatch(..))
);
}
@ -242,7 +244,7 @@ fn dynamic_record_field() {
#[test]
fn piecewise_signature() {
assert_matches!(
type_check_expr("{foo : Num, foo = \"bar\"}"),
type_check_expr("{foo : Number, foo = \"bar\"}"),
Err(TypecheckError::TypeMismatch(..))
);
}
@ -250,7 +252,7 @@ fn piecewise_signature() {
#[test]
fn recursive_let() {
assert_matches!(
type_check_expr("let rec f : Num -> Num = fun x => f \"hoi\" in null"),
type_check_expr("let rec f : Number -> Number = fun x => f \"hoi\" in null"),
Err(TypecheckError::TypeMismatch(..))
);
}
@ -283,7 +285,7 @@ fn wildcards_apparent_type_is_dyn() {
assert_matches!(
type_check_expr(
r#"let f : _ -> _ = fun x => x + 1 in
let g : Num = f 0 in
let g : Number = f 0 in
g"#
),
Err(TypecheckError::TypeMismatch(

2
tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl
View File

@ -1,5 +1,5 @@
{
split : forall a. Array { key: Str, value: a } -> { keys: Array Str, values: Array a } = fun pairs =>
split : forall a. Array { key: String, value: a } -> { keys: Array String, values: Array a } = fun pairs =>
array.fold_right (fun pair acc =>
{
# Error: `pair.key` should be wrapped in an array before we concat.

2
tests/snapshot/inputs/errors/dictionary_contract_fail.ncl
View File

@ -1 +1 @@
{ foo = 1, bar = "bar" } | {_: Str}
{ foo = 1, bar = "bar" } | {_: String}

2
tests/snapshot/inputs/errors/simple_contract_fail.ncl
View File

@ -1 +1 @@
1 | Str
1 | String

8
tests/snapshot/inputs/pretty/simple_record.ncl
View File

@ -1,6 +1,6 @@
{
a | Num | default = 1,
b : Str | force = "some long string that goes past the 80 character line limit for pretty printing",
c : { x : Num, y: Num } = { x = 999.8979, y = 500 },
a | Number | default = 1,
b : String | force = "some long string that goes past the 80 character line limit for pretty printing",
c : { x : Number, y: Number } = { x = 999.8979, y = 500 },
d | Array string.NonEmpty = ["a", "list", "of", "non", "empty", "strings"],
}
}

10
tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap
View File

@ -5,18 +5,18 @@ expression: snapshot
error: contract broken by a value
┌─ :1:5
│
1 │ {_: Str}
│ --- expected dictionary field type
1 │ {_: String}
│ ------ expected dictionary field type
│
┌─ [INPUTS_PATH]/errors/dictionary_contract_fail.ncl:1:9
│
1 │ { foo = 1, bar = "bar" } | {_: Str}
1 │ { foo = 1, bar = "bar" } | {_: String}
│ ^ applied to this expression
note:
┌─ [INPUTS_PATH]/errors/dictionary_contract_fail.ncl:1:28
│
1 │ { foo = 1, bar = "bar" } | {_: Str}
│ ^^^^^^^^ bound here
1 │ { foo = 1, bar = "bar" } | {_: String}
│ ^^^^^^^^^^^ bound here

10
tests/snapshot/snapshots/snapshot__error_simple_contract_fail.ncl.snap
View File

@ -5,18 +5,18 @@ expression: snapshot
error: contract broken by a value
┌─ :1:1
│
1 │ Str
│ --- expected type
1 │ String
│ ------ expected type
│
┌─ [INPUTS_PATH]/errors/simple_contract_fail.ncl:1:1
│
1 │ 1 | Str
1 │ 1 | String
│ ^ applied to this expression
note:
┌─ [INPUTS_PATH]/errors/simple_contract_fail.ncl:1:5
│
1 │ 1 | Str
│ ^^^ bound here
1 │ 1 | String
│ ^^^^^^ bound here

6
tests/snapshot/snapshots/snapshot__pretty_simple_record.ncl.snap
View File

@ -3,12 +3,12 @@ source: tests/snapshot/main.rs
expression: snapshot
---
{
a | Num | default
a | Number | default
= 1,
b : Str | force
b : String | force
=
"some long string that goes past the 80 character line limit for pretty printing",
c : {x: Num, y: Num}
c : {x: Number, y: Number}
= { x = 999.8979, y = 500, },
d | Array (string.NonEmpty)
= [ "a", "list", "of", "non", "empty", "strings" ],