summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-03-03Add function to eliminate all calls in expressionsGreg Brown
2022-03-03Add way to convert function calls to expressionsGreg Brown
2022-02-22Add if_then_ statementsGreg Brown
2022-02-22Change stateful expressions to index on expressionGreg 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-19Add predicate for being a sliced type.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-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
generated by cgit v1.2.3 (git 2.49.0) at 2025-04-30 23:13:16 +0000