yellowsquid/helium.git/src/Helium/Semantics/Denotational, branch master [no description] http://git.yellowsquid.uk/yellowsquid/helium.git/atom?h=master 2022-04-18T14:21:38Z Do a big refactor. 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. Add more properties for ordered structures. 2022-04-02T10:59:21Z Greg Brown greg.brown@cl.cam.ac.uk 2022-04-02T10:41:51Z urn:sha1:2167866c53aa7f9cbb52e776bfb64f53acf3fa2c Rename Pseudocode.Types to something more sensible 2022-03-20T14:05:57Z Greg Brown greg.brown@cl.cam.ac.uk 2022-03-20T14:05:57Z urn:sha1:0ceb2b6f579c94fe82dbe17e073408145f637fcb Modify pseudocode definition. 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. Make expressions unable to change state. 2022-02-15T17:04:28Z Greg Brown greg.brown@cl.cam.ac.uk 2022-02-15T17:04:28Z urn:sha1:78aad93db3d7029e0a9a8517a2db92533fd1f401 Remove unnecessary return-type part of Statement 2022-02-15T15:40:04Z Greg Brown greg.brown@cl.cam.ac.uk 2022-02-15T15:40:04Z urn:sha1:146aa079c60c25e1953b94d9799ef520243aefdb Finish definition of denotational semantics. 2022-02-13T13:51:43Z Greg Brown greg.brown@cl.cam.ac.uk 2022-02-13T13:51:43Z urn:sha1:687f7031131ac12bd382be831114661be785dd0d Define pseudocode for a number of instructions. 2022-02-02T14:18:34Z Greg Brown greg.brown@cl.cam.ac.uk 2022-02-02T14:18:34Z urn:sha1:e947c8ef6c844b612e7aec9670f67d00008661e3 Eliminate even more state from the denotational semantics. 2022-01-12T18:32:48Z Greg Brown greg.brown@cl.cam.ac.uk 2022-01-12T18:32:48Z urn:sha1:9901eac3a64249b58789588385a10df9802c9f42 Make the denotational semantics total. 2021-12-28T03:01:55Z Greg Brown greg.brown@cl.cam.ac.uk 2021-12-28T02:46:50Z urn:sha1:5052a3f5ddf5cc65bb5a19e644b01694ba34d0f5