summaryrefslogtreecommitdiff
path: root/src/Helium
AgeCommit message (Collapse)Author
2022-02-15Remove unnecessary return-type part of StatementGreg Brown
2022-02-13Write pseudocode definition of Barrett reductionGreg Brown
2022-02-13Define vmla instruction.Greg Brown
2022-02-13Extract common code from pseudocode instructionsGreg Brown
2022-02-13Refactor to group instruction definitions togetherGreg Brown
2022-02-13Finish definition of denotational semantics.Greg Brown
2022-02-02Define pseudocode for a number of instructions.Greg Brown
2022-01-21Add pseudocode as a data type.Greg Brown
2022-01-19Rename pseudocode file.Greg Brown
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.
2022-01-18Define the semantics of pseudocode data types.Greg Brown
2022-01-16Define ordered algebraic structures.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-07Add a missing raw algebra.Greg Brown
2022-01-07Demonstrate pointwise Vectors inherit algebraic properties.Greg Brown
2022-01-07Add some required algebraic types.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
This is the extraction promised a couple of commits ago.
2021-12-20Define vmul.Greg Brown
2021-12-20Inline and rearrange to make vadd and vhsub look more similar.Greg Brown
If there are other functions with a similar structure, I may extract larger patterns. copy-masked is one example of a structure that was easy to extract.
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-20Add some convenience functions.Greg Brown
2021-12-19Define core of denotational semantics.Greg Brown
2021-12-19Define a minimal interface for working with Arm pseudocode.Greg Brown
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 16:56:29 +0000