From cf9e692e26592fce85db17a6355e1a08db6703ab Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Mon, 2 Dec 2024 14:42:54 +0100 Subject: [PATCH] Add bool field to source Loc values Progress on #1091 --- semantics/semanticPrimitivesScript.sml | 57 +++++++++++++------------- 1 file changed, 29 insertions(+), 28 deletions(-) diff --git a/semantics/semanticPrimitivesScript.sml b/semantics/semanticPrimitivesScript.sml index 91de04ccbe..a49481243a 100644 --- a/semantics/semanticPrimitivesScript.sml +++ b/semantics/semanticPrimitivesScript.sml @@ -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 @@ -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) @@ -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 @@ -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 @@ -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 @@ -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)] ∧ @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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), @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 @@ -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