summaryrefslogtreecommitdiff
path: root/src/gen_lib/deep_shallow_convert.lem
diff options
context:
space:
mode:
authorChristopher Pulte2017-09-19 19:45:36 +0300
committerChristopher Pulte2017-09-19 19:45:36 +0300
commitc3b5af179dde8d0b2c272eb851ebdb59764468d0 (patch)
tree617f555668b941aa29ec8ea9f40daad5510cf188 /src/gen_lib/deep_shallow_convert.lem
parent0ad438b129de243fd573bbf2472858bf853d44c2 (diff)
fix
Diffstat (limited to 'src/gen_lib/deep_shallow_convert.lem')
-rw-r--r--src/gen_lib/deep_shallow_convert.lem14
1 files changed, 7 insertions, 7 deletions
diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
index 4af6eb2f..42a65c49 100644
--- a/src/gen_lib/deep_shallow_convert.lem
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -69,9 +69,9 @@ end
let toInterpValueBitU = function
- | 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)
+ | B1 -> Interp_ast.V_lit (L_aux (L_one) Unknown)
+ | B0 -> Interp_ast.V_lit (L_aux (L_zero) Unknown)
+ | BU -> Interp_ast.V_lit (L_aux (L_undef) Unknown)
end
let rec fromInterpValueBitU v = match v with
| Interp_ast.V_lit (L_aux (L_one) _) -> B1
@@ -391,10 +391,10 @@ let read_kindToInterpValue = function
| 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 ())
+ | Read_RISCV_strong_acquire -> V_ctor (Id_aux (Id "Read_RISCV_strong_acquire") Unknown) (T_id "read_kind") (C_Enum 8) (toInterpValue ())
+ | Read_RISCV_reserved -> V_ctor (Id_aux (Id "Read_RISCV_reserved") Unknown) (T_id "read_kind") (C_Enum 9) (toInterpValue ())
+ | Read_RISCV_reserved_acquire -> V_ctor (Id_aux (Id "Read_RISCV_reserved_acquire") Unknown) (T_id "read_kind") (C_Enum 10) (toInterpValue ())
+ | Read_RISCV_reserved_strong_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