From 00a0ce9082b4cc1389815defcc806efd4a9b80f4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 18 Apr 2022 15:05:24 +0100 Subject: Do a big refactor. - 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. --- Everything.agda | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'Everything.agda') diff --git a/Everything.agda b/Everything.agda index 2f76af0..87109e2 100644 --- a/Everything.agda +++ b/Everything.agda @@ -96,9 +96,6 @@ import Helium.Data.Pseudocode.Core -- Ways to modify pseudocode statements and expressions. import Helium.Data.Pseudocode.Manipulate --- Basic properties of the pseudocode data types -import Helium.Data.Pseudocode.Properties - -- Definition of instructions using the Armv8-M pseudocode. import Helium.Instructions.Base @@ -117,15 +114,15 @@ import Helium.Semantics.Axiomatic -- Definition of assertions used in correctness triples import Helium.Semantics.Axiomatic.Assertion --- Base definitions for the axiomatic semantics -import Helium.Semantics.Axiomatic.Core - -- Definition of terms for use in assertions import Helium.Semantics.Axiomatic.Term -- Definition of Hoare triples import Helium.Semantics.Axiomatic.Triple +-- Base definitions for semantics +import Helium.Semantics.Core + -- Base definitions for the denotational semantics. import Helium.Semantics.Denotational.Core -- cgit v1.2.3