Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Add a few more functions to bitstringSyntax.

  • Loading branch information...
commit b7f30f660ad431d5786612215814dad889f4f97c 1 parent 38a45c2
@acjf3 acjf3 authored
Showing with 31 additions and 0 deletions.
  1. +7 −0 src/n-bit/bitstringSyntax.sig
  2. +24 −0 src/n-bit/bitstringSyntax.sml
View
7 src/n-bit/bitstringSyntax.sig
@@ -33,6 +33,13 @@ sig
val padded_fixedwidth_of_int : int * int -> term
+ val dest_b : term -> bool
+
+ val mk_b : bool -> term
+ val mk_bit : int -> term
+ val mk_bstring : int -> int -> term
+ val mk_nvec : int -> int -> term
+ val mk_vec : int -> int -> term
val mk_fixedwidth : term * int -> term
val add_tm : term
View
24 src/n-bit/bitstringSyntax.sml
@@ -176,4 +176,28 @@ fun padded_fixedwidth_of_int (m, n) =
(* ----------------------------------------------------------------------- *)
+fun dest_b tm =
+ if tm = boolSyntax.T
+ then true
+ else if tm = boolSyntax.F
+ then false
+ else raise ERR "dest_b" ""
+
+fun mk_b b = if b then boolSyntax.T else boolSyntax.F
+
+fun mk_bit n = Term.mk_var ("b" ^ Int.toString n, Type.bool)
+
+(* Make term ``[b(n+w); ... ; b(n)]`` *)
+fun mk_bstring w n =
+ listSyntax.mk_list
+ (List.tabulate (w, fn i => mk_bit (w - i - 1 + n)), Type.bool)
+
+(* Make term ``v2w [b(n+w); ... ; b(n)] : w word`` *)
+fun mk_vec w n = mk_v2w (mk_bstring w n, fcpSyntax.mk_int_numeric_type w)
+
+(* Make term ``v2n [b(n+w); ... ; b(n)]`` *)
+fun mk_nvec w n = mk_v2n (mk_bstring w n)
+
+(* ----------------------------------------------------------------------- *)
+
end
Please sign in to comment.
Something went wrong with that request. Please try again.