Skip to content

Commit

Permalink
Add bool field to source Loc values
Browse files Browse the repository at this point in the history 
Progress on #1091
  • Loading branch information
@myreen
myreen committed Dec 2, 2024
1 parent d0fd8fe commit cf9e692
Showing 1 changed file with 29 additions and 28 deletions.
57 changes: 29 additions & 28 deletions semantics/semanticPrimitivesScript.sml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ Datatype:
* The last variable name indicates which function from the mutually
* recursive bundle this closure value represents *)
| Recclosure (v sem_env) ((varN # varN # exp) list) varN
| Loc num
| Loc bool (* = is allowed *) num (* address *)
| Vectorv (v list)
| FP_WordTree fp_word_val
| FP_BoolTree fp_bool_val
Expand Down Expand Up @@ -385,7 +385,7 @@ Definition compress_def:
compress (Closure env x e) = (Closure env x e) ∧
compress (Env env n) = (Env env n) ∧
compress (Recclosure env es x) = (Recclosure env es x) ∧
compress (Loc n) = (Loc n) ∧
compress (Loc b n) = (Loc b n) ∧
compress (Vectorv vs) = (Vectorv (compress_list vs)) ∧
compress_list [] = [] ∧
compress_list (v::vs) = (compress v)::(compress_list vs)
Expand Down Expand Up @@ -419,7 +419,7 @@ Definition pmatch_def:
pmatch envC s (Pcon NONE ps) (Conv NONE vs) env =
(if LENGTH ps = LENGTH vs then pmatch_list envC s ps vs env
else Match_type_error) ∧
pmatch envC s (Pref p) (Loc lnum) env =
pmatch envC s (Pref p) (Loc _ lnum) env =
(case store_lookup lnum s of
NONE => Match_type_error
| SOME (Refv v) => pmatch envC s p v env
Expand Down Expand Up @@ -477,7 +477,8 @@ End
Definition do_eq_def:
do_eq (Litv l1) (Litv l2) =
(if lit_same_type l1 l2 then Eq_val (l1 = l2) else Eq_type_error) ∧
do_eq (Loc l1) (Loc l2) = Eq_val (l1 = l2) ∧
do_eq (Loc b1 l1) (Loc b2 l2) =
(if b1 ∧ b2 then Eq_val (l1 = l2) else Eq_type_error) ∧
do_eq (Conv cn1 vs1) (Conv cn2 vs2) =
(if cn1 = cn2 ∧ LENGTH vs1 = LENGTH vs2 then do_eq_list vs1 vs2
else if ctor_same_type cn1 cn2 then Eq_val F
Expand Down Expand Up @@ -682,7 +683,7 @@ End
Definition concrete_v_def:
(concrete_v v ⇔
case v of
| Loc _ => T
| Loc _ _ => T
| Litv _ => T
| Conv v_ vs => concrete_v_list vs
| Vectorv vs => concrete_v_list vs
Expand Down Expand Up @@ -867,7 +868,7 @@ Definition do_fpoptimise_def:
do_fpoptimise sc [Conv st vs] = [Conv st (do_fpoptimise sc vs)] ∧
do_fpoptimise sc [Closure env x e] = [Closure env x e] ∧
do_fpoptimise sc [Recclosure env ls x] = [Recclosure env ls x] ∧
do_fpoptimise sc [Loc n] = [Loc n] ∧
do_fpoptimise sc [Loc b n] = [Loc b n] ∧
do_fpoptimise sc [Vectorv vs] = [Vectorv (do_fpoptimise sc vs)] ∧
do_fpoptimise sc [Real r]= [Real r] ∧
do_fpoptimise sc [FP_WordTree fp] = [FP_WordTree (Fp_wopt sc fp)] ∧
Expand Down Expand Up @@ -953,15 +954,15 @@ Definition do_app_def:
Eq_type_error => NONE
| Eq_val b => SOME ((s,t), Rval (Boolv b))
)
| (Opassign, [Loc lnum; v]) =>
| (Opassign, [Loc b lnum; v]) =>
(case store_assign lnum (Refv v) s of
SOME s' => SOME ((s',t), Rval (Conv NONE []))
| NONE => NONE
)
| (Opref, [v]) =>
let (s',n) = (store_alloc (Refv v) s) in
SOME ((s',t), Rval (Loc n))
| (Opderef, [Loc n]) =>
SOME ((s',t), Rval (Loc T n))
| (Opderef, [Loc b n]) =>
(case store_lookup n s of
SOME (Refv v) => SOME ((s,t),Rval v)
| _ => NONE
Expand All @@ -973,8 +974,8 @@ Definition do_app_def:
let (s',lnum) =
(store_alloc (W8array (REPLICATE (Num (ABS (I n))) w)) s)
in
SOME ((s',t), Rval (Loc lnum))
| (Aw8sub, [Loc lnum; Litv (IntLit i)]) =>
SOME ((s',t), Rval (Loc T lnum))
| (Aw8sub, [Loc _ lnum; Litv (IntLit i)]) =>
(case store_lookup lnum s of
SOME (W8array ws) =>
if i <( 0 : int) then
Expand All @@ -987,7 +988,7 @@ Definition do_app_def:
SOME ((s,t), Rval (Litv (Word8 (EL n ws))))
| _ => NONE
)
| (Aw8sub_unsafe, [Loc lnum; Litv (IntLit i)]) =>
| (Aw8sub_unsafe, [Loc _ lnum; Litv (IntLit i)]) =>
(case store_lookup lnum s of
SOME (W8array ws) =>
if i <( 0 : int) then
Expand All @@ -1000,13 +1001,13 @@ Definition do_app_def:
SOME ((s,t), Rval (Litv (Word8 (EL n ws))))
| _ => NONE
)
| (Aw8length, [Loc n]) =>
| (Aw8length, [Loc _ n]) =>
(case store_lookup n s of
SOME (W8array ws) =>
SOME ((s,t),Rval (Litv(IntLit(int_of_num(LENGTH ws)))))
| _ => NONE
)
| (Aw8update, [Loc lnum; Litv(IntLit i); Litv(Word8 w)]) =>
| (Aw8update, [Loc _ lnum; Litv(IntLit i); Litv(Word8 w)]) =>
(case store_lookup lnum s of
SOME (W8array ws) =>
if i <( 0 : int) then
Expand All @@ -1022,7 +1023,7 @@ Definition do_app_def:
)
| _ => NONE
)
| (Aw8update_unsafe, [Loc lnum; Litv(IntLit i); Litv(Word8 w)]) =>
| (Aw8update_unsafe, [Loc _ lnum; Litv(IntLit i); Litv(Word8 w)]) =>
(case store_lookup lnum s of
SOME (W8array ws) =>
if i <( 0 : int) then
Expand Down Expand Up @@ -1056,7 +1057,7 @@ Definition do_app_def:
| SOME cs => Rval (Litv(StrLit(IMPLODE(cs))))
))
| (CopyStrAw8, [Litv(StrLit str);Litv(IntLit off);Litv(IntLit len);
Loc dst;Litv(IntLit dstoff)]) =>
Loc _ dst;Litv(IntLit dstoff)]) =>
(case store_lookup dst s of
SOME (W8array ws) =>
(case copy_array (EXPLODE str,off) len (SOME(ws_to_chars ws,dstoff)) of
Expand All @@ -1069,7 +1070,7 @@ Definition do_app_def:
)
| _ => NONE
)
| (CopyAw8Str, [Loc src;Litv(IntLit off);Litv(IntLit len)]) =>
| (CopyAw8Str, [Loc _ src;Litv(IntLit off);Litv(IntLit len)]) =>
(case store_lookup src s of
SOME (W8array ws) =>
SOME ((s,t),
Expand All @@ -1079,8 +1080,8 @@ Definition do_app_def:
))
| _ => NONE
)
| (CopyAw8Aw8, [Loc src;Litv(IntLit off);Litv(IntLit len);
Loc dst;Litv(IntLit dstoff)]) =>
| (CopyAw8Aw8, [Loc _ src;Litv(IntLit off);Litv(IntLit len);
Loc _ dst;Litv(IntLit dstoff)]) =>
(case (store_lookup src s, store_lookup dst s) of
(SOME (W8array ws), SOME (W8array ds)) =>
(case copy_array (ws,off) len (SOME(ds,dstoff)) of
Expand Down Expand Up @@ -1160,16 +1161,16 @@ Definition do_app_def:
let (s',lnum) =
(store_alloc (Varray (REPLICATE (Num (ABS (I n))) v)) s)
in
SOME ((s',t), Rval (Loc lnum))
SOME ((s',t), Rval (Loc T lnum))
| (AallocEmpty, [Conv NONE []]) =>
let (s',lnum) = (store_alloc (Varray []) s) in
SOME ((s',t), Rval (Loc lnum))
SOME ((s',t), Rval (Loc T lnum))
| (AallocFixed, vs) =>
let (s',lnum) =
(store_alloc (Varray vs) s)
in
SOME ((s',t), Rval (Loc lnum))
| (Asub, [Loc lnum; Litv (IntLit i)]) =>
SOME ((s',t), Rval (Loc T lnum))
| (Asub, [Loc _ lnum; Litv (IntLit i)]) =>
(case store_lookup lnum s of
SOME (Varray vs) =>
if i <( 0 : int) then
Expand All @@ -1182,7 +1183,7 @@ Definition do_app_def:
SOME ((s,t), Rval (EL n vs))
| _ => NONE
)
| (Asub_unsafe, [Loc lnum; Litv (IntLit i)]) =>
| (Asub_unsafe, [Loc _ lnum; Litv (IntLit i)]) =>
(case store_lookup lnum s of
SOME (Varray vs) =>
if i <( 0 : int) then
Expand All @@ -1195,13 +1196,13 @@ Definition do_app_def:
SOME ((s,t), Rval (EL n vs))
| _ => NONE
)
| (Alength, [Loc n]) =>
| (Alength, [Loc _ n]) =>
(case store_lookup n s of
SOME (Varray ws) =>
SOME ((s,t),Rval (Litv(IntLit(int_of_num(LENGTH ws)))))
| _ => NONE
)
| (Aupdate, [Loc lnum; Litv (IntLit i); v]) =>
| (Aupdate, [Loc _ lnum; Litv (IntLit i); v]) =>
(case store_lookup lnum s of
SOME (Varray vs) =>
if i <( 0 : int) then
Expand All @@ -1217,7 +1218,7 @@ Definition do_app_def:
)
| _ => NONE
)
| (Aupdate_unsafe, [Loc lnum; Litv (IntLit i); v]) =>
| (Aupdate_unsafe, [Loc _ lnum; Litv (IntLit i); v]) =>
(case store_lookup lnum s of
SOME (Varray vs) =>
if i <( 0 : int) then
Expand All @@ -1235,7 +1236,7 @@ Definition do_app_def:
)
| (ConfigGC, [Litv (IntLit i); Litv (IntLit j)]) =>
SOME ((s,t), Rval (Conv NONE []))
| (FFI n, [Litv(StrLit conf); Loc lnum]) =>
| (FFI n, [Litv(StrLit conf); Loc _ lnum]) =>
(case store_lookup lnum s of
SOME (W8array ws) =>
(case call_FFI t (ExtCall n) (MAP (n2w o ORD) conf) ws of
Expand Down

0 comments on commit cf9e692

Please sign in to comment.