squash abstract: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>

spec/abstract/AARCH64/FPU_A.thy

@@ -25,15 +25,14 @@ definition load_fpu_state :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad
      do_machine_op (writeFpuState fpu_state)
    od"
 
-\<comment> \<open>FIXME: maybe use a case instead of the if (depends on if wpc or if_split is easier)\<close>
 definition switch_local_fpu_owner :: "obj_ref option \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "switch_local_fpu_owner new_owner \<equiv> do
      do_machine_op enableFpu;
      cur_fpu_owner \<leftarrow> gets (arm_current_fpu_owner \<circ> arch_state);
-     when (cur_fpu_owner \<noteq> None) $ save_fpu_state (the cur_fpu_owner);
-     if (new_owner \<noteq> None)
-     then load_fpu_state (the new_owner)
-     else do_machine_op disableFpu;
+     maybeM save_fpu_state cur_fpu_owner;
+     case new_owner of
+       None \<Rightarrow> do_machine_op disableFpu
+       | Some tcb_ptr \<Rightarrow> load_fpu_state tcb_ptr;
      modify (\<lambda>s. s \<lparr>arch_state := arch_state s\<lparr>arm_current_fpu_owner := new_owner\<rparr>\<rparr>)
    od"
 
@@ -46,7 +45,7 @@ definition fpu_release :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" w
 definition lazy_fpu_restore :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad" where
   "lazy_fpu_restore thread_ptr \<equiv> do
      flags \<leftarrow> thread_get tcb_flags thread_ptr;
-     if (ArchFlag FpuDisabled \<in> flags)
+     if ArchFlag FpuDisabled \<in> flags
      then do_machine_op disableFpu
      else do
        do_machine_op enableFpu;

spec/abstract/Schedule_A.thy

@@ -168,7 +168,7 @@ instantiation unit :: state_ext_sched
 begin
 
 \<comment> \<open>FIXME: update this comment to mention the state that might be
-  saved as part of arch_prepare_next_domain\<close>
+  saved as part of @{term arch_prepare_next_domain}\<close>
 text \<open>
   The scheduler is heavily underspecified.
   It is allowed to pick any active thread or the idle thread.
@@ -193,9 +193,9 @@ definition schedule_unit :: "(unit,unit) s_monad" where
      cur_active \<leftarrow> gets (getActiveTCB cur);
      idl \<leftarrow> gets idle_thread;
      if cur_active \<noteq> None \<or> idl = cur then
-       return () \<sqinter> (do pre_choose_thread_unit; choose_thread_unit od)
+       return () \<sqinter> do pre_choose_thread_unit; choose_thread_unit od
      else
-       (do pre_choose_thread_unit; choose_thread_unit od)
+       do pre_choose_thread_unit; choose_thread_unit od
    od)"
 
 instance ..

spec/machine/AARCH64/MachineOps.thy

@@ -168,7 +168,7 @@ definition setNextPC :: "machine_word \<Rightarrow> unit user_monad" where
 
 subsection "FPU-related"
 
-\<comment> \<open>FIXME: Should this modify fpu_enabled? The C doesn't update isFPUEnabledCached when this is called directly.\<close>
+\<comment> \<open>FIXME: Should this modify @{term fpu_enabled}? The C doesn't update isFPUEnabledCached when this is called directly.\<close>
 consts' enableFpuEL01_impl :: "unit machine_rest_monad"
 definition enableFpuEL01 :: "unit machine_monad" where
   "enableFpuEL01 \<equiv> machine_op_lift enableFpuEL01_impl"