summaryrefslogtreecommitdiff
path: root/src/Helium/Semantics
AgeCommit message (Expand)Author
2022-03-08Migrate to agda-stdlib-2.0-dev.axiomaticGreg Brown
2022-03-08Add semantics of Hoare logic assertions.Greg Brown
2022-03-08Add semantics of Hoare logic terms.Greg Brown
2022-03-08Add Hoare logic assertionsGreg Brown
2022-03-08Add reference substitution to terms.Greg Brown
2022-03-08Separate out Hoare logic terms.Greg Brown
2022-02-22Add if_then_ statementsGreg Brown
2022-02-21Replace tup with cons and nilGreg Brown
2022-02-21Generalise slice and join into cut and splice.Greg Brown
2022-02-21Introduce tuple deconstructor expressionsGreg Brown
2022-02-21Replace nat indices with fins.Greg Brown
2022-02-19Unalias bit type.Greg Brown
2022-02-18Remove declare case of Procedure.Greg Brown
2022-02-17Make call and invoke take All instead of tuple.Greg Brown
2022-02-16Begin work on axiomatic semantics.Greg Brown
2022-02-15Make expressions unable to change state.Greg Brown
2022-02-15Remove unnecessary return-type part of StatementGreg Brown
2022-02-13Finish definition of denotational semantics.Greg Brown
2022-02-02Define pseudocode for a number of instructions.Greg Brown
2022-01-19Rename pseudocode file.Greg Brown
2022-01-18Define the semantics of pseudocode data types.Greg Brown
2022-01-12Eliminate even more state from the denotational semantics.Greg Brown
2022-01-08Make RawPseudocode contain its own bundles.Greg Brown
2022-01-07Introduce semantics for sequences of instructions.Greg Brown
2022-01-07Rename ⟦_⟧ to float.Greg Brown
2021-12-28Make the denotational semantics total.Greg Brown
2021-12-27Introduce Everything.agda to aid in overall compilation.Greg Brown
2021-12-21Define execBeats, a wrapper to execute beat-wise instructions.Greg Brown
2021-12-21Define semantics of vqdmulh.Greg Brown
2021-12-21Define semantics for vmulh.Greg Brown
2021-12-20Define vsub.Greg Brown
2021-12-20Remove bitstring addition.Greg Brown
2021-12-20Extract structures shared by most binary vector operations.Greg Brown
2021-12-20Define vmul.Greg Brown
2021-12-20Inline and rearrange to make vadd and vhsub look more similar.Greg Brown
2021-12-20Define semantics of vhsub.Greg Brown
2021-12-20Improve type-checking efficiency.Greg Brown
2021-12-20Define semantics for vadd.Greg Brown
2021-12-20Add references to the core denotational semantics.last-attemptGreg Brown
2021-12-19Define core of denotational semantics.Greg Brown