1(* Copyright (C) 1997-2001 by Ken Friis Larsen and Jakob Lichtenberg. *)
2structure bvec :> bvec =
3struct
4
5    open MuddyCore
6
7    open bdd fdd
8
9    prim_type bvec
10    type const = int
11
12    val bvectrue: precision -> bvec = app1 (symb "mlbvec_true")
13    val bvecfalse: precision -> bvec = app1 (symb "mlbvec_false")
14    val con: precision -> const -> bvec = app2 (symb "mlbvec_con")
15
16    val var: precision -> varnum -> int -> bvec = app3 (symb "mlbvec_var")
17    val varfdd: fddvar -> bvec = app1 (symb "mlbvec_varfdd")
18
19    val coerce: precision -> bvec -> bvec = app2 (symb "mlbvec_coerce")
20
21    val isConst: bvec -> bool = app1 (symb "mlbvec_isconst")
22    val getConst: bvec -> const = app1 (symb "mlbvec_getconst")
23
24    fun lookupConst bvec =
25        if isConst bvec then SOME(getConst bvec) else NONE
26
27    val add: bvec * bvec -> bvec = cur2 (symb "mlbvec_add")
28    val sub: bvec * bvec -> bvec = cur2 (symb "mlbvec_sub")
29
30    val mul     : bvec * bvec -> bvec = cur2 (symb "mlbvec_mul")
31    val mulfixed: bvec * const -> bvec = cur2 (symb "mlbvec_mulfixed")
32
33    val op div : bvec * bvec -> bvec * bvec = cur2 (symb "mlbvec_div")
34    val divfixed: bvec * const -> bvec * bvec = cur2 (symb "mlbvec_divfixed")
35    val divi      = #1 o op div
36    val divifixed = #1 o divfixed
37    val modu      = #2 o op div
38    val modufixed = #2 o divfixed
39
40(*    val divifixed: bvec * const -> bvec = cur2 (symb "mlbvec_divi")
41    val modufixed: bvec * const -> bvec = cur2 (symb "mlbvec_modu")
42*)
43    val shl     : bvec -> bvec -> bdd -> bvec = app3 (symb "mlbvec_shl")
44    val shlfixed: bvec -> int -> bdd -> bvec = app3 (symb "mlbvec_shlfixed")
45
46    val shr     : bvec -> bvec -> bdd -> bvec = app3 (symb "mlbvec_shr")
47    val shrfixed: bvec -> int  -> bdd -> bvec = app3 (symb "mlbvec_shrfixed")
48
49    val lth: bvec * bvec -> bdd = cur2 (symb "mlbvec_lth")
50    val lte: bvec * bvec -> bdd = cur2 (symb "mlbvec_lte")
51    val gth: bvec * bvec -> bdd = cur2 (symb "mlbvec_gth")
52    val gte: bvec * bvec -> bdd = cur2 (symb "mlbvec_gte")
53    val equ: bvec * bvec -> bdd = cur2 (symb "mlbvec_equ")
54    val neq: bvec * bvec -> bdd = cur2 (symb "mlbvec_neq")
55end
56