summaryrefslogtreecommitdiff
path: root/src/gen_lib/deep_shallow_convert.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/gen_lib/deep_shallow_convert.lem')
-rw-r--r--src/gen_lib/deep_shallow_convert.lem116
1 files changed, 69 insertions, 47 deletions
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 23c34222..4af6eb2f 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -6,20 +6,20 @@ open import Sail_values
class (ToFromInterpValue 'a)
- val toInterpValue : 'a -> Interp.value
- val fromInterpValue : Interp.value -> 'a
+ val toInterpValue : 'a -> Interp_ast.value
+ val fromInterpValue : Interp_ast.value -> 'a
end
let toInterValueBool = function
- | true -> Interp.V_lit (L_aux (L_one) Unknown)
- | false -> Interp.V_lit (L_aux (L_zero) Unknown)
+ | true -> Interp_ast.V_lit (L_aux (L_one) Unknown)
+ | false -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
end
let rec fromInterpValueBool v = match v with
- | Interp.V_lit (L_aux (L_true) _) -> true
- | Interp.V_lit (L_aux (L_false) _) -> false
- | Interp.V_lit (L_aux (L_one) _) -> true
- | Interp.V_lit (L_aux (L_zero) _) -> false
- | Interp.V_tuple [v] -> fromInterpValueBool v
+ | Interp_ast.V_lit (L_aux (L_true) _) -> true
+ | Interp_ast.V_lit (L_aux (L_false) _) -> false
+ | Interp_ast.V_lit (L_aux (L_one) _) -> true
+ | Interp_ast.V_lit (L_aux (L_zero) _) -> false
+ | Interp_ast.V_tuple [v] -> fromInterpValueBool v
| v -> failwith ("fromInterpValue bool: unexpected value. " ^
Interp.debug_print_value v)
end
@@ -29,10 +29,10 @@ instance (ToFromInterpValue bool)
end
-let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown)
+let toInterpValueUnit () = Interp_ast.V_lit (L_aux (L_unit) Unknown)
let rec fromInterpValueUnit v = match v with
- | Interp.V_lit (L_aux (L_unit) _) -> ()
- | Interp.V_tuple [v] -> fromInterpValueUnit v
+ | Interp_ast.V_lit (L_aux (L_unit) _) -> ()
+ | Interp_ast.V_tuple [v] -> fromInterpValueUnit v
| v -> failwith ("fromInterpValue unit: unexpected value. " ^
Interp.debug_print_value v)
end
@@ -44,8 +44,8 @@ end
let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown)
let rec fromInterpValueInteger v = match v with
- | Interp.V_lit (L_aux (L_num i) _) -> i
- | Interp.V_tuple [v] -> fromInterpValueInteger v
+ | Interp_ast.V_lit (L_aux (L_num i) _) -> i
+ | Interp_ast.V_tuple [v] -> fromInterpValueInteger v
| v -> failwith ("fromInterpValue integer: unexpected value. " ^
Interp.debug_print_value v)
end
@@ -57,8 +57,8 @@ end
let toInterpValueString s = V_lit (L_aux (L_string s) Unknown)
let rec fromInterpValueString v = match v with
- | Interp.V_lit (L_aux (L_string s) _) -> s
- | Interp.V_tuple [v] -> fromInterpValueString v
+ | Interp_ast.V_lit (L_aux (L_string s) _) -> s
+ | Interp_ast.V_tuple [v] -> fromInterpValueString v
| v -> failwith ("fromInterpValue integer: unexpected value. " ^
Interp.debug_print_value v)
end
@@ -69,17 +69,17 @@ end
let toInterpValueBitU = function
- | I -> Interp.V_lit (L_aux (L_one) Unknown)
- | O -> Interp.V_lit (L_aux (L_zero) Unknown)
- | Undef -> Interp.V_lit (L_aux (L_undef) Unknown)
+ | I -> Interp_ast.V_lit (L_aux (L_one) Unknown)
+ | O -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
+ | Undef -> Interp_ast.V_lit (L_aux (L_undef) Unknown)
end
let rec fromInterpValueBitU v = match v with
- | Interp.V_lit (L_aux (L_one) _) -> I
- | Interp.V_lit (L_aux (L_zero) _) -> O
- | Interp.V_lit (L_aux (L_undef) _) -> Undef
- | Interp.V_lit (L_aux (L_true) _) -> I
- | Interp.V_lit (L_aux (L_false) _) -> O
- | Interp.V_tuple [v] -> fromInterpValueBitU v
+ | Interp_ast.V_lit (L_aux (L_one) _) -> B1
+ | Interp_ast.V_lit (L_aux (L_zero) _) -> B0
+ | Interp_ast.V_lit (L_aux (L_undef) _) -> BU
+ | Interp_ast.V_lit (L_aux (L_true) _) -> B1
+ | Interp_ast.V_lit (L_aux (L_false) _) -> B0
+ | Interp_ast.V_tuple [v] -> fromInterpValueBitU v
| v -> failwith ("fromInterpValue bitU: unexpected value. " ^
Interp.debug_print_value v)
end
@@ -383,29 +383,31 @@ instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
end
-module SI = Interp
-module SIA = Interp_ast
-
-
let read_kindToInterpValue = function
| Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ())
- | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
- | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
| Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ())
| Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ())
| Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ())
| Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ())
| Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ())
+ | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_acquire") Unknown) (T_id "read_kind") (C_Enum 7) (toInterpValue ())
+ | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ())
+ | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ())
+ | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ())
+ | Read_RISCV_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ())
end
let rec read_kindFromInterpValue v = match v with
| V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain
- | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag
- | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve
| V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve
| V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire
| V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive
| V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire
| V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream
+ | V_ctor (Id_aux (Id "Read_RISCV_acquire") _) _ _ v -> Read_RISCV_acquire
+ | V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") _) _ _ v -> Read_RISCV_strong_acquire
+ | V_ctor (Id_aux (Id "Read_RISCV_reserved") _) _ _ v -> Read_RISCV_reserved
+ | V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") _) _ _ v -> Read_RISCV_reserved_acquire
+ | V_ctor (Id_aux (Id "Read_RISCV_reserved_strong_acquire") _) _ _ v -> Read_RISCV_reserved_strong_acquire
| V_tuple [v] -> read_kindFromInterpValue v
| v -> failwith ("fromInterpValue read_kind: unexpected value. " ^
Interp.debug_print_value v)
@@ -418,21 +420,27 @@ end
let write_kindToInterpValue = function
| Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ())
- | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
- | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
| Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ())
| Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ())
| Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ())
| Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ())
+ | Write_RISCV_release -> V_ctor (Id_aux (Id "Write_RISCV_release") Unknown) (T_id "write_kind") (C_Enum 6) (toInterpValue ())
+ | Write_RISCV_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_strong_release") Unknown) (T_id "write_kind") (C_Enum 7) (toInterpValue ())
+ | Write_RISCV_conditional -> V_ctor (Id_aux (Id "Write_RISCV_conditional") Unknown) (T_id "write_kind") (C_Enum 8) (toInterpValue ())
+ | Write_RISCV_conditional_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_release") Unknown) (T_id "write_kind") (C_Enum 9) (toInterpValue ())
+ | Write_RISCV_conditional_strong_release -> V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") Unknown) (T_id "write_kind") (C_Enum 10) (toInterpValue ())
end
let rec write_kindFromInterpValue v = match v with
| V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain
- | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag
- | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional
| V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional
| V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release
| V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive
| V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release
+ | V_ctor (Id_aux (Id "Write_RISCV_release") _) _ _ v -> Write_RISCV_release
+ | V_ctor (Id_aux (Id "Write_RISCV_strong_release") _) _ _ v -> Write_RISCV_strong_release
+ | V_ctor (Id_aux (Id "Write_RISCV_conditional") _) _ _ v -> Write_RISCV_conditional
+ | V_ctor (Id_aux (Id "Write_RISCV_conditional_release") _) _ _ v -> Write_RISCV_conditional_release
+ | V_ctor (Id_aux (Id "Write_RISCV_conditional_strong_release") _) _ _ v -> Write_RISCV_conditional_strong_release
| V_tuple [v] -> write_kindFromInterpValue v
| v -> failwith ("fromInterpValue write_kind: unexpected value " ^
Interp.debug_print_value v)
@@ -455,7 +463,14 @@ let barrier_kindToInterpValue = function
| Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ())
| Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ())
| Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ())
- | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ())
+ | Barrier_TM_COMMIT -> V_ctor (Id_aux (Id "Barrier_TM_COMMIT") Unknown) (T_id "barrier_kind") (C_Enum 11) (toInterpValue ())
+ | Barrier_MIPS_SYNC -> V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") Unknown) (T_id "barrier_kind") (C_Enum 12) (toInterpValue ())
+ | Barrier_RISCV_rw_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") Unknown) (T_id "barrier_kind") (C_Enum 13) (toInterpValue ())
+ | Barrier_RISCV_r_rw -> V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") Unknown) (T_id "barrier_kind") (C_Enum 14) (toInterpValue ())
+ | Barrier_RISCV_rw_w -> V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") Unknown) (T_id "barrier_kind") (C_Enum 15) (toInterpValue ())
+ | Barrier_RISCV_w_w -> V_ctor (Id_aux (Id "Barrier_RISCV_w_w") Unknown) (T_id "barrier_kind") (C_Enum 16) (toInterpValue ())
+ | Barrier_RISCV_i -> V_ctor (Id_aux (Id "Barrier_RISCV_i") Unknown) (T_id "barrier_kind") (C_Enum 17) (toInterpValue ())
+ | Barrier_x86_MFENCE -> V_ctor (Id_aux (Id "Barrier_x86_MFENCE") Unknown) (T_id "barrier_kind") (C_Enum 18) (toInterpValue ())
end
let rec barrier_kindFromInterpValue v = match v with
| V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync
@@ -469,7 +484,14 @@ let rec barrier_kindFromInterpValue v = match v with
| V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST
| V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD
| V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB
+ | V_ctor (Id_aux (Id "Barrier_TM_COMMIT") _) _ _ v -> Barrier_TM_COMMIT
| V_ctor (Id_aux (Id "Barrier_MIPS_SYNC") _) _ _ v -> Barrier_MIPS_SYNC
+ | V_ctor (Id_aux (Id "Barrier_RISCV_rw_rw") _) _ _ v -> Barrier_RISCV_rw_rw
+ | V_ctor (Id_aux (Id "Barrier_RISCV_r_rw") _) _ _ v -> Barrier_RISCV_r_rw
+ | V_ctor (Id_aux (Id "Barrier_RISCV_rw_w") _) _ _ v -> Barrier_RISCV_rw_w
+ | V_ctor (Id_aux (Id "Barrier_RISCV_w_w") _) _ _ v -> Barrier_RISCV_w_w
+ | V_ctor (Id_aux (Id "Barrier_RISCV_i") _) _ _ v -> Barrier_RISCV_i
+ | V_ctor (Id_aux (Id "Barrier_x86_MFENCE") _) _ _ v -> Barrier_x86_MFENCE
| V_tuple [v] -> barrier_kindFromInterpValue v
| v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^
Interp.debug_print_value v)
@@ -503,18 +525,18 @@ instance (ToFromInterpValue instruction_kind)
end
let regfpToInterpValue = function
- | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
- | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
- | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
- | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
+ | RFull v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
+ | RSlice v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
+ | RSliceBit v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
+ | RField v -> Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") Interp_ast.Unknown) (Interp_ast.T_id "regfp") Interp_ast.C_Union (toInterpValue v)
end
let rec regfpFromInterpValue v = match v with
- | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
- | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
- | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
- | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v)
- | SI.V_tuple [v] -> regfpFromInterpValue v
+ | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
+ | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
+ | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
+ | Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id "RField") _) _ _ v -> RField (fromInterpValue v)
+ | Interp_ast.V_tuple [v] -> regfpFromInterpValue v
| v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v)
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:48:27 +0000