1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
open import Pervasives
open import Interp
open import Interp_ast
import Maybe_extra
open import Num
open import List
open import Word
let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;
let compose f g x = f (V_tuple [g x]) ;;
let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
| L_one -> L_zero
| L_zero -> L_one end) la) ;;
let neq = compose neg eq ;;
let bit_to_bool b = match b with
V_lit (L_aux L_zero _) -> false
| V_lit (L_aux L_one _) -> true
end ;;
let bool_to_bit b = match b with
false -> V_lit (L_aux L_zero Unknown)
| true -> V_lit (L_aux L_one Unknown)
end ;;
(* BitSeq expects LSB first.
* By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
* hence MSB first.
* http://en.wikipedia.org/wiki/Bit_numbering *)
let to_num signed (V_vector idx inc l) =
(* Word library in Lem expects bitseq with LSB first *)
let l = if inc then reverse l else l in
(* Make sure the last bit is a zero to force unsigned numbers *)
let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
V_vector 0 true (map bool_to_bit (reverse l)) ;;
let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
V_vector 0 false (map bool_to_bit l) ;;
let rec add (V_tuple args) = match args with
| [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
end ;;
let rec vec_concat (V_tuple args) = match args with
| [V_vector n d l; V_vector n' d' l'] ->
(* XXX d = d' ? droping n' ? *)
V_vector n d (l ++ l')
| [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l; x])
| [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l])
end ;;
let function_map = [
("ignore", ignore_sail);
("add", add);
("eq", eq);
("vec_concat", vec_concat);
("is_one", is_one);
("to_num_inc", to_num false);
("to_num_dec", to_num false);
("exts", to_num true);
(* XXX the size of the target vector should be given by the interpreter *)
("to_vec_inc", to_vec_inc 64);
("to_vec_dec", to_vec_dec 64);
] ;;
let eval_external name v = (Maybe_extra.fromJust (List.lookup name function_map)) v ;;
|
