From 2aadbf958981b2bf247915aa546ce56112b8319d Mon Sep 17 00:00:00 2001
From: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
Date: Thu, 24 Jun 2021 18:23:18 +1000
Subject: [PATCH] trivial: restyle `spec/machine/ARM*/Platform.thy`

Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
---
 spec/machine/ARM/Platform.thy     | 30 +++++++--------------
 spec/machine/ARM_HYP/Platform.thy | 44 +++++++++++--------------------
 2 files changed, 26 insertions(+), 48 deletions(-)

diff --git a/spec/machine/ARM/Platform.thy b/spec/machine/ARM/Platform.thy
index e34707af7..307b4073e 100644
--- a/spec/machine/ARM/Platform.thy
+++ b/spec/machine/ARM/Platform.thy
@@ -29,45 +29,35 @@ type_synonym paddr = word32
 abbreviation (input) "toPAddr \<equiv> id"
 abbreviation (input) "fromPAddr \<equiv> id"
 
-definition
-  pageColourBits :: nat where
+definition pageColourBits :: nat where
   "pageColourBits \<equiv> 2"
 
-definition
-  cacheLineBits :: nat where
+definition cacheLineBits :: nat where
   "cacheLineBits = 5"
 
-definition
-  cacheLine :: nat where
+definition cacheLine :: nat where
   "cacheLine = 2^cacheLineBits"
 
 (* Arch specific kernel base address used for haskell spec *)
-definition
-  pptrBase :: word32 where
+definition pptrBase :: word32 where
   "pptrBase \<equiv> 0xe0000000"
 
-definition
-  physBase :: word32 where
+definition physBase :: word32 where
   "physBase \<equiv> 0x10000000"
 
-definition
-  pptrBaseOffset :: word32 where
+definition pptrBaseOffset :: word32 where
   "pptrBaseOffset \<equiv> pptrBase - physBase"
 
-definition
-  ptrFromPAddr :: "paddr \<Rightarrow> word32" where
+definition ptrFromPAddr :: "paddr \<Rightarrow> word32" where
   "ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
 
-definition
-  addrFromPPtr :: "word32 \<Rightarrow> paddr" where
+definition addrFromPPtr :: "word32 \<Rightarrow> paddr" where
   "addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
 
-definition
-  minIRQ :: "irq" where
+definition minIRQ :: "irq" where
   "minIRQ \<equiv> 0"
 
-definition
-  maxIRQ :: "irq" where
+definition maxIRQ :: "irq" where
   "maxIRQ \<equiv> 0x9F"
 
 end
diff --git a/spec/machine/ARM_HYP/Platform.thy b/spec/machine/ARM_HYP/Platform.thy
index 2a0b60465..7f9b72ced 100644
--- a/spec/machine/ARM_HYP/Platform.thy
+++ b/spec/machine/ARM_HYP/Platform.thy
@@ -29,62 +29,50 @@ type_synonym paddr = word32
 abbreviation (input) "toPAddr \<equiv> id"
 abbreviation (input) "fromPAddr \<equiv> id"
 
-definition
-  pageColourBits :: nat where
+definition pageColourBits :: nat where
   "pageColourBits \<equiv> 2"
 
-definition
-  cacheLineBits :: nat where
+definition cacheLineBits :: nat where
   "cacheLineBits = 6"
 
-definition
-  cacheLine :: nat where
+definition cacheLine :: nat where
   "cacheLine = 2^cacheLineBits"
 
 (* Arch specific kernel base address used for haskell spec *)
-definition
-  pptrBase :: word32 where
+definition pptrBase :: word32 where
   "pptrBase \<equiv> 0xe0000000"
 
-definition
-  physBase :: word32 where
+definition physBase :: word32 where
   "physBase \<equiv> 0x80000000"
 
 abbreviation (input) "paddrBase \<equiv> physBase"
 
-definition
-  pptrTop :: "32 word" where
+definition pptrTop :: "32 word" where
   "pptrTop \<equiv> 0xfff00000"
 
-definition
-  paddrTop :: "32 word" where
+definition paddrTop :: "32 word" where
   "paddrTop \<equiv> pptrTop - (pptrBase - physBase)"
 
-definition
-  pptrBaseOffset :: word32 where
+definition pptrBaseOffset :: word32 where
   "pptrBaseOffset \<equiv> pptrBase - physBase"
 
-definition
-  ptrFromPAddr :: "paddr \<Rightarrow> word32" where
+definition ptrFromPAddr :: "paddr \<Rightarrow> word32" where
   "ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
 
-definition
-  addrFromPPtr :: "word32 \<Rightarrow> paddr" where
+definition addrFromPPtr :: "word32 \<Rightarrow> paddr" where
   "addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
 
-definition
-  minIRQ :: "irq" where
+definition minIRQ :: "irq" where
   "minIRQ \<equiv> 0"
 
-definition
-  maxIRQ :: "irq" where
+definition maxIRQ :: "irq" where
   "maxIRQ \<equiv> 191"
 
-definition irqVGICMaintenance :: "irq"
-  where "irqVGICMaintenance \<equiv> 25"
+definition irqVGICMaintenance :: "irq" where
+  "irqVGICMaintenance \<equiv> 25"
 
-definition irqVTimerEvent :: "irq"
-  where "irqVTimerEvent  \<equiv> 27"
+definition irqVTimerEvent :: "irq" where
+  "irqVTimerEvent  \<equiv> 27"
 
 end