From b2a2656c19c5075870fb9d9692c80b1940b1d0d2 Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Fri, 22 Jun 2018 16:50:46 +0200
Subject: [PATCH] Isabelle2018: DSpec

---
 spec/capDL/CNode_D.thy  | 2 +-
 spec/capDL/CSpace_D.thy | 8 ++++----
 spec/capDL/KHeap_D.thy  | 2 +-
 spec/capDL/Types_D.thy  | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/spec/capDL/CNode_D.thy b/spec/capDL/CNode_D.thy
index 32495999c..a9fd59d7e 100644
--- a/spec/capDL/CNode_D.thy
+++ b/spec/capDL/CNode_D.thy
@@ -27,7 +27,7 @@ definition
       cdl_cnode_intent \<Rightarrow> cdl_cnode_invocation except_monad"
 where
   "decode_cnode_invocation target target_ref caps intent \<equiv> case intent of
-     (* Copy a cap to anther capslot, without modifying the cap. *)
+       \<comment> \<open>Copy a cap to anther capslot, without modifying the cap.\<close>
        CNodeCopyIntent dest_index dest_depth src_index src_depth rights \<Rightarrow>
          doE
            (src_root, _) \<leftarrow> throw_on_none $ get_index caps 0;
diff --git a/spec/capDL/CSpace_D.thy b/spec/capDL/CSpace_D.thy
index 14c5266d3..eb82c29d2 100644
--- a/spec/capDL/CSpace_D.thy
+++ b/spec/capDL/CSpace_D.thy
@@ -521,7 +521,7 @@ where
   "resolve_address_bits cnode_cap cap_ptr remaining_size = doE
     unlessE (is_cnode_cap cnode_cap) $ throw;
 
-    (* Fetch the next level CNode. *)
+    \<comment> \<open>Fetch the next level CNode.\<close>
     cnode \<leftarrow> liftE $ get_cnode $ cap_object cnode_cap;
     radix_size \<leftarrow> returnOk $ cdl_cnode_size_bits cnode;
     guard_size \<leftarrow> returnOk $ cap_guard_size cnode_cap;
@@ -529,14 +529,14 @@ where
     level_size \<leftarrow> returnOk (radix_size + guard_size);
     assertE (level_size \<noteq> 0);
 
-    (* Ensure the guard matches up. *)
+    \<comment> \<open>Ensure the guard matches up.\<close>
     guard \<leftarrow> returnOk $ (cap_ptr >> (remaining_size-guard_size)) && (mask guard_size);
     unlessE (guard_size \<le> remaining_size \<and> guard = cap_guard) $ throw;
 
-    (* Ensure we still enough unresolved bits left in our CPTR. *)
+    \<comment> \<open>Ensure we still enough unresolved bits left in our CPTR.\<close>
     whenE (level_size > remaining_size) $ throw;
 
-    (* Find the next slot. *)
+    \<comment> \<open>Find the next slot.\<close>
     offset \<leftarrow> returnOk $ (cap_ptr >> (remaining_size-level_size)) && (mask radix_size);
     slot \<leftarrow> returnOk (cap_object cnode_cap, unat offset);
     size_left \<leftarrow> returnOk (remaining_size - level_size);
diff --git a/spec/capDL/KHeap_D.thy b/spec/capDL/KHeap_D.thy
index a599069f6..f637056d2 100644
--- a/spec/capDL/KHeap_D.thy
+++ b/spec/capDL/KHeap_D.thy
@@ -120,7 +120,7 @@ definition
 where
   "slots_of obj_id \<equiv> \<lambda>s.
   case opt_object obj_id s of
-    None \<Rightarrow> empty
+    None \<Rightarrow> Map.empty
   | Some obj \<Rightarrow> object_slots obj"
 
 (* The cap at the given cap_ref. None if object or cap does not exist *)
diff --git a/spec/capDL/Types_D.thy b/spec/capDL/Types_D.thy
index cc499990a..4504557e8 100644
--- a/spec/capDL/Types_D.thy
+++ b/spec/capDL/Types_D.thy
@@ -460,7 +460,7 @@ where
   | CNode x \<Rightarrow> cdl_cnode_caps x
   | Tcb x \<Rightarrow> cdl_tcb_caps x
   | IRQNode x \<Rightarrow> cdl_irq_node_caps x
-  | _ \<Rightarrow> empty"
+  | _ \<Rightarrow> Map.empty"
 
 definition
   update_slots :: "cdl_cap_map \<Rightarrow> cdl_object \<Rightarrow> cdl_object"