Add bool to Loc values

Author: myreen

characteristic/cfHeapsBaseScript.sml

@@ -233,19 +233,19 @@ End
 (* A reference cell, as a convenience wrapper over cell and Refv *)
 Definition REF_def:
   REF rv xv =
-    SEP_EXISTS loc. cond (rv = Loc loc) * cell loc (Refv xv)
+    SEP_EXISTS loc. cond (rv = Loc T loc) * cell loc (Refv xv)
 End
 
 (* An array cell, as a wrapper over cell and Varray *)
 Definition ARRAY_def:
   ARRAY av vl =
-    SEP_EXISTS loc. cond (av = Loc loc) * cell loc (Varray vl)
+    SEP_EXISTS loc. cond (av = Loc T loc) * cell loc (Varray vl)
 End
 
 (* A bytearray cell, as a wrapper over cell and W8array *)
 Definition W8ARRAY_def:
   W8ARRAY av wl =
-    SEP_EXISTS loc. cond (av = Loc loc) * cell loc (W8array wl)
+    SEP_EXISTS loc. cond (av = Loc T loc) * cell loc (W8array wl)
 End
 
 Definition IO_def:

characteristic/cfLetAutoScript.sml

@@ -143,7 +143,7 @@ metis_tac[HEAP_FROM_STATE_def, UNIQUE_PTRS_HFS]
 QED
 
 Theorem PTR_IN_HEAP:
- !l xv H s. (REF (Loc l) xv * H) s ==> Mem l (Refv xv) IN s
+ !l xv H s. (REF (Loc T l) xv * H) s ==> Mem l (Refv xv) IN s
 Proof
 fs[STAR_def, SPLIT_def] >>
 fs[REF_def, SEP_EXISTS] >>

characteristic/cfScript.sml

@@ -3053,7 +3053,7 @@ Proof
       cf_exp2v_evaluate_tac `st` \\ first_assum progress \\
       rename1 `SPLIT h_i (h_i', _)` \\ rename1 `FF h_i'` \\
       fs [do_app_def, store_assign_def] \\
-      rename1 `rv = Loc r` \\ rw [] \\
+      rename1 `rv = Loc T r` \\ rw [] \\
       `Mem r (Refv x') IN (st2heap p st)` by SPLIT_TAC \\
       `Mem r (Refv x') IN (store2heap st.refs)` by
           fs [st2heap_def,Mem_NOT_IN_ffi2heap] \\
@@ -3080,7 +3080,7 @@ Proof
       fs [st2heap_def, cond_def, SEP_IMP_def, STAR_def, one_def, cell_def] \\
       GEN_EXISTS_TAC "ck" `st.clock` \\ fs [with_clock_self] \\
       cf_exp2v_evaluate_tac `st` \\
-      first_x_assum (qspec_then `Loc (LENGTH st.refs)` strip_assume_tac) \\
+      first_x_assum (qspec_then `Loc T (LENGTH st.refs)` strip_assume_tac) \\
       first_x_assum (qspec_then `Mem (LENGTH st.refs) (Refv xv) INSERT h_i` mp_tac) \\
       assume_tac store2heap_alloc_disjoint \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
@@ -3102,7 +3102,7 @@ Proof
       rpt (first_x_assum progress) \\
       fs [do_app_def, store_lookup_def] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
-      rename1 `rv = Loc r` \\ rw [] \\
+      rename1 `rv = Loc T r` \\ rw [] \\
       `Mem r (Refv x) IN (store2heap st.refs)` by SPLIT_TAC \\
       progress store2heap_IN_LENGTH \\ progress store2heap_IN_EL \\
       fs [state_component_equality]
@@ -3115,7 +3115,7 @@ Proof
       fs [do_app_def, store_alloc_def, st2heap_def] \\
       fs [app_aalloc_def, app_aw8alloc_def, W8ARRAY_def, ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, cell_def, one_def] \\
-      first_x_assum (qspec_then `Loc (LENGTH st.refs)` strip_assume_tac) \\
+      first_x_assum (qspec_then `Loc T (LENGTH st.refs)` strip_assume_tac) \\
       qmatch_asmsub_rename_tac(`REPLICATE (Num n) vv`) \\
       ((rename1 `W8array _` \\ (fn l => first_x_assum (qspecl_then l mp_tac))
           [`Mem (LENGTH st.refs) (W8array (REPLICATE (Num n) vv)) INSERT h_i`])
@@ -3141,7 +3141,7 @@ Proof
       fs [do_app_def, store_alloc_def, st2heap_def] \\
       fs [app_aalloc_def, app_aw8alloc_def, W8ARRAY_def, ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, cell_def, one_def] \\
-      first_x_assum (qspec_then `Loc (LENGTH st.refs)` strip_assume_tac) \\
+      first_x_assum (qspec_then `Loc T (LENGTH st.refs)` strip_assume_tac) \\
       ((rename1 `W8array _` \\ (fn l => first_x_assum (qspecl_then l mp_tac))
           [`Mem (LENGTH st.refs) (W8array []) INSERT h_i`])
         ORELSE (fn l => first_x_assum (qspecl_then l mp_tac))
@@ -3166,7 +3166,7 @@ Proof
       fs [st2heap_def, app_aw8sub_def, app_asub_def, W8ARRAY_def, ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, one_def, cell_def] \\
       progress SPLIT3_of_SPLIT_emp3 \\ instantiate \\
-      rpt (first_x_assum progress) \\ rename1 `a = Loc l` \\ rw [] \\
+      rpt (first_x_assum progress) \\ rename1 `a = Loc T l` \\ rw [] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
       fs [do_app_def, store_lookup_def] \\
       ((`Mem l (W8array ws) IN (store2heap st.refs)` by SPLIT_TAC) ORELSE
@@ -3186,7 +3186,7 @@ Proof
       fs [SEP_EXISTS, SEP_IMP_def, STAR_def, one_def, cell_def, cond_def] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
       progress SPLIT3_of_SPLIT_emp3 \\ instantiate \\
-      rpt (first_x_assum progress) \\ rename1 `a = Loc l` \\ rw [] \\
+      rpt (first_x_assum progress) \\ rename1 `a = Loc T l` \\ rw [] \\
       fs [do_app_def, store_lookup_def] \\
       ((`Mem l (W8array ws) IN (store2heap st.refs)` by SPLIT_TAC) ORELSE
        (`Mem l (Varray vs) IN (store2heap st.refs)` by SPLIT_TAC)) \\
@@ -3201,7 +3201,7 @@ Proof
       fs [st2heap_def, app_aw8update_def, app_aupdate_def] \\
       fs [W8ARRAY_def, ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, one_def, cell_def] \\
-      first_x_assum progress \\ rename1 `a = Loc l` \\ rw [] \\
+      first_x_assum progress \\ rename1 `a = Loc T l` \\ rw [] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
       ((rename1 `W8array _` \\
         `Mem l (W8array ws) IN (store2heap st.refs)` by SPLIT_TAC) ORELSE
@@ -3237,7 +3237,7 @@ Proof
       fs [W8ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, one_def, cell_def] \\
       first_x_assum progress
-      \\ rename1 `d = Loc ld` \\ rw [] \\
+      \\ rename1 `d = Loc T ld` \\ rw [] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
       (rename1 `W8array _` \\
         `Mem ld (W8array wd) IN (store2heap st.refs)` by SPLIT_TAC) \\
@@ -3271,7 +3271,7 @@ Proof
       fs [W8ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, one_def, cell_def] \\
       first_x_assum progress
-      \\ rename1 `s = Loc ls` \\ rw [] \\
+      \\ rename1 `s = Loc T ls` \\ rw [] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
       (rename1 `W8array _` \\
         `Mem ls (W8array ws) IN (store2heap st.refs)` by SPLIT_TAC) \\
@@ -3297,7 +3297,7 @@ Proof
       fs [W8ARRAY_def] \\
       fs [SEP_EXISTS, cond_def, SEP_IMP_def, STAR_def, one_def, cell_def] \\
       first_x_assum progress
-      \\ rename1 `s = Loc ls` \\ rename1 `d = Loc ld` \\ rw [] \\
+      \\ rename1 `s = Loc T ls` \\ rename1 `d = Loc T ld` \\ rw [] \\
       assume_tac (GEN_ALL Mem_NOT_IN_ffi2heap) \\
       rename1`Mem ls (W8array ws)` \\
       (rename1 `W8array _` \\