From 030c71eed71f66b58fb9101e66ba6d8353655cc0 Mon Sep 17 00:00:00 2001 From: Yann Hamdaoui Date: Tue, 7 Mar 2023 10:52:26 +0100 Subject: [PATCH] Use long names for string and numbers 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. --- HACKING.md | 4 +- benches/arrays/fold.ncl | 2 +- benches/arrays/generate.ncl | 2 +- benches/arrays/primes.ncl | 6 +- benches/arrays/random.ncl | 4 +- benches/arrays/sum.ncl | 2 +- benches/mantis/deploy.ncl | 2 +- benches/mantis/jobs/mantis.ncl | 18 +- benches/mantis/lib.ncl | 2 +- benches/mantis/schemas/nomad/types.ncl | 332 +++++++++--------- benches/mantis/tasks/telegraf.ncl | 4 +- benches/nixpkgs/lists.ncl | 30 +- doc/manual/contracts.md | 91 +++-- doc/manual/cookbook.md | 8 +- doc/manual/correctness.md | 36 +- doc/manual/merging.md | 18 +- doc/manual/syntax.md | 30 +- doc/manual/tuto.md | 16 +- doc/manual/types-vs-contracts.md | 10 +- doc/manual/typing.md | 128 +++---- examples/config-gcc/config-gcc.ncl | 8 +- examples/record-contract/record-contract.ncl | 20 +- .../simple-contracts/simple-contract-div.ncl | 4 +- lsp/nls/src/requests/completion.rs | 2 +- notes/standardization-meeting-07.12.21.md | 14 +- notes/sum-as-dependent-records.md | 2 +- notes/typechecking.md | 4 +- spec/type-system/notes/examples.md | 38 +- src/deserialize.rs | 6 +- src/error.rs | 8 +- src/eval/fixpoint.rs | 4 +- src/eval/operation.rs | 10 +- src/eval/tests.rs | 4 +- src/label.rs | 43 +-- src/parser/grammar.lalrpop | 8 +- src/parser/lexer.rs | 8 +- src/parser/uniterm.rs | 6 +- src/pretty.rs | 6 +- src/stdlib.rs | 12 +- src/term/mod.rs | 2 +- src/transform/free_vars.rs | 6 +- src/typecheck/eq.rs | 6 +- src/typecheck/mk_uniftype.rs | 6 +- src/typecheck/mod.rs | 32 +- src/typecheck/operation.rs | 26 +- src/types.rs | 84 ++--- stdlib/array.ncl | 6 +- stdlib/builtin.ncl | 40 +-- stdlib/contract.ncl | 14 +- stdlib/internals.ncl | 6 +- stdlib/{num.ncl => number.ncl} | 26 +- stdlib/record.ncl | 18 +- stdlib/string.ncl | 70 ++-- tests/integration/contracts_fail.rs | 70 ++-- .../destructuring/nonexistent_idents.ncl | 2 +- .../destructuring/pass/preserves_types.ncl | 40 +-- .../destructuring/pass/typecontract.ncl | 2 +- .../destructuring/repeated_ident.ncl | 2 +- .../destructuring/type_mismatch_fail.ncl | 4 +- .../destructuring/typecontract_fail.ncl | 2 +- tests/integration/imports.rs | 2 +- tests/integration/imports/contract-fail.ncl | 2 +- tests/integration/imports/two.ncl | 2 +- tests/integration/imports/typecheck-fail.ncl | 2 +- tests/integration/pass/complete.ncl | 8 +- tests/integration/pass/contracts.ncl | 46 +-- tests/integration/pass/lazy-propagation.ncl | 10 +- tests/integration/pass/lib/typed-import.ncl | 2 +- tests/integration/pass/metavalues.ncl | 24 +- tests/integration/pass/multiple-overrides.ncl | 16 +- tests/integration/pass/records.ncl | 12 +- tests/integration/pass/serialize-package.ncl | 6 +- tests/integration/pass/typechecking.ncl | 140 ++++---- tests/integration/pass/types.ncl | 4 +- tests/integration/pretty.rs | 2 +- tests/integration/query.rs | 8 +- tests/integration/records_fail.rs | 4 +- tests/integration/typecheck_fail.rs | 78 ++-- ...row_type_unification_variable_mismatch.ncl | 2 +- .../errors/dictionary_contract_fail.ncl | 2 +- .../inputs/errors/simple_contract_fail.ncl | 2 +- .../snapshot/inputs/pretty/simple_record.ncl | 8 +- ...t__error_dictionary_contract_fail.ncl.snap | 10 +- ...pshot__error_simple_contract_fail.ncl.snap | 10 +- .../snapshot__pretty_simple_record.ncl.snap | 6 +- 85 files changed, 920 insertions(+), 904 deletions(-) rename stdlib/{num.ncl => number.ncl} (89%) diff --git a/HACKING.md b/HACKING.md index 0b208b85..44d03947 100644 --- a/HACKING.md +++ b/HACKING.md @@ -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 diff --git a/benches/arrays/fold.ncl b/benches/arrays/fold.ncl index 2c75ae8d..4bb934ed 100644 --- a/benches/arrays/fold.ncl +++ b/benches/arrays/fold.ncl @@ -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 diff --git a/benches/arrays/generate.ncl b/benches/arrays/generate.ncl index 71a7b326..b9fb2b1e 100644 --- a/benches/arrays/generate.ncl +++ b/benches/arrays/generate.ncl @@ -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], diff --git a/benches/arrays/primes.ncl b/benches/arrays/primes.ncl index dd932b77..81a8f0e0 100644 --- a/benches/arrays/primes.ncl +++ b/benches/arrays/primes.ncl @@ -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) diff --git a/benches/arrays/random.ncl b/benches/arrays/random.ncl index 48a0772e..adcbdf1f 100644 --- a/benches/arrays/random.ncl +++ b/benches/arrays/random.ncl @@ -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] diff --git a/benches/arrays/sum.ncl b/benches/arrays/sum.ncl index 018fb0b3..8cc10a9a 100644 --- a/benches/arrays/sum.ncl +++ b/benches/arrays/sum.ncl @@ -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) diff --git a/benches/mantis/deploy.ncl b/benches/mantis/deploy.ncl index 54863073..e5b75769 100644 --- a/benches/mantis/deploy.ncl +++ b/benches/mantis/deploy.ncl @@ -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}"}) diff --git a/benches/mantis/jobs/mantis.ncl b/benches/mantis/jobs/mantis.ncl index 5d047ff0..cb486987 100644 --- a/benches/mantis/jobs/mantis.ncl +++ b/benches/mantis/jobs/mantis.ncl @@ -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, diff --git a/benches/mantis/lib.ncl b/benches/mantis/lib.ncl index 9e22b440..0e01099f 100644 --- a/benches/mantis/lib.ncl +++ b/benches/mantis/lib.ncl @@ -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 diff --git a/benches/mantis/schemas/nomad/types.ncl b/benches/mantis/schemas/nomad/types.ncl index 1106d919..5c635297 100644 --- a/benches/mantis/schemas/nomad/types.ncl +++ b/benches/mantis/schemas/nomad/types.ncl @@ -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. diff --git a/benches/mantis/tasks/telegraf.ncl b/benches/mantis/tasks/telegraf.ncl index cc687ed9..a67ea8c5 100644 --- a/benches/mantis/tasks/telegraf.ncl +++ b/benches/mantis/tasks/telegraf.ncl @@ -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, diff --git a/benches/nixpkgs/lists.ncl b/benches/nixpkgs/lists.ncl index 176eb0f2..4b6edb2c 100644 --- a/benches/nixpkgs/lists.ncl +++ b/benches/nixpkgs/lists.ncl @@ -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`. diff --git a/doc/manual/contracts.md b/doc/manual/contracts.md index 99994193..ac391515 100644 --- a/doc/manual/contracts.md +++ b/doc/manual/contracts.md @@ -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 = , 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. diff --git a/doc/manual/cookbook.md b/doc/manual/cookbook.md index c5f6aac2..83237dcf 100644 --- a/doc/manual/cookbook.md +++ b/doc/manual/cookbook.md @@ -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, } ``` diff --git a/doc/manual/correctness.md b/doc/manual/correctness.md index e2e3c10d..d5834ca7 100644 --- a/doc/manual/correctness.md +++ b/doc/manual/correctness.md @@ -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 │ ┌─ (generated by evaluation):1:1 diff --git a/doc/manual/merging.md b/doc/manual/merging.md index ef92d0e7..b7a3699c 100644 --- a/doc/manual/merging.md +++ b/doc/manual/merging.md @@ -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 diff --git a/doc/manual/syntax.md b/doc/manual/syntax.md index 4994e78b..d149f568 100644 --- a/doc/manual/syntax.md +++ b/doc/manual/syntax.md @@ -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 ` | `. 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 diff --git a/doc/manual/tuto.md b/doc/manual/tuto.md index cf16d299..ab9b8001 100644 --- a/doc/manual/tuto.md +++ b/doc/manual/tuto.md @@ -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. diff --git a/doc/manual/types-vs-contracts.md b/doc/manual/types-vs-contracts.md index 525013eb..2d80077d 100644 --- a/doc/manual/types-vs-contracts.md +++ b/doc/manual/types-vs-contracts.md @@ -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", diff --git a/doc/manual/typing.md b/doc/manual/typing.md index ad472a03..4618af24 100644 --- a/doc/manual/typing.md +++ b/doc/manual/typing.md @@ -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`. @@ -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 diff --git a/examples/config-gcc/config-gcc.ncl b/examples/config-gcc/config-gcc.ncl index 402cf023..9bdf88ef 100644 --- a/examples/config-gcc/config-gcc.ncl +++ b/examples/config-gcc/config-gcc.ncl @@ -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 = [], diff --git a/examples/record-contract/record-contract.ncl b/examples/record-contract/record-contract.ncl index ee4fbf76..b9a8ecdc 100644 --- a/examples/record-contract/record-contract.ncl +++ b/examples/record-contract/record-contract.ncl @@ -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, }, }, diff --git a/examples/simple-contracts/simple-contract-div.ncl b/examples/simple-contracts/simple-contract-div.ncl index 3821a759..ae8ca0a0 100644 --- a/examples/simple-contracts/simple-contract-div.ncl +++ b/examples/simple-contracts/simple-contract-div.ncl @@ -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 diff --git a/lsp/nls/src/requests/completion.rs b/lsp/nls/src/requests/completion.rs index fa001735..843c6be2 100644 --- a/lsp/nls/src/requests/completion.rs +++ b/lsp/nls/src/requests/completion.rs @@ -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)); diff --git a/notes/standardization-meeting-07.12.21.md b/notes/standardization-meeting-07.12.21.md index 9acac595..c6b0f3d7 100644 --- a/notes/standardization-meeting-07.12.21.md +++ b/notes/standardization-meeting-07.12.21.md @@ -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 diff --git a/notes/sum-as-dependent-records.md b/notes/sum-as-dependent-records.md index 22e2b7ac..7251d4db 100644 --- a/notes/sum-as-dependent-records.md +++ b/notes/sum-as-dependent-records.md @@ -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. diff --git a/notes/typechecking.md b/notes/typechecking.md index 880fb837..4e5cf477 100644 --- a/notes/typechecking.md +++ b/notes/typechecking.md @@ -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.... diff --git a/spec/type-system/notes/examples.md b/spec/type-system/notes/examples.md index f8f760e2..d9ce4beb 100644 --- a/spec/type-system/notes/examples.md +++ b/spec/type-system/notes/examples.md @@ -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 diff --git a/src/deserialize.rs b/src/deserialize.rs index d4619b6e..32a1e157 100644 --- a/src/deserialize.rs +++ b/src/deserialize.rs @@ -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") diff --git a/src/error.rs b/src/error.rs index 3dc4b8f1..9792f169 100644 --- a/src/error.rs +++ b/src/error.rs @@ -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, diff --git a/src/eval/fixpoint.rs b/src/eval/fixpoint.rs index 1ed402c0..94895347 100644 --- a/src/eval/fixpoint.rs +++ b/src/eval/fixpoint.rs @@ -153,8 +153,8 @@ pub fn patch_field( // // ``` // let Variant = match { - // `num => Num, - // `str => Str, + // `num => Number, + // `str => String, // `any => Dyn, // } in // diff --git a/src/eval/operation.rs b/src/eval/operation.rs index 625dc2da..d3d4e988 100644 --- a/src/eval/operation.rs +++ b/src/eval/operation.rs @@ -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 VirtualMachine { } 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( diff --git a/src/eval/tests.rs b/src/eval/tests.rs index 0fe79a6e..fd1d6b03 100644 --- a/src/eval/tests.rs +++ b/src/eval/tests.rs @@ -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] diff --git a/src/label.rs b/src/label.rs index 88ef3e2e..d241e368 100644 --- a/src/label.rs +++ b/src/label.rs @@ -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("", String::from("empty")), diff --git a/src/parser/grammar.lalrpop b/src/parser/grammar.lalrpop index be15d405..32c24fab 100644 --- a/src/parser/grammar.lalrpop +++ b/src/parser/grammar.lalrpop @@ -870,9 +870,9 @@ NOpPre: 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: })), - "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), diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs index f969e5e0..06e2b499 100644 --- a/src/parser/lexer.rs +++ b/src/parser/lexer.rs @@ -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, diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs index 1a4f0739..a29811a3 100644 --- a/src/parser/uniterm.rs +++ b/src/parser/uniterm.rs @@ -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) => { diff --git a/src/pretty.rs b/src/pretty.rs index 9955f4b7..09093996 100644 --- a/src/pretty.rs +++ b/src/pretty.rs @@ -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, .. } => { diff --git a/src/stdlib.rs b/src/stdlib.rs index 545c8495..df8ad9dd 100644 --- a/src/stdlib.rs +++ b/src/stdlib.rs @@ -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 => "", StdlibModule::Record => "", StdlibModule::String => "", - StdlibModule::Num => "", + StdlibModule::Number => "", StdlibModule::Function => "", StdlibModule::Internals => "", } @@ -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 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 for Ident { StdlibModule::Array => "array", StdlibModule::Record => "record", StdlibModule::String => "string", - StdlibModule::Num => "num", + StdlibModule::Number => "num", StdlibModule::Function => "function", StdlibModule::Internals => "internals", }; diff --git a/src/term/mod.rs b/src/term/mod.rs index 90aa14e0..03ca21af 100644 --- a/src/term/mod.rs +++ b/src/term/mod.rs @@ -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() diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs index 5e1868d6..5393f74e 100644 --- a/src/transform/free_vars.rs +++ b/src/transform/free_vars.rs @@ -180,10 +180,10 @@ impl CollectFreeVars for Types { fn collect_free_vars(&mut self, set: &mut HashSet) { 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) => { diff --git a/src/typecheck/eq.rs b/src/typecheck/eq.rs index bca53e2a..f385d903 100644 --- a/src/typecheck/eq.rs +++ b/src/typecheck/eq.rs @@ -441,10 +441,10 @@ fn type_eq_bounded( (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) } diff --git a/src/typecheck/mk_uniftype.rs b/src/typecheck/mk_uniftype.rs index bff8eedc..357e9c85 100644 --- a/src/typecheck/mk_uniftype.rs +++ b/src/typecheck/mk_uniftype.rs @@ -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); diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs index 69629fba..d96556d6 100644 --- a/src/typecheck/mod.rs +++ b/src/typecheck/mod.rs @@ -123,7 +123,7 @@ pub enum UnifEnumRows { /// representation, hence the parametrization. #[derive(Clone, PartialEq, Debug)] pub enum GenericUnifType { - /// A concrete type (like `Num` or `Str -> Str`). + /// A concrete type (like `Number` or `String -> String`). Concrete(TypeF>, GenericUnifRecordRows, 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( ) -> 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(_) => (), diff --git a/src/typecheck/operation.rs b/src/typecheck/operation.rs index f2a41fc2..a1dc0520 100644 --- a/src/typecheck/operation.rs +++ b/src/typecheck/operation.rs @@ -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(), ), diff --git a/src/types.rs b/src/types.rs index 47ba4c0c..d58573ec 100644 --- a/src/types.rs +++ b/src/types.rs @@ -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 { /// 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 { /// 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 TypeF { /// `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 TypeF { { 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 { 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("_ -> _"); diff --git a/stdlib/array.ncl b/stdlib/array.ncl index f75dab49..f3c4f097 100644 --- a/stdlib/array.ncl +++ b/stdlib/array.ncl @@ -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) ]`. diff --git a/stdlib/builtin.ncl b/stdlib/builtin.ncl index 924015d0..a97b768a 100644 --- a/stdlib/builtin.ncl +++ b/stdlib/builtin.ncl @@ -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. diff --git a/stdlib/contract.ncl b/stdlib/contract.ncl index b3a6565d..2671d703 100644 --- a/stdlib/contract.ncl +++ b/stdlib/contract.ncl @@ -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) ``` diff --git a/stdlib/internals.ncl b/stdlib/internals.ncl index 912890ac..e7ffb5db 100644 --- a/stdlib/internals.ncl +++ b/stdlib/internals.ncl @@ -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, diff --git a/stdlib/num.ncl b/stdlib/number.ncl similarity index 89% rename from stdlib/num.ncl rename to stdlib/number.ncl index 0499d1b3..8168fe67 100644 --- a/stdlib/num.ncl +++ b/stdlib/number.ncl @@ -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`. diff --git a/stdlib/record.ncl b/stdlib/record.ncl index d862412a..a2425b10 100644 --- a/stdlib/record.ncl +++ b/stdlib/record.ncl @@ -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. diff --git a/stdlib/string.ncl b/stdlib/string.ncl index 719e03f1..a0ffcd9a 100644 --- a/stdlib/string.ncl +++ b/stdlib/string.ncl @@ -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. diff --git a/tests/integration/contracts_fail.rs b/tests/integration/contracts_fail.rs index 15bc685e..bce79004 100644 --- a/tests/integration/contracts_fail.rs +++ b/tests/integration/contracts_fail.rs @@ -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)", ); } diff --git a/tests/integration/destructuring/nonexistent_idents.ncl b/tests/integration/destructuring/nonexistent_idents.ncl index adc2cffe..4dde684f 100644 --- a/tests/integration/destructuring/nonexistent_idents.ncl +++ b/tests/integration/destructuring/nonexistent_idents.ncl @@ -1,4 +1,4 @@ ( let { a, b } = { a = 1, c = 2 } in - a: Num + a: Number ): _ diff --git a/tests/integration/destructuring/pass/preserves_types.ncl b/tests/integration/destructuring/pass/preserves_types.ncl index 1bf8fa9a..b09d0f89 100644 --- a/tests/integration/destructuring/pass/preserves_types.ncl +++ b/tests/integration/destructuring/pass/preserves_types.ncl @@ -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 diff --git a/tests/integration/destructuring/pass/typecontract.ncl b/tests/integration/destructuring/pass/typecontract.ncl index fdd5cca4..6ba39b51 100644 --- a/tests/integration/destructuring/pass/typecontract.ncl +++ b/tests/integration/destructuring/pass/typecontract.ncl @@ -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 diff --git a/tests/integration/destructuring/repeated_ident.ncl b/tests/integration/destructuring/repeated_ident.ncl index c7370fe9..cc9293e1 100644 --- a/tests/integration/destructuring/repeated_ident.ncl +++ b/tests/integration/destructuring/repeated_ident.ncl @@ -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 ): _ diff --git a/tests/integration/destructuring/type_mismatch_fail.ncl b/tests/integration/destructuring/type_mismatch_fail.ncl index 25f7833b..3c86e06b 100644 --- a/tests/integration/destructuring/type_mismatch_fail.ncl +++ b/tests/integration/destructuring/type_mismatch_fail.ncl @@ -1,2 +1,2 @@ -let { a : Num } = { a = "hi" } in -a : _ \ No newline at end of file +let { a : Number } = { a = "hi" } in +a : _ diff --git a/tests/integration/destructuring/typecontract_fail.ncl b/tests/integration/destructuring/typecontract_fail.ncl index c570eeb8..a78cee85 100644 --- a/tests/integration/destructuring/typecontract_fail.ncl +++ b/tests/integration/destructuring/typecontract_fail.ncl @@ -1,2 +1,2 @@ -let {a | Str} = {a=1} in +let {a | String} = {a=1} in a diff --git a/tests/integration/imports.rs b/tests/integration/imports.rs index 70c7a880..ef1eb9bc 100644 --- a/tests/integration/imports.rs +++ b/tests/integration/imports.rs @@ -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(); diff --git a/tests/integration/imports/contract-fail.ncl b/tests/integration/imports/contract-fail.ncl index 3054229d..5dc51108 100644 --- a/tests/integration/imports/contract-fail.ncl +++ b/tests/integration/imports/contract-fail.ncl @@ -1 +1 @@ -1 | Str +1 | String diff --git a/tests/integration/imports/two.ncl b/tests/integration/imports/two.ncl index a4368194..92a490cd 100644 --- a/tests/integration/imports/two.ncl +++ b/tests/integration/imports/two.ncl @@ -1 +1 @@ -1 + 1 : Num +1 + 1 : Number diff --git a/tests/integration/imports/typecheck-fail.ncl b/tests/integration/imports/typecheck-fail.ncl index 707321ad..11d3bfbf 100644 --- a/tests/integration/imports/typecheck-fail.ncl +++ b/tests/integration/imports/typecheck-fail.ncl @@ -1 +1 @@ -false : Num +false : Number diff --git a/tests/integration/pass/complete.ncl b/tests/integration/pass/complete.ncl index 16537223..8f5955fc 100644 --- a/tests/integration/pass/complete.ncl +++ b/tests/integration/pass/complete.ncl @@ -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) diff --git a/tests/integration/pass/contracts.ncl b/tests/integration/pass/contracts.ncl index 4252689e..4e25f899 100644 --- a/tests/integration/pass/contracts.ncl +++ b/tests/integration/pass/contracts.ncl @@ -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) diff --git a/tests/integration/pass/lazy-propagation.ncl b/tests/integration/pass/lazy-propagation.ncl index 8db45279..1e5228af 100644 --- a/tests/integration/pass/lazy-propagation.ncl +++ b/tests/integration/pass/lazy-propagation.ncl @@ -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"}, ] diff --git a/tests/integration/pass/lib/typed-import.ncl b/tests/integration/pass/lib/typed-import.ncl index a4368194..92a490cd 100644 --- a/tests/integration/pass/lib/typed-import.ncl +++ b/tests/integration/pass/lib/typed-import.ncl @@ -1 +1 @@ -1 + 1 : Num +1 + 1 : Number diff --git a/tests/integration/pass/metavalues.ncl b/tests/integration/pass/metavalues.ncl index dd76454c..18971718 100644 --- a/tests/integration/pass/metavalues.ncl +++ b/tests/integration/pass/metavalues.ncl @@ -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 diff --git a/tests/integration/pass/multiple-overrides.ncl b/tests/integration/pass/multiple-overrides.ncl index 8890c150..89be1b07 100644 --- a/tests/integration/pass/multiple-overrides.ncl +++ b/tests/integration/pass/multiple-overrides.ncl @@ -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", }, diff --git a/tests/integration/pass/records.ncl b/tests/integration/pass/records.ncl index ffbdcf36..522d8aff 100644 --- a/tests/integration/pass/records.ncl +++ b/tests/integration/pass/records.ncl @@ -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 }, diff --git a/tests/integration/pass/serialize-package.ncl b/tests/integration/pass/serialize-package.ncl index fb56d1ff..0aa97aa9 100644 --- a/tests/integration/pass/serialize-package.ncl +++ b/tests/integration/pass/serialize-package.ncl @@ -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."% diff --git a/tests/integration/pass/typechecking.ncl b/tests/integration/pass/typechecking.ncl index 0b8ab096..e0da94a3 100644 --- a/tests/integration/pass/typechecking.ncl +++ b/tests/integration/pass/typechecking.ncl @@ -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 = { diff --git a/tests/integration/pass/types.ncl b/tests/integration/pass/types.ncl index fac37312..92ef322c 100644 --- a/tests/integration/pass/types.ncl +++ b/tests/integration/pass/types.ncl @@ -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) diff --git a/tests/integration/pretty.rs b/tests/integration/pretty.rs index 33b1801b..2a552b46 100644 --- a/tests/integration/pretty.rs +++ b/tests/integration/pretty.rs @@ -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() { diff --git a/tests/integration/query.rs b/tests/integration/query.rs index 1bf1b00f..fdfb294d 100644 --- a/tests/integration/query.rs +++ b/tests/integration/query.rs @@ -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, ); } diff --git a/tests/integration/records_fail.rs b/tests/integration/records_fail.rs index 3312cac2..0bd04f4f 100644 --- a/tests/integration/records_fail.rs +++ b/tests/integration/records_fail.rs @@ -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!( diff --git a/tests/integration/typecheck_fail.rs b/tests/integration/typecheck_fail.rs index 6bb6a15d..fcf3b36d 100644 --- a/tests/integration/typecheck_fail.rs +++ b/tests/integration/typecheck_fail.rs @@ -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( diff --git a/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl b/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl index 49897d99..c7069bb8 100644 --- a/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl +++ b/tests/integration/typecheck_fail/row_type_unification_variable_mismatch.ncl @@ -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. diff --git a/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl b/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl index 3dec3c8c..50a2042c 100644 --- a/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl +++ b/tests/snapshot/inputs/errors/dictionary_contract_fail.ncl @@ -1 +1 @@ -{ foo = 1, bar = "bar" } | {_: Str} \ No newline at end of file +{ foo = 1, bar = "bar" } | {_: String} diff --git a/tests/snapshot/inputs/errors/simple_contract_fail.ncl b/tests/snapshot/inputs/errors/simple_contract_fail.ncl index 13c3b9c1..5dc51108 100644 --- a/tests/snapshot/inputs/errors/simple_contract_fail.ncl +++ b/tests/snapshot/inputs/errors/simple_contract_fail.ncl @@ -1 +1 @@ -1 | Str \ No newline at end of file +1 | String diff --git a/tests/snapshot/inputs/pretty/simple_record.ncl b/tests/snapshot/inputs/pretty/simple_record.ncl index 23f59862..dc3bf94b 100644 --- a/tests/snapshot/inputs/pretty/simple_record.ncl +++ b/tests/snapshot/inputs/pretty/simple_record.ncl @@ -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"], -} \ No newline at end of file +} diff --git a/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap index 2dd5274f..d87b9f87 100644 --- a/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap +++ b/tests/snapshot/snapshots/snapshot__error_dictionary_contract_fail.ncl.snap @@ -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 diff --git a/tests/snapshot/snapshots/snapshot__error_simple_contract_fail.ncl.snap b/tests/snapshot/snapshots/snapshot__error_simple_contract_fail.ncl.snap index 6a082aaf..a8c0c812 100644 --- a/tests/snapshot/snapshots/snapshot__error_simple_contract_fail.ncl.snap +++ b/tests/snapshot/snapshots/snapshot__error_simple_contract_fail.ncl.snap @@ -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 diff --git a/tests/snapshot/snapshots/snapshot__pretty_simple_record.ncl.snap b/tests/snapshot/snapshots/snapshot__pretty_simple_record.ncl.snap index 758923bd..3c47e9a2 100644 --- a/tests/snapshot/snapshots/snapshot__pretty_simple_record.ncl.snap +++ b/tests/snapshot/snapshots/snapshot__pretty_simple_record.ncl.snap @@ -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" ],