From d6c745207be59ef8301580782dee2abd717f9fee Mon Sep 17 00:00:00 2001 From: Peter <43498358+Petersmit27@users.noreply.github.com> Date: Wed, 1 Nov 2023 09:29:33 +0100 Subject: [PATCH] init commit again --- IBAF-cbs/Funcons-beta | 1 - IBAF-cbs/Funcons-beta/.gitignore | 5 + .../Abnormal/Abrupting/Abrupting.cbs | 91 +++ .../Computations/Abnormal/Abrupting/index.md | 131 ++++ .../Abnormal/Abrupting/tests/finally.config | 15 + .../Abrupting/tests/handle-abrupt.config | 17 + .../Abnormal/Breaking/Breaking.cbs | 59 ++ .../Computations/Abnormal/Breaking/index.md | 98 +++ .../Breaking/tests/handle-break.config | 16 + .../Abnormal/Continuing/Continuing.cbs | 59 ++ .../Computations/Abnormal/Continuing/index.md | 98 +++ .../Continuing/tests/handle-continue.config | 16 + .../Abnormal/Controlling/Controlling.cbs | 89 +++ .../Abnormal/Controlling/index.md | 131 ++++ .../Computations/Abnormal/Failing/Failing.cbs | 108 +++ .../Computations/Abnormal/Failing/index.md | 149 ++++ .../Abnormal/Failing/tests/check-true.config | 16 + .../Abnormal/Failing/tests/checked.config | 16 + .../Abnormal/Failing/tests/defined.config | 14 + .../Abnormal/Failing/tests/else-choice.config | 16 + .../Abnormal/Failing/tests/else.config | 19 + .../Abnormal/Returning/Returning.cbs | 60 ++ .../Computations/Abnormal/Returning/index.md | 100 +++ .../Returning/tests/handle-return.config | 16 + .../Abnormal/Throwing/Throwing.cbs | 86 +++ .../Computations/Abnormal/Throwing/index.md | 128 ++++ .../Throwing/tests/catch-else-throw.config | 19 + .../Throwing/tests/handle-recursively.config | 17 + .../Throwing/tests/handle-thrown.config | 17 + .../Computation-Types/Computation-Types.cbs | 13 + .../Computations/Computation-Types/index.md | 47 ++ .../Computations/Normal/Binding/Binding.cbs | 269 +++++++ .../Computations/Normal/Binding/index.md | 320 +++++++++ .../Normal/Binding/tests/accumulate.config | 27 + .../Binding/tests/bind-recursively.config | 16 + .../Normal/Binding/tests/bind-value.config | 9 + .../Binding/tests/bound-directly.config | 15 + .../Normal/Binding/tests/bound-value.config | 15 + .../Normal/Binding/tests/closed.config | 11 + .../Normal/Binding/tests/collateral.config | 27 + .../Normal/Binding/tests/environments.config | 12 + .../Binding/tests/fresh-identifier.config | 10 + .../Normal/Binding/tests/identifiers.config | 14 + .../Binding/tests/initialise-binding.config | 10 + .../Normal/Binding/tests/recursive.config | 17 + .../Normal/Binding/tests/scope.config | 15 + .../Normal/Binding/tests/unbind.config | 9 + .../Computations/Normal/Flowing/Flowing.cbs | 242 +++++++ .../Computations/Normal/Flowing/index.md | 289 ++++++++ .../Normal/Flowing/tests/atomic.config | 27 + .../Normal/Flowing/tests/choice.config | 19 + .../Normal/Flowing/tests/do-while.config | 16 + .../Normal/Flowing/tests/effect.config | 10 + .../Normal/Flowing/tests/if-true-else.config | 12 + .../Normal/Flowing/tests/interleave.config | 18 + .../Normal/Flowing/tests/left-to-right.config | 18 + .../Normal/Flowing/tests/right-to-left.config | 18 + .../Normal/Flowing/tests/sequential.config | 13 + .../Normal/Flowing/tests/while.config | 16 + .../Normal/Generating/Generating.cbs | 58 ++ .../Computations/Normal/Generating/index.md | 97 +++ .../Normal/Generating/tests/fresh-atom.config | 11 + .../Generating/tests/use-atom-not-in.config | 14 + .../Computations/Normal/Giving/Giving.cbs | 212 ++++++ .../Computations/Normal/Giving/index.md | 260 +++++++ .../Normal/Giving/tests/fold-left.config | 15 + .../Normal/Giving/tests/fold-right.config | 15 + .../Normal/Giving/tests/give.config | 18 + .../Giving/tests/interleave-filter.config | 21 + .../Normal/Giving/tests/interleave-map.config | 20 + .../Giving/tests/interleave-repeat.config | 23 + .../Giving/tests/left-to-right-filter.config | 15 + .../Giving/tests/left-to-right-map.config | 18 + .../Giving/tests/left-to-right-repeat.config | 18 + .../Normal/Giving/tests/no-given.config | 16 + .../Normal/Interacting/Interacting.cbs | 59 ++ .../Computations/Normal/Interacting/index.md | 99 +++ .../Normal/Interacting/tests/print-1.config | 12 + .../Normal/Interacting/tests/print-2.config | 14 + .../Normal/Interacting/tests/read-1.config | 12 + .../Normal/Interacting/tests/read-2.config | 12 + .../Normal/Interacting/tests/read-3.config | 12 + .../Computations/Normal/Linking/Linking.cbs | 67 ++ .../Computations/Normal/Linking/index.md | 106 +++ .../Linking/tests/follow-if-link.config | 20 + .../Normal/Linking/tests/follow-link.config | 18 + .../tests/fresh-initialised-link.config | 10 + .../Normal/Linking/tests/fresh-link.config | 10 + .../Linking/tests/initialise-linking.config | 10 + .../Normal/Linking/tests/links.config | 10 + .../Normal/Linking/tests/set-link.config | 17 + .../Computations/Normal/Storing/Storing.cbs | 346 +++++++++ .../Computations/Normal/Storing/index.md | 392 +++++++++++ .../allocate-initialised-variable.config | 12 + .../Storing/tests/allocate-variable.config | 10 + .../Normal/Storing/tests/assign.config | 15 + .../Normal/Storing/tests/assigned.config | 16 + .../Storing/tests/current-value-2.config | 29 + .../Normal/Storing/tests/current-value.config | 14 + .../Storing/tests/initialise-storing.config | 10 + .../Storing/tests/initialise-variable.config | 15 + .../Normal/Storing/tests/locations.config | 10 + .../Storing/tests/recycle-variables-1.config | 13 + .../Storing/tests/recycle-variables-2.config | 13 + .../Storing/tests/recycle-variables-3.config | 15 + .../Normal/Storing/tests/store-clear.config | 13 + .../Normal/Storing/tests/stores.config | 14 + .../Storing/tests/structural-assign-1.config | 15 + .../Storing/tests/structural-assign-2.config | 22 + .../Storing/tests/structural-assign-3.config | 25 + .../tests/structural-assigned-1.config | 12 + .../tests/structural-assigned-2.config | 17 + .../tests/structural-assigned-3.config | 23 + .../tests/structural-assigned-4.config | 24 + .../Normal/Storing/tests/un-assign.config | 18 + .../Funcons-Index/Funcons-Index.cbs | 577 +++++++++++++++ IBAF-cbs/Funcons-beta/Funcons-Index/index.md | 654 ++++++++++++++++++ .../Abstraction/Functions/Functions.cbs | 92 +++ .../Values/Abstraction/Functions/index.md | 135 ++++ .../Abstraction/Functions/tests/apply.config | 16 + .../Functions/tests/compose.config | 20 + .../Abstraction/Functions/tests/curry.config | 17 + .../tests/function-abstraction.config | 27 + .../Functions/tests/function-closure.config | 27 + .../Functions/tests/partial-apply.config | 17 + .../Abstraction/Functions/tests/supply.config | 17 + .../Functions/tests/uncurry.config | 17 + .../Values/Abstraction/Generic/Generic.cbs | 49 ++ .../Values/Abstraction/Generic/index.md | 85 +++ .../Generic/tests/abstraction.config | 25 + .../Abstraction/Generic/tests/closure.config | 25 + .../Values/Abstraction/Patterns/Patterns.cbs | 224 ++++++ .../Values/Abstraction/Patterns/index.md | 267 +++++++ .../Patterns/tests/case-match-loosely.config | 14 + .../Patterns/tests/case-match.config | 14 + .../Patterns/tests/case-variant-value.config | 18 + .../Patterns/tests/match-loosely.config | 36 + .../Abstraction/Patterns/tests/match.config | 35 + .../Patterns/tests/pattern-any.config | 18 + .../Patterns/tests/pattern-bind.config | 19 + .../Patterns/tests/pattern-else.config | 19 + .../Patterns/tests/pattern-type.config | 24 + .../Patterns/tests/pattern-unite.config | 19 + .../Values/Abstraction/Thunks/Thunks.cbs | 30 + .../Values/Abstraction/Thunks/index.md | 68 ++ .../Thunks/tests/thunk-abstraction.config | 25 + .../Thunks/tests/thunk-closure.config | 27 + .../Values/Composite/Bits/Bits.cbs | 110 +++ .../Values/Composite/Bits/index.md | 152 ++++ .../Values/Composite/Classes/Classes.cbs | 86 +++ .../Values/Composite/Classes/index.md | 125 ++++ .../Classes/tests/class-feature-map.config | 120 ++++ .../Classes/tests/class-instantiator.config | 127 ++++ ...name-single-inheritance-feature-map.config | 127 ++++ .../Classes/tests/class-name-tree.config | 129 ++++ .../class-superclass-name-sequence.config | 120 ++++ .../Composite/Classes/tests/class.config | 142 ++++ .../Classes/tests/is-subclass-name.config | 124 ++++ .../Values/Composite/Datatypes/Datatypes.cbs | 41 ++ .../Values/Composite/Datatypes/index.md | 76 ++ .../Values/Composite/Graphs/Graphs.cbs | 33 + .../Values/Composite/Graphs/index.md | 69 ++ .../Values/Composite/Lists/Lists.cbs | 98 +++ .../Values/Composite/Lists/index.md | 132 ++++ .../Values/Composite/Lists/tests/lists.config | 30 + .../Values/Composite/Maps/Maps.cbs | 111 +++ .../Values/Composite/Maps/index.md | 147 ++++ .../Composite/Maps/tests/map-delete.config | 29 + .../Composite/Maps/tests/map-domain.config | 16 + .../Composite/Maps/tests/map-elements.config | 15 + .../Composite/Maps/tests/map-lookup.config | 22 + .../Composite/Maps/tests/map-override.config | 31 + .../Composite/Maps/tests/map-unite.config | 31 + .../Values/Composite/Maps/tests/map.config | 23 + .../Values/Composite/Multisets/Multisets.cbs | 77 +++ .../Values/Composite/Multisets/index.md | 114 +++ .../Values/Composite/Objects/Objects.cbs | 81 +++ .../Values/Composite/Objects/index.md | 119 ++++ .../Objects/tests/object-feature-map.config | 17 + .../Objects/tests/object-identity.config | 17 + ...ject-single-inheritance-feature-map.config | 28 + .../tests/object-subobject-sequence.config | 27 + .../Objects/tests/object-tree.config | 32 + .../Composite/Objects/tests/object.config | 25 + .../Values/Composite/Records/Records.cbs | 32 + .../Values/Composite/Records/index.md | 68 ++ .../Composite/References/References.cbs | 29 + .../Values/Composite/References/index.md | 66 ++ .../Values/Composite/Sequences/Sequences.cbs | 157 +++++ .../Values/Composite/Sequences/index.md | 192 +++++ .../Sequences/tests/drop-first-n.config | 14 + .../Composite/Sequences/tests/first-n.config | 14 + .../Composite/Sequences/tests/first.config | 12 + .../Composite/Sequences/tests/index.config | 21 + .../Sequences/tests/intersperse.config | 14 + .../Composite/Sequences/tests/is-in.config | 18 + .../Composite/Sequences/tests/length.config | 13 + .../Composite/Sequences/tests/n-of.config | 14 + .../Composite/Sequences/tests/reverse.config | 14 + .../Composite/Sequences/tests/second.config | 12 + .../Composite/Sequences/tests/third.config | 12 + .../Values/Composite/Sets/Sets.cbs | 155 +++++ .../Values/Composite/Sets/index.md | 198 ++++++ .../Sets/tests/set-difference.config | 27 + .../Composite/Sets/tests/set-elements.config | 15 + .../Composite/Sets/tests/set-unite.config | 27 + .../Values/Composite/Sets/tests/set.config | 21 + .../Composite/Sets/tests/some-element.config | 15 + .../Values/Composite/Strings/Strings.cbs | 36 + .../Values/Composite/Strings/index.md | 75 ++ .../Values/Composite/Trees/Trees.cbs | 94 +++ .../Values/Composite/Trees/index.md | 130 ++++ .../Trees/tests/forest-branch-sequence.config | 20 + .../tests/forest-root-value-sequence.config | 20 + .../Trees/tests/forest-value-sequence.config | 20 + .../tests/single-branching-sequence.config | 22 + .../Trees/tests/tree-branch-sequence.config | 16 + .../Trees/tests/tree-root-value.config | 16 + .../Values/Composite/Trees/tests/tree.config | 21 + .../Values/Composite/Tuples/Tuples.cbs | 47 ++ .../Values/Composite/Tuples/index.md | 84 +++ .../Composite/Tuples/tests/tuple-zip.config | 18 + .../Values/Composite/Variants/Variants.cbs | 32 + .../Values/Composite/Variants/index.md | 67 ++ .../Values/Composite/Vectors/Vectors.cbs | 21 + .../Values/Composite/Vectors/index.md | 57 ++ .../Composite/Vectors/tests/vector.config | 21 + .../Values/Primitive/Booleans/Booleans.cbs | 87 +++ .../Values/Primitive/Booleans/index.md | 128 ++++ .../Primitive/Booleans/tests/and.config | 20 + .../Booleans/tests/exclusive-or.config | 14 + .../Primitive/Booleans/tests/implies.config | 14 + .../Primitive/Booleans/tests/not.config | 12 + .../Values/Primitive/Booleans/tests/or.config | 17 + .../Primitive/Characters/Characters.cbs | 171 +++++ .../Values/Primitive/Characters/index.md | 225 ++++++ .../Values/Primitive/Floats/Floats.cbs | 230 ++++++ .../Values/Primitive/Floats/index.md | 262 +++++++ .../Values/Primitive/Integers/Integers.cbs | 230 ++++++ .../Values/Primitive/Integers/index.md | 263 +++++++ .../Values/Primitive/Null/Null.cbs | 15 + .../Values/Primitive/Null/index.md | 52 ++ .../Values/Value-Types/Value-Types.cbs | 216 ++++++ .../Funcons-beta/Values/Value-Types/index.md | 258 +++++++ .../Value-Types/tests/cast-to-type.config | 14 + .../Values/Value-Types/tests/is-equal.config | 17 + .../Value-Types/tests/is-in-type.config | 30 + .../Values/Value-Types/tests/is-value.config | 12 + .../Values/Value-Types/tests/when-true.config | 12 + IBAF-cbs/Funcons-beta/cbs.css | 244 +++++++ 250 files changed, 15552 insertions(+), 1 deletion(-) delete mode 120000 IBAF-cbs/Funcons-beta create mode 100644 IBAF-cbs/Funcons-beta/.gitignore create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/Abrupting.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/tests/finally.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/tests/handle-abrupt.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Breaking/Breaking.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Breaking/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Breaking/tests/handle-break.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Continuing/Continuing.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Continuing/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Continuing/tests/handle-continue.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Controlling/Controlling.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Controlling/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/Failing.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/check-true.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/checked.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/defined.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else-choice.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/Returning.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/tests/handle-return.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/Throwing.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/catch-else-throw.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-recursively.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-thrown.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Computation-Types/Computation-Types.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Computation-Types/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/Binding.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/accumulate.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-recursively.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-value.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-directly.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-value.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/closed.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/collateral.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/environments.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/fresh-identifier.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/identifiers.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/initialise-binding.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/recursive.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/scope.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/unbind.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/Flowing.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/atomic.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/choice.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/do-while.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/effect.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/if-true-else.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/interleave.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/left-to-right.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/right-to-left.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/sequential.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/tests/while.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Generating/Generating.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Generating/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Generating/tests/fresh-atom.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Generating/tests/use-atom-not-in.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/Giving.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/fold-left.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/fold-right.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/give.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/interleave-filter.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/interleave-map.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/interleave-repeat.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/left-to-right-filter.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/left-to-right-map.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/left-to-right-repeat.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Giving/tests/no-given.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/Interacting.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/tests/print-1.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/tests/print-2.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/tests/read-1.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/tests/read-2.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Interacting/tests/read-3.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/Linking.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/follow-if-link.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/follow-link.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/fresh-initialised-link.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/fresh-link.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/initialise-linking.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/links.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Linking/tests/set-link.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/Storing.cbs create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/index.md create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/allocate-initialised-variable.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/allocate-variable.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/assign.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/assigned.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/current-value-2.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/current-value.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/initialise-storing.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/initialise-variable.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/locations.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/recycle-variables-1.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/recycle-variables-2.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/recycle-variables-3.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/store-clear.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/stores.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assign-1.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assign-2.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assign-3.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assigned-1.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assigned-2.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assigned-3.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/structural-assigned-4.config create mode 100644 IBAF-cbs/Funcons-beta/Computations/Normal/Storing/tests/un-assign.config create mode 100644 IBAF-cbs/Funcons-beta/Funcons-Index/Funcons-Index.cbs create mode 100644 IBAF-cbs/Funcons-beta/Funcons-Index/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/Functions.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/apply.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/compose.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/curry.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-abstraction.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-closure.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/partial-apply.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/supply.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/uncurry.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/Generic.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/tests/abstraction.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/tests/closure.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/Patterns.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/case-match-loosely.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/case-match.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/case-variant-value.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/match-loosely.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/match.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/pattern-any.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/pattern-bind.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/pattern-else.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/pattern-type.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Patterns/tests/pattern-unite.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Thunks/Thunks.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Thunks/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Thunks/tests/thunk-abstraction.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Abstraction/Thunks/tests/thunk-closure.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Bits/Bits.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Bits/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/Classes.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/class-feature-map.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/class-instantiator.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/class-name-single-inheritance-feature-map.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/class-name-tree.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/class-superclass-name-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/class.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Classes/tests/is-subclass-name.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Datatypes/Datatypes.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Datatypes/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Graphs/Graphs.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Graphs/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Lists/Lists.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Lists/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Lists/tests/lists.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/Maps.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map-delete.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map-domain.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map-elements.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map-lookup.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map-override.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map-unite.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Maps/tests/map.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Multisets/Multisets.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Multisets/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/Objects.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/tests/object-feature-map.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/tests/object-identity.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/tests/object-single-inheritance-feature-map.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/tests/object-subobject-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/tests/object-tree.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Objects/tests/object.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Records/Records.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Records/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/References/References.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/References/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/Sequences.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/drop-first-n.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/first-n.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/first.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/index.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/intersperse.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/is-in.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/length.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/n-of.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/reverse.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/second.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sequences/tests/third.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/Sets.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-difference.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-elements.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-unite.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/some-element.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Strings/Strings.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Strings/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/Trees.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/forest-branch-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/forest-root-value-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/forest-value-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/single-branching-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/tree-branch-sequence.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/tree-root-value.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Trees/tests/tree.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Tuples/Tuples.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Tuples/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Tuples/tests/tuple-zip.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Variants/Variants.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Variants/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Vectors/Vectors.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Vectors/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Composite/Vectors/tests/vector.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/Booleans.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/tests/and.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/tests/exclusive-or.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/tests/implies.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/tests/not.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Booleans/tests/or.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Characters/Characters.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Characters/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Floats/Floats.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Floats/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Integers/Integers.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Integers/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Null/Null.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Primitive/Null/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/Value-Types.cbs create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/index.md create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/tests/cast-to-type.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/tests/is-equal.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/tests/is-in-type.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/tests/is-value.config create mode 100644 IBAF-cbs/Funcons-beta/Values/Value-Types/tests/when-true.config create mode 100644 IBAF-cbs/Funcons-beta/cbs.css diff --git a/IBAF-cbs/Funcons-beta b/IBAF-cbs/Funcons-beta deleted file mode 120000 index 02b90f3..0000000 --- a/IBAF-cbs/Funcons-beta +++ /dev/null @@ -1 +0,0 @@ -/home/peter/cbs-all/CBS-beta/Funcons-beta \ No newline at end of file diff --git a/IBAF-cbs/Funcons-beta/.gitignore b/IBAF-cbs/Funcons-beta/.gitignore new file mode 100644 index 0000000..292720e --- /dev/null +++ b/IBAF-cbs/Funcons-beta/.gitignore @@ -0,0 +1,5 @@ +/.cache +/target + +/.project +/.settings diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/Abrupting.cbs b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/Abrupting.cbs new file mode 100644 index 0000000..fc166c0 --- /dev/null +++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/Abrupting.cbs @@ -0,0 +1,91 @@ +### Abruptly terminating + +[ + Funcon stuck + Entity abrupted + Funcon finalise-abrupting + Funcon abrupt + Funcon handle-abrupt + Funcon finally +] + + +Meta-variables + T, T', T'' <: values + + +Funcon + stuck : =>empty-type +/* + `stuck` does not have any computation. It is used to represent the result of + a transition that causes the computation to terminate abruptly. +*/ + + +Entity + _ --abrupted(_:values?)-> _ +/* + `abrupted(V)` in a label on a tranistion indicates abrupt termination for + reason `V`. `abrupted( )` indicates the absence of abrupt termination. +*/ + + +Funcon + finalise-abrupting(X:=>T) : =>T|null-type + ~> handle-abrupt(X, null-value) +/* + `finalise-abrupting(X)` handles abrupt termination of `X` for any reason. +*/ + + +Funcon + abrupt(_:values) :=>empty-type +/* + `abrupt(V)` terminates abruptly for reason `V`. +*/ +Rule + abrupt(V:values) --abrupted(V)-> stuck + + +Funcon + handle-abrupt(_:T'=>T, _:T''=>T) : T'=>T +/* + `handle-abrupt(X, Y)` first evaluates `X`. If `X` terminates normally with + value `V`, then `V` is returned and `Y` is ignored. If `X` terminates abruptly + for reason `V`, then `Y` is executed with `V` as `given` value. + + `handle-abrupt(X, Y)` is associative, with `abrupt(given)` as left and right + unit. `handle-abrupt(X, else(Y, abrupt(given)))` ensures propagation of + abrupt termination for the given reason if `Y` fails +*/ +Rule + X --abrupted( )-> X' + -------------------------------------------------------- + handle-abrupt(X, Y) --abrupted( )-> handle-abrupt(X', Y) +Rule + X --abrupted(V:T'')-> X' + ---------------------------------------------- + handle-abrupt(X, Y) --abrupted( )-> give(V, Y) +Rule + handle-abrupt(V:T, Y) ~> V + + +Funcon + finally(_:=>T, _:=>null-type) : =>T +/* + `finally(X, Y)` first executes `X`. If `X` terminates normally with + value `V`, then `Y` is executed before terminating normally with value `V`. + If `X` terminates abruptly for reason `V`, then `Y` is executed before + terminating abruptly with the same reason `V`. +*/ +Rule + X --abrupted( )-> X' + -------------------------------------------- + finally(X, Y) --abrupted( )-> finally(X', Y) +Rule + X --abrupted(V:values)-> X' + ----------------------------------------------------- + finally(X, Y) --abrupted()-> sequential(Y, abrupt(V)) +Rule + finally(V:T, Y) ~> sequential(Y,V) + \ No newline at end of file diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/index.md b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/index.md new file mode 100644 index 0000000..bf645d2 --- /dev/null +++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Abrupting/index.md @@ -0,0 +1,131 @@ +--- +layout: default +title: "Abrupting" +parent: Abnormal +ancestor: Funcons-beta + +--- + +[Funcons-beta] : [Abrupting.cbs] +----------------------------- + +### Abruptly terminating + +
[
+ Funcon stuck
+ Entity abrupted
+ Funcon finalise-abrupting
+ Funcon abrupt
+ Funcon handle-abrupt
+ Funcon finally
+]Meta-variables
+ T, T′, T′′ <: valuesFuncon
+ stuck : =>empty-typestuck does not have any computation. It is used to represent the result of
+ a transition that causes the computation to terminate abruptly.
+
+
+
+Entity
+ _ --abrupted(_:values?)-> _abrupted(V) in a label on a tranistion indicates abrupt termination for
+ reason V. abrupted( ) indicates the absence of abrupt termination.
+
+
+
+Funcon
+ finalise-abrupting(X:=>T) : =>T|null-type
+ ~> handle-abrupt(X, null-value)finalise-abrupting(X) handles abrupt termination of X for any reason.
+
+
+
+Funcon
+ abrupt(_:values) :=>empty-typeabrupt(V) terminates abruptly for reason V.
+
+
+
+
+
+Funcon
+ handle-abrupt(_:T′=>T, _:T′′=>T) : T′=>Thandle-abrupt(X, Y) first evaluates X. If X terminates normally with
+ value V, then V is returned and Y is ignored. If X terminates abruptly
+ for reason V, then Y is executed with V as given value.
+
+ handle-abrupt(X, Y) is associative, with abrupt(given) as left and right
+ unit. handle-abrupt(X, else(Y, abrupt(given))) ensures propagation of
+ abrupt termination for the given reason if Y fails
+
+Rule
+ X --abrupted( )-> X′
+ --------------------------------------------------------
+ handle-abrupt(X, Y) --abrupted( )-> handle-abrupt(X′, Y)
+Rule
+ X --abrupted(V:T′′)-> X′
+ ----------------------------------------------
+ handle-abrupt(X, Y) --abrupted( )-> give(V, Y)
+Rule
+ handle-abrupt(V:T, Y) ~> VFuncon
+ finally(_:=>T, _:=>null-type) : =>Tfinally(X, Y) first executes X. If X terminates normally with
+ value V, then Y is executed before terminating normally with value V.
+ If X terminates abruptly for reason V, then Y is executed before
+ terminating abruptly with the same reason V.
+
+Rule
+ X --abrupted( )-> X′
+ --------------------------------------------
+ finally(X, Y) --abrupted( )-> finally(X′, Y)
+Rule
+ X --abrupted(V:values)-> X′
+ -----------------------------------------------------
+ finally(X, Y) --abrupted()-> sequential(Y, abrupt(V))
+Rule
+ finally(V:T, Y) ~> sequential(Y,V)[
+ Datatype breaking
+ Funcon broken
+ Funcon finalise-breaking
+ Funcon break
+ Funcon handle-break
+]Meta-variables
+ T <: valuesDatatype
+ breaking ::= brokenbroken is a reason for abrupt termination.
+
+
+
+Funcon
+ finalise-breaking(X:=>T) : =>T|null-type
+ ~> finalise-abrupting(X)finalise-breaking(X) handles abrupt termination of X due to executing
+ break.
+
+
+
+Funcon
+ break : =>empty-type
+ ~> abrupt(broken)break abruptly terminates all enclosing computations until it is handled.
+
+
+
+
+
+ handle-break(X) terminates normally when X terminates abruptly for the
+ reason broken.
+
+Rule
+ X --abrupted( )-> X′
+ ------------------------------------------------
+ handle-break(X) --abrupted( )-> handle-break(X′)
+Rule
+ X --abrupted(broken)-> _
+ ---------------------------------------
+ handle-break(X) --abrupted( )-> null-value
+Rule
+ X --abrupted(V:~breaking)-> X′
+ ------------------------------------------------
+ handle-break(X) --abrupted(V)-> handle-break(X′)
+Rule
+ handle-break(null-value) ~> null-value[
+ Datatype continuing
+ Funcon continued
+ Funcon finalise-continuing
+ Funcon continue
+ Funcon handle-continue
+]Meta-variables
+ T <: valuesDatatype
+ continuing ::= continuedcontinued is a reason for abrupt termination.
+
+
+
+Funcon
+ finalise-continuing(X:=>T) : =>T|null-type
+ ~> finalise-abrupting(X)finalise-continuing(X) handles abrupt termination of X due to executing
+ continue.
+
+
+
+Funcon
+ continue : =>empty-type
+ ~> abrupt(continued)continue abruptly terminates all enclosing computations until it is handled.
+
+
+
+
+
+ handle-continue(X) terminates normally when X terminates abruptly for the
+ reason continued.
+
+Rule
+ X --abrupted( )-> X′
+ ------------------------------------------------------
+ handle-continue(X) --abrupted( )-> handle-continue(X′)
+Rule
+ X --abrupted(continued)-> _
+ --------------------------------------------
+ handle-continue(X) --abrupted( )-> null-value
+Rule
+ X --abrupted(V:~continuing)-> X′
+ ------------------------------------------------------
+ handle-continue(X) --abrupted(V)-> handle-continue(X′)
+Rule
+ handle-continue(null-value) ~> null-value[
+ Datatype continuations
+ Funcon continuation
+ Entity plug-signal
+ Funcon hole
+ Funcon resume-continuation
+ Entity control-signal
+ Funcon control
+ Funcon delimit-current-continuation Alias delimit-cc
+]Meta-variables
+ T, T1, T2 <: valuesDatatype
+ continuations(T1,T2) ::= continuation(_:abstractions(()=>T2))continuations(T1, T2) consists of abstractions whose bodies contain a hole,
+ and which will normally compute a value of type T2 when the hole is plugged
+ with a value of type T1.
+
+
+Entity
+ _ --plug-signal(V?:values?)-> _hole in a continuation,
+ thereby allowing a continuation to resume.
+
+
+ Funcon
+ hole : =>valueshole in a term cannot proceed until it receives a plug-signal
+ containing a value to plug the hole.
+
+Rule
+ hole --plug-signal(V)-> VFuncon
+ resume-continuation(K:continuations(T1, T2), V:T1) : =>T2resume-continuation(K, V) resumes a continuation K by plugging the value
+ V into the hole in the continuation.
+
+Rule
+ X --plug-signal(V)-> X′
+ ---------------------------------------------------------------------------
+ resume-continuation(continuation(abstraction(X)), V:T) --plug-signal()-> X′Entity
+ _ --control-signal(F?:(functions(continuations(T1, T2), T2))?)-> _delimit-current-continuation(X).
+
+
+Funcon
+ control(F:functions(continuations(T1, T2), T2)) : =>T1control(F) emits a control-signal that, when handled by an enclosing
+ delimit-current-continuation(X), will apply F to the current continuation of
+ control(F), (rather than proceeding with that current continuation).
+
+Rule
+ control(F:functions(_,_)) --control-signal(F)-> holeFuncon
+ delimit-current-continuation(X:=>T) : =>T
+Alias
+ delimit-cc = delimit-current-continuationdelimit-current-continuation(X) delimits the scope of captured continuations.
+
+Rule
+ delimit-current-continuation(V:T) ~> V
+Rule
+ X --control-signal( )-> X′
+ -----------------------------------------------------
+ delimit-current-continuation(X) --control-signal( )->
+ delimit-current-continuation(X′)
+Rule
+ X --control-signal(F)-> X′
+ ------------------------------------------------------------------
+ delimit-current-continuation(X) --control-signal( )->
+ delimit-current-continuation(apply(F, continuation closure(X′)))[
+ Datatype failing
+ Funcon failed
+ Funcon finalise-failing
+ Funcon fail
+ Funcon else
+ Funcon else-choice
+ Funcon checked
+ Funcon check-true
+]Meta-variables
+ T <: valuesDatatype
+ failing ::= failedfailed is a reason for abrupt termination.
+
+
+
+Funcon
+ finalise-failing(X:=>T) : =>T|null-type
+ ~> finalise-abrupting(X)finalise-failing(X) handles abrupt termination of X due to executing fail.
+
+
+
+Funcon
+ fail : =>empty-type
+ ~> abrupt(failed)fail abruptly terminates all enclosing computations until it is handled.
+
+
+
+Funcon
+ else(_:=>T, _:(=>T)+) : =>Telse(X1, X2, ...) executes the arguments in turn until either some
+ Xi does *not* fail, or all arguments Xi have been executed.
+ The last argument executed determines the result.
+ else(X, Y) is associative, with unit fail.
+
+Rule
+ X --abrupted( )-> X′
+ --------------------------------------
+ else(X, Y) --abrupted( )-> else(X′, Y)
+Rule
+ X --abrupted(failed)-> _
+ ---------------------------------
+ else(X, Y) --abrupted( )-> Y
+Rule
+ X --abrupted(V:~failing)-> X′
+ --------------------------------------
+ else(X, Y) --abrupted(V)-> else(X′, Y)
+Rule
+ else(V:T, Y) ~> V
+Rule
+ else(X, Y, Z+) ~> else(X, else(Y, Z+))Funcon
+ else-choice(_:(=>T)+) : =>Telse-choice(X,...) executes the arguments in any order until either some
+ Xi does *not* fail, or all arguments Xi have been executed.
+ The last argument executed determines the result.
+ else(X, Y) is associative and commutative, with unit fail.
+
+Rule
+ else-choice(W*, X, Y, Z*)
+ ~> choice(else(X, else-choice(W*, Y, Z*),
+ else(Y, else-choice(W*, X, Z*))))
+Rule
+ else-choice(X) ~> XFuncon
+ check-true(_:booleans) : =>null-type
+Alias
+ check = check-truecheck-true(X) terminates normally if the value computed by X is true,
+ and fails if it is false.
+
+Rule
+ check-true(true) ~> null-value
+Rule
+ check-true(false) ~> failFuncon
+ checked(_:(T)?) : =>Tchecked(X) fails when X gives the empty sequence of values ( ),
+ representing that an optional value has not been computed. It otherwise
+ computes the same as X.
+
+
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Failing.cbs]: Failing.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Computations/Abnormal/Failing/Failing.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/check-true.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/check-true.config
new file mode 100644
index 0000000..9644185
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/check-true.config
@@ -0,0 +1,16 @@
+general {
+ funcon-term:
+ finalise-failing
+ sequential(
+ check-true(true), print 1,
+ else(check-true(false), print 2),
+ check-true(not false), print 3,
+ print sequential(check-true(true),4)
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, 4];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/checked.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/checked.config
new file mode 100644
index 0000000..27819bc
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/checked.config
@@ -0,0 +1,16 @@
+general {
+ funcon-term:
+ finalise-failing
+ sequential(
+ effect(checked(true)), print 1,
+ else(effect(checked()), print 2),
+ else(effect(checked(map-lookup(map(),1))), print 3),
+ print(checked(map-lookup(map(tuple(0,1),tuple(1,4)),1)))
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, 4];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/defined.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/defined.config
new file mode 100644
index 0000000..fdc1584
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/defined.config
@@ -0,0 +1,14 @@
+general {
+ funcon-term:
+ finalise-failing
+ sequential(
+ effect(checked(42)), print 1,
+ else(checked(sequential(print(2),lookup(map-empty,"x"))), print 3)
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else-choice.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else-choice.config
new file mode 100644
index 0000000..1d3c541
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else-choice.config
@@ -0,0 +1,16 @@
+general {
+ funcon-term:
+ finalise-failing finalise-abrupting
+ sequential(
+ else-choice(print 1),
+ else-choice(fail, fail, fail, print 2, fail, print 3)
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2];
+// Also possible:
+// standard-out: [1, 3];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else.config
new file mode 100644
index 0000000..0407a80
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Failing/tests/else.config
@@ -0,0 +1,19 @@
+general {
+ funcon-term:
+ finalise-failing finalise-abrupting
+ sequential(
+ else(fail, print 1),
+ print else(2, fail),
+ else(print 3, fail),
+ handle-abrupt(
+ else(abrupt(true), print 99),
+ print 4),
+ else(fail, fail, print 5)
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, 4, 5];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/Returning.cbs b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/Returning.cbs
new file mode 100644
index 0000000..7835b90
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/Returning.cbs
@@ -0,0 +1,60 @@
+### Returning
+
+[
+ Datatype returning
+ Funcon returned
+ Funcon finalise-returning
+ Funcon return
+ Funcon handle-return
+]
+
+
+Meta-variables
+ T <: values
+
+
+Datatype
+ returning ::= returned(_:values)
+/*
+ `returned(V?)` is a reason for abrupt termination.
+*/
+
+
+Funcon
+ finalise-returning(X:=>T) : =>T|null-type
+ ~> finalise-abrupting(X)
+/*
+ `finalise-returning(X)` handles abrupt termination of `X` due to
+ executing `return(V)`.
+*/
+
+
+Funcon
+ return(V:T) : =>empty-type
+ ~> abrupt(returned(V))
+/*
+ `return(V)` abruptly terminates all enclosing computations until it is
+ handled, then giving `V`. Note that `V` may be `null-value`.
+*/
+
+
+Funcon
+ handle-return(_:=>T) : =>T
+/*
+ `handle-return(X)` first evaluates `X`. If `X` either terminates abruptly for
+ reason `returned(V)`, or terminates normally with value `V`, it gives `V`.
+*/
+Rule
+ X --abrupted( )-> X'
+ --------------------------------------------------
+ handle-return(X) --abrupted( )-> handle-return(X')
+Rule
+ X --abrupted(returned(V:values))-> X'
+ ----------------------------------------------
+ handle-return(X) --abrupted( )-> V
+Rule
+ X --abrupted(V':~returning)-> X'
+ ---------------------------------------------------
+ handle-return(X) --abrupted(V')-> handle-return(X')
+Rule
+ handle-return(V:T) ~> V
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/index.md b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/index.md
new file mode 100644
index 0000000..b1dd016
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Returning/index.md
@@ -0,0 +1,100 @@
+---
+layout: default
+title: "Returning"
+parent: Abnormal
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Returning.cbs]
+-----------------------------
+
+### Returning
+
+[
+ Datatype returning
+ Funcon returned
+ Funcon finalise-returning
+ Funcon return
+ Funcon handle-return
+]Meta-variables
+ T <: valuesDatatype
+ returning ::= returned(_:values)returned(V?) is a reason for abrupt termination.
+
+
+
+Funcon
+ finalise-returning(X:=>T) : =>T|null-type
+ ~> finalise-abrupting(X)finalise-returning(X) handles abrupt termination of X due to
+ executing return(V).
+
+
+
+Funcon
+ return(V:T) : =>empty-type
+ ~> abrupt(returned(V))return(V) abruptly terminates all enclosing computations until it is
+ handled, then giving V. Note that V may be null-value.
+
+
+
+Funcon
+ handle-return(_:=>T) : =>Thandle-return(X) first evaluates X. If X either terminates abruptly for
+ reason returned(V), or terminates normally with value V, it gives V.
+
+Rule
+ X --abrupted( )-> X′
+ --------------------------------------------------
+ handle-return(X) --abrupted( )-> handle-return(X′)
+Rule
+ X --abrupted(returned(V:values))-> X′
+ ----------------------------------------------
+ handle-return(X) --abrupted( )-> V
+Rule
+ X --abrupted(V′:~returning)-> X′
+ ---------------------------------------------------
+ handle-return(X) --abrupted(V′)-> handle-return(X′)
+Rule
+ handle-return(V:T) ~> V[
+ Datatype throwing
+ Funcon thrown
+ Funcon finalise-throwing
+ Funcon throw
+ Funcon handle-thrown
+ Funcon handle-recursively
+ Funcon catch-else-throw
+]Meta-variables
+ R, S, T, T′, T′′ <: valuesDatatype
+ throwing ::= thrown(_:values)thrown(V) is a reason for abrupt termination.
+
+
+
+Funcon
+ finalise-throwing(X:=>T) : =>T|null-type
+ ~> finalise-abrupting(X)finalise-throwing(X) handles abrupt termination of X due to
+ executing throw(V).
+
+
+
+Funcon
+ throw(V:T) : =>empty-type
+ ~> abrupt(thrown(V))throw(V) abruptly terminates all enclosing computations uTil it is handled.
+
+
+
+Funcon
+ handle-thrown(_:T′=>T, _:T′′=>T) : T′=>Thandle-thrown(X, Y) first evaluates X. If X terminates normally with
+ value V, then V is returned and Y is ignored. If X terminates abruptly
+ with a thrown eTity having value V, then Y is executed with V as
+ given value.
+
+ handle-thrown(X, Y) is associative, with throw(given) as unit.
+ handle-thrown(X, else(Y, throw(given))) ensures that if Y fails, the
+ thrown value is re-thrown.
+
+Rule
+ X --abrupted( )-> X′
+ --------------------------------------------------------
+ handle-thrown(X, Y) --abrupted( )-> handle-thrown(X′, Y)
+Rule
+ X --abrupted(thrown(V′′:values))-> X′
+ ----------------------------------------------
+ handle-thrown(X, Y) --abrupted( )-> give(V′′, Y)
+Rule
+ X --abrupted(V′:~throwing)-> X′
+ ---------------------------------------------------------
+ handle-thrown(X, Y) --abrupted(V′)-> handle-thrown(X′, Y)
+Rule
+ handle-thrown(V:T, Y) ~> VFuncon
+ handle-recursively(X:S=>T, Y:R=>T) : S=>T
+ ~> handle-thrown(X, else(handle-recursively(Y, Y), throw(given)))handle-recursively(X, Y) behaves similarly to handle-thrown(X, Y), except
+ that another copy of the handler attempts to handle any values thrown by Y.
+ Thus, many thrown values may get handled by the same handler.
+
+
+
+
+
+
+ handle-thrown(X, catch-else-throw(P, Y)) handles those values thrown by X
+ that match pattern P. Other thrown values are re-thrown.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Throwing.cbs]: Throwing.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Computations/Abnormal/Throwing/Throwing.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/catch-else-throw.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/catch-else-throw.config
new file mode 100644
index 0000000..0a77e42
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/catch-else-throw.config
@@ -0,0 +1,19 @@
+general {
+ funcon-term:
+ initialise-binding
+ finalise-throwing
+ sequential(
+ handle-thrown(
+ throw 1,
+ catch-else-throw(1, print 1)),
+ handle-thrown(
+ handle-thrown(throw 2,
+ catch-else-throw(1, fail)),
+ catch-else-throw(2, print 2)))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-recursively.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-recursively.config
new file mode 100644
index 0000000..71bd0dd
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-recursively.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ finalise-throwing
+ handle-recursively(
+ throw 1,
+ if-true-else(
+ is-less(given,4),
+ sequential(print given, throw integer-add(1,given)),
+ print"OK")
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, "OK"];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-thrown.config b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-thrown.config
new file mode 100644
index 0000000..547d41e
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Abnormal/Throwing/tests/handle-thrown.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ finalise-throwing
+ sequential(
+ print handle-thrown(1, fail),
+ handle-thrown(print 2, fail),
+ handle-thrown(
+ sequential(print 3, throw(sequential(print 4, 5))),
+ print given)
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, 4, 5];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Computation-Types/Computation-Types.cbs b/IBAF-cbs/Funcons-beta/Computations/Computation-Types/Computation-Types.cbs
new file mode 100644
index 0000000..1f6ef95
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Computation-Types/Computation-Types.cbs
@@ -0,0 +1,13 @@
+## Computation Types
+
+Built-in Funcon
+ computation-types : types
+/*
+ For any value type `T`, the term `=>T` is the type of computations that
+ compute values of type `T` whenever they terminate normally.
+
+ For any subtypes `S`, `T` of `values`, `S=>T` is the type of computations
+ that compute values of type `T` whenever they terminate normally, and
+ either do not refer at all to the `given` entity, or require the `given`
+ entity to have type `S`.
+*/
diff --git a/IBAF-cbs/Funcons-beta/Computations/Computation-Types/index.md b/IBAF-cbs/Funcons-beta/Computations/Computation-Types/index.md
new file mode 100644
index 0000000..7531018
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Computation-Types/index.md
@@ -0,0 +1,47 @@
+---
+layout: default
+title: "Computation-Types"
+parent: Computations
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Computation-Types.cbs]
+-----------------------------
+
+## Computation Types
+
+Built-in Funcon
+ computation-types : typesT, the term =>T is the type of computations that
+ compute values of type T whenever they terminate normally.
+
+ For any subtypes S, T of values, S=>T is the type of computations
+ that compute values of type T whenever they terminate normally, and
+ either do not refer at all to the given entity, or require the given
+ entity to have type S.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Computation-Types.cbs]: Computation-Types.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Computations/Computation-Types/Computation-Types.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/Binding.cbs b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/Binding.cbs
new file mode 100644
index 0000000..967d5cb
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/Binding.cbs
@@ -0,0 +1,269 @@
+### Binding
+
+[
+ Type environments Alias envs
+ Datatype identifiers Alias ids
+ Funcon identifier-tagged Alias id-tagged
+ Funcon fresh-identifier
+ Entity environment Alias env
+ Funcon initialise-binding
+ Funcon bind-value Alias bind
+ Funcon unbind
+ Funcon bound-directly
+ Funcon bound-value Alias bound
+ Funcon closed
+ Funcon scope
+ Funcon accumulate
+ Funcon collateral
+ Funcon bind-recursively
+ Funcon recursive
+]
+
+
+Meta-variables
+ T <: values
+
+
+#### Environments
+
+Type
+ environments ~> maps(identifiers, values?)
+Alias
+ envs = environments
+/*
+ An environment represents bindings of identifiers to values.
+ Mapping an identifier to `( )` represents that its binding is hidden.
+
+ Circularity in environments (due to recursive bindings) is represented using
+ bindings to cut-points called `links`. Funcons are provided for making
+ declarations recursive and for referring to bound values without explicit
+ mention of links, so their existence can generally be ignored.
+*/
+
+
+Datatype
+ identifiers ::= {_:strings} | identifier-tagged(_:identifiers, _:values)
+Alias
+ ids = identifiers
+Alias
+ id-tagged = identifier-tagged
+/*
+ An identifier is either a string of characters, or an identifier tagged with
+ some value (e.g., with the identifier of a namespace).
+*/
+
+
+Funcon
+ fresh-identifier : =>identifiers
+/*
+ `fresh-identifier` computes an identifier distinct from all previously
+ computed identifiers.
+*/
+Rule
+ fresh-identifier ~> identifier-tagged("generated", fresh-atom)
+
+
+#### Current bindings
+
+Entity
+ environment(_:environments) |- _ ---> _
+Alias
+ env = environment
+/*
+ The environment entity allows a computation to refer to the current bindings
+ of identifiers to values.
+*/
+
+
+Funcon
+ initialise-binding(X:=>T) : =>T
+ ~> initialise-linking(initialise-generating(closed(X)))
+/*
+ `initialise-binding(X)` ensures that `X` does not depend on non-local bindings.
+ It also ensures that the linking entity (used to represent potentially cyclic
+ bindings) and the generating entity (for creating fresh identifiers) are
+ initialised.
+*/
+
+
+Funcon
+ bind-value(I:identifiers, V:values) : =>environments
+ ~> { I |-> V }
+Alias
+ bind = bind-value
+/*
+ `bind-value(I, X)` computes the environment that binds only `I` to the value
+ computed by `X`.
+*/
+
+
+Funcon
+ unbind(I:identifiers) : =>environments
+ ~> { I |-> ( ) }
+/*
+ `unbind(I)` computes the environment that hides the binding of `I`.
+*/
+
+
+Funcon
+ bound-directly(_:identifiers) : =>values
+/*
+ `bound-directly(I)` returns the value to which `I` is currently bound, if any,
+ and otherwise fails.
+
+ `bound-directly(I)` does *not* follow links. It is used only in connection with
+ recursively-bound values when references are not encapsulated in abstractions.
+*/
+Rule
+ lookup(Rho, I) ~> (V:values)
+ --------------------------------------------------------
+ environment(Rho) |- bound-directly(I:identifiers) ---> V
+Rule
+ lookup(Rho, I) ~> ( )
+ -----------------------------------------------------------
+ environment(Rho) |- bound-directly(I:identifiers) ---> fail
+
+
+Funcon
+ bound-value(I:identifiers) : =>values
+ ~> follow-if-link(bound-directly(I))
+Alias
+ bound = bound-value
+/*
+ `bound-value(I)` inspects the value to which `I` is currently bound, if any,
+ and otherwise fails. If the value is a link, `bound-value(I)` returns the
+ value obtained by following the link, if any, and otherwise fails. If the
+ inspected value is not a link, `bound-value(I)` returns it.
+
+ `bound-value(I)` is used for references to non-recursive bindings and to
+ recursively-bound values when references are encapsulated in abstractions.
+*/
+
+
+#### Scope
+
+Funcon
+ closed(X:=>T) : =>T
+/*
+ `closed(X)` ensures that `X` does not depend on non-local bindings.
+*/
+Rule
+ environment(map( )) |- X ---> X'
+ -------------------------------------------
+ environment(_) |- closed(X) ---> closed(X')
+Rule
+ closed(V:T) ~> V
+
+
+Funcon
+ scope(_:environments, _:=>T) : =>T
+/*
+ `scope(D,X)` executes `D` with the current bindings, to compute an environment
+ `Rho` representing local bindings. It then executes `X` to compute the result,
+ with the current bindings extended by `Rho`, which may shadow or hide previous
+ bindings.
+
+ `closed(scope(Rho, X))` ensures that `X` can reference only the bindings
+ provided by `Rho`.
+*/
+Rule
+ environment(map-override(Rho1, Rho0)) |- X ---> X'
+ ---------------------------------------------------------------------
+ environment(Rho0) |- scope(Rho1:environments, X) ---> scope(Rho1, X')
+Rule
+ scope(_:environments, V:T) ~> V
+
+
+Funcon
+ accumulate(_:(=>environments)*) : =>environments
+/*
+ `accumulate(D1, D2)` executes `D1` with the current bindings, to compute an
+ environment `Rho1` representing some local bindings. It then executes `D2` to
+ compute an environment `Rho2` representing further local bindings, with the
+ current bindings extended by `Rho1`, which may shadow or hide previous
+ current bindings. The result is `Rho1` extended by `Rho2`, which may shadow
+ or hide the bindings of `Rho1`.
+
+ `accumulate(_, _)` is associative, with `map( )` as unit, and extends to any
+ number of arguments.
+*/
+Rule
+ D1 ---> D1'
+ -------------------------------------------
+ accumulate(D1, D2) ---> accumulate(D1', D2)
+Rule
+ accumulate(Rho1:environments, D2) ~> scope(Rho1, map-override(D2, Rho1))
+Rule
+ accumulate( ) ~> map( )
+Rule
+ accumulate(D1) ~> D1
+Rule
+ accumulate(D1, D2, D+) ~> accumulate(D1, accumulate(D2, D+))
+
+
+Funcon
+ collateral(Rho*:environments*) : =>environments
+ ~> checked map-unite(Rho*)
+/*
+ `collateral(D1, ...)` pre-evaluates its arguments with the current bindings,
+ and unites the resulting maps, which fails if the domains are not pairwise
+ disjoint.
+
+ `collateral(D1, D2)` is associative and commutative with `map( )` as unit,
+ and extends to any number of arguments.
+*/
+
+
+#### Recurse
+
+Funcon
+ bind-recursively(I:identifiers, E:=>values) : =>environments
+ ~> recursive({I}, bind-value(I, E))
+/*
+ `bind-recursively(I, E)` binds `I` to a link that refers to the value of `E`,
+ representing a recursive binding of `I` to the value of `E`.
+ Since `bound-value(I)` follows links, it should not be executed during the
+ evaluation of `E`.
+*/
+
+
+Funcon
+ recursive(SI:sets(identifiers), D:=>environments) : =>environments
+ ~> re-close(bind-to-forward-links(SI), D)
+/*
+ `recursive(SI, D)` executes `D` with potential recursion on the bindings of
+ the identifiers in the set `SI` (which need not be the same as the set of
+ identifiers bound by `D`).
+*/
+
+
+Auxiliary Funcon
+ re-close(M:maps(identifiers, links), D:=>environments) : =>environments
+ ~> accumulate(scope(M, D), sequential(set-forward-links(M), map( )))
+/*
+ `re-close(M, D)` first executes `D` in the scope `M`, which maps identifiers
+ to freshly allocated links. This computes an environment `Rho` where the bound
+ values may contain links, or implicit references to links in abstraction
+ values. It then sets the link for each identifier in the domain of `M` to
+ refer to its bound value in `Rho`, and returns `Rho` as the result.
+*/
+
+
+Auxiliary Funcon
+ bind-to-forward-links(SI:sets(identifiers)) : =>maps(identifiers, links)
+ ~> map-unite(interleave-map(bind-value(given, fresh-link(values)),
+ set-elements(SI)))
+/*
+ `bind-to-forward-links(SI)` binds each identifier in the set `SI` to a
+ freshly allocated link.
+*/
+
+
+Auxiliary Funcon
+ set-forward-links(M:maps(identifiers, links)) : =>null-type
+ ~> effect(interleave-map(set-link(map-lookup(M, given), bound-value(given)),
+ set-elements(map-domain(M))))
+/*
+ For each identifier `I` in the domain of `M`, `set-forward-links(M)` sets the
+ link to which `I` is mapped by `M` to the current bound value of `I`.
+*/
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/index.md b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/index.md
new file mode 100644
index 0000000..cb6b402
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/index.md
@@ -0,0 +1,320 @@
+---
+layout: default
+title: "Binding"
+parent: Normal
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Binding.cbs]
+-----------------------------
+
+### Binding
+
+[
+ Type environments Alias envs
+ Datatype identifiers Alias ids
+ Funcon identifier-tagged Alias id-tagged
+ Funcon fresh-identifier
+ Entity environment Alias env
+ Funcon initialise-binding
+ Funcon bind-value Alias bind
+ Funcon unbind
+ Funcon bound-directly
+ Funcon bound-value Alias bound
+ Funcon closed
+ Funcon scope
+ Funcon accumulate
+ Funcon collateral
+ Funcon bind-recursively
+ Funcon recursive
+]Meta-variables
+ T <: valuesType
+ environments ~> maps(identifiers, values?)
+Alias
+ envs = environments( ) represents that its binding is hidden.
+
+ Circularity in environments (due to recursive bindings) is represented using
+ bindings to cut-points called links. Funcons are provided for making
+ declarations recursive and for referring to bound values without explicit
+ mention of links, so their existence can generally be ignored.
+
+Datatype
+ identifiers ::= {_:strings} | identifier-tagged(_:identifiers, _:values)
+Alias
+ ids = identifiersAlias
+ id-tagged = identifier-taggedFuncon
+ fresh-identifier : =>identifiersfresh-identifier computes an identifier distinct from all previously
+ computed identifiers.
+
+Rule
+ fresh-identifier ~> identifier-tagged("generated", fresh-atom)Entity
+ environment(_:environments) |- _ ---> _Alias
+ env = environmentFuncon
+ initialise-binding(X:=>T) : =>T
+ ~> initialise-linking(initialise-generating(closed(X)))initialise-binding(X) ensures that X does not depend on non-local bindings.
+ It also ensures that the linking entity (used to represent potentially cyclic
+ bindings) and the generating entity (for creating fresh identifiers) are
+ initialised.
+
+Funcon
+ bind-value(I:identifiers, V:values) : =>environments
+ ~> { I |-> V }
+Alias
+ bind = bind-valuebind-value(I, X) computes the environment that binds only I to the value
+ computed by X.
+
+
+
+Funcon
+ unbind(I:identifiers) : =>environments
+ ~> { I |-> ( ) }unbind(I) computes the environment that hides the binding of I.
+
+
+
+Funcon
+ bound-directly(_:identifiers) : =>valuesbound-directly(I) returns the value to which I is currently bound, if any,
+ and otherwise fails.
+
+ bound-directly(I) does *not* follow links. It is used only in connection with
+ recursively-bound values when references are not encapsulated in abstractions.
+
+Rule
+ lookup(Rho, I) ~> (V:values)
+ --------------------------------------------------------
+ environment(Rho) |- bound-directly(I:identifiers) ---> V
+Rule
+ lookup(Rho, I) ~> ( )
+ -----------------------------------------------------------
+ environment(Rho) |- bound-directly(I:identifiers) ---> failFuncon
+ bound-value(I:identifiers) : =>values
+ ~> follow-if-link(bound-directly(I))
+Alias
+ bound = bound-valuebound-value(I) inspects the value to which I is currently bound, if any,
+ and otherwise fails. If the value is a link, bound-value(I) returns the
+ value obtained by following the link, if any, and otherwise fails. If the
+ inspected value is not a link, bound-value(I) returns it.
+
+ bound-value(I) is used for references to non-recursive bindings and to
+ recursively-bound values when references are encapsulated in abstractions.
+
+
+
+#### Scope
+
+Funcon
+ closed(X:=>T) : =>Tclosed(X) ensures that X does not depend on non-local bindings.
+
+Rule
+ environment(map( )) |- X ---> X′
+ -------------------------------------------
+ environment(_) |- closed(X) ---> closed(X′)
+Rule
+ closed(V:T) ~> VFuncon
+ scope(_:environments, _:=>T) : =>Tscope(D,X) executes D with the current bindings, to compute an environment
+ Rho representing local bindings. It then executes X to compute the result,
+ with the current bindings extended by Rho, which may shadow or hide previous
+ bindings.
+
+ closed(scope(Rho, X)) ensures that X can reference only the bindings
+ provided by Rho.
+
+Rule
+ environment(map-override(Rho1, Rho0)) |- X ---> X′
+ ---------------------------------------------------------------------
+ environment(Rho0) |- scope(Rho1:environments, X) ---> scope(Rho1, X′)
+Rule
+ scope(_:environments, V:T) ~> VFuncon
+ accumulate(_:(=>environments)*) : =>environmentsaccumulate(D1, D2) executes D1 with the current bindings, to compute an
+ environment Rho1 representing some local bindings. It then executes D2 to
+ compute an environment Rho2 representing further local bindings, with the
+ current bindings extended by Rho1, which may shadow or hide previous
+ current bindings. The result is Rho1 extended by Rho2, which may shadow
+ or hide the bindings of Rho1.
+
+ accumulate(_, _) is associative, with map( ) as unit, and extends to any
+ number of arguments.
+
+Rule
+ D1 ---> D1′
+ -------------------------------------------
+ accumulate(D1, D2) ---> accumulate(D1′, D2)
+Rule
+ accumulate(Rho1:environments, D2) ~> scope(Rho1, map-override(D2, Rho1))
+Rule
+ accumulate( ) ~> map( )
+Rule
+ accumulate(D1) ~> D1
+Rule
+ accumulate(D1, D2, D+) ~> accumulate(D1, accumulate(D2, D+))Funcon
+ collateral(Rho*:environments*) : =>environments
+ ~> checked map-unite(Rho*)collateral(D1, ...) pre-evaluates its arguments with the current bindings,
+ and unites the resulting maps, which fails if the domains are not pairwise
+ disjoint.
+
+ collateral(D1, D2) is associative and commutative with map( ) as unit,
+ and extends to any number of arguments.
+
+
+
+#### Recurse
+
+Funcon
+ bind-recursively(I:identifiers, E:=>values) : =>environments
+ ~> recursive({I}, bind-value(I, E))bind-recursively(I, E) binds I to a link that refers to the value of E,
+ representing a recursive binding of I to the value of E.
+ Since bound-value(I) follows links, it should not be executed during the
+ evaluation of E.
+
+
+
+Funcon
+ recursive(SI:sets(identifiers), D:=>environments) : =>environments
+ ~> re-close(bind-to-forward-links(SI), D)recursive(SI, D) executes D with potential recursion on the bindings of
+ the identifiers in the set SI (which need not be the same as the set of
+ identifiers bound by D).
+
+
+
+Auxiliary Funcon
+ re-close(M:maps(identifiers, links), D:=>environments) : =>environments
+ ~> accumulate(scope(M, D), sequential(set-forward-links(M), map( )))re-close(M, D) first executes D in the scope M, which maps identifiers
+ to freshly allocated links. This computes an environment Rho where the bound
+ values may contain links, or implicit references to links in abstraction
+ values. It then sets the link for each identifier in the domain of M to
+ refer to its bound value in Rho, and returns Rho as the result.
+
+
+
+Auxiliary Funcon
+ bind-to-forward-links(SI:sets(identifiers)) : =>maps(identifiers, links)
+ ~> map-unite(interleave-map(bind-value(given, fresh-link(values)),
+ set-elements(SI)))bind-to-forward-links(SI) binds each identifier in the set SI to a
+ freshly allocated link.
+
+
+
+Auxiliary Funcon
+ set-forward-links(M:maps(identifiers, links)) : =>null-type
+ ~> effect(interleave-map(set-link(map-lookup(M, given), bound-value(given)),
+ set-elements(map-domain(M))))I in the domain of M, set-forward-links(M) sets the
+ link to which I is mapped by M to the current bound value of I.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Binding.cbs]: Binding.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Computations/Normal/Binding/Binding.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/accumulate.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/accumulate.config
new file mode 100644
index 0000000..21daf12
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/accumulate.config
@@ -0,0 +1,27 @@
+general {
+ funcon-term:
+ initialise-binding
+ tuple(
+ accumulate( ),
+ accumulate(bind-value("x", true)),
+ accumulate(bind-value("x", true),
+ bind-value("y", bound-directly"x")),
+ accumulate(bind-value("x", true),
+ bind-value("y", bound-directly"x"),
+ bind-value("z", bound-directly"x")),
+ accumulate(bind-value("x", true),
+ bind-value("y", true),
+ bind-value("x", bound-directly"x")))
+ ;
+}
+
+tests {
+ result-term:
+ tuple(
+ map( ),
+ {"x"|->true},
+ {"x"|->true, "y"|->true},
+ {"x"|->true, "y"|->true, "z"|->true},
+ {"y"|->true, "x"|->true})
+ ;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-recursively.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-recursively.config
new file mode 100644
index 0000000..c7a75d4
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-recursively.config
@@ -0,0 +1,16 @@
+general {
+ funcon-term:
+ initialise-binding
+ scope(
+ bind-recursively("x",
+ thunk closure
+ is-value bound-value"x"),
+ force bound-value"x")
+ ;
+}
+
+tests {
+ result-term:
+ true
+ ;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-value.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-value.config
new file mode 100644
index 0000000..6e3d821
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bind-value.config
@@ -0,0 +1,9 @@
+general {
+ funcon-term:
+ bind-value("x", 1)
+ ;
+}
+
+tests {
+ result-term: {"x"|->1};
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-directly.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-directly.config
new file mode 100644
index 0000000..d876434
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-directly.config
@@ -0,0 +1,15 @@
+general {
+ funcon-term:
+ initialise-binding
+ scope(
+ {"x"|->true, "y"|->fresh-link(booleans)},
+ and(
+ bound-directly"x",
+ is-in-type(bound-directly"y", links),
+ else(bound-directly"z", true)))
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-value.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-value.config
new file mode 100644
index 0000000..567a028
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/bound-value.config
@@ -0,0 +1,15 @@
+general {
+ funcon-term:
+ initialise-binding
+ scope(
+ {"x"|->true, "y"|->fresh-initialised-link(booleans,true)},
+ and(
+ bound-value"x",
+ bound-value"y",
+ else(bound-value"z",true)))
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/closed.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/closed.config
new file mode 100644
index 0000000..d2fd86e
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/closed.config
@@ -0,0 +1,11 @@
+general {
+ funcon-term:
+ initialise-binding
+ scope({"x"|->1},
+ closed(else(bound-directly"x", true)))
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/collateral.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/collateral.config
new file mode 100644
index 0000000..906ef86
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/collateral.config
@@ -0,0 +1,27 @@
+general {
+ funcon-term:
+ initialise-binding tuple(
+ collateral( ),
+ collateral(bind-value("x", true)),
+ collateral(bind-value("x", true),
+ bind-value("y", false)),
+ collateral(bind-value("x", true),
+ bind-value("y", false),
+ unbind"z"),
+ scope(bind-value("x",true),
+ collateral(bind-value("x", false),
+ bind-value("y", true),
+ bind-value("z", bound-directly"x"))))
+ ;
+}
+
+tests {
+ result-term:
+ tuple(
+ map( ),
+ {"x"|->true},
+ {"x"|->true, "y"|->false},
+ {"x"|->true, "y"|->false, "z"|->( )},
+ {"x"|->false,"y"|->true, "z"|->true})
+ ;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/environments.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/environments.config
new file mode 100644
index 0000000..74c0a67
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/environments.config
@@ -0,0 +1,12 @@
+general {
+ funcon-term:
+ and(
+ is-in-type(map(),environments),
+ is-in-type({"x"|->true},environments),
+ is-in-type({"x"|->true, "y"|->false},environments))
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/fresh-identifier.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/fresh-identifier.config
new file mode 100644
index 0000000..9c7ada7
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/fresh-identifier.config
@@ -0,0 +1,10 @@
+general {
+ funcon-term:
+ initialise-generating
+ not is-equal(fresh-identifier, fresh-identifier)
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/identifiers.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/identifiers.config
new file mode 100644
index 0000000..9bfdb50
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/identifiers.config
@@ -0,0 +1,14 @@
+general {
+ funcon-term:
+ and(
+ is-in-type("x", identifiers),
+ is-in-type(identifier-tagged("x",false), identifiers),
+ is-in-type(identifier-tagged(identifier-tagged("x",true),false), identifiers),
+ is-in-type(identifier-tagged("x",identifier-tagged("x",true)), identifiers)
+ )
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/initialise-binding.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/initialise-binding.config
new file mode 100644
index 0000000..ec7df7d
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/initialise-binding.config
@@ -0,0 +1,10 @@
+general {
+ funcon-term:
+ initialise-binding(print"OK")
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: ["OK"];
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/recursive.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/recursive.config
new file mode 100644
index 0000000..9f6f8a2
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/recursive.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ initialise-binding
+ scope(
+ recursive(
+ {"x"},
+ bind-value("x", thunk closure
+ if-true-else(not is-equal(null-value, bound-value"x"), true, false))),
+ force bound-value"x")
+ ;
+}
+
+tests {
+ result-term:
+ true
+ ;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/scope.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/scope.config
new file mode 100644
index 0000000..80cd350
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/scope.config
@@ -0,0 +1,15 @@
+general {
+ funcon-term:
+ initialise-binding
+ and(
+ scope(bind-value("x", false),
+ scope(bind-value("x", true),
+ bound-directly"x")),
+ scope(bind-value("x", false),
+ true))
+ ;
+}
+
+tests {
+ result-term: true;
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/unbind.config b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/unbind.config
new file mode 100644
index 0000000..f3f63aa
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Binding/tests/unbind.config
@@ -0,0 +1,9 @@
+general {
+ funcon-term:
+ unbind("x")
+ ;
+}
+
+tests {
+ result-term: {"x"|->( )};
+}
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/Flowing.cbs b/IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/Flowing.cbs
new file mode 100644
index 0000000..15907e1
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/Flowing.cbs
@@ -0,0 +1,242 @@
+### Flowing
+
+[
+ Funcon left-to-right Alias l-to-r
+ Funcon right-to-left Alias r-to-l
+ Funcon sequential Alias seq
+ Funcon effect
+ Funcon choice
+ Funcon if-true-else Alias if-else
+ Funcon while-true Alias while
+ Funcon do-while-true Alias do-while
+ Funcon interleave
+ Datatype yielding
+ Funcon signal
+ Funcon yielded
+ Funcon yield
+ Funcon yield-on-value
+ Funcon yield-on-abrupt
+ Funcon atomic
+]
+
+
+Meta-variables
+ T <: values
+ T* <: values*
+
+
+#### Sequencing
+
+Funcon
+ left-to-right(_:(=>(T)*)*) : =>(T)*
+Alias
+ l-to-r = left-to-right
+/*
+ `left-to-right(...)` computes its arguments sequentially, from left to right,
+ and gives the resulting sequence of values, provided all terminate normally.
+ For example, `integer-add(X, Y)` may interleave the computations of `X` and
+ `Y`, whereas `integer-add left-to-right(X, Y)` always computes `X` before `Y`.
+
+ When each argument of `left-to-right(...)` computes a single value, the type
+ of the result is the same as that of the argument sequence. For instance,
+ when `X:T` and `Y:T'`, the result of `left-to-right(X, Y)` is of type `(T, T')`.
+ The only effect of wrapping an argument sequence in `left-to-right(...)` is to
+ ensure that when the arguments are to be evaluated, it is done in the
+ specified order.
+*/
+Rule
+ Y ---> Y'
+ ------------------------------------------------------------
+ left-to-right(V*:(T)*, Y, Z*) ---> left-to-right(V*, Y', Z*)
+Rule
+ left-to-right(V*:(T)*) ~> V*
+
+
+Funcon
+ right-to-left(_:(=>(T)*)*) : =>(T)*
+Alias
+ r-to-l = right-to-left
+/*
+ `right-to-left(...)` computes its arguments sequentially, from right to left,
+ and gives the resulting sequence of values, provided all terminate normally.
+
+ Note that `right-to-left(X*)` and `reverse left-to-right reverse(X*)` are
+ not equivalent: `reverse(X*)` interleaves the evaluation of `X*`.
+*/
+Rule
+ Y ---> Y'
+ ------------------------------------------------------------
+ right-to-left(X*, Y, V*:(T)*) ---> right-to-left(X*, Y', V*)
+Rule
+ right-to-left(V*:(T)*) ~> V*
+
+
+Funcon
+ sequential(_:(=>null-type)*, _:=>T) : =>T
+Alias
+ seq = sequential
+/*
+ `sequential(X, ...)` computes its arguments in the given order. On normal
+ termination, it returns the value of the last argument; the other arguments
+ all compute `null-value`.
+
+ Binary `sequential(X, Y)` is associative, with unit `null-value`.
+*/
+Rule
+ X ---> X'
+ -----------------------------------------
+ sequential(X, Y+) ---> sequential(X', Y+)
+Rule
+ sequential(null-value, Y+) ~> sequential(Y+)
+Rule
+ sequential(Y) ~> Y
+
+
+Funcon
+ effect(V*:T*) : =>null-type
+ ~> null-value
+/*
+ `effect(...)` interleaves the computations of its arguments, then discards
+ all the computed values.
+*/
+
+
+#### Choosing
+
+Funcon
+ choice(_:(=>T)+) : =>T
+/*
+ `choice(Y, ...)` selects one of its arguments, then computes it.
+ It is associative and commutative.
+*/
+Rule
+ choice(X*, Y, Z*) ~> Y
+
+
+Funcon
+ if-true-else(_:booleans, _:=>T, _:=>T) : =>T
+Alias
+ if-else = if-true-else
+/*
+ `if-true-else(B, X, Y)` evaluates `B` to a Boolean value, then reduces
+ to `X` or `Y`, depending on the value of `B`.
+*/
+Rule
+ if-true-else(true, X, Y) ~> X
+Rule
+ if-true-else(false, X, Y) ~> Y
+
+
+#### Iterating
+
+Funcon
+ while-true(B:=>booleans, X:=>null-type) : =>null-type
+ ~> if-true-else(B, sequential(X, while-true(B, X)), null-value)
+Alias
+ while = while-true
+/*
+ `while-true(B, X)` evaluates `B` to a Boolean value. Depending on the value
+ of `B`, it either executes `X` and iterates, or terminates normally.
+
+ The effect of abruptly breaking the iteration is obtained by the combination
+ `handle-break(while-true(B, X))`, and that of abruptly continuing the iteration by
+ `while-true(B, handle-continue(X))`.
+*/
+
+Funcon
+ do-while-true(X:=>null-type, B:=>booleans) : =>null-type
+ ~> sequential(X, if-true-else(B, do-while-true(X, B), null-value))
+Alias
+ do-while = do-while-true
+/*
+ `do-while-true(X, B)` is equivalent to `sequential(X, while-true(B, X))`.
+*/
+
+
+#### Interleaving
+
+Funcon
+ interleave(_:T*) : =>T*
+/*
+ `interleave(...)` computes its arguments in any order, possibly interleaved,
+ and returns the resulting sequence of values, provided all terminate normally.
+ Fairness of interleaving is not required, so pure left-to-right computation
+ is allowed.
+
+ `atomic(X)` prevents interleaving in `X`, except after transitions that emit
+ a `yielded(signal)`.
+*/
+Rule
+ interleave(V*:T*) ~> V*
+
+
+Datatype
+ yielding ::= signal
+
+
+Entity
+ _ --yielded(_:yielding?)-> _
+/*
+ `yielded(signal)` in a label on a transition allows interleaving at that point
+ in the enclosing atomic computation.
+ `yielded( )` indicates interleaving at that point in an atomic computation
+ is not allowed.
+*/
+
+
+Funcon
+ yield : =>null-type
+ ~> yield-on-value(null-value)
+
+
+Funcon
+ yield-on-value(_:T) : =>T
+/*
+ `yield-on-value(X)` allows interleaving in an enclosing atomic computation
+ on normal termination of `X`.
+*/
+Rule
+ yield-on-value(V:T) --yielded(signal)-> V
+
+
+Funcon
+ yield-on-abrupt(_:=>T) : =>T
+/*
+ `yield-on-abrupt(X)` ensures that abrupt termination of `X` is propagated
+ through an enclosing atomic computation.
+*/
+Rule
+ X --abrupt(V:T),yielded(_?)-> X'
+ --------------------------------------------------------------------
+ yield-on-abrupt(X) --abrupt(V),yielded(signal)-> yield-on-abrupt(X')
+Rule
+ X --abrupt( )-> X'
+ ----------------------------------------------------
+ yield-on-abrupt(X) --abrupt( )-> yield-on-abrupt(X')
+Rule
+ yield-on-abrupt(V:T) ~> V
+
+
+Funcon
+ atomic(_:=>T) : =>T
+/*
+ `atomic(X)` computes `X`, but controls its potential interleaving with other
+ computations: interleaving is only allowed following a transition of `X` that
+ emits `yielded(signal)`.
+*/
+Rule
+ X --yielded( )->1 X'
+ atomic(X') --yielded( )->2 X''
+ -----------------------------------------------
+ atomic(X) --yielded( )->1 ; --yielded( )->2 X''
+Rule
+ X --yielded( )-> V
+ V : T
+ ---------------------------
+ atomic(X) --yielded( )-> V
+Rule
+ atomic(V:T) ~> V
+Rule
+ X --yielded(signal)-> X'
+ -----------------------------------
+ atomic(X) --yielded( )-> atomic(X')
diff --git a/IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/index.md b/IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/index.md
new file mode 100644
index 0000000..0768615
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Computations/Normal/Flowing/index.md
@@ -0,0 +1,289 @@
+---
+layout: default
+title: "Flowing"
+parent: Normal
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Flowing.cbs]
+-----------------------------
+
+### Flowing
+
+[
+ Funcon left-to-right Alias l-to-r
+ Funcon right-to-left Alias r-to-l
+ Funcon sequential Alias seq
+ Funcon effect
+ Funcon choice
+ Funcon if-true-else Alias if-else
+ Funcon while-true Alias while
+ Funcon do-while-true Alias do-while
+ Funcon interleave
+ Datatype yielding
+ Funcon signal
+ Funcon yielded
+ Funcon yield
+ Funcon yield-on-value
+ Funcon yield-on-abrupt
+ Funcon atomic
+]Funcon
+ left-to-right(_:(=>(T)*)*) : =>(T)*
+Alias
+ l-to-r = left-to-rightleft-to-right(...) computes its arguments sequentially, from left to right,
+ and gives the resulting sequence of values, provided all terminate normally.
+ For example, integer-add(X, Y) may interleave the computations of X and
+ Y, whereas integer-add left-to-right(X, Y) always computes X before Y.
+
+ When each argument of left-to-right(...) computes a single value, the type
+ of the result is the same as that of the argument sequence. For instance,
+ when X:T and Y:T′, the result of left-to-right(X, Y) is of type (T, T′).
+ The only effect of wrapping an argument sequence in left-to-right(...) is to
+ ensure that when the arguments are to be evaluated, it is done in the
+ specified order.
+
+Rule
+ Y ---> Y′
+ ------------------------------------------------------------
+ left-to-right(V*:(T)*, Y, Z*) ---> left-to-right(V*, Y′, Z*)
+Rule
+ left-to-right(V*:(T)*) ~> V*Funcon
+ right-to-left(_:(=>(T)*)*) : =>(T)*
+Alias
+ r-to-l = right-to-leftright-to-left(...) computes its arguments sequentially, from right to left,
+ and gives the resulting sequence of values, provided all terminate normally.
+
+ Note that right-to-left(X*) and reverse left-to-right reverse(X*) are
+ not equivalent: reverse(X*) interleaves the evaluation of X*.
+
+Rule
+ Y ---> Y′
+ ------------------------------------------------------------
+ right-to-left(X*, Y, V*:(T)*) ---> right-to-left(X*, Y′, V*)
+Rule
+ right-to-left(V*:(T)*) ~> V*Funcon
+ sequential(_:(=>null-type)*, _:=>T) : =>T
+Alias
+ seq = sequentialsequential(X, ...) computes its arguments in the given order. On normal
+ termination, it returns the value of the last argument; the other arguments
+ all compute null-value.
+
+ Binary sequential(X, Y) is associative, with unit null-value.
+
+Rule
+ X ---> X′
+ -----------------------------------------
+ sequential(X, Y+) ---> sequential(X′, Y+)
+Rule
+ sequential(null-value, Y+) ~> sequential(Y+)
+Rule
+ sequential(Y) ~> YFuncon
+ effect(V*:T*) : =>null-type
+ ~> null-valueeffect(...) interleaves the computations of its arguments, then discards
+ all the computed values.
+
+
+
+#### Choosing
+
+Funcon
+ choice(_:(=>T)+) : =>Tchoice(Y, ...) selects one of its arguments, then computes it.
+ It is associative and commutative.
+
+
+
+Funcon
+ if-true-else(_:booleans, _:=>T, _:=>T) : =>T
+Alias
+ if-else = if-true-elseif-true-else(B, X, Y) evaluates B to a Boolean value, then reduces
+ to X or Y, depending on the value of B.
+
+Rule
+ if-true-else(true, X, Y) ~> X
+Rule
+ if-true-else(false, X, Y) ~> YFuncon
+ while-true(B:=>booleans, X:=>null-type) : =>null-type
+ ~> if-true-else(B, sequential(X, while-true(B, X)), null-value)
+Alias
+ while = while-truewhile-true(B, X) evaluates B to a Boolean value. Depending on the value
+ of B, it either executes X and iterates, or terminates normally.
+
+ The effect of abruptly breaking the iteration is obtained by the combination
+ handle-break(while-true(B, X)), and that of abruptly continuing the iteration by
+ while-true(B, handle-continue(X)).
+
+Funcon
+ do-while-true(X:=>null-type, B:=>booleans) : =>null-type
+ ~> sequential(X, if-true-else(B, do-while-true(X, B), null-value))
+Alias
+ do-while = do-while-truedo-while-true(X, B) is equivalent to sequential(X, while-true(B, X)).
+
+
+
+#### Interleaving
+
+Funcon
+ interleave(_:T*) : =>T*interleave(...) computes its arguments in any order, possibly interleaved,
+ and returns the resulting sequence of values, provided all terminate normally.
+ Fairness of interleaving is not required, so pure left-to-right computation
+ is allowed.
+
+ atomic(X) prevents interleaving in X, except after transitions that emit
+ a yielded(signal).
+
+Rule
+ interleave(V*:T*) ~> V*Datatype
+ yielding ::= signalEntity
+ _ --yielded(_:yielding?)-> _yielded(signal) in a label on a transition allows interleaving at that point
+ in the enclosing atomic computation.
+ yielded( ) indicates interleaving at that point in an atomic computation
+ is not allowed.
+
+
+
+Funcon
+ yield : =>null-type
+ ~> yield-on-value(null-value)Funcon
+ yield-on-value(_:T) : =>Tyield-on-value(X) allows interleaving in an enclosing atomic computation
+ on normal termination of X.
+
+Rule
+ yield-on-value(V:T) --yielded(signal)-> VFuncon
+ yield-on-abrupt(_:=>T) : =>Tyield-on-abrupt(X) ensures that abrupt termination of X is propagated
+ through an enclosing atomic computation.
+
+Rule
+ X --abrupt(V:T),yielded(_?)-> X′
+ --------------------------------------------------------------------
+ yield-on-abrupt(X) --abrupt(V),yielded(signal)-> yield-on-abrupt(X′)
+Rule
+ X --abrupt( )-> X′
+ ----------------------------------------------------
+ yield-on-abrupt(X) --abrupt( )-> yield-on-abrupt(X′)
+Rule
+ yield-on-abrupt(V:T) ~> VFuncon
+ atomic(_:=>T) : =>Tatomic(X) computes X, but controls its potential interleaving with other
+ computations: interleaving is only allowed following a transition of X that
+ emits yielded(signal).
+
+Rule
+ X --yielded( )->1 X′
+ atomic(X′) --yielded( )->2 X′′
+ -----------------------------------------------
+ atomic(X) --yielded( )->1 ; --yielded( )->2 X′′
+Rule
+ X --yielded( )-> V
+ V : T
+ ---------------------------
+ atomic(X) --yielded( )-> V
+Rule
+ atomic(V:T) ~> V
+Rule
+ X --yielded(signal)-> X′
+ -----------------------------------
+ atomic(X) --yielded( )-> atomic(X′)[
+ Type atoms
+ Entity used-atom-set
+ Funcon initialise-generating
+ Funcon fresh-atom
+ Funcon use-atom-not-in
+]Meta-variables
+ T <: valuesBuilt-in Type
+ atomsatoms is the type of values used as distinguishable tags.
+ Notation for individual atoms is not provided.
+
+
+
+
+
+
+
+Built-in Funcon
+ initialise-generating(_:=>T) : =>Tused-atom-set(SA) entity is unspecified. It could
+ contains atoms that are reserved for internal use.
+
+
+
+Funcon
+ fresh-atom : =>atomsfresh-atom computes an atom distinct from all previously computed atoms.
+
+Rule
+ element-not-in(atoms, SA) ~> A
+ -----------------------------------------------
+ < fresh-atom , used-atom-set(SA) >
+ ---> < A , used-atom-set(set-insert(A, SA)) >use-atom-not-in(SA) computes an atom not in the set SA, and inserts it
+ in the used-atom-set(SA′) entity, in case it was not previously used.
+
+Rule
+ element-not-in(atoms, SA) ~> A
+ --------------------------------------------------------
+ < use-atom-not-in(SA:sets(atoms)) , used-atom-set(SA′) >
+ ---> < A , used-atom-set(set-insert(A, SA′)) >[
+ Entity given-value
+ Funcon initialise-giving
+ Funcon give
+ Funcon given
+ Funcon no-given
+ Funcon left-to-right-map
+ Funcon interleave-map
+ Funcon left-to-right-repeat
+ Funcon interleave-repeat
+ Funcon left-to-right-filter
+ Funcon interleave-filter
+ Funcon fold-left
+ Funcon fold-right
+]Entity
+ given-value(_:values?) |- _ ---> _V:values. The given value ( ) represents
+ the absence of a current given value.
+
+
+
+
+
+
+ initialise-giving(X) ensures that the entities used by the funcons for
+ giving are properly initialised.
+
+
+
+Funcon
+ give(_:T, _:T=>T′) : =>T′give(X, Y) executes X, possibly referring to the current given value,
+ to compute a value V. It then executes Y with V as the given value,
+ to compute the result.
+
+Rule
+ given-value(V) |- Y ---> Y′
+ ------------------------------------------------
+ given-value(_?) |- give(V:T, Y) ---> give(V, Y′)
+Rule
+ give(_:T, W:T′) ~> WFuncon
+ given : T=>Tgiven refers to the current given value.
+
+Rule
+ given-value(V:values) |- given ---> V
+Rule
+ given-value( ) |- given ---> failFuncon
+ no-given(_:( )=>T′) : ( )=>T′no-given(X) computes X without references to the current given value.
+
+Rule
+ given-value( ) |- X ---> X′
+ ------------------------------------------------
+ given-value(_?) |- no-given(X) ---> no-given(X′)
+Rule
+ no-given(U:T′) ~> Ulist(left-to-right-map(F, list-elements(L))).
+
+
+Funcon
+ left-to-right-map(_:T=>T′, _:(T)*) : =>(T′)*left-to-right-map(F, V*) computes F for each value in V* from left
+ to right, returning the sequence of resulting values.
+
+Rule
+ left-to-right-map(F, V:T, V*:(T)*)
+ ~> left-to-right(give(V, F), left-to-right-map(F, V*))
+Rule
+ left-to-right-map(_, ( )) ~> ( )Funcon
+ interleave-map(_:T=>T′, _:(T)*) : =>(T′)*interleave-map(F, V*) computes F for each value in V* interleaved,
+ returning the sequence of resulting values.
+
+Rule
+ interleave-map(F, V:T, V*:(T)*)
+ ~> interleave(give(V, F), interleave-map(F, V*))
+Rule
+ interleave-map(_, ( )) ~> ( )left-to-right-repeat(F, M, N) computes F for each value from M to N
+ sequentially, returning the sequence of resulting values.
+
+Rule
+ is-less-or-equal(M, N) == true
+ -------------------------------------------------------------------------
+ left-to-right-repeat(F, M:integers, N:integers)
+ ~> left-to-right(give(M, F), left-to-right-repeat(F, int-add(M, 1), N))
+Rule
+ is-less-or-equal(M, N) == false
+ ----------------------------------------------
+ left-to-right-repeat(_, M:integers, N:integers) ~> ( )interleave-repeat(F, M, N) computes F for each value from M to N
+ interleaved, returning the sequence of resulting values.
+
+Rule
+ is-less-or-equal(M, N) == true
+ -------------------------------------------------------------------
+ interleave-repeat(F, M:integers, N:integers)
+ ~> interleave(give(M, F), interleave-repeat(F, int-add(M, 1), N))
+Rule
+ is-less-or-equal(M, N) == false
+ -------------------------------------------
+ interleave-repeat(_, M:integers, N:integers) ~> ( )list(left-to-right-filter(P, list-elements(L))) to filter a list L.
+
+
+
+Funcon
+ left-to-right-filter(_:T=>booleans, _:(T)*) : =>(T)*left-to-right-filter(P, V*) computes P for each value in V* from left
+ to right, returning the sequence of argument values for which the result is
+ true.
+
+Rule
+ left-to-right-filter(P, V:T, V*:(T)*)
+ ~> left-to-right(when-true(give(V, P), V), left-to-right-filter(P, V*))
+Rule
+ left-to-right-filter(_) ~> ( )Funcon
+ interleave-filter(_:T=>booleans, _:(T)*) : =>(T)*interleave-filter(P, V*) computes P for each value in V* interleaved,
+ returning the sequence of argument values for which the result is true.
+
+Rule
+ interleave-filter(P, V:T, V*:(T)*)
+ ~> interleave(when-true(give(V, P), V), interleave-filter(P, V*))
+Rule
+ interleave-filter(_) ~> ( )Funcon
+ fold-left(_:tuples(T,T′)=>T, _:T, _:(T′)*) : =>Tfold-left(F, A, V*) reduces a sequence V* to a single value by folding it
+ from the left, using A as the initial accumulator value, and iteratively
+ updating the accumulator by giving F the pair of the accumulator value and
+ the first of the remaining arguments.
+
+Rule
+ fold-left(_, A:T, ( )) ~> A
+Rule
+ fold-left(F, A:T, V:T′, V*:(T′)*) ~> fold-left(F, give(tuple(A, V), F), V*)Funcon
+ fold-right(_:tuples(T,T′)=>T′, _:T′, _:(T)*) : =>T′fold-right(F, A, V*) reduces a sequence V* to a single value by folding it
+ from the right, using A as the initial accumulator value, and iteratively
+ updating the accumulator by giving F the pair of the the last of the
+ remaining arguments and the accumulator value.
+
+Rule
+ fold-right(_, A:T′, ( )) ~> A
+Rule
+ fold-right(F, A:T′, V*:(T)*, V:T) ~> give(tuple(V, fold-right(F, A, V*)), F)[
+ Entity standard-out
+ Funcon print
+]Entity
+ _ -- standard-out!(_:values*) -> _( ) represents the lack of output.
+ Composition of transitions concatenates their output sequences.
+
+
+
+
+
+ print(X*) evaluates the arguments X* and emits the resulting sequence of
+ values on the standard-out channel. print( ) has no effect.
+
+Rule
+ print(V*:values*) -- standard-out!(V*) -> null-value[
+ Entity standard-in
+ Funcon read
+]Entity
+ _ -- standard-in?(_:values*) -> _( ) represents that no values are
+ input. The value null-value represents the end of the input.
+
+ Composition of transitions concatenates their input sequences, except that
+ when the first sequence ends with null-value, the second seqeunce has to be
+ just null-value.
+
+
+
+Funcon
+ read : =>valuesread inputs a single value from the standard-in channel, and returns it.
+ If the end of the input has been reached, read fails.
+
+Rule
+ read -- standard-in?(V:~null-type) -> V
+Rule
+ read -- standard-in?(null-value) -> fail[
+ Datatype links
+ Funcon initialise-linking
+ Funcon link
+ Funcon fresh-link
+ Funcon fresh-initialised-link Alias fresh-init-link
+ Funcon set-link
+ Funcon follow-if-link
+]Meta-variables
+ T <: valuesDatatype
+ links ::= link(_:variables)Funcon
+ initialise-linking(X:=>T) : =>T
+ ~> initialise-storing(X)initialise-linking(X) ensures that the entities used by the funcons for
+ linking are properly initialised.
+
+
+
+Funcon
+ fresh-link(T) : =>links
+ ~> link(allocate-variable(T))Funcon
+ fresh-initialised-link(T, V:T) : =>links
+ ~> link(allocate-initialised-variable(T, V))
+Alias
+ fresh-init-link = fresh-initialised-linkV is a link, follow-if-link(V) computes the set value, and
+ otherwise it evaluates to V.
+
+Rule
+ follow-if-link(link(Var:variables)) ~> assigned(Var)
+Rule
+ follow-if-link(V:~links) ~> V[
+ Datatype locations Alias locs
+ Type stores
+ Entity store
+ Funcon initialise-storing
+ Funcon store-clear
+ Datatype variables Alias vars
+ Funcon variable Alias var
+ Funcon allocate-variable Alias alloc
+ Funcon recycle-variables Alias recycle
+ Funcon initialise-variable Alias init
+ Funcon allocate-initialised-variable Alias alloc-init
+ Funcon assign
+ Funcon assigned
+ Funcon current-value
+ Funcon un-assign
+ Funcon structural-assign
+ Funcon structural-assigned
+]Meta-variables
+ T, T′ <: values( ) models the absence of its stored value;
+ removing it from the store allows it to be re-allocated.
+
+
+
+Entity
+ < _ , store(_:stores) > ---> < _ , store(_:stores) >< X , store(Sigma) > ---> < X′ , store(Sigma′) > models
+ a step from X to X′ where the difference between Sigma and Sigma′
+ (if any) corresponds to storage effects.
+
+Funcon
+ store-clear : =>null-type
+Rule
+ < store-clear , store(_) > ---> < null-value , store(map( )) >store-clear ensures the store is empty.
+
+Funcon
+ initialise-storing(X:=>T) : =>T
+ ~> sequential(store-clear,
+ initialise-giving(initialise-generating(X)))
+Alias
+ init-storing = initialise-storinginitialise-storing(X) ensures that the entities used by the funcons for
+ storing are properly initialised.
+
+
+
+#### Simple variables
+
+
+ Simple variables may store primitive or structured values. The type of
+ values stored by a variable is fixed when it is allocated. For instance,
+ allocate-variable(integers) allocates a simple integer variable, and
+ allocate-variable(vectors(integers)) allocates a structured variable for
+ storing vectors of integers, which can be updated only monolithically.
+
+Datatype
+ variables ::= variable(_:locations, _:value-types)
+Alias
+ vars = variablesAlias
+ var = variablevariables is the type of simple variables that can store values of
+ a particular type.
+
+ variable(L, T) constructs a simple variable for storing values of
+ type T at location L. Variables at different locations are independent.
+
+ Note that variables is a subtype of datatype-values.
+
+Funcon
+ allocate-variable(T:types) : =>variables
+Alias
+ alloc = allocate-variableallocate-variable(T) gives a simple variable whose location is not in the
+ current store. Subsequent uses of allocate-variable(T′) give independent
+ variables, except after recycle-variables(V,...) or store-clear.
+
+Rule
+ < use-atom-not-in(dom(Sigma)) , store(Sigma) > ---> < L , store(Sigma′) >
+ map-override({L |-> ( )}, Sigma′) ~> Sigma′′
+ -------------------------------------------------------------------------
+ < allocate-variable(T:types) , store(Sigma) >
+ ---> < variable(L, T) , store(Sigma′′) >Funcon
+ recycle-variables(_:variables+) : =>null-type
+Alias
+ recycle = recycle-variablesrecycle-variables(Var,...) removes the locations of Var, ..., from the
+ current store, so that they may subsequently be re-allocated.
+
+Rule
+ is-in-set(L, dom(Sigma)) == true
+ ---------------------------------------------------------------------
+ < recycle-variables(variable(L:locations, T:types)) , store(Sigma) >
+ ---> < null-value , store(map-delete(Sigma, {L})) >
+Rule
+ is-in-set(L, dom(Sigma)) == false
+ ---------------------------------------------------------------------
+ < recycle-variables(variable(L:locations, T:types)) , store(Sigma) >
+ ---> < fail , store(Sigma) >
+Rule
+ recycle-variables(Var:variables, Var+:variables+)
+ ~> sequential(recycle-variables(Var), recycle-variables(Var+))Funcon
+ initialise-variable(_:variables, _:values) : =>null-type
+Alias
+ init = initialise-variableinitialise-variable(Var, Val) assigns Val as the initial value of Var,
+ and gives null-value. If Var already has an assigned value, it fails.
+
+Rule
+ and(is-in-set(L, dom(Sigma)),
+ not is-value(map-lookup(Sigma, L)),
+ is-in-type(Val, T))
+ == true
+ ----------------------------------------------------------------------------
+ < initialise-variable(variable(L:locations, T:types), Val:values) ,
+ store(Sigma) > ---> < null-value , store(map-override({L|->Val}, Sigma)) >
+Rule
+ and(is-in-set(L, dom(Sigma)),
+ not is-value(map-lookup(Sigma, L)),
+ is-in-type(Val, T))
+ == false
+ ----------------------------------------------------------------------------
+ < initialise-variable(variable(L:locations, T:types), Val:values) ,
+ store(Sigma) > ---> < fail , store(Sigma) >Funcon
+ allocate-initialised-variable(T, Val:T) : =>variables
+ ~> give(allocate-variable(T),
+ sequential(initialise-variable(given, Val), given))
+Alias
+ alloc-init = allocate-initialised-variableallocate-initialised-variable(T, Val) allocates a simple variable for
+ storing values of type T, initialises its value to Val, and returns the
+ variable.
+
+
+
+
+
+ assign(Var, Val) assigns the value Val to the variable Var,
+ provided that Var was allocated with a type that contains Val.
+
+Rule
+ and(is-in-set(L, dom(Sigma)), is-in-type(Val, T)) == true
+ -----------------------------------------------------------------------
+ < assign(variable(L:locations, T:types), Val:values) ,
+ store(Sigma) > ---> < null-value , store(map-override({L|->Val}, Sigma)) >
+Rule
+ and(is-in-set(L, dom(Sigma)), is-in-type(Val, T)) == false
+ --------------------------------------------------------------------------
+ < assign(variable(L:locations,T:types), Val:values) ,
+ store(Sigma) > ---> < fail , store(Sigma) >assigned(Var) gives the value assigned to the variable Var,
+ failing if no value is currently assigned.
+
+Rule
+ map-lookup(Sigma, L) ~> (Val:values)
+ ------------------------------------------------------------------
+ < assigned(variable(L:locations, T:types)) , store(Sigma) >
+ ---> < Val , store(Sigma) >
+Rule
+ map-lookup(Sigma, L) == ( )
+ ------------------------------------------------------------------
+ < assigned(variable(L:locations, T:types)) , store(Sigma) >
+ ---> < fail , store(Sigma) >current-value(V) gives the same result as assigned(V) when V is a
+ simple variable, and otherwise gives V.
+
+ It represents implicit dereferencing of a value that might be a variable.
+
+Rule
+ current-value(Var:variables) ~> assigned(Var)
+Rule
+ current-value(U:~variables) ~> Uun-assign(Var) remove the value assigned to the variable Var.
+
+Rule
+ is-in-set(L, dom(Sigma)) == true
+ --------------------------------------------------------------------------
+ < un-assign(variable(L:locations, T:types)) , store(Sigma) >
+ ---> < null-value , store(map-override({L |-> ( )}, Sigma)) >
+Rule
+ is-in-set(L, dom(Sigma)) == false
+ --------------------------------------------------------------------------
+ < un-assign(variable(L:locations, T:types)) , store(Sigma) >
+ ---> < fail , store(Sigma) >assign(Var, Val) and
+ assigned(Var) access all the simple variables contained in a
+ structured variable. Assignment requires each component value of a hybrid
+ structured variable to be equal to the corresponding component of the
+ structured value.
+
+
+
+
+ structural-assign(V1, V2) takes a (potentially) structured variable
+ V1and a (potentially) structured value V2. Provided that the structure
+ and all non-variable values in V1 match the structure and corresponding
+ values of V2, all the simple variables in V1 are assigned the
+ corresponding values of V2; otherwise the assignment fails.
+
+Rule
+ structural-assign(V1:variables, V2:values)
+ ~> assign(V1, V2)
+Rule
+ V1 : ~(variables)
+ V1 ~> datatype-value(I1:identifiers, V1*:values*)
+ V2 ~> datatype-value(I2:identifiers, V2*:values*)
+ -----------------------------------------------------------------------
+ structural-assign(V1:datatype-values, V2:datatype-values)
+ ~> sequential(
+ check-true(is-equal(I1, I2)),
+ effect(tuple(interleave-map(
+ structural-assign(tuple-elements(given)),
+ tuple-zip(tuple(V1*), tuple(V2*))))),
+ null-value)Rule
+ dom(M1) == {}
+ ------------------------------------------------------
+ structural-assign(M1:maps(_,_), M2:maps(_,_))
+ ~> check-true(is-equal(dom(M2), { }))
+Rule
+ some-element(dom(M1)) ~> K
+ ----------------------------------------------------------------------------
+ structural-assign(M1:maps(_, _), M2:maps(_, _))
+ ~> sequential(check-true(is-in-set(K, dom(M2))),
+ structural-assign(map-lookup(M1, K), map-lookup(M2, K)),
+ structural-assign(map-delete(M1, {K}), map-delete(M2, {K})))
+Rule
+ V1 : ~(datatype-values|maps(_, _))
+ ---------------------------------------------------------------
+ structural-assign(V1:values,V2:values)
+ ~> check-true(is-equal(V1, V2))structural-assigned(V) takes a (potentially) structured variable V,
+ and computes the value of V with all simple variables in V replaced by
+ their assigned values, failing if any of them do not have assigned values.
+
+ When V is just a simple variable or a (possibly structured) value with no
+ component variables, structural-assigned(V) gives the same result as
+ current-value(V).
+
+Rule
+ structural-assigned(Var:variables) ~> assigned(Var)
+Rule
+ V : ~(variables)
+ V ~> datatype-value(I:identifiers, V*:values*)
+ ----------------------------------------------------------------------------
+ structural-assigned(V:datatype-values)
+ ~> datatype-value(I, interleave-map(structural-assigned(given), V*))Rule
+ structural-assigned(M:maps(_, _))
+ ~> map(interleave-map(structural-assigned(given), map-elements(M)))
+Rule
+ U : ~(datatype-values|maps(_, _))
+ ------------------------------------------
+ structural-assigned(U:values) ~> U[
+ Funcon computation-types
+][
+ Funcon left-to-right Alias l-to-r
+ Funcon right-to-left Alias r-to-l
+ Funcon sequential Alias seq
+ Funcon effect
+ Funcon choice
+ Funcon if-true-else Alias if-else
+ Funcon while-true Alias while
+ Funcon do-while-true Alias do-while
+ Funcon interleave
+ Datatype yielding
+ Funcon signal
+ Funcon yielded
+ Funcon yield
+ Funcon yield-on-value
+ Funcon yield-on-abrupt
+ Funcon atomic
+][
+ Entity given-value
+ Funcon initialise-giving
+ Funcon give
+ Funcon given
+ Funcon no-given
+ Funcon left-to-right-map
+ Funcon interleave-map
+ Funcon left-to-right-repeat
+ Funcon interleave-repeat
+ Funcon left-to-right-filter
+ Funcon interleave-filter
+ Funcon fold-left
+ Funcon fold-right
+][
+ Type environments Alias envs
+ Datatype identifiers Alias ids
+ Funcon identifier-tagged Alias id-tagged
+ Funcon fresh-identifier
+ Entity environment Alias env
+ Funcon initialise-binding
+ Funcon bind-value Alias bind
+ Funcon unbind
+ Funcon bound-directly
+ Funcon bound-value Alias bound
+ Funcon closed
+ Funcon scope
+ Funcon accumulate
+ Funcon collateral
+ Funcon bind-recursively
+ Funcon recursive
+][
+ Type atoms
+ Entity used-atom-set
+ Funcon initialise-generating
+ Funcon fresh-atom
+ Funcon use-atom-not-in
+][
+ Datatype locations Alias locs
+ Type stores
+ Entity store
+ Funcon initialise-storing
+ Funcon store-clear
+ Datatype variables Alias vars
+ Funcon variable Alias var
+ Funcon allocate-variable Alias alloc
+ Funcon recycle-variables Alias recycle
+ Funcon initialise-variable Alias init
+ Funcon allocate-initialised-variable Alias alloc-init
+ Funcon assign
+ Funcon assigned
+ Funcon current-value
+ Funcon un-assign
+ Funcon structural-assign
+ Funcon structural-assigned
+][
+ Datatype links
+ Funcon initialise-linking
+ Funcon link
+ Funcon fresh-link
+ Funcon fresh-initialised-link Alias fresh-init-link
+ Funcon set-link
+ Funcon follow-if-link
+][
+ Entity standard-in
+ Funcon read
+][
+ Entity standard-out
+ Funcon print
+][
+ Funcon stuck
+ Entity abrupted
+ Funcon finalise-abrupting
+ Funcon abrupt
+ Funcon handle-abrupt
+ Funcon finally
+][
+ Datatype failing
+ Funcon failed
+ Funcon finalise-failing
+ Funcon fail
+ Funcon else
+ Funcon else-choice
+ Funcon checked
+ Funcon check-true
+][
+ Datatype throwing
+ Funcon thrown
+ Funcon finalise-throwing
+ Funcon throw
+ Funcon handle-thrown
+ Funcon handle-recursively
+ Funcon catch-else-throw
+][
+ Datatype returning
+ Funcon returned
+ Funcon finalise-returning
+ Funcon return
+ Funcon handle-return
+][
+ Datatype breaking
+ Funcon broken
+ Funcon finalise-breaking
+ Funcon break
+ Funcon handle-break
+][
+ Datatype continuing
+ Funcon continued
+ Funcon finalise-continuing
+ Funcon continue
+ Funcon handle-continue
+][
+ Datatype continuations
+ Funcon continuation
+ Entity plug-signal
+ Funcon hole
+ Funcon resume-continuation
+ Entity control-signal
+ Funcon control
+ Funcon delimit-current-continuation Alias delimit-cc
+][
+ Type values Alias vals
+ Type value-types Alias types
+ Type empty-type
+ Funcon is-in-type Alias is
+ Funcon is-value Alias is-val
+ Funcon when-true Alias when
+ Type cast-to-type Alias cast
+ Type ground-values Alias ground-vals
+ Funcon is-equal Alias is-eq
+][
+ Datatype booleans Alias bools
+ Funcon true
+ Funcon false
+ Funcon not
+ Funcon implies
+ Funcon and
+ Funcon or
+ Funcon exclusive-or Alias xor
+][
+ Type integers Alias ints
+ Type integers-from Alias from
+ Type integers-up-to Alias up-to
+ Type bounded-integers Alias bounded-ints
+ Type positive-integers Alias pos-ints
+ Type negative-integers Alias neg-ints
+ Type natural-numbers Alias nats
+ Funcon natural-successor Alias nat-succ
+ Funcon natural-predecessor Alias nat-pred
+ Funcon integer-add Alias int-add
+ Funcon integer-subtract Alias int-sub
+ Funcon integer-multiply Alias int-mul
+ Funcon integer-divide Alias int-div
+ Funcon integer-modulo Alias int-mod
+ Funcon integer-power Alias int-pow
+ Funcon integer-absolute-value Alias int-abs
+ Funcon integer-negate Alias int-neg
+ Funcon integer-is-less Alias is-less
+ Funcon integer-is-less-or-equal Alias is-less-or-equal
+ Funcon integer-is-greater Alias is-greater
+ Funcon integer-is-greater-or-equal Alias is-greater-or-equal
+ Funcon binary-natural Alias binary
+ Funcon octal-natural Alias octal
+ Funcon decimal-natural Alias decimal
+ Funcon hexadecimal-natural Alias hexadecimal
+ Funcon integer-sequence
+][
+ Datatype float-formats
+ Funcon binary32
+ Funcon binary64
+ Funcon binary128
+ Funcon decimal64
+ Funcon decimal128
+ Type floats
+ Funcon float
+ Funcon quiet-not-a-number Alias qNaN
+ Funcon signaling-not-a-number Alias sNaN
+ Funcon positive-infinity Alias pos-inf
+ Funcon negative-infinity Alias neg-inf
+ Funcon float-convert
+ Funcon float-equal
+ Funcon float-is-less
+ Funcon float-is-less-or-equal
+ Funcon float-is-greater
+ Funcon float-is-greater-or-equal
+ Funcon float-negate
+ Funcon float-absolute-value
+ Funcon float-add
+ Funcon float-subtract
+ Funcon float-multiply
+ Funcon float-multiply-add
+ Funcon float-divide
+ Funcon float-remainder
+ Funcon float-sqrt
+ Funcon float-integer-power
+ Funcon float-float-power
+ Funcon float-round-ties-to-even
+ Funcon float-round-ties-to-infinity
+ Funcon float-floor
+ Funcon float-ceiling
+ Funcon float-truncate
+ Funcon float-pi
+ Funcon float-e
+ Funcon float-log
+ Funcon float-log10
+ Funcon float-exp
+ Funcon float-sin
+ Funcon float-cos
+ Funcon float-tan
+ Funcon float-asin
+ Funcon float-acos
+ Funcon float-atan
+ Funcon float-sinh
+ Funcon float-cosh
+ Funcon float-tanh
+ Funcon float-asinh
+ Funcon float-acosh
+ Funcon float-atanh
+ Funcon float-atan2
+][
+ Type characters Alias chars
+ Datatype unicode-characters Alias unicode-chars
+ Type unicode-points
+ Funcon unicode-character Alias unicode-char
+ Funcon unicode-point Alias unicode
+ Type basic-multilingual-plane-characters Alias bmp-chars
+ Type basic-multilingual-plane-points
+ Type iso-latin-1-characters Alias latin-1-chars
+ Type iso-latin-1-points
+ Type ascii-characters Alias ascii-chars
+ Type ascii-points
+ Funcon ascii-character Alias ascii-char
+ Funcon utf-8
+ Funcon utf-16
+ Funcon utf-32
+ Funcon backspace
+ Funcon horizontal-tab
+ Funcon line-feed
+ Funcon form-feed
+ Funcon carriage-return
+ Funcon double-quote
+ Funcon single-quote
+ Funcon backslash
+][
+ Datatype null-type
+ Funcon null-value Alias null
+][
+ Funcon length
+ Funcon index
+ Funcon is-in
+ Funcon first
+ Funcon second
+ Funcon third
+ Funcon first-n
+ Funcon drop-first-n
+ Funcon reverse
+ Funcon n-of
+ Funcon intersperse
+][
+ Funcon datatype-value
+ Funcon datatype-value-id
+ Funcon datatype-value-elements
+][
+ Datatype tuples
+ Funcon tuple-elements
+ Funcon tuple-zip
+][
+ Datatype lists
+ Funcon list
+ Funcon list-elements
+ Funcon list-nil Alias nil
+ Funcon list-cons Alias cons
+ Funcon list-head Alias head
+ Funcon list-tail Alias tail
+ Funcon list-length
+ Funcon list-append
+][
+ Type strings
+ Funcon string
+ Funcon string-append
+ Funcon to-string
+][
+ Datatype vectors
+ Funcon vector
+ Funcon vector-elements
+][
+ Type bits
+ Datatype bit-vectors
+ Funcon bit-vector
+ Type bytes Alias octets
+ Funcon bit-vector-not
+ Funcon bit-vector-and
+ Funcon bit-vector-or
+ Funcon bit-vector-xor
+ Funcon bit-vector-shift-left
+ Funcon bit-vector-logical-shift-right
+ Funcon bit-vector-arithmetic-shift-right
+ Funcon integer-to-bit-vector
+ Funcon bit-vector-to-integer
+ Funcon bit-vector-to-natural
+ Funcon unsigned-bit-vector-maximum
+ Funcon signed-bit-vector-maximum
+ Funcon signed-bit-vector-minimum
+ Funcon is-in-signed-bit-vector
+ Funcon is-in-unsigned-bit-vector
+][
+ Type sets
+ Funcon set
+ Funcon set-elements
+ Funcon is-in-set
+ Funcon is-subset
+ Funcon set-insert
+ Funcon set-unite
+ Funcon set-intersect
+ Funcon set-difference
+ Funcon set-size
+ Funcon some-element
+ Funcon element-not-in
+][
+ Type maps
+ Funcon map
+ Funcon map-elements
+ Funcon map-lookup Alias lookup
+ Funcon map-domain Alias dom
+ Funcon map-override
+ Funcon map-unite
+ Funcon map-delete
+][
+ Type multisets
+ Funcon multiset
+ Funcon multiset-elements
+ Funcon multiset-occurrences
+ Funcon multiset-insert
+ Funcon multiset-delete
+ Funcon is-submultiset
+][
+ Datatype trees
+ Funcon tree
+ Funcon tree-root-value
+ Funcon tree-branch-sequence
+ Funcon single-branching-sequence
+ Funcon forest-root-value-sequence
+ Funcon forest-branch-sequence
+ Funcon forest-value-sequence
+][
+ Type directed-graphs
+ Funcon is-cyclic
+ Funcon topological-sort
+][
+ Datatype references
+ Funcon reference
+ Type pointers
+ Funcon dereference
+][
+ Datatype records
+ Funcon record
+ Funcon record-map
+ Funcon record-select
+][
+ Datatype variants
+ Funcon variant
+ Funcon variant-id
+ Funcon variant-value
+][
+ Datatype classes
+ Funcon class
+ Funcon class-instantiator
+ Funcon class-feature-map
+ Funcon class-superclass-name-sequence
+ Funcon class-name-tree
+ Funcon is-subclass-name
+ Funcon class-name-single-inheritance-feature-map
+][
+ Datatype objects
+ Funcon object
+ Funcon object-identity
+ Funcon object-class-name
+ Funcon object-feature-map
+ Funcon object-subobject-sequence
+ Funcon object-tree
+ Funcon object-single-inheritance-feature-map
+][
+ Type abstractions
+ Funcon abstraction
+ Funcon closure
+ Funcon enact
+][
+ Datatype functions
+ Funcon function
+ Funcon apply
+ Funcon supply
+ Funcon compose
+ Funcon uncurry
+ Funcon curry
+ Funcon partial-apply
+][
+ Datatype patterns
+ Funcon pattern
+ Funcon pattern-any
+ Funcon pattern-bind
+ Funcon pattern-type
+ Funcon pattern-else
+ Funcon pattern-unite
+ Funcon match
+ Funcon match-loosely
+ Funcon case-match
+ Funcon case-match-loosely
+ Funcon case-variant-value
+][
+ Datatype functions
+ Funcon function
+ Funcon apply
+ Funcon supply
+ Funcon compose
+ Funcon uncurry
+ Funcon curry
+ Funcon partial-apply
+]Meta-variables
+ T, T′, T1, T2 <: valuesDatatype
+ functions(T,T′) ::= function(A:abstractions(T=>T′))functions(T, T′) consists of abstractions whose bodies may depend on
+ a given value of type T, and whose executions normally compute values
+ of type T′.
+ function(abstraction(X)) evaluates to a function with dynamic bindings,
+ function(closure(X)) computes a function with static bindings.
+
+
+
+Funcon
+ apply(_:functions(T, T′), _:T) : =>T′apply(F, V) applies the function F to the argument value V.
+ This corresponds to call by value; using thunks as argument values
+ corresponds to call by name. Moreover, using tuples as argument values
+ corresponds to application to multiple arguments.
+
+
+
+
+
+
+
+ supply(F, V) determines the argument value of a function application,
+ but returns a thunk that defers executing the body of the function.
+
+Rule
+ supply(function(abstraction(X)), V:T) ~> thunk(abstraction(give(V, X)))compose(F2, F1) returns the function that applies F1 to its argument,
+ then applies F2 to the result of F1.
+
+Rule
+ compose(function(abstraction(Y)), function(abstraction(X)))
+ ~> function(abstraction(give(X, Y)))Funcon
+ uncurry(F:functions(T1, functions(T2, T′))) :
+ =>functions(tuples(T1, T2), T′)
+ ~> function(abstraction(
+ apply(
+ apply(F, checked index(1, tuple-elements given)),
+ checked index(2, tuple-elements given))))uncurry(F) takes a curried function F and returns a function that takes
+ a pair of arguments..
+
+
+
+Funcon
+ curry(F:functions(tuples(T1, T2), T′)) : =>functions(T1, functions(T2, T′))
+ ~> function(abstraction(partial-apply(F, given)))curry(F) takes a function F that takes a pair of arguments, and returns
+ the corresponding 'curried' function.
+
+
+
+Funcon
+ partial-apply(F:functions(tuples(T1, T2), T′), V:T1) : =>functions(T2, T′)
+ ~> function(abstraction(apply(F,tuple(V,given))))partial-apply(F, V) takes a function F that takes a pair of arguments,
+ and determines the first argument, returning a function of the second
+ argument.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Functions.cbs]: Functions.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Values/Abstraction/Functions/Functions.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/apply.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/apply.config
new file mode 100644
index 0000000..fea3d2d
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/apply.config
@@ -0,0 +1,16 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ apply(
+ sequential(print 1, function abstraction print given),
+ sequential(print 2 , 3))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3];
+//Also:
+// standard-out: [2, 1, 3];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/compose.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/compose.config
new file mode 100644
index 0000000..e4dc260
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/compose.config
@@ -0,0 +1,20 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ scope(
+ bind-value("f",
+ function abstraction
+ sequential(print given, integer-add(1,given))),
+ print apply(
+ compose(
+ bound-value"f",
+ function abstraction sequential(print 1, 2)),
+ 99))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/curry.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/curry.config
new file mode 100644
index 0000000..9ba8690
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/curry.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ scope(
+ bind-value("f",
+ function abstraction print given),
+ apply(
+ apply(curry(bound-value"f"), 1),
+ 2))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [tuple(1,2)];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-abstraction.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-abstraction.config
new file mode 100644
index 0000000..a0008dd
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-abstraction.config
@@ -0,0 +1,27 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ scope(
+ bind-value("x",99),
+ give(
+ 99,
+ give(
+ function abstraction(
+ sequential(
+ print given,
+ print bound-value"x")),
+ scope(
+ bind-value("x",4),
+ apply(
+ sequential(print 1, given),
+ sequential(print 2, 3))))))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, 4];
+//Also:
+// standard-out: [2, 1, 3, 4];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-closure.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-closure.config
new file mode 100644
index 0000000..7d4b62f
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/function-closure.config
@@ -0,0 +1,27 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ scope(
+ bind-value("x",4),
+ give(
+ 99,
+ give(
+ function closure(
+ sequential(
+ print given,
+ print bound-value"x")),
+ scope(
+ bind-value("x",99),
+ apply(
+ sequential(print 1, given),
+ sequential(print 2, 3))))))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3, 4];
+//Also:
+// standard-out: [2, 1, 3, 4];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/partial-apply.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/partial-apply.config
new file mode 100644
index 0000000..39c4c87
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/partial-apply.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ scope(
+ bind-value("f",
+ function abstraction print given),
+ apply(
+ partial-apply(bound-value"f", 1),
+ 2))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [tuple(1,2)];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/supply.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/supply.config
new file mode 100644
index 0000000..078ff1a
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/supply.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ force(
+ supply(
+ sequential(print 1, function abstraction print given),
+ sequential(print 2 , 3)))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2, 3];
+//Also:
+// standard-out: [2, 1, 3];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/uncurry.config b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/uncurry.config
new file mode 100644
index 0000000..1664459
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Functions/tests/uncurry.config
@@ -0,0 +1,17 @@
+general {
+ funcon-term:
+ initialise-giving
+ initialise-binding
+ scope(
+ bind-value("f",
+ uncurry function abstraction
+ sequential(print given,
+ function abstraction print given)),
+ apply(bound-value"f", tuple(1,2)))
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 2];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/Generic.cbs b/IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/Generic.cbs
new file mode 100644
index 0000000..3710dd5
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/Generic.cbs
@@ -0,0 +1,49 @@
+### Generic abstractions
+
+[
+ Type abstractions
+ Funcon abstraction
+ Funcon closure
+ Funcon enact
+]
+
+
+Meta-variables
+ T <: values
+ T? <: values?
+
+
+Type
+ abstractions(_:computation-types)
+
+
+Funcon
+ abstraction(_:T?=>T) : abstractions(T?=>T)
+/*
+ The funcon `abstraction(X)` forms abstraction values from computations.
+
+ References to bindings of identifiers in `X` are dynamic.
+ The funcon `closure(X)` forms abstractions with static bindings.
+*/
+
+
+Funcon
+ closure(_:T?=>T) : =>abstractions(T?=>T)
+/*
+ `closure(X)` computes a closed abstraction from the computation `X`.
+ In contrast to `abstraction(X)`, references to bindings of identifiers
+ in `X` are static. Moreover, `closure(X)` is not a value constructor,
+ so it cannot be used in pattern terms in rules.
+*/
+Rule
+ environment(Rho) |- closure(X) ---> abstraction(closed(scope(Rho, X)))
+
+
+Funcon
+ enact(_:abstractions(T?=>T)) : T?=>T
+/*
+ `enact(A)` executes the computation of the abstraction `A`,
+ with access to all the current entities.
+*/
+Rule
+ enact(abstraction(X)) ~> X
diff --git a/IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/index.md b/IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/index.md
new file mode 100644
index 0000000..847d7d7
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Abstraction/Generic/index.md
@@ -0,0 +1,85 @@
+---
+layout: default
+title: "Generic"
+parent: Abstraction
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Generic.cbs]
+-----------------------------
+
+### Generic abstractions
+
+[
+ Type abstractions
+ Funcon abstraction
+ Funcon closure
+ Funcon enact
+]Type
+ abstractions(_:computation-types)Funcon
+ abstraction(_:T?=>T) : abstractions(T?=>T)abstraction(X) forms abstraction values from computations.
+
+ References to bindings of identifiers in X are dynamic.
+ The funcon closure(X) forms abstractions with static bindings.
+
+
+
+Funcon
+ closure(_:T?=>T) : =>abstractions(T?=>T)closure(X) computes a closed abstraction from the computation X.
+ In contrast to abstraction(X), references to bindings of identifiers
+ in X are static. Moreover, closure(X) is not a value constructor,
+ so it cannot be used in pattern terms in rules.
+
+Rule
+ environment(Rho) |- closure(X) ---> abstraction(closed(scope(Rho, X)))Funcon
+ enact(_:abstractions(T?=>T)) : T?=>Tenact(A) executes the computation of the abstraction A,
+ with access to all the current entities.
+
+Rule
+ enact(abstraction(X)) ~> X[
+ Datatype patterns
+ Funcon pattern
+ Funcon pattern-any
+ Funcon pattern-bind
+ Funcon pattern-type
+ Funcon pattern-else
+ Funcon pattern-unite
+ Funcon match
+ Funcon match-loosely
+ Funcon case-match
+ Funcon case-match-loosely
+ Funcon case-variant-value
+]Meta-variables
+ T, T′ <: valuesDatatype
+ patterns ::= pattern(_:abstractions(values=>environments))patterns is the type of simple patterns that can match values of a
+ particular type.
+
+ pattern(abstraction(X)) constructs a pattern with dynamic bindings, and
+ pattern(closure(X)) computes a pattern with static bindings. However,
+ there is no difference between dynamic and static bindings when the pattern
+ is matched in the same scope where it is constructed.
+
+
+
+Funcon
+ pattern-any : =>patterns
+ ~> pattern(abstraction(map( )))pattern-any matches any value, computing the empty environment.
+
+
+
+Funcon
+ pattern-bind(I:identifiers) : =>patterns
+ ~> pattern(abstraction(bind-value(I, given)))pattern-bind(I) matches any value, computing the environment binding I
+ to that value.
+
+
+
+Funcon
+ pattern-type(T) : =>patterns
+ ~> pattern(abstraction(if-true-else(is-in-type(given, T), map( ), fail)))pattern-type(T) matches any value of type T, computing the empty
+ environment.
+
+Funcon
+ pattern-else(_:values, _:values) : =>patterns
+Rule
+ pattern-else(P1:values, P2:values)
+ ~> pattern(abstraction(else(match(given, P1), match(given, P2))))pattern-else(P1, P2) matches all values matched by P1 or by P2.
+ If a value matches P1, that match gives the computed environment;
+ if a value does not match P1 but matches P2, that match gives
+ the computed environment; otherwise the match fails.
+
+Funcon
+ pattern-unite(_:values, _:values) : =>patterns
+Rule
+ pattern-unite(P1:values, P2:values)
+ ~> pattern(abstraction(collateral(match(given, P1), match(given, P2))))pattern-unite(P1, P2) matches all values matched by both P1 and P2,
+ then uniting the computed environments, which fails if the domains of the
+ environments overlap.
+
+
+
+#### Pattern matching
+
+Funcon
+ match(_:values, _:values) : =>environmentsmatch(V, P) takes a (potentially structured) value V and a
+ (potentially structured) pattern P. Provided that the structure and all
+ components of P exactly match the structure and corresponding components
+ of V, the environments computed by the simple pattern matches are united.
+
+Rule
+ match(V:values, pattern(abstraction(X))) ~> give(V, X)
+Rule
+ I2 =/= "pattern"
+ --------------------------------------------
+ match(datatype-value(I1:identifiers, V1*:values*),
+ datatype-value(I2:identifiers, V2*:values*))
+ ~> sequential(
+ check-true(is-equal(I1, I2)),
+ check-true(is-equal(length V1*, length V2*)),
+ collateral(interleave-map(
+ match(tuple-elements(given)),
+ tuple-zip(tuple(V1*), tuple(V2*)))))
+Rule
+ dom(M2) == {}
+ ------------------------------------------------------
+ match(M1:maps(_,_), M2:maps(_,_))
+ ~> if-true-else(is-equal(dom(M1), {}), map( ), fail)
+Rule
+ dom(M2) =/= {}
+ some-element(dom(M2)) ~> K
+ -------------------------------------------------------
+ match(M1:maps(_,_), M2:maps(_,_))
+ ~> if-true-else(
+ is-in-set(K, dom(M1)),
+ collateral(
+ match(map-lookup(M1, K), map-lookup(M2, K)),
+ match(map-delete(M1, {K}), map-delete(M2, {K}))),
+ fail)
+Rule
+ P : ~(datatype-values|maps(_,_))
+ -----------------------------------------------
+ match(V:values, P:values)
+ ~> if-true-else(is-equal(V, P), map( ), fail)Funcon
+ match-loosely(_:values, _:values) : =>environmentsmatch-loosely(V, P) takes a (potentially structured) value V and a
+ (potentially structured) pattern P. Provided that the structure and all
+ components of P loosely match the structure and corresponding components
+ of V, the environments computed by the simple pattern matches are united.
+
+Rule
+ match-loosely(V:values, pattern(abstraction(X))) ~> give(V, X)
+Rule
+ I2 =/= "pattern"
+ ---------------------------------------------------
+ match-loosely(datatype-value(I1:identifiers, V1*:values*),
+ datatype-value(I2:identifiers, V2*:values*))
+ ~> sequential(
+ check-true(is-equal(I1, I2)),
+ check-true(is-equal(length V1*, length V2*)),
+ collateral(interleave-map(
+ match-loosely(tuple-elements(given)),
+ tuple-zip(tuple(V1*), tuple(V2*)))))
+Rule
+ dom(M2) == {}
+ -------------------------------------------------
+ match-loosely(M1:maps(_,_), M2:maps(_,_)) ~> map()
+Rule
+ dom(M2) =/= {}
+ some-element(dom(M2)) ~> K
+ --------------------------------------------------------------
+ match-loosely(M1:maps(_,_), M2:maps(_,_))
+ ~> if-true-else(
+ is-in-set(K, dom(M1)),
+ collateral(
+ match-loosely(map-lookup(M1, K), map-lookup(M2, K)),
+ match-loosely(map-delete(M1, {K}), map-delete(M2, {K}))),
+ fail)
+Rule
+ P : ~(datatype-values|maps(_,_))
+ -------------------------------------------
+ match-loosely(DV:values, P:values)
+ ~> if-true-else(is-equal(DV, P), map( ), fail)Funcon
+ case-match(_:values, _:=>T′) : =>T′case-match(P, X) matches P exactly to the given value.
+ If the match succeeds, the computed bindings have scope X.
+
+
+
+
+
+Funcon
+ case-match-loosely(_:values, _:=>T′) : =>T′case-match(P, X) matches P loosely to the given value.
+ If the match succeeds, the computed bindings have scope X.
+
+Rule
+ case-match-loosely(P:values, X) ~> scope(match-loosely(given, P), X)Funcon
+ case-variant-value(_:identifiers) : =>valuescase-variant-value(I) matches values of variant I, then
+ giving the value contained in the variant.
+
+Rule
+ case-variant-value(I:identifiers) ~>
+ case-match(variant(I, pattern-any), variant-value(given))Meta-variables
+ T <: valuesDatatype
+ thunks(T) ::= thunk(_:abstractions(()=>T))thunks(T) consists of abstractions whose bodies do not depend on
+ a given value, and whose executions normally compute values of type T.
+ thunk(abstraction(X)) evaluates to a thunk with dynamic bindings,
+ thunk(closure(X)) computes a thunk with static bindings.
+
+
+
+Funcon
+ force(_:thunks(T)) : =>Tforce(H) enacts the abstraction of the thunk H.
+
+Rule
+ force(thunk(abstraction(X))) ~> no-given(X)[
+ Type bits
+ Datatype bit-vectors
+ Funcon bit-vector
+ Type bytes Alias octets
+ Funcon bit-vector-not
+ Funcon bit-vector-and
+ Funcon bit-vector-or
+ Funcon bit-vector-xor
+ Funcon bit-vector-shift-left
+ Funcon bit-vector-logical-shift-right
+ Funcon bit-vector-arithmetic-shift-right
+ Funcon integer-to-bit-vector
+ Funcon bit-vector-to-integer
+ Funcon bit-vector-to-natural
+ Funcon unsigned-bit-vector-maximum
+ Funcon signed-bit-vector-maximum
+ Funcon signed-bit-vector-minimum
+ Funcon is-in-signed-bit-vector
+ Funcon is-in-unsigned-bit-vector
+]Type
+ bits ~> booleansfalse represents the absence of a bit, true its presence.
+
+
+
+#### Bit vectors
+
+Datatype
+ bit-vectors(N:natural-numbers) ::= bit-vector(_:bits^N)Type
+ bytes ~> bit-vectors(8)
+Alias
+ octets = bytesMeta-variables
+ BT <: bit-vectors(_)Built-in Funcon
+ bit-vector-not(_:BT) : =>BTBuilt-in Funcon
+ bit-vector-and(_:BT, _:BT) : =>BTBuilt-in Funcon
+ bit-vector-or(_:BT, _:BT) : =>BTBuilt-in Funcon
+ bit-vector-xor(_:BT, _:BT) : =>BTbooleans
+ to bit-vectors(N) of the same length.
+
+
+Built-in Funcon
+ bit-vector-shift-left(_:BT, _:natural-numbers) : BTBuilt-in Funcon
+ bit-vector-logical-shift-right(_:BT, _:natural-numbers) : BTBuilt-in Funcon
+ bit-vector-arithmetic-shift-right(_:BT, _:natural-numbers) : BTBuilt-in Funcon
+ integer-to-bit-vector(_:integers, N:natural-numbers) : bit-vectors(N)integer-to-bit-vector(M, N) converts an integer M to a bit-vector of
+ length N, using Two's Complement representation. If the integer is out of
+ range of the representation, it will wrap around (modulo 2^N).
+
+
+Built-in Funcon
+ bit-vector-to-integer(_:BT) : =>integersbit-vector-to-integer(B) interprets a bit-vector BV as an integer
+ in Two's Complement representation.
+
+
+Built-in Funcon
+ bit-vector-to-natural(_:BT) : =>natural-numbersbit-vector-to-natural(BV) interprets a bit-vector BV as a natural number
+ in unsigned representation.
+
+
+Funcon
+ unsigned-bit-vector-maximum(N:natural-numbers) : =>natural-numbers
+ ~> integer-subtract(integer-power(2, N), 1)Funcon
+ signed-bit-vector-maximum(N:natural-numbers) : =>integers
+ ~> integer-subtract(integer-power(2, integer-subtract(N, 1)), 1)Funcon
+ signed-bit-vector-minimum(N:natural-numbers) : =>integers
+ ~> integer-negate(integer-power(2, integer-subtract(N, 1)))Funcon
+ is-in-signed-bit-vector(M:integers, N:natural-numbers) : =>booleans
+ ~> and(integer-is-less-or-equal(M, signed-bit-vector-maximum(N)),
+ integer-is-greater-or-equal(M, signed-bit-vector-minimum(N)))Funcon
+ is-in-unsigned-bit-vector(M:integers, N:natural-numbers) : =>booleans
+ ~> and(integer-is-less-or-equal(M, unsigned-bit-vector-maximum(N)),
+ integer-is-greater-or-equal(M, 0))[
+ Datatype classes
+ Funcon class
+ Funcon class-instantiator
+ Funcon class-feature-map
+ Funcon class-superclass-name-sequence
+ Funcon class-name-tree
+ Funcon is-subclass-name
+ Funcon class-name-single-inheritance-feature-map
+]Datatype
+ classes ::=
+ class(_:thunks(references(objects)), _:environments, _:identifiers*)class(Thunk, Env, C*) is a class with:
+ * a thunk Thunk for instantiating the class,
+ * an environment Env with the features declared by the class, and
+ * a sequence C* of names of direct superclasses.
+ class(Thunk, Env) is a base class, having no superclasses.
+ class(Thunk, Env, C) is a class with a single superclass.
+
+ Class instantiation forces its thunk to compute a reference to an object.
+
+ Features are inherited from superclasses. When features with the same name
+ are declared in simultaneously inherited classes, the order of the superclass
+ identifiers in C* may affect resolution of references to features.
+ Overloading of feature names is supported by using type maps as features.
+
+ The class table is represented by binding class names to classes.
+ The class superclass hierarchy is assumed to be acyclic.
+
+Funcon
+ class-instantiator(_:classes) : =>thunks(references(objects))
+Rule
+ class-instantiator
+ class(Thunk:thunks(_), Envs:environments, C*:identifiers*) ~> ThunkFuncon
+ class-feature-map(_:classes) : =>environments
+Rule
+ class-feature-map
+ class(Thunk:thunks(_), Env:environments, C*:identifiers*) ~> EnvFuncon
+ class-superclass-name-sequence(_:classes) : =>identifiers*
+Rule
+ class-superclass-name-sequence
+ class(Thunk:thunks(_), Env:environments, C*:identifiers*) ~> C*Funcon
+ class-name-tree(_:identifiers) : =>trees(identifiers)class-name-tree C forms a tree where the branches are the class name
+ trees for the superclasses of C.
+
+Rule
+ class-name-tree(C : identifiers)
+ ~> tree(C,
+ interleave-map(
+ class-name-tree given,
+ class-superclass-name-sequence bound-value C))Funcon
+ is-subclass-name(C:identifiers, C′:identifiers) : =>booleans
+ ~> is-in-set(C, { forest-value-sequence class-name-tree C′ })is-subclass-name(C, C′) does not depend on the order of
+ the names in forest-value-sequence class-name-tree C′.
+
+
+
+Funcon
+ class-name-single-inheritance-feature-map(C:identifiers) : =>environments
+ ~> map-override interleave-map(
+ class-feature-map bound-value given,
+ single-branching-sequence class-name-tree C)[
+ Type datatype-values
+ Funcon datatype-value
+ Funcon datatype-value-id
+ Funcon datatype-value-elements
+]T to refer to a fresh value
+ constructor in types, and asserts T <: datatype-values.
+
+ Each constructor funcon 'F(_:T1,...,_:Tn)' of the datatype declaration
+ generates values in T of the form datatype-value("F", V1, ..., Vn) from
+ V1:T1, ..., Vn:Tn.
+
+ Note that a computation X cannot be directly included in datatype values:
+ it is necessary to encapsulate it in abstraction(X).
+
+ 'Datatype T', followed by declarations of constructor funcons for 'T',
+ allows specification of GADTs.
+
+
+Built-in Type
+ datatype-valuesBuilt-in Funcon
+ datatype-value(_:identifiers, _:values*) : datatype-valuesFuncon
+ datatype-value-id(_:datatype-values) : =>identifiers
+Rule
+ datatype-value-id(datatype-value(I:identifiers, _*:values*)) ~> IFuncon
+ datatype-value-elements(_:datatype-values) : =>values*
+Rule
+ datatype-value-elements(datatype-value(_:identifiers, V*:values*)) ~> V*[
+ Type directed-graphs
+ Funcon is-cyclic
+ Funcon topological-sort
+]Meta-variables
+ GT <: ground-valuesdirected-graphs(GT) models directed graphs with vertices of type GT,
+ represented as maps from vertices to the set of vertices to which the
+ vertex has an edge. E.g., the graph
+
+ (1)--->(2)
+
+ would be represented as { 1 |-> {2}, 2 |-> {} }
+
+
+Built-in Funcon
+ is-cyclic(_:directed-graphs(GT)) : =>booleansBuilt-in Funcon
+ topological-sort(_:directed-graphs(GT)) : =>(GT)*topological-sort(DG) returns a topological ordering of the vertices
+ of the graph DG, as a sequence of vertices, provided that DG is not
+ cyclic.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Graphs.cbs]: Graphs.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Values/Composite/Graphs/Graphs.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Lists/Lists.cbs b/IBAF-cbs/Funcons-beta/Values/Composite/Lists/Lists.cbs
new file mode 100644
index 0000000..bb4312d
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Lists/Lists.cbs
@@ -0,0 +1,98 @@
+### Lists
+
+[
+ Datatype lists
+ Funcon list
+ Funcon list-elements
+ Funcon list-nil Alias nil
+ Funcon list-cons Alias cons
+ Funcon list-head Alias head
+ Funcon list-tail Alias tail
+ Funcon list-length
+ Funcon list-append
+]
+
+
+Meta-variables
+ T <: values
+
+
+Datatype
+ lists(T) ::= list(_:(T)*)
+/*
+ `lists(T)` is the type of possibly-empty finite lists `[V1,...,Vn]`
+ where `V1:T`, ..., `Vn:T`.
+
+ N.B. `[T]` is always a single list value, and *not* interpreted as the
+ type `lists(T)`.
+
+ The notation `[V1, ..., Vn]` for `list(V1, ..., Vn)` is built-in.
+*/
+Assert
+ [V*:values*] == list(V*)
+
+
+Funcon
+ list-elements(_:lists(T)) : =>(T)*
+Rule
+ list-elements(list(V*:values*)) ~> V*
+
+
+Funcon
+ list-nil : =>lists(_)
+ ~> [ ]
+Alias
+ nil = list-nil
+
+
+Funcon
+ list-cons(_:T, _:lists(T)) : =>lists(T)
+Alias
+ cons = list-cons
+Rule
+ list-cons(V:values, [V*:values*]) ~> [V, V*]
+
+
+Funcon
+ list-head(_:lists(T)) : =>(T)?
+Alias
+ head = list-head
+Rule
+ list-head[V:values, _*:values*] ~> V
+Rule
+ list-head[ ] ~> ( )
+
+
+Funcon
+ list-tail(_:lists(T)) : =>(lists(T))?
+Alias
+ tail = list-tail
+Rule
+ list-tail[_:values, V*:values*] ~> [V*]
+Rule
+ list-tail[ ] ~> ( )
+
+
+Funcon
+ list-length(_:lists(T)) : =>natural-numbers
+Rule
+ list-length[V*:values*] ~> length(V*)
+
+
+Funcon
+ list-append(_:(lists(T))*) : =>lists(T)
+Rule
+ list-append([V1*:values*], [V2*:values*]) ~> [V1*, V2*]
+Rule
+ list-append(L1:lists(_), L2:lists(_), L3:lists(_), L*:(lists(_))*)
+ ~> list-append(L1, list-append(L2, L3, L*))
+Rule
+ list-append( ) ~> [ ]
+Rule
+ list-append(L:lists(_)) ~> L
+
+
+/*
+ Datatypes of infinite and possibly-infinite lists can be specified as
+ algebraic datatypes using abstractions.
+*/
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Lists/index.md b/IBAF-cbs/Funcons-beta/Values/Composite/Lists/index.md
new file mode 100644
index 0000000..076e88d
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Lists/index.md
@@ -0,0 +1,132 @@
+---
+layout: default
+title: "Lists"
+parent: Composite
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Lists.cbs]
+-----------------------------
+
+### Lists
+
+[
+ Datatype lists
+ Funcon list
+ Funcon list-elements
+ Funcon list-nil Alias nil
+ Funcon list-cons Alias cons
+ Funcon list-head Alias head
+ Funcon list-tail Alias tail
+ Funcon list-length
+ Funcon list-append
+]Meta-variables
+ T <: valuesDatatype
+ lists(T) ::= list(_:(T)*)lists(T) is the type of possibly-empty finite lists [V1,...,Vn]
+ where V1:T, ..., Vn:T.
+
+ N.B. [T] is always a single list value, and *not* interpreted as the
+ type lists(T).
+
+ The notation [V1, ..., Vn] for list(V1, ..., Vn) is built-in.
+
+
+
+Funcon
+ list-elements(_:lists(T)) : =>(T)*
+Rule
+ list-elements(list(V*:values*)) ~> V*Funcon
+ list-length(_:lists(T)) : =>natural-numbers
+Rule
+ list-length[V*:values*] ~> length(V*)Funcon
+ list-append(_:(lists(T))*) : =>lists(T)
+Rule
+ list-append([V1*:values*], [V2*:values*]) ~> [V1*, V2*]
+Rule
+ list-append(L1:lists(_), L2:lists(_), L3:lists(_), L*:(lists(_))*)
+ ~> list-append(L1, list-append(L2, L3, L*))
+Rule
+ list-append( ) ~> [ ]
+Rule
+ list-append(L:lists(_)) ~> L[
+ Type maps
+ Funcon map
+ Funcon map-elements
+ Funcon map-lookup Alias lookup
+ Funcon map-domain Alias dom
+ Funcon map-override
+ Funcon map-unite
+ Funcon map-delete
+]Meta-variables
+ GT <: ground-values
+ T? <: values?Built-in Type
+ maps(GT, T?)maps(GT, T?) is the type of possibly-empty finite maps from values of
+ type GT to optional values of type T?.
+
+
+
+
+
+ map(tuple(K1, V1?), ..., tuple(Kn, Vn?)) constructs a map from
+ K1 to V1?, ..., Kn to Vn?, provided that K1, ..., Kn
+ are distinct, otherwise the result is ( ).
+
+ Note that map(...) is not a constructor operation.
+
+ The built-in notation {K1|->V1?, ..., Kn|->Vn?} is equivalent to
+ map(tuple(K1, V1?), ..., tuple(Kn, Vn?)). Note however that in general,
+ maps cannot be identified with sets of tuples, since the values Vi? are
+ not restricted to ground-values.
+
+ When T? <: types, maps(GT, T?) <: types. The type MT:maps(GT, T?)
+ represents the set of value-maps MV:maps(GT, values?) such that
+ dom(MV) is a subset of dom(MT) and for all K in dom(MV),
+ map-lookup(MV, K) : map-lookup(MT, K).
+
+
+
+
+
+ The sequence of tuples (tuple(K1, V1?), ..., tuple(Kn, Vn?)) given by
+ map-elements(M) contains each mapped value Ki just once. The order of
+ the elements is unspecified, and may vary between maps.
+
+Assert
+ map(map-elements(M)) == MBuilt-in Funcon
+ map-lookup(_:maps(GT, T?), K:GT) : =>(T?)?
+Alias
+ lookup = map-lookupmap-lookup(M,K) gives the optional value to which K is mapped by M,
+ if any, and otherwise ( ).
+
+Built-in Funcon
+ map-domain(_:maps(GT, T?)) : =>sets(GT)
+Alias
+ dom = map-domainmap-domain(M) gives the set of values mapped by M.
+
+ map-lookup(M, K) is always ( ) when K is not in map-domain(M).
+
+
+
+
+
+ map-override(...) takes a sequence of maps. It returns the map whose
+ domain is the union of their domains, and which maps each of those values
+ to the same optional value as the first map in the sequence in whose domain
+ it occurs
+ .
+ When the domains of the M* are disjoint, map-override(M*) is equivalent
+ to map-unite(M*).
+
+
+
+
+
+ map-unite(...) takes a sequence of maps. It returns the map whose
+ domain is the union of their domains, and which maps each of those values
+ to the same optional value as the map in the sequence in whose domain it occurs,
+ provided that those domains are disjoint - otherwise the result is ( ).
+
+
+
+
+
+ map-delete(M, S) takes a map M and a set of values S, and returns the
+ map obtained from M by removing S from its domain.
+
+Assert
+ map-domain(map-delete(M, S)) == set-difference(map-domain(M), S)[
+ Type multisets
+ Funcon multiset
+ Funcon multiset-elements
+ Funcon multiset-occurrences
+ Funcon multiset-insert
+ Funcon multiset-delete
+ Funcon is-submultiset
+]Meta-variables
+ GT <: ground-valuesBuilt-in Type
+ multisets(GT)multisets(GT) is the type of possibly-empty finite multisets of elements
+ of GT.
+
+
+
+Built-in Funcon
+ multiset(_:(GT)*) : =>multisets(GT)multiset(...) is not a constructor operation. The order of
+ argument values is ignored, but duplicates are significant, e.g.,
+ multiset(1, 2, 2) is equivalent to multiset(2, 1, 2), but not to
+ multiset(1, 2) or multiset(2, 1).
+
+
+
+Built-in Funcon
+ multiset-elements(_:multisets(GT)) : =>(GT)*MS, the sequence of values V* returned by
+ multiset-elements(MS) contains each element of MS the same number of times
+ as MS does.
+ The order of the values in V* is unspecified, and may vary between multisets.
+
+Assert
+ multiset(multiset-elements(S)) == SBuilt-in Funcon
+ multiset-occurrences(_:GT, _:multisets(GT)) : =>natural-numbersmultiset-occurrences(GV, MS) returns the number of occurrences of GV
+ in MS.
+
+
+
+Built-in Funcon
+ multiset-insert(_:GT, _:natural-numbers, _:multisets(GT)) : =>multisets(GT)multiset-insert(GV, N, MS) returns the multiset that differs from MS
+ by containing N more copies of GV.
+
+
+
+Built-in Funcon
+ multiset-delete(_:multisets(GT), _:GT, _:natural-numbers) : =>multisets(GT)multiset-delete(MS, GV, N) removes N copies of V from the multiset MS,
+ or all copies of GV if there are fewer than N in MS.
+
+
+
+
+
+ is-submultiset(MS1, MS2) tests whether every element of MS1 has equal or
+ fewer occurrences in MS1 than in MS2.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Multisets.cbs]: Multisets.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Values/Composite/Multisets/Multisets.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Objects/Objects.cbs b/IBAF-cbs/Funcons-beta/Values/Composite/Objects/Objects.cbs
new file mode 100644
index 0000000..e59437b
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Objects/Objects.cbs
@@ -0,0 +1,81 @@
+### Objects
+
+[
+ Datatype objects
+ Funcon object
+ Funcon object-identity
+ Funcon object-class-name
+ Funcon object-feature-map
+ Funcon object-subobject-sequence
+ Funcon object-tree
+ Funcon object-single-inheritance-feature-map
+]
+
+
+Datatype
+ objects ::= object(_:atoms, _:identifiers, _:environments, _:objects*)
+/*
+ `object( A, C, Env, O*)` is an object:
+ * distinguished by an atom `A`,
+ * of a class named `C`,
+ * with an environment `Env` with the features of the object, and
+ * a sequence `O*` of subobjects of the direct superclasses of `C`.
+ `object( A, C, Env)` is an object of a base class.
+ `object( A, C, Env, O')` is an object of a class with a single superclass.
+ With multiple inheritance, subobjects due to repeated inheritance of the
+ same class may be shared.
+
+ Implementations of objects generally represent an object as a vector of
+ fields, and use pointers and offsets for efficient access to individual
+ fields. The representation of objects used in this specification is
+ independent of such implementation concerns.
+*/
+
+Funcon
+ object-identity(_:objects) : =>atoms
+Rule
+ object-identity
+ object(A:atoms, _:identifiers, _:environments, _*:objects*) ~> A
+
+Funcon
+ object-class-name(_:objects) : =>identifiers
+Rule
+ object-class-name
+ object(_:atoms, C:identifiers, _:environments, _*:objects*) ~> C
+
+Funcon
+ object-feature-map(_:objects) : =>environments
+Rule
+ object-feature-map
+ object(_:atoms, _:identifiers, Env:environments, _*:objects*) ~> Env
+
+Funcon
+ object-subobject-sequence(_:objects) : =>objects*
+Rule
+ object-subobject-sequence
+ object(_:atoms, _:identifiers, _:environments, O*:objects*) ~> O*
+
+
+Funcon
+ object-tree(_:objects) : =>trees(objects)
+/*
+ `object-tree O` forms a tree where the branches are the object trees for
+ the direct subobjects of `O`.
+*/
+Rule
+ object-tree(O:objects)
+ ~> tree(O,
+ interleave-map (
+ object-tree given,
+ object-subobject-sequence O))
+
+
+Funcon
+ object-single-inheritance-feature-map(O:objects) : =>environments
+ ~> map-override left-to-right-map(
+ object-feature-map given,
+ single-branching-sequence object-tree O)
+/*
+ For multiple inheritance, different resolution orders can be specified
+ by using difference linearisations of the object tree.
+*/
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Objects/index.md b/IBAF-cbs/Funcons-beta/Values/Composite/Objects/index.md
new file mode 100644
index 0000000..cf3572a
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Objects/index.md
@@ -0,0 +1,119 @@
+---
+layout: default
+title: "Objects"
+parent: Composite
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Objects.cbs]
+-----------------------------
+
+### Objects
+
+[
+ Datatype objects
+ Funcon object
+ Funcon object-identity
+ Funcon object-class-name
+ Funcon object-feature-map
+ Funcon object-subobject-sequence
+ Funcon object-tree
+ Funcon object-single-inheritance-feature-map
+]Datatype
+ objects ::= object(_:atoms, _:identifiers, _:environments, _:objects*)object( A, C, Env, O*) is an object:
+ * distinguished by an atom A,
+ * of a class named C,
+ * with an environment Env with the features of the object, and
+ * a sequence O* of subobjects of the direct superclasses of C.
+ object( A, C, Env) is an object of a base class.
+ object( A, C, Env, O′) is an object of a class with a single superclass.
+ With multiple inheritance, subobjects due to repeated inheritance of the
+ same class may be shared.
+
+ Implementations of objects generally represent an object as a vector of
+ fields, and use pointers and offsets for efficient access to individual
+ fields. The representation of objects used in this specification is
+ independent of such implementation concerns.
+
+Funcon
+ object-identity(_:objects) : =>atoms
+Rule
+ object-identity
+ object(A:atoms, _:identifiers, _:environments, _*:objects*) ~> AFuncon
+ object-class-name(_:objects) : =>identifiers
+Rule
+ object-class-name
+ object(_:atoms, C:identifiers, _:environments, _*:objects*) ~> CFuncon
+ object-feature-map(_:objects) : =>environments
+Rule
+ object-feature-map
+ object(_:atoms, _:identifiers, Env:environments, _*:objects*) ~> EnvFuncon
+ object-subobject-sequence(_:objects) : =>objects*
+Rule
+ object-subobject-sequence
+ object(_:atoms, _:identifiers, _:environments, O*:objects*) ~> O*object-tree O forms a tree where the branches are the object trees for
+ the direct subobjects of O.
+
+Rule
+ object-tree(O:objects)
+ ~> tree(O,
+ interleave-map (
+ object-tree given,
+ object-subobject-sequence O))Funcon
+ object-single-inheritance-feature-map(O:objects) : =>environments
+ ~> map-override left-to-right-map(
+ object-feature-map given,
+ single-branching-sequence object-tree O)[
+ Datatype records
+ Funcon record
+ Funcon record-map
+ Funcon record-select
+]Meta-variables
+ T <: valuesDatatype
+ records(T) ::= record(_:maps(identifiers,T))records(T) contains a map from identifiers to values of
+ type T.
+
+Funcon
+ record-map(_:records(T)) : =>maps(identifiers,T)
+Rule
+ record-map(record(M:maps(_,_))) ~> MFuncon
+ record-select(R:records(T), I:identifiers) : =>T?
+ ~> map-lookup(record-map(R), I)[
+ Datatype references
+ Funcon reference
+ Type pointers
+ Funcon pointer-null
+ Funcon dereference
+]Meta-variables
+ T <: valuesDatatype
+ references(T) ::= reference(_:T)Datatype
+ pointers(T) ::= pointer-null | { _:references(T) }Funcon
+ dereference(_:pointers(T)) : =>(T)?
+Rule
+ dereference(reference(V:T)) ~> V
+Rule
+ dereference(pointer-null) ~> ( )[
+ Funcon length
+ Funcon index
+ Funcon is-in
+ Funcon first
+ Funcon second
+ Funcon third
+ Funcon first-n
+ Funcon drop-first-n
+ Funcon reverse
+ Funcon n-of
+ Funcon intersperse
+]X1, ..., Xn is written X1,...,Xn.
+ A sequence with a single element X is identified with (and written) X.
+ An empty sequence is indicated by the absence of a term.
+ Any sequence X* can be enclosed in parentheses (X*), e.g.:
+ ( ), (1), (1,2,3). Superfluous commas are ignored.
+
+ The elements of a type sequence T1,...,Tn are the value sequences V1,...,Vn
+ where V1:T1, ..., Vn:Tn. The only element of the empty type sequence ( )
+ is the empty value sequence ( ).
+
+ (T)^N is equivalent to T,...,T with N occurrences of T.
+ (T)* is equivalent to the union of all (T)^N for N>=0,
+ (T)+ is equivalent to the union of all (T)^N for N>=1, and
+ (T)? is equivalent to T | ( ).
+ The parentheses around T above can be omitted when they are not needed for
+ disambiguation.
+
+ (Non-trivial) sequence types are not values, so not included in types.
+
+
+
+Meta-variables
+ T, T′ <: valuesFuncon
+ length(_:values*) : =>natural-numberslength(V*) gives the number of elements in V*.
+
+
+
+Funcon
+ is-in(_:values, _:values*) : =>booleans
+Rule
+ is-in(V:values ,V′:values, V*:values*) ~> or(is-equal(V, V′), is-in(V, V*))
+Rule
+ is-in(V:values, ( )) ~> falseFuncon
+ index(_:natural-numbers, _:values*) : =>values?index(N, V*) gives the Nth element of V*, if it exists, otherwise ( ).
+
+Rule
+ index(1, V:values, V*:values*) ~> V
+Rule
+ natural-predecessor(N) ~> N′
+ -----------------------------------------------------------------
+ index(N:positive-integers, _:values, V*:values*) ~> index(N′, V*)
+Rule
+ index(0, V*:values*) ~> ( )
+Rule
+ index(_:positive-integers, ( )) ~> ( )Funcon
+ third(_:values, _:values, _:T, _:values*) : =>T
+Rule
+ third(_:values, _:values, V:T, V*:values*) ~> VFuncon
+ first-n(_:natural-numbers, _:(T)*) : =>(T)*
+Rule
+ first-n(0, V*:(T)*) ~> ( )
+Rule
+ natural-predecessor(N) ~> N′
+ -----------------------------------------------------------------
+ first-n(N:positive-integers, V:T, V*:(T)*) ~> (V,first-n(N′, V*))
+Rule
+ first-n(N:positive-integers, ( )) ~> ( )Funcon
+ drop-first-n(_:natural-numbers, _:(T)*) : =>(T)*
+Rule
+ drop-first-n(0, V*:(T)*) ~> V*
+Rule
+ natural-predecessor(N) ~> N′
+ -----------------------------------------------------------------------
+ drop-first-n(N:positive-integers, _:T, V*:(T)*) ~> drop-first-n(N′, V*)
+Rule
+ drop-first-n(N:positive-integers, ( )) ~> ( )Funcon
+ reverse(_:(T)*) : =>(T)*
+Rule
+ reverse( ) ~> ( )
+Rule
+ reverse(V:T, V*:(T)*) ~> (reverse(V*), V)Funcon
+ n-of(N:natural-numbers, V:T) : =>(T)*
+Rule
+ n-of(0, _:T) ~> ( )
+Rule
+ natural-predecessor(N) ~> N′
+ --------------------------------------------------
+ n-of(N:positive-integers, V:T) ~> (V, n-of(N′, V))Funcon
+ intersperse(_:T′, _:(T)*) : =>(T, (T′, T)*)?
+Rule
+ intersperse(_:T′, ( )) ~> ( )
+Rule
+ intersperse(_:T′, V) ~> V
+Rule
+ intersperse(V′:T′, V1:T, V2:T, V*:(T)*) ~> (V1, V′, intersperse(V′, V2, V*))[
+ Type sets
+ Funcon set
+ Funcon set-elements
+ Funcon is-in-set
+ Funcon is-subset
+ Funcon set-insert
+ Funcon set-unite
+ Funcon set-intersect
+ Funcon set-difference
+ Funcon set-size
+ Funcon some-element
+ Funcon element-not-in
+]Meta-variables
+ GT <: ground-valuesBuilt-in Type
+ sets(GT)sets(GT) is the type of possibly-empty finite sets {V1, ..., Vn}
+ where V1:GT, ..., Vn:GT.
+
+
+
+Built-in Funcon
+ set(_:(GT)*) : =>sets(GT){V1, ..., Vn} for set(V1, ..., Vn) is built-in.
+
+Assert
+ {V*:(GT)*} == set(V*)set(...) is not a constructor operation. The order and duplicates
+ of argument values are ignored (e.g., {1,2,1} denotes the same set as {1,2}
+ and {2,1}).
+
+
+
+Built-in Funcon
+ set-elements(_:sets(GT)) : =>(GT)*S, the sequence of values V* returned by set-elements(S)
+ contains each element of S just once. The order of the values in V* is
+ unspecified, and may vary between sets (e.g., set-elements{1,2} could be
+ (1,2) and set-elements{1,2,3} could be (3,2,1)).
+
+Assert
+ set(set-elements(S)) == Sis-in-set(GV,S) tests whether GV is in the set S.
+
+
+
+
+
+
+
+ is-subset(S1,S2) tests whether S1 is a subset of S2.
+
+
+
+
+
+
+
+ set-insert(GV, S) returns the set union of {GV} and S.
+
+Assert
+ is-in-set(GV:GT, set-insert(GV:GT, S:sets(GT))) == trueset-unite(...) unites a sequence of sets.
+
+Assert
+ set-unite(S:sets(GT), S) == S
+Assert
+ set-unite(S1:sets(GT), S2:sets(GT)) == set-unite(S2, S1)
+Assert
+ set-unite(S1:sets(GT), set-unite(S2:sets(GT), S3:sets(GT))) ==
+ set-unite(set-unite(S1, S2), S3)
+Assert
+ set-unite(S1:sets(GT), S2:sets(GT), S3:sets(GT)) ==
+ set-unite(S1, set-unite(S2, S3))
+Assert
+ set-unite(S:sets(GT)) == S
+Assert
+ set-unite( ) == { }set-intersect(GT,...) intersects a non-empty sequence of sets.
+
+Assert
+ set-intersect(S:sets(GT), S) == S
+Assert
+ set-intersect(S1:sets(GT), S2:sets(GT)) == set-intersect(S2, S1)
+Assert
+ set-intersect(S1:sets(GT), set-intersect(S2:sets(GT), S3:sets(GT))) ==
+ set-intersect(set-intersect(S1, S2), S3)
+Assert
+ set-intersect(S1:sets(GT), S2:sets(GT), S3:sets(GT)) ==
+ set-intersect(S1, set-intersect(S2, S3))
+Assert
+ set-intersect(S:sets(GT)) == Sset-difference(S1, S2) returns the set containing those elements of S1
+ that are not in S2.
+
+
+Built-in Funcon
+ set-size(_:sets(GT)) : =>natural-numbersAssert
+ set-size(S:sets(GT)) == length(set-elements(S))Funcon
+ some-element(_:sets(GT)) : =>GT?
+Assert
+ some-element(S:sets(GT)) == index(1, set-elements(S))
+Assert
+ some-element{ } == ( )element-not-in(GT, S) gives an element of the type GT not in the set
+ S, or ( ) when S is empty. When the set of elements of GT is infinite,
+ element-not-in(GT, S) never gives ( ).
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Sets.cbs]: Sets.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Values/Composite/Sets/Sets.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-difference.config b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-difference.config
new file mode 100644
index 0000000..94d5607
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-difference.config
@@ -0,0 +1,27 @@
+general {
+ funcon-term:
+ initialise-giving finalise-failing
+ sequential (
+ print set-difference({1},set()),
+ print set-difference(set(),{2}),
+ print set-difference({1},{2}),
+ print set-difference({1,2},{1,2}),
+ print set-difference({1,2},{1}),
+ print set-difference({1,2},set()),
+ print "OK"
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [
+ {1},
+ {},
+ {1},
+ {},
+ {2},
+ {1,2},
+ "OK"
+ ];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-elements.config b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-elements.config
new file mode 100644
index 0000000..755bc42
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-elements.config
@@ -0,0 +1,15 @@
+general {
+ funcon-term:
+ initialise-giving finalise-failing
+ sequential (
+ print tuple(set-elements set( )),
+ print tuple(set-elements {1}),
+ print tuple(set-elements {2,3})
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [tuple(), tuple(1), tuple(2, 3) ];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-unite.config b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-unite.config
new file mode 100644
index 0000000..3a76eda
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set-unite.config
@@ -0,0 +1,27 @@
+general {
+ funcon-term:
+ initialise-giving finalise-failing
+ sequential (
+ print set-unite({1},set()),
+ print set-unite(set(),{2}),
+ print set-unite({1},{2}),
+ print set-unite({1}),
+ print set-unite(set()),
+ print set-unite(),
+ print "OK"
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [
+ {1},
+ {2},
+ {1,2},
+ {1},
+ set(),
+ set(),
+ "OK"
+ ];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set.config b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set.config
new file mode 100644
index 0000000..e52e90a
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/set.config
@@ -0,0 +1,21 @@
+general {
+ funcon-term:
+ initialise-giving finalise-failing
+ sequential (
+ print set(),
+ print {1},
+ print {1,2,3},
+ print cast({1,2}, sets(integers))
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [
+ set(),
+ {1},
+ {1, 2, 3},
+ {1, 2}
+ ];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/some-element.config b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/some-element.config
new file mode 100644
index 0000000..cfc2deb
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Sets/tests/some-element.config
@@ -0,0 +1,15 @@
+general {
+ funcon-term:
+ initialise-giving finalise-failing
+ sequential (
+ print some-element {1},
+ print some-element {1,2},
+ print some-element {1,2,3}
+ )
+ ;
+}
+
+tests {
+ result-term: null-value;
+ standard-out: [1, 1, 1];
+}
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Strings/Strings.cbs b/IBAF-cbs/Funcons-beta/Values/Composite/Strings/Strings.cbs
new file mode 100644
index 0000000..3cd02da
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Strings/Strings.cbs
@@ -0,0 +1,36 @@
+### Strings
+
+[
+ Type strings
+ Funcon string
+ Funcon string-append
+ Funcon to-string
+]
+
+
+Type
+ strings ~> lists(characters)
+
+
+Funcon
+ string(C*:characters*) : =>strings
+ ~> [C*]
+/*
+ Literal strings are written `"C1...Cn"`.
+ A double-quote or backslash needs to be escaped: `"...\"..."`, `"...\\..."`.
+*/
+
+
+Funcon
+ string-append(S*:strings*) : =>strings
+ ~> list-append(S*)
+
+
+Built-in Funcon
+ to-string(_:ground-values) : =>strings
+/*
+ The strings returned by `to-string(GV)` are unspecified, except that when
+ `GV` is already a string, it is returned unchanged.
+*/
+Assert
+ to-string(S:strings) == S
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Strings/index.md b/IBAF-cbs/Funcons-beta/Values/Composite/Strings/index.md
new file mode 100644
index 0000000..7b3ee8e
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Strings/index.md
@@ -0,0 +1,75 @@
+---
+layout: default
+title: "Strings"
+parent: Composite
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Strings.cbs]
+-----------------------------
+
+### Strings
+
+[
+ Type strings
+ Funcon string
+ Funcon string-append
+ Funcon to-string
+]Type
+ strings ~> lists(characters)Funcon
+ string(C*:characters*) : =>strings
+ ~> [C*]"C1...Cn".
+ A double-quote or backslash needs to be escaped: "...\"...", "...\\...".
+
+
+
+Funcon
+ string-append(S*:strings*) : =>strings
+ ~> list-append(S*)Built-in Funcon
+ to-string(_:ground-values) : =>stringsto-string(GV) are unspecified, except that when
+ GV is already a string, it is returned unchanged.
+
+
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Strings.cbs]: Strings.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Values/Composite/Strings/Strings.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Trees/Trees.cbs b/IBAF-cbs/Funcons-beta/Values/Composite/Trees/Trees.cbs
new file mode 100644
index 0000000..1b82cb2
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Trees/Trees.cbs
@@ -0,0 +1,94 @@
+### Trees
+
+[
+ Datatype trees
+ Funcon tree
+ Funcon tree-root-value
+ Funcon tree-branch-sequence
+ Funcon single-branching-sequence
+ Funcon forest-root-value-sequence
+ Funcon forest-branch-sequence
+ Funcon forest-value-sequence
+]
+
+
+Meta-variables
+ T <: values
+
+
+Datatype
+ trees(T) ::= tree( _:T, _:(trees(T))*)
+/*
+ `trees(T)` consists of finitely-branching trees with elements of type `T`.
+ When `V:T`, `tree(V)` is a leaf, and `tree(V,B1,...,Bn)` is a tree with
+ branches `B1`, ..., `Bn`.
+*/
+
+
+Funcon
+ tree-root-value(_:trees(T)) : =>(T)?
+Rule
+ tree-root-value tree(V:T, _*:(trees(T))*) ~> V
+
+
+Funcon
+ tree-branch-sequence(_:trees(T)) : =>(trees(T))*
+Rule
+ tree-branch-sequence tree(_:T, B*:(trees(T))*) ~> B*
+
+
+Funcon
+ single-branching-sequence(_:trees(T)) : =>T+
+/*
+ `single-branching-sequence B ` extracts the values in `B` starting from
+ the root, provided that `B` is at most single-branching; otherwise it fails.
+*/
+Rule
+ single-branching-sequence tree(V:T) ~> V
+Rule
+ single-branching-sequence tree(V:T, B:trees(T))
+ ~> left-to-right( V, single-branching-sequence B)
+Rule
+ single-branching-sequence tree(_:T, _:trees(T), _+:(trees(T))+) ~> fail
+
+
+/*
+ A sequence of trees corresponds to a forest, and the selector funcons
+ on trees `B` extend to forests `B*`:
+*/
+
+Funcon
+ forest-root-value-sequence(_:(trees(T))*) : =>T*
+Rule
+ forest-root-value-sequence(B:trees(T), B*:(trees(T))*)
+ ~>(tree-root-value B , forest-root-value-sequence B*)
+Rule
+ forest-root-value-sequence( ) ~>( )
+
+
+Funcon
+ forest-branch-sequence(_:(trees(T))*) : =>T*
+Rule
+ forest-branch-sequence(B:trees(T), B*:(trees(T))*)
+ ~>(tree-branch-sequence B , forest-branch-sequence B*)
+Rule
+ forest-branch-sequence( ) ~>( )
+
+
+Funcon
+ forest-value-sequence(_:(trees(T))*) : =>T*
+/*
+ `forest-value-sequence B*` provides the values from a left-to-right pre-order
+ depth-first traversal.
+*/
+Rule
+ forest-value-sequence(tree(V:T, B1*:(trees(T))*), B2*:(trees(T))*)
+ ~>(V , forest-value-sequence B1*, forest-value-sequence B2*)
+Rule
+ forest-value-sequence( ) ~>( )
+
+
+/*
+ Other linearizations of trees can be added: breadth-first, right-to-left,
+ C3, etc.
+*/
diff --git a/IBAF-cbs/Funcons-beta/Values/Composite/Trees/index.md b/IBAF-cbs/Funcons-beta/Values/Composite/Trees/index.md
new file mode 100644
index 0000000..b3c794d
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Composite/Trees/index.md
@@ -0,0 +1,130 @@
+---
+layout: default
+title: "Trees"
+parent: Composite
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Trees.cbs]
+-----------------------------
+
+### Trees
+
+[
+ Datatype trees
+ Funcon tree
+ Funcon tree-root-value
+ Funcon tree-branch-sequence
+ Funcon single-branching-sequence
+ Funcon forest-root-value-sequence
+ Funcon forest-branch-sequence
+ Funcon forest-value-sequence
+]Meta-variables
+ T <: valuesDatatype
+ trees(T) ::= tree( _:T, _:(trees(T))*)trees(T) consists of finitely-branching trees with elements of type T.
+ When V:T, tree(V) is a leaf, and tree(V,B1,...,Bn) is a tree with
+ branches B1, ..., Bn.
+
+Funcon
+ tree-root-value(_:trees(T)) : =>(T)?
+Rule
+ tree-root-value tree(V:T, _*:(trees(T))*) ~> VFuncon
+ tree-branch-sequence(_:trees(T)) : =>(trees(T))*
+Rule
+ tree-branch-sequence tree(_:T, B*:(trees(T))*) ~> B*Funcon
+ single-branching-sequence(_:trees(T)) : =>T+single-branching-sequence B extracts the values in B starting from
+ the root, provided that B is at most single-branching; otherwise it fails.
+
+Rule
+ single-branching-sequence tree(V:T) ~> V
+Rule
+ single-branching-sequence tree(V:T, B:trees(T))
+ ~> left-to-right( V, single-branching-sequence B)
+Rule
+ single-branching-sequence tree(_:T, _:trees(T), _+:(trees(T))+) ~> failB extend to forests B*:
+
+Funcon
+ forest-root-value-sequence(_:(trees(T))*) : =>T*
+Rule
+ forest-root-value-sequence(B:trees(T), B*:(trees(T))*)
+ ~>(tree-root-value B , forest-root-value-sequence B*)
+Rule
+ forest-root-value-sequence( ) ~>( )Funcon
+ forest-branch-sequence(_:(trees(T))*) : =>T*
+Rule
+ forest-branch-sequence(B:trees(T), B*:(trees(T))*)
+ ~>(tree-branch-sequence B , forest-branch-sequence B*)
+Rule
+ forest-branch-sequence( ) ~>( )Funcon
+ forest-value-sequence(_:(trees(T))*) : =>T*forest-value-sequence B* provides the values from a left-to-right pre-order
+ depth-first traversal.
+
+Rule
+ forest-value-sequence(tree(V:T, B1*:(trees(T))*), B2*:(trees(T))*)
+ ~>(V , forest-value-sequence B1*, forest-value-sequence B2*)
+Rule
+ forest-value-sequence( ) ~>( )[
+ Datatype tuples
+ Funcon tuple-elements
+ Funcon tuple-zip
+]Datatype
+ tuples(T*) ::= tuple(_:T*)T* can be any sequence of types, including ( ) and values*.
+
+ The values of type tuples(T1, ..., Tn) are of the form tuple(V1, ..., Vn)
+ with V1:T1, ..., Vn:Tn.
+
+Funcon
+ tuple-elements(_:tuples(T*)) : =>(T*)
+Rule
+ tuple-elements(tuple(V*:T*)) ~> V*tuple-zip(TV1, TV2) takes two tuples, and returns the sequence of pairs of
+ their elements, provided that they have the same length. If they have
+ different lengths, the last elements of the longer sequence are ignored.
+
+Rule
+ tuple-zip(tuple(V1:T1, V1*:T1*), tuple(V2:T2, V2*:T2*))
+ ~> (tuple(V1, V2), tuple-zip(tuple(V1*), tuple(V2*)))
+Rule
+ tuple-zip(tuple( ), tuple( )) ~> ( )
+Rule
+ tuple-zip(tuple(V1+:T1+), tuple( )) ~> ( )
+Rule
+ tuple-zip(tuple( ), tuple(V2+:T2+)) ~> ( )[
+ Datatype variants
+ Funcon variant
+ Funcon variant-id
+ Funcon variant-value
+]Meta-variables
+ T <: valuesDatatype
+ variants(T) ::= variant(_:identifiers, _:T)variants(T) is a pair formed from an identifier and
+ a value of type T.
+
+Funcon
+ variant-id(_:variants(T)) : =>identifiers
+Rule
+ variant-id(variant(I:identifiers, _:T)) ~> IFuncon
+ variant-value(_:variants(T)) : =>T
+Rule
+ variant-value(variant(_:identifiers, V:T)) ~> V[
+ Datatype vectors
+ Funcon vector
+ Funcon vector-elements
+]Meta-variables
+ T <: valuesDatatype
+ vectors(T) ::= vector(_:(T)*)Funcon
+ vector-elements(_:vectors(T)) : =>(T)*
+Rule
+ vector-elements(vector(V*:(T)*)) ~> V*[
+ Datatype booleans Alias bools
+ Funcon true
+ Funcon false
+ Funcon not
+ Funcon implies
+ Funcon and
+ Funcon or
+ Funcon exclusive-or Alias xor
+]Datatype
+ booleans ::= true | false
+Alias
+ bools = booleansnot(B) is logical negation.
+
+
+
+
+
+
+
+ implies(B1, B2) is logical implication.
+
+Rule
+ implies(false, false) ~> true
+Rule
+ implies(false, true) ~> true
+Rule
+ implies(true, true) ~> true
+Rule
+ implies(true, false) ~> falseand(B, ...) is logical conjunction of any number of Boolean values.
+
+Rule
+ and( ) ~> true
+Rule
+ and(false, _*:booleans*) ~> false
+Rule
+ and(true, B*:booleans*) ~> and(B*)or(B, ...) is logical disjunction of any number of Boolean values.
+
+Rule
+ or( ) ~> false
+Rule
+ or(true, _*:booleans*) ~> true
+Rule
+ or(false, B*:booleans*) ~> or(B*)Funcon
+ exclusive-or(_:booleans, _:booleans) : =>booleans
+Alias
+ xor = exclusive-orexclusive-or(B1, B2) is exclusive disjunction.
+
+Rule
+ exclusive-or(false, false) ~> false
+Rule
+ exclusive-or(false, true) ~> true
+Rule
+ exclusive-or(true, false) ~> true
+Rule
+ exclusive-or(true, true) ~> false[
+ Type characters Alias chars
+ Datatype unicode-characters Alias unicode-chars
+ Type unicode-points
+ Funcon unicode-character Alias unicode-char
+ Funcon unicode-point Alias unicode
+ Type basic-multilingual-plane-characters Alias bmp-chars
+ Type basic-multilingual-plane-points
+ Type iso-latin-1-characters Alias latin-1-chars
+ Type iso-latin-1-points
+ Type ascii-characters Alias ascii-chars
+ Type ascii-points
+ Funcon ascii-character Alias ascii-char
+ Funcon utf-8
+ Funcon utf-16
+ Funcon utf-32
+ Funcon backspace
+ Funcon horizontal-tab
+ Funcon line-feed
+ Funcon form-feed
+ Funcon carriage-return
+ Funcon double-quote
+ Funcon single-quote
+ Funcon backslash
+]Built-in Type
+ characters <: values'C' where C is any visible character
+ other than a single-quote or backslash character, which need to be
+ escaped as '\'' and '\\'.
+
+Alias
+ chars = charactersBuilt-in Datatype
+ unicode-characters <: characters
+Alias
+ unicode-chars = unicode-charactersBuilt-in Type
+ unicode-points <: bounded-integers(0, unsigned-bit-vector-maximum(21))Built-in Funcon
+ unicode-character(_:unicode-points) : unicode-characters
+Alias
+ unicode-char = unicode-characterunicode-characters are the values of
+ unicode-character(UP:unicode-points).
+
+Funcon
+ unicode-point(_:unicode-characters) : =>unicode-points
+Alias
+ unicode = unicode-pointRule
+ unicode-point(unicode-character(UP:unicode-points)) ~> UPBuilt-in Datatype
+ basic-multilingual-plane-characters <: unicode-characters
+Alias
+ bmp-chars = basic-multilingual-plane-charactersBuilt-in Type
+ basic-multilingual-plane-points <:
+ bounded-integers(0, unsigned-bit-vector-maximum(17))basic-multilingual-plane-characters are the values of
+ unicode-character(BMPP:basic-multilingual-plane-points).
+
+
+
+#### ISO Latin-1 character set
+
+
+Built-in Datatype
+ iso-latin-1-characters <: basic-multilingual-plane-characters
+Alias
+ latin-1-chars = iso-latin-1-charactersType
+ iso-latin-1-points ~> bounded-integers(0, unsigned-bit-vector-maximum(8))iso-latin-1-characters are the values of
+ unicode-character(ILP:iso-latin-1-points).
+
+
+
+#### ASCII character set
+
+
+Built-in Type
+ ascii-characters <: iso-latin-1-characters
+Alias
+ ascii-chars = ascii-charactersType
+ ascii-points ~> bounded-integers(0, unsigned-bit-vector-maximum(7))ascii-characters are the values of
+ unicode-character(AP:ascii-points).
+
+Funcon
+ ascii-character(_:strings) : =>ascii-characters?
+Alias
+ ascii-char = ascii-characterascii-character"C" takes a string. When it consists of a single ASCII
+ character C it gives the character, otherwise ( ).
+
+Rule
+ ascii-character[C:ascii-characters] ~> C
+Rule
+ C : ~ ascii-characters
+ ------------------------------------
+ ascii-character[C:characters] ~> ( )
+Rule
+ length(C*) =/= 1
+ --------------------------------------
+ ascii-character[C*:characters*] ~> ( )Built-in Funcon
+ utf-8(_:unicode-points) : =>(bytes, (bytes, (bytes, bytes?)? )? )Built-in Funcon
+ utf-16(_:unicode-points) : =>(bit-vectors(16), (bit-vectors(16))? )Built-in Funcon
+ utf-32(_:unicode-points) : =>bit-vectors(32)Funcon
+ backspace : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"0008")Funcon
+ horizontal-tab : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"0009")Funcon
+ line-feed : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"000a")Funcon
+ form-feed : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"000c")Funcon
+ carriage-return : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"000d")Funcon
+ double-quote : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"0022")Funcon
+ single-quote : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"0027")Funcon
+ backslash : =>ascii-characters
+ ~> unicode-character(hexadecimal-natural"005c")[
+ Datatype float-formats
+ Funcon binary32
+ Funcon binary64
+ Funcon binary128
+ Funcon decimal64
+ Funcon decimal128
+ Type floats
+ Funcon float
+ Funcon quiet-not-a-number Alias qNaN
+ Funcon signaling-not-a-number Alias sNaN
+ Funcon positive-infinity Alias pos-inf
+ Funcon negative-infinity Alias neg-inf
+ Funcon float-convert
+ Funcon decimal-float
+ Funcon float-equal
+ Funcon float-is-less
+ Funcon float-is-less-or-equal
+ Funcon float-is-greater
+ Funcon float-is-greater-or-equal
+ Funcon float-negate
+ Funcon float-absolute-value
+ Funcon float-add
+ Funcon float-subtract
+ Funcon float-multiply
+ Funcon float-multiply-add
+ Funcon float-divide
+ Funcon float-remainder
+ Funcon float-sqrt
+ Funcon float-integer-power
+ Funcon float-float-power
+ Funcon float-round-ties-to-even
+ Funcon float-round-ties-to-infinity
+ Funcon float-floor
+ Funcon float-ceiling
+ Funcon float-truncate
+ Funcon float-pi
+ Funcon float-e
+ Funcon float-log
+ Funcon float-log10
+ Funcon float-exp
+ Funcon float-sin
+ Funcon float-cos
+ Funcon float-tan
+ Funcon float-asin
+ Funcon float-acos
+ Funcon float-atan
+ Funcon float-sinh
+ Funcon float-cosh
+ Funcon float-tanh
+ Funcon float-asinh
+ Funcon float-acosh
+ Funcon float-atanh
+ Funcon float-atan2
+]Datatype
+ float-formats ::= binary32 | binary64 | binary128 | decimal64 | decimal128Built-in Type
+ floats(_:float-formats)FF1, FF2, the types floats(FF1) and
+ floats(FF2) are not necessarily disjoint.
+
+
+Built-in Funcon
+ float(FF:float-formats,
+ _:bounded-integers(0, 1), _:natural-numbers, _:integers) : =>floats(FF)float(FF, S, C, Q) is not a 1-1 operation.
+
+Built-in Funcon
+ quiet-not-a-number(FF:float-formats) : floats(FF)
+Alias
+ qNaN = quiet-not-a-numberBuilt-in Funcon
+ signaling-not-a-number(FF:float-formats) : floats(FF)
+Alias
+ sNaN = signaling-not-a-numberBuilt-in Funcon
+ positive-infinity(FF:float-formats) : floats(FF)
+Alias
+ pos-inf = positive-infinityBuilt-in Funcon
+ negative-infinity(FF:float-formats) : floats(FF)
+Alias
+ neg-inf = negative-infinityBuilt-in Funcon
+ float-convert(FF1:float-formats,
+ FF2:float-formats, F:floats(FF1)) : =>floats(FF2)Built-in Funcon
+ decimal-float(FF:float-formats,
+ _:strings, _:strings, _:strings) : =>floats(FF)decimal-float(F, "M", "N", "E") is an approximation in floats(FF) to the
+ value of 'M.N' times 10 to the power 'E', where "M.N" is decimal notation
+ (optionally-signed) for a fixed-point number and "E" is decimal notation
+ (optionally signed) for an integer. When any argument string is invalid,
+ the result is quiet-not-a-number(F).
+
+
+
+#### Comparison
+
+Built-in Funcon
+ float-equal(FF:float-formats,
+ _:floats(FF), _:floats(FF)) : =>booleansBuilt-in Funcon
+ float-is-less(FF:float-formats,
+ _:floats(FF), _:floats(FF)) : =>booleansBuilt-in Funcon
+ float-is-less-or-equal(FF:float-formats,
+ _:floats(FF), _:floats(FF)) : =>booleansBuilt-in Funcon
+ float-is-greater(FF:float-formats,
+ _:floats(FF), _:floats(FF)) : =>booleansBuilt-in Funcon
+ float-is-greater-or-equal(FF:float-formats,
+ _:floats(FF), _:floats(FF)) : =>booleansBuilt-in Funcon
+ float-negate(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-absolute-value(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-add(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-subtract(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-multiply(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-multiply-add(FF:float-formats,
+ _:floats(FF), _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-divide(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-remainder(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-sqrt(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-integer-power(FF:float-formats, _:floats(FF), _:integers) : =>floats(FF)Built-in Funcon
+ float-float-power(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-round-ties-to-even(FF:float-formats, _:floats(FF)) : =>integersBuilt-in Funcon
+ float-round-ties-to-infinity(FF:float-formats, _:floats(FF)) : =>integersBuilt-in Funcon
+ float-floor(FF:float-formats, _:floats(FF)) : =>integersBuilt-in Funcon
+ float-ceiling(FF:float-formats, _:floats(FF)) : =>integersBuilt-in Funcon
+ float-truncate(FF:float-formats, _:floats(FF)) : =>integersBuilt-in Funcon
+ float-pi(FF:float-formats) : =>floats(FF)Built-in Funcon
+ float-e(FF:float-formats) : =>floats(FF)Built-in Funcon
+ float-log(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-log10(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-exp(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-sin(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-cos(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-tan(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-asin(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-acos(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-atan(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-sinh(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-cosh(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-tanh(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-asinh(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-acosh(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-atanh(FF:float-formats, _:floats(FF)) : =>floats(FF)Built-in Funcon
+ float-atan2(FF:float-formats, _:floats(FF), _:floats(FF)) : =>floats(FF)[
+ Type integers Alias ints
+ Type integers-from Alias from
+ Type integers-up-to Alias up-to
+ Type bounded-integers Alias bounded-ints
+ Type positive-integers Alias pos-ints
+ Type negative-integers Alias neg-ints
+ Type natural-numbers Alias nats
+ Funcon natural-successor Alias nat-succ
+ Funcon natural-predecessor Alias nat-pred
+ Funcon integer-add Alias int-add
+ Funcon integer-subtract Alias int-sub
+ Funcon integer-multiply Alias int-mul
+ Funcon integer-divide Alias int-div
+ Funcon integer-modulo Alias int-mod
+ Funcon integer-power Alias int-pow
+ Funcon integer-absolute-value Alias int-abs
+ Funcon integer-negate Alias int-neg
+ Funcon integer-is-less Alias is-less
+ Funcon integer-is-less-or-equal Alias is-less-or-equal
+ Funcon integer-is-greater Alias is-greater
+ Funcon integer-is-greater-or-equal Alias is-greater-or-equal
+ Funcon binary-natural Alias binary
+ Funcon octal-natural Alias octal
+ Funcon decimal-natural Alias decimal
+ Funcon hexadecimal-natural Alias hexadecimal
+ Funcon integer-sequence
+]Built-in Type
+ integers
+Alias
+ ints = integersintegers is the type of unbounded integers. Decimal notation is used to
+ express particular integer values.
+
+
+
+#### Subtypes of integers
+
+
+Built-in Type
+ integers-from(_:integers) <: integers
+Alias
+ from = integers-fromintegers-from(M) is the subtype of integers greater than or equal to M.
+
+Built-in Type
+ integers-up-to(_:integers) <: integers
+Alias
+ up-to = integers-up-tointegers-up-to(N) is the subtype of integers less than or equal to N.
+
+Type
+ bounded-integers(M:integers, N:integers)
+ ~> integers-from(M) & integers-up-to(N)
+Alias
+ bounded-ints = bounded-integersbounded-integers(M,N) is the subtype of integers from M to N, inclusive.
+
+Type
+ positive-integers ~> integers-from(1)
+Alias
+ pos-ints = positive-integersType
+ negative-integers ~> integers-up-to(-1)
+Alias
+ neg-ints = negative-integersType
+ natural-numbers ~> integers-from(0)
+Alias
+ nats = natural-numbersBuilt-in Funcon
+ natural-successor(N:natural-numbers) : =>natural-numbers
+Alias
+ nat-succ = natural-successorBuilt-in Funcon
+ natural-predecessor(_:natural-numbers) : =>natural-numbers?
+Alias
+ nat-pred = natural-predecessorAssert
+ natural-predecessor(0) == ( )Built-in Funcon
+ integer-add(_:integers*) : =>integers
+Alias
+ int-add = integer-addBuilt-in Funcon
+ integer-subtract(_:integers, _:integers) : =>integers
+Alias
+ int-sub = integer-subtractBuilt-in Funcon
+ integer-multiply(_:integers*) : =>integers
+Alias
+ int-mul = integer-multiplyBuilt-in Funcon
+ integer-divide(_:integers, _:integers) : =>integers?
+Alias
+ int-div = integer-divideAssert
+ integer-divide(_:integers, 0) == ( )Built-in Funcon
+ integer-modulo(_:integers, _:integers) : =>integers?
+Alias
+ int-mod = integer-moduloAssert
+ integer-modulo(_:integers, 0) == ( )Built-in Funcon
+ integer-power(_:integers, _:natural-numbers) : =>integers
+Alias
+ int-pow = integer-powerBuilt-in Funcon
+ integer-absolute-value(_:integers) : =>natural-numbers
+Alias
+ int-abs = integer-absolute-valueFuncon
+ integer-negate(N:integers) : =>integers
+ ~> integer-subtract(0, N)
+Alias
+ int-neg = integer-negateBuilt-in Funcon
+ integer-is-less(_:integers, _:integers) : =>booleans
+Alias
+ is-less = integer-is-lessBuilt-in Funcon
+ integer-is-less-or-equal(_:integers, _:integers) : =>booleans
+Alias
+ is-less-or-equal = integer-is-less-or-equalBuilt-in Funcon
+ integer-is-greater(_:integers, _:integers) : =>booleans
+Alias
+ is-greater = integer-is-greaterBuilt-in Funcon
+ integer-is-greater-or-equal(_:integers, _:integers) : =>booleans
+Alias
+ is-greater-or-equal = integer-is-greater-or-equalBuilt-in Funcon
+ binary-natural(_:strings) : =>natural-numbers?
+Alias
+ binary = binary-naturalBuilt-in Funcon
+ octal-natural(_:strings) : =>natural-numbers?
+Alias
+ octal = octal-naturalBuilt-in Funcon
+ decimal-natural(_:strings) : =>natural-numbers?
+Alias
+ decimal = decimal-naturalN are equivalent to decimal-natural"N".
+
+Built-in Funcon
+ hexadecimal-natural(_:strings) : =>natural-numbers?
+Alias
+ hexadecimal = hexadecimal-naturalinteger-sequence(M, N) is the seqeunce of integers from M to N,
+ except that if M is greater than N, it is the empty sequence.
+
+Rule
+ is-greater(M, N) == false
+ ------------------------------------------------
+ integer-sequence(M:integers, N:integers)
+ ~> (M, integer-sequence(integer-add(M, 1), N))
+Rule
+ is-greater(M, N) == true
+ -----------------------------------------------
+ integer-sequence(M:integers, N:integers) ~> ( )[
+Datatype null-type
+Funcon null-value Alias null
+]Datatype
+ null-type ::= null-value
+Alias
+ null = null-valuenull-type is null-value.
+
+
+
+____
+
+From the [PLanCompS Project] | [CBS-beta issues...] | [Suggest an improvement...]
+
+[Null.cbs]: Null.cbs
+ "CBS SOURCE FILE"
+[Funcons-beta]: /CBS-beta/docs/Funcons-beta
+ "FUNCONS-BETA"
+[Unstable-Funcons-beta]: /CBS-beta/docs/Unstable-Funcons-beta
+ "UNSTABLE-FUNCONS-BETA"
+[Languages-beta]: /CBS-beta/docs/Languages-beta
+ "LANGUAGES-BETA"
+[Unstable-Languages-beta]: /CBS-beta/docs/Unstable-Languages-beta
+ "UNSTABLE-LANGUAGES-BETA"
+[CBS-beta]: /CBS-beta "CBS-BETA"
+[PLanCompS Project]: https://plancomps.github.io
+ "PROGRAMMING LANGUAGE COMPONENTS AND SPECIFICATIONS PROJECT HOME PAGE"
+[CBS-beta issues...]: https://github.com/plancomps/CBS-beta/issues
+ "CBS-BETA ISSUE REPORTS ON GITHUB"
+[Suggest an improvement...]: mailto:plancomps@gmail.com?Subject=CBS-beta%20-%20comment&Body=Re%3A%20CBS-beta%20specification%20at%20Values/Primitive/Null/Null.cbs%0A%0AComment/Query/Issue/Suggestion%3A%0A%0A%0ASignature%3A%0A
+ "GENERATE AN EMAIL TEMPLATE"
diff --git a/IBAF-cbs/Funcons-beta/Values/Value-Types/Value-Types.cbs b/IBAF-cbs/Funcons-beta/Values/Value-Types/Value-Types.cbs
new file mode 100644
index 0000000..17a6c39
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Value-Types/Value-Types.cbs
@@ -0,0 +1,216 @@
+## Value Types
+
+[
+ Type values Alias vals
+ Type value-types Alias types
+ Type empty-type
+ Funcon is-in-type Alias is
+ Funcon is-value Alias is-val
+ Funcon when-true Alias when
+ Type cast-to-type Alias cast
+ Type ground-values Alias ground-vals
+ Funcon is-equal Alias is-eq
+]
+
+
+### Values
+
+Built-in Type
+ values
+Alias
+ vals = values
+/*
+ The type `values` includes all values provided by CBS.
+
+ Some funcons are declared as value constructors. Values are constructed by
+ applying value constructor funcons to the required arguments.
+
+ Values are immutable and context-independent. Their structure can be
+ inspected using patterns formed from value constructors and variables.
+ Computations can be extracted from values and executed, but the structure
+ of computations cannot be inspected.
+
+ Some types of values and their funcons are declared as built-in, and not
+ further specified in CBS. New types of built-in values can be added to CBS
+ by its developers.
+
+ New algebraic datatypes may be declared by users of CBS. Their values are
+ disjoint from built-in values.
+*/
+
+
+Meta-variables
+ T, T1, T2 <: values
+
+
+### Types
+
+Built-in Type
+ value-types
+Alias
+ types = value-types
+Built-in Type
+ empty-type
+/*
+ A type `T` is a value that represents a set of values.
+
+ The values of type `types` are all the types, including `types` itself.
+
+ The formula ``V : T`` holds when `V` is a value of type `T`, i.e., `V` is in
+ the set represented by the type `T`.
+
+ The formula ``T1 <: T2`` holds when `T1` is a subtype of `T2`, i.e., the set
+ represented by `T1` is a subset of the set represented by `T2`.
+
+ The set of types forms a Boolean algebra with the following operations and
+ constants:
+ * `T1 & T2` (meet/intersection)
+ * `T1 | T2` (join/union)
+ * `~ T` (complement)
+ * `values` (top)
+ * `empty-type` (bottom)
+
+ Subtyping: ``T1 <: T2`` is the partial order defined by the algebra.
+
+ Subsumption: If ``V : T1`` and ``T1 <: T2`` both hold, so does ``V : T2``.
+
+ Indivisibility: For each value `V` and type `T`, either ``V : T`` or
+ ``V : ~T`` holds.
+
+ Universality: ``V : values`` holds for all values `V`.
+
+ Emptiness: ``V : empty-type`` holds for no value `V`.
+
+ 'Type N' declares the name 'N' to refer to a fresh value constructor
+ and includes it as an element of `types`.
+
+ 'Type N ~> T' moreover specifies 'Rule N ~> T', so that 'N' can be used as
+ an abbreviation for the type term 'T'.
+
+ 'Type N <: T' declares the name 'N' to refer to a fresh value constructor
+ in `types`, and asserts 'N <: T'.
+
+ Parametrised type declarations introduce generic (possibly dependent) types,
+ i.e., families of individual types, indexed by types (and by other values).
+ For example, `lists(T)` is parameterised by the type of list elements `T`.
+ Replacing a parameter by `_` denotes the union over all instances of that
+ parameter, e.g., `lists(_)` is the union of all types `lists(T)` with `T:types`.
+
+ Qualified variables `V:T` in terms range over values of type `T`.
+ Qualified variables ``T1<:T2`` in terms range over subtypes `T1` of `T2`.
+*/
+
+
+Funcon
+ is-in-type(V:values, T:types) : =>booleans
+Alias
+ is = is-in-type
+/*
+ `is-in-type(V, T)` tests whether ``V : T`` holds. The value `V` need not be a
+ ground value, but `T` should not require testing any computation types.
+*/
+Rule
+ V : T
+ -------------------------------------
+ is-in-type(V:values, T:types) ~> true
+Rule
+ V : ~ T
+ --------------------------------------
+ is-in-type(V:values, T:types) ~> false
+
+
+### Option types
+
+/*
+ For any value type `T`, the elements of the option type `(T)?` are the
+ elements of `T` together with the empty sequence `( )`, which represents
+ the absence of a value. Option types are a special case of sequence types.
+
+ A funcon whose result type is an option type `(T)?` may compute a value of
+ type `T` or the empty sequence `( )`; the latter represents undefined results
+ of partial operations.
+
+ The parentheses in `(T)?` and `( )` can be omitted when this does not give
+ rise to grouoing ambiguity. Note however that `T?` is a meta-variable ranging
+ over option types, whereas `(T)?` is the option type for the value type `T`.
+*/
+
+
+Funcon
+ is-value(_:values?) : =>booleans
+Alias
+ is-val = is-value
+/*
+ `is-value(V?)` tests whether the optional value `V?` is a value or absent.
+*/
+Rule
+ is-value(_:values) ~> true
+Rule
+ is-value( ) ~> false
+
+
+Funcon
+ when-true(_:booleans, _:T) : =>(T)?
+Alias
+ when = when-true
+/*
+ `when-true(B, V)` gives `V` when `B` is `true`, and `( )` when `B` is `false`.
+*/
+Rule
+ when-true(true, V:values) ~> V
+Rule
+ when-true(false, V:values) ~> ( )
+
+
+Funcon
+ cast-to-type(V:values, T:types) : =>(T)?
+Alias
+ cast = cast-to-type
+/*
+ `cast-to-type(V, T)` gives `V` if it is in `T`, otherwise `( )`.
+*/
+Rule
+ V : T
+ -------------------------------------
+ cast-to-type(V:values, T:types) ~> V
+Rule
+ V : ~ T
+ --------------------------------------
+ cast-to-type(V:values, T:types) ~> ( )
+
+
+### Ground values
+
+Built-in Type
+ ground-values
+Alias
+ ground-vals = ground-values
+/*
+ The elements of `ground-values` are all values that are formed entirely
+ from value-constructors, and thus do not involve computations.
+
+ A type is a subtype of `ground-values` if and only if all its elements are
+ included in `ground-values`.
+*/
+
+
+Funcon
+ is-equal(V:values, W:values) : =>booleans
+Alias
+ is-eq = is-equal
+/*
+ `is-equal(V, W)` returns `true` when `V` and `W` are identical ground values,
+ otherwise `false`.
+*/
+Rule
+ V == W
+ --------------------------------------------------
+ is-equal(V:ground-values, W:ground-values) ~> true
+Rule
+ V =/= W
+ ---------------------------------------------------
+ is-equal(V:ground-values, W:ground-values) ~> false
+Rule
+ is-equal(V:~ground-values, W:values) ~> false
+Rule
+ is-equal(V:values, W:~ground-values) ~> false
diff --git a/IBAF-cbs/Funcons-beta/Values/Value-Types/index.md b/IBAF-cbs/Funcons-beta/Values/Value-Types/index.md
new file mode 100644
index 0000000..136869c
--- /dev/null
+++ b/IBAF-cbs/Funcons-beta/Values/Value-Types/index.md
@@ -0,0 +1,258 @@
+---
+layout: default
+title: "Value-Types"
+parent: Values
+ancestor: Funcons-beta
+
+---
+
+[Funcons-beta] : [Value-Types.cbs]
+-----------------------------
+
+## Value Types
+
+[
+ Type values Alias vals
+ Type value-types Alias types
+ Type empty-type
+ Funcon is-in-type Alias is
+ Funcon is-value Alias is-val
+ Funcon when-true Alias when
+ Type cast-to-type Alias cast
+ Type ground-values Alias ground-vals
+ Funcon is-equal Alias is-eq
+]Built-in Type
+ values
+Alias
+ vals = valuesvalues includes all values provided by CBS.
+
+ Some funcons are declared as value constructors. Values are constructed by
+ applying value constructor funcons to the required arguments.
+
+ Values are immutable and context-independent. Their structure can be
+ inspected using patterns formed from value constructors and variables.
+ Computations can be extracted from values and executed, but the structure
+ of computations cannot be inspected.
+
+ Some types of values and their funcons are declared as built-in, and not
+ further specified in CBS. New types of built-in values can be added to CBS
+ by its developers.
+
+ New algebraic datatypes may be declared by users of CBS. Their values are
+ disjoint from built-in values.
+
+
+
+Meta-variables
+ T, T1, T2 <: valuesBuilt-in Type
+ value-types
+Alias
+ types = value-typesBuilt-in Type
+ empty-typeT is a value that represents a set of values.
+
+ The values of type types are all the types, including types itself.
+
+ The formula V : T holds when V is a value of type T, i.e., V is in
+ the set represented by the type T.
+
+ The formula T1 <: T2 holds when T1 is a subtype of T2, i.e., the set
+ represented by T1 is a subset of the set represented by T2.
+
+ The set of types forms a Boolean algebra with the following operations and
+ constants:
+ * T1 & T2 (meet/intersection)
+ * T1 | T2 (join/union)
+ * ~ T (complement)
+ * values (top)
+ * empty-type (bottom)
+
+ Subtyping: T1 <: T2 is the partial order defined by the algebra.
+
+ Subsumption: If V : T1 and T1 <: T2 both hold, so does V : T2.
+
+ Indivisibility: For each value V and type T, either V : T or
+ V : ~T holds.
+
+ Universality: V : values holds for all values V.
+
+ Emptiness: V : empty-type holds for no value V.
+
+ 'Type N' declares the name 'N' to refer to a fresh value constructor
+ and includes it as an element of types.
+
+ 'Type N ~> T' moreover specifies 'Rule N ~> T', so that 'N' can be used as
+ an abbreviation for the type term 'T'.
+
+ 'Type N <: T' declares the name 'N' to refer to a fresh value constructor
+ in types, and asserts 'N <: T'.
+
+ Parametrised type declarations introduce generic (possibly dependent) types,
+ i.e., families of individual types, indexed by types (and by other values).
+ For example, lists(T) is parameterised by the type of list elements T.
+ Replacing a parameter by _ denotes the union over all instances of that
+ parameter, e.g., lists(_) is the union of all types lists(T) with T:types.
+
+ Qualified variables V:T in terms range over values of type T.
+ Qualified variables T1<:T2 in terms range over subtypes T1 of T2.
+
+Funcon
+ is-in-type(V:values, T:types) : =>booleans
+Alias
+ is = is-in-typeis-in-type(V, T) tests whether V : T holds. The value V need not be a
+ ground value, but T should not require testing any computation types.
+
+Rule
+ V : T
+ -------------------------------------
+ is-in-type(V:values, T:types) ~> true
+Rule
+ V : ~ T
+ --------------------------------------
+ is-in-type(V:values, T:types) ~> falseT, the elements of the option type (T)? are the
+ elements of T together with the empty sequence ( ), which represents
+ the absence of a value. Option types are a special case of sequence types.
+
+ A funcon whose result type is an option type (T)? may compute a value of
+ type T or the empty sequence ( ); the latter represents undefined results
+ of partial operations.
+
+ The parentheses in (T)? and ( ) can be omitted when this does not give
+ rise to grouoing ambiguity. Note however that T? is a meta-variable ranging
+ over option types, whereas (T)? is the option type for the value type T.
+
+
+
+
+ is-value(V?) tests whether the optional value V? is a value or absent.
+
+
+
+
+
+
+ when-true(B, V) gives V when B is true, and ( ) when B is false.
+
+
+
+Funcon
+ cast-to-type(V:values, T:types) : =>(T)?
+Alias
+ cast = cast-to-typecast-to-type(V, T) gives V if it is in T, otherwise ( ).
+
+Rule
+ V : T
+ -------------------------------------
+ cast-to-type(V:values, T:types) ~> V
+Rule
+ V : ~ T
+ --------------------------------------
+ cast-to-type(V:values, T:types) ~> ( )Built-in Type
+ ground-values
+Alias
+ ground-vals = ground-valuesground-values are all values that are formed entirely
+ from value-constructors, and thus do not involve computations.
+
+ A type is a subtype of ground-values if and only if all its elements are
+ included in ground-values.
+
+
+
+
+ is-equal(V, W) returns true when V and W are identical ground values,
+ otherwise false.
+
+Rule
+ V == W
+ --------------------------------------------------
+ is-equal(V:ground-values, W:ground-values) ~> true
+Rule
+ V =/= W
+ ---------------------------------------------------
+ is-equal(V:ground-values, W:ground-values) ~> false
+Rule
+ is-equal(V:~ground-values, W:values) ~> false
+Rule
+ is-equal(V:values, W:~ground-values) ~> false