[no description] http://git.yellowsquid.uk/yellowsquid/helium.git/atom?h=master 2022-04-18T14:21:38Z 2022-04-18T14:21:38Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-18T14:05:24Z urn:sha1:00a0ce9082b4cc1389815defcc806efd4a9b80f4 - Replace the decidable predicates on expressions and statements with separate data types. - Reorganise the Hoare logic semantics to remove unnecessary definitions. - Make liberal use of modules to group related definitions together. - Unify the types for denotational and Hoare logic semantics. - Make bits an abstraction of array types. 2022-03-19T13:53:40Z Greg Brown greg.brown@cl.cam.ac.uk 2022-03-19T13:28:42Z urn:sha1:535e4297a08c626d0e2e1923914727f914b8c9bd This change makes the following changes to the definition of pseudocode: - Add a separate type `bit` for single-bit values. - Change `var` and `state` to take `Fin`s instead of bounded naturals. - Make `[_]` and `unbox` work for any sliced type. - Generalise `_:_` and `slice` into `splice` and `cut` respectively, making the two new operations inverses. - Replace `tup` with `nil` and `cons` for building tuples. - Add destructors `head` and `tail` for tuple types. - Make function and procedure calls take a vector of arguments instead of a tuple. - Introduce an `if_then_` expression for if statements with a trivial else branch. 2022-02-13T15:28:51Z Greg Brown greg.brown@cl.cam.ac.uk 2022-02-13T15:28:51Z urn:sha1:d00c4d301f2995ac40a011b711f2c16526e188b8