diff options
| author | Kathy Gray | 2015-05-19 14:59:15 +0100 |
|---|---|---|
| committer | Kathy Gray | 2015-05-19 14:59:15 +0100 |
| commit | 2667b17d8bd508b49674928b7440d779f66431cc (patch) | |
| tree | 6cdc8227fd2b75a284c29b9e4cdd957939ed0f41 /src | |
| parent | 7d0eb548189fd99f4f03153d5e6809886aba95f6 (diff) | |
Add signed and unsigned functions, converting bit vectors to appropriate numbers (explicit instead of implicit in operations)
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 2 | ||||
| -rw-r--r-- | src/type_internal.ml | 17 |
2 files changed, 18 insertions, 1 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index bcacaabc..06aabd46 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -683,6 +683,8 @@ let library_functions direction = [ ("gt_vec_unsigned", compare_op_vec (>) Unsigned); ("lteq_vec_unsigned", compare_op_vec (<=) Unsigned); ("gteq_vec_unsigned", compare_op_vec (>=) Unsigned); + ("signed", to_num Signed); + ("unsigned", to_num Unsigned); ("ltu", compare_op_vec_unsigned (<)); ("gtu", compare_op_vec_unsigned (>)); ("duplicate", duplicate direction); diff --git a/src/type_internal.ml b/src/type_internal.ml index c2aa3e85..9b3eab6d 100644 --- a/src/type_internal.ml +++ b/src/type_internal.ml @@ -1683,7 +1683,22 @@ let initial_typ_env = External (Some "gteq_vec_signed"),[],pure_e,nob); ])); ("is_one",Base(([],(mk_pure_fun bit_t bit_t)),External (Some "is_one"),[],pure_e,nob)); - (*correct again*) + ("signed",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})], + (mk_pure_fun (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")) + (mk_atom (mk_nv "o")))), + External (Some "signed"), + [(GtEq(Specc(Parse_ast.Int("signed",None)),Guarantee, + mk_nv "o", {nexp = Nneg({nexp = N2n(mk_nv "m",None)})})); + (LtEq(Specc(Parse_ast.Int("signed",None)),Guarantee, + mk_nv "o", mk_sub {nexp = N2n(mk_nv "m",None)} n_one));],pure_e,nob)); + ("unsigned",Base((mk_nat_params["n";"m";"o"]@[("ord",{k=K_Ord})], + (mk_pure_fun (mk_vector bit_t (Ovar "ord") (Nvar "n") (Nvar "m")) + (mk_atom (mk_nv "o")))), + External (Some "unsigned"), + [(GtEq(Specc(Parse_ast.Int("unsigned",None)),Guarantee, + mk_nv "o", n_zero)); + (LtEq(Specc(Parse_ast.Int("unsigned",None)),Guarantee, + mk_nv "o", mk_sub {nexp = N2n(mk_nv "m",None)} n_one));],pure_e,nob)); mk_bitwise_op "bitwise_not" "~" 1; mk_bitwise_op "bitwise_or" "|" 2; mk_bitwise_op "bitwise_xor" "^" 2; |