diff options
| -rw-r--r-- | mips/prelude.sail | 8 | ||||
| -rw-r--r-- | riscv/prelude.sail | 10 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators.lem | 30 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_bitlists.lem | 16 | ||||
| -rw-r--r-- | src/gen_lib/sail_operators_mwords.lem | 16 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 22 |
6 files changed, 17 insertions, 85 deletions
diff --git a/mips/prelude.sail b/mips/prelude.sail index 152996f1..e0bcd8cf 100644 --- a/mips/prelude.sail +++ b/mips/prelude.sail @@ -242,10 +242,10 @@ infix 4 >=_s infix 4 <_u infix 4 >=_u -val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator <_s : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool function operator <_s (x, y) = signed(x) < signed(y) function operator >=_s (x, y) = signed(x) >= signed(y) diff --git a/riscv/prelude.sail b/riscv/prelude.sail index d667573e..c92497c1 100644 --- a/riscv/prelude.sail +++ b/riscv/prelude.sail @@ -350,11 +350,11 @@ infix 4 <_u infix 4 >=_u infix 4 <=_u -val operator <_s = {lem: "slt_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_s = {lem: "sgteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <_u = {lem: "ult_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator >=_u = {lem: "ugteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool -val operator <=_u = {lem: "ulteq_vec"} : forall 'n. (bits('n), bits('n)) -> bool +val operator <_s : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_s : forall 'n. (bits('n), bits('n)) -> bool +val operator <_u : forall 'n. (bits('n), bits('n)) -> bool +val operator >=_u : forall 'n. (bits('n), bits('n)) -> bool +val operator <=_u : forall 'n. (bits('n), bits('n)) -> bool function operator <_s (x, y) = signed(x) < signed(y) function operator >=_s (x, y) = signed(x) >= signed(y) diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem index 78aab65e..0c5da675 100644 --- a/src/gen_lib/sail_operators.lem +++ b/src/gen_lib/sail_operators.lem @@ -194,36 +194,6 @@ let neq_bv l r = not (eq_bv l r) let inline neq_mword l r = (l <> r) -val ult_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let ult_bv l r = lexicographicLess (List.reverse (bits_of l)) (List.reverse (bits_of r)) -let ulteq_bv l r = (eq_bv l r) || (ult_bv l r) -let ugt_bv l r = not (ulteq_bv l r) -let ugteq_bv l r = (eq_bv l r) || (ugt_bv l r) - -val slt_bv : forall 'a. Bitvector 'a => 'a -> 'a -> bool -let slt_bv l r = - match (most_significant l, most_significant r) with - | (B0, B0) -> ult_bv l r - | (B0, B1) -> false - | (B1, B0) -> true - | (B1, B1) -> - let l' = add_one_bit_ignore_overflow (bits_of l) in - let r' = add_one_bit_ignore_overflow (bits_of r) in - ugt_bv l' r' - | (BU, BU) -> ult_bv l r - | (BU, _) -> true - | (_, BU) -> false - end -let slteq_bv l r = (eq_bv l r) || (slt_bv l r) -let sgt_bv l r = not (slteq_bv l r) -let sgteq_bv l r = (eq_bv l r) || (sgt_bv l r) - -val ucmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool -let inline ucmp_mword cmp l r = cmp (unsignedIntegerFromWord l) (unsignedIntegerFromWord r) - -val scmp_mword : forall 'a. Size 'a => (integer -> integer -> bool) -> mword 'a -> mword 'a -> bool -let inline scmp_mword cmp l r = cmp (signedIntegerFromWord l) (signedIntegerFromWord r) - val get_slice_int_bv : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a let get_slice_int_bv len n lo = let hi = lo + len - 1 in diff --git a/src/gen_lib/sail_operators_bitlists.lem b/src/gen_lib/sail_operators_bitlists.lem index fed293b4..19e9b519 100644 --- a/src/gen_lib/sail_operators_bitlists.lem +++ b/src/gen_lib/sail_operators_bitlists.lem @@ -308,21 +308,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v = val eq_vec : list bitU -> list bitU -> bool val neq_vec : list bitU -> list bitU -> bool -val ult_vec : list bitU -> list bitU -> bool -val slt_vec : list bitU -> list bitU -> bool -val ugt_vec : list bitU -> list bitU -> bool -val sgt_vec : list bitU -> list bitU -> bool -val ulteq_vec : list bitU -> list bitU -> bool -val slteq_vec : list bitU -> list bitU -> bool -val ugteq_vec : list bitU -> list bitU -> bool -val sgteq_vec : list bitU -> list bitU -> bool let eq_vec = eq_bv let neq_vec = neq_bv -let ult_vec = ult_bv -let slt_vec = slt_bv -let ugt_vec = ugt_bv -let sgt_vec = sgt_bv -let ulteq_vec = ulteq_bv -let slteq_vec = slteq_bv -let ugteq_vec = ugteq_bv -let sgteq_vec = sgteq_bv diff --git a/src/gen_lib/sail_operators_mwords.lem b/src/gen_lib/sail_operators_mwords.lem index 077dfb02..22d5b246 100644 --- a/src/gen_lib/sail_operators_mwords.lem +++ b/src/gen_lib/sail_operators_mwords.lem @@ -329,21 +329,5 @@ let set_slice (out_len:ii) (slice_len:ii) out (n:ii) v = val eq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool val neq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ult_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val slt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ugt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val sgt_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ulteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val slteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val ugteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool -val sgteq_vec : forall 'a. Size 'a => mword 'a -> mword 'a -> bool let inline eq_vec = eq_mword let inline neq_vec = neq_mword -let inline ult_vec = ucmp_mword (<) -let inline slt_vec = scmp_mword (<) -let inline ugt_vec = ucmp_mword (>) -let inline sgt_vec = scmp_mword (>) -let inline ulteq_vec = ucmp_mword (<=) -let inline slteq_vec = scmp_mword (<=) -let inline ugteq_vec = ucmp_mword (>=) -let inline sgteq_vec = scmp_mword (>=) diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index c181249d..58bbfc4b 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -111,10 +111,7 @@ let rec fix_id remove_tick name = match name with let doc_id_lem (Id_aux(i,_)) = match i with | Id i -> string (fix_id false i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) + | DeIid x -> string (Util.zencode_string ("op " ^ x)) let doc_id_lem_type (Id_aux(i,_)) = match i with @@ -122,10 +119,7 @@ let doc_id_lem_type (Id_aux(i,_)) = | Id("nat") -> string "ii" | Id("option") -> string "maybe" | Id i -> string (fix_id false i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) + | DeIid x -> string (Util.zencode_string ("op " ^ x)) let doc_id_lem_ctor (Id_aux(i,_)) = match i with @@ -135,10 +129,11 @@ let doc_id_lem_ctor (Id_aux(i,_)) = | Id("Some") -> string "Just" | Id("None") -> string "Nothing" | Id i -> string (fix_id false (String.capitalize i)) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - separate space [colon; string (String.capitalize x); empty] + | DeIid x -> string (Util.zencode_string ("op " ^ x)) + +let deinfix = function + | Id_aux (Id v, l) -> Id_aux (DeIid v, l) + | Id_aux (DeIid v, l) -> Id_aux (DeIid v, l) let doc_var_lem kid = string (fix_id true (string_of_kid kid)) @@ -880,8 +875,7 @@ let doc_exp_lem, doc_let_lem = | E_assert (e1,e2) -> align (liftR (separate space [string "assert_exp"; expY e1; expY e2])) | E_app_infix (e1,id,e2) -> - raise (Reporting_basic.err_unreachable l - "E_app_infix should have been rewritten before pretty-printing") + expV aexp_needed (E_aux (E_app (deinfix id, [e1; e2]), (l, annot))) | E_var(lexp, eq_exp, in_exp) -> raise (report l "E_vars should have been removed before pretty-printing") | E_internal_plet (pat,e1,e2) -> |