| Age | Commit message (Collapse) | Author |
|---|
|
- 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
This is anticipating the addition of pseudocode as a data type. That
should make the denotational semantics much more performant, and allows
the addition of new forms of semantics without duplicating effort.
|
